# HG changeset patch
# User paulson
# Date 1025609288 -7200
# Node ID 3ba9be497c33996da88d17c97a092ab1bd96ae82
# Parent  240509babf00d8b2aa32179a8d3256d770f8f104
Tidying and introduction of various new theorems

diff -r 240509babf00 -r 3ba9be497c33 src/ZF/AC.thy
--- a/src/ZF/AC.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/AC.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -23,27 +23,22 @@
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
 lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
 apply (rule AC_Pi)
-apply (erule bspec)
-apply assumption
+apply (erule bspec, assumption)
 done
 
 lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-apply (erule_tac [2] exI)
-apply blast
+apply (erule_tac [2] exI, blast)
 done
 
 lemma AC_func:
      "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-prefer 2 apply (blast dest: apply_type intro: Pi_type)
-apply (blast intro: elim:); 
+prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) 
 done
 
 lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
-apply (subgoal_tac "x \<noteq> 0")
-apply blast+
-done
+by (subgoal_tac "x \<noteq> 0", blast+)
 
 lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
 apply (rule AC_func)
@@ -53,9 +48,8 @@
 lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
 apply (rule AC_func0 [THEN bexE])
 apply (rule_tac [2] bexI)
-prefer 2 apply (assumption)
-apply (erule_tac [2] fun_weaken_type)
-apply blast+
+prefer 2 apply assumption
+apply (erule_tac [2] fun_weaken_type, blast+)
 done
 
 lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Bool.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -72,7 +72,7 @@
 by (simp add: bool_defs )
 
 lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
-by (simp add: bool_defs , blast)
+by (simp add: bool_defs, blast)
 
 (*For Simp_tac and Blast_tac*)
 lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
@@ -137,7 +137,7 @@
        (a or b) and c  =  (a and c) or (b and c)"
 by (elim boolE, auto)
 
-(** binary orion **)
+(** binary 'or' **)
 
 lemma or_absorb [simp]: "a: bool ==> a or a = a"
 by (elim boolE, auto)
@@ -152,6 +152,25 @@
            (a and b) or c  =  (a or c) and (b or c)"
 by (elim boolE, auto)
 
+
+constdefs bool_of_o :: "o=>i"
+   "bool_of_o(P) == (if P then 1 else 0)"
+
+lemma [simp]: "bool_of_o(True) = 1"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "bool_of_o(False) = 0"
+by (simp add: bool_of_o_def) 
+
+lemma [simp,TC]: "bool_of_o(P) \<in> bool"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+by (simp add: bool_of_o_def) 
+
 ML
 {*
 val bool_def = thm "bool_def";
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Cardinal.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -432,8 +432,7 @@
 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
 
 lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)"
-apply (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
-done
+by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
 
 (*Can use AC or finiteness to discharge first premise*)
 lemma well_ord_lepoll_imp_Card_le:
@@ -805,10 +804,10 @@
 apply (erule Finite_cons)
 done
 
-lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
+lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
 by (blast intro: Finite_cons subset_Finite)
 
-lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
+lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
 by (simp add: succ_def)
 
 lemma nat_le_infinite_Ord: 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/CardinalArith.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -467,7 +467,7 @@
 
 (*A general fact about ordermap*)
 lemma ordermap_eqpoll_pred:
-    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
+    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
 apply (unfold eqpoll_def)
 apply (rule exI)
 apply (simp add: ordermap_eq_image well_ord_is_wf)
@@ -503,7 +503,7 @@
 done
 
 lemma pred_csquare_subset: 
-    "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
+    "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
 apply (unfold Order.pred_def)
 apply (safe del: SigmaI succCI)
 apply (erule csquareD [THEN conjE])
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -22,13 +22,11 @@
 lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cardinal_eqE)
-apply assumption+
+apply (rule well_ord_cardinal_eqE, assumption+)
 done
 
 lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
-apply (blast intro: cardinal_cong cardinal_eqE)
-done
+by (blast intro: cardinal_cong cardinal_eqE)
 
 lemma cardinal_disjoint_Un: "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==>  
           |A Un C| = |B Un D|"
@@ -37,38 +35,33 @@
 
 lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
 apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_lepoll_imp_Card_le)
-apply assumption
+apply (erule well_ord_lepoll_imp_Card_le, assumption)
 done
 
 lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cadd_assoc)
-apply assumption+
+apply (rule well_ord_cadd_assoc, assumption+)
 done
 
 lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cmult_assoc)
-apply assumption+
+apply (rule well_ord_cmult_assoc, assumption+)
 done
 
 lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cadd_cmult_distrib)
-apply assumption+
+apply (rule well_ord_cadd_cmult_distrib, assumption+)
 done
 
 lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
 apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_InfCard_square_eq)
-apply assumption
+apply (erule well_ord_InfCard_square_eq, assumption)
 done
 
 
@@ -83,7 +76,7 @@
 
 lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
 apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
-       erule Card_le_imp_lepoll);
+       erule Card_le_imp_lepoll)
 apply (erule lepoll_imp_Card_le) 
 done
 
@@ -119,12 +112,10 @@
  prefer 2
  apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
              elim!: LeastI Ord_in_Ord)
-apply (rule_tac c = "%z. <LEAST i. z:X (i) , f ` (LEAST i. z:X (i)) ` z>" 
+apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>" 
             and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
 (*Instantiate the lemma proved above*)
-apply (blast intro: inj_is_fun [THEN apply_type] dest: apply_type)
-apply (force ); 
-done
+by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
 
 
 (*The same again, using csucc*)
@@ -139,8 +130,7 @@
 lemma cardinal_UN_Ord_lt_csucc:
      "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
       ==> (UN i:K. j(i)) < csucc(K)"
-apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt])
-apply assumption
+apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
 apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
 apply (blast intro!: Ord_UN elim: ltE)
 apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
@@ -172,9 +162,8 @@
                   Card_is_Ord Ord_0_lt_csucc)
 apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
 apply (safe intro!: equalityI)
-apply (erule swap); 
-apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc])
-apply assumption+
+apply (erule swap) 
+apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
  apply (simp add: inj_converse_fun [THEN apply_type])
 apply (blast intro!: Ord_UN elim: ltE)
 done
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -1,28 +1,4 @@
-theory Datatype_absolute = WF_absolute:
-
-(*Epsilon.thy*)
-lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
-apply (insert arg_subset_eclose [of "{i}"], simp) 
-apply (frule eclose_subset, blast) 
-done
-
-lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
-apply (rule equalityI)
-apply (erule eclose_sing_Ord)  
-apply (rule succ_subset_eclose_sing) 
-done
-
-(*Ordinal.thy*)
-lemma relation_Memrel: "relation(Memrel(A))"
-by (simp add: relation_def Memrel_def, blast)
-
-lemma (in M_axioms) nat_case_closed:
-  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
-apply (case_tac "k=0", simp) 
-apply (case_tac "\<exists>m. k = succ(m)")
-apply force 
-apply (simp add: nat_case_def) 
-done
+theory Datatype_absolute = Formula + WF_absolute:
 
 
 subsection{*The lfp of a continuous function can be expressed as a union*}
@@ -143,13 +119,16 @@
               wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
 
 
+
 locale M_datatypes = M_wfrank +
 (*THEY NEED RELATIVIZATION*)
   assumes list_replacement1: 
 	   "[|M(A); n \<in> nat|] ==> 
 	    strong_replacement(M, 
-	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
-		     is_recfun (Memrel(succ(n)), x,
+	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
+                     pair(M,x,y,z) & successor(M,n,sucn) & 
+                     membership(M,sucn,memr) &
+		     is_recfun (memr, x,
 				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
 		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
       and list_replacement2': 
@@ -159,11 +138,11 @@
 lemma (in M_datatypes) list_replacement1':
   "[|M(A); n \<in> nat|]
    ==> strong_replacement
-	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
+	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
                is_recfun (Memrel(succ(n)), x,
-		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
+		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
  	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
-by (insert list_replacement1, simp) 
+by (insert list_replacement1, simp add: nat_into_M) 
 
 
 lemma (in M_datatypes) list_closed [intro,simp]:
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -2,48 +2,6 @@
 
 theory Formula = Main:
 
-
-(*??for Bool.thy**)
-constdefs bool_of_o :: "o=>i"
-   "bool_of_o(P) == (if P then 1 else 0)"
-
-lemma [simp]: "bool_of_o(True) = 1"
-by (simp add: bool_of_o_def) 
-
-lemma [simp]: "bool_of_o(False) = 0"
-by (simp add: bool_of_o_def) 
-
-lemma [simp,TC]: "bool_of_o(P) \<in> bool"
-by (simp add: bool_of_o_def) 
-
-lemma [simp]: "(bool_of_o(P) = 1) <-> P"
-by (simp add: bool_of_o_def) 
-
-lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
-by (simp add: bool_of_o_def) 
-
-(*????????????????CardinalArith *)
-
-lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
-apply (erule nat_induct)
- apply (simp add: Vfrom_0) 
-apply (simp add: Vset_succ) 
-done
-
-(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
-text{*Every ordinal is exceeded by some limit ordinal.*}
-lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
-apply (rule_tac x="i ++ nat" in exI) 
-apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
-done
-
-lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
-apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
-apply (simp add: Un_least_lt_iff) 
-done
-
-
-
 (*Internalized formulas of FOL. De Bruijn representation. 
   Unbound variables get their denotations from an environment.*)
 
@@ -250,7 +208,7 @@
 
   "arity(And(p,q)) = arity(p) \<union> arity(q)"
 
-  "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
+  "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
 
 
 lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
@@ -262,7 +220,7 @@
 lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
 by (simp add: Implies_def) 
 
-lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
+lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
 by (simp add: Exists_def) 
 
 
@@ -272,8 +230,8 @@
            arity(p) \<le> length(env) --> 
            sats(A, p, env @ extra) <-> sats(A, p, env)"
 apply (induct_tac p)
-apply (simp_all add: nth_append Un_least_lt_iff arity_type 
-                split: split_nat_case3, auto) 
+apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
+                split: split_nat_case, auto) 
 done
 
 lemma arity_sats1_iff:
@@ -308,14 +266,18 @@
 apply (induct_tac p) 
 apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
                      succ_Un_distrib [symmetric] incr_var_lt incr_var_le
-                     Un_commute incr_var_lemma arity_type 
-            split: split_nat_case3) 
-(*left with the And case*)
+                     Un_commute incr_var_lemma arity_type nat_imp_quasinat
+            split: split_nat_case) 
+ txt{*the Forall case reduces to linear arithmetic*}
+ prefer 2
+ apply clarify 
+ apply (blast dest: lt_trans1) 
+txt{*left with the And case*}
 apply safe
  apply (blast intro: incr_And_lemma lt_trans1) 
 apply (subst incr_And_lemma)
- apply (blast intro:  lt_trans1) 
-apply (simp add:  Un_commute)
+ apply (blast intro: lt_trans1) 
+apply (simp add: Un_commute)
 done
 
 lemma arity_incr_boundvars_eq:
@@ -774,8 +736,8 @@
     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
 apply (erule Limit_LsetE, assumption)
 apply (erule Limit_LsetE, assumption)
-apply (blast intro:  lt_LsetI [OF doubleton_in_Lset]
-                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
+apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
+                    Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
 done
 
 lemma Pair_in_LLimit:
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -1,6 +1,6 @@
 header {* The class L satisfies the axioms of ZF*}
 
-theory L_axioms = Formula + Relative:
+theory L_axioms = Formula + Relative + Reflection:
 
 
 text {* The class L satisfies the premises of locale @{text M_axioms} *}
@@ -72,57 +72,57 @@
 (*
 
   and Inter_separation:
-     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
+     "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
   and cartprod_separation:
      "[| L(A); L(B) |] 
-      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
+      ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"
   and image_separation:
      "[| L(A); L(r) |] 
-      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
+      ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(L,x,y,p)))"
   and vimage_separation:
      "[| L(A); L(r) |] 
-      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
+      ==> separation(L, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(L,x,y,p)))"
   and converse_separation:
-     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
-				     pair(M,x,y,p) & pair(M,y,x,z)))"
+     "L(r) ==> separation(L, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
+				     pair(L,x,y,p) & pair(L,y,x,z)))"
   and restrict_separation:
      "L(A) 
-      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
+      ==> separation(L, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(L,x,y,z)))"
   and comp_separation:
      "[| L(r); L(s) |]
-      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
+      ==> separation(L, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
 			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
-		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz)))"
   and pred_separation:
-     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
+     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
   and Memrel_separation:
-     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
+     "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
   and obase_separation:
      --{*part of the order type formalization*}
      "[| L(A); L(r) |] 
-      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
-	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
-	     order_isomorphism(M,par,r,x,mx,g))"
+      ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
+	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
+	     order_isomorphism(L,par,r,x,mx,g))"
   and well_ord_iso_separation:
      "[| L(A); L(f); L(r) |] 
-      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
-		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
+		     fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
   and obase_equals_separation:
      "[| L(A); L(r) |] 
       ==> separation
-      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
-	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
-	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
-	      order_isomorphism(M,pxr,r,y,my,g)))))"
+      (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
+	      ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
+	      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
+	      order_isomorphism(L,pxr,r,y,my,g)))))"
   and is_recfun_separation:
      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
      "[| L(A); L(f); L(g); L(a); L(b) |] 
-     ==> 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)"
+     ==> separation(L, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
   and omap_replacement:
      "[| L(A); L(r) |] 
-      ==> strong_replacement(M,
+      ==> strong_replacement(L,
              \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
-	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
-	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
+	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
 
 *)
\ No newline at end of file
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -2,11 +2,6 @@
 
 theory Relative = Main:
 
-(*func.thy*)
-lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
-by (simp add: succ_def mem_not_refl cons_fun_eq)
-
-
 subsection{* Relativized versions of standard set-theoretic concepts *}
 
 constdefs
@@ -899,6 +894,13 @@
      "n \<in> nat ==> M(n)"
 by (induct n rule: nat_induct, simp_all)
 
+lemma (in M_axioms) nat_case_closed:
+  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
+apply (case_tac "k=0", simp) 
+apply (case_tac "\<exists>m. k = succ(m)", force)
+apply (simp add: nat_case_def) 
+done
+
 lemma (in M_axioms) Inl_in_M_iff [iff]:
      "M(Inl(a)) <-> M(a)"
 by (simp add: Inl_def) 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -1,20 +1,5 @@
 theory WF_absolute = WFrec:
 
-(*????move to Wellorderings.thy*)
-lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
-     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
-by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
-
-lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
-     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
-by (blast intro: wellfounded_imp_wellfounded_on
-                 wellfounded_on_field_imp_wellfounded)
-
-lemma (in M_axioms) wellfounded_on_subset_A:
-     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
-by (simp add: wellfounded_on_def, blast)
-
-
 subsection{*Every well-founded relation is a subset of some inverse image of
       an ordinal*}
 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -3,14 +3,11 @@
 
 (*Many of these might be useful in WF.thy*)
 
-lemma is_recfunI:
-     "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
-by (simp add: is_recfun_def) 
-
-lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
-apply (simp add: is_recfun_def) 
-apply (erule ssubst)
-apply (rule function_lam) 
+lemma apply_recfun2:
+    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
+apply (frule apply_recfun) 
+ apply (blast dest: is_recfun_type fun_is_rel) 
+apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
 done
 
 text{*Expresses @{text is_recfun} as a recursion equation*}
@@ -28,14 +25,7 @@
 done
 
 lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
-by (blast dest:  is_recfun_type fun_is_rel)
-
-lemma apply_recfun2:
-    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
-apply (frule apply_recfun) 
- apply (blast dest: is_recfun_type fun_is_rel) 
-apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
-done
+by (blast dest: is_recfun_type fun_is_rel)
 
 lemma trans_Int_eq:
       "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
@@ -153,7 +143,7 @@
 apply (blast intro!: function_restrictI dest!: pair_components_in_M)
 apply (blast intro!: function_restrictI dest!: pair_components_in_M)
 apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
-apply (simp add:  vimage_singleton_iff) 
+apply (simp add: vimage_singleton_iff) 
 apply (intro allI impI conjI)
 apply (blast intro: transM dest!: pair_components_in_M)
 prefer 4;apply blast 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -71,6 +71,10 @@
     "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
 by (auto simp add: wellfounded_def wellfounded_on_def)
 
+lemma (in M_axioms) wellfounded_on_subset_A:
+     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
+by (simp add: wellfounded_on_def, blast)
+
 
 subsubsection {*Well-founded relations*}
 
@@ -85,6 +89,15 @@
      "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
 
+lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
+     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
+by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
+
+lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
+     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
+by (blast intro: wellfounded_imp_wellfounded_on
+                 wellfounded_on_field_imp_wellfounded)
+
 (*Consider the least z in domain(r) such that P(z) does not hold...*)
 lemma (in M_axioms) wellfounded_induct: 
      "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Epsilon.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -181,6 +181,17 @@
 apply (rule succI1 [THEN singleton_subsetI])
 done
 
+lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
+apply (insert arg_subset_eclose [of "{i}"], simp) 
+apply (frule eclose_subset, blast) 
+done
+
+lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
+apply (rule equalityI)
+apply (erule eclose_sing_Ord)  
+apply (rule succ_subset_eclose_sing) 
+done
+
 lemma Ord_transrec_type:
   assumes jini: "j: i"
       and ordi: "Ord(i)"
@@ -291,8 +302,8 @@
   r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = Union(f``{0}) = Union(nat) = nat,
   whose rank equals that of r.*)
 lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
-apply (clarify );  
-apply (simp add: function_apply_equality); 
+apply clarify  
+apply (simp add: function_apply_equality) 
 apply (blast intro: lt_trans rank_lt rank_pair2)
 done
 
@@ -332,7 +343,7 @@
 lemma transrec2_Limit:
      "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
 apply (rule transrec2_def [THEN def_transrec, THEN trans])
-apply (auto simp add: OUnion_def); 
+apply (auto simp add: OUnion_def) 
 done
 
 lemma def_transrec2:
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Finite.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -151,9 +151,7 @@
 done
 
 lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
-apply (erule FiniteFun.induct, simp)
-apply simp
-done
+by (erule FiniteFun.induct, simp, simp)
 
 lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
 
@@ -175,8 +173,7 @@
 
 lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
 apply (erule Fin.induct)
- apply (simp add: FiniteFun.intros)
-apply clarify
+ apply (simp add: FiniteFun.intros, clarify)
 apply (case_tac "a:b")
  apply (rotate_tac -1)
  apply (simp add: cons_absorb)
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/InfDatatype.thy
--- a/src/ZF/InfDatatype.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/InfDatatype.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -17,8 +17,7 @@
 apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
 apply (rule conjI)
 apply (rule_tac [2] le_UN_Ord_lt_csucc) 
-apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE)
-apply (simp_all add: ) 
+apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) 
  prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
 apply (rule Pi_type)
 apply (rename_tac [2] d)
@@ -44,7 +43,7 @@
 (*This level includes the function, and is below csucc(K)*)
 apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
 apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
-                    Un_least_lt); 
+                    Un_least_lt) 
 apply (erule subset_trans [THEN PowI])
 apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
 done
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Nat.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -12,15 +12,13 @@
   nat :: i
     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
 
+  quasinat :: "i => o"
+    "quasinat(n) == n=0 | (\<exists>m. n = succ(m))"
+
   (*Has an unconditional succ case, which is used in "recursor" below.*)
   nat_case :: "[i, i=>i, i]=>i"
     "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
 
-  (*Slightly different from the version above. Requires k to be a 
-    natural number, but it has a splitting rule.*)
-  nat_case3 :: "[i, i=>i, i]=>i"
-    "nat_case3(a,b,k) == THE y. k=0 & y=a | (EX x:nat. k=succ(x) & y=b(x))"
-
   nat_rec :: "[i, i, [i,i]=>i]=>i"
     "nat_rec(k,a,b) ==   
           wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
@@ -47,8 +45,7 @@
 
 lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
 apply (rule bnd_monoI)
-apply (cut_tac infinity, blast)
-apply blast 
+apply (cut_tac infinity, blast, blast) 
 done
 
 (* nat = {0} Un {succ(x). x:nat} *)
@@ -135,8 +132,7 @@
 
 lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
 apply (erule ltE)
-apply (erule Ord_trans, assumption)
-apply simp 
+apply (erule Ord_trans, assumption, simp) 
 done
 
 lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
@@ -205,6 +201,34 @@
      ==> P(m,n)"
 by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) 
 
+subsection{*quasinat: to allow a case-split rule for @{term nat_case}*}
+
+text{*True if the argument is zero or any successor*}
+lemma [iff]: "quasinat(0)"
+by (simp add: quasinat_def)
+
+lemma [iff]: "quasinat(succ(x))"
+by (simp add: quasinat_def)
+
+lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)"
+by (erule natE, simp_all)
+
+lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0" 
+by (simp add: quasinat_def nat_case_def) 
+
+lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
+txt{*The @{text case_tac} method is not yet available.*}
+apply (rule_tac P = "k=0" in case_split_thm, simp) 
+apply (rule_tac P = "\<exists>m. k = succ(m)" in case_split_thm, simp) 
+apply simp 
+apply (simp add: quasinat_def) 
+done
+
+lemma nat_cases:
+     "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
+apply (insert nat_cases_disj [of k], blast) 
+done
+
 (** nat_case **)
 
 lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
@@ -218,32 +242,13 @@
      ==> nat_case(a,b,n) : C(n)";
 by (erule nat_induct, auto) 
 
-(** nat_case3 **)
-
-lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
-by (simp add: nat_case3_def)
-
-lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
-by (simp add: nat_case3_def)
-
-lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
-apply (simp add: nat_case3_def) 
-apply (blast intro: the_0) 
+lemma split_nat_case:
+  "P(nat_case(a,b,k)) <-> 
+   ((k=0 --> P(a)) & (\<forall>x. k=succ(x) --> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
+apply (rule nat_cases [of k]) 
+apply (auto simp add: non_nat_case)
 done
 
-lemma split_nat_case3:
-  "P(nat_case3(a,b,k)) <-> 
-   ((k=0 --> P(a)) & (\<forall>x\<in>nat. k=succ(x) --> P(b(x))) & (k \<notin> nat \<longrightarrow> P(0)))"
-apply (rule_tac P="k\<in>nat" in case_split_thm)  
-    (*case_tac method not available yet; needs "inductive"*)
-apply (erule natE) 
-apply (auto simp add: non_nat_case3) 
-done
-
-lemma nat_case3_type [TC]:
-    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |] 
-     ==> nat_case3(a,b,n) : C(n)";
-by (erule nat_induct, auto) 
 
 
 (** nat_rec -- used to define eclose and transrec, then obsolete
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/OrderArith.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -38,26 +38,22 @@
 
 lemma radd_Inl_Inr_iff [iff]: 
     "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
 done
 
 lemma radd_Inl_iff [iff]: 
     "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
 done
 
 lemma radd_Inr_iff [iff]: 
     "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
 done
 
 lemma radd_Inr_Inl_iff [iff]: 
     "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
 done
 
 (** Elimination Rule **)
@@ -68,8 +64,7 @@
         !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;  
         !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q   
      |] ==> Q"
-apply (unfold radd_def)
-apply (blast intro: elim:); 
+apply (unfold radd_def, blast) 
 done
 
 (** Type checking **)
@@ -85,8 +80,7 @@
 
 lemma linear_radd: 
     "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
-apply (unfold linear_def)
-apply (blast intro: elim:); 
+apply (unfold linear_def, blast) 
 done
 
 
@@ -100,12 +94,11 @@
  apply (erule_tac V = "y : A + B" in thin_rl)
  apply (rule_tac ballI)
  apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
- apply (blast intro: elim:); 
+ apply blast 
 (*Returning to main part of proof*)
 apply safe
 apply blast
-apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption)
-apply (blast intro: elim:); 
+apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
 done
 
 lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
@@ -126,7 +119,7 @@
 lemma sum_bij:
      "[| f: bij(A,C);  g: bij(B,D) |]
       ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
-apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective)
+apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective)
 apply (typecheck add: bij_is_inj inj_is_fun) 
 apply (auto simp add: left_inverse_bij right_inverse_bij) 
 done
@@ -163,8 +156,7 @@
      "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
       : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
                 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
-apply (rule sum_assoc_bij [THEN ord_isoI])
-apply auto
+apply (rule sum_assoc_bij [THEN ord_isoI], auto)
 done
 
 
@@ -177,8 +169,7 @@
             (<a',a>: r  & a':A & a:A & b': B & b: B) |   
             (<b',b>: s  & a'=a & a:A & b': B & b: B)"
 
-apply (unfold rmult_def)
-apply blast
+apply (unfold rmult_def, blast)
 done
 
 lemma rmultE: 
@@ -186,7 +177,7 @@
         [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;         
         [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q  
      |] ==> Q"
-apply (blast intro: elim:); 
+apply blast 
 done
 
 (** Type checking **)
@@ -202,8 +193,7 @@
 
 lemma linear_rmult:
     "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
-apply (simp add: linear_def); 
-apply (blast intro: elim:); 
+apply (simp add: linear_def, blast) 
 done
 
 (** Well-foundedness **)
@@ -212,11 +202,10 @@
 apply (rule wf_onI2)
 apply (erule SigmaE)
 apply (erule ssubst)
-apply (subgoal_tac "ALL b:B. <x,b>: Ba")
-apply blast
-apply (erule_tac a = "x" in wf_on_induct , assumption)
+apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
+apply (erule_tac a = "x" in wf_on_induct, assumption)
 apply (rule ballI)
-apply (erule_tac a = "b" in wf_on_induct , assumption)
+apply (erule_tac a = "b" in wf_on_induct, assumption)
 apply (best elim!: rmultE bspec [THEN mp])
 done
 
@@ -257,9 +246,7 @@
 done
 
 lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
-apply (rule_tac d = "snd" in lam_bijective)
-apply auto
-done
+by (rule_tac d = "snd" in lam_bijective, auto)
 
 (*Used??*)
 lemma singleton_prod_ord_iso:
@@ -279,8 +266,7 @@
 apply (rule subst_elem)
 apply (rule id_bij [THEN sum_bij, THEN comp_bij])
 apply (rule singleton_prod_bij)
-apply (rule sum_disjoint_bij)
-apply blast
+apply (rule sum_disjoint_bij, blast)
 apply (simp (no_asm_simp) cong add: case_cong)
 apply (rule comp_lam [THEN trans, symmetric])
 apply (fast elim!: case_type)
@@ -303,7 +289,7 @@
 lemma sum_prod_distrib_bij:
      "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
       : bij((A+B)*C, (A*C)+(B*C))"
-apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) " 
+apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " 
        in lam_bijective)
 apply auto
 done
@@ -312,24 +298,21 @@
  "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
   : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),  
             (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
-apply (rule sum_prod_distrib_bij [THEN ord_isoI])
-apply auto
+apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
 done
 
 (** Associativity **)
 
 lemma prod_assoc_bij:
      "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
-apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective)
-apply auto
+apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
 done
 
 lemma prod_assoc_ord_iso:
  "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                    
   : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),   
             A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
-apply (rule prod_assoc_bij [THEN ord_isoI])
-apply auto
+apply (rule prod_assoc_bij [THEN ord_isoI], auto)
 done
 
 (**** Inverse image of a relation ****)
@@ -337,9 +320,7 @@
 (** Rewrite rule **)
 
 lemma rvimage_iff: "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
-apply (unfold rvimage_def)
-apply blast
-done
+by (unfold rvimage_def, blast)
 
 (** Type checking **)
 
@@ -351,9 +332,7 @@
 lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
 
 lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"
-apply (unfold rvimage_def)
-apply blast
-done
+by (unfold rvimage_def, blast)
 
 
 (** Partial Ordering Properties **)
@@ -381,7 +360,7 @@
 lemma linear_rvimage:
     "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
 apply (simp add: inj_def linear_def rvimage_iff) 
-apply (blast intro: apply_funtype); 
+apply (blast intro: apply_funtype) 
 done
 
 lemma tot_ord_rvimage: 
@@ -400,9 +379,9 @@
 apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }")
  apply (erule allE)
  apply (erule impE)
- apply assumption; 
+ apply assumption
  apply blast
-apply (blast intro: elim:); 
+apply blast 
 done
 
 lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
@@ -431,8 +410,7 @@
 
 lemma ord_iso_rvimage_eq: 
     "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
-apply (unfold ord_iso_def rvimage_def)
-apply blast
+apply (unfold ord_iso_def rvimage_def, blast)
 done
 
 
@@ -441,8 +419,7 @@
 lemma measure_eq_rvimage_Memrel:
      "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
 apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff)
-apply (rule equalityI)
-apply auto
+apply (rule equalityI, auto)
 apply (auto intro: Ord_in_Ord simp add: lt_def)
 done
 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/OrderType.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -11,7 +11,7 @@
 But a definition by transfinite recursion would be much simpler!
 *)
 
-theory OrderType = OrderArith + OrdQuant:
+theory OrderType = OrderArith + OrdQuant + Nat:
 
 constdefs
   
@@ -52,7 +52,7 @@
   "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
 
 
-(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
+subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
 
 lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
 apply (rule well_ordI)
@@ -99,7 +99,7 @@
 done
 
 
-(**** Ordermap and ordertype ****)
+subsection{*Ordermap and ordertype*}
 
 lemma ordermap_type: 
     "ordermap(A,r) : A -> ordertype(A,r)"
@@ -310,7 +310,7 @@
 done
 
 
-(**** Alternative definition of ordinal ****)
+subsection{*Alternative definition of ordinal*}
 
 (*proof by Krzysztof Grabczewski*)
 lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
@@ -330,7 +330,7 @@
 done
 
 
-(**** Ordinal Addition ****)
+subsection{*Ordinal Addition*}
 
 (*** Order Type calculations for radd ***)
 
@@ -666,6 +666,17 @@
 apply (blast intro: succ_leI oadd_le_mono)
 done
 
+text{*Every ordinal is exceeded by some limit ordinal.*}
+lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
+apply (rule_tac x="i ++ nat" in exI) 
+apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
+done
+
+lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
+apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
+apply (simp add: Un_least_lt_iff) 
+done
+
 
 (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
     Probably simpler to define the difference recursively!
@@ -733,7 +744,7 @@
 done
 
 
-(**** Ordinal Multiplication ****)
+subsection{*Ordinal Multiplication*}
 
 lemma Ord_omult [simp,TC]: 
     "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Ordinal.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -290,6 +290,9 @@
 lemma Memrel_1 [simp]: "Memrel(1) = 0"
 by (unfold Memrel_def, blast)
 
+lemma relation_Memrel: "relation(Memrel(A))"
+by (simp add: relation_def Memrel_def, blast)
+
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)
 lemma wf_Memrel: "wf(Memrel(A))"
@@ -316,8 +319,7 @@
         !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) |]
      ==>  P(i)"
 apply (simp add: Transset_def) 
-apply (erule wf_Memrel [THEN wf_induct2], blast)
-apply blast 
+apply (erule wf_Memrel [THEN wf_induct2], blast+)
 done
 
 (*Induction over an ordinal*)
@@ -404,8 +406,7 @@
 by (blast intro: Ord_0_le elim: ltE)
 
 lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i"
-apply (rule not_lt_iff_le [THEN iffD1], assumption)
-apply assumption
+apply (rule not_lt_iff_le [THEN iffD1], assumption+)
 apply (blast elim: ltE mem_irrefl)
 done
 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Perm.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -380,8 +380,7 @@
     "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
 apply (unfold inj_def surj_def, safe)
 apply (rule_tac x1 = "x" in bspec [THEN bexE])
-apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+)
-apply safe
+apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
 apply (rule_tac t = "op ` (g) " in subst_context)
 apply (erule asm_rl bspec [THEN bspec, THEN mp])+
 apply (simp (no_asm_simp))
@@ -518,8 +517,7 @@
 
 lemma inj_succ_restrict:
      "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
-apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption)
-apply blast
+apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
 apply (unfold inj_def)
 apply (fast elim: range_type mem_irrefl dest: apply_equality)
 done
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Trancl.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -124,8 +124,7 @@
 (*Closure under composition with r  *)
 lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
 apply (rule rtrancl_unfold [THEN ssubst])
-apply (rule compI [THEN UnI2], assumption)
-apply assumption
+apply (rule compI [THEN UnI2], assumption, assumption)
 done
 
 (*rtrancl of r contains all pairs in r  *)
@@ -301,8 +300,7 @@
 
 lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
 apply (drule rtrancl_mono)
-apply (drule rtrancl_mono, simp_all)
-apply blast
+apply (drule rtrancl_mono, simp_all, blast)
 done
 
 lemma rtrancl_Un_rtrancl:
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Univ.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -11,7 +11,7 @@
   But Ind_Syntax.univ refers to the constant "Univ.univ"
 *)
 
-theory Univ = Epsilon + Sum + Finite + mono:
+theory Univ = Epsilon + Cardinal:
 
 constdefs
   Vfrom       :: "[i,i]=>i"
@@ -37,9 +37,7 @@
 
 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
 lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
-apply (subst Vfrom_def [THEN def_transrec])
-apply simp
-done
+by (subst Vfrom_def [THEN def_transrec], simp)
 
 subsubsection{* Monotonicity *}
 
@@ -450,6 +448,12 @@
                     Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
 done
 
+lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0) 
+apply (simp add: Vset_succ) 
+done
+
 subsubsection{* Reasoning about sets in terms of their elements' ranks *}
 
 lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
@@ -483,8 +487,7 @@
 text{*NOT SUITABLE FOR REWRITING: recursive!*}
 lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
 apply (unfold Vrec_def)
-apply (subst transrec)
-apply simp
+apply (subst transrec, simp)
 apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
 done
 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Update.thy
--- a/src/ZF/Update.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Update.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -39,8 +39,7 @@
 apply (unfold update_def)
 apply (simp add: domain_of_fun cons_absorb)
 apply (rule fun_extension)
-apply (best intro: apply_type if_type lam_type, assumption)
-apply simp
+apply (best intro: apply_type if_type lam_type, assumption, simp)
 done
 
 
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/WF.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -165,20 +165,17 @@
 lemmas wf_asym = wf_not_sym [THEN swap, standard]
 
 lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
-done
+by (erule_tac a=a in wf_on_induct, assumption, blast)
 
 lemma wf_on_not_sym [rule_format]:
      "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
+apply (erule_tac a=a in wf_on_induct, assumption, blast)
 done
 
 lemma wf_on_asym:
      "[| wf[A](r);  ~Z ==> <a,b> : r;
          <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
-by (blast dest: wf_on_not_sym); 
+by (blast dest: wf_on_not_sym) 
 
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
@@ -187,8 +184,7 @@
      "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
 apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
        blast) 
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
+apply (erule_tac a=a in wf_on_induct, assumption, blast)
 done
 
 
@@ -226,12 +222,14 @@
 apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
 done
 
+lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
+
 lemma apply_recfun:
     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
 apply (unfold is_recfun_def) 
   txt{*replace f only on the left-hand side*}
 apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
-apply (simp add: underI); 
+apply (simp add: underI) 
 done
 
 lemma is_recfun_equal [rule_format]:
@@ -311,7 +309,7 @@
 lemma the_recfun_cut:
      "[| wf(r);  trans(r);  <b,a>:r |]
       ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
-by (blast intro: is_recfun_cut unfold_the_recfun);
+by (blast intro: is_recfun_cut unfold_the_recfun)
 
 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
 lemma wftrec:
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Zorn.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -55,12 +55,10 @@
 (*** Section 1.  Mathematical Preamble ***)
 
 lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
-apply blast
-done
+by blast
 
 lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
-apply blast
-done
+by blast
 
 
 (*** Section 2.  The Transfinite Construction ***)
@@ -71,9 +69,7 @@
 done
 
 lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
-apply (unfold increasing_def)
-apply (blast intro: elim:); 
-done
+by (unfold increasing_def, blast)
 
 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
 
@@ -87,8 +83,7 @@
       !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x);  
       !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y))  
    |] ==> P(n)"
-apply (erule TFin.induct)
-apply blast+
+apply (erule TFin.induct, blast+)
 done
 
 
@@ -119,19 +114,17 @@
 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
        assumption+)
 apply (blast del: subsetI
-	     intro: increasing_trans subsetI)
-apply (blast intro: elim:); 
+	     intro: increasing_trans subsetI, blast) 
 (*second induction step*)
 apply (rule impI [THEN ballI])
 apply (rule Union_lemma0 [THEN disjE])
 apply (erule_tac [3] disjI2)
-prefer 2 apply (blast intro: elim:); 
+prefer 2 apply blast 
 apply (rule ballI)
 apply (drule bspec, assumption) 
 apply (drule subsetD, assumption) 
 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
-       assumption+)
-apply (blast intro: elim:); 
+       assumption+, blast) 
 apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
 apply (blast dest: TFin_is_subset)+
 done
@@ -159,9 +152,8 @@
      "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m"
 apply (erule TFin_induct)
 apply (drule TFin_subsetD)
-apply (assumption+)
-apply (force ); 
-apply (blast)
+apply (assumption+, force) 
+apply blast
 done
 
 (*Property 3.3 of section 3.3*)
@@ -172,7 +164,7 @@
 apply (rule_tac [2] equal_next_upper [THEN Union_least])
 apply (assumption+)
 apply (erule ssubst)
-apply (rule increasingD2 [THEN equalityI] , assumption)
+apply (rule increasingD2 [THEN equalityI], assumption)
 apply (blast del: subsetI
 	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
 done
@@ -202,8 +194,7 @@
          X : chain(S);  X ~: maxchain(S) |]      
       ==> ch ` super(S,X) : super(S,X)"
 apply (erule apply_type)
-apply (unfold super_def maxchain_def)
-apply blast
+apply (unfold super_def maxchain_def, blast)
 done
 
 lemma choice_not_equals:
@@ -211,8 +202,7 @@
          X : chain(S);  X ~: maxchain(S) |]      
       ==> ch ` super(S,X) ~= X"
 apply (rule notI)
-apply (drule choice_super)
-apply assumption
+apply (drule choice_super, assumption)
 apply assumption
 apply (simp add: super_def)
 done
@@ -225,7 +215,7 @@
 apply (rule_tac x="\<lambda>X\<in>Pow(S). 
                    if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X" 
        in bexI)
-apply (force ); 
+apply force 
 apply (unfold increasing_def)
 apply (rule CollectI)
 apply (rule lam_type)
@@ -236,8 +226,7 @@
 apply safe
 apply (drule choice_super)
 apply (assumption+)
-apply (simp add: super_def)
-apply blast
+apply (simp add: super_def, blast)
 done
 
 (*Lemma 4*)
@@ -252,16 +241,13 @@
 apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] 
             choice_super [THEN super_subset_chain [THEN subsetD]])
 apply (unfold chain_def)
-apply (rule CollectI , blast)
-apply safe
-apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE])
-apply fast+ (*Blast_tac's slow*)
+apply (rule CollectI, blast, safe)
+apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE], fast+) (*Blast_tac's slow*)
 done
 
 lemma Hausdorff: "EX c. c : maxchain(S)"
 apply (rule AC_Pi_Pow [THEN exE])
-apply (rule Hausdorff_next_exists [THEN bexE])
-apply assumption
+apply (rule Hausdorff_next_exists [THEN bexE], assumption)
 apply (rename_tac ch "next")
 apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ")
 prefer 2
@@ -271,7 +257,7 @@
 apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
 apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
 apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
-prefer 2 apply (assumption)
+prefer 2 apply assumption
 apply (rule_tac [2] refl)
 apply (simp add: subset_refl [THEN TFin_UnionI, 
                               THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
@@ -286,8 +272,7 @@
 (*Used in the proof of Zorn's Lemma*)
 lemma chain_extend: 
     "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
-apply (unfold chain_def)
-apply blast
+apply (unfold chain_def, blast)
 done
 
 lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
@@ -295,14 +280,13 @@
 apply (simp add: maxchain_def)
 apply (rename_tac c)
 apply (rule_tac x = "Union (c)" in bexI)
-prefer 2 apply (blast)
+prefer 2 apply blast
 apply safe
 apply (rename_tac z)
 apply (rule classical)
 apply (subgoal_tac "cons (z,c) : super (S,c) ")
 apply (blast elim: equalityE)
-apply (unfold super_def)
-apply safe
+apply (unfold super_def, safe)
 apply (fast elim: chain_extend)
 apply (fast elim: equalityE)
 done
@@ -315,10 +299,9 @@
      "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]   
       ==> ALL m:Z. n<=m"
 apply (erule TFin_induct)
-prefer 2 apply (blast) (*second induction step is easy*)
+prefer 2 apply blast (*second induction step is easy*)
 apply (rule ballI)
-apply (rule bspec [THEN TFin_subsetD, THEN disjE])
-apply (auto ); 
+apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) 
 apply (subgoal_tac "m = Inter (Z) ")
 apply blast+
 done
@@ -330,8 +313,7 @@
 apply (simp (no_asm_simp) add: Inter_singleton)
 apply (erule equal_singleton)
 apply (rule Union_upper [THEN equalityI])
-apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec])
-apply (blast intro: elim:)+
+apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
 done
 
 (*This theorem just packages the previous result*)
@@ -341,17 +323,16 @@
 apply (unfold Subset_rel_def linear_def)
 (*Prove the well-foundedness goal*)
 apply (rule wf_onI)
-apply (frule well_ord_TFin_lemma , assumption)
-apply (drule_tac x = "Inter (Z) " in bspec , assumption)
+apply (frule well_ord_TFin_lemma, assumption)
+apply (drule_tac x = "Inter (Z) " in bspec, assumption)
 apply blast
 (*Now prove the linearity goal*)
 apply (intro ballI)
 apply (case_tac "x=y")
- apply (blast)
+ apply blast
 (*The x~=y case remains*)
 apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
-       assumption+)
-apply (blast intro: elim:)+
+       assumption+, blast+)
 done
 
 (** Defining the "next" operation for Zermelo's Theorem **)
@@ -369,7 +350,7 @@
                       next`X = (if X=S then S else cons(ch`(S-X), X))"
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
        in bexI)
-apply (force );  
+apply force  
 apply (unfold increasing_def)
 apply (rule CollectI)
 apply (rule lam_type)
@@ -414,13 +395,11 @@
 (*The wellordering theorem*)
 lemma AC_well_ord: "EX r. well_ord(S,r)"
 apply (rule AC_Pi_Pow [THEN exE])
-apply (rule Zermelo_next_exists [THEN bexE])
-apply assumption
+apply (rule Zermelo_next_exists [THEN bexE], assumption)
 apply (rule exI)
 apply (rule well_ord_rvimage)
 apply (erule_tac [2] well_ord_TFin)
-apply (rule choice_imp_injection [THEN inj_weaken_type])
-apply (blast intro: elim:)+
+apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
 done
   
 end
diff -r 240509babf00 -r 3ba9be497c33 src/ZF/func.thy
--- a/src/ZF/func.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/func.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -415,7 +415,7 @@
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
 lemma cons_fun_eq:
-     "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
+     "c ~: A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})"
 apply (rule equalityI)
 apply (safe elim!: fun_extend3)
 (*Inclusion of left into right*)
@@ -432,6 +432,9 @@
 apply (erule consE, simp_all)
 done
 
+lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
+by (simp add: succ_def mem_not_refl cons_fun_eq)
+
 ML
 {*
 val Pi_iff = thm "Pi_iff";