Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.

--- a/src/ZF/Epsilon.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Epsilon.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -66,7 +66,9 @@
    [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    |] ==> P(a) 
 *)
-lemmas eclose_induct = Transset_induct [OF _ Transset_eclose]
+lemmas eclose_induct =
+     Transset_induct [OF _ Transset_eclose, induct set: eclose]
+
 
 (*Epsilon induction*)
 lemma eps_induct:
@@ -105,6 +107,9 @@
 apply (blast intro: arg_subset_eclose [THEN subsetD])
 done
 
+(*fixed up for induct method*)
+lemmas eclose_induct_down = eclose_induct_down [consumes 1]
+
 lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
 apply (erule equalityI [OF eclose_least arg_subset_eclose])
 apply (rule subset_refl)
@@ -327,6 +332,13 @@
 apply (auto simp add: OUnion_def); 
 done
 
+lemma def_transrec2:
+     "(!!x. f(x)==transrec2(x,a,b))
+      ==> f(0) = a & 
+          f(succ(i)) = b(i, f(i)) & 
+          (Limit(K) --> f(K) = (UN j<K. f(j)))"
+by (simp add: transrec2_Limit)
+
 
 (** recursor -- better than nat_rec; the succ case has no type requirement! **)
 

--- a/src/ZF/Finite.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Finite.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -67,17 +67,22 @@
 apply simp
 done
 
+(*fixed up for induct method*)
+lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
+
+
 (** Simplification for Fin **)
 declare Fin.intros [simp]
 
+lemma Fin_0: "Fin(0) = {0}"
+by (blast intro: Fin.emptyI dest: FinD)
+
 (*The union of two finite sets is finite.*)
-lemma Fin_UnI: "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)"
+lemma Fin_UnI [simp]: "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)"
 apply (erule Fin_induct)
 apply (simp_all add: Un_cons)
 done
 
-declare Fin_UnI [simp]
-
 
 (*The union of a set of finite sets is finite.*)
 lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"

--- a/src/ZF/Main.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Main.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -9,20 +9,11 @@
   and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
   and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
 
-(* belongs to theory WF *)
-lemmas wf_induct = wf_induct [induct set: wf]
-  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
-  and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
-  and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]
-
-(* belongs to theory Nat *)
-lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
-  and complete_induct = complete_induct [case_names less, consumes 1]
-  and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1]
-  and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
 
 
-
+(*The theory of "iterates" logically belongs to Nat, but can't go there because
+  primrec isn't available into after Datatype.  The only theories defined
+  after Datatype are List and the Integ theories.*)
 subsection{* Iteration of the function @{term F} *}
 
 consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
@@ -60,15 +51,6 @@
 (* belongs to theory Cardinal *)
 declare Ord_Least [intro,simp,TC]
 
-(* belongs to theory Epsilon *)
-lemmas eclose_induct = eclose_induct [induct set: eclose]
-  and eclose_induct_down = eclose_induct_down [consumes 1]
-
-(* belongs to theory Finite *)
-lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
-
-(* belongs to theory CardinalArith *)
-lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
 
 (* belongs to theory List *)
 lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
@@ -78,16 +60,9 @@
   and negDivAlg_induct = negDivAlg_induct [consumes 2]
 
 
-(* belongs to theory Epsilon *)
+(* belongs to theory CardinalArith *)
 
-lemma def_transrec2:
-     "(!!x. f(x)==transrec2(x,a,b))
-      ==> f(0) = a & 
-          f(succ(i)) = b(i, f(i)) & 
-          (Limit(K) --> f(K) = (UN j<K. f(j)))"
-by (simp add: transrec2_Limit)
-
-(* belongs to theory CardinalArith *)
+lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
 
 lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
 apply (rule well_ord_InfCard_square_eq)  

--- a/src/ZF/Nat.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Nat.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -83,13 +83,14 @@
 (*Mathematical induction*)
 lemma nat_induct:
     "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
-apply (erule def_induct [OF nat_def nat_bnd_mono], blast)
-done
+by (erule def_induct [OF nat_def nat_bnd_mono], blast)
+
+(*fixed up for induct method*)
+lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
 
 lemma natE:
     "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
-apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
-done
+by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
 
 lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
 by (erule nat_induct, auto)
@@ -145,7 +146,12 @@
 (** Variations on mathematical induction **)
 
 (*complete induction*)
-lemmas complete_induct = Ord_induct [OF _ Ord_nat]
+
+lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
+
+lemmas complete_induct_rule =  
+	complete_induct [rule_format, case_names less, consumes 1]
+
 
 lemma nat_induct_from_lemma [rule_format]: 
     "[| n: nat;  m: nat;   
@@ -178,6 +184,9 @@
 apply (erule_tac n=j in nat_induct, auto)  
 done
 
+(*fixed up for induct method*)
+lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
+
 (** Induction principle analogous to trancl_induct **)
 
 lemma succ_lt_induct_lemma [rule_format]:
@@ -268,6 +277,7 @@
 lemma nat_nonempty [simp]: "nat ~= 0"
 by blast
 
+
 ML
 {*
 val Le_def = thm "Le_def";

--- a/src/ZF/Ordinal.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Ordinal.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -97,8 +97,17 @@
 by (unfold Transset_def, blast)
 
 lemma Transset_Inter_family: 
-    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
-by (unfold Transset_def, blast)
+    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
+by (unfold Inter_def Transset_def, blast)
+
+lemma Transset_UN:
+     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
+by (rule Transset_Union_family, auto) 
+
+lemma Transset_INT:
+     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
+by (rule Transset_Inter_family, auto) 
+
 
 (*** Natural Deduction rules for Ord ***)
 
@@ -157,18 +166,6 @@
 apply (blast intro!: Transset_Int)
 done
 
-
-lemma Ord_Inter:
-    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"
-apply (rule Transset_Inter_family [THEN OrdI], assumption)
-apply (blast intro: Ord_is_Transset) 
-apply (blast intro: Ord_contains_Transset) 
-done
-
-lemma Ord_INT:
-    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
-by (rule RepFunI [THEN Ord_Inter], assumption, blast) 
-
 (*There is no set of all ordinals, for then it would contain itself*)
 lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
 apply (rule notI)
@@ -532,8 +529,6 @@
 by (blast intro: Ord_trans)
 
 
-(*FIXME: the Intersection duals are missing!*)
-
 (*** Results about limits ***)
 
 lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"
@@ -545,6 +540,19 @@
      "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
 by (rule Ord_Union, blast)
 
+lemma Ord_Inter [intro,simp,TC]:
+    "[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" 
+apply (rule Transset_Inter_family [THEN OrdI])
+apply (blast intro: Ord_is_Transset) 
+apply (simp add: Inter_def) 
+apply (blast intro: Ord_contains_Transset) 
+done
+
+lemma Ord_INT [intro,simp,TC]:
+    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
+by (rule Ord_Inter, blast) 
+
+
 (* No < version; consider (UN i:nat.i)=nat *)
 lemma UN_least_le:
     "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"

--- a/src/ZF/Univ.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Univ.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -53,6 +53,9 @@
 apply (erule UN_mono, blast) 
 done
 
+lemma VfromI: "[| a: Vfrom(A,j);  j<i |] ==> a : Vfrom(A,i)"
+by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
+
 
 subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
 
@@ -178,20 +181,15 @@
 apply (simp add: Limit_Union_eq) 
 done
 
-lemma Limit_VfromI: "[| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)"
-apply (rule Limit_Vfrom_eq [THEN equalityD2, THEN subsetD], assumption)
-apply (blast intro: ltD) 
-done
-
 lemma Limit_VfromE:
     "[| a: Vfrom(A,i);  ~R ==> Limit(i);
         !!x. [| x<i;  a: Vfrom(A,x) |] ==> R
      |] ==> R"
 apply (rule classical)
 apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
-prefer 2 apply assumption
-apply blast 
-apply (blast intro: ltI  Limit_is_Ord)
+  prefer 2 apply assumption
+ apply blast 
+apply (blast intro: ltI Limit_is_Ord)
 done
 
 lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
@@ -199,7 +197,7 @@
 lemma singleton_in_VLimit:
     "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)"
 apply (erule Limit_VfromE, assumption)
-apply (erule singleton_in_Vfrom [THEN Limit_VfromI], assumption)
+apply (erule singleton_in_Vfrom [THEN VfromI])
 apply (blast intro: Limit_has_succ) 
 done
 
@@ -213,7 +211,7 @@
     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> {a,b} : Vfrom(A,i)"
 apply (erule Limit_VfromE, assumption)
 apply (erule Limit_VfromE, assumption)
-apply (blast intro:  Limit_VfromI [OF doubleton_in_Vfrom]
+apply (blast intro:  VfromI [OF doubleton_in_Vfrom]
                      Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
 done
 
@@ -223,8 +221,8 @@
 apply (erule Limit_VfromE, assumption)
 apply (erule Limit_VfromE, assumption)
 txt{*Infer that succ(succ(x Un xa)) < i *}
-apply (blast intro:  Limit_VfromI [OF Pair_in_Vfrom]
-                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
+apply (blast intro: VfromI [OF Pair_in_Vfrom]
+                    Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
 done
 
 lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
@@ -303,7 +301,7 @@
 lemma Union_in_VLimit:
      "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)"
 apply (rule Limit_VfromE, assumption+)
-apply (blast intro: Limit_has_succ Limit_VfromI Union_in_Vfrom)
+apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
 done
 
 
@@ -324,9 +322,8 @@
 apply (drule_tac x=a in spec) 
 apply (drule_tac x=b in spec) 
 apply (drule_tac x="x Un xa Un 2" in spec) 
-txt{*FIXME: can do better using simprule about Un and <*}
-apply (simp add: Vfrom_UnI2 [THEN Vfrom_UnI1] Vfrom_UnI1 [THEN Vfrom_UnI1]) 
-apply (blast intro: Limit_has_0 Limit_has_succ Un_least_lt Limit_VfromI)
+apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
+apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
 done
 
 subsubsection{* products *}
@@ -401,7 +398,7 @@
 
 lemma Pow_in_VLimit:
      "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)"
-by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom Limit_VfromI)
+by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
 
 
 subsection{* The set Vset(i) *}
@@ -684,7 +681,7 @@
 apply (rule Limit_nat [THEN Fin_VLimit])
 done
 
-subsubsection{* Closure under finite powers (functions from a fixed natural number) *}
+subsubsection{* Closure under finite powers: functions from a natural number *}
 
 lemma nat_fun_VLimit:
      "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
@@ -793,8 +790,6 @@
 val Vfrom_succ = thm "Vfrom_succ";
 val Vfrom_Union = thm "Vfrom_Union";
 val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
-val Limit_VfromI = thm "Limit_VfromI";
-val Limit_VfromE = thm "Limit_VfromE";
 val zero_in_VLimit = thm "zero_in_VLimit";
 val singleton_in_VLimit = thm "singleton_in_VLimit";
 val Vfrom_UnI1 = thm "Vfrom_UnI1";
@@ -814,7 +809,6 @@
 val Transset_Vfrom = thm "Transset_Vfrom";
 val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
 val Transset_Pair_subset = thm "Transset_Pair_subset";
-val Transset_Pair_subset_VLimit = thm "Transset_Pair_subset_VLimit";
 val Union_in_Vfrom = thm "Union_in_Vfrom";
 val Union_in_VLimit = thm "Union_in_VLimit";
 val in_VLimit = thm "in_VLimit";

--- a/src/ZF/WF.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/WF.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -103,6 +103,10 @@
 apply blast 
 done
 
+(*fixed up for induct method*)
+lemmas wf_induct = wf_induct [induct set: wf]
+  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
+
 (*The form of this rule is designed to match wfI*)
 lemma wf_induct2:
     "[| wf(r);  a:A;  field(r)<=A;
@@ -124,6 +128,12 @@
 apply (rule field_Int_square, blast)
 done
 
+(*fixed up for induct method*)
+lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
+   and wf_on_induct_rule = 
+	 wf_on_induct [rule_format, consumes 2, induct set: wf_on]
+
+
 (*If r allows well-founded induction then wf(r)*)
 lemma wfI:
     "[| field(r)<=A;

--- a/src/ZF/equalities.thy	Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/equalities.thy	Wed Jun 05 15:34:55 2002 +0200
@@ -794,6 +794,10 @@
      "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
 by blast
 
+lemma Collect_Union_eq [simp]:
+     "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
+by blast
+
 ML
 {*
 val ZF_cs = claset() delrules [equalityI];