--- a/src/ZF/Arith.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Arith.thy Thu Jan 23 10:30:14 2003 +0100
@@ -200,7 +200,7 @@
(*Must simplify BEFORE the induction: else we get a critical pair*)
lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
apply (simp add: natify_succ diff_def)
-apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
+apply (rule_tac x1 = n in natify_in_nat [THEN nat_induct], auto)
done
(*This defining property is no longer wanted*)
@@ -212,7 +212,7 @@
lemma diff_le_self: "m:nat ==> (m #- n) le m"
apply (subgoal_tac " (m #- natify (n)) le m")
-apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
+apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
apply (erule_tac [6] leE)
apply (simp_all add: le_iff)
done
@@ -528,7 +528,7 @@
lemma less_diff_conv [rule_format]:
"[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
-by (erule_tac m = "k" in diff_induct, auto)
+by (erule_tac m = k in diff_induct, auto)
lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
--- a/src/ZF/ArithSimp.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/ArithSimp.thy Thu Jan 23 10:30:14 2003 +0100
@@ -24,7 +24,7 @@
lemma add_diff_inverse: "[| n le m; m:nat |] ==> n #+ (m#-n) = m"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct, auto)
+apply (rule_tac m = m and n = n in diff_induct, auto)
done
lemma add_diff_inverse2: "[| n le m; m:nat |] ==> (m#-n) #+ n = m"
@@ -36,13 +36,13 @@
lemma diff_succ: "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp))
done
lemma zero_less_diff [simp]:
"[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n"
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp))
done
@@ -67,7 +67,7 @@
apply (frule lt_nat_in_nat, erule nat_succI)
apply (erule rev_mp)
apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
apply (simp_all (no_asm_simp) add: diff_le_self)
done
@@ -236,7 +236,7 @@
done
lemma mod_1_eq [simp]: "m mod 1 = 0"
-by (cut_tac n = "1" in mod_less_divisor, auto)
+by (cut_tac n = 1 in mod_less_divisor, auto)
lemma mod2_cases: "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"
apply (subgoal_tac "k mod 2: 2")
@@ -257,7 +257,7 @@
done
lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
-by (cut_tac n = "0" in mod2_add_more, auto)
+by (cut_tac n = 0 in mod2_add_more, auto)
subsection{*Additional theorems about @{text "\<le>"}*}
@@ -368,7 +368,7 @@
done
lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)"
-by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto)
+by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)"
by (blast intro: le_anti_sym)
@@ -395,7 +395,7 @@
lemma div_cancel_raw:
"[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"
-apply (erule_tac i = "m" in complete_induct)
+apply (erule_tac i = m in complete_induct)
apply (case_tac "x<n")
apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
@@ -419,7 +419,7 @@
apply (case_tac "n=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
-apply (erule_tac i = "m" in complete_induct)
+apply (erule_tac i = m in complete_induct)
apply (case_tac "x<n")
apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
@@ -499,7 +499,7 @@
lemma diff_is_0_lemma:
"[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
-apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)
+apply (rule_tac m = m and n = n in diff_induct, simp_all)
done
lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)"
@@ -514,8 +514,7 @@
(P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
apply (case_tac "a < b")
apply (force simp add: nat_lt_imp_diff_eq_0)
-apply (rule iffI, force)
-apply simp
+apply (rule iffI, force, simp)
apply (drule_tac x="a#-b" in bspec)
apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse)
done
--- a/src/ZF/Cardinal.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Cardinal.thy Thu Jan 23 10:30:14 2003 +0100
@@ -495,7 +495,7 @@
apply (induct_tac m)
apply (blast intro!: nat_0_le)
apply (rule ballI)
-apply (erule_tac n = "n" in natE)
+apply (erule_tac n = n in natE)
apply (simp (no_asm_simp) add: lepoll_def inj_def)
apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
done
@@ -859,7 +859,7 @@
apply (rule Diff_sing_eqpoll [THEN revcut_rl])
prefer 2 apply assumption
apply assumption
-apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
apply (rule Fin.consI, blast)
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
(*Now for the lemma assumed above*)
@@ -907,7 +907,7 @@
apply (subgoal_tac [2] "A-{a}=A", auto)
apply (rule_tac x = "succ (n) " in bexI)
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
-apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
+apply (drule_tac a = a and b = n in cons_eqpoll_cong)
apply (auto dest: mem_irrefl)
done
@@ -976,7 +976,7 @@
apply (drule_tac x = x in bspec, assumption)
apply (blast elim: mem_irrefl mem_asym)
txt{*other case*}
-apply (drule_tac x = "Z" in spec, blast)
+apply (drule_tac x = Z in spec, blast)
done
lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
--- a/src/ZF/CardinalArith.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/CardinalArith.thy Thu Jan 23 10:30:14 2003 +0100
@@ -585,14 +585,14 @@
(*??WHAT A MESS!*)
apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
(assumption | rule refl | erule ltI)+)
-apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
+apply (rule_tac i = "xa Un ya" and j = nat in Ord_linear2,
simp_all add: Ord_Un Ord_nat)
prefer 2 (*case nat le (xa Un ya) *)
apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong]
le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
(*the finite case: xa Un ya < nat *)
-apply (rule_tac j = "nat" in lt_trans2)
+apply (rule_tac j = nat in lt_trans2)
apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
nat_into_Card [THEN Card_cardinal_eq] Ord_nat)
apply (simp add: InfCard_def)
@@ -645,7 +645,7 @@
(*Corollary 10.13 (1), for cardinal multiplication*)
lemma InfCard_cmult_eq: "[| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"
-apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
+apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cmult_commute [THEN ssubst])
apply (rule Un_commute [THEN ssubst])
@@ -669,7 +669,7 @@
done
lemma InfCard_cadd_eq: "[| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"
-apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
+apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cadd_commute [THEN ssubst])
apply (rule Un_commute [THEN ssubst])
@@ -812,7 +812,7 @@
lemma Finite_imp_succ_cardinal_Diff:
"[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"
-apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
apply (simp add: cons_Diff)
done
--- a/src/ZF/Cardinal_AC.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Cardinal_AC.thy Thu Jan 23 10:30:14 2003 +0100
@@ -83,7 +83,7 @@
lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
apply (unfold surj_def)
apply (erule CollectE)
-apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
+apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
apply (fast elim!: apply_Pair)
apply (blast dest: apply_type Pi_memberD
intro: apply_equality Pi_type f_imp_injective)
--- a/src/ZF/Epsilon.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Epsilon.thy Thu Jan 23 10:30:14 2003 +0100
@@ -180,7 +180,7 @@
lemma transrec_type:
"[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) |]
==> transrec(a,H) : B(a)"
-apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
+apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
apply (subst transrec)
apply (simp add: lam_type)
done
@@ -220,7 +220,7 @@
by (subst rank_def [THEN def_transrec], simp)
lemma Ord_rank [simp]: "Ord(rank(a))"
-apply (rule_tac a="a" in eps_induct)
+apply (rule_tac a=a in eps_induct)
apply (subst rank)
apply (rule Ord_succ [THEN Ord_UN])
apply (erule bspec, assumption)
@@ -233,7 +233,7 @@
done
lemma rank_lt: "a:b ==> rank(a) < rank(b)"
-apply (rule_tac a1 = "b" in rank [THEN ssubst])
+apply (rule_tac a1 = b in rank [THEN ssubst])
apply (erule UN_I [THEN ltI])
apply (rule_tac [2] Ord_UN, auto)
done
--- a/src/ZF/Finite.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Finite.thy Thu Jan 23 10:30:14 2003 +0100
@@ -90,7 +90,7 @@
apply (erule Fin_induct)
apply (simp add: subset_empty_iff)
apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
+apply (erule_tac b = z in cons_Diff [THEN subst], simp)
done
lemma Fin_subset: "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"
@@ -158,7 +158,7 @@
apply (erule FiniteFun.induct)
apply (simp add: subset_empty_iff FiniteFun.intros)
apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst])
+apply (erule_tac b = z in cons_Diff [THEN subst])
apply (drule spec [THEN mp], assumption)
apply (fast intro!: FiniteFun.intros)
done
--- a/src/ZF/List.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/List.thy Thu Jan 23 10:30:14 2003 +0100
@@ -354,8 +354,7 @@
lemma drop_length [rule_format]:
"l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
-apply (erule list.induct, simp_all)
-apply safe
+apply (erule list.induct, simp_all, safe)
apply (erule drop_length_Cons)
apply (rule natE)
apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
@@ -1121,8 +1120,7 @@
lemma nth_map_upt [rule_format]:
"[| m:nat; n:nat |] ==>
\<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
-apply (rule_tac n = m and m = n in diff_induct, typecheck, simp)
-apply simp
+apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
apply (subst map_succ_upt [symmetric], simp_all, clarify)
apply (subgoal_tac "i < length (upt (0, x))")
prefer 2
--- a/src/ZF/Nat.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Nat.thy Thu Jan 23 10:30:14 2003 +0100
@@ -174,7 +174,7 @@
!!y. y: nat ==> P(0,succ(y));
!!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |]
==> P(m,n)"
-apply (erule_tac x = "m" in rev_bspec)
+apply (erule_tac x = m in rev_bspec)
apply (erule nat_induct, simp)
apply (rule ballI)
apply (rename_tac i j)
--- a/src/ZF/OrderArith.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/OrderArith.thy Thu Jan 23 10:30:14 2003 +0100
@@ -88,12 +88,12 @@
prefer 2
apply (erule_tac V = "y : A + B" in thin_rl)
apply (rule_tac ballI)
- apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
+ apply (erule_tac r = r and a = x in wf_on_induct, assumption)
apply blast
txt{*Returning to main part of proof*}
apply safe
apply blast
-apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast)
+apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast)
done
lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
@@ -193,9 +193,9 @@
apply (erule SigmaE)
apply (erule ssubst)
apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
-apply (erule_tac a = "x" in wf_on_induct, assumption)
+apply (erule_tac a = x in wf_on_induct, assumption)
apply (rule ballI)
-apply (erule_tac a = "b" in wf_on_induct, assumption)
+apply (erule_tac a = b in wf_on_induct, assumption)
apply (best elim!: rmultE bspec [THEN mp])
done
@@ -236,7 +236,7 @@
done
lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
-by (rule_tac d = "snd" in lam_bijective, auto)
+by (rule_tac d = snd in lam_bijective, auto)
(*Used??*)
lemma singleton_prod_ord_iso:
@@ -310,8 +310,7 @@
subsubsection{*Type checking*}
lemma rvimage_type: "rvimage(A,f,r) <= A*A"
-apply (unfold rvimage_def, rule Collect_subset)
-done
+by (unfold rvimage_def, rule Collect_subset)
lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
@@ -539,8 +538,7 @@
apply (rename_tac u)
apply (drule_tac x=u in bspec, blast)
apply (erule mp, clarify)
-apply (frule ok, assumption+);
-apply blast
+apply (frule ok, assumption+, blast)
done
--- a/src/ZF/Ordinal.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Ordinal.thy Thu Jan 23 10:30:14 2003 +0100
@@ -173,7 +173,7 @@
(*There is no set of all ordinals, for then it would contain itself*)
lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
apply (rule notI)
-apply (frule_tac x = "X" in spec)
+apply (frule_tac x = X in spec)
apply (safe elim!: mem_irrefl)
apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
apply (simp add: Transset_def)
@@ -366,13 +366,13 @@
lemma Ord_linear2:
"[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
+apply (rule_tac i = i and j = j in Ord_linear_lt)
apply (blast intro: leI le_eqI sym ) +
done
lemma Ord_linear_le:
"[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
+apply (rule_tac i = i and j = j in Ord_linear_lt)
apply (blast intro: leI le_eqI ) +
done
@@ -380,7 +380,7 @@
by (blast elim!: leE elim: lt_asym)
lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j le i"
-by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
+by (rule_tac i = i and j = j in Ord_linear2, auto)
subsubsection{*Some Rewrite Rules for <, le*}
@@ -495,7 +495,7 @@
(*Replacing k by succ(k') yields the similar rule for le!*)
lemma Un_least_lt: "[| i<k; j<k |] ==> i Un j < k"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
+apply (rule_tac i = i and j = j in Ord_linear_le)
apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord)
done
@@ -513,7 +513,7 @@
(*Replacing k by succ(k') yields the similar rule for le!*)
lemma Int_greatest_lt: "[| i<k; j<k |] ==> i Int j < k"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
+apply (rule_tac i = i and j = j in Ord_linear_le)
apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord)
done
--- a/src/ZF/Perm.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Perm.thy Thu Jan 23 10:30:14 2003 +0100
@@ -69,7 +69,7 @@
!!y. y:B ==> d(y): A;
!!y. y:B ==> c(d(y)) = y
|] ==> (lam x:A. c(x)) : surj(A,B)"
-apply (rule_tac d = "d" in f_imp_surjective)
+apply (rule_tac d = d in f_imp_surjective)
apply (simp_all add: lam_type)
done
@@ -112,7 +112,7 @@
"[| !!x. x:A ==> c(x): B;
!!x. x:A ==> d(c(x)) = x |]
==> (lam x:A. c(x)) : inj(A,B)"
-apply (rule_tac d = "d" in f_imp_injective)
+apply (rule_tac d = d in f_imp_injective)
apply (simp_all add: lam_type)
done
@@ -143,7 +143,7 @@
lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))
==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
-apply (rule_tac d = "f" in lam_bijective)
+apply (rule_tac d = f in lam_bijective)
apply (auto simp add: the_equality2)
done
@@ -387,8 +387,8 @@
lemma comp_mem_injD2:
"[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"
apply (unfold inj_def surj_def, safe)
-apply (rule_tac x1 = "x" in bspec [THEN bexE])
-apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
+apply (rule_tac x1 = x in bspec [THEN bexE])
+apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
apply (rule_tac t = "op ` (g) " in subst_context)
apply (erule asm_rl bspec [THEN bspec, THEN mp])+
apply (simp (no_asm_simp))
--- a/src/ZF/QPair.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/QPair.thy Thu Jan 23 10:30:14 2003 +0100
@@ -283,7 +283,7 @@
!!x. x: A ==> c(x): C(QInl(x));
!!y. y: B ==> d(y): C(QInr(y))
|] ==> qcase(c,d,u) : C(u)"
-by (simp add: qsum_defs , auto)
+by (simp add: qsum_defs, auto)
(** Rules for the Part primitive **)
--- a/src/ZF/Trancl.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Trancl.thy Thu Jan 23 10:30:14 2003 +0100
@@ -166,7 +166,7 @@
lemma trans_rtrancl: "trans(r^*)"
apply (unfold trans_def)
apply (intro allI impI)
-apply (erule_tac b = "z" in rtrancl_induct, assumption)
+apply (erule_tac b = z in rtrancl_induct, assumption)
apply (blast intro: rtrancl_into_rtrancl)
done
--- a/src/ZF/Univ.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Univ.thy Thu Jan 23 10:30:14 2003 +0100
@@ -147,7 +147,7 @@
lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
-apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
+apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
apply (subst rank_succ)
apply (rule Ord_rank [THEN Vfrom_succ_lemma])
done
--- a/src/ZF/WF.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/WF.thy Thu Jan 23 10:30:14 2003 +0100
@@ -79,7 +79,7 @@
shows "wf[A](r)"
apply (unfold wf_on_def wf_def)
apply (rule equals0I [THEN disjCI, THEN allI])
-apply (rule_tac Z = "Z" in prem, blast+)
+apply (rule_tac Z = Z in prem, blast+)
done
text{*If @{term r} allows well-founded induction over @{term A}
@@ -192,7 +192,7 @@
"[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)"
apply (rule wf_onI2)
apply (frule bspec [THEN mp], assumption+)
-apply (erule_tac a = "y" in wf_on_induct, assumption)
+apply (erule_tac a = y in wf_on_induct, assumption)
apply (blast elim: tranclE, blast)
done
@@ -232,8 +232,8 @@
lemma is_recfun_equal [rule_format]:
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |]
==> <x,a>:r --> <x,b>: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 wf_induct)
apply (intro impI)
@@ -250,7 +250,7 @@
"[| wf(r); trans(r);
is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>: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 dest: transD intro: restrict_type2)
apply (erule is_recfun_type, simp)
@@ -294,7 +294,7 @@
apply (blast dest: transD)
apply (frule spec [THEN mp], assumption)
apply (subgoal_tac "<xa,a1> : r")
- apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
+ apply (drule_tac x1 = xa in spec [THEN mp], assumption)
apply (simp add: vimage_singleton_iff
apply_recfun is_recfun_cut)
apply (blast dest: transD)
@@ -343,7 +343,7 @@
"[| wf(r); a:A; field(r)<=A;
!!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
|] ==> wfrec(r,a,H) : B(a)"
-apply (rule_tac a = "a" in wf_induct2, assumption+)
+apply (rule_tac a = a in wf_induct2, assumption+)
apply (subst wfrec, assumption)
apply (simp add: lam_type underD)
done
--- a/src/ZF/Zorn.thy Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Zorn.thy Thu Jan 23 10:30:14 2003 +0100
@@ -115,7 +115,7 @@
apply (erule TFin_induct)
apply (rule impI [THEN ballI])
txt{*case split using @{text TFin_linear_lemma1}*}
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
assumption+)
apply (blast del: subsetI
intro: increasing_trans subsetI, blast)
@@ -127,7 +127,7 @@
apply (rule ballI)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
assumption+, blast)
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
apply (blast dest: TFin_is_subset)+
@@ -156,8 +156,7 @@
"[| n \<in> TFin(S,next); m \<in> TFin(S,next); m = next`m |] ==> n <= m"
apply (erule TFin_induct)
apply (drule TFin_subsetD)
-apply (assumption+, force)
-apply blast
+apply (assumption+, force, blast)
done
text{*Property 3.3 of section 3.3*}
@@ -208,8 +207,7 @@
"[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
==> ch ` super(S,X) \<noteq> X"
apply (rule notI)
-apply (drule choice_super, assumption)
-apply assumption
+apply (drule choice_super, assumption, assumption)
apply (simp add: super_def)
done