--- a/src/ZF/AC/AC_Equiv.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Mon Dec 07 10:23:50 2015 +0100
@@ -124,7 +124,7 @@
assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =
(\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
- --"AC18 cannot be expressed within the object-logic"
+ \<comment>"AC18 cannot be expressed within the object-logic"
definition
"AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =
--- a/src/ZF/Arith.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Arith.thy Mon Dec 07 10:23:50 2015 +0100
@@ -85,7 +85,7 @@
lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
-subsection\<open>@{text natify}, the Coercion to @{term nat}\<close>
+subsection\<open>\<open>natify\<close>, the Coercion to @{term nat}\<close>
lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
by (unfold pred_def, auto)
@@ -324,7 +324,7 @@
lemma add_lt_mono2: "[| i<j; j\<in>nat |] ==> k#+i < k#+j"
by (simp add: add_commute [of k] add_lt_mono1)
-text\<open>A [clumsy] way of lifting < monotonicity to @{text "\<le>"} monotonicity\<close>
+text\<open>A [clumsy] way of lifting < monotonicity to \<open>\<le>\<close> monotonicity\<close>
lemma Ord_lt_mono_imp_le_mono:
assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
and ford: "!!i. i:k ==> Ord(f(i))"
@@ -335,13 +335,13 @@
apply (blast intro!: leCI lt_mono ford elim!: leE)
done
-text\<open>@{text "\<le>"} monotonicity, 1st argument\<close>
+text\<open>\<open>\<le>\<close> monotonicity, 1st argument\<close>
lemma add_le_mono1: "[| i \<le> j; j\<in>nat |] ==> i#+k \<le> j#+k"
apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck)
apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
done
-text\<open>@{text "\<le>"} monotonicity, both arguments\<close>
+text\<open>\<open>\<le>\<close> monotonicity, both arguments\<close>
lemma add_le_mono: "[| i \<le> j; k \<le> l; j\<in>nat; l\<in>nat |] ==> i#+k \<le> j#+l"
apply (rule add_le_mono1 [THEN le_trans], assumption+)
apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
--- a/src/ZF/ArithSimp.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ArithSimp.thy Mon Dec 07 10:23:50 2015 +0100
@@ -264,7 +264,7 @@
by (cut_tac n = 0 in mod2_add_more, auto)
-subsection\<open>Additional theorems about @{text "\<le>"}\<close>
+subsection\<open>Additional theorems about \<open>\<le>\<close>\<close>
lemma add_le_self: "m:nat ==> m \<le> (m #+ n)"
apply (simp (no_asm_simp))
--- a/src/ZF/Bin.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Bin.thy Mon Dec 07 10:23:50 2015 +0100
@@ -697,7 +697,7 @@
subsection \<open>examples:\<close>
-text \<open>@{text combine_numerals_prod} (products of separate literals)\<close>
+text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
lemma "#5 $* x $* #3 = y" apply simp oops
schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops
--- a/src/ZF/Cardinal.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Cardinal.thy Mon Dec 07 10:23:50 2015 +0100
@@ -439,10 +439,10 @@
proof (unfold cardinal_def)
show "Card(\<mu> i. i \<approx> A)"
proof (cases "\<exists>i. Ord (i) & i \<approx> A")
- case False thus ?thesis --\<open>degenerate case\<close>
+ case False thus ?thesis \<comment>\<open>degenerate case\<close>
by (simp add: Least_0 Card_0)
next
- case True --\<open>real case: @{term A} is isomorphic to some ordinal\<close>
+ case True \<comment>\<open>real case: @{term A} is isomorphic to some ordinal\<close>
then obtain i where i: "Ord(i)" "i \<approx> A" by blast
show ?thesis
proof (rule CardI [OF Ord_Least], rule notI)
@@ -490,7 +490,7 @@
thus ?thesis by simp
qed
-text\<open>Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of @{text cardinal_mono} fails!\<close>
+text\<open>Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of \<open>cardinal_mono\<close> fails!\<close>
lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"
apply (rule Ord_linear2 [of i j], assumption+)
apply (erule lt_trans2 [THEN lt_irrefl])
@@ -687,7 +687,7 @@
thus ?thesis by auto
qed
-text\<open>A slightly weaker version of @{text nat_eqpoll_iff}\<close>
+text\<open>A slightly weaker version of \<open>nat_eqpoll_iff\<close>\<close>
lemma Ord_nat_eqpoll_iff:
assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
using i nat_into_Ord [OF n]
@@ -1109,7 +1109,7 @@
next
case (succ x)
hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)"
- by (simp add: wf_on_def wf_def) --\<open>not easy to erase the duplicate @{term"z \<in> x"}!\<close>
+ by (simp add: wf_on_def wf_def) \<comment>\<open>not easy to erase the duplicate @{term"z \<in> x"}!\<close>
show ?case
proof (rule wf_onI)
fix Z u
--- a/src/ZF/CardinalArith.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/CardinalArith.thy Mon Dec 07 10:23:50 2015 +0100
@@ -28,14 +28,14 @@
definition
jump_cardinal :: "i=>i" where
- --\<open>This def is more complex than Kunen's but it more easily proved to
+ \<comment>\<open>This def is more complex than Kunen's but it more easily proved to
be a cardinal\<close>
"jump_cardinal(K) ==
\<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
definition
csucc :: "i=>i" where
- --\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
+ \<comment>\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
of @{term K}\<close>
"csucc(K) == \<mu> L. Card(L) & K<L"
@@ -574,7 +574,7 @@
finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .
qed
-text\<open>Kunen: "... so the order type is @{text"\<le>"} K"\<close>
+text\<open>Kunen: "... so the order type is \<open>\<le>\<close> K"\<close>
lemma ordertype_csquare_le:
assumes IK: "InfCard(K)" and eq: "\<And>y. y\<in>K \<Longrightarrow> InfCard(y) \<Longrightarrow> y \<otimes> y = y"
shows "ordertype(K*K, csquare_rel(K)) \<le> K"
--- a/src/ZF/Cardinal_AC.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Cardinal_AC.thy Mon Dec 07 10:23:50 2015 +0100
@@ -222,7 +222,7 @@
note lt_subset_trans [OF _ _ OU, trans]
show ?thesis
proof (cases "W=0")
- case True --\<open>solve the easy 0 case\<close>
+ case True \<comment>\<open>solve the easy 0 case\<close>
thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
next
case False
--- a/src/ZF/Constructible/AC_in_L.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Mon Dec 07 10:23:50 2015 +0100
@@ -145,7 +145,7 @@
nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k)
enumerates the triangular numbers and can be defined by triangle(0)=0,
triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is
-needed to show that f is a bijection. We already know that such a bijection exists by the theorem @{text well_ord_InfCard_square_eq}:
+needed to show that f is a bijection. We already know that such a bijection exists by the theorem \<open>well_ord_InfCard_square_eq\<close>:
@{thm[display] well_ord_InfCard_square_eq[no_vars]}
However, this result merely states that there is a bijection between the two
@@ -233,20 +233,20 @@
definition
env_form_r :: "[i,i,i]=>i" where
- --\<open>wellordering on (environment, formula) pairs\<close>
+ \<comment>\<open>wellordering on (environment, formula) pairs\<close>
"env_form_r(f,r,A) ==
rmult(list(A), rlist(A, r),
formula, measure(formula, enum(f)))"
definition
env_form_map :: "[i,i,i,i]=>i" where
- --\<open>map from (environment, formula) pairs to ordinals\<close>
+ \<comment>\<open>map from (environment, formula) pairs to ordinals\<close>
"env_form_map(f,r,A,z)
== ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
definition
DPow_ord :: "[i,i,i,i,i]=>o" where
- --\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close>
+ \<comment>\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close>
"DPow_ord(f,r,A,X,k) ==
\<exists>env \<in> list(A). \<exists>p \<in> formula.
arity(p) \<le> succ(length(env)) &
@@ -255,12 +255,12 @@
definition
DPow_least :: "[i,i,i,i]=>i" where
- --\<open>function yielding the smallest index for @{term X}\<close>
+ \<comment>\<open>function yielding the smallest index for @{term X}\<close>
"DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
definition
DPow_r :: "[i,i,i]=>i" where
- --\<open>a wellordering on @{term "DPow(A)"}\<close>
+ \<comment>\<open>a wellordering on @{term "DPow(A)"}\<close>
"DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"
@@ -332,7 +332,7 @@
definition
rlimit :: "[i,i=>i]=>i" where
- --\<open>Expresses the wellordering at limit ordinals. The conditional
+ \<comment>\<open>Expresses the wellordering at limit ordinals. The conditional
lets us remove the premise @{term "Limit(i)"} from some theorems.\<close>
"rlimit(i,r) ==
if Limit(i) then
@@ -344,7 +344,7 @@
definition
Lset_new :: "i=>i" where
- --\<open>This constant denotes the set of elements introduced at level
+ \<comment>\<open>This constant denotes the set of elements introduced at level
@{term "succ(i)"}\<close>
"Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
--- a/src/ZF/Constructible/DPow_absolute.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Mon Dec 07 10:23:50 2015 +0100
@@ -238,7 +238,7 @@
done
-subsection\<open>Instantiating the Locale @{text M_DPow}\<close>
+subsection\<open>Instantiating the Locale \<open>M_DPow\<close>\<close>
subsubsection\<open>The Instance of Separation\<close>
@@ -510,7 +510,7 @@
definition
is_Lset :: "[i=>o, i, i] => o" where
- --\<open>We can use the term language below because @{term is_Lset} will
+ \<comment>\<open>We can use the term language below because @{term is_Lset} will
not have to be internalized: it isn't used in any instance of
separation.\<close>
"is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
@@ -531,7 +531,7 @@
done
-subsection\<open>Instantiating the Locale @{text M_Lset}\<close>
+subsection\<open>Instantiating the Locale \<open>M_Lset\<close>\<close>
subsubsection\<open>The First Instance of Replacement\<close>
@@ -570,7 +570,7 @@
is_DPow'(##Lset(i),gy,z), r) &
big_union(##Lset(i),r,u), mr, v, y))]"
apply (simp only: rex_setclass_is_bex [symmetric])
- --\<open>Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
+ \<comment>\<open>Convert \<open>\<exists>y\<in>Lset(i)\<close> to \<open>\<exists>y[##Lset(i)]\<close> within the body
of the @{term is_wfrec} application.\<close>
apply (intro FOL_reflections function_reflections
is_wfrec_reflection Replace_reflection DPow'_reflection)
@@ -593,7 +593,7 @@
done
-subsubsection\<open>Actually Instantiating @{text M_Lset}\<close>
+subsubsection\<open>Actually Instantiating \<open>M_Lset\<close>\<close>
lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
apply (rule M_Lset_axioms.intro)
--- a/src/ZF/Constructible/Datatype_absolute.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy Mon Dec 07 10:23:50 2015 +0100
@@ -493,7 +493,7 @@
list_replacement2' relation1_def
iterates_closed [of "is_list_functor(M,A)"])
-text\<open>WARNING: use only with @{text "dest:"} or with variables fixed!\<close>
+text\<open>WARNING: use only with \<open>dest:\<close> or with variables fixed!\<close>
lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
lemma (in M_datatypes) list_N_abs [simp]:
@@ -574,7 +574,7 @@
done
-subsection\<open>Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator\<close>
+subsection\<open>Absoluteness for \<open>\<epsilon>\<close>-Closure: the @{term eclose} Operator\<close>
text\<open>Re-expresses eclose using "iterates"\<close>
lemma eclose_eq_Union:
@@ -664,7 +664,7 @@
wfrec_replacement(M,MH,mesa)"
text\<open>The condition @{term "Ord(i)"} lets us use the simpler
- @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
+ \<open>trans_wfrec_abs\<close> rather than \<open>trans_wfrec_abs\<close>,
which I haven't even proved yet.\<close>
theorem (in M_eclose) transrec_abs:
"[|transrec_replacement(M,MH,i); relation2(M,MH,H);
@@ -765,7 +765,7 @@
definition
is_Member :: "[i=>o,i,i,i] => o" where
- --\<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close>
+ \<comment>\<open>because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}\<close>
"is_Member(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
@@ -779,7 +779,7 @@
definition
is_Equal :: "[i=>o,i,i,i] => o" where
- --\<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close>
+ \<comment>\<open>because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}\<close>
"is_Equal(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
@@ -792,7 +792,7 @@
definition
is_Nand :: "[i=>o,i,i,i] => o" where
- --\<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close>
+ \<comment>\<open>because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}\<close>
"is_Nand(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
@@ -805,7 +805,7 @@
definition
is_Forall :: "[i=>o,i,i] => o" where
- --\<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close>
+ \<comment>\<open>because @{term "Forall(x) \<equiv> Inr(Inr(p))"}\<close>
"is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
lemma (in M_trivial) Forall_abs [simp]:
@@ -821,7 +821,7 @@
definition
formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i" where
- --\<open>the instance of @{term formula_case} in @{term formula_rec}\<close>
+ \<comment>\<open>the instance of @{term formula_case} in @{term formula_rec}\<close>
"formula_rec_case(a,b,c,d,h) ==
formula_case (a, b,
\<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
@@ -881,7 +881,7 @@
definition
is_formula_case ::
"[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" where
- --\<open>no constraint on non-formulas\<close>
+ \<comment>\<open>no constraint on non-formulas\<close>
"is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
(\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) \<longrightarrow> finite_ordinal(M,y) \<longrightarrow>
is_Member(M,x,y,p) \<longrightarrow> is_a(x,y,z)) &
@@ -915,7 +915,7 @@
definition
is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" where
- --\<open>predicate to relativize the functional @{term formula_rec}\<close>
+ \<comment>\<open>predicate to relativize the functional @{term formula_rec}\<close>
"is_formula_rec(M,MH,p,z) ==
\<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
--- a/src/ZF/Constructible/Formula.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Formula.thy Mon Dec 07 10:23:50 2015 +0100
@@ -505,13 +505,13 @@
subsection\<open>Internalized Formulas for the Ordinals\<close>
-text\<open>The @{text sats} theorems below differ from the usual form in that they
+text\<open>The \<open>sats\<close> theorems below differ from the usual form in that they
include an element of absoluteness. That is, they relate internalized
formulas to real concepts such as the subset relation, rather than to the
-relativized concepts defined in theory @{text Relative}. This lets us prove
-the theorem as @{text Ords_in_DPow} without first having to instantiate the
-locale @{text M_trivial}. Note that the present theory does not even take
-@{text Relative} as a parent.\<close>
+relativized concepts defined in theory \<open>Relative\<close>. This lets us prove
+the theorem as \<open>Ords_in_DPow\<close> without first having to instantiate the
+locale \<open>M_trivial\<close>. Note that the present theory does not even take
+\<open>Relative\<close> as a parent.\<close>
subsubsection\<open>The subset relation\<close>
@@ -578,7 +578,7 @@
done
text\<open>The subset consisting of the ordinals is definable. Essential lemma for
-@{text Ord_in_Lset}. This result is the objective of the present subsection.\<close>
+\<open>Ord_in_Lset\<close>. This result is the objective of the present subsection.\<close>
theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
apply (simp add: DPow_def Collect_subset)
apply (rule_tac x=Nil in bexI)
@@ -594,7 +594,7 @@
"Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
definition
- L :: "i=>o" where --\<open>Kunen's definition VI 1.5, page 167\<close>
+ L :: "i=>o" where \<comment>\<open>Kunen's definition VI 1.5, page 167\<close>
"L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
text\<open>NOT SUITABLE FOR REWRITING -- RECURSIVE!\<close>
@@ -837,7 +837,7 @@
text\<open>The rank function for the constructible universe\<close>
definition
- lrank :: "i=>i" where --\<open>Kunen's definition VI 1.7\<close>
+ lrank :: "i=>i" where \<comment>\<open>Kunen's definition VI 1.7\<close>
"lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
--- a/src/ZF/Constructible/Internalize.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Internalize.thy Mon Dec 07 10:23:50 2015 +0100
@@ -634,7 +634,7 @@
text\<open>The additional variable in the premise, namely @{term f'}, is essential.
It lets @{term MH} depend upon @{term x}, which seems often necessary.
-The same thing occurs in @{text is_wfrec_reflection}.\<close>
+The same thing occurs in \<open>is_wfrec_reflection\<close>.\<close>
theorem is_recfun_reflection:
assumes MH_reflection:
"!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
--- a/src/ZF/Constructible/L_axioms.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Mon Dec 07 10:23:50 2015 +0100
@@ -6,7 +6,7 @@
theory L_axioms imports Formula Relative Reflection MetaExists begin
-text \<open>The class L satisfies the premises of locale @{text M_trivial}\<close>
+text \<open>The class L satisfies the premises of locale \<open>M_trivial\<close>\<close>
lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
apply (insert Transset_Lset)
@@ -78,7 +78,7 @@
apply (simp_all add: Replace_iff univalent_def, blast)
done
-subsection\<open>Instantiating the locale @{text M_trivial}\<close>
+subsection\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
text\<open>No instances of Separation yet.\<close>
lemma Lset_mono_le: "mono_le_subset(Lset)"
@@ -110,7 +110,7 @@
...and dozens of similar ones.
*)
-subsection\<open>Instantiation of the locale @{text reflection}\<close>
+subsection\<open>Instantiation of the locale \<open>reflection\<close>\<close>
text\<open>instances of locale constants\<close>
@@ -224,7 +224,7 @@
done
text\<open>This version handles an alternative form of the bounded quantifier
- in the second argument of @{text REFLECTS}.\<close>
+ in the second argument of \<open>REFLECTS\<close>.\<close>
theorem Rex_reflection':
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
@@ -564,11 +564,11 @@
subsubsection\<open>Variants of Satisfaction Definitions for Ordinals, etc.\<close>
-text\<open>The @{text sats} theorems below are standard versions of the ones proved
-in theory @{text Formula}. They relate elements of type @{term formula} to
+text\<open>The \<open>sats\<close> theorems below are standard versions of the ones proved
+in theory \<open>Formula\<close>. They relate elements of type @{term formula} to
relativized concepts such as @{term subset} or @{term ordinal} rather than to
real concepts such as @{term Ord}. Now that we have instantiated the locale
-@{text M_trivial}, we no longer require the earlier versions.\<close>
+\<open>M_trivial\<close>, we no longer require the earlier versions.\<close>
lemma sats_subset_fm':
"[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
--- a/src/ZF/Constructible/Normal.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Normal.thy Mon Dec 07 10:23:50 2015 +0100
@@ -80,8 +80,8 @@
text\<open>The constructions below come from Kunen, \emph{Set Theory}, page 78.\<close>
locale cub_family =
fixes P and A
- fixes next_greater -- "the next ordinal satisfying class @{term A}"
- fixes sup_greater -- "sup of those ordinals over all @{term A}"
+ fixes next_greater \<comment> "the next ordinal satisfying class @{term A}"
+ fixes sup_greater \<comment> "sup of those ordinals over all @{term A}"
assumes closed: "a\<in>A ==> Closed(P(a))"
and unbounded: "a\<in>A ==> Unbounded(P(a))"
and A_non0: "A\<noteq>0"
@@ -335,7 +335,7 @@
apply (frule lt_Ord)
apply (simp add: iterates_omega_def)
apply (rule increasing_LimitI)
- --"this lemma is @{thm increasing_LimitI [no_vars]}"
+ \<comment>"this lemma is @{thm increasing_LimitI [no_vars]}"
apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord
Ord_UN Ord_iterates lt_imp_0_lt
iterates_Normal_increasing, clarify)
@@ -382,11 +382,11 @@
Normal_imp_fp_Unbounded)
-subsubsection\<open>Function @{text normalize}\<close>
+subsubsection\<open>Function \<open>normalize\<close>\<close>
-text\<open>Function @{text normalize} maps a function @{text F} to a
+text\<open>Function \<open>normalize\<close> maps a function \<open>F\<close> to a
normal function that bounds it above. The result is normal if and
- only if @{text F} is continuous: succ is not bounded above by any
+ only if \<open>F\<close> is continuous: succ is not bounded above by any
normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
\<close>
definition
--- a/src/ZF/Constructible/Rank.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Rank.thy Mon Dec 07 10:23:50 2015 +0100
@@ -15,7 +15,7 @@
==> separation (M, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[M]. (\<exists>p[M].
fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
and obase_separation:
- --\<open>part of the order type formalization\<close>
+ \<comment>\<open>part of the order type formalization\<close>
"[| M(A); M(r) |]
==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
@@ -92,7 +92,7 @@
text\<open>Following Kunen's Theorem I 7.6, page 17. Note that this material is
not required elsewhere.\<close>
-text\<open>Can't use @{text well_ord_iso_preserving} because it needs the
+text\<open>Can't use \<open>well_ord_iso_preserving\<close> because it needs the
strong premise @{term "well_ord(A,r)"}\<close>
lemma (in M_ordertype) ord_iso_pred_imp_lt:
"[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
@@ -114,7 +114,7 @@
apply (frule restrict_ord_iso2, assumption+)
apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun])
apply (frule apply_type, blast intro: ltD)
- --\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
+ \<comment>\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
apply (simp add: pred_iff)
apply (subgoal_tac
"\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r,
@@ -137,26 +137,26 @@
definition
obase :: "[i=>o,i,i] => i" where
- --\<open>the domain of @{text om}, eventually shown to equal @{text A}\<close>
+ \<comment>\<open>the domain of \<open>om\<close>, eventually shown to equal \<open>A\<close>\<close>
"obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) &
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
definition
omap :: "[i=>o,i,i,i] => o" where
- --\<open>the function that maps wosets to order types\<close>
+ \<comment>\<open>the function that maps wosets to order types\<close>
"omap(M,A,r,f) ==
\<forall>z[M].
z \<in> f \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) &
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
definition
- otype :: "[i=>o,i,i,i] => o" where --\<open>the order types themselves\<close>
+ otype :: "[i=>o,i,i,i] => o" where \<comment>\<open>the order types themselves\<close>
"otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
text\<open>Can also be proved with the premise @{term "M(z)"} instead of
@{term "M(f)"}, but that version is less useful. This lemma
- is also more useful than the definition, @{text omap_def}.\<close>
+ is also more useful than the definition, \<open>omap_def\<close>.\<close>
lemma (in M_ordertype) omap_iff:
"[| omap(M,A,r,f); M(A); M(f) |]
==> z \<in> f \<longleftrightarrow>
@@ -478,7 +478,7 @@
-text\<open>@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF\<close>
+text\<open>\<open>is_oadd_fun\<close>: Relating the pure "language of set theory" to Isabelle/ZF\<close>
lemma (in M_ord_arith) is_oadd_fun_iff:
"[| a\<le>j; M(i); M(j); M(a); M(f) |]
==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
@@ -602,7 +602,7 @@
"[| M(i); M(x); M(g); function(g) |]
==> M(THE z. omult_eqns(i, x, g, z))"
apply (case_tac "Ord(x)")
- prefer 2 apply (simp add: omult_eqns_Not) --\<open>trivial, non-Ord case\<close>
+ prefer 2 apply (simp add: omult_eqns_Not) \<comment>\<open>trivial, non-Ord case\<close>
apply (erule Ord_cases)
apply (simp add: omult_eqns_0)
apply (simp add: omult_eqns_succ apply_closed oadd_closed)
@@ -897,12 +897,12 @@
apply (frule is_recfun_restrict [of concl: "r^+" a])
apply (rule trans_trancl, assumption)
apply (simp_all add: r_into_trancl trancl_subset_times)
-txt\<open>Still the same goal, but with new @{text is_recfun} assumptions.\<close>
+txt\<open>Still the same goal, but with new \<open>is_recfun\<close> assumptions.\<close>
apply (simp add: wellfoundedrank_eq)
apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
apply (simp_all add: transM [of a])
txt\<open>We have used equations for wellfoundedrank and now must use some
- for @{text is_recfun}.\<close>
+ for \<open>is_recfun\<close>.\<close>
apply (rule_tac a=a in rangeI)
apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
r_into_trancl apply_recfun r_into_trancl)
--- a/src/ZF/Constructible/Rank_Separation.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Mon Dec 07 10:23:50 2015 +0100
@@ -9,10 +9,10 @@
text\<open>This theory proves all instances needed for locales
- @{text "M_ordertype"} and @{text "M_wfrank"}. But the material is not
+ \<open>M_ordertype\<close> and \<open>M_wfrank\<close>. But the material is not
needed for proving the relative consistency of AC.\<close>
-subsection\<open>The Locale @{text "M_ordertype"}\<close>
+subsection\<open>The Locale \<open>M_ordertype\<close>\<close>
subsubsection\<open>Separation for Order-Isomorphisms\<close>
@@ -46,7 +46,7 @@
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma obase_separation:
- --\<open>part of the order type formalization\<close>
+ \<comment>\<open>part of the order type formalization\<close>
"[| L(A); L(r) |]
==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
@@ -109,7 +109,7 @@
-subsection\<open>Instantiating the locale @{text M_ordertype}\<close>
+subsection\<open>Instantiating the locale \<open>M_ordertype\<close>\<close>
text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions
such as intersection, Cartesian Product and image.\<close>
@@ -127,7 +127,7 @@
done
-subsection\<open>The Locale @{text "M_wfrank"}\<close>
+subsection\<open>The Locale \<open>M_wfrank\<close>\<close>
subsubsection\<open>Separation for @{term "wfrank"}\<close>
@@ -182,7 +182,7 @@
done
-subsubsection\<open>Separation for Proving @{text Ord_wfrank_range}\<close>
+subsubsection\<open>Separation for Proving \<open>Ord_wfrank_range\<close>\<close>
lemma Ord_wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) \<longrightarrow>
@@ -213,7 +213,7 @@
done
-subsubsection\<open>Instantiating the locale @{text M_wfrank}\<close>
+subsubsection\<open>Instantiating the locale \<open>M_wfrank\<close>\<close>
lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)"
apply (rule M_wfrank_axioms.intro)
--- a/src/ZF/Constructible/Rec_Separation.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Mon Dec 07 10:23:50 2015 +0100
@@ -6,14 +6,13 @@
theory Rec_Separation imports Separation Internalize begin
-text\<open>This theory proves all instances needed for locales @{text
-"M_trancl"} and @{text "M_datatypes"}\<close>
+text\<open>This theory proves all instances needed for locales \<open>M_trancl\<close> and \<open>M_datatypes\<close>\<close>
lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
by simp
-subsection\<open>The Locale @{text "M_trancl"}\<close>
+subsection\<open>The Locale \<open>M_trancl\<close>\<close>
subsubsection\<open>Separation for Reflexive/Transitive Closure\<close>
@@ -152,7 +151,7 @@
done
-subsubsection\<open>Separation for the Proof of @{text "wellfounded_on_trancl"}\<close>
+subsubsection\<open>Separation for the Proof of \<open>wellfounded_on_trancl\<close>\<close>
lemma wellfounded_trancl_reflects:
"REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
@@ -175,7 +174,7 @@
done
-subsubsection\<open>Instantiating the locale @{text M_trancl}\<close>
+subsubsection\<open>Instantiating the locale \<open>M_trancl\<close>\<close>
lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
apply (rule M_trancl_axioms.intro)
@@ -356,7 +355,7 @@
done
-subsubsection\<open>Instantiating the locale @{text M_datatypes}\<close>
+subsubsection\<open>Instantiating the locale \<open>M_datatypes\<close>\<close>
lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
apply (rule M_datatypes_axioms.intro)
@@ -422,7 +421,7 @@
done
-subsubsection\<open>Instantiating the locale @{text M_eclose}\<close>
+subsubsection\<open>Instantiating the locale \<open>M_eclose\<close>\<close>
lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
apply (rule M_eclose_axioms.intro)
--- a/src/ZF/Constructible/Reflection.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Reflection.thy Mon Dec 07 10:23:50 2015 +0100
@@ -19,15 +19,15 @@
subsection\<open>Basic Definitions\<close>
-text\<open>First part: the cumulative hierarchy defining the class @{text M}.
-To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
-closed under ordered pairing provided @{text l} is limit. Possibly this
+text\<open>First part: the cumulative hierarchy defining the class \<open>M\<close>.
+To avoid handling multiple arguments, we assume that \<open>Mset(l)\<close> is
+closed under ordered pairing provided \<open>l\<close> is limit. Possibly this
could be avoided: the induction hypothesis @{term Cl_reflects}
-(in locale @{text ex_reflection}) could be weakened to
+(in locale \<open>ex_reflection\<close>) could be weakened to
@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)"}, removing most
uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since
-ultimately the @{text ex_reflection} proof is packaged up using the
-predicate @{text Reflects}.
+ultimately the \<open>ex_reflection\<close> proof is packaged up using the
+predicate \<open>Reflects\<close>.
\<close>
locale reflection =
fixes Mset and M and Reflects
@@ -38,9 +38,9 @@
defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)"
and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))"
- fixes F0 --\<open>ordinal for a specific value @{term y}\<close>
- fixes FF --\<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close>
- fixes ClEx --\<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close>
+ fixes F0 \<comment>\<open>ordinal for a specific value @{term y}\<close>
+ fixes FF \<comment>\<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close>
+ fixes ClEx \<comment>\<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close>
defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) \<longrightarrow>
(\<exists>z\<in>Mset(b). P(<y,z>))"
and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
@@ -51,7 +51,7 @@
apply (simp add: mono_le_subset_def leI)
done
-text\<open>Awkward: we need a version of @{text ClEx_def} as an equality
+text\<open>Awkward: we need a version of \<open>ClEx_def\<close> as an equality
at the level of classes, which do not really exist\<close>
lemma (in reflection) ClEx_eq:
"ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a"
@@ -136,9 +136,9 @@
text\<open>Locale for the induction hypothesis\<close>
locale ex_reflection = reflection +
- fixes P --"the original formula"
- fixes Q --"the reflected formula"
- fixes Cl --"the class of reflecting ordinals"
+ fixes P \<comment>"the original formula"
+ fixes Q \<comment>"the reflected formula"
+ fixes Cl \<comment>"the class of reflecting ordinals"
assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)"
lemma (in ex_reflection) ClEx_downward:
@@ -159,7 +159,7 @@
intro: Limit_is_Ord Pair_in_Mset)
done
-text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close>
+text\<open>Class \<open>ClEx\<close> indeed consists of reflecting ordinals...\<close>
lemma (in ex_reflection) ZF_ClEx_iff:
"[| y\<in>Mset(a); Cl(a); ClEx(P,a) |]
==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
@@ -173,9 +173,9 @@
Closed_Unbounded_Limit Normal_normalize)
done
-text\<open>The same two theorems, exported to locale @{text reflection}.\<close>
+text\<open>The same two theorems, exported to locale \<open>reflection\<close>.\<close>
-text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close>
+text\<open>Class \<open>ClEx\<close> indeed consists of reflecting ordinals...\<close>
lemma (in reflection) ClEx_iff:
"[| y\<in>Mset(a); Cl(a); ClEx(P,a);
!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x) |]
@@ -266,7 +266,7 @@
subsection\<open>Simple Examples of Reflection\<close>
text\<open>Example 1: reflecting a simple formula. The reflecting class is first
-given as the variable @{text ?Cl} and later retrieved from the final
+given as the variable \<open>?Cl\<close> and later retrieved from the final
proof state.\<close>
schematic_goal (in reflection)
"Reflects(?Cl,
@@ -349,7 +349,7 @@
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
by fast
-text\<open>Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
+text\<open>Example 4: Axiom of Choice. Possibly wrong, since \<open>\<Pi>\<close> needs
to be relativized.\<close>
schematic_goal (in reflection)
"Reflects(?Cl,
--- a/src/ZF/Constructible/Relative.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Relative.thy Mon Dec 07 10:23:50 2015 +0100
@@ -123,7 +123,7 @@
definition
is_range :: "[i=>o,i,i] => o" where
- --\<open>the cleaner
+ \<comment>\<open>the cleaner
@{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
unfortunately needs an instance of separation in order to prove
@{term "M(converse(r))"}.\<close>
@@ -200,32 +200,32 @@
definition
ordinal :: "[i=>o,i] => o" where
- --\<open>an ordinal is a transitive set of transitive sets\<close>
+ \<comment>\<open>an ordinal is a transitive set of transitive sets\<close>
"ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))"
definition
limit_ordinal :: "[i=>o,i] => o" where
- --\<open>a limit ordinal is a non-empty, successor-closed ordinal\<close>
+ \<comment>\<open>a limit ordinal is a non-empty, successor-closed ordinal\<close>
"limit_ordinal(M,a) ==
ordinal(M,a) & ~ empty(M,a) &
(\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
definition
successor_ordinal :: "[i=>o,i] => o" where
- --\<open>a successor ordinal is any ordinal that is neither empty nor limit\<close>
+ \<comment>\<open>a successor ordinal is any ordinal that is neither empty nor limit\<close>
"successor_ordinal(M,a) ==
ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
definition
finite_ordinal :: "[i=>o,i] => o" where
- --\<open>an ordinal is finite if neither it nor any of its elements are limit\<close>
+ \<comment>\<open>an ordinal is finite if neither it nor any of its elements are limit\<close>
"finite_ordinal(M,a) ==
ordinal(M,a) & ~ limit_ordinal(M,a) &
(\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
definition
omega :: "[i=>o,i] => o" where
- --\<open>omega is a limit ordinal none of whose elements are limit\<close>
+ \<comment>\<open>omega is a limit ordinal none of whose elements are limit\<close>
"omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
definition
@@ -245,7 +245,7 @@
definition
Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
- --\<open>as above, but typed\<close>
+ \<comment>\<open>as above, but typed\<close>
"Relation1(M,A,is_f,f) ==
\<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)"
@@ -294,9 +294,9 @@
definition
separation :: "[i=>o, i=>o] => o" where
- --\<open>The formula @{text P} should only involve parameters
- belonging to @{text M} and all its quantifiers must be relativized
- to @{text M}. We do not have separation as a scheme; every instance
+ \<comment>\<open>The formula \<open>P\<close> should only involve parameters
+ belonging to \<open>M\<close> and all its quantifiers must be relativized
+ to \<open>M\<close>. We do not have separation as a scheme; every instance
that we need must be assumed (and later proved) separately.\<close>
"separation(M,P) ==
\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
@@ -339,7 +339,7 @@
subsection\<open>A trivial consistency proof for $V_\omega$\<close>
text\<open>We prove that $V_\omega$
- (or @{text univ} in Isabelle) satisfies some ZF axioms.
+ (or \<open>univ\<close> in Isabelle) satisfies some ZF axioms.
Kunen, Theorem IV 3.13, page 123.\<close>
lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
@@ -355,7 +355,7 @@
"A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
by (blast intro: univ0_downwards_mem)
-text\<open>Congruence rule for separation: can assume the variable is in @{text M}\<close>
+text\<open>Congruence rule for separation: can assume the variable is in \<open>M\<close>\<close>
lemma separation_cong [cong]:
"(!!x. M(x) ==> P(x) \<longleftrightarrow> P'(x))
==> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))"
@@ -468,8 +468,8 @@
apply (simp add: Pair_def, blast)
done
-text\<open>These two lemmas lets us prove @{text domain_closed} and
- @{text range_closed} without new instances of separation\<close>
+text\<open>These two lemmas lets us prove \<open>domain_closed\<close> and
+ \<open>range_closed\<close> without new instances of separation\<close>
lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
apply (rule equalityI, auto)
@@ -515,7 +515,7 @@
\<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
definition
- membership :: "[i=>o,i,i] => o" where --\<open>membership relation\<close>
+ membership :: "[i=>o,i,i] => o" where \<comment>\<open>membership relation\<close>
"membership(M,A,r) ==
\<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
@@ -534,8 +534,8 @@
and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*)
-text\<open>Automatically discovers the proof using @{text transM}, @{text nat_0I}
-and @{text M_nat}.\<close>
+text\<open>Automatically discovers the proof using \<open>transM\<close>, \<open>nat_0I\<close>
+and \<open>M_nat\<close>.\<close>
lemma (in M_trivial) nonempty [simp]: "M(0)"
by (blast intro: transM)
@@ -758,7 +758,7 @@
lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
by simp
-text\<open>Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
+text\<open>Better than \<open>RepFun_closed\<close> when having the formula @{term "x\<in>A"}
makes relativization easier.\<close>
lemma (in M_trivial) RepFun_closed2:
"[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
@@ -781,7 +781,7 @@
==> M(\<lambda>x\<in>A. b(x))"
by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
-text\<open>Better than @{text lam_closed}: has the formula @{term "x\<in>A"}\<close>
+text\<open>Better than \<open>lam_closed\<close>: has the formula @{term "x\<in>A"}\<close>
lemma (in M_trivial) lam_closed2:
"[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m))|] ==> M(Lambda(A,b))"
@@ -816,14 +816,14 @@
apply (blast intro!: equalityI dest: transM, blast)
done
-text\<open>What about @{text Pow_abs}? Powerset is NOT absolute!
+text\<open>What about \<open>Pow_abs\<close>? Powerset is NOT absolute!
This result is one direction of absoluteness.\<close>
lemma (in M_trivial) powerset_Pow:
"powerset(M, x, Pow(x))"
by (simp add: powerset_def)
-text\<open>But we can't prove that the powerset in @{text M} includes the
+text\<open>But we can't prove that the powerset in \<open>M\<close> includes the
real powerset.\<close>
lemma (in M_trivial) powerset_imp_subset_Pow:
"[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
@@ -992,7 +992,7 @@
pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
upair(M,cnbf,cnbf,z))"
and is_recfun_separation:
- --\<open>for well-founded recursion: used to prove @{text is_recfun_equal}\<close>
+ \<comment>\<open>for well-founded recursion: used to prove \<open>is_recfun_equal\<close>\<close>
"[| M(r); M(f); M(g); M(a); M(b) |]
==> separation(M,
\<lambda>x. \<exists>xa[M]. \<exists>xb[M].
@@ -1360,7 +1360,7 @@
text\<open>@{term M} contains all finite function spaces. Needed to prove the
absoluteness of transitive closure. See the definition of
-@{text rtrancl_alt} in in @{text WF_absolute.thy}.\<close>
+\<open>rtrancl_alt\<close> in in \<open>WF_absolute.thy\<close>.\<close>
lemma (in M_basic) finite_funspace_closed [intro,simp]:
"[|n\<in>nat; M(B)|] ==> M(n->B)"
apply (induct_tac n, simp)
@@ -1428,12 +1428,12 @@
definition
is_Nil :: "[i=>o, i] => o" where
- --\<open>because @{prop "[] \<equiv> Inl(0)"}\<close>
+ \<comment>\<open>because @{prop "[] \<equiv> Inl(0)"}\<close>
"is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
definition
is_Cons :: "[i=>o,i,i,i] => o" where
- --\<open>because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}\<close>
+ \<comment>\<open>because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}\<close>
"is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
@@ -1461,13 +1461,13 @@
definition
list_case' :: "[i, [i,i]=>i, i] => i" where
- --\<open>A version of @{term list_case} that's always defined.\<close>
+ \<comment>\<open>A version of @{term list_case} that's always defined.\<close>
"list_case'(a,b,xs) ==
if quasilist(xs) then list_case(a,b,xs) else 0"
definition
is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
- --\<open>Returns 0 for non-lists\<close>
+ \<comment>\<open>Returns 0 for non-lists\<close>
"is_list_case(M, a, is_b, xs, z) ==
(is_Nil(M,xs) \<longrightarrow> z=a) &
(\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) \<longrightarrow> is_b(x,l,z)) &
@@ -1475,17 +1475,17 @@
definition
hd' :: "i => i" where
- --\<open>A version of @{term hd} that's always defined.\<close>
+ \<comment>\<open>A version of @{term hd} that's always defined.\<close>
"hd'(xs) == if quasilist(xs) then hd(xs) else 0"
definition
tl' :: "i => i" where
- --\<open>A version of @{term tl} that's always defined.\<close>
+ \<comment>\<open>A version of @{term tl} that's always defined.\<close>
"tl'(xs) == if quasilist(xs) then tl(xs) else 0"
definition
is_hd :: "[i=>o,i,i] => o" where
- --\<open>@{term "hd([]) = 0"} no constraints if not a list.
+ \<comment>\<open>@{term "hd([]) = 0"} no constraints if not a list.
Avoiding implication prevents the simplifier's looping.\<close>
"is_hd(M,xs,H) ==
(is_Nil(M,xs) \<longrightarrow> empty(M,H)) &
@@ -1494,7 +1494,7 @@
definition
is_tl :: "[i=>o,i,i] => o" where
- --\<open>@{term "tl([]) = []"}; see comments about @{term is_hd}\<close>
+ \<comment>\<open>@{term "tl([]) = []"}; see comments about @{term is_hd}\<close>
"is_tl(M,xs,T) ==
(is_Nil(M,xs) \<longrightarrow> T=xs) &
(\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
--- a/src/ZF/Constructible/Satisfies_absolute.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Mon Dec 07 10:23:50 2015 +0100
@@ -147,7 +147,7 @@
text\<open>The second argument of @{term is_a} gives it direct access to @{term x},
which is essential for handling free variable references. Treatment is
- based on that of @{text is_nat_case_reflection}.\<close>
+ based on that of \<open>is_nat_case_reflection\<close>.\<close>
theorem is_formula_case_reflection:
assumes is_a_reflection:
"!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
@@ -176,7 +176,7 @@
definition
is_depth_apply :: "[i=>o,i,i,i] => o" where
- --\<open>Merely a useful abbreviation for the sequel.\<close>
+ \<comment>\<open>Merely a useful abbreviation for the sequel.\<close>
"is_depth_apply(M,h,p,z) ==
\<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M].
finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
@@ -190,10 +190,10 @@
text\<open>There is at present some redundancy between the relativizations in
- e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.\<close>
+ e.g. \<open>satisfies_is_a\<close> and those in e.g. \<open>Member_replacement\<close>.\<close>
text\<open>These constants let us instantiate the parameters @{term a}, @{term b},
- @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.\<close>
+ @{term c}, @{term d}, etc., of the locale \<open>Formula_Rec\<close>.\<close>
definition
satisfies_a :: "[i,i,i]=>i" where
"satisfies_a(A) ==
@@ -216,7 +216,7 @@
definition
satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where
- --\<open>We simplify the formula to have just @{term nx} rather than
+ \<comment>\<open>We simplify the formula to have just @{term nx} rather than
introducing @{term ny} with @{term "nx=ny"}\<close>
"satisfies_is_b(M,A) ==
\<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
@@ -259,7 +259,7 @@
definition
satisfies_MH :: "[i=>o,i,i,i,i]=>o" where
- --\<open>The variable @{term u} is unused, but gives @{term satisfies_MH}
+ \<comment>\<open>The variable @{term u} is unused, but gives @{term satisfies_MH}
the correct arity.\<close>
"satisfies_MH ==
\<lambda>M A u f z.
@@ -327,11 +327,11 @@
pair(M,env,bo,z))"
and
formula_rec_replacement:
- --\<open>For the @{term transrec}\<close>
+ \<comment>\<open>For the @{term transrec}\<close>
"[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
and
formula_rec_lambda_replacement:
- --\<open>For the @{text "\<lambda>-abstraction"} in the @{term transrec} body\<close>
+ \<comment>\<open>For the \<open>\<lambda>-abstraction\<close> in the @{term transrec} body\<close>
"[|M(g); M(A)|] ==>
strong_replacement (M,
\<lambda>x y. mem_formula(M,x) &
@@ -460,7 +460,7 @@
-text\<open>Instantiate locale @{text Formula_Rec} for the
+text\<open>Instantiate locale \<open>Formula_Rec\<close> for the
Function @{term satisfies}\<close>
lemma (in M_satisfies) Formula_Rec_axioms_M:
@@ -505,7 +505,7 @@
satisfies_eq is_satisfies_def satisfies_MH_def)
-subsection\<open>Internalizations Needed to Instantiate @{text "M_satisfies"}\<close>
+subsection\<open>Internalizations Needed to Instantiate \<open>M_satisfies\<close>\<close>
subsubsection\<open>The Operator @{term is_depth_apply}, Internalized\<close>
@@ -815,7 +815,7 @@
done
-subsection\<open>Lemmas for Instantiating the Locale @{text "M_satisfies"}\<close>
+subsection\<open>Lemmas for Instantiating the Locale \<open>M_satisfies\<close>\<close>
subsubsection\<open>The @{term "Member"} Case\<close>
@@ -959,7 +959,7 @@
is_wfrec_reflection)
lemma formula_rec_replacement:
- --\<open>For the @{term transrec}\<close>
+ \<comment>\<open>For the @{term transrec}\<close>
"[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
apply (rule transrec_replacementI, simp add: nat_into_M)
apply (rule strong_replacementI)
@@ -995,7 +995,7 @@
satisfies_is_d_reflection)
lemma formula_rec_lambda_replacement:
- --\<open>For the @{term transrec}\<close>
+ \<comment>\<open>For the @{term transrec}\<close>
"[|L(g); L(A)|] ==>
strong_replacement (L,
\<lambda>x y. mem_formula(L,x) &
@@ -1016,7 +1016,7 @@
done
-subsection\<open>Instantiating @{text M_satisfies}\<close>
+subsection\<open>Instantiating \<open>M_satisfies\<close>\<close>
lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
apply (rule M_satisfies_axioms.intro)
--- a/src/ZF/Constructible/Separation.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Separation.thy Mon Dec 07 10:23:50 2015 +0100
@@ -6,7 +6,7 @@
theory Separation imports L_axioms WF_absolute begin
-text\<open>This theory proves all instances needed for locale @{text "M_basic"}\<close>
+text\<open>This theory proves all instances needed for locale \<open>M_basic\<close>\<close>
text\<open>Helps us solve for de Bruijn indices!\<close>
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
@@ -274,7 +274,7 @@
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma is_recfun_separation:
- --\<open>for well-founded recursion\<close>
+ \<comment>\<open>for well-founded recursion\<close>
"[| L(r); L(f); L(g); L(a); L(b) |]
==> separation(L,
\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
@@ -288,7 +288,7 @@
done
-subsection\<open>Instantiating the locale @{text M_basic}\<close>
+subsection\<open>Instantiating the locale \<open>M_basic\<close>\<close>
text\<open>Separation (and Strong Replacement) for basic set-theoretic constructions
such as intersection, Cartesian Product and image.\<close>
--- a/src/ZF/Constructible/WF_absolute.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy Mon Dec 07 10:23:50 2015 +0100
@@ -60,7 +60,7 @@
definition
rtran_closure_mem :: "[i=>o,i,i,i] => o" where
- --\<open>The property of belonging to @{text "rtran_closure(r)"}\<close>
+ \<comment>\<open>The property of belonging to \<open>rtran_closure(r)\<close>\<close>
"rtran_closure_mem(M,A,r,p) ==
\<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
@@ -140,7 +140,7 @@
"[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)"
by (insert wellfounded_trancl_separation [of r Z], simp)
-text\<open>Alternative proof of @{text wf_on_trancl}; inspiration for the
+text\<open>Alternative proof of \<open>wf_on_trancl\<close>; inspiration for the
relativized version. Original version is on theory WF.\<close>
lemma "[| wf[A](r); r-``A \<subseteq> A |] ==> wf[A](r^+)"
apply (simp add: wf_on_def wf_def)
@@ -200,7 +200,7 @@
done
-text\<open>Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
+text\<open>Assuming @{term r} is transitive simplifies the occurrences of \<open>H\<close>.
The premise @{term "relation(r)"} is necessary
before we can replace @{term "r^+"} by @{term r}.\<close>
theorem (in M_trancl) trans_wfrec_relativize:
@@ -238,7 +238,7 @@
subsection\<open>M is closed under well-founded recursion\<close>
-text\<open>Lemma with the awkward premise mentioning @{text wfrec}.\<close>
+text\<open>Lemma with the awkward premise mentioning \<open>wfrec\<close>.\<close>
lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
"[|wf(r); M(r);
strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
--- a/src/ZF/Constructible/WFrec.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/WFrec.thy Mon Dec 07 10:23:50 2015 +0100
@@ -18,7 +18,7 @@
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
done
-text\<open>Expresses @{text is_recfun} as a recursion equation\<close>
+text\<open>Expresses \<open>is_recfun\<close> as a recursion equation\<close>
lemma is_recfun_iff_equation:
"is_recfun(r,a,H,f) \<longleftrightarrow>
f \<in> r -`` {a} \<rightarrow> range(f) &
@@ -56,7 +56,7 @@
apply (simp_all add: vimage_singleton_iff Int_lower2)
done
-text\<open>For @{text is_recfun} we need only pay attention to functions
+text\<open>For \<open>is_recfun\<close> we need only pay attention to functions
whose domains are initial segments of @{term r}.\<close>
lemma is_recfun_cong:
"[| r = r'; a = a'; f = f';
@@ -82,7 +82,7 @@
text\<open>Stated using @{term "trans(r)"} rather than
@{term "transitive_rel(M,A,r)"} because the latter rewrites to
- the former anyway, by @{text transitive_rel_abs}.
+ the former anyway, by \<open>transitive_rel_abs\<close>.
As always, theorems should be expressed in simplified form.
The last three M-premises are redundant because of @{term "M(r)"},
but without them we'd have to undertake
@@ -130,7 +130,7 @@
apply (blast intro!: is_recfun_equal dest: transM)
done
-text\<open>Tells us that @{text is_recfun} can (in principle) be relativized.\<close>
+text\<open>Tells us that \<open>is_recfun\<close> can (in principle) be relativized.\<close>
lemma (in M_basic) is_recfun_relativize:
"[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |]
==> is_recfun(r,a,H,f) \<longleftrightarrow>
@@ -180,7 +180,7 @@
==> restrict(Y, r -`` {x}) = f"
apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f")
apply (simp (no_asm_simp) add: restrict_def)
- apply (thin_tac "rall(M,P)" for P)+ --\<open>essential for efficiency\<close>
+ apply (thin_tac "rall(M,P)" for P)+ \<comment>\<open>essential for efficiency\<close>
apply (frule is_recfun_type [THEN fun_is_rel], blast)
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
@@ -207,7 +207,7 @@
done
-text\<open>Proof of the inductive step for @{text exists_is_recfun}, since
+text\<open>Proof of the inductive step for \<open>exists_is_recfun\<close>, since
we must prove two versions.\<close>
lemma (in M_basic) exists_is_recfun_indstep:
"[|\<forall>y. \<langle>y, a1\<rangle> \<in> r \<longrightarrow> (\<exists>f[M]. is_recfun(r, y, H, f));
@@ -220,7 +220,7 @@
apply blast
txt\<open>Discharge the "univalent" obligation of Replacement\<close>
apply (simp add: univalent_is_recfun)
-txt\<open>Show that the constructed object satisfies @{text is_recfun}\<close>
+txt\<open>Show that the constructed object satisfies \<open>is_recfun\<close>\<close>
apply clarify
apply (rule_tac x=Y in rexI)
txt\<open>Unfold only the top-level occurrence of @{term is_recfun}\<close>
--- a/src/ZF/Constructible/Wellorderings.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Mon Dec 07 10:23:50 2015 +0100
@@ -9,7 +9,7 @@
text\<open>We define functions analogous to @{term ordermap} @{term ordertype}
but without using recursion. Instead, there is a direct appeal
to Replacement. This will be the basis for a version relativized
- to some class @{text M}. The main result is Theorem I 7.6 in Kunen,
+ to some class \<open>M\<close>. The main result is Theorem I 7.6 in Kunen,
page 17.\<close>
@@ -32,18 +32,18 @@
definition
wellfounded :: "[i=>o,i]=>o" where
- --\<open>EVERY non-empty set has an @{text r}-minimal element\<close>
+ \<comment>\<open>EVERY non-empty set has an \<open>r\<close>-minimal element\<close>
"wellfounded(M,r) ==
\<forall>x[M]. x\<noteq>0 \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
definition
wellfounded_on :: "[i=>o,i,i]=>o" where
- --\<open>every non-empty SUBSET OF @{text A} has an @{text r}-minimal element\<close>
+ \<comment>\<open>every non-empty SUBSET OF \<open>A\<close> has an \<open>r\<close>-minimal element\<close>
"wellfounded_on(M,A,r) ==
\<forall>x[M]. x\<noteq>0 \<longrightarrow> x\<subseteq>A \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
definition
wellordered :: "[i=>o,i,i]=>o" where
- --\<open>linear and wellfounded on @{text A}\<close>
+ \<comment>\<open>linear and wellfounded on \<open>A\<close>\<close>
"wellordered(M,A,r) ==
transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
--- a/src/ZF/EquivClass.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/EquivClass.thy Mon Dec 07 10:23:50 2015 +0100
@@ -27,7 +27,7 @@
abbreviation
RESPECTS2 ::"[i=>i=>i, i] => o" (infixr "respects2 " 80) where
"f respects2 r == congruent2(r,r,f)"
- --\<open>Abbreviation for the common case where the relations are identical\<close>
+ \<comment>\<open>Abbreviation for the common case where the relations are identical\<close>
subsection\<open>Suppes, Theorem 70:
--- a/src/ZF/IMP/Equiv.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/IMP/Equiv.thy Mon Dec 07 10:23:50 2015 +0100
@@ -38,14 +38,14 @@
lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
apply (erule evalc.induct)
apply (simp_all (no_asm_simp))
- txt \<open>@{text assign}\<close>
+ txt \<open>\<open>assign\<close>\<close>
apply (simp add: update_type)
- txt \<open>@{text comp}\<close>
+ txt \<open>\<open>comp\<close>\<close>
apply fast
- txt \<open>@{text while}\<close>
+ txt \<open>\<open>while\<close>\<close>
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
apply (simp add: Gamma_def)
- txt \<open>recursive case of @{text while}\<close>
+ txt \<open>recursive case of \<open>while\<close>\<close>
apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
apply (auto simp add: Gamma_def)
done
@@ -56,19 +56,19 @@
lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
apply (erule com.induct)
- txt \<open>@{text skip}\<close>
+ txt \<open>\<open>skip\<close>\<close>
apply force
- txt \<open>@{text assign}\<close>
+ txt \<open>\<open>assign\<close>\<close>
apply force
- txt \<open>@{text comp}\<close>
+ txt \<open>\<open>comp\<close>\<close>
apply force
- txt \<open>@{text while}\<close>
+ txt \<open>\<open>while\<close>\<close>
apply safe
apply simp_all
apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
apply (unfold Gamma_def)
apply force
- txt \<open>@{text "if"}\<close>
+ txt \<open>\<open>if\<close>\<close>
apply auto
done
--- a/src/ZF/Induct/Acc.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Acc.thy Mon Dec 07 10:23:50 2015 +0100
@@ -8,7 +8,7 @@
theory Acc imports Main begin
text \<open>
- Inductive definition of @{text "acc(r)"}; see @{cite "paulin-tlca"}.
+ Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
\<close>
consts
@@ -22,7 +22,7 @@
text \<open>
The introduction rule must require @{prop "a \<in> field(r)"},
- otherwise @{text "acc(r)"} would be a proper class!
+ otherwise \<open>acc(r)\<close> would be a proper class!
\medskip
The intended introduction rule:
--- a/src/ZF/Induct/Binary_Trees.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy Mon Dec 07 10:23:50 2015 +0100
@@ -21,11 +21,11 @@
by (induct arbitrary: x r set: bt) auto
lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
- -- "Proving a freeness theorem."
+ \<comment> "Proving a freeness theorem."
by (fast elim!: bt.free_elims)
inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
- -- "An elimination rule, for type-checking."
+ \<comment> "An elimination rule, for type-checking."
text \<open>
\medskip Lemmas to justify using @{term bt} in other recursive type
@@ -58,7 +58,7 @@
!!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==>
h(x, y, z, r, s) \<in> C(Br(x, y, z))
|] ==> bt_rec(c, h, t) \<in> C(t)"
- -- \<open>Type checking for recursor -- example only; not really needed.\<close>
+ \<comment> \<open>Type checking for recursor -- example only; not really needed.\<close>
apply (induct_tac t)
apply simp_all
done
--- a/src/ZF/Induct/Brouwer.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Brouwer.thy Mon Dec 07 10:23:50 2015 +0100
@@ -28,7 +28,7 @@
"!!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b))"
"!!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
shows "P(b)"
- -- \<open>A nicer induction rule than the standard one.\<close>
+ \<comment> \<open>A nicer induction rule than the standard one.\<close>
using b
apply induct
apply (rule cases(1))
@@ -45,7 +45,7 @@
Well :: "[i, i => i] => i"
datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
- -- \<open>The union with @{text nat} ensures that the cardinal is infinite.\<close>
+ \<comment> \<open>The union with \<open>nat\<close> ensures that the cardinal is infinite.\<close>
"Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
monos Pi_mono
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
@@ -59,7 +59,7 @@
assumes w: "w \<in> Well(A, B)"
and step: "!!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
shows "P(w)"
- -- \<open>A nicer induction rule than the standard one.\<close>
+ \<comment> \<open>A nicer induction rule than the standard one.\<close>
using w
apply induct
apply (assumption | rule step)+
@@ -68,8 +68,8 @@
done
lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
- -- \<open>In fact it's isomorphic to @{text nat}, but we need a recursion operator\<close>
- -- \<open>for @{text Well} to prove this.\<close>
+ \<comment> \<open>In fact it's isomorphic to \<open>nat\<close>, but we need a recursion operator\<close>
+ \<comment> \<open>for \<open>Well\<close> to prove this.\<close>
apply (rule Well_unfold [THEN trans])
apply (simp add: Sigma_bool succ_def)
done
--- a/src/ZF/Induct/Comb.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Comb.thy Mon Dec 07 10:23:50 2015 +0100
@@ -15,7 +15,7 @@
subsection \<open>Definitions\<close>
-text \<open>Datatype definition of combinators @{text S} and @{text K}.\<close>
+text \<open>Datatype definition of combinators \<open>S\<close> and \<open>K\<close>.\<close>
consts comb :: i
datatype comb =
@@ -24,8 +24,8 @@
| app ("p \<in> comb", "q \<in> comb") (infixl "\<bullet>" 90)
text \<open>
- Inductive definition of contractions, @{text "-1->"} and
- (multi-step) reductions, @{text "-\<longrightarrow>"}.
+ Inductive definition of contractions, \<open>-1->\<close> and
+ (multi-step) reductions, \<open>-\<longrightarrow>\<close>.
\<close>
consts
@@ -49,8 +49,8 @@
type_intros comb.intros
text \<open>
- Inductive definition of parallel contractions, @{text "=1=>"} and
- (multi-step) parallel reductions, @{text "===>"}.
+ Inductive definition of parallel contractions, \<open>=1=>\<close> and
+ (multi-step) parallel reductions, \<open>===>\<close>.
\<close>
consts
@@ -115,8 +115,8 @@
subsection \<open>Results about Contraction\<close>
text \<open>
- For type checking: replaces @{term "a -1-> b"} by @{text "a, b \<in>
- comb"}.
+ For type checking: replaces @{term "a -1-> b"} by \<open>a, b \<in>
+ comb\<close>.
\<close>
lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
@@ -141,7 +141,7 @@
contract.Ap2 [THEN rtrancl_into_rtrancl2]
lemma "p \<in> comb ==> I\<bullet>p -\<longrightarrow> p"
- -- \<open>Example only: not used\<close>
+ \<comment> \<open>Example only: not used\<close>
by (unfold I_def) (blast intro: reduction_rls)
lemma comb_I: "I \<in> comb"
@@ -181,7 +181,7 @@
contract_combD2 reduction_rls)
done
-text \<open>Counterexample to the diamond property for @{text "-1->"}.\<close>
+text \<open>Counterexample to the diamond property for \<open>-1->\<close>.\<close>
lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
by (blast intro: comb_I)
@@ -201,8 +201,8 @@
subsection \<open>Results about Parallel Contraction\<close>
-text \<open>For type checking: replaces @{text "a =1=> b"} by @{text "a, b
- \<in> comb"}\<close>
+text \<open>For type checking: replaces \<open>a =1=> b\<close> by \<open>a, b
+ \<in> comb\<close>\<close>
lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
@@ -234,7 +234,7 @@
by auto
lemma diamond_parcontract: "diamond(parcontract)"
- -- \<open>Church-Rosser property for parallel contraction\<close>
+ \<comment> \<open>Church-Rosser property for parallel contraction\<close>
apply (unfold diamond_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule parcontract.induct)
--- a/src/ZF/Induct/Datatypes.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Datatypes.thy Mon Dec 07 10:23:50 2015 +0100
@@ -10,8 +10,7 @@
subsection \<open>A type with four constructors\<close>
text \<open>
- It has four contructors, of arities 0--3, and two parameters @{text
- A} and @{text B}.
+ It has four contructors, of arities 0--3, and two parameters \<open>A\<close> and \<open>B\<close>.
\<close>
consts
--- a/src/ZF/Induct/ListN.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/ListN.thy Mon Dec 07 10:23:50 2015 +0100
@@ -8,7 +8,7 @@
theory ListN imports Main begin
text \<open>
- Inductive definition of lists of @{text n} elements; see
+ Inductive definition of lists of \<open>n\<close> elements; see
@{cite "paulin-tlca"}.
\<close>
--- a/src/ZF/Induct/Multiset.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Multiset.thy Mon Dec 07 10:23:50 2015 +0100
@@ -12,7 +12,7 @@
begin
abbreviation (input)
- -- \<open>Short cut for multiset space\<close>
+ \<comment> \<open>Short cut for multiset space\<close>
Mult :: "i=>i" where
"Mult(A) == A -||> nat-{0}"
--- a/src/ZF/Induct/Ntree.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Ntree.thy Mon Dec 07 10:23:50 2015 +0100
@@ -9,7 +9,7 @@
text \<open>
Demonstrates a simple use of function space in a datatype
- definition. Based upon theory @{text Term}.
+ definition. Based upon theory \<open>Term\<close>.
\<close>
consts
@@ -18,12 +18,12 @@
maptree2 :: "[i, i] => i"
datatype "ntree(A)" = Branch ("a \<in> A", "h \<in> (\<Union>n \<in> nat. n -> ntree(A))")
- monos UN_mono [OF subset_refl Pi_mono] -- \<open>MUST have this form\<close>
+ monos UN_mono [OF subset_refl Pi_mono] \<comment> \<open>MUST have this form\<close>
type_intros nat_fun_univ [THEN subsetD]
type_elims UN_E
datatype "maptree(A)" = Sons ("a \<in> A", "h \<in> maptree(A) -||> maptree(A)")
- monos FiniteFun_mono1 -- \<open>Use monotonicity in BOTH args\<close>
+ monos FiniteFun_mono1 \<comment> \<open>Use monotonicity in BOTH args\<close>
type_intros FiniteFun_univ1 [THEN subsetD]
datatype "maptree2(A, B)" = Sons2 ("a \<in> A", "h \<in> B -||> maptree2(A, B)")
@@ -41,7 +41,7 @@
text \<open>
- \medskip @{text ntree}
+ \medskip \<open>ntree\<close>
\<close>
lemma ntree_unfold: "ntree(A) = A \<times> (\<Union>n \<in> nat. n -> ntree(A))"
@@ -53,7 +53,7 @@
and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i)
|] ==> P(Branch(x,h))"
shows "P(t)"
- -- \<open>A nicer induction rule than the standard one.\<close>
+ \<comment> \<open>A nicer induction rule than the standard one.\<close>
using t
apply induct
apply (erule UN_E)
@@ -69,7 +69,7 @@
and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); f O h = g O h |] ==>
f ` Branch(x,h) = g ` Branch(x,h)"
shows "f`t=g`t"
- -- \<open>Induction on @{term "ntree(A)"} to prove an equation\<close>
+ \<comment> \<open>Induction on @{term "ntree(A)"} to prove an equation\<close>
using t
apply induct
apply (assumption | rule step)+
@@ -80,7 +80,7 @@
done
text \<open>
- \medskip Lemmas to justify using @{text Ntree} in other recursive
+ \medskip Lemmas to justify using \<open>Ntree\<close> in other recursive
type definitions.
\<close>
@@ -92,7 +92,7 @@
done
lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)"
- -- \<open>Easily provable by induction also\<close>
+ \<comment> \<open>Easily provable by induction also\<close>
apply (unfold ntree.defs ntree.con_defs)
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
@@ -104,7 +104,7 @@
text \<open>
- \medskip @{text ntree} recursion.
+ \medskip \<open>ntree\<close> recursion.
\<close>
lemma ntree_rec_Branch:
@@ -125,7 +125,7 @@
text \<open>
- \medskip @{text maptree}
+ \medskip \<open>maptree\<close>
\<close>
lemma maptree_unfold: "maptree(A) = A \<times> (maptree(A) -||> maptree(A))"
@@ -138,7 +138,7 @@
\<forall>y \<in> field(h). P(y)
|] ==> P(Sons(x,h))"
shows "P(t)"
- -- \<open>A nicer induction rule than the standard one.\<close>
+ \<comment> \<open>A nicer induction rule than the standard one.\<close>
using t
apply induct
apply (assumption | rule step)+
@@ -150,7 +150,7 @@
text \<open>
- \medskip @{text maptree2}
+ \medskip \<open>maptree2\<close>
\<close>
lemma maptree2_unfold: "maptree2(A, B) = A \<times> (B -||> maptree2(A, B))"
--- a/src/ZF/Induct/Primrec.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Primrec.thy Mon Dec 07 10:23:50 2015 +0100
@@ -37,7 +37,7 @@
"PREC(f,g) ==
\<lambda>l \<in> list(nat). list_case(0,
\<lambda>x xs. rec(x, f`xs, \<lambda>y r. g ` Cons(r, Cons(y, xs))), l)"
- -- \<open>Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}!\<close>
+ \<comment> \<open>Note that \<open>g\<close> is applied first to @{term "PREC(f,g)`y"} and then to \<open>y\<close>!\<close>
consts
ACK :: "i=>i"
@@ -115,16 +115,16 @@
subsection \<open>Ackermann's function cases\<close>
lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
- -- \<open>PROPERTY A 1\<close>
+ \<comment> \<open>PROPERTY A 1\<close>
by (simp add: SC)
lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
- -- \<open>PROPERTY A 2\<close>
+ \<comment> \<open>PROPERTY A 2\<close>
by (simp add: CONSTANT PREC_0)
lemma ack_succ_succ:
"[| i\<in>nat; j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
- -- \<open>PROPERTY A 3\<close>
+ \<comment> \<open>PROPERTY A 3\<close>
by (simp add: CONSTANT PREC_succ COMP_1 PROJ_0)
lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
@@ -132,7 +132,7 @@
lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)"
- -- \<open>PROPERTY A 4\<close>
+ \<comment> \<open>PROPERTY A 4\<close>
apply (induct i arbitrary: j set: nat)
apply simp
apply (induct_tac j)
@@ -142,11 +142,11 @@
done
lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
- -- \<open>PROPERTY A 5-, the single-step lemma\<close>
+ \<comment> \<open>PROPERTY A 5-, the single-step lemma\<close>
by (induct set: nat) (simp_all add: lt_ack2)
lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
- -- \<open>PROPERTY A 5, monotonicity for @{text "<"}\<close>
+ \<comment> \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close>
apply (frule lt_nat_in_nat, assumption)
apply (erule succ_lt_induct)
apply assumption
@@ -155,14 +155,14 @@
done
lemma ack_le_mono2: "[|j\<le>k; i\<in>nat; k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"
- -- \<open>PROPERTY A 5', monotonicity for @{text \<le>}\<close>
+ \<comment> \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close>
apply (rule_tac f = "\<lambda>j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+
done
lemma ack2_le_ack1:
"[| i\<in>nat; j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
- -- \<open>PROPERTY A 6\<close>
+ \<comment> \<open>PROPERTY A 6\<close>
apply (induct_tac j)
apply simp_all
apply (rule ack_le_mono2)
@@ -171,14 +171,14 @@
done
lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"
- -- \<open>PROPERTY A 7-, the single-step lemma\<close>
+ \<comment> \<open>PROPERTY A 7-, the single-step lemma\<close>
apply (rule ack_lt_mono2 [THEN lt_trans2])
apply (rule_tac [4] ack2_le_ack1)
apply auto
done
lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"
- -- \<open>PROPERTY A 7, monotonicity for @{text "<"}\<close>
+ \<comment> \<open>PROPERTY A 7, monotonicity for \<open><\<close>\<close>
apply (frule lt_nat_in_nat, assumption)
apply (erule succ_lt_induct)
apply assumption
@@ -187,23 +187,23 @@
done
lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"
- -- \<open>PROPERTY A 7', monotonicity for @{text \<le>}\<close>
+ \<comment> \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close>
apply (rule_tac f = "\<lambda>j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+
done
lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
- -- \<open>PROPERTY A 8\<close>
+ \<comment> \<open>PROPERTY A 8\<close>
by (induct set: nat) simp_all
lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
- -- \<open>PROPERTY A 9\<close>
+ \<comment> \<open>PROPERTY A 9\<close>
by (induct set: nat) (simp_all add: ack_1)
lemma ack_nest_bound:
"[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
- -- \<open>PROPERTY A 10\<close>
+ \<comment> \<open>PROPERTY A 10\<close>
apply (rule lt_trans2 [OF _ ack2_le_ack1])
apply simp
apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
@@ -214,7 +214,7 @@
lemma ack_add_bound:
"[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
- -- \<open>PROPERTY A 11\<close>
+ \<comment> \<open>PROPERTY A 11\<close>
apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans)
apply (simp add: ack_2)
apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
@@ -225,9 +225,9 @@
lemma ack_add_bound2:
"[| i < ack(k,j); j \<in> nat; k \<in> nat |]
==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
- -- \<open>PROPERTY A 12.\<close>
- -- \<open>Article uses existential quantifier but the ALF proof used @{term "k#+#4"}.\<close>
- -- \<open>Quantified version must be nested @{text "\<exists>k'. \<forall>i,j \<dots>"}.\<close>
+ \<comment> \<open>PROPERTY A 12.\<close>
+ \<comment> \<open>Article uses existential quantifier but the ALF proof used @{term "k#+#4"}.\<close>
+ \<comment> \<open>Quantified version must be nested \<open>\<exists>k'. \<forall>i,j \<dots>\<close>.\<close>
apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
apply (rule add_lt_mono)
@@ -247,7 +247,7 @@
done
lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
- -- \<open>PROPERTY A 4'? Extra lemma needed for @{text CONSTANT} case, constant functions.\<close>
+ \<comment> \<open>PROPERTY A 4'? Extra lemma needed for \<open>CONSTANT\<close> case, constant functions.\<close>
apply (induct_tac i)
apply (simp add: nat_0_le)
apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
@@ -275,7 +275,7 @@
done
text \<open>
- \medskip @{text COMP} case.
+ \medskip \<open>COMP\<close> case.
\<close>
lemma COMP_map_lemma:
@@ -312,7 +312,7 @@
done
text \<open>
- \medskip @{text PREC} case.
+ \medskip \<open>PREC\<close> case.
\<close>
lemma PREC_case_lemma:
@@ -326,7 +326,7 @@
apply (erule list.cases)
apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
apply simp
- apply (erule ssubst) -- \<open>get rid of the needless assumption\<close>
+ apply (erule ssubst) \<comment> \<open>get rid of the needless assumption\<close>
apply (induct_tac a)
apply simp_all
txt \<open>base case\<close>
--- a/src/ZF/Induct/PropLog.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/PropLog.thy Mon Dec 07 10:23:50 2015 +0100
@@ -14,8 +14,8 @@
Inductive definition of propositional logic. Soundness and
completeness w.r.t.\ truth-tables.
- Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
- Fin(H)"}
+ Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
+ Fin(H)\<close>
\<close>
@@ -66,7 +66,7 @@
definition
is_true :: "[i,i] => o" where
"is_true(p,t) == is_true_fun(p,t) = 1"
- -- \<open>this definition is required since predicates can't be recursive\<close>
+ \<comment> \<open>this definition is required since predicates can't be recursive\<close>
lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
by (simp add: is_true_def)
@@ -81,8 +81,8 @@
subsubsection \<open>Logical consequence\<close>
text \<open>
- For every valuation, if all elements of @{text H} are true then so
- is @{text p}.
+ For every valuation, if all elements of \<open>H\<close> are true then so
+ is \<open>p\<close>.
\<close>
definition
@@ -91,8 +91,8 @@
text \<open>
- A finite set of hypotheses from @{text t} and the @{text Var}s in
- @{text p}.
+ A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
+ \<open>p\<close>.
\<close>
consts
@@ -118,13 +118,13 @@
inductive_cases ImpE: "p=>q \<in> propn"
lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q"
- -- \<open>Stronger Modus Ponens rule: no typechecking!\<close>
+ \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
apply (rule thms.MP)
apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
done
lemma thms_I: "p \<in> propn ==> H |- p=>p"
- -- \<open>Rule is called @{text I} for Identity Combinator, not for Introduction.\<close>
+ \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
apply (rule thms.S [THEN thms_MP, THEN thms_MP])
apply (rule_tac [5] thms.K)
apply (rule_tac [4] thms.K)
@@ -135,7 +135,7 @@
subsubsection \<open>Weakening, left and right\<close>
lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p"
- -- \<open>Order of premises is convenient with @{text THEN}\<close>
+ \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
by (erule thms_mono [THEN subsetD])
lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
@@ -208,7 +208,7 @@
lemma hyps_thms_if:
"p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
- -- \<open>Typical example of strengthening the induction statement.\<close>
+ \<comment> \<open>Typical example of strengthening the induction statement.\<close>
apply simp
apply (induct_tac p)
apply (simp_all add: thms_I thms.H)
@@ -217,7 +217,7 @@
done
lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p"
- -- \<open>Key lemma for completeness; yields a set of assumptions satisfying @{text p}\<close>
+ \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
apply (drule hyps_thms_if)
apply (simp add: logcon_def)
done
@@ -242,7 +242,7 @@
lemma thms_excluded_middle_rule:
"[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q"
- -- \<open>Hard to prove directly because it requires cuts\<close>
+ \<comment> \<open>Hard to prove directly because it requires cuts\<close>
apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
apply (blast intro!: propn_SIs intro: propn_Is)+
done
@@ -268,7 +268,7 @@
"p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
by (induct set: propn) auto
-text \<open>Two lemmas for use with @{text weaken_left}\<close>
+text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>
lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
by blast
@@ -317,13 +317,13 @@
subsubsection \<open>Completeness theorem\<close>
lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p"
- -- \<open>The base case for completeness\<close>
+ \<comment> \<open>The base case for completeness\<close>
apply (rule Diff_cancel [THEN subst])
apply (blast intro: completeness_0_lemma)
done
lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
- -- \<open>A semantic analogue of the Deduction Theorem\<close>
+ \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
by (simp add: logcon_def)
lemma completeness:
--- a/src/ZF/Induct/Rmap.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Rmap.thy Mon Dec 07 10:23:50 2015 +0100
@@ -53,7 +53,7 @@
done
text \<open>
- \medskip If @{text f} is a function then @{text "rmap(f)"} behaves
+ \medskip If \<open>f\<close> is a function then \<open>rmap(f)\<close> behaves
as expected.
\<close>
--- a/src/ZF/Induct/Term.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Term.thy Mon Dec 07 10:23:50 2015 +0100
@@ -8,8 +8,7 @@
theory Term imports Main begin
text \<open>
- Illustrates the list functor (essentially the same type as in @{text
- Trees_Forest}).
+ Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>).
\<close>
consts
@@ -56,7 +55,7 @@
!!x z zs. [| x \<in> A; z \<in> term(A); zs: list(term(A)); P(Apply(x,zs))
|] ==> P(Apply(x, Cons(z,zs)))
|] ==> P(t)"
- -- \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
+ \<comment> \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
apply (induct_tac t)
apply (erule list.induct)
apply (auto dest: list_CollectD)
@@ -67,7 +66,7 @@
!!x zs. [| x \<in> A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==>
f(Apply(x,zs)) = g(Apply(x,zs))
|] ==> f(t) = g(t)"
- -- \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
+ \<comment> \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
apply (induct_tac t)
apply (auto dest: map_list_Collect list_CollectD)
done
@@ -85,7 +84,7 @@
done
lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
- -- \<open>Easily provable by induction also\<close>
+ \<comment> \<open>Easily provable by induction also\<close>
apply (unfold term.defs term.con_defs)
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
@@ -103,12 +102,12 @@
by (rule term_subset_univ [THEN subsetD])
text \<open>
- \medskip @{text term_rec} -- by @{text Vset} recursion.
+ \medskip \<open>term_rec\<close> -- by \<open>Vset\<close> recursion.
\<close>
lemma map_lemma: "[| l \<in> list(A); Ord(i); rank(l)<i |]
==> map(\<lambda>z. (\<lambda>x \<in> Vset(i).h(x)) ` z, l) = map(h,l)"
- -- \<open>@{term map} works correctly on the underlying list of terms.\<close>
+ \<comment> \<open>@{term map} works correctly on the underlying list of terms.\<close>
apply (induct set: list)
apply simp
apply (subgoal_tac "rank (a) <i & rank (l) < i")
@@ -119,7 +118,7 @@
lemma term_rec [simp]: "ts \<in> list(A) ==>
term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
- -- \<open>Typing premise is necessary to invoke @{text map_lemma}.\<close>
+ \<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close>
apply (rule term_rec_def [THEN def_Vrec, THEN trans])
apply (unfold term.con_defs)
apply (simp add: rank_pair2 map_lemma)
@@ -131,7 +130,7 @@
r \<in> list(\<Union>t \<in> term(A). C(t)) |]
==> d(x, zs, r): C(Apply(x,zs))"
shows "term_rec(t,d) \<in> C(t)"
- -- \<open>Slightly odd typing condition on @{text r} in the second premise!\<close>
+ \<comment> \<open>Slightly odd typing condition on \<open>r\<close> in the second premise!\<close>
using t
apply induct
apply (frule list_CollectD)
@@ -194,7 +193,7 @@
text \<open>
- \medskip @{text reflect}.
+ \medskip \<open>reflect\<close>.
\<close>
lemma reflect [simp]:
@@ -206,7 +205,7 @@
text \<open>
- \medskip @{text preorder}.
+ \medskip \<open>preorder\<close>.
\<close>
lemma preorder [simp]:
@@ -218,7 +217,7 @@
text \<open>
- \medskip @{text postorder}.
+ \medskip \<open>postorder\<close>.
\<close>
lemma postorder [simp]:
@@ -230,7 +229,7 @@
text \<open>
- \medskip Theorems about @{text term_map}.
+ \medskip Theorems about \<open>term_map\<close>.
\<close>
declare map_compose [simp]
@@ -248,7 +247,7 @@
text \<open>
- \medskip Theorems about @{text term_size}.
+ \medskip Theorems about \<open>term_size\<close>.
\<close>
lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
@@ -262,7 +261,7 @@
text \<open>
- \medskip Theorems about @{text reflect}.
+ \medskip Theorems about \<open>reflect\<close>.
\<close>
lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
--- a/src/ZF/Induct/Tree_Forest.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Mon Dec 07 10:23:50 2015 +0100
@@ -61,7 +61,7 @@
lemma tree_forest_unfold:
"tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
- -- \<open>NOT useful, but interesting \dots\<close>
+ \<comment> \<open>NOT useful, but interesting \dots\<close>
supply rews = tree_forest.con_defs tree_def forest_def
apply (unfold tree_def forest_def)
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
@@ -108,7 +108,7 @@
|] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f))
|] ==> (\<forall>t \<in> tree(A). tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
(\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
- -- \<open>Mutually recursive version.\<close>
+ \<comment> \<open>Mutually recursive version.\<close>
apply (unfold Ball_def)
apply (rule tree_forest.mutual_induct)
apply simp_all
@@ -157,7 +157,7 @@
text \<open>
- \medskip @{text list_of_TF} and @{text of_list}.
+ \medskip \<open>list_of_TF\<close> and \<open>of_list\<close>.
\<close>
lemma list_of_TF_type [TC]:
@@ -168,7 +168,7 @@
by (induct set: list) simp_all
text \<open>
- \medskip @{text map}.
+ \medskip \<open>map\<close>.
\<close>
lemma
@@ -179,7 +179,7 @@
by (induct rule: tree'induct forest'induct) simp_all
text \<open>
- \medskip @{text size}.
+ \medskip \<open>size\<close>.
\<close>
lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
@@ -187,7 +187,7 @@
text \<open>
- \medskip @{text preorder}.
+ \medskip \<open>preorder\<close>.
\<close>
lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
@@ -195,7 +195,7 @@
text \<open>
- \medskip Theorems about @{text list_of_TF} and @{text of_list}.
+ \medskip Theorems about \<open>list_of_TF\<close> and \<open>of_list\<close>.
\<close>
lemma forest_induct [consumes 1, case_names Fnil Fcons]:
@@ -203,7 +203,7 @@
R(Fnil);
!!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f))
|] ==> R(f)"
- -- \<open>Essentially the same as list induction.\<close>
+ \<comment> \<open>Essentially the same as list induction.\<close>
apply (erule tree_forest.mutual_induct
[THEN conjunct2, THEN spec, THEN [2] rev_mp])
apply (rule TrueI)
@@ -219,7 +219,7 @@
text \<open>
- \medskip Theorems about @{text map}.
+ \medskip Theorems about \<open>map\<close>.
\<close>
lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
@@ -231,7 +231,7 @@
text \<open>
- \medskip Theorems about @{text size}.
+ \medskip Theorems about \<open>size\<close>.
\<close>
lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
@@ -241,7 +241,7 @@
by (induct set: tree_forest) (simp_all add: length_app)
text \<open>
- \medskip Theorems about @{text preorder}.
+ \medskip Theorems about \<open>preorder\<close>.
\<close>
lemma preorder_map:
--- a/src/ZF/InfDatatype.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/InfDatatype.thy Mon Dec 07 10:23:50 2015 +0100
@@ -70,7 +70,7 @@
==> f: Vfrom(A,csucc(K))"
by (blast intro: fun_Vcsucc [THEN subsetD])
-text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
+text\<open>Remove \<open>\<subseteq>\<close> from the rule above\<close>
lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
(** Version where K itself is the index set **)
--- a/src/ZF/IntDiv_ZF.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/IntDiv_ZF.thy Mon Dec 07 10:23:50 2015 +0100
@@ -401,7 +401,7 @@
subsection\<open>Correctness of posDivAlg,
- the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"}\<close>
+ the Division Algorithm for \<open>a\<ge>0\<close> and \<open>b>0\<close>\<close>
lemma adjust_eq [simp]:
"adjust(b, <q,r>) = (let diff = r$-b in
--- a/src/ZF/Int_ZF.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Int_ZF.thy Mon Dec 07 10:23:50 2015 +0100
@@ -17,11 +17,11 @@
"int == (nat*nat)//intrel"
definition
- int_of :: "i=>i" --\<open>coercion from nat to int\<close> ("$# _" [80] 80) where
+ int_of :: "i=>i" \<comment>\<open>coercion from nat to int\<close> ("$# _" [80] 80) where
"$# m == intrel `` {<natify(m), 0>}"
definition
- intify :: "i=>i" --\<open>coercion from ANYTHING to int\<close> where
+ intify :: "i=>i" \<comment>\<open>coercion from ANYTHING to int\<close> where
"intify(m) == if m \<in> int then m else $#0"
definition
@@ -50,7 +50,7 @@
definition
zmagnitude :: "i=>i" where
- --\<open>could be replaced by an absolute value function from int to int?\<close>
+ \<comment>\<open>could be replaced by an absolute value function from int to int?\<close>
"zmagnitude(z) ==
THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
(znegative(z) & $- z = $# m))"
@@ -770,7 +770,7 @@
by (simp add: not_zless_iff_zle [THEN iff_sym])
-subsection\<open>More subtraction laws (for @{text zcompare_rls})\<close>
+subsection\<open>More subtraction laws (for \<open>zcompare_rls\<close>)\<close>
lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
by (simp add: zdiff_def zadd_ac)
@@ -808,7 +808,7 @@
text\<open>This list of rewrites simplifies (in)equalities by bringing subtractions
to the top and then moving negative terms to the other side.
- Use with @{text zadd_ac}\<close>
+ Use with \<open>zadd_ac\<close>\<close>
lemmas zcompare_rls =
zdiff_def [symmetric]
zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2
--- a/src/ZF/List_ZF.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/List_ZF.thy Mon Dec 07 10:23:50 2015 +0100
@@ -98,7 +98,7 @@
definition
nth :: "[i, i]=>i" where
- --\<open>returns the (n+1)th element of a list, or 0 if the
+ \<comment>\<open>returns the (n+1)th element of a list, or 0 if the
list is too short.\<close>
"nth(n, as) == list_rec(\<lambda>n\<in>nat. 0,
%a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n"
--- a/src/ZF/Order.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Order.thy Mon Dec 07 10:23:50 2015 +0100
@@ -11,8 +11,8 @@
theory Order imports WF Perm begin
-text \<open>We adopt the following convention: @{text ord} is used for
- strict orders and @{text order} is used for their reflexive
+text \<open>We adopt the following convention: \<open>ord\<close> is used for
+ strict orders and \<open>order\<close> is used for their reflexive
counterparts.\<close>
definition
--- a/src/ZF/OrderArith.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/OrderArith.thy Mon Dec 07 10:23:50 2015 +0100
@@ -87,7 +87,7 @@
lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
apply (rule wf_onI2)
apply (subgoal_tac "\<forall>x\<in>A. Inl (x) \<in> Ba")
- --\<open>Proving the lemma, which is needed twice!\<close>
+ \<comment>\<open>Proving the lemma, which is needed twice!\<close>
prefer 2
apply (erule_tac V = "y \<in> A + B" in thin_rl)
apply (rule_tac ballI)
@@ -369,8 +369,8 @@
apply blast
done
-text\<open>But note that the combination of @{text wf_imp_wf_on} and
- @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
+text\<open>But note that the combination of \<open>wf_imp_wf_on\<close> and
+ \<open>wf_rvimage\<close> gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
lemma wf_on_rvimage: "[| f \<in> A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
apply (rule wf_onI2)
apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z \<in> Ba")
@@ -460,7 +460,7 @@
lemma wf_times: "A \<inter> B = 0 ==> wf(A*B)"
by (simp add: wf_def, blast)
-text\<open>Could also be used to prove @{text wf_radd}\<close>
+text\<open>Could also be used to prove \<open>wf_radd\<close>\<close>
lemma wf_Un:
"[| range(r) \<inter> domain(s) = 0; wf(r); wf(s) |] ==> wf(r \<union> s)"
apply (simp add: wf_def, clarify)
--- a/src/ZF/Ordinal.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Ordinal.thy Mon Dec 07 10:23:50 2015 +0100
@@ -390,7 +390,7 @@
by (rule_tac i = i and j = j in Ord_linear2, auto)
-subsubsection \<open>Some Rewrite Rules for @{text "<"}, @{text "\<le>"}\<close>
+subsubsection \<open>Some Rewrite Rules for \<open><\<close>, \<open>\<le>\<close>\<close>
lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
by (unfold lt_def, blast)
--- a/src/ZF/UNITY/AllocBase.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Mon Dec 07 10:23:50 2015 +0100
@@ -45,11 +45,11 @@
"all_distinct(l) == all_distinct0(l)=1"
definition
- state_of :: "i =>i" --\<open>coersion from anyting to state\<close> where
+ state_of :: "i =>i" \<comment>\<open>coersion from anyting to state\<close> where
"state_of(s) == if s \<in> state then s else st0"
definition
- lift :: "i =>(i=>i)" --\<open>simplifies the expression of programs\<close> where
+ lift :: "i =>(i=>i)" \<comment>\<open>simplifies the expression of programs\<close> where
"lift(x) == %s. s`x"
text\<open>function to show that the set of variables is infinite\<close>
--- a/src/ZF/UNITY/Distributor.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/Distributor.thy Mon Dec 07 10:23:50 2015 +0100
@@ -37,10 +37,10 @@
distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
locale distr =
- fixes In --\<open>items to distribute\<close>
- and iIn --\<open>destinations of items to distribute\<close>
- and Out --\<open>distributed items\<close>
- and A --\<open>the type of items being distributed\<close>
+ fixes In \<comment>\<open>items to distribute\<close>
+ and iIn \<comment>\<open>destinations of items to distribute\<close>
+ and Out \<comment>\<open>distributed items\<close>
+ and A \<comment>\<open>the type of items being distributed\<close>
and D
assumes
var_assumes [simp]: "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
--- a/src/ZF/UNITY/Merge.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/Merge.thy Mon Dec 07 10:23:50 2015 +0100
@@ -64,10 +64,10 @@
(** State definitions. OUTPUT variables are locals **)
locale merge =
- fixes In --\<open>merge's INPUT histories: streams to merge\<close>
- and Out --\<open>merge's OUTPUT history: merged items\<close>
- and iOut --\<open>merge's OUTPUT history: origins of merged items\<close>
- and A --\<open>the type of items being merged\<close>
+ fixes In \<comment>\<open>merge's INPUT histories: streams to merge\<close>
+ and Out \<comment>\<open>merge's OUTPUT history: merged items\<close>
+ and iOut \<comment>\<open>merge's OUTPUT history: origins of merged items\<close>
+ and A \<comment>\<open>the type of items being merged\<close>
and M
assumes var_assumes [simp]:
"(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
--- a/src/ZF/UNITY/Mutex.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/Mutex.thy Mon Dec 07 10:23:50 2015 +0100
@@ -27,7 +27,7 @@
abbreviation "u == Var([0,1])"
abbreviation "v == Var([1,0])"
-axiomatization where --\<open>* Type declarations *\<close>
+axiomatization where \<comment>\<open>* Type declarations *\<close>
p_type: "type_of(p)=bool & default_val(p)=0" and
m_type: "type_of(m)=int & default_val(m)=#0" and
n_type: "type_of(n)=int & default_val(n)=#0" and
--- a/src/ZF/UNITY/UNITY.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/UNITY.thy Mon Dec 07 10:23:50 2015 +0100
@@ -20,7 +20,7 @@
definition
mk_program :: "[i,i,i]=>i" where
- --\<open>The definition yields a program thanks to the coercions
+ \<comment>\<open>The definition yields a program thanks to the coercions
init \<inter> state, acts \<inter> Pow(state*state), etc.\<close>
"mk_program(init, acts, allowed) ==
<init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
@@ -70,7 +70,7 @@
definition "constrains" :: "[i, i] => i" (infixl "co" 60) where
"A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
- --\<open>the condition @{term "st_set(A)"} makes the definition slightly
+ \<comment>\<open>the condition @{term "st_set(A)"} makes the definition slightly
stronger than the HOL one\<close>
definition unless :: "[i, i] => i" (infixl "unless" 60) where
@@ -199,7 +199,7 @@
"Pow(state*state) \<subseteq> AllowedActs(F) \<longleftrightarrow> AllowedActs(F)=Pow(state*state)"
by (cut_tac F = F in AllowedActs_type, auto)
-subsubsection\<open>Eliminating @{text "\<inter> state"} from expressions\<close>
+subsubsection\<open>Eliminating \<open>\<inter> state\<close> from expressions\<close>
lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)"
by (cut_tac F = F in Init_type, blast)
--- a/src/ZF/UNITY/WFair.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/UNITY/WFair.thy Mon Dec 07 10:23:50 2015 +0100
@@ -283,7 +283,7 @@
lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto> B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto> B) & F \<in> program & st_set(B)"
by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)
-text\<open>Set difference: maybe combine with @{text leadsTo_weaken_L}??\<close>
+text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close>
lemma leadsTo_Diff:
"[| F: (A-B) \<longmapsto> C; F \<in> B \<longmapsto> C; st_set(C) |]
==> F \<in> A \<longmapsto> C"
--- a/src/ZF/Univ.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Univ.thy Mon Dec 07 10:23:50 2015 +0100
@@ -77,7 +77,7 @@
apply (subst Vfrom)
apply (subst Vfrom, rule subset_refl [THEN Un_mono])
apply (rule UN_least)
-txt\<open>expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions\<close>
+txt\<open>expand \<open>rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))\<close> in assumptions\<close>
apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
apply (rule subset_trans)
apply (erule_tac [2] UN_upper)
@@ -748,7 +748,7 @@
"[| f: W -||> univ(A); W \<subseteq> univ(A) |] ==> f \<in> univ(A)"
by (erule FiniteFun_univ [THEN subsetD], assumption)
-text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
+text\<open>Remove \<open>\<subseteq>\<close> from the rule above\<close>
lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
--- a/src/ZF/WF.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/WF.thy Mon Dec 07 10:23:50 2015 +0100
@@ -116,7 +116,7 @@
lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
-text\<open>The form of this rule is designed to match @{text wfI}\<close>
+text\<open>The form of this rule is designed to match \<open>wfI\<close>\<close>
lemma wf_induct2:
"[| wf(r); a \<in> A; field(r)<=A;
!!x.[| x \<in> A; \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
@@ -287,7 +287,7 @@
apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
apply typecheck
apply (unfold is_recfun_def wftrec_def)
- --\<open>Applying the substitution: must keep the quantified assumption!\<close>
+ \<comment>\<open>Applying the substitution: must keep the quantified assumption!\<close>
apply (rule lam_cong [OF refl])
apply (drule underD)
apply (fold is_recfun_def)
--- a/src/ZF/ZF.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ZF.thy Mon Dec 07 10:23:50 2015 +0100
@@ -15,9 +15,9 @@
instance i :: "term" ..
axiomatization
- zero :: "i" ("0") --\<open>the empty set\<close> and
- Pow :: "i => i" --\<open>power sets\<close> and
- Inf :: "i" --\<open>infinite set\<close>
+ zero :: "i" ("0") \<comment>\<open>the empty set\<close> and
+ Pow :: "i => i" \<comment>\<open>power sets\<close> and
+ Inf :: "i" \<comment>\<open>infinite set\<close>
text \<open>Bounded Quantifiers\<close>
consts
@@ -56,7 +56,7 @@
Pair :: "[i, i] => i"
fst :: "i => i"
snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::{}" --\<open>for pattern-matching\<close>
+ split :: "[[i, i] => 'a, i] => 'a::{}" \<comment>\<open>for pattern-matching\<close>
text \<open>Sigma and Pi Operators\<close>
consts
@@ -69,35 +69,35 @@
range :: "i => i"
field :: "i => i"
converse :: "i => i"
- relation :: "i => o" --\<open>recognizes sets of pairs\<close>
- "function" :: "i => o" --\<open>recognizes functions; can have non-pairs\<close>
+ relation :: "i => o" \<comment>\<open>recognizes sets of pairs\<close>
+ "function" :: "i => o" \<comment>\<open>recognizes functions; can have non-pairs\<close>
Lambda :: "[i, i => i] => i"
restrict :: "[i, i] => i"
text \<open>Infixes in order of decreasing precedence\<close>
consts
- Image :: "[i, i] => i" (infixl "``" 90) --\<open>image\<close>
- vimage :: "[i, i] => i" (infixl "-``" 90) --\<open>inverse image\<close>
- "apply" :: "[i, i] => i" (infixl "`" 90) --\<open>function application\<close>
- "Int" :: "[i, i] => i" (infixl "Int" 70) --\<open>binary intersection\<close>
- "Un" :: "[i, i] => i" (infixl "Un" 65) --\<open>binary union\<close>
- Diff :: "[i, i] => i" (infixl "-" 65) --\<open>set difference\<close>
- Subset :: "[i, i] => o" (infixl "<=" 50) --\<open>subset relation\<close>
+ Image :: "[i, i] => i" (infixl "``" 90) \<comment>\<open>image\<close>
+ vimage :: "[i, i] => i" (infixl "-``" 90) \<comment>\<open>inverse image\<close>
+ "apply" :: "[i, i] => i" (infixl "`" 90) \<comment>\<open>function application\<close>
+ "Int" :: "[i, i] => i" (infixl "Int" 70) \<comment>\<open>binary intersection\<close>
+ "Un" :: "[i, i] => i" (infixl "Un" 65) \<comment>\<open>binary union\<close>
+ Diff :: "[i, i] => i" (infixl "-" 65) \<comment>\<open>set difference\<close>
+ Subset :: "[i, i] => o" (infixl "<=" 50) \<comment>\<open>subset relation\<close>
axiomatization
- mem :: "[i, i] => o" (infixl ":" 50) --\<open>membership relation\<close>
+ mem :: "[i, i] => o" (infixl ":" 50) \<comment>\<open>membership relation\<close>
abbreviation
- not_mem :: "[i, i] => o" (infixl "~:" 50) --\<open>negated membership relation\<close>
+ not_mem :: "[i, i] => o" (infixl "~:" 50) \<comment>\<open>negated membership relation\<close>
where "x ~: y == ~ (x : y)"
abbreviation
- cart_prod :: "[i, i] => i" (infixr "*" 80) --\<open>Cartesian product\<close>
+ cart_prod :: "[i, i] => i" (infixr "*" 80) \<comment>\<open>Cartesian product\<close>
where "A * B == Sigma(A, %_. B)"
abbreviation
- function_space :: "[i, i] => i" (infixr "->" 60) --\<open>function space\<close>
+ function_space :: "[i, i] => i" (infixr "->" 60) \<comment>\<open>function space\<close>
where "A -> B == Pi(A, %_. B)"
@@ -616,8 +616,8 @@
declare Pow_iff [iff]
-lemmas Pow_bottom = empty_subsetI [THEN PowI] --\<open>@{term"0 \<in> Pow(B)"}\<close>
-lemmas Pow_top = subset_refl [THEN PowI] --\<open>@{term"A \<in> Pow(A)"}\<close>
+lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
+lemmas Pow_top = subset_refl [THEN PowI] \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
--- a/src/ZF/Zorn.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Zorn.thy Mon Dec 07 10:23:50 2015 +0100
@@ -114,7 +114,7 @@
==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
apply (erule TFin_induct)
apply (rule impI [THEN ballI])
-txt\<open>case split using @{text TFin_linear_lemma1}\<close>
+txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
assumption+)
apply (blast del: subsetI
@@ -176,7 +176,7 @@
subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close>
-text\<open>NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
+text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset
relation!\<close>
text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
@@ -248,7 +248,7 @@
apply (unfold chain_def)
apply (rule CollectI, blast, safe)
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
- txt\<open>@{text "Blast_tac's"} slow\<close>
+ txt\<open>\<open>Blast_tac's\<close> slow\<close>
done
theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
@@ -404,7 +404,7 @@
prefer 2 apply (blast elim: equalityE)
apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
prefer 2 apply (blast elim: equalityE)
-txt\<open>For proving @{text "x \<in> next`\<Union>(...)"}.
+txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
Abrial and Laffitte's justification appears to be faulty.\<close>
apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y})
\<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
@@ -449,7 +449,7 @@
shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
proof -
have "Preorder(r)" using po by (simp add: partial_order_on_def)
- --\<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
+ \<comment>\<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
let ?B = "\<lambda>x\<in>field(r). r -`` {x}" let ?S = "?B `` field(r)"
have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
--- a/src/ZF/equalities.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/equalities.thy Mon Dec 07 10:23:50 2015 +0100
@@ -20,7 +20,7 @@
text \<open>\medskip
The following are not added to the default simpset because
- (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close>
+ (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
by blast
--- a/src/ZF/ex/CoUnit.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/CoUnit.thy Mon Dec 07 10:23:50 2015 +0100
@@ -25,14 +25,14 @@
"counit" = Con ("x \<in> counit")
inductive_cases ConE: "Con(x) \<in> counit"
- -- \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close>
+ \<comment> \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close>
lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y"
- -- \<open>Proving freeness results.\<close>
+ \<comment> \<open>Proving freeness results.\<close>
by (auto elim!: counit.free_elims)
lemma counit_eq_univ: "counit = quniv(0)"
- -- \<open>Should be a singleton, not everything!\<close>
+ \<comment> \<open>Should be a singleton, not everything!\<close>
apply (rule counit.dom_subset [THEN equalityI])
apply (rule subsetI)
apply (erule counit.coinduct)
@@ -56,7 +56,7 @@
inductive_cases Con2E: "Con2(x, y) \<in> counit2"
lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'"
- -- \<open>Proving freeness results.\<close>
+ \<comment> \<open>Proving freeness results.\<close>
by (fast elim!: counit2.free_elims)
lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))"
@@ -74,7 +74,7 @@
lemma counit2_Int_Vset_subset [rule_format]:
"Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y"
- -- \<open>Lemma for proving finality.\<close>
+ \<comment> \<open>Lemma for proving finality.\<close>
apply (erule trans_induct)
apply (tactic "safe_tac (put_claset subset_cs @{context})")
apply (erule counit2.cases)
--- a/src/ZF/ex/Group.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/Group.thy Mon Dec 07 10:23:50 2015 +0100
@@ -274,14 +274,14 @@
text \<open>
Since @{term H} is nonempty, it contains some element @{term x}. Since
- it is closed under inverse, it contains @{text "inv x"}. Since
- it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
+ it is closed under inverse, it contains \<open>inv x\<close>. Since
+ it is closed under product, it contains \<open>x \<cdot> inv x = \<one>\<close>.
\<close>
text \<open>
Since @{term H} is nonempty, it contains some element @{term x}. Since
- it is closed under inverse, it contains @{text "inv x"}. Since
- it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
+ it is closed under inverse, it contains \<open>inv x\<close>. Since
+ it is closed under product, it contains \<open>x \<cdot> inv x = \<one>\<close>.
\<close>
lemma (in group) one_in_subset:
@@ -628,7 +628,7 @@
lemma (in group) coset_join2:
"\<lbrakk>x \<in> carrier(G); subgroup(H,G); x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
- --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
+ \<comment>\<open>Alternative proof is to put @{term "x=\<one>"} in \<open>repr_independence\<close>.\<close>
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
lemma (in group) r_coset_subset_G:
@@ -788,7 +788,7 @@
done
-subsubsection \<open>Set of inverses of an @{text r_coset}.\<close>
+subsubsection \<open>Set of inverses of an \<open>r_coset\<close>.\<close>
lemma (in normal) rcos_inv:
assumes x: "x \<in> carrier(G)"
@@ -817,7 +817,7 @@
-subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
+subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
lemma (in group) setmult_rcos_assoc:
"\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
@@ -852,7 +852,7 @@
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
- -- \<open>generalizes @{text subgroup_mult_id}\<close>
+ \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
by (auto simp add: RCOSETS_def subset
setmult_rcos_assoc subgroup_mult_id normal_axioms normal.axioms)
@@ -897,7 +897,7 @@
qed
qed
-text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
+text\<open>Equivalence classes of \<open>rcong\<close> correspond to left cosets.
Was there a mistake in the definitions? I'd have expected them to
correspond to right cosets.\<close>
lemma (in subgroup) l_coset_eq_rcong:
@@ -1021,7 +1021,7 @@
definition
FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
- --\<open>Actually defined for groups rather than monoids\<close>
+ \<comment>\<open>Actually defined for groups rather than monoids\<close>
"G Mod H ==
<rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
@@ -1085,7 +1085,7 @@
definition
kernel :: "[i,i,i] => i" where
- --\<open>the kernel of a homomorphism\<close>
+ \<comment>\<open>the kernel of a homomorphism\<close>
"kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
@@ -1215,7 +1215,7 @@
hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
- --\<open>The witness is @{term "kernel(G,H,h) #> g"}\<close>
+ \<comment>\<open>The witness is @{term "kernel(G,H,h) #> g"}\<close>
by (force simp add: FactGroup_def RCOSETS_def
image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
qed
--- a/src/ZF/ex/Limit.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/Limit.thy Mon Dec 07 10:23:50 2015 +0100
@@ -1295,7 +1295,7 @@
apply (simp add: Dinf_def [symmetric])
apply (rule ballI)
apply (simplesubst lub_iprod)
- --\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
+ \<comment>\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
apply (assumption | rule chain_Dinf emb_chain_cpo)+
apply simp
apply (subst Rp_cont [THEN cont_lub])
@@ -1736,7 +1736,7 @@
apply blast
apply assumption
apply (simplesubst eps_split_right_le)
- --\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
+ \<comment>\<open>Subst would rewrite the lhs. We want to change the rhs.\<close>
prefer 2 apply assumption
apply simp
apply (assumption | rule add_le_self nat_0I nat_succI)+
--- a/src/ZF/ex/Primes.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/Primes.thy Mon Dec 07 10:23:50 2015 +0100
@@ -12,22 +12,22 @@
"m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
definition
- is_gcd :: "[i,i,i]=>o" --\<open>definition of great common divisor\<close> where
+ is_gcd :: "[i,i,i]=>o" \<comment>\<open>definition of great common divisor\<close> where
"is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
(\<forall>d\<in>nat. (d dvd m) & (d dvd n) \<longrightarrow> d dvd p)"
definition
- gcd :: "[i,i]=>i" --\<open>Euclid's algorithm for the gcd\<close> where
+ gcd :: "[i,i]=>i" \<comment>\<open>Euclid's algorithm for the gcd\<close> where
"gcd(m,n) == transrec(natify(n),
%n f. \<lambda>m \<in> nat.
if n=0 then m else f`(m mod n)`n) ` natify(m)"
definition
- coprime :: "[i,i]=>o" --\<open>the coprime relation\<close> where
+ coprime :: "[i,i]=>o" \<comment>\<open>the coprime relation\<close> where
"coprime(m,n) == gcd(m,n) = 1"
definition
- prime :: i --\<open>the set of prime numbers\<close> where
+ prime :: i \<comment>\<open>the set of prime numbers\<close> where
"prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p \<longrightarrow> m=1 | m=p)}"
--- a/src/ZF/ex/Ramsey.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/Ramsey.thy Mon Dec 07 10:23:50 2015 +0100
@@ -31,7 +31,7 @@
"Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)"
definition
- Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality"
+ Atleast :: "[i,i]=>o" where \<comment> "not really necessary: ZF defines cardinality"
"Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))"
definition
--- a/src/ZF/ex/misc.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ex/misc.thy Mon Dec 07 10:23:50 2015 +0100
@@ -19,11 +19,11 @@
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
- -- \<open>Variant of the problem above.\<close>
+ \<comment> \<open>Variant of the problem above.\<close>
by blast
lemma "\<exists>!x. f (g(x)) = x \<Longrightarrow> \<exists>!y. g (f(y)) = y"
- -- \<open>A unique fixpoint theorem --- @{text fast}/@{text best}/@{text auto} all fail.\<close>
+ \<comment> \<open>A unique fixpoint theorem --- \<open>fast\<close>/\<open>best\<close>/\<open>auto\<close> all fail.\<close>
apply (erule ex1E, rule ex1I, erule subst_context)
apply (rule subst, assumption, erule allE, rule subst_context, erule mp)
apply (erule subst_context)
--- a/src/ZF/upair.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/upair.thy Mon Dec 07 10:23:50 2015 +0100
@@ -195,7 +195,7 @@
by blast
-subsection\<open>Conditional Terms: @{text "if-then-else"}\<close>
+subsection\<open>Conditional Terms: \<open>if-then-else\<close>\<close>
lemma if_true [simp]: "(if True then a else b) = a"
by (unfold if_def, blast)