src/ZF/Epsilon.thy
changeset 46820 c656222c4dc1
parent 46751 6b94c39b7366
child 46953 2b6e55924af3
     1.1 --- a/src/ZF/Epsilon.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -9,23 +9,23 @@
     1.4  
     1.5  definition
     1.6    eclose    :: "i=>i"  where
     1.7 -    "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))"
     1.8 +    "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. \<Union>(r))"
     1.9  
    1.10  definition
    1.11    transrec  :: "[i, [i,i]=>i] =>i"  where
    1.12      "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    1.13 - 
    1.14 +
    1.15  definition
    1.16    rank      :: "i=>i"  where
    1.17      "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
    1.18  
    1.19  definition
    1.20    transrec2 :: "[i, i, [i,i]=>i] =>i"  where
    1.21 -    "transrec2(k, a, b) ==                     
    1.22 -       transrec(k, 
    1.23 -                %i r. if(i=0, a, 
    1.24 -                        if(EX j. i=succ(j),        
    1.25 -                           b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    1.26 +    "transrec2(k, a, b) ==
    1.27 +       transrec(k,
    1.28 +                %i r. if(i=0, a,
    1.29 +                        if(\<exists>j. i=succ(j),
    1.30 +                           b(THE j. i=succ(j), r`(THE j. i=succ(j))),
    1.31                             \<Union>j<i. r`j)))"
    1.32  
    1.33  definition
    1.34 @@ -39,7 +39,7 @@
    1.35  
    1.36  subsection{*Basic Closure Properties*}
    1.37  
    1.38 -lemma arg_subset_eclose: "A <= eclose(A)"
    1.39 +lemma arg_subset_eclose: "A \<subseteq> eclose(A)"
    1.40  apply (unfold eclose_def)
    1.41  apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
    1.42  apply (rule nat_0I [THEN UN_upper])
    1.43 @@ -56,19 +56,19 @@
    1.44  apply (erule UnionI, assumption)
    1.45  done
    1.46  
    1.47 -(* x : eclose(A) ==> x <= eclose(A) *)
    1.48 -lemmas eclose_subset =  
    1.49 +(* @{term"x \<in> eclose(A) ==> x \<subseteq> eclose(A)"} *)
    1.50 +lemmas eclose_subset =
    1.51         Transset_eclose [unfolded Transset_def, THEN bspec]
    1.52  
    1.53 -(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    1.54 +(* @{term"[| A \<in> eclose(B); c \<in> A |] ==> c \<in> eclose(B)"} *)
    1.55  lemmas ecloseD = eclose_subset [THEN subsetD]
    1.56  
    1.57  lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
    1.58  lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
    1.59  
    1.60  (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    1.61 -   [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    1.62 -   |] ==> P(a) 
    1.63 +   [| a: eclose(A);  !!x. [| x: eclose(A); \<forall>y\<in>x. P(y) |] ==> P(x)
    1.64 +   |] ==> P(a)
    1.65  *)
    1.66  lemmas eclose_induct =
    1.67       Transset_induct [OF _ Transset_eclose, induct set: eclose]
    1.68 @@ -76,37 +76,37 @@
    1.69  
    1.70  (*Epsilon induction*)
    1.71  lemma eps_induct:
    1.72 -    "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)"
    1.73 -by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 
    1.74 +    "[| !!x. \<forall>y\<in>x. P(y) ==> P(x) |]  ==>  P(a)"
    1.75 +by (rule arg_in_eclose_sing [THEN eclose_induct], blast)
    1.76  
    1.77  
    1.78  subsection{*Leastness of @{term eclose}*}
    1.79  
    1.80  (** eclose(A) is the least transitive set including A as a subset. **)
    1.81  
    1.82 -lemma eclose_least_lemma: 
    1.83 -    "[| Transset(X);  A<=X;  n: nat |] ==> nat_rec(n, A, %m r. Union(r)) <= X"
    1.84 +lemma eclose_least_lemma:
    1.85 +    "[| Transset(X);  A<=X;  n: nat |] ==> nat_rec(n, A, %m r. \<Union>(r)) \<subseteq> X"
    1.86  apply (unfold Transset_def)
    1.87 -apply (erule nat_induct) 
    1.88 +apply (erule nat_induct)
    1.89  apply (simp add: nat_rec_0)
    1.90  apply (simp add: nat_rec_succ, blast)
    1.91  done
    1.92  
    1.93 -lemma eclose_least: 
    1.94 -     "[| Transset(X);  A<=X |] ==> eclose(A) <= X"
    1.95 +lemma eclose_least:
    1.96 +     "[| Transset(X);  A<=X |] ==> eclose(A) \<subseteq> X"
    1.97  apply (unfold eclose_def)
    1.98  apply (rule eclose_least_lemma [THEN UN_least], assumption+)
    1.99  done
   1.100  
   1.101  (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
   1.102  lemma eclose_induct_down [consumes 1]:
   1.103 -    "[| a: eclose(b);                                            
   1.104 -        !!y.   [| y: b |] ==> P(y);                              
   1.105 -        !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
   1.106 +    "[| a: eclose(b);
   1.107 +        !!y.   [| y: b |] ==> P(y);
   1.108 +        !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)
   1.109       |] ==> P(a)"
   1.110  apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
   1.111    prefer 3 apply assumption
   1.112 - apply (unfold Transset_def) 
   1.113 + apply (unfold Transset_def)
   1.114   apply (blast intro: ecloseD)
   1.115  apply (blast intro: arg_subset_eclose [THEN subsetD])
   1.116  done
   1.117 @@ -117,10 +117,10 @@
   1.118  done
   1.119  
   1.120  text{*A transitive set either is empty or contains the empty set.*}
   1.121 -lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A --> 0\<in>A";
   1.122 -apply (simp add: Transset_def) 
   1.123 -apply (rule_tac a=x in eps_induct, clarify) 
   1.124 -apply (drule bspec, assumption) 
   1.125 +lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
   1.126 +apply (simp add: Transset_def)
   1.127 +apply (rule_tac a=x in eps_induct, clarify)
   1.128 +apply (drule bspec, assumption)
   1.129  apply (case_tac "x=0", auto)
   1.130  done
   1.131  
   1.132 @@ -132,28 +132,28 @@
   1.133  
   1.134  (*Unused...*)
   1.135  lemma mem_eclose_trans: "[| A: eclose(B);  B: eclose(C) |] ==> A: eclose(C)"
   1.136 -by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 
   1.137 +by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD],
   1.138      assumption+)
   1.139  
   1.140  (*Variant of the previous lemma in a useable form for the sequel*)
   1.141  lemma mem_eclose_sing_trans:
   1.142       "[| A: eclose({B});  B: eclose({C}) |] ==> A: eclose({C})"
   1.143 -by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 
   1.144 +by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD],
   1.145      assumption+)
   1.146  
   1.147  lemma under_Memrel: "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j"
   1.148  by (unfold Transset_def, blast)
   1.149  
   1.150  lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
   1.151 -by (simp add: lt_def Ord_def under_Memrel) 
   1.152 +by (simp add: lt_def Ord_def under_Memrel)
   1.153  
   1.154 -(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   1.155 +(* @{term"j \<in> eclose(A) ==> Memrel(eclose(A)) -`` j = j"} *)
   1.156  lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
   1.157  
   1.158  lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
   1.159  
   1.160  lemma wfrec_eclose_eq:
   1.161 -    "[| k:eclose({j});  j:eclose({i}) |] ==>  
   1.162 +    "[| k:eclose({j});  j:eclose({i}) |] ==>
   1.163       wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
   1.164  apply (erule eclose_induct)
   1.165  apply (rule wfrec_ssubst)
   1.166 @@ -161,13 +161,13 @@
   1.167  apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
   1.168  done
   1.169  
   1.170 -lemma wfrec_eclose_eq2: 
   1.171 +lemma wfrec_eclose_eq2:
   1.172      "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
   1.173  apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
   1.174  apply (erule arg_into_eclose_sing)
   1.175  done
   1.176  
   1.177 -lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))"
   1.178 +lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))"
   1.179  apply (unfold transrec_def)
   1.180  apply (rule wfrec_ssubst)
   1.181  apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
   1.182 @@ -175,44 +175,44 @@
   1.183  
   1.184  (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
   1.185  lemma def_transrec:
   1.186 -    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"
   1.187 +    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, \<lambda>x\<in>a. f(x))"
   1.188  apply simp
   1.189  apply (rule transrec)
   1.190  done
   1.191  
   1.192  lemma transrec_type:
   1.193 -    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
   1.194 -     ==> transrec(a,H) : B(a)"
   1.195 +    "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) \<in> B(x) |]
   1.196 +     ==> transrec(a,H) \<in> B(a)"
   1.197  apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
   1.198  apply (subst transrec)
   1.199 -apply (simp add: lam_type) 
   1.200 +apply (simp add: lam_type)
   1.201  done
   1.202  
   1.203 -lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)"
   1.204 +lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) \<subseteq> succ(i)"
   1.205  apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
   1.206  apply (rule succI1 [THEN singleton_subsetI])
   1.207  done
   1.208  
   1.209 -lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
   1.210 -apply (insert arg_subset_eclose [of "{i}"], simp) 
   1.211 -apply (frule eclose_subset, blast) 
   1.212 +lemma succ_subset_eclose_sing: "succ(i) \<subseteq> eclose({i})"
   1.213 +apply (insert arg_subset_eclose [of "{i}"], simp)
   1.214 +apply (frule eclose_subset, blast)
   1.215  done
   1.216  
   1.217  lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
   1.218  apply (rule equalityI)
   1.219 -apply (erule eclose_sing_Ord)  
   1.220 -apply (rule succ_subset_eclose_sing) 
   1.221 +apply (erule eclose_sing_Ord)
   1.222 +apply (rule succ_subset_eclose_sing)
   1.223  done
   1.224  
   1.225  lemma Ord_transrec_type:
   1.226    assumes jini: "j: i"
   1.227        and ordi: "Ord(i)"
   1.228 -      and minor: " !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)"
   1.229 -  shows "transrec(j,H) : B(j)"
   1.230 +      and minor: " !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) \<in> B(x)"
   1.231 +  shows "transrec(j,H) \<in> B(j)"
   1.232  apply (rule transrec_type)
   1.233  apply (insert jini ordi)
   1.234  apply (blast intro!: minor
   1.235 -             intro: Ord_trans 
   1.236 +             intro: Ord_trans
   1.237               dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
   1.238  done
   1.239  
   1.240 @@ -223,7 +223,7 @@
   1.241  by (subst rank_def [THEN def_transrec], simp)
   1.242  
   1.243  lemma Ord_rank [simp]: "Ord(rank(a))"
   1.244 -apply (rule_tac a=a in eps_induct) 
   1.245 +apply (rule_tac a=a in eps_induct)
   1.246  apply (subst rank)
   1.247  apply (rule Ord_succ [THEN Ord_UN])
   1.248  apply (erule bspec, assumption)
   1.249 @@ -247,9 +247,9 @@
   1.250  apply (erule rank_lt [THEN lt_trans], assumption)
   1.251  done
   1.252  
   1.253 -lemma rank_mono: "a<=b ==> rank(a) le rank(b)"
   1.254 +lemma rank_mono: "a<=b ==> rank(a) \<le> rank(b)"
   1.255  apply (rule subset_imp_le)
   1.256 -apply (auto simp add: rank [of a] rank [of b]) 
   1.257 +apply (auto simp add: rank [of a] rank [of b])
   1.258  done
   1.259  
   1.260  lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"
   1.261 @@ -270,7 +270,7 @@
   1.262  apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
   1.263  done
   1.264  
   1.265 -lemma rank_Union: "rank(Union(A)) = (\<Union>x\<in>A. rank(x))"
   1.266 +lemma rank_Union: "rank(\<Union>(A)) = (\<Union>x\<in>A. rank(x))"
   1.267  apply (rule equalityI)
   1.268  apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
   1.269  apply (erule_tac [2] Union_upper)
   1.270 @@ -308,13 +308,13 @@
   1.271       "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
   1.272  by (simp add: the_0 the_equality2)
   1.273  
   1.274 -(*The first premise not only fixs i but ensures f~=0.
   1.275 -  The second premise is now essential.  Consider otherwise the relation 
   1.276 -  r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = Union(f``{0}) = Union(nat) = nat,
   1.277 +(*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
   1.278 +  The second premise is now essential.  Consider otherwise the relation
   1.279 +  r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = \<Union>(f``{0}) = \<Union>(nat) = nat,
   1.280    whose rank equals that of r.*)
   1.281 -lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
   1.282 -apply clarify  
   1.283 -apply (simp add: function_apply_equality) 
   1.284 +lemma rank_apply: "[|i \<in> domain(f); function(f)|] ==> rank(f`i) < rank(f)"
   1.285 +apply clarify
   1.286 +apply (simp add: function_apply_equality)
   1.287  apply (blast intro: lt_trans rank_lt rank_pair2)
   1.288  done
   1.289  
   1.290 @@ -326,7 +326,7 @@
   1.291  apply (erule arg_into_eclose [THEN eclose_subset])
   1.292  done
   1.293  
   1.294 -lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)"
   1.295 +lemma eclose_mono: "A<=B ==> eclose(A) \<subseteq> eclose(B)"
   1.296  apply (rule Transset_eclose [THEN eclose_least])
   1.297  apply (erule subset_trans)
   1.298  apply (rule arg_subset_eclose)
   1.299 @@ -340,7 +340,7 @@
   1.300  apply (rule arg_subset_eclose)
   1.301  done
   1.302  
   1.303 -(** Transfinite recursion for definitions based on the 
   1.304 +(** Transfinite recursion for definitions based on the
   1.305      three cases of ordinals **)
   1.306  
   1.307  lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
   1.308 @@ -354,14 +354,14 @@
   1.309  lemma transrec2_Limit:
   1.310       "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
   1.311  apply (rule transrec2_def [THEN def_transrec, THEN trans])
   1.312 -apply (auto simp add: OUnion_def) 
   1.313 +apply (auto simp add: OUnion_def)
   1.314  done
   1.315  
   1.316  lemma def_transrec2:
   1.317       "(!!x. f(x)==transrec2(x,a,b))
   1.318 -      ==> f(0) = a & 
   1.319 -          f(succ(i)) = b(i, f(i)) & 
   1.320 -          (Limit(K) --> f(K) = (\<Union>j<K. f(j)))"
   1.321 +      ==> f(0) = a &
   1.322 +          f(succ(i)) = b(i, f(i)) &
   1.323 +          (Limit(K) \<longrightarrow> f(K) = (\<Union>j<K. f(j)))"
   1.324  by (simp add: transrec2_Limit)
   1.325  
   1.326  
   1.327 @@ -390,10 +390,10 @@
   1.328  done
   1.329  
   1.330  lemma rec_type:
   1.331 -    "[| n: nat;   
   1.332 -        a: C(0);   
   1.333 +    "[| n: nat;
   1.334 +        a: C(0);
   1.335          !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m)) |]
   1.336 -     ==> rec(n,a,b) : C(n)"
   1.337 +     ==> rec(n,a,b) \<in> C(n)"
   1.338  by (erule nat_induct, auto)
   1.339  
   1.340  end