src/ZF/Constructible/WF_absolute.thy
changeset 60770 240563fbf41d
parent 58871 c399ae4b836f
child 61798 27f3c10b0b50
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Thu Jul 23 14:20:51 2015 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Thu Jul 23 14:25:05 2015 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5  *)
     1.6  
     1.7 -section {*Absoluteness of Well-Founded Recursion*}
     1.8 +section \<open>Absoluteness of Well-Founded Recursion\<close>
     1.9  
    1.10  theory WF_absolute imports WFrec begin
    1.11  
    1.12 -subsection{*Transitive closure without fixedpoints*}
    1.13 +subsection\<open>Transitive closure without fixedpoints\<close>
    1.14  
    1.15  definition
    1.16    rtrancl_alt :: "[i,i]=>i" where
    1.17 @@ -38,11 +38,11 @@
    1.18  apply (simp add: rtrancl_alt_def, clarify)
    1.19  apply (frule rtrancl_type [THEN subsetD], clarify, simp)
    1.20  apply (erule rtrancl_induct)
    1.21 - txt{*Base case, trivial*}
    1.22 + txt\<open>Base case, trivial\<close>
    1.23   apply (rule_tac x=0 in bexI)
    1.24    apply (rule_tac x="\<lambda>x\<in>1. xa" in bexI)
    1.25     apply simp_all
    1.26 -txt{*Inductive step*}
    1.27 +txt\<open>Inductive step\<close>
    1.28  apply clarify
    1.29  apply (rename_tac n f)
    1.30  apply (rule_tac x="succ(n)" in bexI)
    1.31 @@ -60,7 +60,7 @@
    1.32  
    1.33  definition
    1.34    rtran_closure_mem :: "[i=>o,i,i,i] => o" where
    1.35 -    --{*The property of belonging to @{text "rtran_closure(r)"}*}
    1.36 +    --\<open>The property of belonging to @{text "rtran_closure(r)"}\<close>
    1.37      "rtran_closure_mem(M,A,r,p) ==
    1.38                \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.39                 omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
    1.40 @@ -120,7 +120,7 @@
    1.41  lemma (in M_trancl) rtrancl_abs [simp]:
    1.42       "[| M(r); M(z) |] ==> rtran_closure(M,r,z) \<longleftrightarrow> z = rtrancl(r)"
    1.43  apply (rule iffI)
    1.44 - txt{*Proving the right-to-left implication*}
    1.45 + txt\<open>Proving the right-to-left implication\<close>
    1.46   prefer 2 apply (blast intro: rtran_closure_rtrancl)
    1.47  apply (rule M_equalityI)
    1.48  apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
    1.49 @@ -140,8 +140,8 @@
    1.50       "[| M(r); M(Z) |] ==> separation (M, \<lambda>x. \<exists>w[M]. w \<in> Z & <w,x> \<in> r^+)"
    1.51  by (insert wellfounded_trancl_separation [of r Z], simp) 
    1.52  
    1.53 -text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
    1.54 -      relativized version.  Original version is on theory WF.*}
    1.55 +text\<open>Alternative proof of @{text wf_on_trancl}; inspiration for the
    1.56 +      relativized version.  Original version is on theory WF.\<close>
    1.57  lemma "[| wf[A](r);  r-``A \<subseteq> A |] ==> wf[A](r^+)"
    1.58  apply (simp add: wf_on_def wf_def)
    1.59  apply (safe intro!: equalityI)
    1.60 @@ -176,7 +176,7 @@
    1.61  done
    1.62  
    1.63  
    1.64 -text{*Absoluteness for wfrec-defined functions.*}
    1.65 +text\<open>Absoluteness for wfrec-defined functions.\<close>
    1.66  
    1.67  (*first use is_recfun, then M_is_recfun*)
    1.68  
    1.69 @@ -200,9 +200,9 @@
    1.70  done
    1.71  
    1.72  
    1.73 -text{*Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
    1.74 +text\<open>Assuming @{term r} is transitive simplifies the occurrences of @{text H}.
    1.75        The premise @{term "relation(r)"} is necessary 
    1.76 -      before we can replace @{term "r^+"} by @{term r}. *}
    1.77 +      before we can replace @{term "r^+"} by @{term r}.\<close>
    1.78  theorem (in M_trancl) trans_wfrec_relativize:
    1.79    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
    1.80       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
    1.81 @@ -230,15 +230,15 @@
    1.82         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    1.83  apply safe 
    1.84   apply (simp add: trans_wfrec_relativize [THEN iff_sym, of concl: _ x]) 
    1.85 -txt{*converse direction*}
    1.86 +txt\<open>converse direction\<close>
    1.87  apply (rule sym)
    1.88  apply (simp add: trans_wfrec_relativize, blast) 
    1.89  done
    1.90  
    1.91  
    1.92 -subsection{*M is closed under well-founded recursion*}
    1.93 +subsection\<open>M is closed under well-founded recursion\<close>
    1.94  
    1.95 -text{*Lemma with the awkward premise mentioning @{text wfrec}.*}
    1.96 +text\<open>Lemma with the awkward premise mentioning @{text wfrec}.\<close>
    1.97  lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
    1.98       "[|wf(r); M(r); 
    1.99          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.100 @@ -252,7 +252,7 @@
   1.101  apply (blast intro: lam_closed dest: pair_components_in_M) 
   1.102  done
   1.103  
   1.104 -text{*Eliminates one instance of replacement.*}
   1.105 +text\<open>Eliminates one instance of replacement.\<close>
   1.106  lemma (in M_trancl) wfrec_replacement_iff:
   1.107       "strong_replacement(M, \<lambda>x z. 
   1.108            \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) \<longleftrightarrow>
   1.109 @@ -262,7 +262,7 @@
   1.110  apply (rule strong_replacement_cong, blast) 
   1.111  done
   1.112  
   1.113 -text{*Useful version for transitive relations*}
   1.114 +text\<open>Useful version for transitive relations\<close>
   1.115  theorem (in M_trancl) trans_wfrec_closed:
   1.116       "[|wf(r); trans(r); relation(r); M(r); M(a);
   1.117         wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.118 @@ -274,7 +274,7 @@
   1.119  apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
   1.120  done
   1.121  
   1.122 -subsection{*Absoluteness without assuming transitivity*}
   1.123 +subsection\<open>Absoluteness without assuming transitivity\<close>
   1.124  lemma (in M_trancl) eq_pair_wfrec_iff:
   1.125    "[|wf(r);  M(r);  M(y); 
   1.126       strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
   1.127 @@ -287,12 +287,12 @@
   1.128              y = <x, H(x,restrict(f,r-``{x}))>)"
   1.129  apply safe  
   1.130   apply (simp add: wfrec_relativize [THEN iff_sym, of concl: _ x]) 
   1.131 -txt{*converse direction*}
   1.132 +txt\<open>converse direction\<close>
   1.133  apply (rule sym)
   1.134  apply (simp add: wfrec_relativize, blast) 
   1.135  done
   1.136  
   1.137 -text{*Full version not assuming transitivity, but maybe not very useful.*}
   1.138 +text\<open>Full version not assuming transitivity, but maybe not very useful.\<close>
   1.139  theorem (in M_trancl) wfrec_closed:
   1.140       "[|wf(r); M(r); M(a);
   1.141          wfrec_replacement(M,MH,r^+);