Commit 6b06e135 authored by wenzelm's avatar wenzelm
Browse files

standardized towards new-style formal comments: isabelle update_comments from...

standardized towards new-style formal comments: isabelle update_comments from Isabelle/f075640b8868;
parent cda7cc51c330
......@@ -900,7 +900,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -898,7 +898,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -898,7 +898,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -893,7 +893,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -898,7 +898,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -893,7 +893,7 @@ lemma seq_nhop_quality_increases':
and \<open>nsqn (rt (\<sigma> sip)) oip = osn \<longrightarrow> the (dhops (rt (\<sigma> sip)) oip) \<le> hops\<close>
show ?thesis by auto
next
-- "alternative to using @{text sip_not_ip}"
\<comment> \<open>alternative to using @{text sip_not_ip}\<close>
assume [simp]: "sip = i"
have "?rt1 = rt (\<sigma> i)"
proof (rule update_cases_kD, simp_all)
......
......@@ -137,11 +137,11 @@ qed
lemma is_bal_l_bal:
"is_bal l \<Longrightarrow> is_bal r \<Longrightarrow> height l = height r + 2 \<Longrightarrow> is_bal (l_bal\<^sub>0 n l r)"
by (cases l) (auto, auto split: tree\<^sub>0.split) -- "separating the two auto's is just for speed"
by (cases l) (auto, auto split: tree\<^sub>0.split) \<comment> \<open>separating the two auto's is just for speed\<close>
lemma is_bal_r_bal:
"is_bal l \<Longrightarrow> is_bal r \<Longrightarrow> height r = height l + 2 \<Longrightarrow> is_bal (r_bal\<^sub>0 n l r)"
by (cases r) (auto, auto split: tree\<^sub>0.split) -- "separating the two auto's is just for speed"
by (cases r) (auto, auto split: tree\<^sub>0.split) \<comment> \<open>separating the two auto's is just for speed\<close>
theorem is_bal_insrt:
"is_bal t \<Longrightarrow> is_bal(insrt\<^sub>0 x t)"
......
......@@ -11,7 +11,7 @@ typedecl proc
typedecl val
locale Consensus
-- {* To avoid name clashes *}
\<comment> \<open>To avoid name clashes\<close>
begin
fun \<delta>::"val option \<Rightarrow> (proc \<times> val) \<Rightarrow> val option" (infix "\<bullet>" 65) where
......
......@@ -165,9 +165,9 @@ fun P16 where
"P16 (s1,s2) = (dstate s2 \<noteq> \<bottom> \<longrightarrow> initialized s2)"
fun P17 where
-- {* For the Response1 case of the refinement proof, in case a response
\<comment> \<open>For the Response1 case of the refinement proof, in case a response
is produced in the first instance and the second instance is already
initialized *}
initialized\<close>
"P17 (s1,s2) = (initialized s2
\<longrightarrow> (\<forall> p .
((status s1 p = Ready
......@@ -1374,22 +1374,22 @@ theorem idempotence:
shows "((composition) =<| (ioa 0 id2))"
proof -
have same_input_sig:"inp (composition) = inp (ioa 0 id2)"
-- {*First we show that both automata have the same input and output signature*}
\<comment> \<open>First we show that both automata have the same input and output signature\<close>
using ids by auto
moreover
have same_output_sig:"out (composition) = out (ioa 0 id2)"
-- {*Then we show that output signatures match*}
\<comment> \<open>Then we show that output signatures match\<close>
using ids by auto
moreover
have "traces (composition) \<subseteq> traces (ioa 0 id2)"
-- {*Finally we show trace inclusion*}
\<comment> \<open>Finally we show trace inclusion\<close>
proof -
have "ext (composition) = ext (ioa 0 id2)"
-- {*First we show that they have the same external signature*}
\<comment> \<open>First we show that they have the same external signature\<close>
using same_input_sig and same_output_sig by simp
moreover
have "is_ref_map f (composition) (ioa 0 id2)"
-- {*Then we show that @{text f_comp} is a refinement mapping*}
\<comment> \<open>Then we show that @{text f_comp} is a refinement mapping\<close>
proof (auto simp only:is_ref_map_def)
fix s1 s2
assume 1:"(s1,s2) \<in> ioa.start (composition)"
......
......@@ -7,7 +7,7 @@ imports IOA RDR
begin
datatype ('a,'b,'c,'d)SLin_action =
-- {* The nat component is the instance number *}
\<comment> \<open>The nat component is the instance number\<close>
Invoke nat 'b 'c
| Response nat 'b 'd
| Switch nat 'b 'c 'a
......@@ -29,7 +29,7 @@ begin
definition
asig :: "nat \<Rightarrow> nat \<Rightarrow> ('a,'b,'c,'d)SLin_action signature"
-- {* The first instance has number 0 *}
\<comment> \<open>The first instance has number 0\<close>
where
"asig i j \<equiv> \<lparr>
inputs = {act . \<exists> p c iv i' .
......
......@@ -320,7 +320,7 @@ using e proof coinduct
ultimately show ?case by (auto intro: eff_S elim: epath.cases)
qed
end -- {* context RuleSystem *}
end \<comment> \<open>context RuleSystem\<close>
(*<*) (* Rule-persistent rule system *) (*>*)
......@@ -372,7 +372,7 @@ proof -
qed
end -- {* context PersistentRuleSystem *}
end \<comment> \<open>context PersistentRuleSystem\<close>
......@@ -382,7 +382,7 @@ section{* Code generation *}
locale RuleSystem_Code =
fixes eff' :: "'rule \<Rightarrow> 'state \<Rightarrow> 'state fset option"
and rules :: "'rule stream" -- {* countably many rules *}
and rules :: "'rule stream" \<comment> \<open>countably many rules\<close>
begin
definition "eff r s sl \<equiv> eff' r s = Some sl"
......
......@@ -10,7 +10,7 @@ imports
begin
text \<open>\label{sec:approxaffine}\<close>
lemma convex_on_imp_above_tangent:\<comment>\<open>TODO: generalizes @{thm convex_on_imp_above_tangent}\<close>
lemma convex_on_imp_above_tangent:\<comment> \<open>TODO: generalizes @{thm convex_on_imp_above_tangent}\<close>
assumes convex: "convex_on A f" and connected: "connected A"
assumes c: "c \<in> A" and x : "x \<in> A"
assumes deriv: "(f has_field_derivative f') (at c within A)"
......@@ -778,7 +778,7 @@ lemma aform_val_mult_exact:
using that
by (auto simp: pdevs_val_sum_less_degree[where d=d] aform_val_def algebra_simps)
lemma sum_times_bound:\<comment>\<open>TODO: this gives better bounds for the remainder of multiplication\<close>
lemma sum_times_bound:\<comment> \<open>TODO: this gives better bounds for the remainder of multiplication\<close>
"(\<Sum>i<d. e i * f i::real) * (\<Sum>i<d. e i * g i) =
(\<Sum>i<d. (e i)\<^sup>2 * (f i * g i)) +
(\<Sum>(i, j) | i < j \<and> j < d. (e i * e j) * (f j * g i + f i * g j))" for d::nat
......@@ -1861,7 +1861,7 @@ definition affine_unop :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarro
(y, ye) = trunc_bound_eucl p (ax + b);
(ys, yse) = trunc_bound_pdevs p (scaleR_pdevs a xs)
in ((y, ys), sum_list' p [truncate_up p (\<bar>a\<bar> * xe), axe, ye, yse, d]))"
\<comment>\<open>TODO: also do binop\<close>
\<comment> \<open>TODO: also do binop\<close>
lemma aform_err_leI:
"y \<in> aform_err e (c, d)"
......
......@@ -24,7 +24,7 @@ lemmas [derivative_intros] =
DERIV_compose_FDERIV[OF DERIV_real_sqrt]
DERIV_compose_FDERIV[OF floor_has_real_derivative]
lemma has_derivative_powr[derivative_intros]:\<comment>\<open>TODO: generalize @{thm DERIV_powr}?\<close>
lemma has_derivative_powr[derivative_intros]:\<comment> \<open>TODO: generalize @{thm DERIV_powr}?\<close>
assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
and f[derivative_intros]:"(f has_derivative f') (at x within X)"
assumes pos: "0 < g x" and "x \<in> X"
......
......@@ -108,7 +108,7 @@ qed
subsection \<open>Partial Deviations\<close>
typedef (overloaded) 'a pdevs = "{x::nat \<Rightarrow> 'a::zero. finite {i. x i \<noteq> 0}}"
\<comment>\<open>TODO: unify with polynomials\<close>
\<comment> \<open>TODO: unify with polynomials\<close>
morphisms pdevs_apply Abs_pdev
by (auto intro!: exI[where x="\<lambda>x. 0"])
......
......@@ -259,8 +259,8 @@ ML \<open>
fun iter f 0 = f ()
| iter f i = let val _ = f () in iter f (i - 1) end
\<close>
ML \<open>iter ri1 100\<close> \<comment>"0.7 s"
ML \<open>iter ri2 100\<close> \<comment>"1.3 s"
ML \<open>iter ri3 100\<close> \<comment>"1.3 s"
ML \<open>iter ri1 100\<close> \<comment> \<open>0.7 s\<close>
ML \<open>iter ri2 100\<close> \<comment> \<open>1.3 s\<close>
ML \<open>iter ri3 100\<close> \<comment> \<open>1.3 s\<close>
end
......@@ -751,7 +751,7 @@ notation blinfun_apply (infixl "$" 999)
end
lemma bounded_linear_via_derivative:
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector" \<comment>\<open>TODO: generalize?\<close>
fixes f::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector" \<comment> \<open>TODO: generalize?\<close>
assumes "\<And>i. ((\<lambda>x. blinfun_apply (f x) i) has_derivative (\<lambda>x. f' y x i)) (at y)"
shows "bounded_linear (f' y x)"
proof -
......
......@@ -203,7 +203,7 @@ lemma fold_const_fa[simp]: "interpret_floatarith (fold_const_fa fa) xs = interpr
subsection \<open>Free Variables\<close>
primrec max_Var_floatarith where\<comment>\<open>TODO: include bound in predicate\<close>
primrec max_Var_floatarith where\<comment> \<open>TODO: include bound in predicate\<close>
"max_Var_floatarith (Add a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (Mult a b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
| "max_Var_floatarith (Inverse a) = max_Var_floatarith a"
......@@ -700,7 +700,7 @@ lemma max_Var_floatarith_inner_floatariths[simp]:
definition FDERIV_floatarith where
"FDERIV_floatarith fa xs d = inner_floatariths (map (\<lambda>x. fold_const_fa (DERIV_floatarith x fa)) xs) d"
\<comment>\<open>TODO: specialize to \<open>FDERIV_floatarith fa [0..<n] [m..<m + n]\<close> and do the rest with @{term subst_floatarith}?
\<comment> \<open>TODO: specialize to \<open>FDERIV_floatarith fa [0..<n] [m..<m + n]\<close> and do the rest with @{term subst_floatarith}?
TODO: introduce approximation on type @{typ "real^'i^'j"} and use @{term jacobian}?\<close>
lemma interpret_floatariths_map: "interpret_floatariths (map f xs) vs = map (\<lambda>x. interpret_floatarith (f x) vs) xs"
......@@ -1309,7 +1309,7 @@ fun subterms :: "floatarith \<Rightarrow> floatarith set" where
lemma subterms_self[simp]: "fa2 \<in> subterms fa2"
by (induction fa2) auto
lemma interpret_floatarith_FDERIV_floatarith_eucl_of_env:\<comment>\<open>TODO: cleanup, reduce to DERIV?!\<close>
lemma interpret_floatarith_FDERIV_floatarith_eucl_of_env:\<comment> \<open>TODO: cleanup, reduce to DERIV?!\<close>
assumes iD: "\<And>i. i < DIM('a) \<Longrightarrow> isDERIV (xs ! i) fa vs"
assumes ds_fresh: "freshs_floatarith fa ds"
assumes [simp]: "length xs = DIM ('a)" "length ds = DIM ('a)"
......@@ -2197,11 +2197,11 @@ fun plain_floatarith::"nat \<Rightarrow> floatarith \<Rightarrow> bool" where
| "plain_floatarith N (floatarith.Max a b) \<longleftrightarrow> plain_floatarith N a \<and> plain_floatarith N b"
| "plain_floatarith N (floatarith.Min a b) \<longleftrightarrow> plain_floatarith N a \<and> plain_floatarith N b"
| "plain_floatarith N (floatarith.Power a n) \<longleftrightarrow> plain_floatarith N a"
| "plain_floatarith N (floatarith.Cos a) \<longleftrightarrow> False" \<comment>\<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Arctan a) \<longleftrightarrow> False" \<comment>\<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Cos a) \<longleftrightarrow> False" \<comment> \<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Arctan a) \<longleftrightarrow> False" \<comment> \<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Abs a) \<longleftrightarrow> plain_floatarith N a"
| "plain_floatarith N (floatarith.Exp a) \<longleftrightarrow> False" \<comment>\<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Sqrt a) \<longleftrightarrow> False" \<comment>\<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Exp a) \<longleftrightarrow> False" \<comment> \<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Sqrt a) \<longleftrightarrow> False" \<comment> \<open>TODO: should be plain!\<close>
| "plain_floatarith N (floatarith.Floor a) \<longleftrightarrow> plain_floatarith N a"
| "plain_floatarith N (floatarith.Powr a b) \<longleftrightarrow> False"
......
......@@ -190,7 +190,7 @@ definition shows_segments_of_aform
(polychain_of_segments (segments_of_aform (prod_of_aforms (xs ! a) (xs ! b)))))"
abbreviation "show_segments_of_aform a b x c \<equiv> shows_segments_of_aform a b x c ''''"
definition shows_box_of_aforms\<comment>\<open>box and some further information\<close>
definition shows_box_of_aforms\<comment> \<open>box and some further information\<close>
where "shows_box_of_aforms (XS::real aform list) = (let
RS = map (Radius' 20) XS;
l = map (Inf_aform' 20) XS;
......@@ -210,7 +210,7 @@ definition "generators XS =
in
(map fst XS, rs))"
definition shows_box_of_aforms_hr\<comment>\<open>human readable\<close>
definition shows_box_of_aforms_hr\<comment> \<open>human readable\<close>
where "shows_box_of_aforms_hr XS = (let
RS = map (Radius' 20) XS;
l = map (Inf_aform' 20) XS;
......@@ -221,7 +221,7 @@ where "shows_box_of_aforms_hr XS = (let
)"
abbreviation "show_box_of_aforms_hr x \<equiv> shows_box_of_aforms_hr x ''''"
definition shows_aforms_hr\<comment>\<open>human readable\<close>
definition shows_aforms_hr\<comment> \<open>human readable\<close>
where "shows_aforms_hr XS = shows (generators XS)"
abbreviation "show_aform_hr x \<equiv> shows_aforms_hr x ''''"
......
......@@ -39,8 +39,8 @@ since the present King of France does not exist. *}
text {* This problem can be avoided by introducing a null individual @{term "n"} to serve as the
reference of non-denoting definite descriptions, as follows: *}
typedecl i -- "the type of individuals"
consts n:: "i" ("n") -- "the null individual"
typedecl i \<comment> \<open>the type of individuals\<close>
consts n:: "i" ("n") \<comment> \<open>the null individual\<close>
text {* Then the universal and particular quantifiers can be restricted to
individuals excluding the null-individual as follows, where the new free quantifiers
......@@ -128,9 +128,9 @@ whereas the first two theorems depend only on the atomicity of identity. *}
section {* Anselm's Argument *}
text {* The argument proper employs the following non-logical vocabulary: *}
consts existence:: "i \<Rightarrow> bool" ("E") -- "exists in reality"
consts greater_than:: "i\<Rightarrow>i\<Rightarrow>bool" ("G") -- "is greater than"
consts conceivable:: "i\<Rightarrow>bool" ("C") -- "exists in the understanding"
consts existence:: "i \<Rightarrow> bool" ("E") \<comment> \<open>exists in reality\<close>
consts greater_than:: "i\<Rightarrow>i\<Rightarrow>bool" ("G") \<comment> \<open>is greater than\<close>
consts conceivable:: "i\<Rightarrow>bool" ("C") \<comment> \<open>exists in the understanding\<close>
text {* Note that @{term "E a"} is not intended by Oppenheimer and Zalta to be equivalent to
@{term "\<^bold>\<exists> x. a = x"} since according to their reading of the argument, some things do not exist
in reality @{cite "oppenheimer_logic_1991"}, p. 514. *}
......@@ -169,14 +169,14 @@ text {* With this vocabulary in place, Anselm's ontological argument, as reconst
Oppenheimer and Zalta, can be stated as follows: *}
theorem
assumes premise_1: "\<^bold>\<exists> x. \<Phi> x"
-- "there exists in the understanding a being greater than which
none can be conceived"
\<comment> \<open>there exists in the understanding a being greater than which
none can be conceived\<close>
and premise_2: "\<not> E (\<^bold>\<tau> x. \<Phi> x) \<longrightarrow> (\<^bold>\<exists> y. G y (\<^bold>\<tau> x. \<Phi> x) \<and> C y)"
-- "if the being greater than which none can be conceived does not exist in reality,
\<comment> \<open>if the being greater than which none can be conceived does not exist in reality,
then a being exists in the understanding which is greater than the being greater than
which none can be conceived"
which none can be conceived\<close>
and connectivity: "\<^bold>\<forall> x. \<^bold>\<forall> y. G x y \<or> G y x \<or> x \<^bold>= y"
shows "E g" -- "God exists."
shows "E g" \<comment> \<open>God exists.\<close>
text {* Isabelle can verify the argument in one line with the command @{text "using premise_1 premise_2 connectivity lemma_1 g_def description_theorem_1 by smt"}.
But since proofs in Isabelle using @{text "smt"} are currently considered impermanent, I instead give Zalta
......
......@@ -64,6 +64,6 @@ qed (simp add: some_ap_option ap_some_option)
lemma map_option_ap_conv[applicative_unfold]: "map_option f x = ap_option (pure f) x"
by (cases x rule: option.exhaust) simp_all
no_adhoc_overloading Applicative.pure pure_option -- \<open>We do not want to print all occurrences of @{const "Some"} as @{const "pure"}\<close>
no_adhoc_overloading Applicative.pure pure_option \<comment> \<open>We do not want to print all occurrences of @{const "Some"} as @{const "pure"}\<close>
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment