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.84    apply (simp add: trans_pred_pred_eq)
    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.94  apply (simp add: pred_iff) 
    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.150 -txt{*the case @{term "x=y"} leads to immediate contradiction*} 
   1.151 +txt\<open>the case @{term "x=y"} leads to immediate contradiction\<close> 
   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.207 -subsubsection{*Ordinal Addition*}
   1.208 +subsubsection\<open>Ordinal Addition\<close>
   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.218  lemma (in M_ord_arith) is_oadd_fun_iff:
   1.219     "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
   1.220      ==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
   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.237    apply (simp add: omult_eqns_0)
   1.238   apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
   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.288   apply (simp add: Transset_def)
   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.298  apply (simp add: wellfoundedrank_def)
   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>
   1.351  apply (simp add: wellfoundedrank_eq)
   1.352  apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   1.353     apply (simp_all add: transM [of a])
   1.354 -txt{*We have used equations for wellfoundedrank and now must use some
   1.355 -    for  @{text is_recfun}. *}
   1.356 +txt\<open>We have used equations for wellfoundedrank and now must use some
   1.357 +    for  @{text is_recfun}.\<close>
   1.358  apply (rule_tac a=a in rangeI)
   1.359  apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
   1.360                   r_into_trancl apply_recfun r_into_trancl)