# HG changeset patch # User paulson # Date 1026312847 -7200 # Node ID 0f89104dd377d723d57e63e5173909b89d8b60b6 # Parent 20ca66539bef00bfb7e08d472c7a321acf320123 Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying. diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/AC16_WO4.thy --- a/src/ZF/AC/AC16_WO4.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/AC16_WO4.thy Wed Jul 10 16:54:07 2002 +0200 @@ -21,7 +21,7 @@ apply (erule bexE) apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]]) apply (erule exE) -apply (rule_tac x = "n" in exI) +apply (rule_tac x = n in exI) apply (rule_tac x = "\i \ n. {f`i}" in exI) apply (simp add: ltD bij_def surj_def) apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun] @@ -267,7 +267,7 @@ ==> \! c. c \ s(u) & a \ c & b \ c" apply (rule all_ex [simplified k_def, THEN ballE]) apply (erule ex1E) - apply (rule_tac a = "w" in ex1I, blast intro: sI) + apply (rule_tac a = w in ex1I, blast intro: sI) apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in) apply (blast del: PowI intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll]) @@ -295,7 +295,7 @@ apply (rule lam_type) apply (frule ex1_superset_a [THEN theI], fast+, clarify) apply (rule cons_eqE [of _ a]) -apply (drule_tac A = "THE c. ?P (c) " and C = "y" in eq_imp_Int_eq) +apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq) apply (simp_all add: the_eq_cons) done @@ -412,7 +412,7 @@ "v \ LL ==> \! w. w \ MM & v \ w" apply (unfold MM_def LL_def, safe, fast) apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption) -apply (rule_tac x = "x" in all_ex [THEN ballE]) +apply (rule_tac x = x in all_ex [THEN ballE]) apply (blast intro: eqpoll_sym)+ done @@ -436,7 +436,7 @@ done lemma (in AC16) unique_superset1: "a \ LL \ (THE x. x \ MM \ a \ x) \ MM" -by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]); +by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) lemma (in AC16) the_in_MM_subset: "v \ LL ==> (THE x. x \ MM & v \ x) \ x Un y" diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/AC16_lemmas.thy --- a/src/ZF/AC/AC16_lemmas.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/AC16_lemmas.thy Wed Jul 10 16:54:07 2002 +0200 @@ -82,7 +82,7 @@ apply (rule subsetI) apply (case_tac "\y \ z. y \ x", blast ) apply (simp, erule bexE) -apply (rule_tac i=xa and j=x in Ord_linear_le) +apply (rule_tac i=y and j=x in Ord_linear_le) apply (blast dest: le_imp_subset elim: leE ltE)+ done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/AC17_AC1.thy --- a/src/ZF/AC/AC17_AC1.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/AC17_AC1.thy Wed Jul 10 16:54:07 2002 +0200 @@ -235,7 +235,7 @@ lemma AC3_AC1_lemma: "b\A ==> (\x \ {a \ A. id(A)`a\b}. id(A)`x) = (\x \ A. x)" apply (simp add: id_def cong add: Pi_cong) -apply (rule_tac b = "A" in subst_context, fast) +apply (rule_tac b = A in subst_context, fast) done lemma AC3_AC1: "AC3 ==> AC1" diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/AC18_AC19.thy --- a/src/ZF/AC/AC18_AC19.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/AC18_AC19.thy Wed Jul 10 16:54:07 2002 +0200 @@ -89,7 +89,7 @@ lemma lemma2: "[| A\0; 0\A |] ==> (\x \ {uu(a). a \ A}. \b \ x. b) \ 0" apply (erule not_emptyE) -apply (rule_tac a = "0" in not_emptyI) +apply (rule_tac a = 0 in not_emptyI) apply (fast intro!: lemma2_1) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/Cardinal_aux.thy --- a/src/ZF/AC/Cardinal_aux.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/Cardinal_aux.thy Wed Jul 10 16:54:07 2002 +0200 @@ -24,7 +24,7 @@ "[| A \ i; Ord(i) |] ==> \j. j le i & A \ j" by (blast intro!: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym] - dest: lepoll_well_ord); + dest: lepoll_well_ord) (* j=|A| *) lemma lesspoll_imp_ex_lt_eqpoll: @@ -87,7 +87,7 @@ above?*) lemma Un_lepoll_Inf_Ord: "[| A \ i; B \ i; ~Finite(i); Ord(i) |] ==> A Un B \ i" -apply (rule_tac A1 = "i" and C1 = "i" in ex_eqpoll_disjoint [THEN exE]) +apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE]) apply (erule conjE) apply (drule lepoll_trans) apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) @@ -144,7 +144,7 @@ lemma UN_fun_lepoll: "[| \b \ a. f`b \ n & f`b \ T; well_ord(T, R); ~Finite(a); Ord(a); n \ nat |] ==> (\b \ a. f`b) \ a" -by (blast intro: UN_fun_lepoll_lemma); +by (blast intro: UN_fun_lepoll_lemma) lemma UN_lepoll: "[| \b \ a. F(b) \ n & F(b) \ T; well_ord(T, R); @@ -164,7 +164,7 @@ apply (rule UN_I) apply (rule_tac P = "%z. x \ F (z) " in Least_in_Ord, (assumption+)) apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify) -apply (erule_tac P = "%z. x \ F (z) " and i = "c" in less_LeastE) +apply (erule_tac P = "%z. x \ F (z) " and i = c in less_LeastE) apply (blast intro: Ord_Least ltI) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/DC.thy --- a/src/ZF/AC/DC.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/DC.thy Wed Jul 10 16:54:07 2002 +0200 @@ -175,7 +175,7 @@ apply (drule bspec [OF _ nat_0I]) apply (simp add: XX_def, safe) apply (rule rev_bexI, assumption) -apply (subgoal_tac "0 \ x", force) +apply (subgoal_tac "0 \ y", force) apply (force simp add: RR_def intro: ltD elim!: nat_0_le [THEN leE]) (** LEVEL 7, other subgoal **) @@ -186,7 +186,7 @@ apply safe apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans], assumption) -apply (frule_tac a="xa" in domain_of_fun [symmetric, THEN trans], +apply (frule_tac a=y in domain_of_fun [symmetric, THEN trans], assumption) apply (fast elim!: nat_into_Ord [THEN succ_in_succ] dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]]) @@ -208,7 +208,7 @@ apply (simp add: RR_def) apply (drule lemma2, assumption+) apply (fast dest!: domain_of_fun) -apply (drule_tac x = "xa" in bspec, assumption) +apply (drule_tac x = xa in bspec, assumption) apply (erule sym [THEN trans, symmetric]) apply (rule restrict_eq_imp_val_eq [symmetric]) apply (drule bspec [OF _ nat_succI], assumption) @@ -392,7 +392,7 @@ apply (unfold RR_def allRR_def) apply (rule oallI, drule ltD) apply (erule nat_induct) -apply (drule_tac x="0" in ospec, blast intro: Limit_has_0) +apply (drule_tac x=0 in ospec, blast intro: Limit_has_0) apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) (*induction step*) (** LEVEL 5 **) (*prevent simplification of ~\ to \~ *) @@ -409,7 +409,8 @@ apply (frule f_n_type) apply (simp add: XX_def, assumption+) apply (rule rev_bexI, erule nat_succI) -apply (rule_tac x = "cons (, f`xa) " in bexI) +apply (rename_tac m i j y z) +apply (rule_tac x = "cons(, f`m)" in bexI) prefer 2 apply (blast intro: cons_fun_type2) apply (rule conjI) prefer 2 apply (fast del: ballI subsetI @@ -497,7 +498,7 @@ intro!: Ord_Hartog leI [THEN le_imp_subset]) apply (erule allE impE)+ apply (rule Card_Hartog) -apply (erule_tac x = "A" in allE) +apply (erule_tac x = A in allE) apply (erule_tac x = "{ \ Pow (A) *A . z1 \ Hartog (A) & z2 \ z1}" in allE) apply simp diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/HH.thy --- a/src/ZF/AC/HH.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/HH.thy Wed Jul 10 16:54:07 2002 +0200 @@ -88,14 +88,14 @@ lemma HH_eq_arg_lt: "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v) \ Pow(x)-{0}; v \ w |] ==> P" apply (frule_tac P = "%y. y \ Pow (x) -{0}" in subst, assumption) -apply (drule_tac a = "w" in HH_subset_x_imp_subset_Diff_UN) +apply (drule_tac a = w in HH_subset_x_imp_subset_Diff_UN) apply (drule subst_elem, assumption) apply (fast intro!: singleton_iff [THEN iffD2] equals0I) done lemma HH_eq_imp_arg_eq: "[| HH(f,x,v)=HH(f,x,w); HH(f,x,w) \ Pow(x)-{0}; Ord(v); Ord(w) |] ==> v=w" -apply (rule_tac j = "w" in Ord_linear_lt) +apply (rule_tac j = w in Ord_linear_lt) apply (simp_all (no_asm_simp)) apply (drule subst_elem, assumption) apply (blast dest: ltD HH_eq_arg_lt) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/Hartog.thy --- a/src/ZF/AC/Hartog.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/Hartog.thy Wed Jul 10 16:54:07 2002 +0200 @@ -74,7 +74,7 @@ lemma less_HartogE: "[| i < Hartog(A); i \ Hartog(A) |] ==> P" by (blast intro: less_HartogE1 eqpoll_sym eqpoll_imp_lepoll - lepoll_trans [THEN Hartog_lepoll_selfE]); + lepoll_trans [THEN Hartog_lepoll_selfE]) lemma Card_Hartog: "Card(Hartog(A))" by (fast intro!: CardI Ord_Hartog elim: less_HartogE) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/WO1_WO7.thy --- a/src/ZF/AC/WO1_WO7.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/WO1_WO7.thy Wed Jul 10 16:54:07 2002 +0200 @@ -52,7 +52,7 @@ apply (unfold wf_on_def wf_def) apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption) apply (rule notI) -apply (erule_tac x = "nat" in allE, blast) +apply (erule_tac x = nat in allE, blast) done lemma converse_Memrel_not_well_ord: diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/WO2_AC16.thy --- a/src/ZF/AC/WO2_AC16.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/WO2_AC16.thy Wed Jul 10 16:54:07 2002 +0200 @@ -45,7 +45,7 @@ lemma recfunAC16_Limit: "Limit(i) ==> recfunAC16(f,h,i,a) = (\j F(x); Ord(x) |] ==> z \ F(LEAST i. z \ F(i)) - (\j<(LEAST i. z \ F(i)). F(j))" -by (fast elim: less_LeastE elim!: LeastI); +by (fast elim: less_LeastE elim!: LeastI) lemma Least_eq_imp_ex: "[| (LEAST i. w \ F(i)) = (LEAST i. z \ F(i)); @@ -291,7 +291,7 @@ A\a; y nat |] ==> Union(recfunAC16(f,g,y,a))\a" apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE]) -apply (rule_tac T="A" in Union_lesspoll, simp_all) +apply (rule_tac T=A in Union_lesspoll, simp_all) apply (blast intro!: eqpoll_imp_lepoll) apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel] well_ord_rvimage) @@ -334,7 +334,7 @@ lemma lemma6: "[| \yx Q(x,y)); succ(j) F(j)<=X & (\x Q(x,j))" -by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]); +by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) lemma lemma7: @@ -539,7 +539,7 @@ prefer 2 apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) (** LEVEL 20 **) -apply (drule_tac x1="aa" in spec [THEN mp], assumption) +apply (drule_tac x1=aa in spec [THEN mp], assumption) apply (frule succ_leE) apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/AC/WO6_WO1.thy --- a/src/ZF/AC/WO6_WO1.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/AC/WO6_WO1.thy Wed Jul 10 16:54:07 2002 +0200 @@ -86,7 +86,7 @@ lemma WO1_WO4: "WO1 ==> WO4(1)" apply (unfold WO1_def WO4_def) apply (rule allI) -apply (erule_tac x = "A" in allE) +apply (erule_tac x = A in allE) apply (erule exE) apply (intro exI conjI) apply (erule Ord_ordertype) @@ -124,7 +124,7 @@ lemma lt_oadd_odiff_disj: "[| k < i++j; Ord(i); Ord(j) |] ==> k < i | (~ k NN(y) ==> \a f. Ord(a) & f \ inj(y, a)" apply (unfold NN_def) apply (elim CollectE exE conjE) -apply (rule_tac x = "a" in exI) +apply (rule_tac x = a in exI) apply (rule_tac x = "\x \ y. LEAST i. f`i = {x}" in exI) apply (rule conjI, assumption) apply (rule_tac d = "%i. THE x. x \ f`i" in lam_injective) @@ -519,7 +519,7 @@ apply (rule allI) apply (case_tac "A=0") apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord]) -apply (rule_tac x1 = "A" in lemma_iv [THEN revcut_rl]) +apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl]) apply (erule exE) apply (drule WO6_imp_NN_not_empty) apply (erule Un_subset_iff [THEN iffD1, THEN conjE]) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Coind/ECR.thy --- a/src/ZF/Coind/ECR.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Coind/ECR.thy Wed Jul 10 16:54:07 2002 +0200 @@ -40,8 +40,7 @@ {.y \ ve_dom(ve)} \ Pow({} Un HasTyRel) |] ==> \ HasTyRel" -apply (rule singletonI [THEN HasTyRel.coinduct]) -apply auto +apply (rule singletonI [THEN HasTyRel.coinduct], auto) done (* Specialised elimination rules *) @@ -101,15 +100,13 @@ hastyenv(ve,te); \ ElabRel |] ==> \ HasTyRel" apply (unfold hastyenv_def) -apply (erule elab_fixE) -apply safe +apply (erule elab_fixE, safe) apply (rule subst, assumption) apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI) apply simp_all apply (blast intro: ve_owrI) apply (rule ElabRel.fnI) -apply (simp_all add: ValNEE) -apply force +apply (simp_all add: ValNEE, force) done @@ -143,16 +140,13 @@ apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+) apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+) apply (erule htr_closE) -apply (erule elab_fnE) -apply simp +apply (erule elab_fnE, simp) apply clarify apply (drule spec [THEN spec, THEN mp, THEN mp]) prefer 2 apply assumption+ -apply (rule hastyenv_owr) -apply assumption +apply (rule hastyenv_owr, assumption) apply assumption -apply (simp add: hastyenv_def) -apply blast+ +apply (simp add: hastyenv_def, blast+) done lemma consistency [rule_format]: diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Coind/Map.thy --- a/src/ZF/Coind/Map.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Coind/Map.thy Wed Jul 10 16:54:07 2002 +0200 @@ -105,10 +105,8 @@ lemma pmap_owrI: "[| m \ PMap(A,B); a \ A; b \ B |] ==> map_owr(m,a,b):PMap(A,B)" -apply (unfold map_owr_def PMap_def TMap_def) -apply safe -apply (simp_all add: if_iff) -apply auto +apply (unfold map_owr_def PMap_def TMap_def, safe) +apply (simp_all add: if_iff, auto) (*Remaining subgoal*) apply (rule excluded_middle [THEN disjE]) apply (erule image_Sigma1) @@ -130,8 +128,7 @@ "[| m \ PMap(A,B); a \ domain(m) |] ==> map_app(m,a):B" apply (unfold PMap_def) apply (frule tmap_app_notempty, assumption) -apply (drule tmap_appI) -apply auto +apply (drule tmap_appI, auto) done (** domain **) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Coind/Types.thy --- a/src/ZF/Coind/Types.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Coind/Types.thy Wed Jul 10 16:54:07 2002 +0200 @@ -54,8 +54,7 @@ lemma te_appI: "[| te \ TyEnv; x \ ExVar; x \ te_dom(te) |] ==> te_app(te,x) \ Ty" apply (erule_tac P = "x \ te_dom (te) " in rev_mp) -apply (erule TyEnv.induct) -apply auto +apply (erule TyEnv.induct, auto) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Coind/Values.thy --- a/src/ZF/Coind/Values.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Coind/Values.thy Wed Jul 10 16:54:07 2002 +0200 @@ -42,8 +42,7 @@ lemma ValEnvE: "[| ve \ ValEnv; !!m.[| ve=ve_mk(m); m \ PMap(ExVar,Val) |] ==> Q |] ==> Q" -apply (unfold Part_def Val_def ValEnv_def) -apply (clarify ); +apply (unfold Part_def Val_def ValEnv_def, clarify) apply (erule Val_ValEnv.cases) apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs) done @@ -55,26 +54,22 @@ [| v = v_clos(x,e,ve); x \ ExVar; e \ Exp; ve \ ValEnv |] ==> Q |] ==> Q" -apply (unfold Part_def Val_def ValEnv_def) -apply (clarify ); +apply (unfold Part_def Val_def ValEnv_def, clarify) apply (erule Val_ValEnv.cases) -apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs); +apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs) done (* Nonempty sets *) lemma v_closNE [simp]: "v_clos(x,e,ve) \ 0" -apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs) -apply blast -done +by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast) declare v_closNE [THEN notE, elim!] lemma v_constNE [simp]: "c \ Const ==> v_const(c) \ 0" apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs) -apply (drule constNEE) -apply auto +apply (drule constNEE, auto) done @@ -102,8 +97,7 @@ by (erule ValEnvE, simp add: pmap_appI) lemma ve_domI: "[| ve \ ValEnv; x \ ve_dom(ve) |] ==> x \ ExVar" -apply (erule ValEnvE) -apply (simp ); +apply (erule ValEnvE, simp) apply (blast dest: pmap_domainD) done @@ -115,8 +109,7 @@ lemma ve_owrI: "[|ve \ ValEnv; x \ ExVar; v \ Val |] ==> ve_owr(ve,x,v):ValEnv" -apply (erule ValEnvE) -apply simp +apply (erule ValEnvE, simp) apply (blast intro: pmap_owrI Val_ValEnv.intros) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 10 16:54:07 2002 +0200 @@ -39,7 +39,7 @@ "bnd_mono(D,h) ==> (\n\nat. h^n(0)) <= lfp(D,h)" apply (simp add: UN_subset_iff) apply (rule ballI) -apply (induct_tac x, simp_all) +apply (induct_tac n, simp_all) apply (rule subset_trans [of _ "h(lfp(D,h))"]) apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] ) apply (erule lfp_lemma2) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Wed Jul 10 16:54:07 2002 +0200 @@ -441,7 +441,7 @@ lemma empty_in_DPow: "0 \ DPow(A)" apply (simp add: DPow_def) -apply (rule_tac x="Nil" in bexI) +apply (rule_tac x=Nil in bexI) apply (rule_tac x="Neg(Equal(0,0))" in bexI) apply (auto simp add: Un_least_lt_iff) done @@ -729,7 +729,7 @@ text{*The subset consisting of the ordinals is definable.*} lemma Ords_in_DPow: "Transset(A) ==> {x \ A. Ord(x)} \ DPow(A)" apply (simp add: DPow_def Collect_subset) -apply (rule_tac x="Nil" in bexI) +apply (rule_tac x=Nil in bexI) apply (rule_tac x="ordinal_fm(0)" in bexI) apply (simp_all add: sats_ordinal_fm) done @@ -927,7 +927,7 @@ text{*Kunen's VI, 1.10 *} lemma Lset_in_Lset_succ: "Lset(i) \ Lset(succ(i))"; apply (simp add: Lset_succ DPow_def) -apply (rule_tac x="Nil" in bexI) +apply (rule_tac x=Nil in bexI) apply (rule_tac x="Equal(0,0)" in bexI) apply auto done @@ -998,7 +998,7 @@ apply (rule LsetI [OF succI1]) apply (simp add: DPow_def) apply (intro conjI, clarify) -apply (rule_tac a="x" in UN_I, simp+) +apply (rule_tac a=x in UN_I, simp+) txt{*Now to create the formula @{term "y \ X"} *} apply (rule_tac x="Cons(X,Nil)" in bexI) apply (rule_tac x="subset_fm(0,1)" in bexI) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Wed Jul 10 16:54:07 2002 +0200 @@ -1,9 +1,8 @@ -header {*The Class L Satisfies the ZF Axioms*} +header {*The ZF Axioms (Except Separation) in L*} theory L_axioms = Formula + Relative + Reflection + MetaExists: - -text {* The class L satisfies the premises of locale @{text M_axioms} *} +text {* The class L satisfies the premises of locale @{text M_triv_axioms} *} lemma transL: "[| y\x; L(x) |] ==> L(y)" apply (insert Transset_Lset) @@ -47,7 +46,7 @@ in exI) apply simp apply clarify -apply (rule_tac a="x" in UN_I) +apply (rule_tac a=x in UN_I) apply (simp_all add: Replace_iff univalent_def) apply (blast dest: transL L_I) done @@ -316,7 +315,7 @@ by blast -subsection{*Internalized formulas for some relativized ones*} +subsection{*Internalized Formulas for some Set-Theoretic Concepts*} lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex @@ -341,7 +340,7 @@ "9" == "succ(8)" -subsubsection{*The Empty Set*} +subsubsection{*The Empty Set, Internalized*} constdefs empty_fm :: "i=>i" "empty_fm(x) == Forall(Neg(Member(0,succ(x))))" @@ -373,7 +372,7 @@ done -subsubsection{*Unordered pairs*} +subsubsection{*Unordered Pairs, Internalized*} constdefs upair_fm :: "[i,i,i]=>i" "upair_fm(x,y,z) == @@ -420,7 +419,7 @@ apply (intro FOL_reflections) done -subsubsection{*Ordered pairs*} +subsubsection{*Ordered pairs, Internalized*} constdefs pair_fm :: "[i,i,i]=>i" "pair_fm(x,y,z) == @@ -457,7 +456,7 @@ done -subsubsection{*Binary Unions*} +subsubsection{*Binary Unions, Internalized*} constdefs union_fm :: "[i,i,i]=>i" "union_fm(x,y,z) == @@ -493,7 +492,7 @@ done -subsubsection{*`Cons' for sets*} +subsubsection{*Set ``Cons,'' Internalized*} constdefs cons_fm :: "[i,i,i]=>i" "cons_fm(x,y,z) == @@ -530,7 +529,7 @@ done -subsubsection{*Successor Function*} +subsubsection{*Successor Function, Internalized*} constdefs succ_fm :: "[i,i]=>i" "succ_fm(x,y) == cons_fm(x,x,y)" @@ -564,7 +563,7 @@ done -subsubsection{*Function Applications*} +subsubsection{*Function Application, Internalized*} constdefs fun_apply_fm :: "[i,i,i]=>i" "fun_apply_fm(f,x,y) == @@ -647,7 +646,7 @@ done -subsubsection{*Membership Relation*} +subsubsection{*Membership Relation, Internalized*} constdefs Memrel_fm :: "[i,i]=>i" "Memrel_fm(A,r) == @@ -685,7 +684,7 @@ apply (intro FOL_reflections pair_reflection) done -subsubsection{*Predecessor Set*} +subsubsection{*Predecessor Set, Internalized*} constdefs pred_set_fm :: "[i,i,i,i]=>i" "pred_set_fm(A,x,r,B) == @@ -726,7 +725,7 @@ -subsubsection{*Domain*} +subsubsection{*Domain of a Relation, Internalized*} (* "is_domain(M,r,z) == \x[M]. (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" *) @@ -765,7 +764,7 @@ done -subsubsection{*Range*} +subsubsection{*Range of a Relation, Internalized*} (* "is_range(M,r,z) == \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" *) @@ -804,7 +803,7 @@ done -subsubsection{*Field*} +subsubsection{*Field of a Relation, Internalized*} (* "is_field(M,r,z) == \dr[M]. is_domain(M,r,dr) & @@ -845,7 +844,7 @@ done -subsubsection{*Image*} +subsubsection{*Image under a Relation, Internalized*} (* "image(M,r,A,z) == \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" *) @@ -885,7 +884,7 @@ done -subsubsection{*The Concept of Relation*} +subsubsection{*The Concept of Relation, Internalized*} (* "is_relation(M,r) == (\z[M]. z\r --> (\x[M]. \y[M]. pair(M,x,y,z)))" *) @@ -920,7 +919,7 @@ done -subsubsection{*The Concept of Function*} +subsubsection{*The Concept of Function, Internalized*} (* "is_function(M,r) == \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. @@ -960,7 +959,7 @@ done -subsubsection{*Typed Functions*} +subsubsection{*Typed Functions, Internalized*} (* "typed_function(M,A,B,r) == is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & @@ -1021,7 +1020,7 @@ done -subsubsection{*Composition of Relations*} +subsubsection{*Composition of Relations, Internalized*} (* "composition(M,r,s,t) == \p[M]. p \ t <-> @@ -1066,7 +1065,7 @@ done -subsubsection{*Injections*} +subsubsection{*Injections, Internalized*} (* "injection(M,A,B,f) == typed_function(M,A,B,f) & @@ -1111,7 +1110,7 @@ done -subsubsection{*Surjections*} +subsubsection{*Surjections, Internalized*} (* surjection :: "[i=>o,i,i,i] => o" "surjection(M,A,B,f) == @@ -1154,7 +1153,7 @@ -subsubsection{*Bijections*} +subsubsection{*Bijections, Internalized*} (* bijection :: "[i=>o,i,i,i] => o" "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *) @@ -1190,7 +1189,7 @@ done -subsubsection{*Order-Isomorphisms*} +subsubsection{*Order-Isomorphisms, Internalized*} (* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" "order_isomorphism(M,A,r,B,s,f) == @@ -1246,7 +1245,7 @@ apply (intro FOL_reflections function_reflections bijection_reflection) done -subsubsection{*Limit Ordinals*} +subsubsection{*Limit Ordinals, Internalized*} text{*A limit ordinal is a non-empty, successor-closed ordinal*} diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Wed Jul 10 16:54:07 2002 +0200 @@ -10,5 +10,5 @@ use_thy "Reflection"; use_thy "WF_absolute"; -use_thy "Separation"; +use_thy "Rec_Separation"; use_thy "Datatype_absolute"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Wed Jul 10 16:54:07 2002 +0200 @@ -227,18 +227,20 @@ text{*Congruence rule for separation: can assume the variable is in @{text M}*} lemma separation_cong [cong]: - "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')" + "(!!x. M(x) ==> P(x) <-> P'(x)) + ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))" by (simp add: separation_def) text{*Congruence rules for replacement*} lemma univalent_cong [cong]: "[| A=A'; !!x y. [| x\A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] - ==> univalent(M,A,P) <-> univalent(M,A',P')" + ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))" by (simp add: univalent_def) lemma strong_replacement_cong [cong]: "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] - ==> strong_replacement(M,P) <-> strong_replacement(M,P')" + ==> strong_replacement(M, %x y. P(x,y)) <-> + strong_replacement(M, %x y. P'(x,y))" by (simp add: strong_replacement_def) text{*The extensionality axiom*} @@ -268,7 +270,7 @@ lemma "separation(\x. x \ univ(0), P)" apply (simp add: separation_def, clarify) -apply (rule_tac x = "Collect(x,P)" in bexI) +apply (rule_tac x = "Collect(z,P)" in bexI) apply (blast intro: Collect_in_univ Transset_0)+ done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Wed Jul 10 16:54:07 2002 +0200 @@ -1,9 +1,9 @@ -header{*Some Instances of Separation and Strong Replacement*} - -(*This theory proves all instances needed for locale M_axioms*) +header{*Early Instances of Separation and Strong Replacement*} theory Separation = L_axioms + WF_absolute: +text{*This theory proves all instances needed for locale @{text "M_axioms"}*} + text{*Helps us solve for de Bruijn indices!*} lemma nth_ConsI: "[|nth(n,l) = x; n \ nat|] ==> nth(succ(n), Cons(a,l)) = x" by simp @@ -141,7 +141,7 @@ apply (rename_tac u) apply (rule bex_iff_sats) apply (rule conj_iff_sats) -apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all) +apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done @@ -166,7 +166,7 @@ apply (rename_tac u) apply (rule bex_iff_sats) apply (rule conj_iff_sats) -apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all) +apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done @@ -282,7 +282,7 @@ apply (rename_tac u) apply (rule bex_iff_sats) apply (rule conj_iff_sats) -apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats) +apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done @@ -415,7 +415,7 @@ apply (rule DPowI2) apply (rename_tac u) apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,u,A,B,r]" in mem_iff_sats) +apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done @@ -451,7 +451,7 @@ apply (rule DPowI2) apply (rename_tac u) apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,u,r,f,g,a,b]" in pair_iff_sats) +apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done @@ -628,88 +628,4 @@ declare is_funspace_abs [simp] declare finite_funspace_closed [intro,simp] - -(***NOW FOR THE LOCALE M_TRANCL***) - -subsection{*Separation for Reflexive/Transitive Closure*} - -subsubsection{*First, The Defining Formula*} - -(* "rtran_closure_mem(M,A,r,p) == - \nnat[M]. \n[M]. \n'[M]. - omega(M,nnat) & n\nnat & successor(M,n,n') & - (\f[M]. typed_function(M,n',A,f) & - (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & - fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & - (\j[M]. j\n --> - (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. - fun_apply(M,f,j,fj) & successor(M,j,sj) & - fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r)))"*) -constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" - "rtran_closure_mem_fm(A,r,p) == - Exists(Exists(Exists( - And(omega_fm(2), - And(Member(1,2), - And(succ_fm(1,0), - Exists(And(typed_function_fm(1, A#+4, 0), - And(Exists(Exists(Exists( - And(pair_fm(2,1,p#+7), - And(empty_fm(0), - And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), - Forall(Implies(Member(0,3), - Exists(Exists(Exists(Exists( - And(fun_apply_fm(5,4,3), - And(succ_fm(4,2), - And(fun_apply_fm(5,2,1), - And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" - - -lemma rtran_closure_mem_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> rtran_closure_mem_fm(x,y,z) \ formula" -by (simp add: rtran_closure_mem_fm_def) - -lemma arity_rtran_closure_mem_fm [simp]: - "[| x \ nat; y \ nat; z \ nat |] - ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) - -lemma sats_rtran_closure_mem_fm [simp]: - "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> - rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) - -lemma rtran_closure_mem_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" -by (simp add: sats_rtran_closure_mem_fm) - -theorem rtran_closure_mem_reflection: - "REFLECTS[\x. rtran_closure_mem(L,f(x),g(x),h(x)), - \i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: rtran_closure_mem_def setclass_simps) -apply (intro FOL_reflections function_reflections fun_plus_reflections) -done - -subsubsection{*Then, the Instance of Separation*} - - -text{*This formula describes @{term "rtrancl(r)"}.*} -lemma rtrancl_separation: - "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" -apply (rule separation_CollectI) -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) -apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption) -apply (drule subset_Lset_ltD, assumption) -apply (erule reflection_imp_L_separation) - apply (simp_all add: lt_Ord2) -apply (rule DPowI2) -apply (rename_tac u) -apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats) -apply (rule sep_rules | simp)+ -apply (simp_all add: succ_Un_distrib [symmetric]) -done - - end diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Wed Jul 10 16:54:07 2002 +0200 @@ -21,13 +21,13 @@ by (subst wfrank_def [THEN def_wfrec], simp_all) lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))" -apply (rule_tac a="a" in wf_induct, assumption) +apply (rule_tac a=a in wf_induct, assumption) apply (subst wfrank, assumption) apply (rule Ord_succ [THEN Ord_UN], blast) done lemma wfrank_lt: "[|wf(r); \ r|] ==> wfrank(r,a) < wfrank(r,b)" -apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption) +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption) apply (rule UN_I [THEN ltI]) apply (simp add: Ord_wfrank vimage_iff)+ done @@ -141,8 +141,7 @@ (\x[M]. \y[M]. p = & f`0 = x & f`n = y) & (\i\n. \ r)))" apply (simp add: rtran_closure_mem_def typed_apply_abs - Ord_succ_mem_iff nat_0_le [THEN ltD]) -apply (blast intro: elim:); + Ord_succ_mem_iff nat_0_le [THEN ltD], blast) done locale M_trancl = M_axioms + @@ -159,7 +158,7 @@ "M(r) ==> rtran_closure(M,r,rtrancl(r))" apply (simp add: rtran_closure_def rtran_closure_mem_iff rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def) -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) done lemma (in M_trancl) rtrancl_closed [intro,simp]: @@ -177,7 +176,7 @@ apply (rule M_equalityI) apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def rtran_closure_mem_iff) -apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype) done lemma (in M_trancl) trancl_closed [intro,simp]: @@ -235,10 +234,10 @@ (*NEEDS RELATIVIZATION*) locale M_wfrank = M_trancl + - assumes wfrank_separation': + assumes wfrank_separation: "M(r) ==> - separation - (M, \x. ~ (\f[M]. is_recfun(r^+, x, %x f. range(f), f)))" + separation (M, \x. + ~ (\f[M]. M_is_recfun(M, r^+, x, %mm x f y. y = range(f), f)))" and wfrank_strong_replacement': "M(r) ==> strong_replacement(M, \x z. \y[M]. \f[M]. @@ -247,7 +246,15 @@ and Ord_wfrank_separation: "M(r) ==> separation (M, \x. ~ (\f. M(f) \ - is_recfun(r^+, x, \x. range, f) \ Ord(range(f))))" + is_recfun(r^+, x, \x. range, f) \ Ord(range(f))))" + +lemma (in M_wfrank) wfrank_separation': + "M(r) ==> + separation + (M, \x. ~ (\f[M]. is_recfun(r^+, x, %x f. range(f), f)))" +apply (insert wfrank_separation [of r]) +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym]) +done text{*This function, defined using replacement, is a rank function for well-founded relations within the class M.*} diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Wed Jul 10 16:54:07 2002 +0200 @@ -84,8 +84,8 @@ wellfounded(M,r); trans(r); M(f); M(g); M(r); M(x); M(a); M(b) |] ==> \ r --> \ r --> f`x=g`x" -apply (frule_tac f="f" in is_recfun_type) -apply (frule_tac f="g" in is_recfun_type) +apply (frule_tac f=f in is_recfun_type) +apply (frule_tac f=g in is_recfun_type) apply (simp add: is_recfun_def) apply (erule_tac a=x in wellfounded_induct, assumption+) txt{*Separation to justify the induction*} @@ -107,7 +107,7 @@ wellfounded(M,r); trans(r); M(f); M(g); M(r); \ r |] ==> restrict(f, r-``{b}) = g" -apply (frule_tac f="f" in is_recfun_type) +apply (frule_tac f=f in is_recfun_type) apply (rule fun_extension) apply (blast intro: transD restrict_type2) apply (erule is_recfun_type, simp) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Wed Jul 10 16:54:07 2002 +0200 @@ -141,13 +141,13 @@ lemma (in M_axioms) wf_on_imp_relativized: "wf[A](r) ==> wellfounded_on(M,A,r)" apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) -apply (drule_tac x="x" in spec, blast) +apply (drule_tac x=x in spec, blast) done lemma (in M_axioms) wf_imp_relativized: "wf(r) ==> wellfounded(M,r)" apply (simp add: wellfounded_def wf_def, clarify) -apply (drule_tac x="x" in spec, blast) +apply (drule_tac x=x in spec, blast) done lemma (in M_axioms) well_ord_imp_relativized: @@ -480,8 +480,8 @@ apply (insert omap_funtype [of A r f B i]) apply (auto simp add: bij_def inj_def) prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) -apply (frule_tac a="w" in apply_Pair, assumption) -apply (frule_tac a="x" in apply_Pair, assumption) +apply (frule_tac a=w in apply_Pair, assumption) +apply (frule_tac a=x in apply_Pair, assumption) apply (simp add: omap_iff) apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) done @@ -494,8 +494,8 @@ apply (rule ord_isoI) apply (erule wellordered_omap_bij, assumption+) apply (insert omap_funtype [of A r f B i], simp) -apply (frule_tac a="x" in apply_Pair, assumption) -apply (frule_tac a="y" in apply_Pair, assumption) +apply (frule_tac a=x in apply_Pair, assumption) +apply (frule_tac a=y in apply_Pair, assumption) apply (auto simp add: omap_iff) txt{*direction 1: assuming @{term "\x,y\ \ r"}*} apply (blast intro: ltD ord_iso_pred_imp_lt) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Induct/Multiset.ML Wed Jul 10 16:54:07 2002 +0200 @@ -831,8 +831,8 @@ by (auto_tac (claset(), simpset() addsimps [])); by (ALLGOALS(asm_full_simp_tac(simpset() addsimps [Un_subset_iff, Mult_iff_multiset]))); -by (res_inst_tac [("x", "x")] bexI 3); -by (res_inst_tac [("x", "xb")] bexI 3); +by (res_inst_tac [("x", "a")] bexI 3); +by (res_inst_tac [("x", "M0")] bexI 3); by (Asm_simp_tac 3); by (res_inst_tac [("x", "K")] bexI 3); by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset]))); @@ -841,8 +841,8 @@ Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)"; by (auto_tac (claset(), simpset() addsimps [])); -by (res_inst_tac [("x", "x")] bexI 1); -by (res_inst_tac [("x", "xb")] bexI 1); +by (res_inst_tac [("x", "a")] bexI 1); +by (res_inst_tac [("x", "M0")] bexI 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]))); by (res_inst_tac [("x", "K")] bexI 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]))); diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Induct/Primrec.thy --- a/src/ZF/Induct/Primrec.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Induct/Primrec.thy Wed Jul 10 16:54:07 2002 +0200 @@ -214,7 +214,7 @@ "[| i1 \ nat; i2 \ nat; j \ nat |] ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)" -- {* PROPERTY A 11 *} - apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans) + apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans) apply (simp add: ack_2) apply (rule_tac [2] ack_nest_bound [THEN lt_trans2]) apply (rule add_le_mono [THEN leI, THEN leI]) @@ -265,7 +265,7 @@ apply (simp add: nat_0_le) apply simp apply (rule ballI) - apply (erule_tac n = "x" in natE) + apply (erule_tac n = i in natE) apply (simp add: add_le_self) apply simp apply (erule bspec [THEN lt_trans2]) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Integ/IntDiv.ML --- a/src/ZF/Integ/IntDiv.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Integ/IntDiv.ML Wed Jul 10 16:54:07 2002 +0200 @@ -61,7 +61,7 @@ by (dtac zero_zless_imp_znegative_zminus 1); by (dtac zneg_int_of 2); by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation])); -by (subgoal_tac "0 < zmagnitude($# succ(x))" 1); +by (subgoal_tac "0 < zmagnitude($# succ(n))" 1); by (Asm_full_simp_tac 1); by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1); by (Asm_full_simp_tac 1); @@ -79,9 +79,9 @@ by (cut_inst_tac [("m","m")] int_succ_int_1 1); by (cut_inst_tac [("m","n")] int_succ_int_1 1); by (Asm_full_simp_tac 1); -by (eres_inst_tac [("n","x")] natE 1); +by (etac natE 1); by Auto_tac; -by (res_inst_tac [("x","succ(x)")] bexI 1); +by (res_inst_tac [("x","succ(n)")] bexI 1); by Auto_tac; qed "zless_add_succ_iff"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/IsaMakefile Wed Jul 10 16:54:07 2002 +0200 @@ -82,7 +82,8 @@ Constructible/Formula.thy Constructible/Relative.thy \ Constructible/L_axioms.thy Constructible/Wellorderings.thy \ Constructible/MetaExists.thy Constructible/Normal.thy \ - Constructible/Separation.thy Constructible/WF_absolute.thy \ + Constructible/Rec_Separation.thy Constructible/Separation.thy \ + Constructible/WF_absolute.thy \ Constructible/Reflection.thy Constructible/WFrec.thy \ Constructible/document/root.tex @$(ISATOOL) usedir $(OUT)/ZF Constructible diff -r 20ca66539bef -r 0f89104dd377 src/ZF/List.thy --- a/src/ZF/List.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/List.thy Wed Jul 10 16:54:07 2002 +0200 @@ -597,7 +597,7 @@ apply simp_all txt{*Inductive step*} apply clarify -apply (erule_tac a = xa in list.cases, simp_all) +apply (erule_tac a=ys in list.cases, simp_all) done @@ -761,8 +761,8 @@ apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib) apply clarify (*Both lists are non-empty*) -apply (erule_tac a="xa" in list.cases, simp) -apply (erule_tac a="xb" in list.cases, clarify) +apply (erule_tac a="xs" in list.cases, simp) +apply (erule_tac a="ys" in list.cases, clarify) apply (simp (no_asm_use) ) apply clarify apply (simp (no_asm_simp)) @@ -847,7 +847,7 @@ apply (induct_tac xs) apply simp_all apply (blast intro: list_mono [THEN subsetD], clarify) -apply (erule_tac a=x in list.cases , auto) +apply (erule_tac a=ys in list.cases , auto) apply (blast intro: list_mono [THEN subsetD]) done @@ -875,7 +875,7 @@ apply (unfold min_def) apply (induct_tac "xs", simp_all) apply clarify -apply (erule_tac a = "x" in list.cases, auto) +apply (erule_tac a = ys in list.cases, auto) done lemma zip_append1 [rule_format]: @@ -1011,13 +1011,13 @@ list_update(ys, i, snd(xy)))" apply (induct_tac "ys") apply auto -apply (erule_tac a = "xc" in list.cases) +apply (erule_tac a = "xs" in list.cases) apply (auto elim: natE) done lemma set_update_subset_cons [rule_format]: - "xs:list(A) ==> \i \ nat. set_of_list(list_update(xs, i, x)) - <= cons(x, set_of_list(xs))" + "xs:list(A) ==> + \i \ nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))" apply (induct_tac "xs") apply simp apply (rule ballI) @@ -1121,13 +1121,13 @@ apply simp apply (subst map_succ_upt [symmetric], simp_all) apply clarify -apply (subgoal_tac "xa < length (upt (0, x))") +apply (subgoal_tac "i < length (upt (0, x))") prefer 2 apply (simp add: less_diff_conv) - apply (rule_tac j = "succ (xa #+ y) " in lt_trans2) + apply (rule_tac j = "succ (i #+ y) " in lt_trans2) apply simp apply simp -apply (subgoal_tac "xa < length (upt (y, x))") +apply (subgoal_tac "i < length (upt (y, x))") apply (simp_all add: add_commute less_diff_conv) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/OrdQuant.thy Wed Jul 10 16:54:07 2002 +0200 @@ -232,8 +232,7 @@ (*Congruence rule for rewriting*) lemma rall_cong [cong]: - "(!!x. M(x) ==> P(x) <-> P'(x)) - ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))" + "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (ALL x[M]. P(x)) <-> (ALL x[M]. P'(x))" by (simp add: rall_def) @@ -258,8 +257,7 @@ by (simp add: rex_def) lemma rex_cong [cong]: - "(!!x. M(x) ==> P(x) <-> P'(x)) - ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))" + "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (EX x[M]. P(x)) <-> (EX x[M]. P'(x))" by (simp add: rex_def cong: conj_cong) lemma rall_is_ball [simp]: "(\x[%z. z\A]. P(x)) <-> (\x\A. P(x))" diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Order.thy --- a/src/ZF/Order.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Order.thy Wed Jul 10 16:54:07 2002 +0200 @@ -321,7 +321,7 @@ lemma linear_ord_iso: "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)" apply (simp add: linear_def ord_iso_def, safe) -apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec]) +apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec]) apply (safe elim!: bij_is_fun [THEN apply_type]) apply (drule_tac t = "op ` (converse (f))" in subst_context) apply (simp add: left_inverse_bij) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/OrderType.thy --- a/src/ZF/OrderType.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/OrderType.thy Wed Jul 10 16:54:07 2002 +0200 @@ -619,7 +619,7 @@ apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) apply (force simp add: Union_empty_iff oadd_eq_0_iff Limit_is_Ord [of j, THEN Ord_in_Ord], auto) -apply (rule_tac x="succ(x)" in bexI) +apply (rule_tac x="succ(y)" in bexI) apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) apply (simp add: Limit_def lt_def) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Resid/Confluence.thy --- a/src/ZF/Resid/Confluence.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Resid/Confluence.thy Wed Jul 10 16:54:07 2002 +0200 @@ -25,8 +25,7 @@ "[|confluence(Spar_red1)|]==> strip" apply (unfold confluence_def strip_def) apply (rule impI [THEN allI, THEN allI]) -apply (erule Spar_red.induct) -apply fast +apply (erule Spar_red.induct, fast) apply (fast intro: Spar_red.trans) done @@ -35,8 +34,7 @@ "strip==> confluence(Spar_red)" apply (unfold confluence_def strip_def) apply (rule impI [THEN allI, THEN allI]) -apply (erule Spar_red.induct) -apply blast +apply (erule Spar_red.induct, blast) apply clarify apply (blast intro: Spar_red.trans) done @@ -47,12 +45,10 @@ lemma parallel_moves: "confluence(Spar_red1)" -apply (unfold confluence_def) -apply clarify +apply (unfold confluence_def, clarify) apply (frule simulation) -apply (frule_tac n = "z" in simulation) -apply clarify -apply (frule_tac v = "va" in paving) +apply (frule_tac n = z in simulation, clarify) +apply (frule_tac v = va in paving) apply (force intro: completeness)+ done @@ -60,8 +56,7 @@ parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard] lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)" -apply (unfold confluence_def, blast intro: par_red_red red_par_red) -done +by (unfold confluence_def, blast intro: par_red_red red_par_red) lemmas confluence_beta_reduction = confluence_parallel_reduction [THEN lemma1, standard] @@ -100,8 +95,7 @@ lemma conv_sym: "m<--->n ==> n<--->m" apply (erule Sconv.induct) -apply (erule Sconv1.induct) -apply blast+ +apply (erule Sconv1.induct, blast+) done (* ------------------------------------------------------------------------- *) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Resid/Redex.thy --- a/src/ZF/Resid/Redex.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Resid/Redex.thy Wed Jul 10 16:54:07 2002 +0200 @@ -12,7 +12,7 @@ datatype "redexes" = Var ("n \ nat") | Fun ("t \ redexes") - | App ("b \ bool" ,"f \ redexes" , "a \ redexes") + | App ("b \ bool","f \ redexes", "a \ redexes") consts @@ -75,7 +75,7 @@ type_intros redexes.intros bool_typechecks inductive - domains "Sreg" <= "redexes" + domains "Sreg" <= redexes intros Reg_Var: "n \ nat ==> regular(Var(n))" Reg_Fun: "[|regular(u)|]==> regular(Fun(u))" @@ -161,14 +161,12 @@ lemma union_l: "u ~ v ==> u <== (u un v)" apply (erule Scomp.induct) -apply (erule_tac [3] boolE) -apply simp_all +apply (erule_tac [3] boolE, simp_all) done lemma union_r: "u ~ v ==> v <== (u un v)" apply (erule Scomp.induct) -apply (erule_tac [3] c = "b2" in boolE) -apply simp_all +apply (erule_tac [3] c = b2 in boolE, simp_all) done lemma union_sym: "u ~ v ==> u un v = v un u" @@ -180,8 +178,7 @@ lemma union_preserve_regular [rule_format]: "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)" -apply (erule Scomp.induct) -apply auto +apply (erule Scomp.induct, auto) (*select the given assumption for simplification*) apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp) apply simp diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Resid/Reduction.thy --- a/src/ZF/Resid/Reduction.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Resid/Reduction.thy Wed Jul 10 16:54:07 2002 +0200 @@ -18,7 +18,7 @@ "Apl(n,m)" == "App(0,n,m)" inductive - domains "lambda" <= "redexes" + domains "lambda" <= redexes intros Lambda_Var: " n \ nat ==> Var(n) \ lambda" Lambda_Fun: " u \ lambda ==> Fun(u) \ lambda" @@ -156,20 +156,17 @@ lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)" apply (erule Sred.induct) -apply (rule_tac [3] Sred.trans) -apply simp_all +apply (rule_tac [3] Sred.trans, simp_all) done lemma red_Apll: "[|n \ lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)" apply (erule Sred.induct) -apply (rule_tac [3] Sred.trans) -apply simp_all +apply (rule_tac [3] Sred.trans, simp_all) done lemma red_Aplr: "[|n \ lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')" apply (erule Sred.induct) -apply (rule_tac [3] Sred.trans) -apply simp_all +apply (rule_tac [3] Sred.trans, simp_all) done lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')" @@ -179,7 +176,7 @@ lemma red_beta: "[|m \ lambda; m':lambda; n \ lambda; n':lambda; m ---> m'; n--->n'|] ==> Apl(Fun(m),n)---> n'/m'" -apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans) +apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans) apply (simp_all add: red_Apl red_Fun) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Resid/Residuals.thy --- a/src/ZF/Resid/Residuals.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Resid/Residuals.thy Wed Jul 10 16:54:07 2002 +0200 @@ -82,8 +82,7 @@ lemma comp_resfuncD: "[| u~v; regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))" -apply (frule residuals_intro, assumption) -apply clarify +apply (frule residuals_intro, assumption, clarify) apply (subst the_equality) apply (blast intro: residuals_function)+ done @@ -119,8 +118,7 @@ lemma resfunc_type [simp]: "[|s~t; regular(t)|]==> regular(t) --> s |> t \ redexes" -apply (erule Scomp.induct) -apply auto +apply (erule Scomp.induct, auto) apply (drule_tac psi = "Fun (?u) |> ?v \ redexes" in asm_rl) apply auto done @@ -138,19 +136,16 @@ lemma residuals_lift_rec: "[|u~v; k \ nat|]==> regular(v)--> (\n \ nat. lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))" -apply (erule Scomp.induct) -apply safe +apply (erule Scomp.induct, safe) apply (simp_all add: lift_rec_Var subst_Var lift_subst) -apply (rotate_tac -2) -apply simp +apply (rotate_tac -2, simp) done lemma residuals_subst_rec: "u1~u2 ==> \v1 v2. v1~v2 --> regular(v2) --> regular(u2) --> (\n \ nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = subst_rec(v1 |> v2, u1 |> u2,n))" -apply (erule Scomp.induct) -apply safe +apply (erule Scomp.induct, safe) apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec) apply (drule_tac psi = "\x.?P (x) " in asm_rl) apply (simp add: substitution) @@ -173,8 +168,7 @@ lemma residuals_preserve_reg [rule_format, simp]: "u~v ==> regular(u) --> regular(v) --> regular(u|>v)" -apply (erule Scomp.induct) -apply auto +apply (erule Scomp.induct, auto) apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+ done @@ -187,8 +181,7 @@ lemma preservation [rule_format]: "u ~ v ==> regular(v) --> u|>v = (u un v)|>v" -apply (erule Scomp.induct) -apply safe +apply (erule Scomp.induct, safe) apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl) apply (auto simp add: union_preserve_comp comp_sym_iff) done @@ -208,15 +201,13 @@ "v<==u ==> regular(u) --> (\w. w~v --> w~u --> w |> u = (w|>v) |> (u|>v))" -apply (erule Ssub.induct) -apply force+ +apply (erule Ssub.induct, force+) done lemma prism: "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)" apply (rule prism_l) -apply (rule_tac [4] comp_trans) -apply auto +apply (rule_tac [4] comp_trans, auto) done @@ -226,13 +217,12 @@ lemma cube: "[|u~v; regular(v); regular(u); w~u|]==> (w|>u) |> (v|>u) = (w|>v) |> (u|>v)" -apply (subst preservation , assumption , assumption) -apply (subst preservation , erule comp_sym , assumption) +apply (subst preservation, assumption, assumption) +apply (subst preservation, erule comp_sym, assumption) apply (subst prism [symmetric]) apply (simp add: union_r comp_sym_iff) apply (simp add: union_preserve_regular comp_sym_iff) -apply (erule comp_trans) -apply assumption +apply (erule comp_trans, assumption) apply (simp add: prism [symmetric] union_l union_preserve_regular comp_sym_iff union_sym) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Resid/Substitution.thy --- a/src/ZF/Resid/Substitution.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/Resid/Substitution.thy Wed Jul 10 16:54:07 2002 +0200 @@ -151,8 +151,7 @@ "u \ redexes ==> \n \ nat. \i \ nat. i\n --> (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))" -apply (erule redexes.induct) -apply auto +apply (erule redexes.induct, auto) apply (case_tac "n < i") apply (frule lt_trans2, assumption) apply (simp_all add: lift_rec_Var leI) @@ -173,11 +172,11 @@ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)" apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift) apply safe -apply (case_tac "n < x") - apply (frule_tac j = "x" in lt_trans2, assumption) - apply (simp add: leI) -apply simp -apply (erule_tac j = "n" in leE) +apply (rename_tac n n' m u) +apply (case_tac "n < n'") + apply (frule_tac j = n' in lt_trans2, assumption) + apply (simp add: leI, simp) +apply (erule_tac j=n in leE) apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt) done @@ -193,12 +192,13 @@ \n \ nat. \m \ nat. \u \ redexes. m\n--> lift_rec(subst_rec(u,v,n),m) = subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))" -apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift) +apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift) apply safe -apply (case_tac "n < x") -apply (case_tac "n < xa") +apply (rename_tac n n' m u) +apply (case_tac "n < n'") +apply (case_tac "n < m") apply (simp_all add: leI) -apply (erule_tac i = "x" in leE) +apply (erule_tac i=n' in leE) apply (frule lt_trans1, assumption) apply (simp_all add: succ_pred leI gt_pred) done @@ -207,10 +207,8 @@ lemma subst_rec_lift_rec [rule_format]: "u \ redexes ==> \n \ nat. \v \ redexes. subst_rec(v,lift_rec(u,n),n) = u" -apply (erule redexes.induct) -apply auto -apply (case_tac "n < na") -apply auto +apply (erule redexes.induct, auto) +apply (case_tac "n < na", auto) done lemma subst_rec_subst_rec [rule_format]: @@ -219,21 +217,21 @@ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) = subst_rec(w,subst_rec(u,v,m),n)" apply (erule redexes.induct) -apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt) -apply safe -apply (case_tac "n\succ (xa) ") - apply (erule_tac i = "n" in leE) +apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe) +apply (rename_tac n' u w) +apply (case_tac "n \ succ(n') ") + apply (erule_tac i = n in leE) apply (simp_all add: succ_pred subst_rec_lift_rec leI) - apply (case_tac "n < x") - apply (frule lt_trans2 , assumption, simp add: gt_pred) + apply (case_tac "n < m") + apply (frule lt_trans2, assumption, simp add: gt_pred) apply simp - apply (erule_tac j = "n" in leE, simp add: gt_pred) + apply (erule_tac j = n in leE, simp add: gt_pred) apply (simp add: subst_rec_lift_rec) (*final case*) -apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption) +apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption) apply (erule leE) - apply (frule succ_leI [THEN lt_trans] , assumption) - apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans], + apply (frule succ_leI [THEN lt_trans], assumption) + apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans], assumption) apply (simp_all add: succ_pred lt_pred) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/Comp.ML --- a/src/ZF/UNITY/Comp.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/UNITY/Comp.ML Wed Jul 10 16:54:07 2002 +0200 @@ -71,7 +71,9 @@ by (Force_tac 1); by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); by Auto_tac; -by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2); +by (Blast_tac 1); +by (rename_tac "y" 1); +by (dres_inst_tac [("c", "y"), ("A", "AllowedActs(H)")] subsetD 1); by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1)); qed "JN_component_iff"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/GenPrefix.ML --- a/src/ZF/UNITY/GenPrefix.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/UNITY/GenPrefix.ML Wed Jul 10 16:54:07 2002 +0200 @@ -317,12 +317,15 @@ by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj]))); by (Clarify_tac 1); -by (case_tac "x=[]" 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff]))); +by (eres_inst_tac [("a","ys")] list.elim 1); +by (ALLGOALS Asm_full_simp_tac); by (Clarify_tac 1); -by (dres_inst_tac [("x", "ys")] bspec 1); +by (rename_tac "zs" 1); +by (dres_inst_tac [("x", "zs")] bspec 1); by (ALLGOALS(Clarify_tac)); -by Auto_tac; +(*Faster than Auto_tac*) +by (rtac conjI 1); +by (REPEAT (Force_tac 1)); qed_spec_mp "nth_imp_gen_prefix"; Goal "(: gen_prefix(A,r)) <-> \ @@ -484,7 +487,7 @@ by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1); by Safe_tac; by (Blast_tac 1); -by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1); +by (subgoal_tac "length(xs) #+ (i #- length(xs)) = i" 1); by (stac nth_drop 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI]))); by (rtac (nat_diff_split RS iffD2) 1); @@ -501,8 +504,7 @@ by (Asm_full_simp_tac 1); by (dres_inst_tac [("psi", "ya:list(A)")] asm_rl 1); by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() addsimps - [app_type, app_assoc RS sym] delsimps [app_assoc]) 1); +by (asm_full_simp_tac (simpset() addsimps [app_type, app_assoc RS sym]) 1); by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type])); qed "prefix_snoc"; Addsimps [prefix_snoc]; @@ -514,13 +516,11 @@ by (etac list_append_induct 1); by (Clarify_tac 2); by (rtac iffI 2); -by (asm_full_simp_tac (simpset() delsimps [app_assoc] - addsimps [app_assoc RS sym]) 2); +by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2); by (etac disjE 2 THEN etac disjE 3); by (rtac disjI2 2); by (res_inst_tac [("x", "y @ [x]")] exI 2); -by (asm_full_simp_tac (simpset() delsimps [app_assoc] - addsimps [app_assoc RS sym]) 2); +by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2); by (REPEAT(Force_tac 1)); qed_spec_mp "prefix_append_iff"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/Guar.ML --- a/src/ZF/UNITY/Guar.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/UNITY/Guar.ML Wed Jul 10 16:54:07 2002 +0200 @@ -277,7 +277,7 @@ by (Simp_tac 1); by Safe_tac; by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); -by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1); +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); by (asm_simp_tac (simpset() addsimps Join_ac) 1); qed "guarantees_Join_Int"; @@ -288,9 +288,9 @@ by (Simp_tac 1); by Safe_tac; by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); -by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1); +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); by (rotate_tac 4 1); -by (dres_inst_tac [("x", "F Join x")] bspec 1); +by (dres_inst_tac [("x", "F Join Ga")] bspec 1); by (Simp_tac 1); by (force_tac (claset(), simpset() addsimps [ok_commute]) 1); by (asm_simp_tac (simpset() addsimps Join_ac) 1); @@ -315,11 +315,12 @@ "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F) |] \ \ ==> JOIN(I,F) : (UN i:I. X(i)) guarantees (UN i:I. Y(i))"; by Auto_tac; -by (dres_inst_tac [("x", "xa")] bspec 1); +by (dres_inst_tac [("x", "y")] bspec 1); by (ALLGOALS(Asm_full_simp_tac)); by Safe_tac; by (rotate_tac ~1 1); -by (dres_inst_tac [("x", "JOIN(I-{xa}, F) Join x")] bspec 1); +by (rename_tac "G y" 1); +by (dres_inst_tac [("x", "JOIN(I-{y}, F) Join G")] bspec 1); by (auto_tac (claset() addIs [OK_imp_ok], simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); @@ -441,18 +442,15 @@ by Auto_tac; qed "wx_subset"; -Goal -"ex_prop(wx(X))"; -by (full_simp_tac (simpset() - addsimps [ex_prop_def, wx_def]) 1); +Goal "ex_prop(wx(X))"; +by (full_simp_tac (simpset() addsimps [ex_prop_def, wx_def]) 1); by Safe_tac; by (Blast_tac 1); -by (ALLGOALS(res_inst_tac [("x", "xb")] bexI)); +by (ALLGOALS(res_inst_tac [("x", "x")] bexI)); by (REPEAT(Force_tac 1)); qed "wx_ex_prop"; -Goalw [wx_def] -"ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)"; +Goalw [wx_def] "ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)"; by Auto_tac; qed "wx_weakest"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/ListPlus.ML --- a/src/ZF/UNITY/ListPlus.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/UNITY/ListPlus.ML Wed Jul 10 16:54:07 2002 +0200 @@ -335,16 +335,13 @@ (** More on lists **) -Goal -"n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \ -\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"; +Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \ +\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"; by (induct_tac "n" 1); -by (ALLGOALS(Asm_full_simp_tac)); +by (Asm_full_simp_tac 1); by (Clarify_tac 1); -by (case_tac "xb=Nil" 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff]))); -by (Clarify_tac 1); -by (auto_tac (claset() addSEs [ConsE], simpset())); +by (etac list.elim 1); +by Auto_tac; qed_spec_mp "nth_drop"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/UNITY/Union.ML Wed Jul 10 16:54:07 2002 +0200 @@ -251,15 +251,15 @@ Goalw [constrains_def, JOIN_def,st_set_def] "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)"; by Auto_tac; -by (cut_inst_tac [("F","F(xa)")] Acts_type 1); by (Blast_tac 2); -by (dres_inst_tac [("x", "xb")] bspec 1); +by (rename_tac "j act y z" 1); +by (cut_inst_tac [("F","F(j)")] Acts_type 1); +by (dres_inst_tac [("x", "act")] bspec 1); by Auto_tac; qed "JN_constrains"; Goal "(F Join G : A co B) <-> (programify(F):A co B & programify(G):A co B)"; -by (auto_tac - (claset(), simpset() addsimps [constrains_def])); +by (auto_tac (claset(), simpset() addsimps [constrains_def])); qed "Join_constrains"; Goal "(F Join G : A unless B) <-> \ @@ -288,7 +288,8 @@ by (cut_facts_tac [minor] 1); by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); by (Clarify_tac 1); -by (forw_inst_tac [("i", "x")] major 1); +by (rename_tac "j" 1); +by (forw_inst_tac [("i", "j")] major 1); by (ftac constrainsD2 1); by (Asm_full_simp_tac 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); @@ -298,8 +299,8 @@ by (asm_simp_tac (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1); by Auto_tac; -by (cut_inst_tac [("F", "F(xa)")] Acts_type 1); -by (dres_inst_tac [("x","xb")] bspec 1); +by (cut_inst_tac [("F", "F(i)")] Acts_type 1); +by (dres_inst_tac [("x","act")] bspec 1); by Auto_tac; qed "JN_stable"; @@ -366,7 +367,7 @@ by (auto_tac (claset(), simpset() addsimps [transient_def, JOIN_def])); by (rewtac st_set_def); -by (dres_inst_tac [("x", "xb")] bspec 2); +by (dres_inst_tac [("x", "act")] bspec 2); by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "JN_transient"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ZF.ML --- a/src/ZF/ZF.ML Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ZF.ML Wed Jul 10 16:54:07 2002 +0200 @@ -57,7 +57,8 @@ (*Congruence rule for rewriting*) val prems= Goalw [Ball_def] - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"; + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] \ +\ ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"; by (simp_tac (FOL_ss addsimps prems) 1) ; qed "ball_cong"; @@ -95,8 +96,8 @@ Addsimps [bex_triv]; val prems= Goalw [Bex_def] - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \ -\ |] ==> Bex(A,P) <-> Bex(A',P')"; + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] \ +\ ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"; by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ; qed "bex_cong"; diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/Commutation.thy --- a/src/ZF/ex/Commutation.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/Commutation.thy Wed Jul 10 16:54:07 2002 +0200 @@ -39,8 +39,7 @@ lemma square_rtrancl [rule_format]: "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)" -apply (unfold square_def) -apply clarify +apply (unfold square_def, clarify) apply (erule rtrancl_induct) apply (blast intro: rtrancl_refl) apply (blast intro: rtrancl_into_rtrancl) @@ -50,8 +49,7 @@ lemma diamond_strip: "diamond(r) ==> strip(r)" apply (unfold diamond_def commute_def strip_def) -apply (rule square_rtrancl) -apply simp_all +apply (rule square_rtrancl, simp_all) done (*** commute ***) @@ -62,8 +60,7 @@ lemma commute_rtrancl [rule_format]: "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)" -apply (unfold commute_def) -apply clarify +apply (unfold commute_def, clarify) apply (rule square_rtrancl) apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) apply (simp_all add: rtrancl_field) @@ -89,24 +86,21 @@ lemma diamond_confluent: "diamond(r) ==> confluent(r)" apply (unfold diamond_def confluent_def) -apply (erule commute_rtrancl) -apply simp +apply (erule commute_rtrancl, simp) done lemma confluent_Un: "[| confluent(r); confluent(s); commute(r^*, s^*); relation(r); relation(s) |] ==> confluent(r Un s)" apply (unfold confluent_def) -apply (rule rtrancl_Un_rtrancl [THEN subst]) -apply auto +apply (rule rtrancl_Un_rtrancl [THEN subst], auto) apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) done lemma diamond_to_confluence: "[| diamond(r); s \ r; r<= s^* |] ==> confluent(s)" -apply (drule rtrancl_subset [symmetric]) -apply assumption +apply (drule rtrancl_subset [symmetric], assumption) apply (simp_all add: confluent_def) apply (blast intro: diamond_confluent [THEN confluentD]) done @@ -117,13 +111,12 @@ lemma Church_Rosser1: "Church_Rosser(r) ==> confluent(r)" apply (unfold confluent_def Church_Rosser_def square_def - commute_def diamond_def) -apply auto + commute_def diamond_def, auto) apply (drule converseI) apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) -apply (drule_tac x = "b" in spec) -apply (drule_tac x1 = "c" in spec [THEN mp]) -apply (rule_tac b = "a" in rtrancl_trans) +apply (drule_tac x = b in spec) +apply (drule_tac x1 = c in spec [THEN mp]) +apply (rule_tac b = a in rtrancl_trans) apply (blast intro: rtrancl_mono [THEN subsetD])+ done @@ -131,12 +124,10 @@ lemma Church_Rosser2: "confluent(r) ==> Church_Rosser(r)" apply (unfold confluent_def Church_Rosser_def square_def - commute_def diamond_def) -apply auto + commute_def diamond_def, auto) apply (frule fieldI1) apply (simp add: rtrancl_field) -apply (erule rtrancl_induct) -apply auto +apply (erule rtrancl_induct, auto) apply (blast intro: rtrancl_refl) apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/LList.thy --- a/src/ZF/ex/LList.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/LList.thy Wed Jul 10 16:54:07 2002 +0200 @@ -143,18 +143,15 @@ apply (erule trans_induct) apply (intro allI impI) apply (erule lleq.cases) -apply (unfold QInr_def llist.con_defs) -apply safe +apply (unfold QInr_def llist.con_defs, safe) apply (fast elim!: Ord_trans bspec [elim_format]) done (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) lemma lleq_symmetric: " \ lleq(A) ==> \ lleq(A)" apply (erule lleq.coinduct [OF converseI]) -apply (rule lleq.dom_subset [THEN converse_type]) -apply safe -apply (erule lleq.cases) -apply blast+ +apply (rule lleq.dom_subset [THEN converse_type], safe) +apply (erule lleq.cases, blast+) done lemma lleq_implies_equal: " \ lleq(A) ==> l=l'" @@ -168,8 +165,7 @@ apply (rule_tac X = "{. l \ llist (A) }" in lleq.coinduct) apply blast apply safe -apply (erule_tac a="l" in llist.cases) -apply fast+ +apply (erule_tac a=l in llist.cases, fast+) done @@ -220,25 +216,21 @@ "Ord(i) ==> \l \ llist(bool). flip(l) Int Vset(i) \ univ(eclose(bool))" apply (erule trans_induct) apply (rule ballI) -apply (erule llist.cases) -apply (simp_all) +apply (erule llist.cases, simp_all) apply (simp_all add: QInl_def QInr_def llist.con_defs) (*LCons case: I simply can't get rid of the deepen_tac*) apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1") done lemma flip_in_quniv: "l \ llist(bool) ==> flip(l) \ quniv(bool)" -apply (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI]) -apply assumption+ -done +by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+) lemma flip_type: "l \ llist(bool) ==> flip(l): llist(bool)" apply (rule_tac X = "{flip (l) . l \ llist (bool) }" in llist.coinduct) apply blast apply (fast intro!: flip_in_quniv) apply (erule RepFunE) -apply (erule_tac a="la" in llist.cases) -apply auto +apply (erule_tac a=la in llist.cases, auto) done lemma flip_flip: "l \ llist(bool) ==> flip(flip(l)) = l" @@ -247,7 +239,7 @@ apply blast apply (fast intro!: flip_type) apply (erule RepFunE) -apply (erule_tac a="la" in llist.cases) +apply (erule_tac a=la in llist.cases) apply (simp_all add: flip_type not_not) done diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/Limit.thy Wed Jul 10 16:54:07 2002 +0200 @@ -748,8 +748,7 @@ lemma cf_least: "[|cpo(D); pcpo(E); y \ cont(D,E)|]==>rel(cf(D,E),(\x \ set(D).bot(E)),y)" -apply (rule rel_cfI, simp) -apply typecheck +apply (rule rel_cfI, simp, typecheck) done lemma pcpo_cf: diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/Primes.thy Wed Jul 10 16:54:07 2002 +0200 @@ -31,9 +31,7 @@ (************************************************) lemma dvdD: "m dvd n ==> m \ nat & n \ nat & (\k \ nat. n = m#*k)" -apply (unfold divides_def) -apply assumption -done +by (unfold divides_def, assumption) lemma dvdE: "[|m dvd n; !!k. [|m \ nat; n \ nat; k \ nat; n = m#*k|] ==> P|] ==> P" @@ -69,13 +67,11 @@ lemma dvd_mult_left: "[|(i#*j) dvd k; i \ nat|] ==> i dvd k" apply (unfold divides_def) -apply (simp add: mult_assoc) -apply blast +apply (simp add: mult_assoc, blast) done lemma dvd_mult_right: "[|(i#*j) dvd k; j \ nat|] ==> j dvd k" -apply (unfold divides_def) -apply clarify +apply (unfold divides_def, clarify) apply (rule_tac x = "i#*k" in bexI) apply (simp add: mult_ac) apply (rule mult_type) @@ -90,8 +86,7 @@ lemma gcd_0 [simp]: "gcd(m,0) = natify(m)" apply (unfold gcd_def) -apply (subst transrec) -apply simp +apply (subst transrec, simp) done lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)" @@ -109,7 +104,7 @@ done lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)" -apply (cut_tac m = "m" and n = "natify (n) " in gcd_non_0_raw) +apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw) apply auto done @@ -155,11 +150,11 @@ \m \ nat. P(m,0); \m \ nat. \n \ nat. 0 P(n, m mod n) --> P(m,n) |] ==> \m \ nat. P (m,n)" -apply (erule_tac i = "n" in complete_induct) +apply (erule_tac i = n in complete_induct) apply (case_tac "x=0") apply (simp (no_asm_simp)) apply clarify -apply (drule_tac x1 = "m" and x = "x" in bspec [THEN bspec]) +apply (drule_tac x1 = m and x = x in bspec [THEN bspec]) apply (simp_all add: Ord_0_lt_iff) apply (blast intro: mod_less_divisor [THEN ltD]) done @@ -175,7 +170,7 @@ (* gcd type *) lemma gcd_type [simp,TC]: "gcd(m, n) \ nat" -apply (subgoal_tac "gcd (natify (m) , natify (n)) \ nat") +apply (subgoal_tac "gcd (natify (m), natify (n)) \ nat") apply simp apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct) apply auto @@ -187,7 +182,7 @@ lemma gcd_dvd_both: "[| m \ nat; n \ nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n" -apply (rule_tac m = "m" and n = "n" in gcd_induct) +apply (rule_tac m = m and n = n in gcd_induct) apply (simp_all add: gcd_non_0) apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt]) done @@ -207,8 +202,7 @@ lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)" apply (unfold divides_def) apply (case_tac "b=0") - apply (simp add: DIVISION_BY_ZERO_MOD) -apply auto + apply (simp add: DIVISION_BY_ZERO_MOD, auto) apply (blast intro: mod_mult_distrib2 [symmetric]) done @@ -218,7 +212,7 @@ lemma gcd_greatest_raw [rule_format]: "[| m \ nat; n \ nat; f \ nat |] ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" -apply (rule_tac m = "m" and n = "n" in gcd_induct) +apply (rule_tac m = m and n = n in gcd_induct) apply (simp_all add: gcd_non_0 dvd_mod) done @@ -251,8 +245,7 @@ apply (rule is_gcd_unique) apply (rule is_gcd) apply (rule_tac [3] is_gcd_commute [THEN iffD1]) -apply (rule_tac [3] is_gcd) -apply auto +apply (rule_tac [3] is_gcd, auto) done lemma gcd_commute: "gcd(m,n) = gcd(n,m)" @@ -286,11 +279,9 @@ lemma gcd_mult_distrib2_raw: "[| k \ nat; m \ nat; n \ nat |] ==> k #* gcd (m, n) = gcd (k #* m, k #* n)" -apply (erule_tac m = "m" and n = "n" in gcd_induct) -apply assumption -apply (simp) -apply (case_tac "k = 0") +apply (erule_tac m = m and n = n in gcd_induct, assumption) apply simp +apply (case_tac "k = 0", simp) apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff) done @@ -301,20 +292,15 @@ done lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)" -apply (cut_tac k = "k" and m = "1" and n = "n" in gcd_mult_distrib2) -apply auto -done +by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto) lemma gcd_self [simp]: "gcd (k, k) = natify(k)" -apply (cut_tac k = "k" and n = "1" in gcd_mult) -apply auto -done +by (cut_tac k = k and n = 1 in gcd_mult, auto) lemma relprime_dvd_mult: "[| gcd (k,n) = 1; k dvd (m #* n); m \ nat |] ==> k dvd m" -apply (cut_tac k = "m" and m = "k" and n = "n" in gcd_mult_distrib2) -apply auto -apply (erule_tac b = "m" in ssubst) +apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto) +apply (erule_tac b = m in ssubst) apply (simp add: dvd_imp_nat1) done @@ -324,12 +310,10 @@ lemma prime_imp_relprime: "[| p \ prime; ~ (p dvd n); n \ nat |] ==> gcd (p, n) = 1" -apply (unfold prime_def) -apply clarify +apply (unfold prime_def, clarify) apply (drule_tac x = "gcd (p,n)" in bspec) apply auto -apply (cut_tac m = "p" and n = "n" in gcd_dvd2) -apply auto +apply (cut_tac m = p and n = n in gcd_dvd2, auto) done lemma prime_into_nat: "p \ prime ==> p \ nat" @@ -351,7 +335,7 @@ (** Addition laws **) lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)" -apply (subgoal_tac "gcd (m #+ natify (n) , natify (n)) = gcd (m, natify (n))") +apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))") apply simp apply (case_tac "natify (n) = 0") apply (auto simp add: Ord_0_lt_iff gcd_non_0) @@ -359,8 +343,7 @@ lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)" apply (rule gcd_commute [THEN trans]) -apply (subst add_commute) -apply simp +apply (subst add_commute, simp) apply (rule gcd_commute) done @@ -426,10 +409,8 @@ lemma prime_not_square: "\m \ nat; p \ prime\ \ \k \ nat. 0 m#*m \ p#*(k#*k)" -apply (erule complete_induct) -apply clarify -apply (frule prime_dvd_other_side) -apply assumption +apply (erule complete_induct, clarify) +apply (frule prime_dvd_other_side, assumption) apply assumption apply (erule dvdE) apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/Ramsey.thy --- a/src/ZF/ex/Ramsey.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/Ramsey.thy Wed Jul 10 16:54:07 2002 +0200 @@ -93,29 +93,27 @@ \n \ nat. \A B. Atleast((m#+n) #- succ(0), A Un B) --> Atleast(m,A) | Atleast(n,B)" apply (induct_tac "m") -apply (blast intro!: Atleast0) -apply (simp) +apply (blast intro!: Atleast0, simp) apply (rule ballI) apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) -apply (induct_tac "n") -apply auto +apply (induct_tac "n", auto) apply (erule Atleast_succD [THEN bexE]) apply (rename_tac n' A B z) apply (erule UnE) (**case z \ B. Instantiate the '\A B' induction hypothesis. **) -apply (drule_tac [2] x1 = "A" and x = "B-{z}" in spec [THEN spec]) +apply (drule_tac [2] x1 = A and x = "B-{z}" in spec [THEN spec]) apply (erule_tac [2] mp [THEN disjE]) (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+ (*proving the condition*) prefer 2 apply (blast intro: Atleast_superset) (**case z \ A. Instantiate the '\n \ nat. \A B' induction hypothesis. **) -apply (drule_tac x2="succ(n')" and x1="A-{z}" and x="B" +apply (drule_tac x2="succ(n')" and x1="A-{z}" and x=B in bspec [THEN spec, THEN spec]) apply (erule nat_succI) apply (erule mp [THEN disjE]) (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) -apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+; +apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+ (*proving the condition*) apply simp apply (blast intro: Atleast_superset) @@ -138,10 +136,8 @@ Ramsey_step_lemma.*) lemma Atleast_partition: "[| Atleast(m #+ n, A); m \ nat; n \ nat |] ==> Atleast(succ(m), {x \ A. ~P(x)}) | Atleast(n, {x \ A. P(x)})" -apply (rule nat_succI [THEN pigeon2]) -apply assumption+ -apply (rule Atleast_superset) -apply auto +apply (rule nat_succI [THEN pigeon2], assumption+) +apply (rule Atleast_superset, auto) done (*For the Atleast part, proves ~(a \ I) from the second premise!*) @@ -168,8 +164,7 @@ lemma Ramsey_step_lemma: "[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); m \ nat; n \ nat |] ==> Ramsey(succ(m#+n), succ(i), succ(j))" -apply (unfold Ramsey_def) -apply clarify +apply (unfold Ramsey_def, clarify) apply (erule Atleast_succD [THEN bexE]) apply (erule_tac P1 = "%z.:E" in Atleast_partition [THEN disjE], assumption+) diff -r 20ca66539bef -r 0f89104dd377 src/ZF/ex/misc.thy --- a/src/ZF/ex/misc.thy Wed Jul 10 16:07:52 2002 +0200 +++ b/src/ZF/ex/misc.thy Wed Jul 10 16:54:07 2002 +0200 @@ -60,7 +60,7 @@ (K O J) \ hom(A,f,C,h)" by force -(*Another version , with meta-level rewriting*) +(*Another version, with meta-level rewriting*) lemma "(!! A f B g. hom(A,f,B,g) == {H \ A->B. f \ A*A->A & g \ B*B->B & (\x \ A. \y \ A. H`(f`) = g`)}) @@ -72,9 +72,7 @@ (** A characterization of functions suggested by Tobias Nipkow **) lemma "r \ domain(r)->B <-> r \ domain(r)*B & (\X. r `` (r -`` X) \ X)" -apply (unfold Pi_def function_def) -apply best -done +by (unfold Pi_def function_def, best) (**** From D Pastre. Automatic theorem proving in set theory. Artificial Intelligence, 10:1--27, 1978. @@ -138,11 +136,9 @@ \ bij(Pow(Sigma(A,B)), \x \ A. Pow(B(x)))" apply (rule_tac d = "%f. \x \ A. \y \ f`x. {}" in lam_bijective) apply (blast intro: lam_type) -apply (blast dest: apply_type) -apply simp_all +apply (blast dest: apply_type, simp_all) apply fast (*strange, but blast can't do it*) -apply (rule fun_extension) -apply auto +apply (rule fun_extension, auto) by blast end