Tidying and introduction of various new theorems
authorpaulson
Tue Jul 02 13:28:08 2002 +0200 (2002-07-02)
changeset 132693ba9be497c33
parent 13268 240509babf00
child 13270 d7f35250cbad
Tidying and introduction of various new theorems
src/ZF/AC.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/InfDatatype.thy
src/ZF/Nat.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/Update.thy
src/ZF/WF.thy
src/ZF/Zorn.thy
src/ZF/func.thy
     1.1 --- a/src/ZF/AC.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/AC.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -23,27 +23,22 @@
     1.4  (*Using dtac, this has the advantage of DELETING the universal quantifier*)
     1.5  lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
     1.6  apply (rule AC_Pi)
     1.7 -apply (erule bspec)
     1.8 -apply assumption
     1.9 +apply (erule bspec, assumption)
    1.10  done
    1.11  
    1.12  lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
    1.13  apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
    1.14 -apply (erule_tac [2] exI)
    1.15 -apply blast
    1.16 +apply (erule_tac [2] exI, blast)
    1.17  done
    1.18  
    1.19  lemma AC_func:
    1.20       "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
    1.21  apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
    1.22 -prefer 2 apply (blast dest: apply_type intro: Pi_type)
    1.23 -apply (blast intro: elim:); 
    1.24 +prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) 
    1.25  done
    1.26  
    1.27  lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
    1.28 -apply (subgoal_tac "x \<noteq> 0")
    1.29 -apply blast+
    1.30 -done
    1.31 +by (subgoal_tac "x \<noteq> 0", blast+)
    1.32  
    1.33  lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
    1.34  apply (rule AC_func)
    1.35 @@ -53,9 +48,8 @@
    1.36  lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
    1.37  apply (rule AC_func0 [THEN bexE])
    1.38  apply (rule_tac [2] bexI)
    1.39 -prefer 2 apply (assumption)
    1.40 -apply (erule_tac [2] fun_weaken_type)
    1.41 -apply blast+
    1.42 +prefer 2 apply assumption
    1.43 +apply (erule_tac [2] fun_weaken_type, blast+)
    1.44  done
    1.45  
    1.46  lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
     2.1 --- a/src/ZF/Bool.thy	Mon Jul 01 18:16:18 2002 +0200
     2.2 +++ b/src/ZF/Bool.thy	Tue Jul 02 13:28:08 2002 +0200
     2.3 @@ -72,7 +72,7 @@
     2.4  by (simp add: bool_defs )
     2.5  
     2.6  lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
     2.7 -by (simp add: bool_defs , blast)
     2.8 +by (simp add: bool_defs, blast)
     2.9  
    2.10  (*For Simp_tac and Blast_tac*)
    2.11  lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
    2.12 @@ -137,7 +137,7 @@
    2.13         (a or b) and c  =  (a and c) or (b and c)"
    2.14  by (elim boolE, auto)
    2.15  
    2.16 -(** binary orion **)
    2.17 +(** binary 'or' **)
    2.18  
    2.19  lemma or_absorb [simp]: "a: bool ==> a or a = a"
    2.20  by (elim boolE, auto)
    2.21 @@ -152,6 +152,25 @@
    2.22             (a and b) or c  =  (a or c) and (b or c)"
    2.23  by (elim boolE, auto)
    2.24  
    2.25 +
    2.26 +constdefs bool_of_o :: "o=>i"
    2.27 +   "bool_of_o(P) == (if P then 1 else 0)"
    2.28 +
    2.29 +lemma [simp]: "bool_of_o(True) = 1"
    2.30 +by (simp add: bool_of_o_def) 
    2.31 +
    2.32 +lemma [simp]: "bool_of_o(False) = 0"
    2.33 +by (simp add: bool_of_o_def) 
    2.34 +
    2.35 +lemma [simp,TC]: "bool_of_o(P) \<in> bool"
    2.36 +by (simp add: bool_of_o_def) 
    2.37 +
    2.38 +lemma [simp]: "(bool_of_o(P) = 1) <-> P"
    2.39 +by (simp add: bool_of_o_def) 
    2.40 +
    2.41 +lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
    2.42 +by (simp add: bool_of_o_def) 
    2.43 +
    2.44  ML
    2.45  {*
    2.46  val bool_def = thm "bool_def";
     3.1 --- a/src/ZF/Cardinal.thy	Mon Jul 01 18:16:18 2002 +0200
     3.2 +++ b/src/ZF/Cardinal.thy	Tue Jul 02 13:28:08 2002 +0200
     3.3 @@ -432,8 +432,7 @@
     3.4  by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
     3.5  
     3.6  lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)"
     3.7 -apply (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
     3.8 -done
     3.9 +by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
    3.10  
    3.11  (*Can use AC or finiteness to discharge first premise*)
    3.12  lemma well_ord_lepoll_imp_Card_le:
    3.13 @@ -805,10 +804,10 @@
    3.14  apply (erule Finite_cons)
    3.15  done
    3.16  
    3.17 -lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
    3.18 +lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
    3.19  by (blast intro: Finite_cons subset_Finite)
    3.20  
    3.21 -lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
    3.22 +lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
    3.23  by (simp add: succ_def)
    3.24  
    3.25  lemma nat_le_infinite_Ord: 
     4.1 --- a/src/ZF/CardinalArith.thy	Mon Jul 01 18:16:18 2002 +0200
     4.2 +++ b/src/ZF/CardinalArith.thy	Tue Jul 02 13:28:08 2002 +0200
     4.3 @@ -467,7 +467,7 @@
     4.4  
     4.5  (*A general fact about ordermap*)
     4.6  lemma ordermap_eqpoll_pred:
     4.7 -    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
     4.8 +    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
     4.9  apply (unfold eqpoll_def)
    4.10  apply (rule exI)
    4.11  apply (simp add: ordermap_eq_image well_ord_is_wf)
    4.12 @@ -503,7 +503,7 @@
    4.13  done
    4.14  
    4.15  lemma pred_csquare_subset: 
    4.16 -    "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
    4.17 +    "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
    4.18  apply (unfold Order.pred_def)
    4.19  apply (safe del: SigmaI succCI)
    4.20  apply (erule csquareD [THEN conjE])
     5.1 --- a/src/ZF/Cardinal_AC.thy	Mon Jul 01 18:16:18 2002 +0200
     5.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Jul 02 13:28:08 2002 +0200
     5.3 @@ -22,13 +22,11 @@
     5.4  lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
     5.5  apply (rule AC_well_ord [THEN exE])
     5.6  apply (rule AC_well_ord [THEN exE])
     5.7 -apply (rule well_ord_cardinal_eqE)
     5.8 -apply assumption+
     5.9 +apply (rule well_ord_cardinal_eqE, assumption+)
    5.10  done
    5.11  
    5.12  lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
    5.13 -apply (blast intro: cardinal_cong cardinal_eqE)
    5.14 -done
    5.15 +by (blast intro: cardinal_cong cardinal_eqE)
    5.16  
    5.17  lemma cardinal_disjoint_Un: "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==>  
    5.18            |A Un C| = |B Un D|"
    5.19 @@ -37,38 +35,33 @@
    5.20  
    5.21  lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
    5.22  apply (rule AC_well_ord [THEN exE])
    5.23 -apply (erule well_ord_lepoll_imp_Card_le)
    5.24 -apply assumption
    5.25 +apply (erule well_ord_lepoll_imp_Card_le, assumption)
    5.26  done
    5.27  
    5.28  lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
    5.29  apply (rule AC_well_ord [THEN exE])
    5.30  apply (rule AC_well_ord [THEN exE])
    5.31  apply (rule AC_well_ord [THEN exE])
    5.32 -apply (rule well_ord_cadd_assoc)
    5.33 -apply assumption+
    5.34 +apply (rule well_ord_cadd_assoc, assumption+)
    5.35  done
    5.36  
    5.37  lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
    5.38  apply (rule AC_well_ord [THEN exE])
    5.39  apply (rule AC_well_ord [THEN exE])
    5.40  apply (rule AC_well_ord [THEN exE])
    5.41 -apply (rule well_ord_cmult_assoc)
    5.42 -apply assumption+
    5.43 +apply (rule well_ord_cmult_assoc, assumption+)
    5.44  done
    5.45  
    5.46  lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
    5.47  apply (rule AC_well_ord [THEN exE])
    5.48  apply (rule AC_well_ord [THEN exE])
    5.49  apply (rule AC_well_ord [THEN exE])
    5.50 -apply (rule well_ord_cadd_cmult_distrib)
    5.51 -apply assumption+
    5.52 +apply (rule well_ord_cadd_cmult_distrib, assumption+)
    5.53  done
    5.54  
    5.55  lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
    5.56  apply (rule AC_well_ord [THEN exE])
    5.57 -apply (erule well_ord_InfCard_square_eq)
    5.58 -apply assumption
    5.59 +apply (erule well_ord_InfCard_square_eq, assumption)
    5.60  done
    5.61  
    5.62  
    5.63 @@ -83,7 +76,7 @@
    5.64  
    5.65  lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
    5.66  apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
    5.67 -       erule Card_le_imp_lepoll);
    5.68 +       erule Card_le_imp_lepoll)
    5.69  apply (erule lepoll_imp_Card_le) 
    5.70  done
    5.71  
    5.72 @@ -119,12 +112,10 @@
    5.73   prefer 2
    5.74   apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
    5.75               elim!: LeastI Ord_in_Ord)
    5.76 -apply (rule_tac c = "%z. <LEAST i. z:X (i) , f ` (LEAST i. z:X (i)) ` z>" 
    5.77 +apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>" 
    5.78              and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
    5.79  (*Instantiate the lemma proved above*)
    5.80 -apply (blast intro: inj_is_fun [THEN apply_type] dest: apply_type)
    5.81 -apply (force ); 
    5.82 -done
    5.83 +by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
    5.84  
    5.85  
    5.86  (*The same again, using csucc*)
    5.87 @@ -139,8 +130,7 @@
    5.88  lemma cardinal_UN_Ord_lt_csucc:
    5.89       "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
    5.90        ==> (UN i:K. j(i)) < csucc(K)"
    5.91 -apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt])
    5.92 -apply assumption
    5.93 +apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
    5.94  apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
    5.95  apply (blast intro!: Ord_UN elim: ltE)
    5.96  apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
    5.97 @@ -172,9 +162,8 @@
    5.98                    Card_is_Ord Ord_0_lt_csucc)
    5.99  apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
   5.100  apply (safe intro!: equalityI)
   5.101 -apply (erule swap); 
   5.102 -apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc])
   5.103 -apply assumption+
   5.104 +apply (erule swap) 
   5.105 +apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
   5.106   apply (simp add: inj_converse_fun [THEN apply_type])
   5.107  apply (blast intro!: Ord_UN elim: ltE)
   5.108  done
     6.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 02 13:28:08 2002 +0200
     6.3 @@ -1,28 +1,4 @@
     6.4 -theory Datatype_absolute = WF_absolute:
     6.5 -
     6.6 -(*Epsilon.thy*)
     6.7 -lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
     6.8 -apply (insert arg_subset_eclose [of "{i}"], simp) 
     6.9 -apply (frule eclose_subset, blast) 
    6.10 -done
    6.11 -
    6.12 -lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
    6.13 -apply (rule equalityI)
    6.14 -apply (erule eclose_sing_Ord)  
    6.15 -apply (rule succ_subset_eclose_sing) 
    6.16 -done
    6.17 -
    6.18 -(*Ordinal.thy*)
    6.19 -lemma relation_Memrel: "relation(Memrel(A))"
    6.20 -by (simp add: relation_def Memrel_def, blast)
    6.21 -
    6.22 -lemma (in M_axioms) nat_case_closed:
    6.23 -  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    6.24 -apply (case_tac "k=0", simp) 
    6.25 -apply (case_tac "\<exists>m. k = succ(m)")
    6.26 -apply force 
    6.27 -apply (simp add: nat_case_def) 
    6.28 -done
    6.29 +theory Datatype_absolute = Formula + WF_absolute:
    6.30  
    6.31  
    6.32  subsection{*The lfp of a continuous function can be expressed as a union*}
    6.33 @@ -143,13 +119,16 @@
    6.34                wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
    6.35  
    6.36  
    6.37 +
    6.38  locale M_datatypes = M_wfrank +
    6.39  (*THEY NEED RELATIVIZATION*)
    6.40    assumes list_replacement1: 
    6.41  	   "[|M(A); n \<in> nat|] ==> 
    6.42  	    strong_replacement(M, 
    6.43 -	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
    6.44 -		     is_recfun (Memrel(succ(n)), x,
    6.45 +	      \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
    6.46 +                     pair(M,x,y,z) & successor(M,n,sucn) & 
    6.47 +                     membership(M,sucn,memr) &
    6.48 +		     is_recfun (memr, x,
    6.49  				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    6.50  		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
    6.51        and list_replacement2': 
    6.52 @@ -159,11 +138,11 @@
    6.53  lemma (in M_datatypes) list_replacement1':
    6.54    "[|M(A); n \<in> nat|]
    6.55     ==> strong_replacement
    6.56 -	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
    6.57 +	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
    6.58                 is_recfun (Memrel(succ(n)), x,
    6.59 -		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
    6.60 +		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    6.61   	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
    6.62 -by (insert list_replacement1, simp) 
    6.63 +by (insert list_replacement1, simp add: nat_into_M) 
    6.64  
    6.65  
    6.66  lemma (in M_datatypes) list_closed [intro,simp]:
     7.1 --- a/src/ZF/Constructible/Formula.thy	Mon Jul 01 18:16:18 2002 +0200
     7.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Jul 02 13:28:08 2002 +0200
     7.3 @@ -2,48 +2,6 @@
     7.4  
     7.5  theory Formula = Main:
     7.6  
     7.7 -
     7.8 -(*??for Bool.thy**)
     7.9 -constdefs bool_of_o :: "o=>i"
    7.10 -   "bool_of_o(P) == (if P then 1 else 0)"
    7.11 -
    7.12 -lemma [simp]: "bool_of_o(True) = 1"
    7.13 -by (simp add: bool_of_o_def) 
    7.14 -
    7.15 -lemma [simp]: "bool_of_o(False) = 0"
    7.16 -by (simp add: bool_of_o_def) 
    7.17 -
    7.18 -lemma [simp,TC]: "bool_of_o(P) \<in> bool"
    7.19 -by (simp add: bool_of_o_def) 
    7.20 -
    7.21 -lemma [simp]: "(bool_of_o(P) = 1) <-> P"
    7.22 -by (simp add: bool_of_o_def) 
    7.23 -
    7.24 -lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
    7.25 -by (simp add: bool_of_o_def) 
    7.26 -
    7.27 -(*????????????????CardinalArith *)
    7.28 -
    7.29 -lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
    7.30 -apply (erule nat_induct)
    7.31 - apply (simp add: Vfrom_0) 
    7.32 -apply (simp add: Vset_succ) 
    7.33 -done
    7.34 -
    7.35 -(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
    7.36 -text{*Every ordinal is exceeded by some limit ordinal.*}
    7.37 -lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
    7.38 -apply (rule_tac x="i ++ nat" in exI) 
    7.39 -apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
    7.40 -done
    7.41 -
    7.42 -lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
    7.43 -apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
    7.44 -apply (simp add: Un_least_lt_iff) 
    7.45 -done
    7.46 -
    7.47 -
    7.48 -
    7.49  (*Internalized formulas of FOL. De Bruijn representation. 
    7.50    Unbound variables get their denotations from an environment.*)
    7.51  
    7.52 @@ -250,7 +208,7 @@
    7.53  
    7.54    "arity(And(p,q)) = arity(p) \<union> arity(q)"
    7.55  
    7.56 -  "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
    7.57 +  "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
    7.58  
    7.59  
    7.60  lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
    7.61 @@ -262,7 +220,7 @@
    7.62  lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
    7.63  by (simp add: Implies_def) 
    7.64  
    7.65 -lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
    7.66 +lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
    7.67  by (simp add: Exists_def) 
    7.68  
    7.69  
    7.70 @@ -272,8 +230,8 @@
    7.71             arity(p) \<le> length(env) --> 
    7.72             sats(A, p, env @ extra) <-> sats(A, p, env)"
    7.73  apply (induct_tac p)
    7.74 -apply (simp_all add: nth_append Un_least_lt_iff arity_type 
    7.75 -                split: split_nat_case3, auto) 
    7.76 +apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
    7.77 +                split: split_nat_case, auto) 
    7.78  done
    7.79  
    7.80  lemma arity_sats1_iff:
    7.81 @@ -308,14 +266,18 @@
    7.82  apply (induct_tac p) 
    7.83  apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
    7.84                       succ_Un_distrib [symmetric] incr_var_lt incr_var_le
    7.85 -                     Un_commute incr_var_lemma arity_type 
    7.86 -            split: split_nat_case3) 
    7.87 -(*left with the And case*)
    7.88 +                     Un_commute incr_var_lemma arity_type nat_imp_quasinat
    7.89 +            split: split_nat_case) 
    7.90 + txt{*the Forall case reduces to linear arithmetic*}
    7.91 + prefer 2
    7.92 + apply clarify 
    7.93 + apply (blast dest: lt_trans1) 
    7.94 +txt{*left with the And case*}
    7.95  apply safe
    7.96   apply (blast intro: incr_And_lemma lt_trans1) 
    7.97  apply (subst incr_And_lemma)
    7.98 - apply (blast intro:  lt_trans1) 
    7.99 -apply (simp add:  Un_commute)
   7.100 + apply (blast intro: lt_trans1) 
   7.101 +apply (simp add: Un_commute)
   7.102  done
   7.103  
   7.104  lemma arity_incr_boundvars_eq:
   7.105 @@ -774,8 +736,8 @@
   7.106      "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
   7.107  apply (erule Limit_LsetE, assumption)
   7.108  apply (erule Limit_LsetE, assumption)
   7.109 -apply (blast intro:  lt_LsetI [OF doubleton_in_Lset]
   7.110 -                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   7.111 +apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
   7.112 +                    Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   7.113  done
   7.114  
   7.115  lemma Pair_in_LLimit:
     8.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
     8.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 02 13:28:08 2002 +0200
     8.3 @@ -1,6 +1,6 @@
     8.4  header {* The class L satisfies the axioms of ZF*}
     8.5  
     8.6 -theory L_axioms = Formula + Relative:
     8.7 +theory L_axioms = Formula + Relative + Reflection:
     8.8  
     8.9  
    8.10  text {* The class L satisfies the premises of locale @{text M_axioms} *}
    8.11 @@ -72,57 +72,57 @@
    8.12  (*
    8.13  
    8.14    and Inter_separation:
    8.15 -     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    8.16 +     "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    8.17    and cartprod_separation:
    8.18       "[| L(A); L(B) |] 
    8.19 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
    8.20 +      ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"
    8.21    and image_separation:
    8.22       "[| L(A); L(r) |] 
    8.23 -      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
    8.24 +      ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(L,x,y,p)))"
    8.25    and vimage_separation:
    8.26       "[| L(A); L(r) |] 
    8.27 -      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
    8.28 +      ==> separation(L, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(L,x,y,p)))"
    8.29    and converse_separation:
    8.30 -     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    8.31 -				     pair(M,x,y,p) & pair(M,y,x,z)))"
    8.32 +     "L(r) ==> separation(L, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    8.33 +				     pair(L,x,y,p) & pair(L,y,x,z)))"
    8.34    and restrict_separation:
    8.35       "L(A) 
    8.36 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
    8.37 +      ==> separation(L, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(L,x,y,z)))"
    8.38    and comp_separation:
    8.39       "[| L(r); L(s) |]
    8.40 -      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    8.41 +      ==> separation(L, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    8.42  			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
    8.43 -		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
    8.44 +		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz)))"
    8.45    and pred_separation:
    8.46 -     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
    8.47 +     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
    8.48    and Memrel_separation:
    8.49 -     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
    8.50 +     "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
    8.51    and obase_separation:
    8.52       --{*part of the order type formalization*}
    8.53       "[| L(A); L(r) |] 
    8.54 -      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
    8.55 -	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    8.56 -	     order_isomorphism(M,par,r,x,mx,g))"
    8.57 +      ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
    8.58 +	     ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
    8.59 +	     order_isomorphism(L,par,r,x,mx,g))"
    8.60    and well_ord_iso_separation:
    8.61       "[| L(A); L(f); L(r) |] 
    8.62 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
    8.63 -		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
    8.64 +      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
    8.65 +		     fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
    8.66    and obase_equals_separation:
    8.67       "[| L(A); L(r) |] 
    8.68        ==> separation
    8.69 -      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
    8.70 -	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
    8.71 -	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
    8.72 -	      order_isomorphism(M,pxr,r,y,my,g)))))"
    8.73 +      (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
    8.74 +	      ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
    8.75 +	      membership(L,y,my) & pred_set(L,A,x,r,pxr) &
    8.76 +	      order_isomorphism(L,pxr,r,y,my,g)))))"
    8.77    and is_recfun_separation:
    8.78       --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
    8.79       "[| L(A); L(f); L(g); L(a); L(b) |] 
    8.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)"
    8.81 +     ==> 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)"
    8.82    and omap_replacement:
    8.83       "[| L(A); L(r) |] 
    8.84 -      ==> strong_replacement(M,
    8.85 +      ==> strong_replacement(L,
    8.86               \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
    8.87 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
    8.88 -	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
    8.89 +	     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & 
    8.90 +	     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
    8.91  
    8.92  *)
    8.93 \ No newline at end of file
     9.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jul 01 18:16:18 2002 +0200
     9.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 02 13:28:08 2002 +0200
     9.3 @@ -2,11 +2,6 @@
     9.4  
     9.5  theory Relative = Main:
     9.6  
     9.7 -(*func.thy*)
     9.8 -lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
     9.9 -by (simp add: succ_def mem_not_refl cons_fun_eq)
    9.10 -
    9.11 -
    9.12  subsection{* Relativized versions of standard set-theoretic concepts *}
    9.13  
    9.14  constdefs
    9.15 @@ -899,6 +894,13 @@
    9.16       "n \<in> nat ==> M(n)"
    9.17  by (induct n rule: nat_induct, simp_all)
    9.18  
    9.19 +lemma (in M_axioms) nat_case_closed:
    9.20 +  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
    9.21 +apply (case_tac "k=0", simp) 
    9.22 +apply (case_tac "\<exists>m. k = succ(m)", force)
    9.23 +apply (simp add: nat_case_def) 
    9.24 +done
    9.25 +
    9.26  lemma (in M_axioms) Inl_in_M_iff [iff]:
    9.27       "M(Inl(a)) <-> M(a)"
    9.28  by (simp add: Inl_def) 
    10.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Jul 01 18:16:18 2002 +0200
    10.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 02 13:28:08 2002 +0200
    10.3 @@ -1,20 +1,5 @@
    10.4  theory WF_absolute = WFrec:
    10.5  
    10.6 -(*????move to Wellorderings.thy*)
    10.7 -lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
    10.8 -     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
    10.9 -by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
   10.10 -
   10.11 -lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
   10.12 -     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
   10.13 -by (blast intro: wellfounded_imp_wellfounded_on
   10.14 -                 wellfounded_on_field_imp_wellfounded)
   10.15 -
   10.16 -lemma (in M_axioms) wellfounded_on_subset_A:
   10.17 -     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
   10.18 -by (simp add: wellfounded_on_def, blast)
   10.19 -
   10.20 -
   10.21  subsection{*Every well-founded relation is a subset of some inverse image of
   10.22        an ordinal*}
   10.23  
    11.1 --- a/src/ZF/Constructible/WFrec.thy	Mon Jul 01 18:16:18 2002 +0200
    11.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Jul 02 13:28:08 2002 +0200
    11.3 @@ -3,14 +3,11 @@
    11.4  
    11.5  (*Many of these might be useful in WF.thy*)
    11.6  
    11.7 -lemma is_recfunI:
    11.8 -     "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
    11.9 -by (simp add: is_recfun_def) 
   11.10 -
   11.11 -lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
   11.12 -apply (simp add: is_recfun_def) 
   11.13 -apply (erule ssubst)
   11.14 -apply (rule function_lam) 
   11.15 +lemma apply_recfun2:
   11.16 +    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
   11.17 +apply (frule apply_recfun) 
   11.18 + apply (blast dest: is_recfun_type fun_is_rel) 
   11.19 +apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   11.20  done
   11.21  
   11.22  text{*Expresses @{text is_recfun} as a recursion equation*}
   11.23 @@ -28,14 +25,7 @@
   11.24  done
   11.25  
   11.26  lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
   11.27 -by (blast dest:  is_recfun_type fun_is_rel)
   11.28 -
   11.29 -lemma apply_recfun2:
   11.30 -    "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
   11.31 -apply (frule apply_recfun) 
   11.32 - apply (blast dest: is_recfun_type fun_is_rel) 
   11.33 -apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   11.34 -done
   11.35 +by (blast dest: is_recfun_type fun_is_rel)
   11.36  
   11.37  lemma trans_Int_eq:
   11.38        "[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
   11.39 @@ -153,7 +143,7 @@
   11.40  apply (blast intro!: function_restrictI dest!: pair_components_in_M)
   11.41  apply (blast intro!: function_restrictI dest!: pair_components_in_M)
   11.42  apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
   11.43 -apply (simp add:  vimage_singleton_iff) 
   11.44 +apply (simp add: vimage_singleton_iff) 
   11.45  apply (intro allI impI conjI)
   11.46  apply (blast intro: transM dest!: pair_components_in_M)
   11.47  prefer 4;apply blast 
    12.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Jul 01 18:16:18 2002 +0200
    12.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Jul 02 13:28:08 2002 +0200
    12.3 @@ -71,6 +71,10 @@
    12.4      "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    12.5  by (auto simp add: wellfounded_def wellfounded_on_def)
    12.6  
    12.7 +lemma (in M_axioms) wellfounded_on_subset_A:
    12.8 +     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    12.9 +by (simp add: wellfounded_on_def, blast)
   12.10 +
   12.11  
   12.12  subsubsection {*Well-founded relations*}
   12.13  
   12.14 @@ -85,6 +89,15 @@
   12.15       "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
   12.16  by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
   12.17  
   12.18 +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
   12.19 +     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
   12.20 +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
   12.21 +
   12.22 +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
   12.23 +     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
   12.24 +by (blast intro: wellfounded_imp_wellfounded_on
   12.25 +                 wellfounded_on_field_imp_wellfounded)
   12.26 +
   12.27  (*Consider the least z in domain(r) such that P(z) does not hold...*)
   12.28  lemma (in M_axioms) wellfounded_induct: 
   12.29       "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
    13.1 --- a/src/ZF/Epsilon.thy	Mon Jul 01 18:16:18 2002 +0200
    13.2 +++ b/src/ZF/Epsilon.thy	Tue Jul 02 13:28:08 2002 +0200
    13.3 @@ -181,6 +181,17 @@
    13.4  apply (rule succI1 [THEN singleton_subsetI])
    13.5  done
    13.6  
    13.7 +lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
    13.8 +apply (insert arg_subset_eclose [of "{i}"], simp) 
    13.9 +apply (frule eclose_subset, blast) 
   13.10 +done
   13.11 +
   13.12 +lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
   13.13 +apply (rule equalityI)
   13.14 +apply (erule eclose_sing_Ord)  
   13.15 +apply (rule succ_subset_eclose_sing) 
   13.16 +done
   13.17 +
   13.18  lemma Ord_transrec_type:
   13.19    assumes jini: "j: i"
   13.20        and ordi: "Ord(i)"
   13.21 @@ -291,8 +302,8 @@
   13.22    r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = Union(f``{0}) = Union(nat) = nat,
   13.23    whose rank equals that of r.*)
   13.24  lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
   13.25 -apply (clarify );  
   13.26 -apply (simp add: function_apply_equality); 
   13.27 +apply clarify  
   13.28 +apply (simp add: function_apply_equality) 
   13.29  apply (blast intro: lt_trans rank_lt rank_pair2)
   13.30  done
   13.31  
   13.32 @@ -332,7 +343,7 @@
   13.33  lemma transrec2_Limit:
   13.34       "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
   13.35  apply (rule transrec2_def [THEN def_transrec, THEN trans])
   13.36 -apply (auto simp add: OUnion_def); 
   13.37 +apply (auto simp add: OUnion_def) 
   13.38  done
   13.39  
   13.40  lemma def_transrec2:
    14.1 --- a/src/ZF/Finite.thy	Mon Jul 01 18:16:18 2002 +0200
    14.2 +++ b/src/ZF/Finite.thy	Tue Jul 02 13:28:08 2002 +0200
    14.3 @@ -151,9 +151,7 @@
    14.4  done
    14.5  
    14.6  lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
    14.7 -apply (erule FiniteFun.induct, simp)
    14.8 -apply simp
    14.9 -done
   14.10 +by (erule FiniteFun.induct, simp, simp)
   14.11  
   14.12  lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
   14.13  
   14.14 @@ -175,8 +173,7 @@
   14.15  
   14.16  lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
   14.17  apply (erule Fin.induct)
   14.18 - apply (simp add: FiniteFun.intros)
   14.19 -apply clarify
   14.20 + apply (simp add: FiniteFun.intros, clarify)
   14.21  apply (case_tac "a:b")
   14.22   apply (rotate_tac -1)
   14.23   apply (simp add: cons_absorb)
    15.1 --- a/src/ZF/InfDatatype.thy	Mon Jul 01 18:16:18 2002 +0200
    15.2 +++ b/src/ZF/InfDatatype.thy	Tue Jul 02 13:28:08 2002 +0200
    15.3 @@ -17,8 +17,7 @@
    15.4  apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
    15.5  apply (rule conjI)
    15.6  apply (rule_tac [2] le_UN_Ord_lt_csucc) 
    15.7 -apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE)
    15.8 -apply (simp_all add: ) 
    15.9 +apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) 
   15.10   prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
   15.11  apply (rule Pi_type)
   15.12  apply (rename_tac [2] d)
   15.13 @@ -44,7 +43,7 @@
   15.14  (*This level includes the function, and is below csucc(K)*)
   15.15  apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
   15.16  apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
   15.17 -                    Un_least_lt); 
   15.18 +                    Un_least_lt) 
   15.19  apply (erule subset_trans [THEN PowI])
   15.20  apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
   15.21  done
    16.1 --- a/src/ZF/Nat.thy	Mon Jul 01 18:16:18 2002 +0200
    16.2 +++ b/src/ZF/Nat.thy	Tue Jul 02 13:28:08 2002 +0200
    16.3 @@ -12,15 +12,13 @@
    16.4    nat :: i
    16.5      "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
    16.6  
    16.7 +  quasinat :: "i => o"
    16.8 +    "quasinat(n) == n=0 | (\<exists>m. n = succ(m))"
    16.9 +
   16.10    (*Has an unconditional succ case, which is used in "recursor" below.*)
   16.11    nat_case :: "[i, i=>i, i]=>i"
   16.12      "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
   16.13  
   16.14 -  (*Slightly different from the version above. Requires k to be a 
   16.15 -    natural number, but it has a splitting rule.*)
   16.16 -  nat_case3 :: "[i, i=>i, i]=>i"
   16.17 -    "nat_case3(a,b,k) == THE y. k=0 & y=a | (EX x:nat. k=succ(x) & y=b(x))"
   16.18 -
   16.19    nat_rec :: "[i, i, [i,i]=>i]=>i"
   16.20      "nat_rec(k,a,b) ==   
   16.21            wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
   16.22 @@ -47,8 +45,7 @@
   16.23  
   16.24  lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
   16.25  apply (rule bnd_monoI)
   16.26 -apply (cut_tac infinity, blast)
   16.27 -apply blast 
   16.28 +apply (cut_tac infinity, blast, blast) 
   16.29  done
   16.30  
   16.31  (* nat = {0} Un {succ(x). x:nat} *)
   16.32 @@ -135,8 +132,7 @@
   16.33  
   16.34  lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
   16.35  apply (erule ltE)
   16.36 -apply (erule Ord_trans, assumption)
   16.37 -apply simp 
   16.38 +apply (erule Ord_trans, assumption, simp) 
   16.39  done
   16.40  
   16.41  lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
   16.42 @@ -205,6 +201,34 @@
   16.43       ==> P(m,n)"
   16.44  by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) 
   16.45  
   16.46 +subsection{*quasinat: to allow a case-split rule for @{term nat_case}*}
   16.47 +
   16.48 +text{*True if the argument is zero or any successor*}
   16.49 +lemma [iff]: "quasinat(0)"
   16.50 +by (simp add: quasinat_def)
   16.51 +
   16.52 +lemma [iff]: "quasinat(succ(x))"
   16.53 +by (simp add: quasinat_def)
   16.54 +
   16.55 +lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)"
   16.56 +by (erule natE, simp_all)
   16.57 +
   16.58 +lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0" 
   16.59 +by (simp add: quasinat_def nat_case_def) 
   16.60 +
   16.61 +lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
   16.62 +txt{*The @{text case_tac} method is not yet available.*}
   16.63 +apply (rule_tac P = "k=0" in case_split_thm, simp) 
   16.64 +apply (rule_tac P = "\<exists>m. k = succ(m)" in case_split_thm, simp) 
   16.65 +apply simp 
   16.66 +apply (simp add: quasinat_def) 
   16.67 +done
   16.68 +
   16.69 +lemma nat_cases:
   16.70 +     "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
   16.71 +apply (insert nat_cases_disj [of k], blast) 
   16.72 +done
   16.73 +
   16.74  (** nat_case **)
   16.75  
   16.76  lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
   16.77 @@ -218,32 +242,13 @@
   16.78       ==> nat_case(a,b,n) : C(n)";
   16.79  by (erule nat_induct, auto) 
   16.80  
   16.81 -(** nat_case3 **)
   16.82 -
   16.83 -lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
   16.84 -by (simp add: nat_case3_def)
   16.85 -
   16.86 -lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
   16.87 -by (simp add: nat_case3_def)
   16.88 -
   16.89 -lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
   16.90 -apply (simp add: nat_case3_def) 
   16.91 -apply (blast intro: the_0) 
   16.92 +lemma split_nat_case:
   16.93 +  "P(nat_case(a,b,k)) <-> 
   16.94 +   ((k=0 --> P(a)) & (\<forall>x. k=succ(x) --> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
   16.95 +apply (rule nat_cases [of k]) 
   16.96 +apply (auto simp add: non_nat_case)
   16.97  done
   16.98  
   16.99 -lemma split_nat_case3:
  16.100 -  "P(nat_case3(a,b,k)) <-> 
  16.101 -   ((k=0 --> P(a)) & (\<forall>x\<in>nat. k=succ(x) --> P(b(x))) & (k \<notin> nat \<longrightarrow> P(0)))"
  16.102 -apply (rule_tac P="k\<in>nat" in case_split_thm)  
  16.103 -    (*case_tac method not available yet; needs "inductive"*)
  16.104 -apply (erule natE) 
  16.105 -apply (auto simp add: non_nat_case3) 
  16.106 -done
  16.107 -
  16.108 -lemma nat_case3_type [TC]:
  16.109 -    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |] 
  16.110 -     ==> nat_case3(a,b,n) : C(n)";
  16.111 -by (erule nat_induct, auto) 
  16.112  
  16.113  
  16.114  (** nat_rec -- used to define eclose and transrec, then obsolete
    17.1 --- a/src/ZF/OrderArith.thy	Mon Jul 01 18:16:18 2002 +0200
    17.2 +++ b/src/ZF/OrderArith.thy	Tue Jul 02 13:28:08 2002 +0200
    17.3 @@ -38,26 +38,22 @@
    17.4  
    17.5  lemma radd_Inl_Inr_iff [iff]: 
    17.6      "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
    17.7 -apply (unfold radd_def)
    17.8 -apply blast
    17.9 +apply (unfold radd_def, blast)
   17.10  done
   17.11  
   17.12  lemma radd_Inl_iff [iff]: 
   17.13      "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
   17.14 -apply (unfold radd_def)
   17.15 -apply blast
   17.16 +apply (unfold radd_def, blast)
   17.17  done
   17.18  
   17.19  lemma radd_Inr_iff [iff]: 
   17.20      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
   17.21 -apply (unfold radd_def)
   17.22 -apply blast
   17.23 +apply (unfold radd_def, blast)
   17.24  done
   17.25  
   17.26  lemma radd_Inr_Inl_iff [iff]: 
   17.27      "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
   17.28 -apply (unfold radd_def)
   17.29 -apply blast
   17.30 +apply (unfold radd_def, blast)
   17.31  done
   17.32  
   17.33  (** Elimination Rule **)
   17.34 @@ -68,8 +64,7 @@
   17.35          !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;  
   17.36          !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q   
   17.37       |] ==> Q"
   17.38 -apply (unfold radd_def)
   17.39 -apply (blast intro: elim:); 
   17.40 +apply (unfold radd_def, blast) 
   17.41  done
   17.42  
   17.43  (** Type checking **)
   17.44 @@ -85,8 +80,7 @@
   17.45  
   17.46  lemma linear_radd: 
   17.47      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
   17.48 -apply (unfold linear_def)
   17.49 -apply (blast intro: elim:); 
   17.50 +apply (unfold linear_def, blast) 
   17.51  done
   17.52  
   17.53  
   17.54 @@ -100,12 +94,11 @@
   17.55   apply (erule_tac V = "y : A + B" in thin_rl)
   17.56   apply (rule_tac ballI)
   17.57   apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
   17.58 - apply (blast intro: elim:); 
   17.59 + apply blast 
   17.60  (*Returning to main part of proof*)
   17.61  apply safe
   17.62  apply blast
   17.63 -apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption)
   17.64 -apply (blast intro: elim:); 
   17.65 +apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
   17.66  done
   17.67  
   17.68  lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
   17.69 @@ -126,7 +119,7 @@
   17.70  lemma sum_bij:
   17.71       "[| f: bij(A,C);  g: bij(B,D) |]
   17.72        ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
   17.73 -apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective)
   17.74 +apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective)
   17.75  apply (typecheck add: bij_is_inj inj_is_fun) 
   17.76  apply (auto simp add: left_inverse_bij right_inverse_bij) 
   17.77  done
   17.78 @@ -163,8 +156,7 @@
   17.79       "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
   17.80        : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
   17.81                  A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
   17.82 -apply (rule sum_assoc_bij [THEN ord_isoI])
   17.83 -apply auto
   17.84 +apply (rule sum_assoc_bij [THEN ord_isoI], auto)
   17.85  done
   17.86  
   17.87  
   17.88 @@ -177,8 +169,7 @@
   17.89              (<a',a>: r  & a':A & a:A & b': B & b: B) |   
   17.90              (<b',b>: s  & a'=a & a:A & b': B & b: B)"
   17.91  
   17.92 -apply (unfold rmult_def)
   17.93 -apply blast
   17.94 +apply (unfold rmult_def, blast)
   17.95  done
   17.96  
   17.97  lemma rmultE: 
   17.98 @@ -186,7 +177,7 @@
   17.99          [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;         
  17.100          [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q  
  17.101       |] ==> Q"
  17.102 -apply (blast intro: elim:); 
  17.103 +apply blast 
  17.104  done
  17.105  
  17.106  (** Type checking **)
  17.107 @@ -202,8 +193,7 @@
  17.108  
  17.109  lemma linear_rmult:
  17.110      "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
  17.111 -apply (simp add: linear_def); 
  17.112 -apply (blast intro: elim:); 
  17.113 +apply (simp add: linear_def, blast) 
  17.114  done
  17.115  
  17.116  (** Well-foundedness **)
  17.117 @@ -212,11 +202,10 @@
  17.118  apply (rule wf_onI2)
  17.119  apply (erule SigmaE)
  17.120  apply (erule ssubst)
  17.121 -apply (subgoal_tac "ALL b:B. <x,b>: Ba")
  17.122 -apply blast
  17.123 -apply (erule_tac a = "x" in wf_on_induct , assumption)
  17.124 +apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
  17.125 +apply (erule_tac a = "x" in wf_on_induct, assumption)
  17.126  apply (rule ballI)
  17.127 -apply (erule_tac a = "b" in wf_on_induct , assumption)
  17.128 +apply (erule_tac a = "b" in wf_on_induct, assumption)
  17.129  apply (best elim!: rmultE bspec [THEN mp])
  17.130  done
  17.131  
  17.132 @@ -257,9 +246,7 @@
  17.133  done
  17.134  
  17.135  lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
  17.136 -apply (rule_tac d = "snd" in lam_bijective)
  17.137 -apply auto
  17.138 -done
  17.139 +by (rule_tac d = "snd" in lam_bijective, auto)
  17.140  
  17.141  (*Used??*)
  17.142  lemma singleton_prod_ord_iso:
  17.143 @@ -279,8 +266,7 @@
  17.144  apply (rule subst_elem)
  17.145  apply (rule id_bij [THEN sum_bij, THEN comp_bij])
  17.146  apply (rule singleton_prod_bij)
  17.147 -apply (rule sum_disjoint_bij)
  17.148 -apply blast
  17.149 +apply (rule sum_disjoint_bij, blast)
  17.150  apply (simp (no_asm_simp) cong add: case_cong)
  17.151  apply (rule comp_lam [THEN trans, symmetric])
  17.152  apply (fast elim!: case_type)
  17.153 @@ -303,7 +289,7 @@
  17.154  lemma sum_prod_distrib_bij:
  17.155       "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
  17.156        : bij((A+B)*C, (A*C)+(B*C))"
  17.157 -apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) " 
  17.158 +apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " 
  17.159         in lam_bijective)
  17.160  apply auto
  17.161  done
  17.162 @@ -312,24 +298,21 @@
  17.163   "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
  17.164    : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),  
  17.165              (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
  17.166 -apply (rule sum_prod_distrib_bij [THEN ord_isoI])
  17.167 -apply auto
  17.168 +apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
  17.169  done
  17.170  
  17.171  (** Associativity **)
  17.172  
  17.173  lemma prod_assoc_bij:
  17.174       "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
  17.175 -apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective)
  17.176 -apply auto
  17.177 +apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
  17.178  done
  17.179  
  17.180  lemma prod_assoc_ord_iso:
  17.181   "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                    
  17.182    : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),   
  17.183              A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
  17.184 -apply (rule prod_assoc_bij [THEN ord_isoI])
  17.185 -apply auto
  17.186 +apply (rule prod_assoc_bij [THEN ord_isoI], auto)
  17.187  done
  17.188  
  17.189  (**** Inverse image of a relation ****)
  17.190 @@ -337,9 +320,7 @@
  17.191  (** Rewrite rule **)
  17.192  
  17.193  lemma rvimage_iff: "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
  17.194 -apply (unfold rvimage_def)
  17.195 -apply blast
  17.196 -done
  17.197 +by (unfold rvimage_def, blast)
  17.198  
  17.199  (** Type checking **)
  17.200  
  17.201 @@ -351,9 +332,7 @@
  17.202  lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
  17.203  
  17.204  lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"
  17.205 -apply (unfold rvimage_def)
  17.206 -apply blast
  17.207 -done
  17.208 +by (unfold rvimage_def, blast)
  17.209  
  17.210  
  17.211  (** Partial Ordering Properties **)
  17.212 @@ -381,7 +360,7 @@
  17.213  lemma linear_rvimage:
  17.214      "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
  17.215  apply (simp add: inj_def linear_def rvimage_iff) 
  17.216 -apply (blast intro: apply_funtype); 
  17.217 +apply (blast intro: apply_funtype) 
  17.218  done
  17.219  
  17.220  lemma tot_ord_rvimage: 
  17.221 @@ -400,9 +379,9 @@
  17.222  apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }")
  17.223   apply (erule allE)
  17.224   apply (erule impE)
  17.225 - apply assumption; 
  17.226 + apply assumption
  17.227   apply blast
  17.228 -apply (blast intro: elim:); 
  17.229 +apply blast 
  17.230  done
  17.231  
  17.232  lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
  17.233 @@ -431,8 +410,7 @@
  17.234  
  17.235  lemma ord_iso_rvimage_eq: 
  17.236      "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
  17.237 -apply (unfold ord_iso_def rvimage_def)
  17.238 -apply blast
  17.239 +apply (unfold ord_iso_def rvimage_def, blast)
  17.240  done
  17.241  
  17.242  
  17.243 @@ -441,8 +419,7 @@
  17.244  lemma measure_eq_rvimage_Memrel:
  17.245       "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
  17.246  apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff)
  17.247 -apply (rule equalityI)
  17.248 -apply auto
  17.249 +apply (rule equalityI, auto)
  17.250  apply (auto intro: Ord_in_Ord simp add: lt_def)
  17.251  done
  17.252  
    18.1 --- a/src/ZF/OrderType.thy	Mon Jul 01 18:16:18 2002 +0200
    18.2 +++ b/src/ZF/OrderType.thy	Tue Jul 02 13:28:08 2002 +0200
    18.3 @@ -11,7 +11,7 @@
    18.4  But a definition by transfinite recursion would be much simpler!
    18.5  *)
    18.6  
    18.7 -theory OrderType = OrderArith + OrdQuant:
    18.8 +theory OrderType = OrderArith + OrdQuant + Nat:
    18.9  
   18.10  constdefs
   18.11    
   18.12 @@ -52,7 +52,7 @@
   18.13    "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
   18.14  
   18.15  
   18.16 -(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
   18.17 +subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
   18.18  
   18.19  lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
   18.20  apply (rule well_ordI)
   18.21 @@ -99,7 +99,7 @@
   18.22  done
   18.23  
   18.24  
   18.25 -(**** Ordermap and ordertype ****)
   18.26 +subsection{*Ordermap and ordertype*}
   18.27  
   18.28  lemma ordermap_type: 
   18.29      "ordermap(A,r) : A -> ordertype(A,r)"
   18.30 @@ -310,7 +310,7 @@
   18.31  done
   18.32  
   18.33  
   18.34 -(**** Alternative definition of ordinal ****)
   18.35 +subsection{*Alternative definition of ordinal*}
   18.36  
   18.37  (*proof by Krzysztof Grabczewski*)
   18.38  lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
   18.39 @@ -330,7 +330,7 @@
   18.40  done
   18.41  
   18.42  
   18.43 -(**** Ordinal Addition ****)
   18.44 +subsection{*Ordinal Addition*}
   18.45  
   18.46  (*** Order Type calculations for radd ***)
   18.47  
   18.48 @@ -666,6 +666,17 @@
   18.49  apply (blast intro: succ_leI oadd_le_mono)
   18.50  done
   18.51  
   18.52 +text{*Every ordinal is exceeded by some limit ordinal.*}
   18.53 +lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
   18.54 +apply (rule_tac x="i ++ nat" in exI) 
   18.55 +apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
   18.56 +done
   18.57 +
   18.58 +lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
   18.59 +apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
   18.60 +apply (simp add: Un_least_lt_iff) 
   18.61 +done
   18.62 +
   18.63  
   18.64  (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
   18.65      Probably simpler to define the difference recursively!
   18.66 @@ -733,7 +744,7 @@
   18.67  done
   18.68  
   18.69  
   18.70 -(**** Ordinal Multiplication ****)
   18.71 +subsection{*Ordinal Multiplication*}
   18.72  
   18.73  lemma Ord_omult [simp,TC]: 
   18.74      "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"
    19.1 --- a/src/ZF/Ordinal.thy	Mon Jul 01 18:16:18 2002 +0200
    19.2 +++ b/src/ZF/Ordinal.thy	Tue Jul 02 13:28:08 2002 +0200
    19.3 @@ -290,6 +290,9 @@
    19.4  lemma Memrel_1 [simp]: "Memrel(1) = 0"
    19.5  by (unfold Memrel_def, blast)
    19.6  
    19.7 +lemma relation_Memrel: "relation(Memrel(A))"
    19.8 +by (simp add: relation_def Memrel_def, blast)
    19.9 +
   19.10  (*The membership relation (as a set) is well-founded.
   19.11    Proof idea: show A<=B by applying the foundation axiom to A-B *)
   19.12  lemma wf_Memrel: "wf(Memrel(A))"
   19.13 @@ -316,8 +319,7 @@
   19.14          !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) |]
   19.15       ==>  P(i)"
   19.16  apply (simp add: Transset_def) 
   19.17 -apply (erule wf_Memrel [THEN wf_induct2], blast)
   19.18 -apply blast 
   19.19 +apply (erule wf_Memrel [THEN wf_induct2], blast+)
   19.20  done
   19.21  
   19.22  (*Induction over an ordinal*)
   19.23 @@ -404,8 +406,7 @@
   19.24  by (blast intro: Ord_0_le elim: ltE)
   19.25  
   19.26  lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i"
   19.27 -apply (rule not_lt_iff_le [THEN iffD1], assumption)
   19.28 -apply assumption
   19.29 +apply (rule not_lt_iff_le [THEN iffD1], assumption+)
   19.30  apply (blast elim: ltE mem_irrefl)
   19.31  done
   19.32  
    20.1 --- a/src/ZF/Perm.thy	Mon Jul 01 18:16:18 2002 +0200
    20.2 +++ b/src/ZF/Perm.thy	Tue Jul 02 13:28:08 2002 +0200
    20.3 @@ -380,8 +380,7 @@
    20.4      "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
    20.5  apply (unfold inj_def surj_def, safe)
    20.6  apply (rule_tac x1 = "x" in bspec [THEN bexE])
    20.7 -apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+)
    20.8 -apply safe
    20.9 +apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
   20.10  apply (rule_tac t = "op ` (g) " in subst_context)
   20.11  apply (erule asm_rl bspec [THEN bspec, THEN mp])+
   20.12  apply (simp (no_asm_simp))
   20.13 @@ -518,8 +517,7 @@
   20.14  
   20.15  lemma inj_succ_restrict:
   20.16       "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
   20.17 -apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption)
   20.18 -apply blast
   20.19 +apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
   20.20  apply (unfold inj_def)
   20.21  apply (fast elim: range_type mem_irrefl dest: apply_equality)
   20.22  done
    21.1 --- a/src/ZF/Trancl.thy	Mon Jul 01 18:16:18 2002 +0200
    21.2 +++ b/src/ZF/Trancl.thy	Tue Jul 02 13:28:08 2002 +0200
    21.3 @@ -124,8 +124,7 @@
    21.4  (*Closure under composition with r  *)
    21.5  lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
    21.6  apply (rule rtrancl_unfold [THEN ssubst])
    21.7 -apply (rule compI [THEN UnI2], assumption)
    21.8 -apply assumption
    21.9 +apply (rule compI [THEN UnI2], assumption, assumption)
   21.10  done
   21.11  
   21.12  (*rtrancl of r contains all pairs in r  *)
   21.13 @@ -301,8 +300,7 @@
   21.14  
   21.15  lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
   21.16  apply (drule rtrancl_mono)
   21.17 -apply (drule rtrancl_mono, simp_all)
   21.18 -apply blast
   21.19 +apply (drule rtrancl_mono, simp_all, blast)
   21.20  done
   21.21  
   21.22  lemma rtrancl_Un_rtrancl:
    22.1 --- a/src/ZF/Univ.thy	Mon Jul 01 18:16:18 2002 +0200
    22.2 +++ b/src/ZF/Univ.thy	Tue Jul 02 13:28:08 2002 +0200
    22.3 @@ -11,7 +11,7 @@
    22.4    But Ind_Syntax.univ refers to the constant "Univ.univ"
    22.5  *)
    22.6  
    22.7 -theory Univ = Epsilon + Sum + Finite + mono:
    22.8 +theory Univ = Epsilon + Cardinal:
    22.9  
   22.10  constdefs
   22.11    Vfrom       :: "[i,i]=>i"
   22.12 @@ -37,9 +37,7 @@
   22.13  
   22.14  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
   22.15  lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
   22.16 -apply (subst Vfrom_def [THEN def_transrec])
   22.17 -apply simp
   22.18 -done
   22.19 +by (subst Vfrom_def [THEN def_transrec], simp)
   22.20  
   22.21  subsubsection{* Monotonicity *}
   22.22  
   22.23 @@ -450,6 +448,12 @@
   22.24                      Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   22.25  done
   22.26  
   22.27 +lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
   22.28 +apply (erule nat_induct)
   22.29 + apply (simp add: Vfrom_0) 
   22.30 +apply (simp add: Vset_succ) 
   22.31 +done
   22.32 +
   22.33  subsubsection{* Reasoning about sets in terms of their elements' ranks *}
   22.34  
   22.35  lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   22.36 @@ -483,8 +487,7 @@
   22.37  text{*NOT SUITABLE FOR REWRITING: recursive!*}
   22.38  lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   22.39  apply (unfold Vrec_def)
   22.40 -apply (subst transrec)
   22.41 -apply simp
   22.42 +apply (subst transrec, simp)
   22.43  apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
   22.44  done
   22.45  
    23.1 --- a/src/ZF/Update.thy	Mon Jul 01 18:16:18 2002 +0200
    23.2 +++ b/src/ZF/Update.thy	Tue Jul 02 13:28:08 2002 +0200
    23.3 @@ -39,8 +39,7 @@
    23.4  apply (unfold update_def)
    23.5  apply (simp add: domain_of_fun cons_absorb)
    23.6  apply (rule fun_extension)
    23.7 -apply (best intro: apply_type if_type lam_type, assumption)
    23.8 -apply simp
    23.9 +apply (best intro: apply_type if_type lam_type, assumption, simp)
   23.10  done
   23.11  
   23.12  
    24.1 --- a/src/ZF/WF.thy	Mon Jul 01 18:16:18 2002 +0200
    24.2 +++ b/src/ZF/WF.thy	Tue Jul 02 13:28:08 2002 +0200
    24.3 @@ -165,20 +165,17 @@
    24.4  lemmas wf_asym = wf_not_sym [THEN swap, standard]
    24.5  
    24.6  lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
    24.7 -apply (erule_tac a=a in wf_on_induct, assumption)
    24.8 -apply blast
    24.9 -done
   24.10 +by (erule_tac a=a in wf_on_induct, assumption, blast)
   24.11  
   24.12  lemma wf_on_not_sym [rule_format]:
   24.13       "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
   24.14 -apply (erule_tac a=a in wf_on_induct, assumption)
   24.15 -apply blast
   24.16 +apply (erule_tac a=a in wf_on_induct, assumption, blast)
   24.17  done
   24.18  
   24.19  lemma wf_on_asym:
   24.20       "[| wf[A](r);  ~Z ==> <a,b> : r;
   24.21           <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
   24.22 -by (blast dest: wf_on_not_sym); 
   24.23 +by (blast dest: wf_on_not_sym) 
   24.24  
   24.25  
   24.26  (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   24.27 @@ -187,8 +184,7 @@
   24.28       "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
   24.29  apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
   24.30         blast) 
   24.31 -apply (erule_tac a=a in wf_on_induct, assumption)
   24.32 -apply blast
   24.33 +apply (erule_tac a=a in wf_on_induct, assumption, blast)
   24.34  done
   24.35  
   24.36  
   24.37 @@ -226,12 +222,14 @@
   24.38  apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
   24.39  done
   24.40  
   24.41 +lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
   24.42 +
   24.43  lemma apply_recfun:
   24.44      "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
   24.45  apply (unfold is_recfun_def) 
   24.46    txt{*replace f only on the left-hand side*}
   24.47  apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
   24.48 -apply (simp add: underI); 
   24.49 +apply (simp add: underI) 
   24.50  done
   24.51  
   24.52  lemma is_recfun_equal [rule_format]:
   24.53 @@ -311,7 +309,7 @@
   24.54  lemma the_recfun_cut:
   24.55       "[| wf(r);  trans(r);  <b,a>:r |]
   24.56        ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
   24.57 -by (blast intro: is_recfun_cut unfold_the_recfun);
   24.58 +by (blast intro: is_recfun_cut unfold_the_recfun)
   24.59  
   24.60  (*NOT SUITABLE FOR REWRITING: it is recursive!*)
   24.61  lemma wftrec:
    25.1 --- a/src/ZF/Zorn.thy	Mon Jul 01 18:16:18 2002 +0200
    25.2 +++ b/src/ZF/Zorn.thy	Tue Jul 02 13:28:08 2002 +0200
    25.3 @@ -55,12 +55,10 @@
    25.4  (*** Section 1.  Mathematical Preamble ***)
    25.5  
    25.6  lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
    25.7 -apply blast
    25.8 -done
    25.9 +by blast
   25.10  
   25.11  lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
   25.12 -apply blast
   25.13 -done
   25.14 +by blast
   25.15  
   25.16  
   25.17  (*** Section 2.  The Transfinite Construction ***)
   25.18 @@ -71,9 +69,7 @@
   25.19  done
   25.20  
   25.21  lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
   25.22 -apply (unfold increasing_def)
   25.23 -apply (blast intro: elim:); 
   25.24 -done
   25.25 +by (unfold increasing_def, blast)
   25.26  
   25.27  lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
   25.28  
   25.29 @@ -87,8 +83,7 @@
   25.30        !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x);  
   25.31        !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y))  
   25.32     |] ==> P(n)"
   25.33 -apply (erule TFin.induct)
   25.34 -apply blast+
   25.35 +apply (erule TFin.induct, blast+)
   25.36  done
   25.37  
   25.38  
   25.39 @@ -119,19 +114,17 @@
   25.40  apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
   25.41         assumption+)
   25.42  apply (blast del: subsetI
   25.43 -	     intro: increasing_trans subsetI)
   25.44 -apply (blast intro: elim:); 
   25.45 +	     intro: increasing_trans subsetI, blast) 
   25.46  (*second induction step*)
   25.47  apply (rule impI [THEN ballI])
   25.48  apply (rule Union_lemma0 [THEN disjE])
   25.49  apply (erule_tac [3] disjI2)
   25.50 -prefer 2 apply (blast intro: elim:); 
   25.51 +prefer 2 apply blast 
   25.52  apply (rule ballI)
   25.53  apply (drule bspec, assumption) 
   25.54  apply (drule subsetD, assumption) 
   25.55  apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
   25.56 -       assumption+)
   25.57 -apply (blast intro: elim:); 
   25.58 +       assumption+, blast) 
   25.59  apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
   25.60  apply (blast dest: TFin_is_subset)+
   25.61  done
   25.62 @@ -159,9 +152,8 @@
   25.63       "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m"
   25.64  apply (erule TFin_induct)
   25.65  apply (drule TFin_subsetD)
   25.66 -apply (assumption+)
   25.67 -apply (force ); 
   25.68 -apply (blast)
   25.69 +apply (assumption+, force) 
   25.70 +apply blast
   25.71  done
   25.72  
   25.73  (*Property 3.3 of section 3.3*)
   25.74 @@ -172,7 +164,7 @@
   25.75  apply (rule_tac [2] equal_next_upper [THEN Union_least])
   25.76  apply (assumption+)
   25.77  apply (erule ssubst)
   25.78 -apply (rule increasingD2 [THEN equalityI] , assumption)
   25.79 +apply (rule increasingD2 [THEN equalityI], assumption)
   25.80  apply (blast del: subsetI
   25.81  	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
   25.82  done
   25.83 @@ -202,8 +194,7 @@
   25.84           X : chain(S);  X ~: maxchain(S) |]      
   25.85        ==> ch ` super(S,X) : super(S,X)"
   25.86  apply (erule apply_type)
   25.87 -apply (unfold super_def maxchain_def)
   25.88 -apply blast
   25.89 +apply (unfold super_def maxchain_def, blast)
   25.90  done
   25.91  
   25.92  lemma choice_not_equals:
   25.93 @@ -211,8 +202,7 @@
   25.94           X : chain(S);  X ~: maxchain(S) |]      
   25.95        ==> ch ` super(S,X) ~= X"
   25.96  apply (rule notI)
   25.97 -apply (drule choice_super)
   25.98 -apply assumption
   25.99 +apply (drule choice_super, assumption)
  25.100  apply assumption
  25.101  apply (simp add: super_def)
  25.102  done
  25.103 @@ -225,7 +215,7 @@
  25.104  apply (rule_tac x="\<lambda>X\<in>Pow(S). 
  25.105                     if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X" 
  25.106         in bexI)
  25.107 -apply (force ); 
  25.108 +apply force 
  25.109  apply (unfold increasing_def)
  25.110  apply (rule CollectI)
  25.111  apply (rule lam_type)
  25.112 @@ -236,8 +226,7 @@
  25.113  apply safe
  25.114  apply (drule choice_super)
  25.115  apply (assumption+)
  25.116 -apply (simp add: super_def)
  25.117 -apply blast
  25.118 +apply (simp add: super_def, blast)
  25.119  done
  25.120  
  25.121  (*Lemma 4*)
  25.122 @@ -252,16 +241,13 @@
  25.123  apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] 
  25.124              choice_super [THEN super_subset_chain [THEN subsetD]])
  25.125  apply (unfold chain_def)
  25.126 -apply (rule CollectI , blast)
  25.127 -apply safe
  25.128 -apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE])
  25.129 -apply fast+ (*Blast_tac's slow*)
  25.130 +apply (rule CollectI, blast, safe)
  25.131 +apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE], fast+) (*Blast_tac's slow*)
  25.132  done
  25.133  
  25.134  lemma Hausdorff: "EX c. c : maxchain(S)"
  25.135  apply (rule AC_Pi_Pow [THEN exE])
  25.136 -apply (rule Hausdorff_next_exists [THEN bexE])
  25.137 -apply assumption
  25.138 +apply (rule Hausdorff_next_exists [THEN bexE], assumption)
  25.139  apply (rename_tac ch "next")
  25.140  apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ")
  25.141  prefer 2
  25.142 @@ -271,7 +257,7 @@
  25.143  apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
  25.144  apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
  25.145  apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
  25.146 -prefer 2 apply (assumption)
  25.147 +prefer 2 apply assumption
  25.148  apply (rule_tac [2] refl)
  25.149  apply (simp add: subset_refl [THEN TFin_UnionI, 
  25.150                                THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
  25.151 @@ -286,8 +272,7 @@
  25.152  (*Used in the proof of Zorn's Lemma*)
  25.153  lemma chain_extend: 
  25.154      "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
  25.155 -apply (unfold chain_def)
  25.156 -apply blast
  25.157 +apply (unfold chain_def, blast)
  25.158  done
  25.159  
  25.160  lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
  25.161 @@ -295,14 +280,13 @@
  25.162  apply (simp add: maxchain_def)
  25.163  apply (rename_tac c)
  25.164  apply (rule_tac x = "Union (c)" in bexI)
  25.165 -prefer 2 apply (blast)
  25.166 +prefer 2 apply blast
  25.167  apply safe
  25.168  apply (rename_tac z)
  25.169  apply (rule classical)
  25.170  apply (subgoal_tac "cons (z,c) : super (S,c) ")
  25.171  apply (blast elim: equalityE)
  25.172 -apply (unfold super_def)
  25.173 -apply safe
  25.174 +apply (unfold super_def, safe)
  25.175  apply (fast elim: chain_extend)
  25.176  apply (fast elim: equalityE)
  25.177  done
  25.178 @@ -315,10 +299,9 @@
  25.179       "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]   
  25.180        ==> ALL m:Z. n<=m"
  25.181  apply (erule TFin_induct)
  25.182 -prefer 2 apply (blast) (*second induction step is easy*)
  25.183 +prefer 2 apply blast (*second induction step is easy*)
  25.184  apply (rule ballI)
  25.185 -apply (rule bspec [THEN TFin_subsetD, THEN disjE])
  25.186 -apply (auto ); 
  25.187 +apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) 
  25.188  apply (subgoal_tac "m = Inter (Z) ")
  25.189  apply blast+
  25.190  done
  25.191 @@ -330,8 +313,7 @@
  25.192  apply (simp (no_asm_simp) add: Inter_singleton)
  25.193  apply (erule equal_singleton)
  25.194  apply (rule Union_upper [THEN equalityI])
  25.195 -apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec])
  25.196 -apply (blast intro: elim:)+
  25.197 +apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
  25.198  done
  25.199  
  25.200  (*This theorem just packages the previous result*)
  25.201 @@ -341,17 +323,16 @@
  25.202  apply (unfold Subset_rel_def linear_def)
  25.203  (*Prove the well-foundedness goal*)
  25.204  apply (rule wf_onI)
  25.205 -apply (frule well_ord_TFin_lemma , assumption)
  25.206 -apply (drule_tac x = "Inter (Z) " in bspec , assumption)
  25.207 +apply (frule well_ord_TFin_lemma, assumption)
  25.208 +apply (drule_tac x = "Inter (Z) " in bspec, assumption)
  25.209  apply blast
  25.210  (*Now prove the linearity goal*)
  25.211  apply (intro ballI)
  25.212  apply (case_tac "x=y")
  25.213 - apply (blast)
  25.214 + apply blast
  25.215  (*The x~=y case remains*)
  25.216  apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
  25.217 -       assumption+)
  25.218 -apply (blast intro: elim:)+
  25.219 +       assumption+, blast+)
  25.220  done
  25.221  
  25.222  (** Defining the "next" operation for Zermelo's Theorem **)
  25.223 @@ -369,7 +350,7 @@
  25.224                        next`X = (if X=S then S else cons(ch`(S-X), X))"
  25.225  apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
  25.226         in bexI)
  25.227 -apply (force );  
  25.228 +apply force  
  25.229  apply (unfold increasing_def)
  25.230  apply (rule CollectI)
  25.231  apply (rule lam_type)
  25.232 @@ -414,13 +395,11 @@
  25.233  (*The wellordering theorem*)
  25.234  lemma AC_well_ord: "EX r. well_ord(S,r)"
  25.235  apply (rule AC_Pi_Pow [THEN exE])
  25.236 -apply (rule Zermelo_next_exists [THEN bexE])
  25.237 -apply assumption
  25.238 +apply (rule Zermelo_next_exists [THEN bexE], assumption)
  25.239  apply (rule exI)
  25.240  apply (rule well_ord_rvimage)
  25.241  apply (erule_tac [2] well_ord_TFin)
  25.242 -apply (rule choice_imp_injection [THEN inj_weaken_type])
  25.243 -apply (blast intro: elim:)+
  25.244 +apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
  25.245  done
  25.246    
  25.247  end
    26.1 --- a/src/ZF/func.thy	Mon Jul 01 18:16:18 2002 +0200
    26.2 +++ b/src/ZF/func.thy	Tue Jul 02 13:28:08 2002 +0200
    26.3 @@ -415,7 +415,7 @@
    26.4  
    26.5  (*For Finite.ML.  Inclusion of right into left is easy*)
    26.6  lemma cons_fun_eq:
    26.7 -     "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
    26.8 +     "c ~: A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})"
    26.9  apply (rule equalityI)
   26.10  apply (safe elim!: fun_extend3)
   26.11  (*Inclusion of left into right*)
   26.12 @@ -432,6 +432,9 @@
   26.13  apply (erule consE, simp_all)
   26.14  done
   26.15  
   26.16 +lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
   26.17 +by (simp add: succ_def mem_not_refl cons_fun_eq)
   26.18 +
   26.19  ML
   26.20  {*
   26.21  val Pi_iff = thm "Pi_iff";