development and tweaks
authorpaulson
Mon Jun 24 11:59:21 2002 +0200 (2002-06-24)
changeset 13245714f7a423a15
parent 13244 7b37e218f298
child 13246 e51efc2029e9
development and tweaks
src/ZF/AC/AC15_WO6.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/AC/AC15_WO6.thy	Mon Jun 24 11:59:14 2002 +0200
     1.2 +++ b/src/ZF/AC/AC15_WO6.thy	Mon Jun 24 11:59:21 2002 +0200
     1.3 @@ -40,10 +40,9 @@
     1.4  lemma cons_times_nat_not_Finite:
     1.5       "0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
     1.6  apply clarify 
     1.7 -apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
     1.8  apply (rule nat_not_Finite [THEN notE] )
     1.9  apply (subgoal_tac "x ~= 0")
    1.10 -apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast) 
    1.11 + apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
    1.12  done
    1.13  
    1.14  lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
     2.1 --- a/src/ZF/Constructible/Formula.thy	Mon Jun 24 11:59:14 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Formula.thy	Mon Jun 24 11:59:21 2002 +0200
     2.3 @@ -22,54 +22,7 @@
     2.4  lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
     2.5  by (simp add: bool_of_o_def) 
     2.6  
     2.7 -(*????????????????Cardinal.ML*)
     2.8 -lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
     2.9 -by (blast intro: Finite_cons subset_Finite)
    2.10 -
    2.11 -lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
    2.12 -by (simp add: succ_def)
    2.13 -
    2.14 -declare Finite_0 [simp]
    2.15 -
    2.16 -lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
    2.17 -by (erule Finite_induct, simp_all)
    2.18 -
    2.19 -lemma Finite_RepFun_lemma [rule_format]:
    2.20 -     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
    2.21 -      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
    2.22 -apply (erule Finite_induct)
    2.23 - apply clarify 
    2.24 - apply (case_tac "A=0", simp)
    2.25 - apply (blast del: allE, clarify) 
    2.26 -apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
    2.27 - prefer 2 apply (blast del: allE elim: equalityE, clarify) 
    2.28 -apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
    2.29 - apply (blast intro: Diff_sing_Finite) 
    2.30 -apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
    2.31 -apply (rule equalityI) 
    2.32 - apply (blast intro: elim: equalityE) 
    2.33 -apply (blast intro: elim: equalityCE) 
    2.34 -done
    2.35 -
    2.36 -text{*I don't know why, but if the premise is expressed using meta-connectives
    2.37 -then  the simplifier cannot prove it automatically in conditional rewriting.*}
    2.38 -lemma Finite_RepFun_iff:
    2.39 -     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
    2.40 -by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f]) 
    2.41 -
    2.42 -lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
    2.43 -apply (erule Finite_induct) 
    2.44 -apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
    2.45 -done
    2.46 -
    2.47 -lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
    2.48 -apply (subgoal_tac "Finite({{x} . x \<in> A})")
    2.49 - apply (simp add: Finite_RepFun_iff ) 
    2.50 -apply (blast intro: subset_Finite) 
    2.51 -done
    2.52 -
    2.53 -lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
    2.54 -by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
    2.55 +(*????????????????CardinalArith *)
    2.56  
    2.57  lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
    2.58  apply (erule nat_induct)
    2.59 @@ -922,6 +875,10 @@
    2.60  apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
    2.61  done
    2.62  
    2.63 +
    2.64 +lemma Ord_in_L: "Ord(i) ==> L(i)"
    2.65 +by (blast intro: Ord_in_Lset L_I)
    2.66 +
    2.67  text{*This is lrank(lrank(a)) = lrank(a) *}
    2.68  declare Ord_lrank [THEN lrank_of_Ord, simp]
    2.69  
    2.70 @@ -963,13 +920,13 @@
    2.71  
    2.72  subsection{*For L to satisfy the ZF axioms*}
    2.73  
    2.74 -lemma Union_in_L: "L(X) ==> L(Union(X))"
    2.75 +theorem Union_in_L: "L(X) ==> L(Union(X))"
    2.76  apply (simp add: L_def, clarify) 
    2.77  apply (drule Ord_imp_greater_Limit) 
    2.78  apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
    2.79  done
    2.80  
    2.81 -lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
    2.82 +theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
    2.83  apply (simp add: L_def, clarify) 
    2.84  apply (drule Ord2_imp_greater_Limit, assumption) 
    2.85  apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
    2.86 @@ -1000,7 +957,7 @@
    2.87  apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
    2.88  done
    2.89  
    2.90 -lemma LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
    2.91 +theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
    2.92  by (blast intro: L_I dest: L_D LPow_in_Lset)
    2.93  
    2.94  end
     3.1 --- a/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:14 2002 +0200
     3.2 +++ b/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:21 2002 +0200
     3.3 @@ -1,4 +1,11 @@
     3.4 +(*  Title:      ZF/Constructible/ROOT.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   2002  University of Cambridge
     3.8 +
     3.9 +Inner Models and Absoluteness
    3.10 +*)
    3.11 +
    3.12  use_thy "Reflection";
    3.13  use_thy "WFrec";
    3.14 -use_thy "WF_extras";
    3.15  use_thy "L_axioms";
     4.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jun 24 11:59:14 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Jun 24 11:59:21 2002 +0200
     4.3 @@ -18,15 +18,15 @@
     4.4      "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
     4.5                            (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
     4.6  
     4.7 +  union :: "[i=>o,i,i,i] => o"
     4.8 +    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
     4.9 +
    4.10    successor :: "[i=>o,i,i] => o"
    4.11      "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
    4.12  
    4.13    powerset :: "[i=>o,i,i] => o"
    4.14      "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
    4.15  
    4.16 -  union :: "[i=>o,i,i,i] => o"
    4.17 -    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
    4.18 -
    4.19    inter :: "[i=>o,i,i,i] => o"
    4.20      "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
    4.21  
    4.22 @@ -72,6 +72,11 @@
    4.23      "is_range(M,r,z) == 
    4.24  	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
    4.25  
    4.26 +  is_field :: "[i=>o,i,i] => o"
    4.27 +    "is_field(M,r,z) == 
    4.28 +	\<exists>dr. M(dr) & is_domain(M,r,dr) & 
    4.29 +            (\<exists>rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))"
    4.30 +
    4.31    is_relation :: "[i=>o,i] => o"
    4.32      "is_relation(M,r) == 
    4.33          (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
    4.34 @@ -91,6 +96,13 @@
    4.35          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    4.36          (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    4.37  
    4.38 +  composition :: "[i=>o,i,i,i] => o"
    4.39 +    "composition(M,r,s,t) == 
    4.40 +        \<forall>p. M(p) --> (p \<in> t <-> 
    4.41 +                      (\<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
    4.42 +                           p = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))))"
    4.43 +
    4.44 +
    4.45    injection :: "[i=>o,i,i,i] => o"
    4.46      "injection(M,A,B,f) == 
    4.47  	typed_function(M,A,B,f) &
    4.48 @@ -373,6 +385,7 @@
    4.49        and Union_ax:	    "Union_ax(M)"
    4.50        and power_ax:         "power_ax(M)"
    4.51        and replacement:      "replacement(M,P)"
    4.52 +      and M_nat:            "M(nat)"   (*i.e. the axiom of infinity*)
    4.53    and Inter_separation:
    4.54       "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
    4.55    and cartprod_separation:
    4.56 @@ -398,7 +411,7 @@
    4.57    and pred_separation:
    4.58       "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
    4.59    and Memrel_separation:
    4.60 -     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
    4.61 +     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) & x \<in> y)"
    4.62    and obase_separation:
    4.63       --{*part of the order type formalization*}
    4.64       "[| M(A); M(r) |] 
    4.65 @@ -407,8 +420,8 @@
    4.66  	     order_isomorphism(M,par,r,x,mx,g))"
    4.67    and well_ord_iso_separation:
    4.68       "[| M(A); M(f); M(r) |] 
    4.69 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and> 
    4.70 -		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
    4.71 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) & 
    4.72 +		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
    4.73    and obase_equals_separation:
    4.74       "[| M(A); M(r) |] 
    4.75        ==> separation
    4.76 @@ -419,7 +432,7 @@
    4.77    and is_recfun_separation:
    4.78       --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
    4.79       "[| M(A); M(f); M(g); M(a); M(b) |] 
    4.80 -     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
    4.81 +     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & f`x \<noteq> g`x)"
    4.82    and omap_replacement:
    4.83       "[| M(A); M(r) |] 
    4.84        ==> strong_replacement(M,
    4.85 @@ -440,6 +453,12 @@
    4.86                 (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
    4.87  by (blast intro: transM)
    4.88  
    4.89 +text{*Simplifies proofs of equalities when there's an iff-equality
    4.90 +      available for rewriting, universally quantified over M. *}
    4.91 +lemma (in M_axioms) M_equalityI: 
    4.92 +     "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
    4.93 +by (blast intro!: equalityI dest: transM) 
    4.94 +
    4.95  lemma (in M_axioms) empty_abs [simp]: 
    4.96       "M(z) ==> empty(M,z) <-> z=0"
    4.97  apply (simp add: empty_def)
    4.98 @@ -516,15 +535,15 @@
    4.99  apply (blast intro!: equalityI dest: transM) 
   4.100  done
   4.101  
   4.102 -lemma (in M_axioms) Union_closed [intro]:
   4.103 +lemma (in M_axioms) Union_closed [intro,simp]:
   4.104       "M(A) ==> M(Union(A))"
   4.105  by (insert Union_ax, simp add: Union_ax_def) 
   4.106  
   4.107 -lemma (in M_axioms) Un_closed [intro]:
   4.108 +lemma (in M_axioms) Un_closed [intro,simp]:
   4.109       "[| M(A); M(B) |] ==> M(A Un B)"
   4.110  by (simp only: Un_eq_Union, blast) 
   4.111  
   4.112 -lemma (in M_axioms) cons_closed [intro]:
   4.113 +lemma (in M_axioms) cons_closed [intro,simp]:
   4.114       "[| M(a); M(A) |] ==> M(cons(a,A))"
   4.115  by (subst cons_eq [symmetric], blast) 
   4.116  
   4.117 @@ -538,7 +557,7 @@
   4.118  apply (blast intro: transM) 
   4.119  done
   4.120  
   4.121 -lemma (in M_axioms) separation_closed [intro]:
   4.122 +lemma (in M_axioms) separation_closed [intro,simp]:
   4.123       "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   4.124  apply (insert separation, simp add: separation_def) 
   4.125  apply (drule spec [THEN mp], assumption, clarify) 
   4.126 @@ -565,7 +584,7 @@
   4.127  
   4.128  
   4.129  (*The last premise expresses that P takes M to M*)
   4.130 -lemma (in M_axioms) strong_replacement_closed [intro]:
   4.131 +lemma (in M_axioms) strong_replacement_closed [intro,simp]:
   4.132       "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   4.133         !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   4.134  apply (simp add: strong_replacement_def) 
   4.135 @@ -589,7 +608,7 @@
   4.136    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   4.137    even for f : M -> M.
   4.138  *)
   4.139 -lemma (in M_axioms) RepFun_closed [intro]:
   4.140 +lemma (in M_axioms) RepFun_closed [intro,simp]:
   4.141       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
   4.142        ==> M(RepFun(A,f))"
   4.143  apply (simp add: RepFun_def) 
   4.144 @@ -669,20 +688,20 @@
   4.145  prefer 6 apply (rule refl) 
   4.146  prefer 4 apply assumption
   4.147  prefer 4 apply assumption
   4.148 -apply (insert cartprod_separation [of A B], simp, blast+)
   4.149 +apply (insert cartprod_separation [of A B], auto)
   4.150  done
   4.151  
   4.152  
   4.153  text{*All the lemmas above are necessary because Powerset is not absolute.
   4.154        I should have used Replacement instead!*}
   4.155 -lemma (in M_axioms) cartprod_closed [intro]: 
   4.156 +lemma (in M_axioms) cartprod_closed [intro,simp]: 
   4.157       "[| M(A); M(B) |] ==> M(A*B)"
   4.158  by (frule cartprod_closed_lemma, assumption, force)
   4.159  
   4.160 -lemma (in M_axioms) image_closed [intro]: 
   4.161 +lemma (in M_axioms) image_closed [intro,simp]: 
   4.162       "[| M(A); M(r) |] ==> M(r``A)"
   4.163  apply (simp add: image_iff_Collect)
   4.164 -apply (insert image_separation [of A r], simp, blast) 
   4.165 +apply (insert image_separation [of A r], simp) 
   4.166  done
   4.167  
   4.168  lemma (in M_axioms) vimage_abs [simp]: 
   4.169 @@ -692,10 +711,10 @@
   4.170   apply (blast intro!: equalityI dest: transM, blast) 
   4.171  done
   4.172  
   4.173 -lemma (in M_axioms) vimage_closed [intro]: 
   4.174 +lemma (in M_axioms) vimage_closed [intro,simp]: 
   4.175       "[| M(A); M(r) |] ==> M(r-``A)"
   4.176  apply (simp add: vimage_iff_Collect)
   4.177 -apply (insert vimage_separation [of A r], simp, blast) 
   4.178 +apply (insert vimage_separation [of A r], simp) 
   4.179  done
   4.180  
   4.181  lemma (in M_axioms) domain_abs [simp]: 
   4.182 @@ -704,10 +723,9 @@
   4.183  apply (blast intro!: equalityI dest: transM) 
   4.184  done
   4.185  
   4.186 -lemma (in M_axioms) domain_closed [intro]: 
   4.187 +lemma (in M_axioms) domain_closed [intro,simp]: 
   4.188       "M(r) ==> M(domain(r))"
   4.189  apply (simp add: domain_eq_vimage)
   4.190 -apply (blast intro: vimage_closed) 
   4.191  done
   4.192  
   4.193  lemma (in M_axioms) range_abs [simp]: 
   4.194 @@ -716,24 +734,31 @@
   4.195  apply (blast intro!: equalityI dest: transM)
   4.196  done
   4.197  
   4.198 -lemma (in M_axioms) range_closed [intro]: 
   4.199 +lemma (in M_axioms) range_closed [intro,simp]: 
   4.200       "M(r) ==> M(range(r))"
   4.201  apply (simp add: range_eq_image)
   4.202 -apply (blast intro: image_closed) 
   4.203  done
   4.204  
   4.205 +lemma (in M_axioms) field_abs [simp]: 
   4.206 +     "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   4.207 +by (simp add: domain_closed range_closed is_field_def field_def)
   4.208 +
   4.209 +lemma (in M_axioms) field_closed [intro,simp]: 
   4.210 +     "M(r) ==> M(field(r))"
   4.211 +by (simp add: domain_closed range_closed Un_closed field_def) 
   4.212 +
   4.213 +
   4.214  lemma (in M_axioms) M_converse_iff:
   4.215       "M(r) ==> 
   4.216        converse(r) = 
   4.217        {z \<in> range(r) * domain(r). 
   4.218 -        \<exists>p\<in>r. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"
   4.219 +        \<exists>p\<in>r. \<exists>x. M(x) & (\<exists>y. M(y) & p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>)}"
   4.220  by (blast dest: transM)
   4.221  
   4.222 -lemma (in M_axioms) converse_closed [intro]: 
   4.223 +lemma (in M_axioms) converse_closed [intro,simp]: 
   4.224       "M(r) ==> M(converse(r))"
   4.225  apply (simp add: M_converse_iff)
   4.226 -apply (insert converse_separation [of r], simp) 
   4.227 -apply (blast intro: image_closed) 
   4.228 +apply (insert converse_separation [of r], simp)
   4.229  done
   4.230  
   4.231  lemma (in M_axioms) relation_abs [simp]: 
   4.232 @@ -749,10 +774,9 @@
   4.233    apply (blast dest: pair_components_in_M)+
   4.234  done
   4.235  
   4.236 -lemma (in M_axioms) apply_closed [intro]: 
   4.237 +lemma (in M_axioms) apply_closed [intro,simp]: 
   4.238       "[|M(f); M(a)|] ==> M(f`a)"
   4.239 -apply (simp add: apply_def) 
   4.240 -apply (blast intro: elim:); 
   4.241 +apply (simp add: apply_def)
   4.242  done
   4.243  
   4.244  lemma (in M_axioms) apply_abs: 
   4.245 @@ -808,19 +832,18 @@
   4.246       "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
   4.247  by (simp add: restrict_def, blast dest: transM)
   4.248  
   4.249 -lemma (in M_axioms) restrict_closed [intro]: 
   4.250 +lemma (in M_axioms) restrict_closed [intro,simp]: 
   4.251       "[| M(A); M(r) |] ==> M(restrict(r,A))"
   4.252  apply (simp add: M_restrict_iff)
   4.253 -apply (insert restrict_separation [of A], simp, blast) 
   4.254 +apply (insert restrict_separation [of A], simp) 
   4.255  done
   4.256  
   4.257 -
   4.258  lemma (in M_axioms) M_comp_iff:
   4.259       "[| M(r); M(s) |] 
   4.260        ==> r O s = 
   4.261            {xz \<in> domain(s) * range(r).  
   4.262 -            \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and> 
   4.263 -                xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
   4.264 +            \<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
   4.265 +                xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"
   4.266  apply (simp add: comp_def)
   4.267  apply (rule equalityI) 
   4.268   apply (clarify ); 
   4.269 @@ -828,10 +851,24 @@
   4.270   apply  (blast dest:  transM)+
   4.271  done
   4.272  
   4.273 -lemma (in M_axioms) comp_closed [intro]: 
   4.274 +lemma (in M_axioms) comp_closed [intro,simp]: 
   4.275       "[| M(r); M(s) |] ==> M(r O s)"
   4.276  apply (simp add: M_comp_iff)
   4.277 -apply (insert comp_separation [of r s], simp, blast) 
   4.278 +apply (insert comp_separation [of r s], simp) 
   4.279 +done
   4.280 +
   4.281 +lemma (in M_axioms) composition_abs [simp]: 
   4.282 +     "[| M(r); M(s); M(t) |] 
   4.283 +      ==> composition(M,r,s,t) <-> t = r O s"
   4.284 +apply safe;
   4.285 + txt{*Proving @{term "composition(M, r, s, r O s)"}*}
   4.286 + prefer 2 
   4.287 + apply (simp add: composition_def comp_def)
   4.288 + apply (blast dest: transM) 
   4.289 +txt{*Opposite implication*}
   4.290 +apply (rule M_equalityI)
   4.291 +  apply (simp add: composition_def comp_def)
   4.292 +  apply (blast del: allE dest: transM)+
   4.293  done
   4.294  
   4.295  lemma (in M_axioms) nat_into_M [intro]:
   4.296 @@ -852,16 +889,34 @@
   4.297  apply (blast intro!: equalityI dest: transM) 
   4.298  done
   4.299  
   4.300 -lemma (in M_axioms) Inter_closed [intro]:
   4.301 +lemma (in M_axioms) Inter_closed [intro,simp]:
   4.302       "M(A) ==> M(Inter(A))"
   4.303 -by (insert Inter_separation, simp add: Inter_def, blast)
   4.304 +by (insert Inter_separation, simp add: Inter_def)
   4.305  
   4.306 -lemma (in M_axioms) Int_closed [intro]:
   4.307 +lemma (in M_axioms) Int_closed [intro,simp]:
   4.308       "[| M(A); M(B) |] ==> M(A Int B)"
   4.309  apply (subgoal_tac "M({A,B})")
   4.310  apply (frule Inter_closed, force+); 
   4.311  done
   4.312  
   4.313 +text{*M contains all finite functions*}
   4.314 +lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
   4.315 +     "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
   4.316 +apply (induct_tac n, simp)
   4.317 +apply (rule ballI)  
   4.318 +apply (simp add: succ_def) 
   4.319 +apply (frule fun_cons_restrict_eq)
   4.320 +apply (erule ssubst) 
   4.321 +apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
   4.322 + apply (simp add: cons_closed nat_into_M apply_closed) 
   4.323 +apply (blast intro: apply_funtype transM restrict_type2) 
   4.324 +done
   4.325 +
   4.326 +lemma (in M_axioms) finite_fun_closed [rule_format]: 
   4.327 +     "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
   4.328 +by (blast intro: finite_fun_closed_lemma) 
   4.329 +
   4.330 +
   4.331  subsection{*Absoluteness for ordinals*}
   4.332  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   4.333  
     5.1 --- a/src/ZF/Constructible/WFrec.thy	Mon Jun 24 11:59:14 2002 +0200
     5.2 +++ b/src/ZF/Constructible/WFrec.thy	Mon Jun 24 11:59:21 2002 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  theory WFrec = Wellorderings:
     5.5  
     5.6  
     5.7 -(*WF.thy??*)
     5.8 +(*FIXME: could move these to WF.thy*)
     5.9  
    5.10  lemma is_recfunI:
    5.11       "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
    5.12 @@ -27,6 +27,16 @@
    5.13   apply (fast intro: lam_type, simp) 
    5.14  done
    5.15  
    5.16 +lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
    5.17 +by (blast dest:  is_recfun_type fun_is_rel)
    5.18 +
    5.19 +lemma apply_recfun2:
    5.20 +    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
    5.21 +apply (frule apply_recfun) 
    5.22 + apply (blast dest: is_recfun_type fun_is_rel) 
    5.23 +apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
    5.24 +done
    5.25 +
    5.26  lemma trans_on_Int_eq [simp]:
    5.27        "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
    5.28         ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
    5.29 @@ -38,11 +48,6 @@
    5.30  by (blast intro: trans_onD) 
    5.31  
    5.32  
    5.33 -constdefs
    5.34 -   M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
    5.35 -     "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
    5.36 -
    5.37 -
    5.38  text{*Stated using @{term "trans[A](r)"} rather than
    5.39        @{term "transitive_rel(M,A,r)"} because the latter rewrites to
    5.40        the former anyway, by @{text transitive_rel_abs}.
    5.41 @@ -178,6 +183,16 @@
    5.42                   apply_recfun is_recfun_type [THEN apply_iff]) 
    5.43  done
    5.44  
    5.45 +(*FIXME: use this lemma just below*)
    5.46 +text{*For typical applications of Replacement for recursive definitions*}
    5.47 +lemma (in M_axioms) univalent_is_recfun:
    5.48 +     "[|wellfounded_on(M,A,r); trans[A](r); r \<subseteq> A*A; M(r); M(A)|]
    5.49 +      ==> univalent (M, A, \<lambda>x p. \<exists>y. M(y) &
    5.50 +                    (\<exists>f. M(f) & p = \<langle>x, y\<rangle> & is_recfun(r,x,H,f) & y = H(x,f)))"
    5.51 +apply (simp add: univalent_def) 
    5.52 +apply (blast dest: is_recfun_functional) 
    5.53 +done
    5.54 +
    5.55  text{*Proof of the inductive step for @{text exists_is_recfun}, since
    5.56        we must prove two versions.*}
    5.57  lemma (in M_axioms) exists_is_recfun_indstep:
    5.58 @@ -240,23 +255,28 @@
    5.59                     pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    5.60         M(A);  M(r);  r \<subseteq> A*A;  
    5.61         \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
    5.62 -      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
    5.63 +      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"        
    5.64  apply (rule wf_on_induct2, assumption+)
    5.65  apply (frule wf_on_imp_relativized)  
    5.66  apply (rule exists_is_recfun_indstep, assumption+)
    5.67  done
    5.68  
    5.69 -(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
    5.70 -lemma (in M_axioms) M_is_the_recfun: 
    5.71 -    "[|is_recfun(r,a,H,f);  
    5.72 -       wellfounded_on(M,A,r); trans[A](r); 
    5.73 -       M(A); M(f); M(a); r \<subseteq> A*A |]   
    5.74 -     ==> M(M_the_recfun(M,r,a,H)) & 
    5.75 -         is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
    5.76 -apply (unfold M_the_recfun_def)
    5.77 -apply (rule ex1I [THEN theI2], fast)
    5.78 -apply (blast intro: is_recfun_functional, blast) 
    5.79 -done
    5.80 +    (*????????????????NOT USED????????????????*)
    5.81 +    constdefs
    5.82 +      M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
    5.83 +      "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
    5.84 +    
    5.85 +    (*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
    5.86 +    lemma (in M_axioms) M_is_the_recfun: 
    5.87 +      "[|is_recfun(r,a,H,f);  
    5.88 +      wellfounded_on(M,A,r); trans[A](r); 
    5.89 +      M(A); M(f); M(a); r \<subseteq> A*A |]   
    5.90 +      ==> M(M_the_recfun(M,r,a,H)) & 
    5.91 +      is_recfun(r, a, H, M_the_recfun(M,r,a,H))"    
    5.92 +    apply (unfold M_the_recfun_def)
    5.93 +    apply (rule ex1I [THEN theI2], fast)
    5.94 +    apply (blast intro: is_recfun_functional, blast) 
    5.95 +    done
    5.96  
    5.97  constdefs
    5.98     M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
    5.99 @@ -432,7 +452,7 @@
   5.100  apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
   5.101  done
   5.102  
   5.103 -lemma (in M_recursion) oadd_closed [intro]:
   5.104 +lemma (in M_recursion) oadd_closed [intro,simp]:
   5.105      "[| M(i); M(j) |] ==> M(i++j)"
   5.106  apply (simp add: oadd_eq_if_raw_oadd, clarify) 
   5.107  apply (simp add: raw_oadd_eq_oadd) 
   5.108 @@ -485,7 +505,6 @@
   5.109    apply (simp add: omult_eqns_0)
   5.110   apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
   5.111  apply (simp add: omult_eqns_Limit) 
   5.112 -apply (simp add: Union_closed image_closed) 
   5.113  done
   5.114  
   5.115  lemma (in M_recursion) exists_omult:
     6.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:14 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Mon Jun 24 11:59:21 2002 +0200
     6.3 @@ -144,10 +144,10 @@
     6.4  apply (blast dest: transM) 
     6.5  done
     6.6  
     6.7 -lemma (in M_axioms) pred_closed [intro]: 
     6.8 +lemma (in M_axioms) pred_closed [intro,simp]: 
     6.9       "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
    6.10  apply (simp add: Order.pred_def) 
    6.11 -apply (insert pred_separation [of r x], simp, blast) 
    6.12 +apply (insert pred_separation [of r x], simp) 
    6.13  done
    6.14  
    6.15  lemma (in M_axioms) membership_abs [simp]: 
    6.16 @@ -170,10 +170,10 @@
    6.17  apply (blast dest: transM)
    6.18  done 
    6.19  
    6.20 -lemma (in M_axioms) Memrel_closed [intro]: 
    6.21 +lemma (in M_axioms) Memrel_closed [intro,simp]: 
    6.22       "M(A) ==> M(Memrel(A))"
    6.23  apply (simp add: M_Memrel_iff) 
    6.24 -apply (insert Memrel_separation, simp, blast)
    6.25 +apply (insert Memrel_separation, simp)
    6.26  done
    6.27  
    6.28