Fixed quantified variable name preservation for ball and bex (bounded quants)
authorpaulson
Wed Jul 10 16:54:07 2002 +0200 (2002-07-10)
changeset 133390f89104dd377
parent 13338 20ca66539bef
child 13340 9b0332344ae2
Fixed quantified variable name preservation for ball and bex (bounded quants)
Requires tweaking of other scripts. Also routine tidying.
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/AC16_lemmas.thy
src/ZF/AC/AC17_AC1.thy
src/ZF/AC/AC18_AC19.thy
src/ZF/AC/Cardinal_aux.thy
src/ZF/AC/DC.thy
src/ZF/AC/HH.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/WO1_WO7.thy
src/ZF/AC/WO2_AC16.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/Coind/ECR.thy
src/ZF/Coind/Map.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/Induct/Multiset.ML
src/ZF/Induct/Primrec.thy
src/ZF/Integ/IntDiv.ML
src/ZF/IsaMakefile
src/ZF/List.thy
src/ZF/OrdQuant.thy
src/ZF/Order.thy
src/ZF/OrderType.thy
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Redex.thy
src/ZF/Resid/Reduction.thy
src/ZF/Resid/Residuals.thy
src/ZF/Resid/Substitution.thy
src/ZF/UNITY/Comp.ML
src/ZF/UNITY/GenPrefix.ML
src/ZF/UNITY/Guar.ML
src/ZF/UNITY/ListPlus.ML
src/ZF/UNITY/Union.ML
src/ZF/ZF.ML
src/ZF/ex/Commutation.thy
src/ZF/ex/LList.thy
src/ZF/ex/Limit.thy
src/ZF/ex/Primes.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/misc.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Wed Jul 10 16:07:52 2002 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Wed Jul 10 16:54:07 2002 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  apply (erule bexE)
     1.5  apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
     1.6  apply (erule exE)
     1.7 -apply (rule_tac x = "n" in exI)
     1.8 +apply (rule_tac x = n in exI)
     1.9  apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI)
    1.10  apply (simp add: ltD bij_def surj_def)
    1.11  apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun] 
    1.12 @@ -267,7 +267,7 @@
    1.13        ==> \<exists>! c. c \<in> s(u) & a \<subseteq> c & b \<in> c"
    1.14  apply (rule all_ex [simplified k_def, THEN ballE])
    1.15   apply (erule ex1E)
    1.16 - apply (rule_tac a = "w" in ex1I, blast intro: sI)
    1.17 + apply (rule_tac a = w in ex1I, blast intro: sI)
    1.18   apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in)
    1.19  apply (blast del: PowI 
    1.20               intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll])
    1.21 @@ -295,7 +295,7 @@
    1.22  apply (rule lam_type)
    1.23  apply (frule ex1_superset_a [THEN theI], fast+, clarify)
    1.24  apply (rule cons_eqE [of _ a])
    1.25 -apply (drule_tac A = "THE c. ?P (c) " and C = "y" in eq_imp_Int_eq)
    1.26 +apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
    1.27  apply (simp_all add: the_eq_cons)
    1.28  done
    1.29  
    1.30 @@ -412,7 +412,7 @@
    1.31       "v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
    1.32  apply (unfold MM_def LL_def, safe, fast)
    1.33  apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
    1.34 -apply (rule_tac x = "x" in all_ex [THEN ballE]) 
    1.35 +apply (rule_tac x = x in all_ex [THEN ballE]) 
    1.36  apply (blast intro: eqpoll_sym)+
    1.37  done
    1.38  
    1.39 @@ -436,7 +436,7 @@
    1.40  done
    1.41  
    1.42  lemma (in AC16) unique_superset1: "a \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> MM"
    1.43 -by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]); 
    1.44 +by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) 
    1.45  
    1.46  lemma (in AC16) the_in_MM_subset:
    1.47       "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x Un y"
     2.1 --- a/src/ZF/AC/AC16_lemmas.thy	Wed Jul 10 16:07:52 2002 +0200
     2.2 +++ b/src/ZF/AC/AC16_lemmas.thy	Wed Jul 10 16:54:07 2002 +0200
     2.3 @@ -82,7 +82,7 @@
     2.4  apply (rule subsetI)
     2.5  apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
     2.6  apply (simp, erule bexE) 
     2.7 -apply (rule_tac i=xa and j=x in Ord_linear_le)
     2.8 +apply (rule_tac i=y and j=x in Ord_linear_le)
     2.9  apply (blast dest: le_imp_subset elim: leE ltE)+
    2.10  done
    2.11  
     3.1 --- a/src/ZF/AC/AC17_AC1.thy	Wed Jul 10 16:07:52 2002 +0200
     3.2 +++ b/src/ZF/AC/AC17_AC1.thy	Wed Jul 10 16:54:07 2002 +0200
     3.3 @@ -235,7 +235,7 @@
     3.4  lemma AC3_AC1_lemma:
     3.5       "b\<notin>A ==> (\<Pi>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi>x \<in> A. x)"
     3.6  apply (simp add: id_def cong add: Pi_cong)
     3.7 -apply (rule_tac b = "A" in subst_context, fast)
     3.8 +apply (rule_tac b = A in subst_context, fast)
     3.9  done
    3.10  
    3.11  lemma AC3_AC1: "AC3 ==> AC1"
     4.1 --- a/src/ZF/AC/AC18_AC19.thy	Wed Jul 10 16:07:52 2002 +0200
     4.2 +++ b/src/ZF/AC/AC18_AC19.thy	Wed Jul 10 16:54:07 2002 +0200
     4.3 @@ -89,7 +89,7 @@
     4.4  
     4.5  lemma lemma2: "[| A\<noteq>0; 0\<notin>A |] ==> (\<Inter>x \<in> {uu(a). a \<in> A}. \<Union>b \<in> x. b) \<noteq> 0"
     4.6  apply (erule not_emptyE) 
     4.7 -apply (rule_tac a = "0" in not_emptyI)
     4.8 +apply (rule_tac a = 0 in not_emptyI)
     4.9  apply (fast intro!: lemma2_1)
    4.10  done
    4.11  
     5.1 --- a/src/ZF/AC/Cardinal_aux.thy	Wed Jul 10 16:07:52 2002 +0200
     5.2 +++ b/src/ZF/AC/Cardinal_aux.thy	Wed Jul 10 16:54:07 2002 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4       "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j le i & A \<approx> j"
     5.5  by (blast intro!: lepoll_cardinal_le well_ord_Memrel 
     5.6                    well_ord_cardinal_eqpoll [THEN eqpoll_sym]
     5.7 -          dest: lepoll_well_ord);
     5.8 +          dest: lepoll_well_ord)
     5.9  
    5.10  (* j=|A| *)
    5.11  lemma lesspoll_imp_ex_lt_eqpoll: 
    5.12 @@ -87,7 +87,7 @@
    5.13    above?*)
    5.14  lemma Un_lepoll_Inf_Ord:
    5.15       "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A Un B \<lesssim> i"
    5.16 -apply (rule_tac A1 = "i" and C1 = "i" in ex_eqpoll_disjoint [THEN exE])
    5.17 +apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
    5.18  apply (erule conjE)
    5.19  apply (drule lepoll_trans) 
    5.20  apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
    5.21 @@ -144,7 +144,7 @@
    5.22  lemma UN_fun_lepoll:
    5.23       "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);   
    5.24           ~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a"
    5.25 -by (blast intro: UN_fun_lepoll_lemma); 
    5.26 +by (blast intro: UN_fun_lepoll_lemma) 
    5.27  
    5.28  lemma UN_lepoll:
    5.29       "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);   
    5.30 @@ -164,7 +164,7 @@
    5.31  apply (rule UN_I)
    5.32   apply (rule_tac P = "%z. x \<in> F (z) " in Least_in_Ord, (assumption+))
    5.33  apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify)
    5.34 -apply (erule_tac P = "%z. x \<in> F (z) " and i = "c" in less_LeastE)
    5.35 +apply (erule_tac P = "%z. x \<in> F (z) " and i = c in less_LeastE)
    5.36  apply (blast intro: Ord_Least ltI)
    5.37  done
    5.38  
     6.1 --- a/src/ZF/AC/DC.thy	Wed Jul 10 16:07:52 2002 +0200
     6.2 +++ b/src/ZF/AC/DC.thy	Wed Jul 10 16:54:07 2002 +0200
     6.3 @@ -175,7 +175,7 @@
     6.4  apply (drule bspec [OF _ nat_0I])
     6.5  apply (simp add: XX_def, safe)
     6.6  apply (rule rev_bexI, assumption)
     6.7 -apply (subgoal_tac "0 \<in> x", force)
     6.8 +apply (subgoal_tac "0 \<in> y", force)
     6.9  apply (force simp add: RR_def
    6.10  	     intro: ltD elim!: nat_0_le [THEN leE])
    6.11  (** LEVEL 7, other subgoal **)
    6.12 @@ -186,7 +186,7 @@
    6.13  apply safe
    6.14  apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans], 
    6.15         assumption)
    6.16 -apply (frule_tac a="xa" in domain_of_fun [symmetric, THEN trans], 
    6.17 +apply (frule_tac a=y in domain_of_fun [symmetric, THEN trans], 
    6.18         assumption)
    6.19  apply (fast elim!: nat_into_Ord [THEN succ_in_succ] 
    6.20              dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]])
    6.21 @@ -208,7 +208,7 @@
    6.22    apply (simp add: RR_def)
    6.23   apply (drule lemma2, assumption+)
    6.24   apply (fast dest!: domain_of_fun)
    6.25 -apply (drule_tac x = "xa" in bspec, assumption)
    6.26 +apply (drule_tac x = xa in bspec, assumption)
    6.27  apply (erule sym [THEN trans, symmetric])
    6.28  apply (rule restrict_eq_imp_val_eq [symmetric])
    6.29   apply (drule bspec [OF _ nat_succI], assumption)
    6.30 @@ -392,7 +392,7 @@
    6.31  apply (unfold RR_def allRR_def)
    6.32  apply (rule oallI, drule ltD)
    6.33  apply (erule nat_induct)
    6.34 -apply (drule_tac x="0" in ospec, blast intro: Limit_has_0) 
    6.35 +apply (drule_tac x=0 in ospec, blast intro: Limit_has_0) 
    6.36  apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) 
    6.37  (*induction step*) (** LEVEL 5 **)
    6.38  (*prevent simplification of ~\<exists> to \<forall>~ *)
    6.39 @@ -409,7 +409,8 @@
    6.40  apply (frule f_n_type)
    6.41  apply (simp add: XX_def, assumption+)
    6.42  apply (rule rev_bexI, erule nat_succI)
    6.43 -apply (rule_tac x = "cons (<succ (xa), ya>, f`xa) " in bexI)
    6.44 +apply (rename_tac m i j y z) 
    6.45 +apply (rule_tac x = "cons(<succ(m), z>, f`m)" in bexI)
    6.46  prefer 2 apply (blast intro: cons_fun_type2) 
    6.47  apply (rule conjI)
    6.48  prefer 2 apply (fast del: ballI subsetI
    6.49 @@ -497,7 +498,7 @@
    6.50              intro!: Ord_Hartog leI [THEN le_imp_subset])
    6.51  apply (erule allE impE)+
    6.52  apply (rule Card_Hartog)
    6.53 -apply (erule_tac x = "A" in allE)
    6.54 +apply (erule_tac x = A in allE)
    6.55  apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}" 
    6.56                   in allE)
    6.57  apply simp
     7.1 --- a/src/ZF/AC/HH.thy	Wed Jul 10 16:07:52 2002 +0200
     7.2 +++ b/src/ZF/AC/HH.thy	Wed Jul 10 16:54:07 2002 +0200
     7.3 @@ -88,14 +88,14 @@
     7.4  lemma HH_eq_arg_lt:
     7.5       "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v) \<in> Pow(x)-{0}; v \<in> w |] ==> P"
     7.6  apply (frule_tac P = "%y. y \<in> Pow (x) -{0}" in subst, assumption)
     7.7 -apply (drule_tac a = "w" in HH_subset_x_imp_subset_Diff_UN)
     7.8 +apply (drule_tac a = w in HH_subset_x_imp_subset_Diff_UN)
     7.9  apply (drule subst_elem, assumption)
    7.10  apply (fast intro!: singleton_iff [THEN iffD2] equals0I)
    7.11  done
    7.12  
    7.13  lemma HH_eq_imp_arg_eq:
    7.14    "[| HH(f,x,v)=HH(f,x,w); HH(f,x,w) \<in> Pow(x)-{0}; Ord(v); Ord(w) |] ==> v=w"
    7.15 -apply (rule_tac j = "w" in Ord_linear_lt)
    7.16 +apply (rule_tac j = w in Ord_linear_lt)
    7.17  apply (simp_all (no_asm_simp))
    7.18   apply (drule subst_elem, assumption) 
    7.19   apply (blast dest: ltD HH_eq_arg_lt)
     8.1 --- a/src/ZF/AC/Hartog.thy	Wed Jul 10 16:07:52 2002 +0200
     8.2 +++ b/src/ZF/AC/Hartog.thy	Wed Jul 10 16:54:07 2002 +0200
     8.3 @@ -74,7 +74,7 @@
     8.4  
     8.5  lemma less_HartogE: "[| i < Hartog(A); i \<approx> Hartog(A) |] ==> P"
     8.6  by (blast intro: less_HartogE1 eqpoll_sym eqpoll_imp_lepoll 
     8.7 -                 lepoll_trans [THEN Hartog_lepoll_selfE]);
     8.8 +                 lepoll_trans [THEN Hartog_lepoll_selfE])
     8.9  
    8.10  lemma Card_Hartog: "Card(Hartog(A))"
    8.11  by (fast intro!: CardI Ord_Hartog elim: less_HartogE)
     9.1 --- a/src/ZF/AC/WO1_WO7.thy	Wed Jul 10 16:07:52 2002 +0200
     9.2 +++ b/src/ZF/AC/WO1_WO7.thy	Wed Jul 10 16:54:07 2002 +0200
     9.3 @@ -52,7 +52,7 @@
     9.4  apply (unfold wf_on_def wf_def)
     9.5  apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
     9.6  apply (rule notI)
     9.7 -apply (erule_tac x = "nat" in allE, blast)
     9.8 +apply (erule_tac x = nat in allE, blast)
     9.9  done
    9.10  
    9.11  lemma converse_Memrel_not_well_ord: 
    10.1 --- a/src/ZF/AC/WO2_AC16.thy	Wed Jul 10 16:07:52 2002 +0200
    10.2 +++ b/src/ZF/AC/WO2_AC16.thy	Wed Jul 10 16:54:07 2002 +0200
    10.3 @@ -45,7 +45,7 @@
    10.4  
    10.5  lemma recfunAC16_Limit: "Limit(i)   
    10.6          ==> recfunAC16(f,h,i,a) = (\<Union>j<i. recfunAC16(f,h,j,a))"
    10.7 -by (simp add: recfunAC16_def transrec2_Limit);
    10.8 +by (simp add: recfunAC16_def transrec2_Limit)
    10.9  
   10.10  (* ********************************************************************** *)
   10.11  (* Monotonicity of transrec2                                              *)
   10.12 @@ -135,7 +135,7 @@
   10.13  apply (rule impI)
   10.14  apply (erule disjE)
   10.15  apply (frule ospec, erule Limit_has_succ, assumption) 
   10.16 -apply (drule_tac A = "a" and x = "xa" in ospec, assumption)
   10.17 +apply (drule_tac A = a and x = xa in ospec, assumption)
   10.18  apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord) 
   10.19  apply (blast intro: lemma3 Limit_has_succ) 
   10.20  apply (blast intro: lemma3) 
   10.21 @@ -234,7 +234,7 @@
   10.22  lemma in_Least_Diff:
   10.23       "[| z \<in> F(x); Ord(x) |]   
   10.24        ==> z \<in> F(LEAST i. z \<in> F(i)) - (\<Union>j<(LEAST i. z \<in> F(i)). F(j))"
   10.25 -by (fast elim: less_LeastE elim!: LeastI);
   10.26 +by (fast elim: less_LeastE elim!: LeastI)
   10.27  
   10.28  lemma Least_eq_imp_ex:
   10.29       "[| (LEAST i. w \<in> F(i)) = (LEAST i. z \<in> F(i));   
   10.30 @@ -291,7 +291,7 @@
   10.31           A\<approx>a;  y<a;  ~Finite(a);  Card(a);  n \<in> nat |]   
   10.32        ==> Union(recfunAC16(f,g,y,a))\<prec>a"
   10.33  apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
   10.34 -apply (rule_tac T="A" in Union_lesspoll, simp_all)
   10.35 +apply (rule_tac T=A in Union_lesspoll, simp_all)
   10.36  apply (blast intro!: eqpoll_imp_lepoll)
   10.37  apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel]
   10.38                      well_ord_rvimage)
   10.39 @@ -334,7 +334,7 @@
   10.40  lemma lemma6:
   10.41       "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) --> Q(x,y)); succ(j)<a |]
   10.42        ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) --> Q(x,j))"
   10.43 -by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]); 
   10.44 +by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 
   10.45  
   10.46  
   10.47  lemma lemma7:
   10.48 @@ -539,7 +539,7 @@
   10.49  prefer 2 
   10.50  apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
   10.51  (** LEVEL 20 **)
   10.52 -apply (drule_tac x1="aa" in spec [THEN mp], assumption)
   10.53 +apply (drule_tac x1=aa in spec [THEN mp], assumption)
   10.54  apply (frule succ_leE)
   10.55  apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
   10.56  done
    11.1 --- a/src/ZF/AC/WO6_WO1.thy	Wed Jul 10 16:07:52 2002 +0200
    11.2 +++ b/src/ZF/AC/WO6_WO1.thy	Wed Jul 10 16:54:07 2002 +0200
    11.3 @@ -86,7 +86,7 @@
    11.4  lemma WO1_WO4: "WO1 ==> WO4(1)"
    11.5  apply (unfold WO1_def WO4_def)
    11.6  apply (rule allI)
    11.7 -apply (erule_tac x = "A" in allE)
    11.8 +apply (erule_tac x = A in allE)
    11.9  apply (erule exE)
   11.10  apply (intro exI conjI)
   11.11  apply (erule Ord_ordertype)
   11.12 @@ -124,7 +124,7 @@
   11.13  lemma lt_oadd_odiff_disj:
   11.14        "[| k < i++j;  Ord(i);  Ord(j) |] 
   11.15         ==> k < i  |  (~ k<i & k = i ++ (k--i) & (k--i)<j)"
   11.16 -apply (rule_tac i = "k" and j = "i" in Ord_linear2)
   11.17 +apply (rule_tac i = k and j = i in Ord_linear2)
   11.18  prefer 4 
   11.19     apply (drule odiff_lt_mono2, assumption)
   11.20     apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)
   11.21 @@ -467,7 +467,7 @@
   11.22  lemma NN_imp_ex_inj: "1 \<in> NN(y) ==> \<exists>a f. Ord(a) & f \<in> inj(y, a)"
   11.23  apply (unfold NN_def)
   11.24  apply (elim CollectE exE conjE)
   11.25 -apply (rule_tac x = "a" in exI)
   11.26 +apply (rule_tac x = a in exI)
   11.27  apply (rule_tac x = "\<lambda>x \<in> y. LEAST i. f`i = {x}" in exI)
   11.28  apply (rule conjI, assumption)
   11.29  apply (rule_tac d = "%i. THE x. x \<in> f`i" in lam_injective)
   11.30 @@ -519,7 +519,7 @@
   11.31  apply (rule allI)
   11.32  apply (case_tac "A=0")
   11.33  apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
   11.34 -apply (rule_tac x1 = "A" in lemma_iv [THEN revcut_rl])
   11.35 +apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl])
   11.36  apply (erule exE)
   11.37  apply (drule WO6_imp_NN_not_empty)
   11.38  apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
    12.1 --- a/src/ZF/Coind/ECR.thy	Wed Jul 10 16:07:52 2002 +0200
    12.2 +++ b/src/ZF/Coind/ECR.thy	Wed Jul 10 16:54:07 2002 +0200
    12.3 @@ -40,8 +40,7 @@
    12.4           {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
    12.5             Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]     
    12.6        ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
    12.7 -apply (rule singletonI [THEN HasTyRel.coinduct])
    12.8 -apply auto
    12.9 +apply (rule singletonI [THEN HasTyRel.coinduct], auto)
   12.10  done
   12.11  
   12.12  (* Specialised elimination rules *)
   12.13 @@ -101,15 +100,13 @@
   12.14        hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>        
   12.15     <cl,t> \<in> HasTyRel"
   12.16  apply (unfold hastyenv_def)
   12.17 -apply (erule elab_fixE)
   12.18 -apply safe
   12.19 +apply (erule elab_fixE, safe)
   12.20  apply (rule subst, assumption) 
   12.21  apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
   12.22  apply simp_all
   12.23  apply (blast intro: ve_owrI) 
   12.24  apply (rule ElabRel.fnI)
   12.25 -apply (simp_all add: ValNEE)
   12.26 -apply force
   12.27 +apply (simp_all add: ValNEE, force)
   12.28  done
   12.29  
   12.30  
   12.31 @@ -143,16 +140,13 @@
   12.32  apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
   12.33  apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
   12.34  apply (erule htr_closE)
   12.35 -apply (erule elab_fnE)
   12.36 -apply simp
   12.37 +apply (erule elab_fnE, simp)
   12.38  apply clarify
   12.39  apply (drule spec [THEN spec, THEN mp, THEN mp])
   12.40  prefer 2 apply assumption+
   12.41 -apply (rule hastyenv_owr)
   12.42 -apply assumption
   12.43 +apply (rule hastyenv_owr, assumption)
   12.44  apply assumption 
   12.45 -apply (simp add: hastyenv_def)
   12.46 -apply blast+
   12.47 +apply (simp add: hastyenv_def, blast+)
   12.48  done
   12.49  
   12.50  lemma consistency [rule_format]:
    13.1 --- a/src/ZF/Coind/Map.thy	Wed Jul 10 16:07:52 2002 +0200
    13.2 +++ b/src/ZF/Coind/Map.thy	Wed Jul 10 16:54:07 2002 +0200
    13.3 @@ -105,10 +105,8 @@
    13.4  
    13.5  lemma pmap_owrI: 
    13.6    "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |]  ==> map_owr(m,a,b):PMap(A,B)"
    13.7 -apply (unfold map_owr_def PMap_def TMap_def)
    13.8 -apply safe
    13.9 -apply (simp_all add: if_iff)
   13.10 -apply auto
   13.11 +apply (unfold map_owr_def PMap_def TMap_def, safe)
   13.12 +apply (simp_all add: if_iff, auto)
   13.13  (*Remaining subgoal*)
   13.14  apply (rule excluded_middle [THEN disjE])
   13.15  apply (erule image_Sigma1)
   13.16 @@ -130,8 +128,7 @@
   13.17    "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
   13.18  apply (unfold PMap_def)
   13.19  apply (frule tmap_app_notempty, assumption)
   13.20 -apply (drule tmap_appI)
   13.21 -apply auto
   13.22 +apply (drule tmap_appI, auto)
   13.23  done
   13.24  
   13.25  (** domain **)
    14.1 --- a/src/ZF/Coind/Types.thy	Wed Jul 10 16:07:52 2002 +0200
    14.2 +++ b/src/ZF/Coind/Types.thy	Wed Jul 10 16:54:07 2002 +0200
    14.3 @@ -54,8 +54,7 @@
    14.4  lemma te_appI:
    14.5       "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
    14.6  apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
    14.7 -apply (erule TyEnv.induct)
    14.8 -apply auto
    14.9 +apply (erule TyEnv.induct, auto)
   14.10  done
   14.11  
   14.12  
    15.1 --- a/src/ZF/Coind/Values.thy	Wed Jul 10 16:07:52 2002 +0200
    15.2 +++ b/src/ZF/Coind/Values.thy	Wed Jul 10 16:54:07 2002 +0200
    15.3 @@ -42,8 +42,7 @@
    15.4  
    15.5  lemma ValEnvE:
    15.6    "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
    15.7 -apply (unfold Part_def Val_def ValEnv_def)
    15.8 -apply (clarify ); 
    15.9 +apply (unfold Part_def Val_def ValEnv_def, clarify) 
   15.10  apply (erule Val_ValEnv.cases) 
   15.11  apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
   15.12  done
   15.13 @@ -55,26 +54,22 @@
   15.14          [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q  
   15.15     |] ==>  
   15.16     Q"
   15.17 -apply (unfold Part_def Val_def ValEnv_def)
   15.18 -apply (clarify ); 
   15.19 +apply (unfold Part_def Val_def ValEnv_def, clarify) 
   15.20  apply (erule Val_ValEnv.cases) 
   15.21 -apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs);
   15.22 +apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs)
   15.23  done
   15.24  
   15.25  (* Nonempty sets *)
   15.26  
   15.27  lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
   15.28 -apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
   15.29 -apply blast
   15.30 -done
   15.31 +by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast)
   15.32  
   15.33  declare v_closNE [THEN notE, elim!]
   15.34  
   15.35  
   15.36  lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
   15.37  apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
   15.38 -apply (drule constNEE)
   15.39 -apply auto
   15.40 +apply (drule constNEE, auto)
   15.41  done
   15.42  
   15.43  
   15.44 @@ -102,8 +97,7 @@
   15.45  by (erule ValEnvE, simp add: pmap_appI) 
   15.46  
   15.47  lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
   15.48 -apply (erule ValEnvE)
   15.49 -apply (simp ); 
   15.50 +apply (erule ValEnvE, simp) 
   15.51  apply (blast dest: pmap_domainD)
   15.52  done
   15.53  
   15.54 @@ -115,8 +109,7 @@
   15.55  
   15.56  lemma ve_owrI:
   15.57       "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
   15.58 -apply (erule ValEnvE)
   15.59 -apply simp
   15.60 +apply (erule ValEnvE, simp)
   15.61  apply (blast intro: pmap_owrI Val_ValEnv.intros)
   15.62  done
   15.63  
    16.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 10 16:07:52 2002 +0200
    16.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 10 16:54:07 2002 +0200
    16.3 @@ -39,7 +39,7 @@
    16.4       "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)"
    16.5  apply (simp add: UN_subset_iff)
    16.6  apply (rule ballI)  
    16.7 -apply (induct_tac x, simp_all) 
    16.8 +apply (induct_tac n, simp_all) 
    16.9  apply (rule subset_trans [of _ "h(lfp(D,h))"])
   16.10   apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )  
   16.11  apply (erule lfp_lemma2) 
    17.1 --- a/src/ZF/Constructible/Formula.thy	Wed Jul 10 16:07:52 2002 +0200
    17.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Jul 10 16:54:07 2002 +0200
    17.3 @@ -441,7 +441,7 @@
    17.4  
    17.5  lemma empty_in_DPow: "0 \<in> DPow(A)"
    17.6  apply (simp add: DPow_def)
    17.7 -apply (rule_tac x="Nil" in bexI) 
    17.8 +apply (rule_tac x=Nil in bexI) 
    17.9   apply (rule_tac x="Neg(Equal(0,0))" in bexI) 
   17.10    apply (auto simp add: Un_least_lt_iff) 
   17.11  done
   17.12 @@ -729,7 +729,7 @@
   17.13  text{*The subset consisting of the ordinals is definable.*}
   17.14  lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
   17.15  apply (simp add: DPow_def Collect_subset) 
   17.16 -apply (rule_tac x="Nil" in bexI) 
   17.17 +apply (rule_tac x=Nil in bexI) 
   17.18   apply (rule_tac x="ordinal_fm(0)" in bexI) 
   17.19  apply (simp_all add: sats_ordinal_fm)
   17.20  done 
   17.21 @@ -927,7 +927,7 @@
   17.22  text{*Kunen's VI, 1.10 *}
   17.23  lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
   17.24  apply (simp add: Lset_succ DPow_def) 
   17.25 -apply (rule_tac x="Nil" in bexI) 
   17.26 +apply (rule_tac x=Nil in bexI) 
   17.27   apply (rule_tac x="Equal(0,0)" in bexI) 
   17.28  apply auto 
   17.29  done
   17.30 @@ -998,7 +998,7 @@
   17.31  apply (rule LsetI [OF succI1])
   17.32  apply (simp add: DPow_def) 
   17.33  apply (intro conjI, clarify) 
   17.34 -apply (rule_tac a="x" in UN_I, simp+)  
   17.35 +apply (rule_tac a=x in UN_I, simp+)  
   17.36  txt{*Now to create the formula @{term "y \<subseteq> X"} *}
   17.37  apply (rule_tac x="Cons(X,Nil)" in bexI) 
   17.38   apply (rule_tac x="subset_fm(0,1)" in bexI) 
    18.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 10 16:07:52 2002 +0200
    18.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 10 16:54:07 2002 +0200
    18.3 @@ -1,9 +1,8 @@
    18.4 -header {*The Class L Satisfies the ZF Axioms*}
    18.5 +header {*The ZF Axioms (Except Separation) in L*}
    18.6  
    18.7  theory L_axioms = Formula + Relative + Reflection + MetaExists:
    18.8  
    18.9 -
   18.10 -text {* The class L satisfies the premises of locale @{text M_axioms} *}
   18.11 +text {* The class L satisfies the premises of locale @{text M_triv_axioms} *}
   18.12  
   18.13  lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
   18.14  apply (insert Transset_Lset) 
   18.15 @@ -47,7 +46,7 @@
   18.16         in exI)
   18.17  apply simp
   18.18  apply clarify 
   18.19 -apply (rule_tac a="x" in UN_I)  
   18.20 +apply (rule_tac a=x in UN_I)  
   18.21   apply (simp_all add: Replace_iff univalent_def) 
   18.22  apply (blast dest: transL L_I) 
   18.23  done
   18.24 @@ -316,7 +315,7 @@
   18.25  by blast
   18.26  
   18.27  
   18.28 -subsection{*Internalized formulas for some relativized ones*}
   18.29 +subsection{*Internalized Formulas for some Set-Theoretic Concepts*}
   18.30  
   18.31  lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex
   18.32  
   18.33 @@ -341,7 +340,7 @@
   18.34     "9"  == "succ(8)"
   18.35  
   18.36  
   18.37 -subsubsection{*The Empty Set*}
   18.38 +subsubsection{*The Empty Set, Internalized*}
   18.39  
   18.40  constdefs empty_fm :: "i=>i"
   18.41      "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
   18.42 @@ -373,7 +372,7 @@
   18.43  done
   18.44  
   18.45  
   18.46 -subsubsection{*Unordered pairs*}
   18.47 +subsubsection{*Unordered Pairs, Internalized*}
   18.48  
   18.49  constdefs upair_fm :: "[i,i,i]=>i"
   18.50      "upair_fm(x,y,z) == 
   18.51 @@ -420,7 +419,7 @@
   18.52  apply (intro FOL_reflections)  
   18.53  done
   18.54  
   18.55 -subsubsection{*Ordered pairs*}
   18.56 +subsubsection{*Ordered pairs, Internalized*}
   18.57  
   18.58  constdefs pair_fm :: "[i,i,i]=>i"
   18.59      "pair_fm(x,y,z) == 
   18.60 @@ -457,7 +456,7 @@
   18.61  done
   18.62  
   18.63  
   18.64 -subsubsection{*Binary Unions*}
   18.65 +subsubsection{*Binary Unions, Internalized*}
   18.66  
   18.67  constdefs union_fm :: "[i,i,i]=>i"
   18.68      "union_fm(x,y,z) == 
   18.69 @@ -493,7 +492,7 @@
   18.70  done
   18.71  
   18.72  
   18.73 -subsubsection{*`Cons' for sets*}
   18.74 +subsubsection{*Set ``Cons,'' Internalized*}
   18.75  
   18.76  constdefs cons_fm :: "[i,i,i]=>i"
   18.77      "cons_fm(x,y,z) == 
   18.78 @@ -530,7 +529,7 @@
   18.79  done
   18.80  
   18.81  
   18.82 -subsubsection{*Successor Function*}
   18.83 +subsubsection{*Successor Function, Internalized*}
   18.84  
   18.85  constdefs succ_fm :: "[i,i]=>i"
   18.86      "succ_fm(x,y) == cons_fm(x,x,y)"
   18.87 @@ -564,7 +563,7 @@
   18.88  done
   18.89  
   18.90  
   18.91 -subsubsection{*Function Applications*}
   18.92 +subsubsection{*Function Application, Internalized*}
   18.93  
   18.94  constdefs fun_apply_fm :: "[i,i,i]=>i"
   18.95      "fun_apply_fm(f,x,y) == 
   18.96 @@ -647,7 +646,7 @@
   18.97  done
   18.98  
   18.99  
  18.100 -subsubsection{*Membership Relation*}
  18.101 +subsubsection{*Membership Relation, Internalized*}
  18.102  
  18.103  constdefs Memrel_fm :: "[i,i]=>i"
  18.104      "Memrel_fm(A,r) == 
  18.105 @@ -685,7 +684,7 @@
  18.106  apply (intro FOL_reflections pair_reflection)  
  18.107  done
  18.108  
  18.109 -subsubsection{*Predecessor Set*}
  18.110 +subsubsection{*Predecessor Set, Internalized*}
  18.111  
  18.112  constdefs pred_set_fm :: "[i,i,i,i]=>i"
  18.113      "pred_set_fm(A,x,r,B) == 
  18.114 @@ -726,7 +725,7 @@
  18.115  
  18.116  
  18.117  
  18.118 -subsubsection{*Domain*}
  18.119 +subsubsection{*Domain of a Relation, Internalized*}
  18.120  
  18.121  (* "is_domain(M,r,z) == 
  18.122  	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
  18.123 @@ -765,7 +764,7 @@
  18.124  done
  18.125  
  18.126  
  18.127 -subsubsection{*Range*}
  18.128 +subsubsection{*Range of a Relation, Internalized*}
  18.129  
  18.130  (* "is_range(M,r,z) == 
  18.131  	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
  18.132 @@ -804,7 +803,7 @@
  18.133  done
  18.134  
  18.135   
  18.136 -subsubsection{*Field*}
  18.137 +subsubsection{*Field of a Relation, Internalized*}
  18.138  
  18.139  (* "is_field(M,r,z) == 
  18.140  	\<exists>dr[M]. is_domain(M,r,dr) & 
  18.141 @@ -845,7 +844,7 @@
  18.142  done
  18.143  
  18.144  
  18.145 -subsubsection{*Image*}
  18.146 +subsubsection{*Image under a Relation, Internalized*}
  18.147  
  18.148  (* "image(M,r,A,z) == 
  18.149          \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
  18.150 @@ -885,7 +884,7 @@
  18.151  done
  18.152  
  18.153  
  18.154 -subsubsection{*The Concept of Relation*}
  18.155 +subsubsection{*The Concept of Relation, Internalized*}
  18.156  
  18.157  (* "is_relation(M,r) == 
  18.158          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
  18.159 @@ -920,7 +919,7 @@
  18.160  done
  18.161  
  18.162  
  18.163 -subsubsection{*The Concept of Function*}
  18.164 +subsubsection{*The Concept of Function, Internalized*}
  18.165  
  18.166  (* "is_function(M,r) == 
  18.167  	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
  18.168 @@ -960,7 +959,7 @@
  18.169  done
  18.170  
  18.171  
  18.172 -subsubsection{*Typed Functions*}
  18.173 +subsubsection{*Typed Functions, Internalized*}
  18.174  
  18.175  (* "typed_function(M,A,B,r) == 
  18.176          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
  18.177 @@ -1021,7 +1020,7 @@
  18.178  done
  18.179  
  18.180  
  18.181 -subsubsection{*Composition of Relations*}
  18.182 +subsubsection{*Composition of Relations, Internalized*}
  18.183  
  18.184  (* "composition(M,r,s,t) == 
  18.185          \<forall>p[M]. p \<in> t <-> 
  18.186 @@ -1066,7 +1065,7 @@
  18.187  done
  18.188  
  18.189  
  18.190 -subsubsection{*Injections*}
  18.191 +subsubsection{*Injections, Internalized*}
  18.192  
  18.193  (* "injection(M,A,B,f) == 
  18.194  	typed_function(M,A,B,f) &
  18.195 @@ -1111,7 +1110,7 @@
  18.196  done
  18.197  
  18.198  
  18.199 -subsubsection{*Surjections*}
  18.200 +subsubsection{*Surjections, Internalized*}
  18.201  
  18.202  (*  surjection :: "[i=>o,i,i,i] => o"
  18.203      "surjection(M,A,B,f) == 
  18.204 @@ -1154,7 +1153,7 @@
  18.205  
  18.206  
  18.207  
  18.208 -subsubsection{*Bijections*}
  18.209 +subsubsection{*Bijections, Internalized*}
  18.210  
  18.211  (*   bijection :: "[i=>o,i,i,i] => o"
  18.212      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
  18.213 @@ -1190,7 +1189,7 @@
  18.214  done
  18.215  
  18.216  
  18.217 -subsubsection{*Order-Isomorphisms*}
  18.218 +subsubsection{*Order-Isomorphisms, Internalized*}
  18.219  
  18.220  (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
  18.221     "order_isomorphism(M,A,r,B,s,f) == 
  18.222 @@ -1246,7 +1245,7 @@
  18.223  apply (intro FOL_reflections function_reflections bijection_reflection)  
  18.224  done
  18.225  
  18.226 -subsubsection{*Limit Ordinals*}
  18.227 +subsubsection{*Limit Ordinals, Internalized*}
  18.228  
  18.229  text{*A limit ordinal is a non-empty, successor-closed ordinal*}
  18.230  
    19.1 --- a/src/ZF/Constructible/ROOT.ML	Wed Jul 10 16:07:52 2002 +0200
    19.2 +++ b/src/ZF/Constructible/ROOT.ML	Wed Jul 10 16:54:07 2002 +0200
    19.3 @@ -10,5 +10,5 @@
    19.4  
    19.5  use_thy "Reflection";
    19.6  use_thy "WF_absolute";
    19.7 -use_thy "Separation";
    19.8 +use_thy "Rec_Separation";
    19.9  use_thy "Datatype_absolute";
    20.1 --- a/src/ZF/Constructible/Relative.thy	Wed Jul 10 16:07:52 2002 +0200
    20.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jul 10 16:54:07 2002 +0200
    20.3 @@ -227,18 +227,20 @@
    20.4  
    20.5  text{*Congruence rule for separation: can assume the variable is in @{text M}*}
    20.6  lemma separation_cong [cong]:
    20.7 -     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
    20.8 +     "(!!x. M(x) ==> P(x) <-> P'(x)) 
    20.9 +      ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   20.10  by (simp add: separation_def) 
   20.11  
   20.12  text{*Congruence rules for replacement*}
   20.13  lemma univalent_cong [cong]:
   20.14       "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   20.15 -      ==> univalent(M,A,P) <-> univalent(M,A',P')"
   20.16 +      ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   20.17  by (simp add: univalent_def) 
   20.18  
   20.19  lemma strong_replacement_cong [cong]:
   20.20       "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   20.21 -      ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
   20.22 +      ==> strong_replacement(M, %x y. P(x,y)) <-> 
   20.23 +          strong_replacement(M, %x y. P'(x,y))" 
   20.24  by (simp add: strong_replacement_def) 
   20.25  
   20.26  text{*The extensionality axiom*}
   20.27 @@ -268,7 +270,7 @@
   20.28  
   20.29  lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   20.30  apply (simp add: separation_def, clarify) 
   20.31 -apply (rule_tac x = "Collect(x,P)" in bexI) 
   20.32 +apply (rule_tac x = "Collect(z,P)" in bexI) 
   20.33  apply (blast intro: Collect_in_univ Transset_0)+
   20.34  done
   20.35  
    21.1 --- a/src/ZF/Constructible/Separation.thy	Wed Jul 10 16:07:52 2002 +0200
    21.2 +++ b/src/ZF/Constructible/Separation.thy	Wed Jul 10 16:54:07 2002 +0200
    21.3 @@ -1,9 +1,9 @@
    21.4 -header{*Some Instances of Separation and Strong Replacement*}
    21.5 -
    21.6 -(*This theory proves all instances needed for locale M_axioms*)
    21.7 +header{*Early Instances of Separation and Strong Replacement*}
    21.8  
    21.9  theory Separation = L_axioms + WF_absolute:
   21.10  
   21.11 +text{*This theory proves all instances needed for locale @{text "M_axioms"}*}
   21.12 +
   21.13  text{*Helps us solve for de Bruijn indices!*}
   21.14  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
   21.15  by simp
   21.16 @@ -141,7 +141,7 @@
   21.17  apply (rename_tac u) 
   21.18  apply (rule bex_iff_sats) 
   21.19  apply (rule conj_iff_sats)
   21.20 -apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
   21.21 +apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
   21.22  apply (rule sep_rules | simp)+
   21.23  apply (simp_all add: succ_Un_distrib [symmetric])
   21.24  done
   21.25 @@ -166,7 +166,7 @@
   21.26  apply (rename_tac u) 
   21.27  apply (rule bex_iff_sats) 
   21.28  apply (rule conj_iff_sats)
   21.29 -apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
   21.30 +apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
   21.31  apply (rule sep_rules | simp)+
   21.32  apply (simp_all add: succ_Un_distrib [symmetric])
   21.33  done
   21.34 @@ -282,7 +282,7 @@
   21.35  apply (rename_tac u) 
   21.36  apply (rule bex_iff_sats)
   21.37  apply (rule conj_iff_sats)
   21.38 -apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats) 
   21.39 +apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) 
   21.40  apply (rule sep_rules | simp)+
   21.41  apply (simp_all add: succ_Un_distrib [symmetric])
   21.42  done
   21.43 @@ -415,7 +415,7 @@
   21.44  apply (rule DPowI2)
   21.45  apply (rename_tac u) 
   21.46  apply (rule bex_iff_sats conj_iff_sats)+
   21.47 -apply (rule_tac env = "[x,u,A,B,r]" in mem_iff_sats) 
   21.48 +apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) 
   21.49  apply (rule sep_rules | simp)+
   21.50  apply (simp_all add: succ_Un_distrib [symmetric])
   21.51  done
   21.52 @@ -451,7 +451,7 @@
   21.53  apply (rule DPowI2)
   21.54  apply (rename_tac u) 
   21.55  apply (rule bex_iff_sats conj_iff_sats)+
   21.56 -apply (rule_tac env = "[x,u,r,f,g,a,b]" in pair_iff_sats) 
   21.57 +apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) 
   21.58  apply (rule sep_rules | simp)+
   21.59  apply (simp_all add: succ_Un_distrib [symmetric])
   21.60  done
   21.61 @@ -628,88 +628,4 @@
   21.62  declare is_funspace_abs [simp]
   21.63  declare finite_funspace_closed [intro,simp]
   21.64  
   21.65 -
   21.66 -(***NOW FOR THE LOCALE M_TRANCL***)
   21.67 -
   21.68 -subsection{*Separation for Reflexive/Transitive Closure*}
   21.69 -
   21.70 -subsubsection{*First, The Defining Formula*}
   21.71 -
   21.72 -(* "rtran_closure_mem(M,A,r,p) ==
   21.73 -      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
   21.74 -       omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
   21.75 -       (\<exists>f[M]. typed_function(M,n',A,f) &
   21.76 -	(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
   21.77 -	  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
   21.78 -	(\<forall>j[M]. j\<in>n --> 
   21.79 -	  (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M]. 
   21.80 -	    fun_apply(M,f,j,fj) & successor(M,j,sj) &
   21.81 -	    fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
   21.82 -constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
   21.83 - "rtran_closure_mem_fm(A,r,p) == 
   21.84 -   Exists(Exists(Exists(
   21.85 -    And(omega_fm(2),
   21.86 -     And(Member(1,2),
   21.87 -      And(succ_fm(1,0),
   21.88 -       Exists(And(typed_function_fm(1, A#+4, 0),
   21.89 -	And(Exists(Exists(Exists(
   21.90 -	      And(pair_fm(2,1,p#+7), 
   21.91 -	       And(empty_fm(0),
   21.92 -		And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
   21.93 -	    Forall(Implies(Member(0,3),
   21.94 -	     Exists(Exists(Exists(Exists(
   21.95 -	      And(fun_apply_fm(5,4,3),
   21.96 -	       And(succ_fm(4,2),
   21.97 -		And(fun_apply_fm(5,2,1),
   21.98 -		 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
   21.99 -
  21.100 -
  21.101 -lemma rtran_closure_mem_type [TC]:
  21.102 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
  21.103 -by (simp add: rtran_closure_mem_fm_def) 
  21.104 -
  21.105 -lemma arity_rtran_closure_mem_fm [simp]:
  21.106 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
  21.107 -      ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  21.108 -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) 
  21.109 -
  21.110 -lemma sats_rtran_closure_mem_fm [simp]:
  21.111 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  21.112 -    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> 
  21.113 -        rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
  21.114 -by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
  21.115 -
  21.116 -lemma rtran_closure_mem_iff_sats:
  21.117 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
  21.118 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  21.119 -       ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
  21.120 -by (simp add: sats_rtran_closure_mem_fm)
  21.121 -
  21.122 -theorem rtran_closure_mem_reflection:
  21.123 -     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)), 
  21.124 -               \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
  21.125 -apply (simp only: rtran_closure_mem_def setclass_simps)
  21.126 -apply (intro FOL_reflections function_reflections fun_plus_reflections)  
  21.127 -done
  21.128 -
  21.129 -subsubsection{*Then, the Instance of Separation*}
  21.130 -
  21.131 -
  21.132 -text{*This formula describes @{term "rtrancl(r)"}.*}
  21.133 -lemma rtrancl_separation:
  21.134 -     "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
  21.135 -apply (rule separation_CollectI) 
  21.136 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) 
  21.137 -apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
  21.138 -apply (drule subset_Lset_ltD, assumption) 
  21.139 -apply (erule reflection_imp_L_separation)
  21.140 -  apply (simp_all add: lt_Ord2)
  21.141 -apply (rule DPowI2)
  21.142 -apply (rename_tac u)
  21.143 -apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
  21.144 -apply (rule sep_rules | simp)+
  21.145 -apply (simp_all add: succ_Un_distrib [symmetric])
  21.146 -done
  21.147 -
  21.148 -
  21.149  end
    22.1 --- a/src/ZF/Constructible/WF_absolute.thy	Wed Jul 10 16:07:52 2002 +0200
    22.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jul 10 16:54:07 2002 +0200
    22.3 @@ -21,13 +21,13 @@
    22.4  by (subst wfrank_def [THEN def_wfrec], simp_all)
    22.5  
    22.6  lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))"
    22.7 -apply (rule_tac a="a" in wf_induct, assumption)
    22.8 +apply (rule_tac a=a in wf_induct, assumption)
    22.9  apply (subst wfrank, assumption)
   22.10  apply (rule Ord_succ [THEN Ord_UN], blast)
   22.11  done
   22.12  
   22.13  lemma wfrank_lt: "[|wf(r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   22.14 -apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
   22.15 +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption)
   22.16  apply (rule UN_I [THEN ltI])
   22.17  apply (simp add: Ord_wfrank vimage_iff)+
   22.18  done
   22.19 @@ -141,8 +141,7 @@
   22.20              (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
   22.21                             (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
   22.22  apply (simp add: rtran_closure_mem_def typed_apply_abs
   22.23 -                 Ord_succ_mem_iff nat_0_le [THEN ltD])
   22.24 -apply (blast intro: elim:); 
   22.25 +                 Ord_succ_mem_iff nat_0_le [THEN ltD], blast) 
   22.26  done
   22.27  
   22.28  locale M_trancl = M_axioms +
   22.29 @@ -159,7 +158,7 @@
   22.30       "M(r) ==> rtran_closure(M,r,rtrancl(r))"
   22.31  apply (simp add: rtran_closure_def rtran_closure_mem_iff 
   22.32                   rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def)
   22.33 -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
   22.34 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) 
   22.35  done
   22.36  
   22.37  lemma (in M_trancl) rtrancl_closed [intro,simp]:
   22.38 @@ -177,7 +176,7 @@
   22.39  apply (rule M_equalityI)
   22.40  apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
   22.41                   rtrancl_alt_def rtran_closure_mem_iff)
   22.42 -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); 
   22.43 +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) 
   22.44  done
   22.45  
   22.46  lemma (in M_trancl) trancl_closed [intro,simp]:
   22.47 @@ -235,10 +234,10 @@
   22.48  
   22.49  (*NEEDS RELATIVIZATION*)
   22.50  locale M_wfrank = M_trancl +
   22.51 -  assumes wfrank_separation':
   22.52 +  assumes wfrank_separation:
   22.53       "M(r) ==>
   22.54 -	separation
   22.55 -	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   22.56 +      separation (M, \<lambda>x. 
   22.57 +         ~ (\<exists>f[M]. M_is_recfun(M, r^+, x, %mm x f y. y = range(f), f)))"
   22.58   and wfrank_strong_replacement':
   22.59       "M(r) ==>
   22.60        strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
   22.61 @@ -247,7 +246,15 @@
   22.62   and Ord_wfrank_separation:
   22.63       "M(r) ==>
   22.64        separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
   22.65 -                       is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
   22.66 +                       is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))" 
   22.67 +
   22.68 +lemma (in M_wfrank) wfrank_separation':
   22.69 +     "M(r) ==>
   22.70 +      separation
   22.71 +	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   22.72 +apply (insert wfrank_separation [of r])
   22.73 +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
   22.74 +done
   22.75  
   22.76  text{*This function, defined using replacement, is a rank function for
   22.77  well-founded relations within the class M.*}
    23.1 --- a/src/ZF/Constructible/WFrec.thy	Wed Jul 10 16:07:52 2002 +0200
    23.2 +++ b/src/ZF/Constructible/WFrec.thy	Wed Jul 10 16:54:07 2002 +0200
    23.3 @@ -84,8 +84,8 @@
    23.4         wellfounded(M,r);  trans(r);
    23.5         M(f); M(g); M(r); M(x); M(a); M(b) |] 
    23.6       ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
    23.7 -apply (frule_tac f="f" in is_recfun_type) 
    23.8 -apply (frule_tac f="g" in is_recfun_type) 
    23.9 +apply (frule_tac f=f in is_recfun_type) 
   23.10 +apply (frule_tac f=g in is_recfun_type) 
   23.11  apply (simp add: is_recfun_def)
   23.12  apply (erule_tac a=x in wellfounded_induct, assumption+)
   23.13  txt{*Separation to justify the induction*}
   23.14 @@ -107,7 +107,7 @@
   23.15         wellfounded(M,r); trans(r); 
   23.16         M(f); M(g); M(r); <b,a> \<in> r |]   
   23.17        ==> restrict(f, r-``{b}) = g"
   23.18 -apply (frule_tac f="f" in is_recfun_type) 
   23.19 +apply (frule_tac f=f in is_recfun_type) 
   23.20  apply (rule fun_extension) 
   23.21  apply (blast intro: transD restrict_type2) 
   23.22  apply (erule is_recfun_type, simp) 
    24.1 --- a/src/ZF/Constructible/Wellorderings.thy	Wed Jul 10 16:07:52 2002 +0200
    24.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jul 10 16:54:07 2002 +0200
    24.3 @@ -141,13 +141,13 @@
    24.4  lemma (in M_axioms) wf_on_imp_relativized: 
    24.5       "wf[A](r) ==> wellfounded_on(M,A,r)" 
    24.6  apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) 
    24.7 -apply (drule_tac x="x" in spec, blast) 
    24.8 +apply (drule_tac x=x in spec, blast) 
    24.9  done
   24.10  
   24.11  lemma (in M_axioms) wf_imp_relativized: 
   24.12       "wf(r) ==> wellfounded(M,r)" 
   24.13  apply (simp add: wellfounded_def wf_def, clarify) 
   24.14 -apply (drule_tac x="x" in spec, blast) 
   24.15 +apply (drule_tac x=x in spec, blast) 
   24.16  done
   24.17  
   24.18  lemma (in M_axioms) well_ord_imp_relativized: 
   24.19 @@ -480,8 +480,8 @@
   24.20  apply (insert omap_funtype [of A r f B i]) 
   24.21  apply (auto simp add: bij_def inj_def) 
   24.22  prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
   24.23 -apply (frule_tac a="w" in apply_Pair, assumption) 
   24.24 -apply (frule_tac a="x" in apply_Pair, assumption) 
   24.25 +apply (frule_tac a=w in apply_Pair, assumption) 
   24.26 +apply (frule_tac a=x in apply_Pair, assumption) 
   24.27  apply (simp add: omap_iff) 
   24.28  apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
   24.29  done
   24.30 @@ -494,8 +494,8 @@
   24.31  apply (rule ord_isoI)
   24.32   apply (erule wellordered_omap_bij, assumption+) 
   24.33  apply (insert omap_funtype [of A r f B i], simp) 
   24.34 -apply (frule_tac a="x" in apply_Pair, assumption) 
   24.35 -apply (frule_tac a="y" in apply_Pair, assumption) 
   24.36 +apply (frule_tac a=x in apply_Pair, assumption) 
   24.37 +apply (frule_tac a=y in apply_Pair, assumption) 
   24.38  apply (auto simp add: omap_iff)
   24.39   txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
   24.40   apply (blast intro: ltD ord_iso_pred_imp_lt)
    25.1 --- a/src/ZF/Induct/Multiset.ML	Wed Jul 10 16:07:52 2002 +0200
    25.2 +++ b/src/ZF/Induct/Multiset.ML	Wed Jul 10 16:54:07 2002 +0200
    25.3 @@ -831,8 +831,8 @@
    25.4  by (auto_tac (claset(), simpset() addsimps []));
    25.5  by (ALLGOALS(asm_full_simp_tac(simpset() 
    25.6      addsimps [Un_subset_iff, Mult_iff_multiset])));
    25.7 -by (res_inst_tac [("x", "x")] bexI 3);
    25.8 -by (res_inst_tac [("x", "xb")] bexI 3);
    25.9 +by (res_inst_tac [("x", "a")] bexI 3);
   25.10 +by (res_inst_tac [("x", "M0")] bexI 3);
   25.11  by (Asm_simp_tac 3);
   25.12  by (res_inst_tac [("x", "K")] bexI 3);
   25.13  by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset])));
   25.14 @@ -841,8 +841,8 @@
   25.15  
   25.16  Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)";
   25.17  by (auto_tac (claset(), simpset() addsimps []));
   25.18 -by (res_inst_tac [("x", "x")] bexI 1);
   25.19 -by (res_inst_tac [("x", "xb")] bexI 1);
   25.20 +by (res_inst_tac [("x", "a")] bexI 1);
   25.21 +by (res_inst_tac [("x", "M0")] bexI 1);
   25.22  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
   25.23  by (res_inst_tac [("x", "K")] bexI 1);
   25.24  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
    26.1 --- a/src/ZF/Induct/Primrec.thy	Wed Jul 10 16:07:52 2002 +0200
    26.2 +++ b/src/ZF/Induct/Primrec.thy	Wed Jul 10 16:54:07 2002 +0200
    26.3 @@ -214,7 +214,7 @@
    26.4    "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
    26.5      ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
    26.6    -- {* PROPERTY A 11 *}
    26.7 -  apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans)
    26.8 +  apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans)
    26.9     apply (simp add: ack_2)
   26.10     apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
   26.11        apply (rule add_le_mono [THEN leI, THEN leI])
   26.12 @@ -265,7 +265,7 @@
   26.13     apply (simp add: nat_0_le)
   26.14    apply simp
   26.15    apply (rule ballI)
   26.16 -  apply (erule_tac n = "x" in natE)
   26.17 +  apply (erule_tac n = i in natE)
   26.18     apply (simp add: add_le_self)
   26.19    apply simp
   26.20    apply (erule bspec [THEN lt_trans2])
    27.1 --- a/src/ZF/Integ/IntDiv.ML	Wed Jul 10 16:07:52 2002 +0200
    27.2 +++ b/src/ZF/Integ/IntDiv.ML	Wed Jul 10 16:54:07 2002 +0200
    27.3 @@ -61,7 +61,7 @@
    27.4  by (dtac zero_zless_imp_znegative_zminus 1);
    27.5  by (dtac zneg_int_of 2);
    27.6  by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation]));  
    27.7 -by (subgoal_tac "0 < zmagnitude($# succ(x))" 1);
    27.8 +by (subgoal_tac "0 < zmagnitude($# succ(n))" 1);
    27.9  by (Asm_full_simp_tac 1);
   27.10  by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1);
   27.11  by (Asm_full_simp_tac 1); 
   27.12 @@ -79,9 +79,9 @@
   27.13  by (cut_inst_tac [("m","m")] int_succ_int_1 1);
   27.14  by (cut_inst_tac [("m","n")] int_succ_int_1 1);
   27.15  by (Asm_full_simp_tac 1);
   27.16 -by (eres_inst_tac [("n","x")] natE 1);
   27.17 +by (etac natE 1);
   27.18  by Auto_tac;
   27.19 -by (res_inst_tac [("x","succ(x)")] bexI 1);
   27.20 +by (res_inst_tac [("x","succ(n)")] bexI 1);
   27.21  by Auto_tac;  
   27.22  qed "zless_add_succ_iff";
   27.23  
    28.1 --- a/src/ZF/IsaMakefile	Wed Jul 10 16:07:52 2002 +0200
    28.2 +++ b/src/ZF/IsaMakefile	Wed Jul 10 16:54:07 2002 +0200
    28.3 @@ -82,7 +82,8 @@
    28.4    Constructible/Formula.thy     Constructible/Relative.thy \
    28.5    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
    28.6    Constructible/MetaExists.thy  Constructible/Normal.thy \
    28.7 -  Constructible/Separation.thy      Constructible/WF_absolute.thy \
    28.8 +  Constructible/Rec_Separation.thy Constructible/Separation.thy \
    28.9 +  Constructible/WF_absolute.thy \
   28.10    Constructible/Reflection.thy  Constructible/WFrec.thy \
   28.11    Constructible/document/root.tex
   28.12  	@$(ISATOOL) usedir $(OUT)/ZF Constructible
    29.1 --- a/src/ZF/List.thy	Wed Jul 10 16:07:52 2002 +0200
    29.2 +++ b/src/ZF/List.thy	Wed Jul 10 16:54:07 2002 +0200
    29.3 @@ -597,7 +597,7 @@
    29.4   apply simp_all
    29.5  txt{*Inductive step*}  
    29.6  apply clarify 
    29.7 -apply (erule_tac a = xa in list.cases, simp_all)  
    29.8 +apply (erule_tac a=ys in list.cases, simp_all)  
    29.9  done
   29.10  
   29.11  
   29.12 @@ -761,8 +761,8 @@
   29.13  apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
   29.14  apply clarify
   29.15  (*Both lists are non-empty*)
   29.16 -apply (erule_tac a="xa" in list.cases, simp) 
   29.17 -apply (erule_tac a="xb" in list.cases, clarify) 
   29.18 +apply (erule_tac a="xs" in list.cases, simp) 
   29.19 +apply (erule_tac a="ys" in list.cases, clarify) 
   29.20  apply (simp (no_asm_use) )
   29.21  apply clarify
   29.22  apply (simp (no_asm_simp))
   29.23 @@ -847,7 +847,7 @@
   29.24  apply (induct_tac xs) 
   29.25   apply simp_all 
   29.26   apply (blast intro: list_mono [THEN subsetD], clarify) 
   29.27 -apply (erule_tac a=x in list.cases , auto) 
   29.28 +apply (erule_tac a=ys in list.cases , auto) 
   29.29  apply (blast intro: list_mono [THEN subsetD]) 
   29.30  done
   29.31  
   29.32 @@ -875,7 +875,7 @@
   29.33  apply (unfold min_def)
   29.34  apply (induct_tac "xs", simp_all) 
   29.35  apply clarify 
   29.36 -apply (erule_tac a = "x" in list.cases, auto)
   29.37 +apply (erule_tac a = ys in list.cases, auto)
   29.38  done
   29.39  
   29.40  lemma zip_append1 [rule_format]:
   29.41 @@ -1011,13 +1011,13 @@
   29.42                                            list_update(ys, i, snd(xy)))"
   29.43  apply (induct_tac "ys")
   29.44   apply auto
   29.45 -apply (erule_tac a = "xc" in list.cases)
   29.46 +apply (erule_tac a = "xs" in list.cases)
   29.47  apply (auto elim: natE)
   29.48  done
   29.49  
   29.50  lemma set_update_subset_cons [rule_format]:
   29.51 -     "xs:list(A) ==> \<forall>i \<in> nat. set_of_list(list_update(xs, i, x))
   29.52 -   <= cons(x, set_of_list(xs))"
   29.53 +  "xs:list(A) ==> 
   29.54 +   \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
   29.55  apply (induct_tac "xs")
   29.56   apply simp
   29.57  apply (rule ballI)
   29.58 @@ -1121,13 +1121,13 @@
   29.59  apply simp 
   29.60  apply (subst map_succ_upt [symmetric], simp_all)
   29.61  apply clarify 
   29.62 -apply (subgoal_tac "xa < length (upt (0, x))")
   29.63 +apply (subgoal_tac "i < length (upt (0, x))")
   29.64   prefer 2 
   29.65   apply (simp add: less_diff_conv) 
   29.66 - apply (rule_tac j = "succ (xa #+ y) " in lt_trans2)
   29.67 + apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
   29.68    apply simp 
   29.69   apply simp 
   29.70 -apply (subgoal_tac "xa < length (upt (y, x))")
   29.71 +apply (subgoal_tac "i < length (upt (y, x))")
   29.72   apply (simp_all add: add_commute less_diff_conv)
   29.73  done
   29.74  
    30.1 --- a/src/ZF/OrdQuant.thy	Wed Jul 10 16:07:52 2002 +0200
    30.2 +++ b/src/ZF/OrdQuant.thy	Wed Jul 10 16:54:07 2002 +0200
    30.3 @@ -232,8 +232,7 @@
    30.4  
    30.5  (*Congruence rule for rewriting*)
    30.6  lemma rall_cong [cong]:
    30.7 -    "(!!x. M(x) ==> P(x) <-> P'(x))
    30.8 -     ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))"
    30.9 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (ALL x[M]. P(x)) <-> (ALL x[M]. P'(x))"
   30.10  by (simp add: rall_def)
   30.11  
   30.12  
   30.13 @@ -258,8 +257,7 @@
   30.14  by (simp add: rex_def)
   30.15  
   30.16  lemma rex_cong [cong]:
   30.17 -    "(!!x. M(x) ==> P(x) <-> P'(x))
   30.18 -     ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))"
   30.19 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (EX x[M]. P(x)) <-> (EX x[M]. P'(x))"
   30.20  by (simp add: rex_def cong: conj_cong)
   30.21  
   30.22  lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
    31.1 --- a/src/ZF/Order.thy	Wed Jul 10 16:07:52 2002 +0200
    31.2 +++ b/src/ZF/Order.thy	Wed Jul 10 16:54:07 2002 +0200
    31.3 @@ -321,7 +321,7 @@
    31.4  lemma linear_ord_iso:
    31.5      "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
    31.6  apply (simp add: linear_def ord_iso_def, safe)
    31.7 -apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec])
    31.8 +apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec])
    31.9  apply (safe elim!: bij_is_fun [THEN apply_type])
   31.10  apply (drule_tac t = "op ` (converse (f))" in subst_context)
   31.11  apply (simp add: left_inverse_bij)
    32.1 --- a/src/ZF/OrderType.thy	Wed Jul 10 16:07:52 2002 +0200
    32.2 +++ b/src/ZF/OrderType.thy	Wed Jul 10 16:54:07 2002 +0200
    32.3 @@ -619,7 +619,7 @@
    32.4    apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
    32.5   apply (force simp add: Union_empty_iff oadd_eq_0_iff
    32.6                          Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
    32.7 -apply (rule_tac x="succ(x)" in bexI)
    32.8 +apply (rule_tac x="succ(y)" in bexI)
    32.9   apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
   32.10  apply (simp add: Limit_def lt_def) 
   32.11  done
    33.1 --- a/src/ZF/Resid/Confluence.thy	Wed Jul 10 16:07:52 2002 +0200
    33.2 +++ b/src/ZF/Resid/Confluence.thy	Wed Jul 10 16:54:07 2002 +0200
    33.3 @@ -25,8 +25,7 @@
    33.4      "[|confluence(Spar_red1)|]==> strip"
    33.5  apply (unfold confluence_def strip_def)
    33.6  apply (rule impI [THEN allI, THEN allI])
    33.7 -apply (erule Spar_red.induct)
    33.8 -apply fast
    33.9 +apply (erule Spar_red.induct, fast)
   33.10  apply (fast intro: Spar_red.trans)
   33.11  done
   33.12  
   33.13 @@ -35,8 +34,7 @@
   33.14      "strip==> confluence(Spar_red)"
   33.15  apply (unfold confluence_def strip_def)
   33.16  apply (rule impI [THEN allI, THEN allI])
   33.17 -apply (erule Spar_red.induct)
   33.18 -apply blast
   33.19 +apply (erule Spar_red.induct, blast)
   33.20  apply clarify
   33.21  apply (blast intro: Spar_red.trans)
   33.22  done
   33.23 @@ -47,12 +45,10 @@
   33.24  
   33.25  
   33.26  lemma parallel_moves: "confluence(Spar_red1)"
   33.27 -apply (unfold confluence_def)
   33.28 -apply clarify
   33.29 +apply (unfold confluence_def, clarify)
   33.30  apply (frule simulation)
   33.31 -apply (frule_tac n = "z" in simulation)
   33.32 -apply clarify
   33.33 -apply (frule_tac v = "va" in paving)
   33.34 +apply (frule_tac n = z in simulation, clarify)
   33.35 +apply (frule_tac v = va in paving)
   33.36  apply (force intro: completeness)+
   33.37  done
   33.38  
   33.39 @@ -60,8 +56,7 @@
   33.40        parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
   33.41  
   33.42  lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
   33.43 -apply (unfold confluence_def, blast intro: par_red_red red_par_red)
   33.44 -done
   33.45 +by (unfold confluence_def, blast intro: par_red_red red_par_red)
   33.46  
   33.47  lemmas confluence_beta_reduction =
   33.48         confluence_parallel_reduction [THEN lemma1, standard]
   33.49 @@ -100,8 +95,7 @@
   33.50  
   33.51  lemma conv_sym: "m<--->n ==> n<--->m"
   33.52  apply (erule Sconv.induct)
   33.53 -apply (erule Sconv1.induct)
   33.54 -apply blast+
   33.55 +apply (erule Sconv1.induct, blast+)
   33.56  done
   33.57  
   33.58  (* ------------------------------------------------------------------------- *)
    34.1 --- a/src/ZF/Resid/Redex.thy	Wed Jul 10 16:07:52 2002 +0200
    34.2 +++ b/src/ZF/Resid/Redex.thy	Wed Jul 10 16:54:07 2002 +0200
    34.3 @@ -12,7 +12,7 @@
    34.4  datatype
    34.5    "redexes" = Var ("n \<in> nat")            
    34.6              | Fun ("t \<in> redexes")
    34.7 -            | App ("b \<in> bool" ,"f \<in> redexes" , "a \<in> redexes")
    34.8 +            | App ("b \<in> bool","f \<in> redexes", "a \<in> redexes")
    34.9  
   34.10  
   34.11  consts
   34.12 @@ -75,7 +75,7 @@
   34.13    type_intros    redexes.intros bool_typechecks
   34.14  
   34.15  inductive
   34.16 -  domains       "Sreg" <= "redexes"
   34.17 +  domains       "Sreg" <= redexes
   34.18    intros
   34.19      Reg_Var:     "n \<in> nat ==> regular(Var(n))"
   34.20      Reg_Fun:     "[|regular(u)|]==> regular(Fun(u))"
   34.21 @@ -161,14 +161,12 @@
   34.22  
   34.23  lemma union_l: "u ~ v ==> u <== (u un v)"
   34.24  apply (erule Scomp.induct)
   34.25 -apply (erule_tac [3] boolE)
   34.26 -apply simp_all
   34.27 +apply (erule_tac [3] boolE, simp_all)
   34.28  done
   34.29  
   34.30  lemma union_r: "u ~ v ==> v <== (u un v)"
   34.31  apply (erule Scomp.induct)
   34.32 -apply (erule_tac [3] c = "b2" in boolE)
   34.33 -apply simp_all
   34.34 +apply (erule_tac [3] c = b2 in boolE, simp_all)
   34.35  done
   34.36  
   34.37  lemma union_sym: "u ~ v ==> u un v = v un u"
   34.38 @@ -180,8 +178,7 @@
   34.39  
   34.40  lemma union_preserve_regular [rule_format]:
   34.41       "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
   34.42 -apply (erule Scomp.induct)
   34.43 -apply auto
   34.44 +apply (erule Scomp.induct, auto)
   34.45  (*select the given assumption for simplification*)
   34.46  apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
   34.47  apply simp
    35.1 --- a/src/ZF/Resid/Reduction.thy	Wed Jul 10 16:07:52 2002 +0200
    35.2 +++ b/src/ZF/Resid/Reduction.thy	Wed Jul 10 16:54:07 2002 +0200
    35.3 @@ -18,7 +18,7 @@
    35.4    "Apl(n,m)" == "App(0,n,m)"
    35.5    
    35.6  inductive
    35.7 -  domains       "lambda" <= "redexes"
    35.8 +  domains       "lambda" <= redexes
    35.9    intros
   35.10      Lambda_Var:  "               n \<in> nat ==>     Var(n) \<in> lambda"
   35.11      Lambda_Fun:  "            u \<in> lambda ==>     Fun(u) \<in> lambda"
   35.12 @@ -156,20 +156,17 @@
   35.13  
   35.14  lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
   35.15  apply (erule Sred.induct)
   35.16 -apply (rule_tac [3] Sred.trans)
   35.17 -apply simp_all
   35.18 +apply (rule_tac [3] Sred.trans, simp_all)
   35.19  done
   35.20  
   35.21  lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
   35.22  apply (erule Sred.induct)
   35.23 -apply (rule_tac [3] Sred.trans)
   35.24 -apply simp_all
   35.25 +apply (rule_tac [3] Sred.trans, simp_all)
   35.26  done
   35.27  
   35.28  lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
   35.29  apply (erule Sred.induct)
   35.30 -apply (rule_tac [3] Sred.trans)
   35.31 -apply simp_all
   35.32 +apply (rule_tac [3] Sred.trans, simp_all)
   35.33  done
   35.34  
   35.35  lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
   35.36 @@ -179,7 +176,7 @@
   35.37  
   35.38  lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>  
   35.39                 Apl(Fun(m),n)---> n'/m'"
   35.40 -apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans)
   35.41 +apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans)
   35.42  apply (simp_all add: red_Apl red_Fun)
   35.43  done
   35.44  
    36.1 --- a/src/ZF/Resid/Residuals.thy	Wed Jul 10 16:07:52 2002 +0200
    36.2 +++ b/src/ZF/Resid/Residuals.thy	Wed Jul 10 16:54:07 2002 +0200
    36.3 @@ -82,8 +82,7 @@
    36.4  
    36.5  lemma comp_resfuncD:
    36.6       "[| u~v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
    36.7 -apply (frule residuals_intro, assumption)
    36.8 -apply clarify
    36.9 +apply (frule residuals_intro, assumption, clarify)
   36.10  apply (subst the_equality)
   36.11  apply (blast intro: residuals_function)+
   36.12  done
   36.13 @@ -119,8 +118,7 @@
   36.14  
   36.15  lemma resfunc_type [simp]:
   36.16       "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
   36.17 -apply (erule Scomp.induct)
   36.18 -apply auto
   36.19 +apply (erule Scomp.induct, auto)
   36.20  apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
   36.21  apply auto
   36.22  done
   36.23 @@ -138,19 +136,16 @@
   36.24  
   36.25  lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> nat.   
   36.26           lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
   36.27 -apply (erule Scomp.induct)
   36.28 -apply safe
   36.29 +apply (erule Scomp.induct, safe)
   36.30  apply (simp_all add: lift_rec_Var subst_Var lift_subst)
   36.31 -apply (rotate_tac -2)
   36.32 -apply simp
   36.33 +apply (rotate_tac -2, simp)
   36.34  done
   36.35  
   36.36  lemma residuals_subst_rec:
   36.37       "u1~u2 ==>  \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) --> 
   36.38                    (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =  
   36.39                      subst_rec(v1 |> v2, u1 |> u2,n))"
   36.40 -apply (erule Scomp.induct)
   36.41 -apply safe
   36.42 +apply (erule Scomp.induct, safe)
   36.43  apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
   36.44  apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
   36.45  apply (simp add: substitution)
   36.46 @@ -173,8 +168,7 @@
   36.47  
   36.48  lemma residuals_preserve_reg [rule_format, simp]:
   36.49       "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
   36.50 -apply (erule Scomp.induct)
   36.51 -apply auto
   36.52 +apply (erule Scomp.induct, auto)
   36.53  apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+
   36.54  done
   36.55  
   36.56 @@ -187,8 +181,7 @@
   36.57  
   36.58  lemma preservation [rule_format]:
   36.59       "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
   36.60 -apply (erule Scomp.induct)
   36.61 -apply safe
   36.62 +apply (erule Scomp.induct, safe)
   36.63  apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
   36.64  apply (auto simp add: union_preserve_comp comp_sym_iff)
   36.65  done
   36.66 @@ -208,15 +201,13 @@
   36.67       "v<==u ==>  
   36.68         regular(u) --> (\<forall>w. w~v --> w~u -->   
   36.69                              w |> u = (w|>v) |> (u|>v))"
   36.70 -apply (erule Ssub.induct)
   36.71 -apply force+
   36.72 +apply (erule Ssub.induct, force+)
   36.73  done
   36.74  
   36.75  lemma prism:
   36.76       "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
   36.77  apply (rule prism_l)
   36.78 -apply (rule_tac [4] comp_trans)
   36.79 -apply auto
   36.80 +apply (rule_tac [4] comp_trans, auto)
   36.81  done
   36.82  
   36.83  
   36.84 @@ -226,13 +217,12 @@
   36.85  
   36.86  lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>   
   36.87             (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
   36.88 -apply (subst preservation , assumption , assumption)
   36.89 -apply (subst preservation , erule comp_sym , assumption)
   36.90 +apply (subst preservation, assumption, assumption)
   36.91 +apply (subst preservation, erule comp_sym, assumption)
   36.92  apply (subst prism [symmetric])
   36.93  apply (simp add: union_r comp_sym_iff)
   36.94  apply (simp add: union_preserve_regular comp_sym_iff)
   36.95 -apply (erule comp_trans)
   36.96 -apply assumption
   36.97 +apply (erule comp_trans, assumption)
   36.98  apply (simp add: prism [symmetric] union_l union_preserve_regular 
   36.99                   comp_sym_iff union_sym)
  36.100  done
    37.1 --- a/src/ZF/Resid/Substitution.thy	Wed Jul 10 16:07:52 2002 +0200
    37.2 +++ b/src/ZF/Resid/Substitution.thy	Wed Jul 10 16:54:07 2002 +0200
    37.3 @@ -151,8 +151,7 @@
    37.4       "u \<in> redexes 
    37.5        ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->    
    37.6             (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
    37.7 -apply (erule redexes.induct)
    37.8 -apply auto
    37.9 +apply (erule redexes.induct, auto)
   37.10  apply (case_tac "n < i")
   37.11  apply (frule lt_trans2, assumption)
   37.12  apply (simp_all add: lift_rec_Var leI)
   37.13 @@ -173,11 +172,11 @@
   37.14                 subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
   37.15  apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
   37.16  apply safe
   37.17 -apply (case_tac "n < x")
   37.18 - apply (frule_tac j = "x" in lt_trans2, assumption)
   37.19 - apply (simp add: leI)
   37.20 -apply simp
   37.21 -apply (erule_tac j = "n" in leE)
   37.22 +apply (rename_tac n n' m u) 
   37.23 +apply (case_tac "n < n'")
   37.24 + apply (frule_tac j = n' in lt_trans2, assumption)
   37.25 + apply (simp add: leI, simp)
   37.26 +apply (erule_tac j=n in leE)
   37.27  apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
   37.28  done
   37.29  
   37.30 @@ -193,12 +192,13 @@
   37.31         \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n--> 
   37.32            lift_rec(subst_rec(u,v,n),m) =  
   37.33                 subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
   37.34 -apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift)
   37.35 +apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
   37.36  apply safe
   37.37 -apply (case_tac "n < x")
   37.38 -apply (case_tac "n < xa")
   37.39 +apply (rename_tac n n' m u) 
   37.40 +apply (case_tac "n < n'")
   37.41 +apply (case_tac "n < m")
   37.42  apply (simp_all add: leI)
   37.43 -apply (erule_tac i = "x" in leE)
   37.44 +apply (erule_tac i=n' in leE)
   37.45  apply (frule lt_trans1, assumption)
   37.46  apply (simp_all add: succ_pred leI gt_pred)
   37.47  done
   37.48 @@ -207,10 +207,8 @@
   37.49  lemma subst_rec_lift_rec [rule_format]:
   37.50       "u \<in> redexes ==>   
   37.51          \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
   37.52 -apply (erule redexes.induct)
   37.53 -apply auto
   37.54 -apply (case_tac "n < na")
   37.55 -apply auto
   37.56 +apply (erule redexes.induct, auto)
   37.57 +apply (case_tac "n < na", auto)
   37.58  done
   37.59  
   37.60  lemma subst_rec_subst_rec [rule_format]:
   37.61 @@ -219,21 +217,21 @@
   37.62  	  subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) = 
   37.63  	  subst_rec(w,subst_rec(u,v,m),n)"
   37.64  apply (erule redexes.induct)
   37.65 -apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt)
   37.66 -apply safe
   37.67 -apply (case_tac "n\<le>succ (xa) ")
   37.68 - apply (erule_tac i = "n" in leE)
   37.69 +apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe)
   37.70 +apply (rename_tac n' u w) 
   37.71 +apply (case_tac "n \<le> succ(n') ")
   37.72 + apply (erule_tac i = n in leE)
   37.73   apply (simp_all add: succ_pred subst_rec_lift_rec leI)
   37.74 - apply (case_tac "n < x")
   37.75 -  apply (frule lt_trans2 , assumption, simp add: gt_pred)
   37.76 + apply (case_tac "n < m")
   37.77 +  apply (frule lt_trans2, assumption, simp add: gt_pred)
   37.78   apply simp
   37.79 - apply (erule_tac j = "n" in leE, simp add: gt_pred)
   37.80 + apply (erule_tac j = n in leE, simp add: gt_pred)
   37.81   apply (simp add: subst_rec_lift_rec)
   37.82  (*final case*)
   37.83 -apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption)
   37.84 +apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption)
   37.85  apply (erule leE)
   37.86 - apply (frule succ_leI [THEN lt_trans] , assumption)
   37.87 - apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans], 
   37.88 + apply (frule succ_leI [THEN lt_trans], assumption)
   37.89 + apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans], 
   37.90          assumption)
   37.91   apply (simp_all add: succ_pred lt_pred)
   37.92  done
    38.1 --- a/src/ZF/UNITY/Comp.ML	Wed Jul 10 16:07:52 2002 +0200
    38.2 +++ b/src/ZF/UNITY/Comp.ML	Wed Jul 10 16:54:07 2002 +0200
    38.3 @@ -71,7 +71,9 @@
    38.4  by (Force_tac 1);
    38.5  by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    38.6  by Auto_tac;
    38.7 -by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2);
    38.8 +by (Blast_tac 1); 
    38.9 +by (rename_tac "y" 1);
   38.10 +by (dres_inst_tac [("c", "y"), ("A", "AllowedActs(H)")] subsetD 1);
   38.11  by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
   38.12  qed "JN_component_iff";
   38.13  
    39.1 --- a/src/ZF/UNITY/GenPrefix.ML	Wed Jul 10 16:07:52 2002 +0200
    39.2 +++ b/src/ZF/UNITY/GenPrefix.ML	Wed Jul 10 16:54:07 2002 +0200
    39.3 @@ -317,12 +317,15 @@
    39.4  by (induct_tac "xs" 1);
    39.5  by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj]))); 
    39.6  by (Clarify_tac 1);
    39.7 -by (case_tac "x=[]" 1);
    39.8 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
    39.9 +by (eres_inst_tac [("a","ys")] list.elim 1); 
   39.10 +by (ALLGOALS Asm_full_simp_tac);
   39.11  by (Clarify_tac 1);
   39.12 -by (dres_inst_tac [("x", "ys")] bspec 1);
   39.13 +by (rename_tac "zs" 1);
   39.14 +by (dres_inst_tac [("x", "zs")] bspec 1);
   39.15  by (ALLGOALS(Clarify_tac));
   39.16 -by Auto_tac;
   39.17 +(*Faster than Auto_tac*)
   39.18 +by (rtac conjI 1); 
   39.19 +by (REPEAT (Force_tac 1));
   39.20  qed_spec_mp "nth_imp_gen_prefix";
   39.21  
   39.22  Goal "(<xs,ys>: gen_prefix(A,r)) <-> \
   39.23 @@ -484,7 +487,7 @@
   39.24  by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1);
   39.25  by Safe_tac;
   39.26  by (Blast_tac 1);
   39.27 -by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1);
   39.28 +by (subgoal_tac "length(xs) #+ (i #- length(xs)) = i" 1);
   39.29  by (stac nth_drop 1);
   39.30  by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI])));
   39.31  by (rtac (nat_diff_split RS iffD2) 1);
   39.32 @@ -501,8 +504,7 @@
   39.33  by (Asm_full_simp_tac 1);
   39.34  by (dres_inst_tac [("psi", "ya:list(A)")] asm_rl 1);
   39.35  by (rotate_tac ~1 1);
   39.36 -by (asm_full_simp_tac (simpset() addsimps
   39.37 -           [app_type, app_assoc RS sym] delsimps [app_assoc]) 1);
   39.38 +by (asm_full_simp_tac (simpset() addsimps [app_type, app_assoc RS sym]) 1);
   39.39  by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
   39.40  qed "prefix_snoc";
   39.41  Addsimps [prefix_snoc];
   39.42 @@ -514,13 +516,11 @@
   39.43  by (etac list_append_induct 1);
   39.44  by (Clarify_tac 2);
   39.45  by (rtac iffI 2);
   39.46 -by (asm_full_simp_tac (simpset()  delsimps [app_assoc]
   39.47 -                                 addsimps [app_assoc RS sym]) 2);
   39.48 +by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2);
   39.49  by (etac disjE 2 THEN etac disjE 3);
   39.50  by (rtac disjI2 2);
   39.51  by (res_inst_tac [("x", "y @ [x]")] exI 2);
   39.52 -by (asm_full_simp_tac (simpset()  delsimps [app_assoc]
   39.53 -                                 addsimps [app_assoc RS sym]) 2);
   39.54 +by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2);
   39.55  by (REPEAT(Force_tac 1));
   39.56  qed_spec_mp "prefix_append_iff";
   39.57  
    40.1 --- a/src/ZF/UNITY/Guar.ML	Wed Jul 10 16:07:52 2002 +0200
    40.2 +++ b/src/ZF/UNITY/Guar.ML	Wed Jul 10 16:54:07 2002 +0200
    40.3 @@ -277,7 +277,7 @@
    40.4  by (Simp_tac 1);
    40.5  by Safe_tac;
    40.6  by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
    40.7 -by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1);
    40.8 +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
    40.9  by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
   40.10  by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   40.11  qed "guarantees_Join_Int";
   40.12 @@ -288,9 +288,9 @@
   40.13  by (Simp_tac 1);
   40.14  by Safe_tac;
   40.15  by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   40.16 -by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1);
   40.17 +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   40.18  by (rotate_tac 4 1);
   40.19 -by (dres_inst_tac [("x", "F Join x")] bspec 1);
   40.20 +by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
   40.21  by (Simp_tac 1);
   40.22  by (force_tac (claset(), simpset() addsimps [ok_commute]) 1);
   40.23  by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   40.24 @@ -315,11 +315,12 @@
   40.25      "[| ALL i:I. F(i) : X(i) guarantees Y(i);  OK(I,F) |] \
   40.26  \    ==> JOIN(I,F) : (UN i:I. X(i)) guarantees (UN i:I. Y(i))";
   40.27  by Auto_tac;
   40.28 -by (dres_inst_tac [("x", "xa")] bspec 1);
   40.29 +by (dres_inst_tac [("x", "y")] bspec 1);
   40.30  by (ALLGOALS(Asm_full_simp_tac));
   40.31  by Safe_tac;
   40.32  by (rotate_tac ~1 1);
   40.33 -by (dres_inst_tac [("x", "JOIN(I-{xa}, F) Join x")] bspec 1);
   40.34 +by (rename_tac "G y" 1);
   40.35 +by (dres_inst_tac [("x", "JOIN(I-{y}, F) Join G")] bspec 1);
   40.36  by (auto_tac
   40.37      (claset() addIs [OK_imp_ok],
   40.38       simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
   40.39 @@ -441,18 +442,15 @@
   40.40  by Auto_tac;
   40.41  qed "wx_subset";
   40.42  
   40.43 -Goal
   40.44 -"ex_prop(wx(X))";
   40.45 -by (full_simp_tac (simpset() 
   40.46 -        addsimps [ex_prop_def, wx_def]) 1);
   40.47 +Goal "ex_prop(wx(X))";
   40.48 +by (full_simp_tac (simpset() addsimps [ex_prop_def, wx_def]) 1);
   40.49  by Safe_tac;
   40.50  by (Blast_tac 1);
   40.51 -by (ALLGOALS(res_inst_tac [("x", "xb")] bexI));
   40.52 +by (ALLGOALS(res_inst_tac [("x", "x")] bexI));
   40.53  by (REPEAT(Force_tac 1));
   40.54  qed "wx_ex_prop";
   40.55  
   40.56 -Goalw [wx_def]
   40.57 -"ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)";
   40.58 +Goalw [wx_def] "ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)";
   40.59  by Auto_tac;
   40.60  qed "wx_weakest";
   40.61  
    41.1 --- a/src/ZF/UNITY/ListPlus.ML	Wed Jul 10 16:07:52 2002 +0200
    41.2 +++ b/src/ZF/UNITY/ListPlus.ML	Wed Jul 10 16:54:07 2002 +0200
    41.3 @@ -335,16 +335,13 @@
    41.4  
    41.5  (** More on lists **)
    41.6  
    41.7 -Goal
    41.8 -"n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
    41.9 -\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
   41.10 +Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
   41.11 +\               --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
   41.12  by (induct_tac "n" 1);
   41.13 -by (ALLGOALS(Asm_full_simp_tac));
   41.14 +by (Asm_full_simp_tac 1);
   41.15  by (Clarify_tac 1);
   41.16 -by (case_tac "xb=Nil" 1);
   41.17 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
   41.18 -by (Clarify_tac 1);
   41.19 -by (auto_tac (claset() addSEs [ConsE], simpset()));
   41.20 +by (etac list.elim 1);
   41.21 +by Auto_tac;  
   41.22  qed_spec_mp "nth_drop";
   41.23  
   41.24  
    42.1 --- a/src/ZF/UNITY/Union.ML	Wed Jul 10 16:07:52 2002 +0200
    42.2 +++ b/src/ZF/UNITY/Union.ML	Wed Jul 10 16:54:07 2002 +0200
    42.3 @@ -251,15 +251,15 @@
    42.4  Goalw [constrains_def, JOIN_def,st_set_def]
    42.5   "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)";
    42.6  by Auto_tac;
    42.7 -by (cut_inst_tac [("F","F(xa)")] Acts_type 1);
    42.8  by (Blast_tac 2);
    42.9 -by (dres_inst_tac [("x", "xb")] bspec 1);
   42.10 +by (rename_tac "j act y z" 1);
   42.11 +by (cut_inst_tac [("F","F(j)")] Acts_type 1);
   42.12 +by (dres_inst_tac [("x", "act")] bspec 1);
   42.13  by Auto_tac;
   42.14  qed "JN_constrains";
   42.15  
   42.16  Goal "(F Join G : A co B) <-> (programify(F):A co B & programify(G):A co B)";
   42.17 -by (auto_tac
   42.18 -    (claset(), simpset() addsimps [constrains_def]));
   42.19 +by (auto_tac (claset(), simpset() addsimps [constrains_def]));
   42.20  qed "Join_constrains";
   42.21  
   42.22  Goal "(F Join G : A unless B) <-> \
   42.23 @@ -288,7 +288,8 @@
   42.24  by (cut_facts_tac [minor] 1);
   42.25  by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
   42.26  by (Clarify_tac 1);
   42.27 -by (forw_inst_tac [("i", "x")] major 1);
   42.28 +by (rename_tac "j" 1);
   42.29 +by (forw_inst_tac [("i", "j")] major 1);
   42.30  by (ftac constrainsD2 1);
   42.31  by (Asm_full_simp_tac 1);
   42.32  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   42.33 @@ -298,8 +299,8 @@
   42.34  by (asm_simp_tac 
   42.35      (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
   42.36  by Auto_tac;
   42.37 -by (cut_inst_tac [("F", "F(xa)")] Acts_type 1);
   42.38 -by (dres_inst_tac [("x","xb")] bspec 1);
   42.39 +by (cut_inst_tac [("F", "F(i)")] Acts_type 1);
   42.40 +by (dres_inst_tac [("x","act")] bspec 1);
   42.41  by Auto_tac;
   42.42  qed "JN_stable";
   42.43  
   42.44 @@ -366,7 +367,7 @@
   42.45  by (auto_tac (claset(),
   42.46                simpset() addsimps [transient_def, JOIN_def]));
   42.47  by (rewtac st_set_def);
   42.48 -by (dres_inst_tac [("x", "xb")] bspec 2);
   42.49 +by (dres_inst_tac [("x", "act")] bspec 2);
   42.50  by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
   42.51  qed "JN_transient";
   42.52  
    43.1 --- a/src/ZF/ZF.ML	Wed Jul 10 16:07:52 2002 +0200
    43.2 +++ b/src/ZF/ZF.ML	Wed Jul 10 16:54:07 2002 +0200
    43.3 @@ -57,7 +57,8 @@
    43.4  
    43.5  (*Congruence rule for rewriting*)
    43.6  val prems= Goalw [Ball_def] 
    43.7 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')";
    43.8 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] \
    43.9 +\    ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))";
   43.10  by (simp_tac (FOL_ss addsimps prems) 1) ;
   43.11  qed "ball_cong";
   43.12  
   43.13 @@ -95,8 +96,8 @@
   43.14  Addsimps [bex_triv];
   43.15  
   43.16  val prems= Goalw [Bex_def] 
   43.17 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   43.18 -\    |] ==> Bex(A,P) <-> Bex(A',P')";
   43.19 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] \
   43.20 +\    ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))";
   43.21  by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
   43.22  qed "bex_cong";
   43.23  
    44.1 --- a/src/ZF/ex/Commutation.thy	Wed Jul 10 16:07:52 2002 +0200
    44.2 +++ b/src/ZF/ex/Commutation.thy	Wed Jul 10 16:54:07 2002 +0200
    44.3 @@ -39,8 +39,7 @@
    44.4  
    44.5  lemma square_rtrancl [rule_format]: 
    44.6       "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)"
    44.7 -apply (unfold square_def)
    44.8 -apply clarify
    44.9 +apply (unfold square_def, clarify)
   44.10  apply (erule rtrancl_induct)
   44.11  apply (blast intro: rtrancl_refl)
   44.12  apply (blast intro: rtrancl_into_rtrancl)
   44.13 @@ -50,8 +49,7 @@
   44.14  lemma diamond_strip: 
   44.15   "diamond(r) ==> strip(r)"
   44.16  apply (unfold diamond_def commute_def strip_def)
   44.17 -apply (rule square_rtrancl)
   44.18 -apply simp_all
   44.19 +apply (rule square_rtrancl, simp_all)
   44.20  done
   44.21  
   44.22  (*** commute ***)
   44.23 @@ -62,8 +60,7 @@
   44.24  
   44.25  lemma commute_rtrancl [rule_format]: 
   44.26      "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"
   44.27 -apply (unfold commute_def)
   44.28 -apply clarify
   44.29 +apply (unfold commute_def, clarify)
   44.30  apply (rule square_rtrancl)
   44.31  apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) 
   44.32  apply (simp_all add: rtrancl_field)
   44.33 @@ -89,24 +86,21 @@
   44.34  lemma diamond_confluent: 
   44.35      "diamond(r) ==> confluent(r)"
   44.36  apply (unfold diamond_def confluent_def)
   44.37 -apply (erule commute_rtrancl)
   44.38 -apply simp
   44.39 +apply (erule commute_rtrancl, simp)
   44.40  done
   44.41  
   44.42  lemma confluent_Un: 
   44.43   "[| confluent(r); confluent(s); commute(r^*, s^*); 
   44.44       relation(r); relation(s) |] ==> confluent(r Un s)"
   44.45  apply (unfold confluent_def)
   44.46 -apply (rule rtrancl_Un_rtrancl [THEN subst])
   44.47 -apply auto
   44.48 +apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
   44.49  apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
   44.50  done
   44.51  
   44.52  
   44.53  lemma diamond_to_confluence: 
   44.54       "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
   44.55 -apply (drule rtrancl_subset [symmetric])
   44.56 -apply assumption
   44.57 +apply (drule rtrancl_subset [symmetric], assumption)
   44.58  apply (simp_all add: confluent_def)
   44.59  apply (blast intro: diamond_confluent [THEN confluentD])
   44.60  done
   44.61 @@ -117,13 +111,12 @@
   44.62  lemma Church_Rosser1: 
   44.63       "Church_Rosser(r) ==> confluent(r)"
   44.64  apply (unfold confluent_def Church_Rosser_def square_def 
   44.65 -              commute_def diamond_def)
   44.66 -apply auto
   44.67 +              commute_def diamond_def, auto)
   44.68  apply (drule converseI)
   44.69  apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
   44.70 -apply (drule_tac x = "b" in spec)
   44.71 -apply (drule_tac x1 = "c" in spec [THEN mp])
   44.72 -apply (rule_tac b = "a" in rtrancl_trans)
   44.73 +apply (drule_tac x = b in spec)
   44.74 +apply (drule_tac x1 = c in spec [THEN mp])
   44.75 +apply (rule_tac b = a in rtrancl_trans)
   44.76  apply (blast intro: rtrancl_mono [THEN subsetD])+
   44.77  done
   44.78  
   44.79 @@ -131,12 +124,10 @@
   44.80  lemma Church_Rosser2: 
   44.81       "confluent(r) ==> Church_Rosser(r)"
   44.82  apply (unfold confluent_def Church_Rosser_def square_def 
   44.83 -              commute_def diamond_def)
   44.84 -apply auto
   44.85 +              commute_def diamond_def, auto)
   44.86  apply (frule fieldI1)
   44.87  apply (simp add: rtrancl_field)
   44.88 -apply (erule rtrancl_induct)
   44.89 -apply auto
   44.90 +apply (erule rtrancl_induct, auto)
   44.91  apply (blast intro: rtrancl_refl)
   44.92  apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+
   44.93  done
    45.1 --- a/src/ZF/ex/LList.thy	Wed Jul 10 16:07:52 2002 +0200
    45.2 +++ b/src/ZF/ex/LList.thy	Wed Jul 10 16:54:07 2002 +0200
    45.3 @@ -143,18 +143,15 @@
    45.4  apply (erule trans_induct)
    45.5  apply (intro allI impI)
    45.6  apply (erule lleq.cases)
    45.7 -apply (unfold QInr_def llist.con_defs)
    45.8 -apply safe
    45.9 +apply (unfold QInr_def llist.con_defs, safe)
   45.10  apply (fast elim!: Ord_trans bspec [elim_format])
   45.11  done
   45.12  
   45.13  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
   45.14  lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)"
   45.15  apply (erule lleq.coinduct [OF converseI]) 
   45.16 -apply (rule lleq.dom_subset [THEN converse_type])
   45.17 -apply safe
   45.18 -apply (erule lleq.cases)
   45.19 -apply blast+
   45.20 +apply (rule lleq.dom_subset [THEN converse_type], safe)
   45.21 +apply (erule lleq.cases, blast+)
   45.22  done
   45.23  
   45.24  lemma lleq_implies_equal: "<l,l'> \<in> lleq(A) ==> l=l'"
   45.25 @@ -168,8 +165,7 @@
   45.26  apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct)
   45.27  apply blast
   45.28  apply safe
   45.29 -apply (erule_tac a="l" in llist.cases)
   45.30 -apply fast+
   45.31 +apply (erule_tac a=l in llist.cases, fast+)
   45.32  done
   45.33  
   45.34  
   45.35 @@ -220,25 +216,21 @@
   45.36       "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))"
   45.37  apply (erule trans_induct)
   45.38  apply (rule ballI)
   45.39 -apply (erule llist.cases)
   45.40 -apply (simp_all)
   45.41 +apply (erule llist.cases, simp_all)
   45.42  apply (simp_all add: QInl_def QInr_def llist.con_defs)
   45.43  (*LCons case: I simply can't get rid of the deepen_tac*)
   45.44  apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1")
   45.45  done
   45.46  
   45.47  lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
   45.48 -apply (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI])
   45.49 -apply assumption+
   45.50 -done
   45.51 +by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)
   45.52  
   45.53  lemma flip_type: "l \<in> llist(bool) ==> flip(l): llist(bool)"
   45.54  apply (rule_tac X = "{flip (l) . l \<in> llist (bool) }" in llist.coinduct)
   45.55  apply blast
   45.56  apply (fast intro!: flip_in_quniv)
   45.57  apply (erule RepFunE)
   45.58 -apply (erule_tac a="la" in llist.cases)
   45.59 -apply auto
   45.60 +apply (erule_tac a=la in llist.cases, auto)
   45.61  done
   45.62  
   45.63  lemma flip_flip: "l \<in> llist(bool) ==> flip(flip(l)) = l"
   45.64 @@ -247,7 +239,7 @@
   45.65  apply blast
   45.66  apply (fast intro!: flip_type)
   45.67  apply (erule RepFunE)
   45.68 -apply (erule_tac a="la" in llist.cases)
   45.69 +apply (erule_tac a=la in llist.cases)
   45.70  apply (simp_all add: flip_type not_not)
   45.71  done
   45.72  
    46.1 --- a/src/ZF/ex/Limit.thy	Wed Jul 10 16:07:52 2002 +0200
    46.2 +++ b/src/ZF/ex/Limit.thy	Wed Jul 10 16:54:07 2002 +0200
    46.3 @@ -748,8 +748,7 @@
    46.4  
    46.5  lemma cf_least:
    46.6      "[|cpo(D); pcpo(E); y \<in> cont(D,E)|]==>rel(cf(D,E),(\<lambda>x \<in> set(D).bot(E)),y)"
    46.7 -apply (rule rel_cfI, simp)
    46.8 -apply typecheck
    46.9 +apply (rule rel_cfI, simp, typecheck)
   46.10  done
   46.11  
   46.12  lemma pcpo_cf:
    47.1 --- a/src/ZF/ex/Primes.thy	Wed Jul 10 16:07:52 2002 +0200
    47.2 +++ b/src/ZF/ex/Primes.thy	Wed Jul 10 16:54:07 2002 +0200
    47.3 @@ -31,9 +31,7 @@
    47.4  (************************************************)
    47.5  
    47.6  lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
    47.7 -apply (unfold divides_def)
    47.8 -apply assumption
    47.9 -done
   47.10 +by (unfold divides_def, assumption)
   47.11  
   47.12  lemma dvdE:
   47.13       "[|m dvd n;  !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P"
   47.14 @@ -69,13 +67,11 @@
   47.15  
   47.16  lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k"
   47.17  apply (unfold divides_def)
   47.18 -apply (simp add: mult_assoc)
   47.19 -apply blast
   47.20 +apply (simp add: mult_assoc, blast)
   47.21  done
   47.22  
   47.23  lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
   47.24 -apply (unfold divides_def)
   47.25 -apply clarify
   47.26 +apply (unfold divides_def, clarify)
   47.27  apply (rule_tac x = "i#*k" in bexI)
   47.28  apply (simp add: mult_ac)
   47.29  apply (rule mult_type)
   47.30 @@ -90,8 +86,7 @@
   47.31  
   47.32  lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
   47.33  apply (unfold gcd_def)
   47.34 -apply (subst transrec)
   47.35 -apply simp
   47.36 +apply (subst transrec, simp)
   47.37  done
   47.38  
   47.39  lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)"
   47.40 @@ -109,7 +104,7 @@
   47.41  done
   47.42  
   47.43  lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)"
   47.44 -apply (cut_tac m = "m" and n = "natify (n) " in gcd_non_0_raw)
   47.45 +apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw)
   47.46  apply auto
   47.47  done
   47.48  
   47.49 @@ -155,11 +150,11 @@
   47.50           \<forall>m \<in> nat. P(m,0);  
   47.51           \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]  
   47.52        ==> \<forall>m \<in> nat. P (m,n)"
   47.53 -apply (erule_tac i = "n" in complete_induct)
   47.54 +apply (erule_tac i = n in complete_induct)
   47.55  apply (case_tac "x=0")
   47.56  apply (simp (no_asm_simp))
   47.57  apply clarify
   47.58 -apply (drule_tac x1 = "m" and x = "x" in bspec [THEN bspec])
   47.59 +apply (drule_tac x1 = m and x = x in bspec [THEN bspec])
   47.60  apply (simp_all add: Ord_0_lt_iff)
   47.61  apply (blast intro: mod_less_divisor [THEN ltD])
   47.62  done
   47.63 @@ -175,7 +170,7 @@
   47.64  (* gcd type *)
   47.65  
   47.66  lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
   47.67 -apply (subgoal_tac "gcd (natify (m) , natify (n)) \<in> nat")
   47.68 +apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> nat")
   47.69  apply simp
   47.70  apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct)
   47.71  apply auto
   47.72 @@ -187,7 +182,7 @@
   47.73  
   47.74  lemma gcd_dvd_both:
   47.75       "[| m \<in> nat; n \<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n"
   47.76 -apply (rule_tac m = "m" and n = "n" in gcd_induct)
   47.77 +apply (rule_tac m = m and n = n in gcd_induct)
   47.78  apply (simp_all add: gcd_non_0)
   47.79  apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt])
   47.80  done
   47.81 @@ -207,8 +202,7 @@
   47.82  lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
   47.83  apply (unfold divides_def)
   47.84  apply (case_tac "b=0")
   47.85 - apply (simp add: DIVISION_BY_ZERO_MOD)
   47.86 -apply auto
   47.87 + apply (simp add: DIVISION_BY_ZERO_MOD, auto)
   47.88  apply (blast intro: mod_mult_distrib2 [symmetric])
   47.89  done
   47.90  
   47.91 @@ -218,7 +212,7 @@
   47.92  lemma gcd_greatest_raw [rule_format]:
   47.93       "[| m \<in> nat; n \<in> nat; f \<in> nat |]    
   47.94        ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
   47.95 -apply (rule_tac m = "m" and n = "n" in gcd_induct)
   47.96 +apply (rule_tac m = m and n = n in gcd_induct)
   47.97  apply (simp_all add: gcd_non_0 dvd_mod)
   47.98  done
   47.99  
  47.100 @@ -251,8 +245,7 @@
  47.101  apply (rule is_gcd_unique)
  47.102  apply (rule is_gcd)
  47.103  apply (rule_tac [3] is_gcd_commute [THEN iffD1])
  47.104 -apply (rule_tac [3] is_gcd)
  47.105 -apply auto
  47.106 +apply (rule_tac [3] is_gcd, auto)
  47.107  done
  47.108  
  47.109  lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
  47.110 @@ -286,11 +279,9 @@
  47.111  lemma gcd_mult_distrib2_raw:
  47.112       "[| k \<in> nat; m \<in> nat; n \<in> nat |]  
  47.113        ==> k #* gcd (m, n) = gcd (k #* m, k #* n)"
  47.114 -apply (erule_tac m = "m" and n = "n" in gcd_induct)
  47.115 -apply assumption
  47.116 -apply (simp)
  47.117 -apply (case_tac "k = 0")
  47.118 +apply (erule_tac m = m and n = n in gcd_induct, assumption)
  47.119  apply simp
  47.120 +apply (case_tac "k = 0", simp)
  47.121  apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff)
  47.122  done
  47.123  
  47.124 @@ -301,20 +292,15 @@
  47.125  done
  47.126  
  47.127  lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)"
  47.128 -apply (cut_tac k = "k" and m = "1" and n = "n" in gcd_mult_distrib2)
  47.129 -apply auto
  47.130 -done
  47.131 +by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto)
  47.132  
  47.133  lemma gcd_self [simp]: "gcd (k, k) = natify(k)"
  47.134 -apply (cut_tac k = "k" and n = "1" in gcd_mult)
  47.135 -apply auto
  47.136 -done
  47.137 +by (cut_tac k = k and n = 1 in gcd_mult, auto)
  47.138  
  47.139  lemma relprime_dvd_mult:
  47.140       "[| gcd (k,n) = 1;  k dvd (m #* n);  m \<in> nat |] ==> k dvd m"
  47.141 -apply (cut_tac k = "m" and m = "k" and n = "n" in gcd_mult_distrib2)
  47.142 -apply auto
  47.143 -apply (erule_tac b = "m" in ssubst)
  47.144 +apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto)
  47.145 +apply (erule_tac b = m in ssubst)
  47.146  apply (simp add: dvd_imp_nat1)
  47.147  done
  47.148  
  47.149 @@ -324,12 +310,10 @@
  47.150  
  47.151  lemma prime_imp_relprime: 
  47.152       "[| p \<in> prime;  ~ (p dvd n);  n \<in> nat |] ==> gcd (p, n) = 1"
  47.153 -apply (unfold prime_def)
  47.154 -apply clarify
  47.155 +apply (unfold prime_def, clarify)
  47.156  apply (drule_tac x = "gcd (p,n)" in bspec)
  47.157  apply auto
  47.158 -apply (cut_tac m = "p" and n = "n" in gcd_dvd2)
  47.159 -apply auto
  47.160 +apply (cut_tac m = p and n = n in gcd_dvd2, auto)
  47.161  done
  47.162  
  47.163  lemma prime_into_nat: "p \<in> prime ==> p \<in> nat"
  47.164 @@ -351,7 +335,7 @@
  47.165  (** Addition laws **)
  47.166  
  47.167  lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
  47.168 -apply (subgoal_tac "gcd (m #+ natify (n) , natify (n)) = gcd (m, natify (n))")
  47.169 +apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
  47.170  apply simp
  47.171  apply (case_tac "natify (n) = 0")
  47.172  apply (auto simp add: Ord_0_lt_iff gcd_non_0)
  47.173 @@ -359,8 +343,7 @@
  47.174  
  47.175  lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
  47.176  apply (rule gcd_commute [THEN trans])
  47.177 -apply (subst add_commute)
  47.178 -apply simp
  47.179 +apply (subst add_commute, simp)
  47.180  apply (rule gcd_commute)
  47.181  done
  47.182  
  47.183 @@ -426,10 +409,8 @@
  47.184  
  47.185  lemma prime_not_square:
  47.186       "\<lbrakk>m \<in> nat; p \<in> prime\<rbrakk> \<Longrightarrow> \<forall>k \<in> nat. 0<k \<longrightarrow> m#*m \<noteq> p#*(k#*k)"
  47.187 -apply (erule complete_induct)
  47.188 -apply clarify
  47.189 -apply (frule prime_dvd_other_side)
  47.190 -apply assumption
  47.191 +apply (erule complete_induct, clarify)
  47.192 +apply (frule prime_dvd_other_side, assumption)
  47.193  apply assumption
  47.194  apply (erule dvdE)
  47.195  apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat)
    48.1 --- a/src/ZF/ex/Ramsey.thy	Wed Jul 10 16:07:52 2002 +0200
    48.2 +++ b/src/ZF/ex/Ramsey.thy	Wed Jul 10 16:54:07 2002 +0200
    48.3 @@ -93,29 +93,27 @@
    48.4            \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A Un B) -->    
    48.5                             Atleast(m,A) | Atleast(n,B)"
    48.6  apply (induct_tac "m")
    48.7 -apply (blast intro!: Atleast0)
    48.8 -apply (simp)
    48.9 +apply (blast intro!: Atleast0, simp)
   48.10  apply (rule ballI)
   48.11  apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*)
   48.12 -apply (induct_tac "n")
   48.13 -apply auto
   48.14 +apply (induct_tac "n", auto)
   48.15  apply (erule Atleast_succD [THEN bexE])
   48.16  apply (rename_tac n' A B z)
   48.17  apply (erule UnE)
   48.18  (**case z \<in> B.  Instantiate the '\<forall>A B' induction hypothesis. **)
   48.19 -apply (drule_tac [2] x1 = "A" and x = "B-{z}" in spec [THEN spec])
   48.20 +apply (drule_tac [2] x1 = A and x = "B-{z}" in spec [THEN spec])
   48.21  apply (erule_tac [2] mp [THEN disjE])
   48.22  (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
   48.23  apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+
   48.24  (*proving the condition*)
   48.25  prefer 2 apply (blast intro: Atleast_superset)
   48.26  (**case z \<in> A.  Instantiate the '\<forall>n \<in> nat. \<forall>A B' induction hypothesis. **)
   48.27 -apply (drule_tac x2="succ(n')" and x1="A-{z}" and x="B"
   48.28 +apply (drule_tac x2="succ(n')" and x1="A-{z}" and x=B
   48.29         in bspec [THEN spec, THEN spec])
   48.30  apply (erule nat_succI)
   48.31  apply (erule mp [THEN disjE])
   48.32  (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
   48.33 -apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+;
   48.34 +apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+
   48.35  (*proving the condition*)
   48.36  apply simp
   48.37  apply (blast intro: Atleast_superset)
   48.38 @@ -138,10 +136,8 @@
   48.39    Ramsey_step_lemma.*)
   48.40  lemma Atleast_partition: "[| Atleast(m #+ n, A);  m \<in> nat;  n \<in> nat |]   
   48.41        ==> Atleast(succ(m), {x \<in> A. ~P(x)}) | Atleast(n, {x \<in> A. P(x)})"
   48.42 -apply (rule nat_succI [THEN pigeon2])
   48.43 -apply assumption+
   48.44 -apply (rule Atleast_superset)
   48.45 -apply auto
   48.46 +apply (rule nat_succI [THEN pigeon2], assumption+)
   48.47 +apply (rule Atleast_superset, auto)
   48.48  done
   48.49  
   48.50  (*For the Atleast part, proves ~(a \<in> I) from the second premise!*)
   48.51 @@ -168,8 +164,7 @@
   48.52  lemma Ramsey_step_lemma:
   48.53     "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));   
   48.54         m \<in> nat;  n \<in> nat |] ==> Ramsey(succ(m#+n), succ(i), succ(j))"
   48.55 -apply (unfold Ramsey_def)
   48.56 -apply clarify
   48.57 +apply (unfold Ramsey_def, clarify)
   48.58  apply (erule Atleast_succD [THEN bexE])
   48.59  apply (erule_tac P1 = "%z.<x,z>:E" in Atleast_partition [THEN disjE],
   48.60         assumption+)
    49.1 --- a/src/ZF/ex/misc.thy	Wed Jul 10 16:07:52 2002 +0200
    49.2 +++ b/src/ZF/ex/misc.thy	Wed Jul 10 16:54:07 2002 +0200
    49.3 @@ -60,7 +60,7 @@
    49.4         (K O J) \<in> hom(A,f,C,h)"
    49.5  by force
    49.6  
    49.7 -(*Another version , with meta-level rewriting*)
    49.8 +(*Another version, with meta-level rewriting*)
    49.9  lemma "(!! A f B g. hom(A,f,B,g) ==  
   49.10             {H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &  
   49.11                       (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) 
   49.12 @@ -72,9 +72,7 @@
   49.13  (** A characterization of functions suggested by Tobias Nipkow **)
   49.14  
   49.15  lemma "r \<in> domain(r)->B  <->  r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
   49.16 -apply (unfold Pi_def function_def)
   49.17 -apply best
   49.18 -done
   49.19 +by (unfold Pi_def function_def, best)
   49.20  
   49.21  (**** From D Pastre.  Automatic theorem proving in set theory. 
   49.22           Artificial Intelligence, 10:1--27, 1978.
   49.23 @@ -138,11 +136,9 @@
   49.24       \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
   49.25  apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
   49.26  apply (blast intro: lam_type)
   49.27 -apply (blast dest: apply_type)
   49.28 -apply simp_all
   49.29 +apply (blast dest: apply_type, simp_all)
   49.30  apply fast (*strange, but blast can't do it*)
   49.31 -apply (rule fun_extension)
   49.32 -apply auto
   49.33 +apply (rule fun_extension, auto)
   49.34  by blast
   49.35  
   49.36  end