Fixed quantified variable name preservation for ball and bex (bounded quants)
Requires tweaking of other scripts. Also routine tidying.
--- 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 = "\<lambda>i \<in> 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 @@
==> \<exists>! c. c \<in> s(u) & a \<subseteq> c & b \<in> 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 \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> 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 \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> 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 \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x Un y"
--- 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 "\<forall>y \<in> z. y \<subseteq> 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
--- 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\<notin>A ==> (\<Pi>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi>x \<in> 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"
--- 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\<noteq>0; 0\<notin>A |] ==> (\<Inter>x \<in> {uu(a). a \<in> A}. \<Union>b \<in> x. b) \<noteq> 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
--- 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 \<lesssim> i; Ord(i) |] ==> \<exists>j. j le i & A \<approx> 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 \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A Un B \<lesssim> 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:
"[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);
~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a"
-by (blast intro: UN_fun_lepoll_lemma);
+by (blast intro: UN_fun_lepoll_lemma)
lemma UN_lepoll:
"[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);
@@ -164,7 +164,7 @@
apply (rule UN_I)
apply (rule_tac P = "%z. x \<in> F (z) " in Least_in_Ord, (assumption+))
apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify)
-apply (erule_tac P = "%z. x \<in> F (z) " and i = "c" in less_LeastE)
+apply (erule_tac P = "%z. x \<in> F (z) " and i = c in less_LeastE)
apply (blast intro: Ord_Least ltI)
done
--- 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 \<in> x", force)
+apply (subgoal_tac "0 \<in> 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 ~\<exists> to \<forall>~ *)
@@ -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 (<succ (xa), ya>, f`xa) " in bexI)
+apply (rename_tac m i j y z)
+apply (rule_tac x = "cons(<succ(m), z>, 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 = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}"
in allE)
apply simp
--- 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) \<in> Pow(x)-{0}; v \<in> w |] ==> P"
apply (frule_tac P = "%y. y \<in> 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) \<in> 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)
--- 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 \<approx> 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)
--- 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:
--- 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) = (\<Union>j<i. recfunAC16(f,h,j,a))"
-by (simp add: recfunAC16_def transrec2_Limit);
+by (simp add: recfunAC16_def transrec2_Limit)
(* ********************************************************************** *)
(* Monotonicity of transrec2 *)
@@ -135,7 +135,7 @@
apply (rule impI)
apply (erule disjE)
apply (frule ospec, erule Limit_has_succ, assumption)
-apply (drule_tac A = "a" and x = "xa" in ospec, assumption)
+apply (drule_tac A = a and x = xa in ospec, assumption)
apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord)
apply (blast intro: lemma3 Limit_has_succ)
apply (blast intro: lemma3)
@@ -234,7 +234,7 @@
lemma in_Least_Diff:
"[| z \<in> F(x); Ord(x) |]
==> z \<in> F(LEAST i. z \<in> F(i)) - (\<Union>j<(LEAST i. z \<in> 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 \<in> F(i)) = (LEAST i. z \<in> F(i));
@@ -291,7 +291,7 @@
A\<approx>a; y<a; ~Finite(a); Card(a); n \<in> nat |]
==> Union(recfunAC16(f,g,y,a))\<prec>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:
"[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) --> Q(x,y)); succ(j)<a |]
==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) --> 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
--- 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<i & k = i ++ (k--i) & (k--i)<j)"
-apply (rule_tac i = "k" and j = "i" in Ord_linear2)
+apply (rule_tac i = k and j = i in Ord_linear2)
prefer 4
apply (drule odiff_lt_mono2, assumption)
apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)
@@ -467,7 +467,7 @@
lemma NN_imp_ex_inj: "1 \<in> NN(y) ==> \<exists>a f. Ord(a) & f \<in> 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 = "\<lambda>x \<in> y. LEAST i. f`i = {x}" in exI)
apply (rule conjI, assumption)
apply (rule_tac d = "%i. THE x. x \<in> 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])
--- 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 @@
{<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]
==> <v_clos(x, e, ve),t> \<in> 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); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>
<cl,t> \<in> 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]:
--- 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 \<in> PMap(A,B); a \<in> A; b \<in> 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 \<in> PMap(A,B); a \<in> 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 **)
--- 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 \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
-apply (erule TyEnv.induct)
-apply auto
+apply (erule TyEnv.induct, auto)
done
--- 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 \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> 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 \<in> ExVar; e \<in> Exp; ve \<in> 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) \<noteq> 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 \<in> Const ==> v_const(c) \<noteq> 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 \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
-apply (erule ValEnvE)
-apply (simp );
+apply (erule ValEnvE, simp)
apply (blast dest: pmap_domainD)
done
@@ -115,8 +109,7 @@
lemma ve_owrI:
"[|ve \<in> ValEnv; x \<in> ExVar; v \<in> 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
--- 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) ==> (\<Union>n\<in>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)
--- 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 \<in> 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 \<in> A. Ord(x)} \<in> 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) \<in> 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 \<subseteq> X"} *}
apply (rule_tac x="Cons(X,Nil)" in bexI)
apply (rule_tac x="subset_fm(0,1)" in bexI)
--- 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\<in>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) ==
\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>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) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>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) ==
\<exists>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) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>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) ==
(\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>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) ==
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>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) ==
\<forall>p[M]. p \<in> 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*}
--- 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";
--- 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\<in>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(\<lambda>x. x \<in> 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
--- 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 \<in> 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) ==
- \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
- omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
- (\<exists>f[M]. typed_function(M,n',A,f) &
- (\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
- fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
- (\<forall>j[M]. j\<in>n -->
- (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
- fun_apply(M,f,j,fj) & successor(M,j,sj) &
- fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> 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 \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
-by (simp add: rtran_closure_mem_fm_def)
-
-lemma arity_rtran_closure_mem_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
-
-lemma sats_rtran_closure_mem_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
- \<lambda>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
--- 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); <a,b> \<in> 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 @@
(\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
(\<forall>i\<in>n. <f`i, f`succ(i)> \<in> 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, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
+ separation (M, \<lambda>x.
+ ~ (\<exists>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, \<lambda>x z. \<exists>y[M]. \<exists>f[M].
@@ -247,7 +246,15 @@
and Ord_wfrank_separation:
"M(r) ==>
separation (M, \<lambda>x. ~ (\<forall>f. M(f) \<longrightarrow>
- is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
+ is_recfun(r^+, x, \<lambda>x. range, f) \<longrightarrow> Ord(range(f))))"
+
+lemma (in M_wfrank) wfrank_separation':
+ "M(r) ==>
+ separation
+ (M, \<lambda>x. ~ (\<exists>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.*}
--- 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) |]
==> <x,a> \<in> r --> <x,b> \<in> 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); <b,a> \<in> 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)
--- 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 "\<langle>x,y\<rangle> \<in> r"}*}
apply (blast intro: ltD ord_iso_pred_imp_lt)
--- 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])));
--- 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 \<in> nat; i2 \<in> nat; j \<in> 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])
--- 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";
--- 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
--- 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) ==> \<forall>i \<in> nat. set_of_list(list_update(xs, i, x))
- <= cons(x, set_of_list(xs))"
+ "xs:list(A) ==>
+ \<forall>i \<in> 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
--- 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]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
--- 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)
--- 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
--- 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
(* ------------------------------------------------------------------------- *)
--- 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 \<in> nat")
| Fun ("t \<in> redexes")
- | App ("b \<in> bool" ,"f \<in> redexes" , "a \<in> redexes")
+ | App ("b \<in> bool","f \<in> redexes", "a \<in> redexes")
consts
@@ -75,7 +75,7 @@
type_intros redexes.intros bool_typechecks
inductive
- domains "Sreg" <= "redexes"
+ domains "Sreg" <= redexes
intros
Reg_Var: "n \<in> 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
--- 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 \<in> nat ==> Var(n) \<in> lambda"
Lambda_Fun: " u \<in> lambda ==> Fun(u) \<in> 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 \<in> 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 \<in> 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 \<in> lambda; m':lambda; n \<in> 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
--- 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 \<in> redexes"
-apply (erule Scomp.induct)
-apply auto
+apply (erule Scomp.induct, auto)
apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
apply auto
done
@@ -138,19 +136,16 @@
lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> 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 ==> \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->
(\<forall>n \<in> 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 = "\<forall>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) --> (\<forall>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
--- 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 \<in> redexes
==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>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 @@
\<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>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 \<in> redexes ==>
\<forall>n \<in> nat. \<forall>v \<in> 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\<le>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 \<le> 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
--- 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";
--- 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 "(<xs,ys>: 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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 \<subseteq> 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
--- 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: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> 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: "<l,l'> \<in> lleq(A) ==> l=l'"
@@ -168,8 +165,7 @@
apply (rule_tac X = "{<l,l>. l \<in> 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) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> 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 \<in> llist(bool) ==> flip(l) \<in> 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 \<in> llist(bool) ==> flip(l): llist(bool)"
apply (rule_tac X = "{flip (l) . l \<in> 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 \<in> 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
--- 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 \<in> cont(D,E)|]==>rel(cf(D,E),(\<lambda>x \<in> set(D).bot(E)),y)"
-apply (rule rel_cfI, simp)
-apply typecheck
+apply (rule rel_cfI, simp, typecheck)
done
lemma pcpo_cf:
--- 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 \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
-apply (unfold divides_def)
-apply assumption
-done
+by (unfold divides_def, assumption)
lemma dvdE:
"[|m dvd n; !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P"
@@ -69,13 +67,11 @@
lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> 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 \<in> 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 @@
\<forall>m \<in> nat. P(m,0);
\<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]
==> \<forall>m \<in> 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) \<in> nat"
-apply (subgoal_tac "gcd (natify (m) , natify (n)) \<in> nat")
+apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> 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 \<in> nat; n \<in> 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 \<in> nat; n \<in> nat; f \<in> 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 \<in> nat; m \<in> nat; n \<in> 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 \<in> 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 \<in> prime; ~ (p dvd n); n \<in> 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 \<in> prime ==> p \<in> 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:
"\<lbrakk>m \<in> nat; p \<in> prime\<rbrakk> \<Longrightarrow> \<forall>k \<in> nat. 0<k \<longrightarrow> m#*m \<noteq> 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)
--- 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 @@
\<forall>n \<in> nat. \<forall>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 \<in> B. Instantiate the '\<forall>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 \<in> A. Instantiate the '\<forall>n \<in> nat. \<forall>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 \<in> nat; n \<in> nat |]
==> Atleast(succ(m), {x \<in> A. ~P(x)}) | Atleast(n, {x \<in> 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 \<in> 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 \<in> nat; n \<in> 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.<x,z>:E" in Atleast_partition [THEN disjE],
assumption+)
--- 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) \<in> 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 \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &
(\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)})
@@ -72,9 +72,7 @@
(** A characterization of functions suggested by Tobias Nipkow **)
lemma "r \<in> domain(r)->B <-> r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> 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 @@
\<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" 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