src/ZF/Constructible/WF_absolute.thy
changeset 46823 57bf0cecb366
parent 32960 69916a850301
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Mar 06 16:46:27 2012 +0000
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Mar 06 17:01:37 2012 +0000
     1.3 @@ -18,7 +18,7 @@
     1.4  lemma alt_rtrancl_lemma1 [rule_format]:
     1.5      "n \<in> nat
     1.6       ==> \<forall>f \<in> succ(n) -> field(r).
     1.7 -         (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
     1.8 +         (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) \<longrightarrow> \<langle>f`0, f`n\<rangle> \<in> r^*"
     1.9  apply (induct_tac n)
    1.10  apply (simp_all add: apply_funtype rtrancl_refl, clarify)
    1.11  apply (rename_tac n f)
    1.12 @@ -29,24 +29,24 @@
    1.13  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
    1.14  done
    1.15  
    1.16 -lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    1.17 +lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) \<subseteq> r^*"
    1.18  apply (simp add: rtrancl_alt_def)
    1.19  apply (blast intro: alt_rtrancl_lemma1)
    1.20  done
    1.21  
    1.22 -lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    1.23 +lemma rtrancl_subset_rtrancl_alt: "r^* \<subseteq> rtrancl_alt(field(r),r)"
    1.24  apply (simp add: rtrancl_alt_def, clarify)
    1.25  apply (frule rtrancl_type [THEN subsetD], clarify, simp)
    1.26  apply (erule rtrancl_induct)
    1.27   txt{*Base case, trivial*}
    1.28   apply (rule_tac x=0 in bexI)
    1.29 -  apply (rule_tac x="lam x:1. xa" in bexI)
    1.30 +  apply (rule_tac x="\<lambda>x\<in>1. xa" in bexI)
    1.31     apply simp_all
    1.32  txt{*Inductive step*}
    1.33  apply clarify
    1.34  apply (rename_tac n f)
    1.35  apply (rule_tac x="succ(n)" in bexI)
    1.36 - apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    1.37 + apply (rule_tac x="\<lambda>i\<in>succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    1.38    apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
    1.39    apply (blast intro: mem_asym)
    1.40   apply typecheck
    1.41 @@ -67,7 +67,7 @@
    1.42                 (\<exists>f[M]. typed_function(M,n',A,f) &
    1.43                  (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
    1.44                    fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
    1.45 -                  (\<forall>j[M]. j\<in>n --> 
    1.46 +                  (\<forall>j[M]. j\<in>n \<longrightarrow> 
    1.47                      (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
    1.48                        fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.49                        fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
    1.50 @@ -75,8 +75,8 @@
    1.51  definition
    1.52    rtran_closure :: "[i=>o,i,i] => o" where
    1.53      "rtran_closure(M,r,s) == 
    1.54 -        \<forall>A[M]. is_field(M,r,A) -->
    1.55 -         (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"
    1.56 +        \<forall>A[M]. is_field(M,r,A) \<longrightarrow>
    1.57 +         (\<forall>p[M]. p \<in> s \<longleftrightarrow> rtran_closure_mem(M,A,r,p))"
    1.58  
    1.59  definition
    1.60    tran_closure :: "[i=>o,i,i] => o" where
    1.61 @@ -85,7 +85,7 @@
    1.62  
    1.63  lemma (in M_basic) rtran_closure_mem_iff:
    1.64       "[|M(A); M(r); M(p)|]
    1.65 -      ==> rtran_closure_mem(M,A,r,p) <->
    1.66 +      ==> rtran_closure_mem(M,A,r,p) \<longleftrightarrow>
    1.67            (\<exists>n[M]. n\<in>nat & 
    1.68             (\<exists>f[M]. f \<in> succ(n) -> A &
    1.69              (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
    1.70 @@ -118,7 +118,7 @@
    1.71  done
    1.72  
    1.73  lemma (in M_trancl) rtrancl_abs [simp]:
    1.74 -     "[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)"
    1.75 +     "[| M(r); M(z) |] ==> rtran_closure(M,r,z) \<longleftrightarrow> z = rtrancl(r)"
    1.76  apply (rule iffI)
    1.77   txt{*Proving the right-to-left implication*}
    1.78   prefer 2 apply (blast intro: rtran_closure_rtrancl)
    1.79 @@ -133,7 +133,7 @@
    1.80  by (simp add: trancl_def comp_closed rtrancl_closed)
    1.81  
    1.82  lemma (in M_trancl) trancl_abs [simp]:
    1.83 -     "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)"
    1.84 +     "[| M(r); M(z) |] ==> tran_closure(M,r,z) \<longleftrightarrow> z = trancl(r)"
    1.85  by (simp add: tran_closure_def trancl_def)
    1.86  
    1.87  lemma (in M_trancl) wellfounded_trancl_separation':
    1.88 @@ -142,7 +142,7 @@
    1.89  
    1.90  text{*Alternative proof of @{text wf_on_trancl}; inspiration for the
    1.91        relativized version.  Original version is on theory WF.*}
    1.92 -lemma "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
    1.93 +lemma "[| wf[A](r);  r-``A \<subseteq> A |] ==> wf[A](r^+)"
    1.94  apply (simp add: wf_on_def wf_def)
    1.95  apply (safe intro!: equalityI)
    1.96  apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
    1.97 @@ -150,7 +150,7 @@
    1.98  done
    1.99  
   1.100  lemma (in M_trancl) wellfounded_on_trancl:
   1.101 -     "[| wellfounded_on(M,A,r);  r-``A <= A; M(r); M(A) |]
   1.102 +     "[| wellfounded_on(M,A,r);  r-``A \<subseteq> A; M(r); M(A) |]
   1.103        ==> wellfounded_on(M,A,r^+)"
   1.104  apply (simp add: wellfounded_on_def)
   1.105  apply (safe intro!: equalityI)
   1.106 @@ -186,8 +186,8 @@
   1.107            pair(M,x,y,z) & 
   1.108            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.109            y = H(x, restrict(g, r -`` {x}))); 
   1.110 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.111 -   ==> wfrec(r,a,H) = z <-> 
   1.112 +     \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))|] 
   1.113 +   ==> wfrec(r,a,H) = z \<longleftrightarrow> 
   1.114         (\<exists>f[M]. is_recfun(r^+, a, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.115              z = H(a,restrict(f,r-``{a})))"
   1.116  apply (frule wf_trancl) 
   1.117 @@ -206,8 +206,8 @@
   1.118  theorem (in M_trancl) trans_wfrec_relativize:
   1.119    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
   1.120       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.121 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.122 -   ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
   1.123 +     \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))|] 
   1.124 +   ==> wfrec(r,a,H) = z \<longleftrightarrow> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
   1.125  apply (frule wfrec_replacement', assumption+) 
   1.126  apply (simp cong: is_recfun_cong
   1.127             add: wfrec_relativize trancl_eq_r
   1.128 @@ -217,16 +217,16 @@
   1.129  theorem (in M_trancl) trans_wfrec_abs:
   1.130    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
   1.131       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.132 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.133 -   ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" 
   1.134 +     \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))|] 
   1.135 +   ==> is_wfrec(M,MH,r,a,z) \<longleftrightarrow> z=wfrec(r,a,H)" 
   1.136  by (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
   1.137  
   1.138  
   1.139  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
   1.140    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
   1.141       wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.142 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.143 -   ==> y = <x, wfrec(r, x, H)> <-> 
   1.144 +     \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))|] 
   1.145 +   ==> y = <x, wfrec(r, x, H)> \<longleftrightarrow> 
   1.146         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.147  apply safe 
   1.148   apply (simp add: trans_wfrec_relativize [THEN iff_sym, of concl: _ x]) 
   1.149 @@ -242,8 +242,8 @@
   1.150  lemma (in M_trancl) wfrec_closed_lemma [rule_format]:
   1.151       "[|wf(r); M(r); 
   1.152          strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
   1.153 -        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.154 -      ==> M(a) --> M(wfrec(r,a,H))"
   1.155 +        \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |] 
   1.156 +      ==> M(a) \<longrightarrow> M(wfrec(r,a,H))"
   1.157  apply (rule_tac a=a in wf_induct, assumption+)
   1.158  apply (subst wfrec, assumption, clarify)
   1.159  apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
   1.160 @@ -255,7 +255,7 @@
   1.161  text{*Eliminates one instance of replacement.*}
   1.162  lemma (in M_trancl) wfrec_replacement_iff:
   1.163       "strong_replacement(M, \<lambda>x z. 
   1.164 -          \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <->
   1.165 +          \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) \<longleftrightarrow>
   1.166        strong_replacement(M, 
   1.167             \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
   1.168  apply simp 
   1.169 @@ -266,7 +266,7 @@
   1.170  theorem (in M_trancl) trans_wfrec_closed:
   1.171       "[|wf(r); trans(r); relation(r); M(r); M(a);
   1.172         wfrec_replacement(M,MH,r);  relation2(M,MH,H);
   1.173 -        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.174 +        \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |] 
   1.175        ==> M(wfrec(r,a,H))"
   1.176  apply (frule wfrec_replacement', assumption+) 
   1.177  apply (frule wfrec_replacement_iff [THEN iffD1]) 
   1.178 @@ -281,8 +281,8 @@
   1.179            pair(M,x,y,z) & 
   1.180            is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
   1.181            y = H(x, restrict(g, r -`` {x}))); 
   1.182 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.183 -   ==> y = <x, wfrec(r, x, H)> <-> 
   1.184 +     \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g))|] 
   1.185 +   ==> y = <x, wfrec(r, x, H)> \<longleftrightarrow> 
   1.186         (\<exists>f[M]. is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), f) & 
   1.187              y = <x, H(x,restrict(f,r-``{x}))>)"
   1.188  apply safe  
   1.189 @@ -297,7 +297,7 @@
   1.190       "[|wf(r); M(r); M(a);
   1.191          wfrec_replacement(M,MH,r^+);  
   1.192          relation2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
   1.193 -        \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.194 +        \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |] 
   1.195        ==> M(wfrec(r,a,H))"
   1.196  apply (frule wfrec_replacement' 
   1.197                 [of MH "r^+" "\<lambda>x f. H(x, restrict(f, r -`` {x}))"])