src/ZF/Constructible/Rank.thy
 changeset 60770 240563fbf41d parent 58871 c399ae4b836f child 61798 27f3c10b0b50
```     1.1 --- a/src/ZF/Constructible/Rank.thy	Thu Jul 23 14:20:51 2015 +0200
1.2 +++ b/src/ZF/Constructible/Rank.thy	Thu Jul 23 14:25:05 2015 +0200
1.3 @@ -2,12 +2,12 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5  *)
1.6
1.7 -section {*Absoluteness for Order Types, Rank Functions and Well-Founded
1.8 -         Relations*}
1.9 +section \<open>Absoluteness for Order Types, Rank Functions and Well-Founded
1.10 +         Relations\<close>
1.11
1.12  theory Rank imports WF_absolute begin
1.13
1.14 -subsection {*Order Types: A Direct Construction by Replacement*}
1.15 +subsection \<open>Order Types: A Direct Construction by Replacement\<close>
1.16
1.17  locale M_ordertype = M_basic +
1.18  assumes well_ord_iso_separation:
1.19 @@ -15,7 +15,7 @@
1.20        ==> separation (M, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[M]. (\<exists>p[M].
1.21                       fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
1.22    and obase_separation:
1.23 -     --{*part of the order type formalization*}
1.24 +     --\<open>part of the order type formalization\<close>
1.25       "[| M(A); M(r) |]
1.26        ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
1.27               ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
1.28 @@ -34,8 +34,8 @@
1.29               pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
1.30
1.31
1.32 -text{*Inductive argument for Kunen's Lemma I 6.1, etc.
1.33 -      Simple proof from Halmos, page 72*}
1.34 +text\<open>Inductive argument for Kunen's Lemma I 6.1, etc.
1.35 +      Simple proof from Halmos, page 72\<close>
1.36  lemma  (in M_ordertype) wellordered_iso_subset_lemma:
1.37       "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;
1.38         M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
1.39 @@ -48,8 +48,8 @@
1.40  done
1.41
1.42
1.43 -text{*Kunen's Lemma I 6.1, page 14:
1.44 -      there's no order-isomorphism to an initial segment of a well-ordering*}
1.45 +text\<open>Kunen's Lemma I 6.1, page 14:
1.46 +      there's no order-isomorphism to an initial segment of a well-ordering\<close>
1.47  lemma (in M_ordertype) wellordered_iso_predD:
1.48       "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);
1.49         M(A);  M(f);  M(r) |] ==> x \<notin> A"
1.50 @@ -75,7 +75,7 @@
1.51  done
1.52
1.53
1.54 -text{*Simple consequence of Lemma 6.1*}
1.55 +text\<open>Simple consequence of Lemma 6.1\<close>
1.56  lemma (in M_ordertype) wellordered_iso_pred_eq:
1.57       "[| wellordered(M,A,r);
1.58         f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);
1.59 @@ -89,11 +89,11 @@
1.60  done
1.61
1.62
1.63 -text{*Following Kunen's Theorem I 7.6, page 17.  Note that this material is
1.64 -not required elsewhere.*}
1.65 +text\<open>Following Kunen's Theorem I 7.6, page 17.  Note that this material is
1.66 +not required elsewhere.\<close>
1.67
1.68 -text{*Can't use @{text well_ord_iso_preserving} because it needs the
1.69 -strong premise @{term "well_ord(A,r)"}*}
1.70 +text\<open>Can't use @{text well_ord_iso_preserving} because it needs the
1.71 +strong premise @{term "well_ord(A,r)"}\<close>
1.72  lemma (in M_ordertype) ord_iso_pred_imp_lt:
1.73       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
1.74           g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
1.75 @@ -103,18 +103,18 @@
1.76  apply (frule wellordered_is_trans_on, assumption)
1.77  apply (frule_tac y=y in transM, assumption)
1.78  apply (rule_tac i=i and j=j in Ord_linear_lt, auto)
1.79 -txt{*case @{term "i=j"} yields a contradiction*}
1.80 +txt\<open>case @{term "i=j"} yields a contradiction\<close>
1.81   apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in
1.82            wellordered_iso_predD [THEN notE])
1.83     apply (blast intro: wellordered_subset [OF _ pred_subset])
1.85    apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
1.86   apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
1.87 -txt{*case @{term "j<i"} also yields a contradiction*}
1.88 +txt\<open>case @{term "j<i"} also yields a contradiction\<close>
1.89  apply (frule restrict_ord_iso2, assumption+)
1.90  apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun])
1.91  apply (frule apply_type, blast intro: ltD)
1.92 -  --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
1.93 +  --\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
1.95  apply (subgoal_tac
1.96         "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r,
1.97 @@ -137,26 +137,26 @@
1.98
1.99  definition
1.100    obase :: "[i=>o,i,i] => i" where
1.101 -       --{*the domain of @{text om}, eventually shown to equal @{text A}*}
1.102 +       --\<open>the domain of @{text om}, eventually shown to equal @{text A}\<close>
1.103     "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) &
1.104                            g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
1.105
1.106  definition
1.107    omap :: "[i=>o,i,i,i] => o" where
1.108 -    --{*the function that maps wosets to order types*}
1.109 +    --\<open>the function that maps wosets to order types\<close>
1.110     "omap(M,A,r,f) ==
1.111          \<forall>z[M].
1.112           z \<in> f \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) &
1.113                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
1.114
1.115  definition
1.116 -  otype :: "[i=>o,i,i,i] => o" where --{*the order types themselves*}
1.117 +  otype :: "[i=>o,i,i,i] => o" where --\<open>the order types themselves\<close>
1.118     "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
1.119
1.120
1.121 -text{*Can also be proved with the premise @{term "M(z)"} instead of
1.122 +text\<open>Can also be proved with the premise @{term "M(z)"} instead of
1.123        @{term "M(f)"}, but that version is less useful.  This lemma
1.124 -      is also more useful than the definition, @{text omap_def}.*}
1.125 +      is also more useful than the definition, @{text omap_def}.\<close>
1.126  lemma (in M_ordertype) omap_iff:
1.127       "[| omap(M,A,r,f); M(A); M(f) |]
1.128        ==> z \<in> f \<longleftrightarrow>
1.129 @@ -256,7 +256,7 @@
1.130  done
1.131
1.132
1.133 -text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
1.134 +text\<open>This is not the final result: we must show @{term "oB(A,r) = A"}\<close>
1.135  lemma (in M_ordertype) omap_ord_iso:
1.136       "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
1.137         M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(obase(M,A,r),r,i,Memrel(i))"
1.138 @@ -266,15 +266,15 @@
1.139  apply (frule_tac a=x in apply_Pair, assumption)
1.140  apply (frule_tac a=y in apply_Pair, assumption)
1.141  apply (auto simp add: omap_iff)
1.142 - txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
1.143 + txt\<open>direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}\<close>
1.144   apply (blast intro: ltD ord_iso_pred_imp_lt)
1.145 - txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
1.146 + txt\<open>direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}\<close>
1.147  apply (rename_tac x y g ga)
1.148  apply (frule wellordered_is_linear, assumption,
1.149         erule_tac x=x and y=y in linearE, assumption+)
1.152  apply (blast elim: mem_irrefl)
1.153 -txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
1.154 +txt\<open>the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction\<close>
1.155  apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym)
1.156  done
1.157
1.158 @@ -284,7 +284,7 @@
1.159  apply (frule wellordered_is_trans_on, assumption)
1.160  apply (rule OrdI)
1.161          prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast)
1.162 -txt{*Hard part is to show that the image is a transitive set.*}
1.163 +txt\<open>Hard part is to show that the image is a transitive set.\<close>
1.164  apply (simp add: Transset_def, clarify)
1.165  apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]])
1.166  apply (rename_tac c j, clarify)
1.167 @@ -331,8 +331,8 @@
1.168
1.169
1.170
1.171 -text{*Main result: @{term om} gives the order-isomorphism
1.172 -      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
1.173 +text\<open>Main result: @{term om} gives the order-isomorphism
1.174 +      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"}\<close>
1.175  theorem (in M_ordertype) omap_ord_iso_otype:
1.176       "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
1.177         M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
1.178 @@ -390,15 +390,15 @@
1.179  apply (blast intro: well_ord_ord_iso well_ord_Memrel)
1.180  done
1.181
1.182 -subsection {*Kunen's theorem 5.4, page 127*}
1.183 +subsection \<open>Kunen's theorem 5.4, page 127\<close>
1.184
1.185 -text{*(a) The notion of Wellordering is absolute*}
1.186 +text\<open>(a) The notion of Wellordering is absolute\<close>
1.187  theorem (in M_ordertype) well_ord_abs [simp]:
1.188       "[| M(A); M(r) |] ==> wellordered(M,A,r) \<longleftrightarrow> well_ord(A,r)"
1.189  by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)
1.190
1.191
1.192 -text{*(b) Order types are absolute*}
1.193 +text\<open>(b) Order types are absolute\<close>
1.194  theorem (in M_ordertype)
1.195       "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
1.196         M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
1.197 @@ -406,11 +406,11 @@
1.198                   Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
1.199
1.200
1.201 -subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
1.202 +subsection\<open>Ordinal Arithmetic: Two Examples of Recursion\<close>
1.203
1.204 -text{*Note: the remainder of this theory is not needed elsewhere.*}
1.205 +text\<open>Note: the remainder of this theory is not needed elsewhere.\<close>
1.206
1.209
1.210  (*FIXME: update to use new techniques!!*)
1.211   (*This expresses ordinal addition in the language of ZF.  It also
1.212 @@ -478,7 +478,7 @@
1.213
1.214
1.215
1.216 -text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
1.217 +text\<open>@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF\<close>
1.219     "[| a\<le>j; M(i); M(j); M(a); M(f) |]
1.221 @@ -563,7 +563,7 @@
1.222  done
1.223
1.224
1.225 -subsubsection{*Ordinal Multiplication*}
1.226 +subsubsection\<open>Ordinal Multiplication\<close>
1.227
1.228  lemma omult_eqns_unique:
1.229       "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"
1.230 @@ -602,7 +602,7 @@
1.231      "[| M(i); M(x); M(g); function(g) |]
1.232       ==> M(THE z. omult_eqns(i, x, g, z))"
1.233  apply (case_tac "Ord(x)")
1.234 - prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
1.235 + prefer 2 apply (simp add: omult_eqns_Not) --\<open>trivial, non-Ord case\<close>
1.236  apply (erule Ord_cases)
1.239 @@ -669,11 +669,11 @@
1.240
1.241
1.242
1.243 -subsection {*Absoluteness of Well-Founded Relations*}
1.244 +subsection \<open>Absoluteness of Well-Founded Relations\<close>
1.245
1.246 -text{*Relativized to @{term M}: Every well-founded relation is a subset of some
1.247 +text\<open>Relativized to @{term M}: Every well-founded relation is a subset of some
1.248  inverse image of an ordinal.  Key step is the construction (in @{term M}) of a
1.249 -rank function.*}
1.250 +rank function.\<close>
1.251
1.252  locale M_wfrank = M_trancl +
1.253    assumes wfrank_separation:
1.254 @@ -698,8 +698,8 @@
1.255               ordinal(M,rangef)))"
1.256
1.257
1.258 -text{*Proving that the relativized instances of Separation or Replacement
1.259 -agree with the "real" ones.*}
1.260 +text\<open>Proving that the relativized instances of Separation or Replacement
1.261 +agree with the "real" ones.\<close>
1.262
1.263  lemma (in M_wfrank) wfrank_separation':
1.264       "M(r) ==>
1.265 @@ -726,8 +726,8 @@
1.266  apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
1.267  done
1.268
1.269 -text{*This function, defined using replacement, is a rank function for
1.270 -well-founded relations within the class M.*}
1.271 +text\<open>This function, defined using replacement, is a rank function for
1.272 +well-founded relations within the class M.\<close>
1.273  definition
1.274    wellfoundedrank :: "[i=>o,i,i] => i" where
1.275      "wellfoundedrank(M,r,A) ==
1.276 @@ -766,16 +766,16 @@
1.277  apply (rule wellfounded_induct, assumption, erule (1) transM)
1.278    apply simp
1.279   apply (blast intro: Ord_wfrank_separation', clarify)
1.280 -txt{*The reasoning in both cases is that we get @{term y} such that
1.281 +txt\<open>The reasoning in both cases is that we get @{term y} such that
1.282     @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
1.283 -   @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
1.284 +   @{term "f`y = restrict(f, r^+ -`` {y})"}.\<close>
1.285  apply (rule OrdI [OF _ Ord_is_Transset])
1.286 - txt{*An ordinal is a transitive set...*}
1.287 + txt\<open>An ordinal is a transitive set...\<close>
1.289   apply clarify
1.290   apply (frule apply_recfun2, assumption)
1.291   apply (force simp add: restrict_iff)
1.292 -txt{*...of ordinals.  This second case requires the induction hyp.*}
1.293 +txt\<open>...of ordinals.  This second case requires the induction hyp.\<close>
1.294  apply clarify
1.295  apply (rename_tac i y)
1.296  apply (frule apply_recfun2, assumption)
1.297 @@ -799,9 +799,9 @@
1.299  apply (rule OrdI [OF _ Ord_is_Transset])
1.300   prefer 2
1.301 - txt{*by our previous result the range consists of ordinals.*}
1.302 + txt\<open>by our previous result the range consists of ordinals.\<close>
1.303   apply (blast intro: Ord_wfrank_range)
1.304 -txt{*We still must show that the range is a transitive set.*}
1.305 +txt\<open>We still must show that the range is a transitive set.\<close>
1.306  apply (simp add: Transset_def, clarify, simp)
1.307  apply (rename_tac x i f u)
1.308  apply (frule is_recfun_imp_in_r, assumption)
1.309 @@ -814,7 +814,7 @@
1.310     apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
1.311    apply simp
1.312  apply blast
1.313 -txt{*Unicity requirement of Replacement*}
1.314 +txt\<open>Unicity requirement of Replacement\<close>
1.315  apply clarify
1.316  apply (frule apply_recfun2, assumption)
1.317  apply (simp add: trans_trancl is_recfun_cut)
1.318 @@ -824,7 +824,7 @@
1.319      "[| wellfounded(M,r); M(r); M(A)|]
1.320       ==> function(wellfoundedrank(M,r,A))"
1.321  apply (simp add: wellfoundedrank_def function_def, clarify)
1.322 -txt{*Uniqueness: repeated below!*}
1.323 +txt\<open>Uniqueness: repeated below!\<close>
1.324  apply (drule is_recfun_functional, assumption)
1.325       apply (blast intro: wellfounded_trancl)
1.326      apply (simp_all add: trancl_subset_times trans_trancl)
1.327 @@ -841,7 +841,7 @@
1.328  apply (rule_tac x=x in ReplaceI)
1.329    apply simp
1.330    apply (rule_tac x=f in rexI, blast, simp_all)
1.331 -txt{*Uniqueness (for Replacement): repeated above!*}
1.332 +txt\<open>Uniqueness (for Replacement): repeated above!\<close>
1.333  apply clarify
1.334  apply (drule is_recfun_functional, assumption)
1.335      apply (blast intro: wellfounded_trancl)
1.336 @@ -875,7 +875,7 @@
1.337    apply (rule_tac x="range(f)" in rexI)
1.338    apply blast
1.339   apply simp_all
1.340 -txt{*Unicity requirement of Replacement*}
1.341 +txt\<open>Unicity requirement of Replacement\<close>
1.342  apply clarify
1.343  apply (drule is_recfun_functional, assumption)
1.344      apply (blast intro: wellfounded_trancl)
1.345 @@ -897,12 +897,12 @@
1.346  apply (frule is_recfun_restrict [of concl: "r^+" a])
1.347      apply (rule trans_trancl, assumption)
1.348     apply (simp_all add: r_into_trancl trancl_subset_times)
1.349 -txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
1.350 +txt\<open>Still the same goal, but with new @{text is_recfun} assumptions.\<close>