--- a/src/HOL/Arith.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Arith.ML Thu Aug 13 18:14:26 1998 +0200
@@ -221,7 +221,7 @@
qed "add_less_mono";
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
-val [lt_mono,le] = goal thy
+val [lt_mono,le] = Goal
"[| !!i j::nat. i<j ==> f(i) < f(j); \
\ i <= j \
\ |] ==> f(i) <= (f(j)::nat)";
@@ -331,8 +331,8 @@
(*** More results about difference ***)
-val [prem] = goal thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
-by (rtac (prem RS rev_mp) 1);
+Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "Suc_diff_n";
@@ -411,20 +411,20 @@
by (ALLGOALS Asm_simp_tac);
qed "le_imp_diff_is_add";
-val [prem] = goal thy "m < Suc(n) ==> m-n = 0";
-by (rtac (prem RS rev_mp) 1);
+Goal "m < Suc(n) ==> m-n = 0";
+by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_is_0";
-val prems = goal thy "m-n = 0 --> n-m = 0 --> m=n";
+Goal "m-n = 0 --> n-m = 0 --> m=n";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
qed_spec_mp "diffs0_imp_equal";
-val [prem] = goal thy "m<n ==> 0<n-m";
-by (rtac (prem RS rev_mp) 1);
+Goal "m<n ==> 0<n-m";
+by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_positive";
@@ -448,7 +448,7 @@
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
qed "zero_induct_lemma";
-val prems = goal thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
+val prems = Goal "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
by (rtac (diff_self_eq_0 RS subst) 1);
by (rtac (zero_induct_lemma RS mp RS mp) 1);
by (REPEAT (ares_tac ([impI,allI]@prems) 1));
--- a/src/HOL/Divides.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Divides.ML Thu Aug 13 18:14:26 1998 +0200
@@ -10,7 +10,7 @@
(** Less-then properties **)
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
+Goal "[| 0<n; ~ m<n |] ==> m - n < m";
by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
by (Blast_tac 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -200,9 +200,10 @@
by (trans_tac 2);
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
- by (best_tac (claset() addIs [le_trans]
- addss (simpset() addsimps [diff_less])) 1);
-by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
+by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
+br le_trans 1;
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
qed "div_le_mono2";
Goal "0<n ==> m div n <= m";
--- a/src/HOL/Finite.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Finite.ML Thu Aug 13 18:14:26 1998 +0200
@@ -11,7 +11,7 @@
section "finite";
(*Discharging ~ x:y entails extra work*)
-val major::prems = goal Finite.thy
+val major::prems = Goal
"[| finite F; P({}); \
\ !!F x. [| finite F; x ~: F; P(F) |] ==> P(insert x F) \
\ |] ==> P(F)";
@@ -21,7 +21,7 @@
by (REPEAT (ares_tac prems 1));
qed "finite_induct";
-val major::subs::prems = goal Finite.thy
+val major::subs::prems = Goal
"[| finite F; F <= A; \
\ P({}); \
\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
@@ -35,10 +35,9 @@
AddSIs Finites.intrs;
(*The union of two finite sets is finite*)
-val major::prems = goal Finite.thy
- "[| finite F; finite G |] ==> finite(F Un G)";
-by (rtac (major RS finite_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+Goal "[| finite F; finite G |] ==> finite(F Un G)";
+by (etac finite_induct 1);
+by (ALLGOALS Asm_simp_tac);
qed "finite_UnI";
(*Every subset of a finite set is finite*)
@@ -76,7 +75,7 @@
by (Asm_simp_tac 1);
qed "finite_imageI";
-val major::prems = goal Finite.thy
+val major::prems = Goal
"[| finite c; finite b; \
\ P(b); \
\ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \
@@ -87,7 +86,7 @@
(simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
val lemma = result();
-val prems = goal Finite.thy
+val prems = Goal
"[| finite A; \
\ P(A); \
\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \
@@ -134,9 +133,8 @@
(** The finite UNION of finite sets **)
-val [prem] = goal Finite.thy
- "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
-by (rtac (prem RS finite_induct) 1);
+Goal "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
+by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
Addsimps [finite_UnionI];
@@ -187,7 +185,7 @@
section "Finite cardinality -- 'card'";
-goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
+Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
by (Blast_tac 1);
val Collect_conv_insert = result();
@@ -197,9 +195,8 @@
qed "card_empty";
Addsimps [card_empty];
-val [major] = goal Finite.thy
- "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
-by (rtac (major RS finite_induct) 1);
+Goal "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
+by (etac finite_induct 1);
by (res_inst_tac [("x","0")] exI 1);
by (Simp_tac 1);
by (etac exE 1);
--- a/src/HOL/Fun.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Fun.ML Thu Aug 13 18:14:26 1998 +0200
@@ -13,7 +13,7 @@
by (rtac ext 1 THEN Asm_simp_tac 1);
qed "expand_fun_eq";
-val prems = goal thy
+val prems = Goal
"[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)";
by (rtac (arg_cong RS box_equals) 1);
by (REPEAT (resolve_tac (prems@[refl]) 1));
@@ -22,11 +22,11 @@
(** "Axiom" of Choice, proved using the description operator **)
-goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
+Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
by (fast_tac (claset() addEs [selectI]) 1);
qed "choice";
-goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
+Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
by (fast_tac (claset() addEs [selectI]) 1);
qed "bchoice";
@@ -57,44 +57,43 @@
(*** inj(f): f is a one-to-one function ***)
-val prems = goalw thy [inj_def]
+val prems = Goalw [inj_def]
"[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
by (blast_tac (claset() addIs prems) 1);
qed "injI";
-val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
+val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
by (rtac injI 1);
by (etac (arg_cong RS box_equals) 1);
by (rtac major 1);
by (rtac major 1);
qed "inj_inverseI";
-val [major,minor] = goalw thy [inj_def]
- "[| inj(f); f(x) = f(y) |] ==> x=y";
-by (rtac (major RS spec RS spec RS mp) 1);
-by (rtac minor 1);
+Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
+by (Blast_tac 1);
qed "injD";
(*Useful with the simplifier*)
-val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
+Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
by (rtac iffI 1);
-by (etac (major RS injD) 1);
-by (etac arg_cong 1);
+by (etac arg_cong 2);
+by (etac injD 1);
+ba 1;
qed "inj_eq";
-val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
-by (rtac (major RS injD) 1);
+Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
+by (etac injD 1);
by (rtac selectI 1);
by (rtac refl 1);
qed "inj_select";
(*A one-to-one function has an inverse (given using select).*)
-val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
-by (EVERY1 [rtac (major RS inj_select)]);
+Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
+by (etac inj_select 1);
qed "inv_f_f";
(* Useful??? *)
-val [oneone,minor] = goal thy
+val [oneone,minor] = Goal
"[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
by (rtac (rangeI RS minor) 1);
@@ -103,60 +102,52 @@
(*** inj_on f A: f is one-to-one over A ***)
-val prems = goalw thy [inj_on_def]
+val prems = Goalw [inj_on_def]
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A";
by (blast_tac (claset() addIs prems) 1);
qed "inj_onI";
-val [major] = goal thy
+val [major] = Goal
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
by (rtac inj_onI 1);
by (etac (apply_inverse RS trans) 1);
by (REPEAT (eresolve_tac [asm_rl,major] 1));
qed "inj_on_inverseI";
-val major::prems = goalw thy [inj_on_def]
- "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y";
-by (rtac (major RS bspec RS bspec RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
+Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y";
+by (Blast_tac 1);
qed "inj_onD";
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
by (blast_tac (claset() addSDs [inj_onD]) 1);
qed "inj_on_iff";
-val major::prems = goal thy
- "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
-by (rtac contrapos 1);
-by (etac (major RS inj_onD) 2);
-by (REPEAT (resolve_tac prems 1));
+Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
+by (Blast_tac 1);
qed "inj_on_contraD";
-Goalw [inj_on_def]
- "[| A<=B; inj_on f B |] ==> inj_on f A";
+Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
by (Blast_tac 1);
qed "subset_inj_on";
(*** Lemmas about inj ***)
-Goalw [o_def]
- "[| inj(f); inj_on g (range f) |] ==> inj(g o f)";
+Goalw [o_def] "[| inj(f); inj_on g (range f) |] ==> inj(g o f)";
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
qed "comp_inj";
-val [prem] = goal thy "inj(f) ==> inj_on f A";
-by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
+Goal "inj(f) ==> inj_on f A";
+by (blast_tac (claset() addIs [injD, inj_onI]) 1);
qed "inj_imp";
-val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
+Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
+by (fast_tac (claset() addIs [selectI]) 1);
qed "f_inv_f";
-val prems = goal thy
- "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y";
+Goal "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y";
by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
+by (REPEAT (ares_tac [f_inv_f] 1));
qed "inv_injective";
Goal "[| inj(f); A<=range(f) |] ==> inj_on (inv f) A";
--- a/src/HOL/Gfp.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Gfp.ML Thu Aug 13 18:14:26 1998 +0200
@@ -22,18 +22,18 @@
by (etac CollectD 1);
qed "gfp_least";
-val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
+Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
- rtac (mono RS monoD), rtac gfp_upperbound, atac]);
+ etac monoD, rtac gfp_upperbound, atac]);
qed "gfp_lemma2";
-val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
-by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD),
- rtac gfp_lemma2, rtac mono]);
+Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
+by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
+ etac gfp_lemma2]);
qed "gfp_lemma3";
-val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
-by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
+Goal "mono(f) ==> gfp(f) = f(gfp(f))";
+by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
qed "gfp_Tarski";
(*** Coinduction rules for greatest fixed points ***)
@@ -70,8 +70,8 @@
- instead of the condition X <= f(X)
consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)";
-by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
+Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
+by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
qed "coinduct3_mono_lemma";
val [prem,mono] = goal Gfp.thy
@@ -88,12 +88,11 @@
by (rtac Un_upper2 1);
qed "coinduct3_lemma";
-val prems = goal Gfp.thy
- "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
+Goal
+ "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
-by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
-by (rtac (UnI2 RS UnI1) 1);
-by (REPEAT (resolve_tac prems 1));
+by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1);
+by Auto_tac;
qed "coinduct3";
@@ -111,7 +110,7 @@
qed "def_coinduct";
(*The version used in the induction/coinduction package*)
-val prems = goal Gfp.thy
+val prems = Goal
"[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \
\ a: X; !!z. z: X ==> P (X Un A) z |] ==> \
\ a : A";
@@ -126,7 +125,7 @@
qed "def_coinduct3";
(*Monotonicity of gfp!*)
-val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
+val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
by (rtac (gfp_upperbound RS gfp_least) 1);
by (etac (prem RSN (2,subset_trans)) 1);
qed "gfp_mono";
--- a/src/HOL/Integ/Integ.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Thu Aug 13 18:14:26 1998 +0200
@@ -32,10 +32,8 @@
(** Natural deduction for intrel **)
-val prems = goalw Integ.thy [intrel_def]
- "[| x1+y2 = x2+y1|] ==> \
-\ ((x1,y1),(x2,y2)): intrel";
-by (fast_tac (claset() addIs prems) 1);
+Goalw [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
+by (Fast_tac 1);
qed "intrelI";
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
@@ -45,7 +43,7 @@
by (Fast_tac 1);
qed "intrelE_lemma";
-val [major,minor] = goal Integ.thy
+val [major,minor] = Goal
"[| p: intrel; \
\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \
\ ==> Q";
@@ -130,8 +128,7 @@
qed "zminus";
(*by lcp*)
-val [prem] = goal Integ.thy
- "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
+val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
@@ -159,8 +156,7 @@
(**** znegative: the test for negative integers ****)
-Goalw [znegative_def, znat_def]
- "~ znegative($# n)";
+Goalw [znegative_def, znat_def] "~ znegative($# n)";
by (Simp_tac 1);
by Safe_tac;
qed "not_znegative_znat";
@@ -445,13 +441,11 @@
by (Simp_tac 1);
qed "zminus_zpred";
-Goalw [zsuc_def,zpred_def,zdiff_def]
- "zpred(zsuc(z)) = z";
+Goalw [zsuc_def,zpred_def,zdiff_def] "zpred(zsuc(z)) = z";
by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
qed "zpred_zsuc";
-Goalw [zsuc_def,zpred_def,zdiff_def]
- "zsuc(zpred(z)) = z";
+Goalw [zsuc_def,zpred_def,zdiff_def] "zsuc(zpred(z)) = z";
by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
qed "zsuc_zpred";
@@ -473,13 +467,13 @@
by (rtac zminus_zminus 1);
qed "zminus_exchange";
-Goal"(zsuc(z)=zsuc(w)) = (z=w)";
+Goal "(zsuc(z)=zsuc(w)) = (z=w)";
by Safe_tac;
by (dres_inst_tac [("f","zpred")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
qed "bijective_zsuc";
-Goal"(zpred(z)=zpred(w)) = (z=w)";
+Goal "(zpred(z)=zpred(w)) = (z=w)";
by Safe_tac;
by (dres_inst_tac [("f","zsuc")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
@@ -579,7 +573,7 @@
val zless_zsucI = zlessI RSN (2,zless_trans);
-Goal "!!z w::int. z<w ==> ~w<z";
+Goal "!!w::int. z<w ==> ~w<z";
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by Safe_tac;
@@ -611,7 +605,7 @@
by (asm_full_simp_tac
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (REPEAT (fast_tac (claset() addss (simpset() addsimps add_ac)) 1));
+by (auto_tac (claset(), simpset() addsimps add_ac));
qed "zless_linear";
@@ -664,14 +658,15 @@
by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
qed "zle_refl";
-val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
+Goal "[| i <= j; j < k |] ==> i < (k::int)";
by (dtac zle_imp_zless_or_eq 1);
by (fast_tac (claset() addIs [zless_trans]) 1);
qed "zle_zless_trans";
Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
- rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
+ rtac zless_or_eq_imp_zle,
+ fast_tac (claset() addIs [zless_trans])]);
qed "zle_trans";
Goal "[| z <= w; w <= z |] ==> z = (w::int)";
@@ -680,7 +675,7 @@
qed "zle_anti_sym";
-Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
+Goal "!!w::int. z + w' = z + w ==> w' = w";
by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
qed "zadd_left_cancel";
@@ -688,19 +683,19 @@
(*** Monotonicity results ***)
-Goal "!!v w z::int. v < w ==> v + z < w + z";
+Goal "!!z::int. v < w ==> v + z < w + z";
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
by (simp_tac (simpset() addsimps zadd_ac) 1);
by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
qed "zadd_zless_mono1";
-Goal "!!v w z::int. (v+z < w+z) = (v < w)";
+Goal "!!z::int. (v+z < w+z) = (v < w)";
by (safe_tac (claset() addSEs [zadd_zless_mono1]));
by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
qed "zadd_left_cancel_zless";
-Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
+Goal "!!z::int. (v+z <= w+z) = (v <= w)";
by (asm_full_simp_tac
(simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
qed "zadd_left_cancel_zle";
@@ -709,14 +704,14 @@
bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
-Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
by (etac (zadd_zle_mono1 RS zle_trans) 1);
by (simp_tac (simpset() addsimps [zadd_commute]) 1);
(*w moves to the end because it is free while z', z are bound*)
by (etac zadd_zle_mono1 1);
qed "zadd_zle_mono";
-Goal "!!w z::int. z<=$#0 ==> w+z <= w";
+Goal "!!z::int. z<=$#0 ==> w+z <= w";
by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
qed "zadd_zle_self";
@@ -726,7 +721,7 @@
(** One auxiliary theorem...**)
-goal HOL.thy "(x = False) = (~ x)";
+Goal "(x = False) = (~ x)";
by (fast_tac HOL_cs 1);
qed "eq_False_conv";
@@ -848,8 +843,7 @@
(* a case theorem distinguishing positive and negative int *)
-val prems = goal Integ.thy
- "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z";
+val prems = Goal "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z";
by (cut_inst_tac [("P","znegative z")] excluded_middle 1);
by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1);
qed "int_cases";
--- a/src/HOL/Lfp.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Lfp.ML Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For lfp.thy. The Knaster-Tarski Theorem
+The Knaster-Tarski Theorem
*)
open Lfp;
@@ -12,34 +12,34 @@
(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
-val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
+Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
by (rtac (CollectI RS Inter_lower) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
qed "lfp_lowerbound";
-val prems = goalw Lfp.thy [lfp_def]
+val prems = Goalw [lfp_def]
"[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
by (etac CollectD 1);
qed "lfp_greatest";
-val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
+Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
- rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
+ etac monoD, rtac lfp_lowerbound, atac, atac]);
qed "lfp_lemma2";
-val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
-by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD),
- rtac lfp_lemma2, rtac mono]);
+Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
+by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
+ etac lfp_lemma2]);
qed "lfp_lemma3";
-val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
-by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
+Goal "mono(f) ==> lfp(f) = f(lfp(f))";
+by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
qed "lfp_Tarski";
(*** General induction rule for least fixed points ***)
-val [lfp,mono,indhyp] = goal Lfp.thy
+val [lfp,mono,indhyp] = Goal
"[| a: lfp(f); mono(f); \
\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
@@ -62,7 +62,7 @@
by (rtac (mono RS lfp_Tarski) 1);
qed "def_lfp_Tarski";
-val rew::prems = goal Lfp.thy
+val rew::prems = Goal
"[| A == lfp(f); mono(f); a:A; \
\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
@@ -71,7 +71,7 @@
qed "def_induct";
(*Monotonicity of lfp!*)
-val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
+val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
by (rtac (lfp_lowerbound RS lfp_greatest) 1);
by (etac (prem RS subset_trans) 1);
qed "lfp_mono";
--- a/src/HOL/List.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/List.ML Thu Aug 13 18:14:26 1998 +0200
@@ -8,14 +8,14 @@
Goal "!x. xs ~= x#xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "not_Cons_self";
bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
Addsimps [not_Cons_self,not_Cons_self2];
Goal "(xs ~= []) = (? y ys. xs = y#ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "neq_Nil_conv";
(* Induction over the length of a list: *)
@@ -71,43 +71,43 @@
Goal "length(xs@ys) = length(xs)+length(ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed"length_append";
Addsimps [length_append];
Goal "length (map f xs) = length xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_map";
Addsimps [length_map];
Goal "length(rev xs) = length(xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_rev";
Addsimps [length_rev];
Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
by (exhaust_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_tl";
Addsimps [length_tl];
Goal "(length xs = 0) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_0_conv";
AddIffs [length_0_conv];
Goal "(0 = length xs) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "zero_length_conv";
AddIffs [zero_length_conv];
Goal "(0 < length xs) = (xs ~= [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_greater_0_conv";
AddIffs [length_greater_0_conv];
@@ -123,36 +123,36 @@
Goal "(xs@ys)@zs = xs@(ys@zs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "append_assoc";
Addsimps [append_assoc];
Goal "xs @ [] = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "append_Nil2";
Addsimps [append_Nil2];
Goal "(xs@ys = []) = (xs=[] & ys=[])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "append_is_Nil_conv";
AddIffs [append_is_Nil_conv];
Goal "([] = xs@ys) = (xs=[] & ys=[])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "Nil_is_append_conv";
AddIffs [Nil_is_append_conv];
Goal "(xs @ ys = xs) = (ys=[])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "append_self_conv";
Goal "(xs = xs @ ys) = (ys=[])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "self_append_conv";
AddIffs [append_self_conv,self_append_conv];
@@ -192,7 +192,7 @@
Goal "(xs @ ys = ys) = (xs=[])";
by (cut_inst_tac [("zs","[]")] append_same_eq 1);
-by (Auto_tac);
+by Auto_tac;
qed "append_self_conv2";
Goal "(ys = xs @ ys) = (xs=[])";
@@ -204,13 +204,13 @@
Goal "xs ~= [] --> hd xs # tl xs = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "hd_Cons_tl";
Addsimps [hd_Cons_tl];
Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "hd_append";
Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
@@ -252,31 +252,31 @@
Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
Goal "map (%x. x) = (%xs. xs)";
by (rtac ext 1);
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "map_ident";
Addsimps[map_ident];
Goal "map f (xs@ys) = map f xs @ map f ys";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "map_append";
Addsimps[map_append];
Goalw [o_def] "map (f o g) xs = map f (map g xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "map_compose";
Addsimps[map_compose];
Goal "rev(map f xs) = map f (rev xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "rev_map";
(* a congruence rule for map: *)
@@ -284,19 +284,19 @@
by (rtac impI 1);
by (hyp_subst_tac 1);
by (induct_tac "ys" 1);
-by (Auto_tac);
+by Auto_tac;
val lemma = result();
bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
Goal "(map f xs = []) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "map_is_Nil_conv";
AddIffs [map_is_Nil_conv];
Goal "([] = map f xs) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "Nil_is_map_conv";
AddIffs [Nil_is_map_conv];
@@ -307,25 +307,25 @@
Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "rev_append";
Addsimps[rev_append];
Goal "rev(rev l) = l";
by (induct_tac "l" 1);
-by (Auto_tac);
+by Auto_tac;
qed "rev_rev_ident";
Addsimps[rev_rev_ident];
Goal "(rev xs = []) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "rev_is_Nil_conv";
AddIffs [rev_is_Nil_conv];
Goal "([] = rev xs) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "Nil_is_rev_conv";
AddIffs [Nil_is_rev_conv];
@@ -341,7 +341,7 @@
Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";
by (res_inst_tac [("xs","xs")] rev_induct 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm ("rev_exhaust",
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
@@ -352,13 +352,13 @@
Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "mem_append";
Addsimps[mem_append];
Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "mem_filter";
Addsimps[mem_filter];
@@ -373,40 +373,40 @@
Goal "set (xs@ys) = (set xs Un set ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "set_append";
Addsimps[set_append];
Goal "(x mem xs) = (x: set xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "set_mem_eq";
Goal "set l <= set (x#l)";
-by (Auto_tac);
+by Auto_tac;
qed "set_subset_Cons";
Goal "(set xs = {}) = (xs = [])";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "set_empty";
Addsimps [set_empty];
Goal "set(rev xs) = set(xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "set_rev";
Addsimps [set_rev];
Goal "set(map f xs) = f``(set xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "set_map";
Addsimps [set_map];
Goal "(x : set(filter P xs)) = (x : set xs & P x)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "in_set_filter";
Addsimps [in_set_filter];
@@ -418,14 +418,14 @@
by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
by(REPEAT(etac exE 1));
by(exhaust_tac "ys" 1);
-by(Auto_tac);
+by Auto_tac;
qed "in_set_conv_decomp";
(* eliminate `lists' in favour of `set' *)
Goal "(xs : lists A) = (!x : set xs. x : A)";
by(induct_tac "xs" 1);
-by(Auto_tac);
+by Auto_tac;
qed "in_lists_conv_set";
bind_thm("in_listsD",in_lists_conv_set RS iffD1);
@@ -439,19 +439,19 @@
Goal "list_all (%x. True) xs = True";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "list_all_True";
Addsimps [list_all_True];
Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "list_all_append";
Addsimps [list_all_append];
Goal "list_all P xs = (!x. x mem xs --> P(x))";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "list_all_mem_conv";
@@ -461,25 +461,25 @@
Goal "filter P (xs@ys) = filter P xs @ filter P ys";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "filter_append";
Addsimps [filter_append];
Goal "filter (%x. True) xs = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "filter_True";
Addsimps [filter_True];
Goal "filter (%x. False) xs = []";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "filter_False";
Addsimps [filter_False];
Goal "length (filter P xs) <= length xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_filter";
@@ -489,41 +489,41 @@
Goal "concat(xs@ys) = concat(xs)@concat(ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed"concat_append";
Addsimps [concat_append];
Goal "(concat xss = []) = (!xs:set xss. xs=[])";
by (induct_tac "xss" 1);
-by (Auto_tac);
+by Auto_tac;
qed "concat_eq_Nil_conv";
AddIffs [concat_eq_Nil_conv];
Goal "([] = concat xss) = (!xs:set xss. xs=[])";
by (induct_tac "xss" 1);
-by (Auto_tac);
+by Auto_tac;
qed "Nil_eq_concat_conv";
AddIffs [Nil_eq_concat_conv];
Goal "set(concat xs) = Union(set `` set xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed"set_concat";
Addsimps [set_concat];
Goal "map f (concat xs) = concat (map (map f) xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "map_concat";
Goal "filter p (concat xs) = concat (map (filter p) xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed"filter_concat";
Goal "rev(concat xs) = concat (map rev (rev xs))";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "rev_concat";
(** nth **)
@@ -535,7 +535,7 @@
by (Asm_simp_tac 1);
by (rtac allI 1);
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "nth_append";
Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
@@ -545,7 +545,7 @@
(* case x#xl *)
by (rtac allI 1);
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "nth_map";
Addsimps [nth_map];
@@ -556,7 +556,7 @@
(* case x#xl *)
by (rtac allI 1);
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "list_all_nth";
Goal "!n. n < length xs --> xs!n mem xs";
@@ -589,30 +589,30 @@
Goal "last(xs@[x]) = x";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "last_snoc";
Addsimps [last_snoc];
Goal "butlast(xs@[x]) = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "butlast_snoc";
Addsimps [butlast_snoc];
Goal "length(butlast xs) = length xs - 1";
by (res_inst_tac [("xs","xs")] rev_induct 1);
-by (Auto_tac);
+by Auto_tac;
qed "length_butlast";
Addsimps [length_butlast];
Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "butlast_append";
Goal "x:set(butlast xs) --> x:set xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "in_set_butlastD";
Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
@@ -631,12 +631,12 @@
Goal "take 0 xs = []";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "take_0";
Goal "drop 0 xs = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "drop_0";
Goal "take (Suc n) (x#xs) = x # take n xs";
@@ -652,102 +652,102 @@
Goal "!xs. length(take n xs) = min (length xs) n";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "length_take";
Addsimps [length_take];
Goal "!xs. length(drop n xs) = (length xs - n)";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "length_drop";
Addsimps [length_drop];
Goal "!xs. length xs <= n --> take n xs = xs";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "take_all";
Goal "!xs. length xs <= n --> drop n xs = []";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "drop_all";
Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "take_append";
Addsimps [take_append];
Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "drop_append";
Addsimps [drop_append];
Goal "!xs n. take n (take m xs) = take (min n m) xs";
by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "na" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "take_take";
Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "drop_drop";
Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
by (induct_tac "m" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "take_drop";
Goal "!xs. take n (map f xs) = map f (take n xs)";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "take_map";
Goal "!xs. drop n (map f xs) = map f (drop n xs)";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "drop_map";
Goal "!n i. i < n --> (take n xs)!i = xs!i";
by (induct_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "n" 1);
by (Blast_tac 1);
by (exhaust_tac "i" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "nth_take";
Addsimps [nth_take];
Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
by (induct_tac "n" 1);
- by (Auto_tac);
+ by Auto_tac;
by (exhaust_tac "xs" 1);
- by (Auto_tac);
+ by Auto_tac;
qed_spec_mp "nth_drop";
Addsimps [nth_drop];
@@ -757,37 +757,37 @@
Goal "takeWhile P xs @ dropWhile P xs = xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "takeWhile_dropWhile_id";
Addsimps [takeWhile_dropWhile_id];
Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
Addsimps [takeWhile_append1];
Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
Addsimps [takeWhile_append2];
Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
Addsimps [dropWhile_append1];
Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
Addsimps [dropWhile_append2];
Goal "x:set(takeWhile P xs) --> x:set xs & P x";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp"set_take_whileD";
qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);
@@ -800,7 +800,7 @@
Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
by(induct_tac "xs" 1);
-by(Auto_tac);
+by Auto_tac;
qed_spec_mp "foldl_append";
Addsimps [foldl_append];
@@ -821,7 +821,7 @@
Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
by(induct_tac "ns" 1);
-by(Auto_tac);
+by Auto_tac;
qed_spec_mp "sum_eq_0_conv";
AddIffs [sum_eq_0_conv];
@@ -838,12 +838,12 @@
Goal "nodups(remdups xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed "nodups_remdups";
Goal "nodups xs --> nodups (filter P xs)";
by (induct_tac "xs" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "nodups_filter";
(** replicate **)
@@ -851,7 +851,7 @@
Goal "set(replicate (Suc n) x) = {x}";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
val lemma = result();
Goal "n ~= 0 ==> set(replicate n x) = {x}";
--- a/src/HOL/Nat.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Nat.ML Thu Aug 13 18:14:26 1998 +0200
@@ -9,12 +9,12 @@
val [nat_rec_0, nat_rec_Suc] = nat.recs;
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
-val prems = goal thy
+val prems = Goal
"[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
by (simp_tac (simpset() addsimps prems) 1);
qed "def_nat_rec_0";
-val prems = goal thy
+val prems = Goal
"[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
by (simp_tac (simpset() addsimps prems) 1);
qed "def_nat_rec_Suc";
@@ -26,9 +26,8 @@
by (REPEAT (Blast_tac 1));
qed "not0_implies_Suc";
-val prems = goal thy "m<n ==> n ~= 0";
+Goal "m<n ==> n ~= 0";
by (exhaust_tac "n" 1);
-by (cut_facts_tac prems 1);
by (ALLGOALS Asm_full_simp_tac);
qed "gr_implies_not0";
--- a/src/HOL/NatDef.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/NatDef.ML Thu Aug 13 18:14:26 1998 +0200
@@ -20,22 +20,22 @@
by (rtac (singletonI RS UnI1) 1);
qed "Zero_RepI";
-val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat";
+Goal "i: Nat ==> Suc_Rep(i) : Nat";
by (stac Nat_unfold 1);
by (rtac (imageI RS UnI2) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
qed "Suc_RepI";
(*** Induction ***)
-val major::prems = goal thy
+val major::prems = Goal
"[| i: Nat; P(Zero_Rep); \
\ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)";
by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
by (blast_tac (claset() addIs prems) 1);
qed "Nat_induct";
-val prems = goalw thy [Zero_def,Suc_def]
+val prems = Goalw [Zero_def,Suc_def]
"[| P(0); \
\ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)";
by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*)
@@ -49,7 +49,7 @@
res_inst_tac [("n",a)] nat_induct i THEN rename_last_tac a [""] (i+1);
(*A special form of induction for reasoning about m<n and m-n*)
-val prems = goal thy
+val prems = Goal
"[| !!x. P x 0; \
\ !!y. P 0 (Suc y); \
\ !!x y. [| P x y |] ==> P (Suc x) (Suc y) \
@@ -131,10 +131,10 @@
(** Introduction properties **)
-val prems = goalw thy [less_def] "[| i<j; j<k |] ==> i<(k::nat)";
+Goalw [less_def] "[| i<j; j<k |] ==> i<(k::nat)";
by (rtac (trans_trancl RS transD) 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
qed "less_trans";
Goalw [less_def, pred_nat_def] "n < Suc(n)";
@@ -156,8 +156,8 @@
(** Elimination properties **)
-val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
-by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+Goalw [less_def] "n<m ==> ~ m<(n::nat)";
+by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1);
qed "less_not_sym";
(* [| n<m; m<n |] ==> R *)
@@ -176,7 +176,7 @@
qed "less_not_refl2";
-val major::prems = goalw thy [less_def, pred_nat_def]
+val major::prems = Goalw [less_def, pred_nat_def]
"[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \
\ |] ==> P";
by (rtac (major RS tranclE) 1);
@@ -197,7 +197,7 @@
(* n<0 ==> R *)
bind_thm ("less_zeroE", not_less0 RS notE);
-val [major,less,eq] = goal thy
+val [major,less,eq] = Goal
"[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P";
by (rtac (major RS lessE) 1);
by (rtac eq 1);
@@ -254,14 +254,14 @@
by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
qed "Suc_lessI";
-val [prem] = goal thy "Suc(m) < n ==> m<n";
-by (rtac (prem RS rev_mp) 1);
+Goal "Suc(m) < n ==> m<n";
+by (etac rev_mp 1);
by (nat_ind_tac "n" 1);
by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI]
addEs [less_trans, lessE])));
qed "Suc_lessD";
-val [major,minor] = goal thy
+val [major,minor] = Goal
"[| Suc(i)<k; !!j. [| i<j; k=Suc(j) |] ==> P \
\ |] ==> P";
by (rtac (major RS lessE) 1);
@@ -299,7 +299,7 @@
qed "not_less_eq";
(*Complete induction, aka course-of-values induction*)
-val prems = goalw thy [less_def]
+val prems = Goalw [less_def]
"[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |] ==> P(n)";
by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
by (eresolve_tac prems 1);
@@ -350,12 +350,12 @@
but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
*)
-val prems = goalw thy [le_def] "~n<m ==> m<=(n::nat)";
-by (resolve_tac prems 1);
+Goalw [le_def] "~n<m ==> m<=(n::nat)";
+by (assume_tac 1);
qed "leI";
-val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)";
-by (resolve_tac prems 1);
+Goalw [le_def] "m<=n ==> ~ n < (m::nat)";
+by (assume_tac 1);
qed "leD";
val leE = make_elim leD;
@@ -505,7 +505,7 @@
by (simp_tac (simpset() addsimps [lemma]) 1);
qed "Least_nat_def";
-val [prem1,prem2] = goalw thy [Least_nat_def]
+val [prem1,prem2] = Goalw [Least_nat_def]
"[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
by (rtac select_equality 1);
by (blast_tac (claset() addSIs [prem1,prem2]) 1);
@@ -513,8 +513,8 @@
by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
qed "Least_equality";
-val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
-by (rtac (prem RS rev_mp) 1);
+Goal "P(k::nat) ==> P(LEAST x. P(x))";
+by (etac rev_mp 1);
by (res_inst_tac [("n","k")] less_induct 1);
by (rtac impI 1);
by (rtac classical 1);
@@ -525,8 +525,8 @@
qed "LeastI";
(*Proof is almost identical to the one above!*)
-val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
-by (rtac (prem RS rev_mp) 1);
+Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
+by (etac rev_mp 1);
by (res_inst_tac [("n","k")] less_induct 1);
by (rtac impI 1);
by (rtac classical 1);
@@ -536,10 +536,9 @@
by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1);
qed "Least_le";
-val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
+Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)";
by (rtac notI 1);
-by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
-by (rtac prem 1);
+by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
qed "not_less_Least";
(*** Instantiation of transitivity prover ***)
--- a/src/HOL/Ord.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Ord.ML Thu Aug 13 18:14:26 1998 +0200
@@ -8,15 +8,13 @@
(** mono **)
-val [prem] = goalw Ord.thy [mono_def]
+val [prem] = Goalw [mono_def]
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
by (REPEAT (ares_tac [allI, impI, prem] 1));
qed "monoI";
-val [major,minor] = goalw Ord.thy [mono_def]
- "[| mono(f); A <= B |] ==> f(A) <= f(B)";
-by (rtac (major RS spec RS spec RS mp) 1);
-by (rtac minor 1);
+Goalw [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)";
+by (Fast_tac 1);
qed "monoD";
@@ -46,7 +44,7 @@
by (simp_tac (simpset() addsimps prems) 1);
qed "min_leastL";
-val prems = goalw thy [min_def]
+val prems = Goalw [min_def]
"(!!x::'a::order. least <= x) ==> min x least = least";
by (cut_facts_tac prems 1);
by (Asm_simp_tac 1);
--- a/src/HOL/Prod.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Prod.ML Thu Aug 13 18:14:26 1998 +0200
@@ -24,7 +24,7 @@
by (etac Abs_Prod_inverse 1);
qed "inj_on_Abs_Prod";
-val prems = goalw Prod.thy [Pair_def]
+val prems = Goalw [Pair_def]
"[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R";
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
by (REPEAT (ares_tac (prems@[ProdI]) 1));
@@ -49,7 +49,7 @@
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]);
qed "PairE_lemma";
-val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
+val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
by (rtac (PairE_lemma RS exE) 1);
by (REPEAT (eresolve_tac [prem,exE] 1));
qed "PairE";
@@ -222,7 +222,7 @@
by (Asm_simp_tac 1);
qed "splitI";
-val prems = goalw Prod.thy [split_def]
+val prems = Goalw [split_def]
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "splitE";
@@ -246,7 +246,7 @@
by (Asm_simp_tac 1);
qed "mem_splitI2";
-val prems = goalw Prod.thy [split_def]
+val prems = Goalw [split_def]
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "mem_splitE";
@@ -298,13 +298,13 @@
qed "prod_fun_ident";
Addsimps [prod_fun_ident];
-val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
by (rtac image_eqI 1);
by (rtac (prod_fun RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
qed "prod_fun_imageI";
-val major::prems = goal Prod.thy
+val major::prems = Goal
"[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
\ |] ==> P";
by (rtac (major RS imageE) 1);
@@ -354,7 +354,7 @@
AddSEs [SigmaE2, SigmaE];
-val prems = goal Prod.thy
+val prems = Goal
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
by (cut_facts_tac prems 1);
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
@@ -384,14 +384,14 @@
(*** Domain of a relation ***)
-val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
+Goalw [image_def] "(a,b) : r ==> a : fst``r";
by (rtac CollectI 1);
by (rtac bexI 1);
by (rtac (fst_conv RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
qed "fst_imageI";
-val major::prems = goal Prod.thy
+val major::prems = Goal
"[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (resolve_tac prems 1);
@@ -402,15 +402,14 @@
(*** Range of a relation ***)
-val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
+Goalw [image_def] "(a,b) : r ==> b : snd``r";
by (rtac CollectI 1);
by (rtac bexI 1);
by (rtac (snd_conv RS sym) 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
qed "snd_imageI";
-val major::prems = goal Prod.thy
- "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P";
+val major::prems = Goal "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (resolve_tac prems 1);
by (etac ssubst 1);
--- a/src/HOL/RelPow.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/RelPow.ML Thu Aug 13 18:14:26 1998 +0200
@@ -31,14 +31,14 @@
by (Asm_full_simp_tac 1);
qed "rel_pow_0_E";
-val [major,minor] = goal RelPow.thy
+val [major,minor] = Goal
"[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
by (cut_facts_tac [major] 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [minor]) 1);
qed "rel_pow_Suc_E";
-val [p1,p2,p3] = goal RelPow.thy
+val [p1,p2,p3] = Goal
"[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
\ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \
\ |] ==> P";
@@ -52,18 +52,20 @@
Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
by (nat_ind_tac "n" 1);
-by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (claset() addIs [rel_pow_0_I]
+ addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (claset() addIs [rel_pow_Suc_I]
+ addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
qed_spec_mp "rel_pow_Suc_D2";
Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
by (nat_ind_tac "n" 1);
-by (fast_tac (claset() addss (simpset())) 1);
-by (fast_tac (claset() addss (simpset())) 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
qed_spec_mp "rel_pow_Suc_D2'";
-val [p1,p2,p3] = goal RelPow.thy
+val [p1,p2,p3] = Goal
"[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
\ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \
\ |] ==> P";
--- a/src/HOL/Relation.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Relation.ML Thu Aug 13 18:14:26 1998 +0200
@@ -12,7 +12,7 @@
by (Blast_tac 1);
qed "idI";
-val major::prems = goalw thy [id_def]
+val major::prems = Goalw [id_def]
"[| p: id; !!x.[| p = (x,x) |] ==> P \
\ |] ==> P";
by (rtac (major RS CollectE) 1);
@@ -34,7 +34,7 @@
qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
-val prems = goalw thy [comp_def]
+val prems = Goalw [comp_def]
"[| xz : r O s; \
\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \
\ |] ==> P";
@@ -43,7 +43,7 @@
ORELSE ares_tac prems 1));
qed "compE";
-val prems = goal thy
+val prems = Goal
"[| (a,c) : r O s; \
\ !!y. [| (a,y):s; (y,c):r |] ==> P \
\ |] ==> P";
@@ -78,7 +78,7 @@
(** Natural deduction for trans(r) **)
-val prems = goalw thy [trans_def]
+val prems = Goalw [trans_def]
"(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)";
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
qed "transI";
--- a/src/HOL/Set.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Set.ML Thu Aug 13 18:14:26 1998 +0200
@@ -17,17 +17,17 @@
by (Asm_simp_tac 1);
qed "CollectI";
-val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
+Goal "a : {x. P(x)} ==> P(a)";
by (Asm_full_simp_tac 1);
qed "CollectD";
-val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
+val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
by (rtac Collect_mem_eq 1);
by (rtac Collect_mem_eq 1);
qed "set_ext";
-val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
+val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
by (rtac (prem RS ext RS arg_cong) 1);
qed "Collect_cong";
@@ -39,17 +39,16 @@
section "Bounded quantifiers";
-val prems = goalw Set.thy [Ball_def]
+val prems = Goalw [Ball_def]
"[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
qed "ballI";
-val [major,minor] = goalw Set.thy [Ball_def]
- "[| ! x:A. P(x); x:A |] ==> P(x)";
-by (rtac (minor RS (major RS spec RS mp)) 1);
+Goalw [Ball_def] "[| ! x:A. P(x); x:A |] ==> P(x)";
+by (Blast_tac 1);
qed "bspec";
-val major::prems = goalw Set.thy [Ball_def]
+val major::prems = Goalw [Ball_def]
"[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
by (rtac (major RS spec RS impCE) 1);
by (REPEAT (eresolve_tac prems 1));
@@ -61,9 +60,8 @@
AddSIs [ballI];
AddEs [ballE];
-val prems = goalw Set.thy [Bex_def]
- "[| P(x); x:A |] ==> ? x:A. P(x)";
-by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
+Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)";
+by (Blast_tac 1);
qed "bexI";
qed_goal "bexCI" Set.thy
@@ -72,7 +70,7 @@
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
-val major::prems = goalw Set.thy [Bex_def]
+val major::prems = Goalw [Bex_def]
"[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q";
by (rtac (major RS exE) 1);
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
@@ -95,7 +93,7 @@
(** Congruence rules **)
-val prems = goal Set.thy
+val prems = Goal
"[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
\ (! x:A. P(x)) = (! x:B. Q(x))";
by (resolve_tac (prems RL [ssubst]) 1);
@@ -103,7 +101,7 @@
ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
qed "ball_cong";
-val prems = goal Set.thy
+val prems = Goal
"[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
\ (? x:A. P(x)) = (? x:B. Q(x))";
by (resolve_tac (prems RL [ssubst]) 1);
@@ -113,7 +111,7 @@
section "Subsets";
-val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
+val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
by (REPEAT (ares_tac (prems @ [ballI]) 1));
qed "subsetI";
@@ -130,9 +128,8 @@
Blast.overloaded ("op ``", domain_type o domain_type);
(*Rule in Modus Ponens style*)
-val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B";
-by (rtac (major RS bspec) 1);
-by (resolve_tac prems 1);
+Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";
+by (Blast_tac 1);
qed "subsetD";
(*The same, with reversed premises for use with etac -- cf rev_mp*)
@@ -149,7 +146,7 @@
(fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
(*Classical elimination rule*)
-val major::prems = goalw Set.thy [subset_def]
+val major::prems = Goalw [subset_def]
"[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
by (rtac (major RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
@@ -164,7 +161,7 @@
qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
(fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*)
-val prems = goal Set.thy "!!B. [| A<=B; B<=C |] ==> A<=(C::'a set)";
+Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)";
by (Blast_tac 1);
qed "subset_trans";
@@ -172,32 +169,32 @@
section "Equality";
(*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)";
-by (rtac (iffI RS set_ext) 1);
-by (REPEAT (ares_tac (prems RL [subsetD]) 1));
+Goal "[| A <= B; B <= A |] ==> A = (B::'a set)";
+br set_ext 1;
+by (blast_tac (claset() addIs [subsetD]) 1);
qed "subset_antisym";
val equalityI = subset_antisym;
AddSIs [equalityI];
(* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
-by (resolve_tac (prems RL [subst]) 1);
+Goal "A = B ==> A<=(B::'a set)";
+by (etac ssubst 1);
by (rtac subset_refl 1);
qed "equalityD1";
-val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
-by (resolve_tac (prems RL [subst]) 1);
+Goal "A = B ==> B<=(A::'a set)";
+by (etac ssubst 1);
by (rtac subset_refl 1);
qed "equalityD2";
-val prems = goal Set.thy
+val prems = Goal
"[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P";
by (resolve_tac prems 1);
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
qed "equalityE";
-val major::prems = goal Set.thy
+val major::prems = Goal
"[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
by (rtac (major RS equalityE) 1);
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
@@ -206,7 +203,7 @@
(*Lemma for creating induction formulae -- for "pattern matching" on p
To make the induction hypotheses usable, apply "spec" or "bspec" to
put universal quantifiers over the free variables in p. *)
-val prems = goal Set.thy
+val prems = Goal
"[| p:A; !!z. z:A ==> p=z --> R |] ==> R";
by (rtac mp 1);
by (REPEAT (resolve_tac (refl::prems) 1));
@@ -305,17 +302,15 @@
Addsimps [Compl_iff];
-val prems = goalw Set.thy [Compl_def]
- "[| c:A ==> False |] ==> c : Compl(A)";
+val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
qed "ComplI";
(*This form, with negated conclusion, works well with the Classical prover.
Negated assumptions behave like formulae on the right side of the notional
turnstile...*)
-val major::prems = goalw Set.thy [Compl_def]
- "c : Compl(A) ==> c~:A";
-by (rtac (major RS CollectD) 1);
+Goalw [Compl_def] "c : Compl(A) ==> c~:A";
+by (etac CollectD 1);
qed "ComplD";
val ComplE = make_elim ComplD;
@@ -345,7 +340,7 @@
[ (Simp_tac 1),
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
-val major::prems = goalw Set.thy [Un_def]
+val major::prems = Goalw [Un_def]
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
by (rtac (major RS CollectD RS disjE) 1);
by (REPEAT (eresolve_tac prems 1));
@@ -374,7 +369,7 @@
by (Asm_full_simp_tac 1);
qed "IntD2";
-val [major,minor] = goal Set.thy
+val [major,minor] = Goal
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P";
by (rtac minor 1);
by (rtac (major RS IntD1) 1);
@@ -479,7 +474,7 @@
by Auto_tac;
qed "UN_I";
-val major::prems = goalw Set.thy [UNION_def]
+val major::prems = Goalw [UNION_def]
"[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R";
by (rtac (major RS CollectD RS bexE) 1);
by (REPEAT (ares_tac prems 1));
@@ -488,7 +483,7 @@
AddIs [UN_I];
AddSEs [UN_E];
-val prems = goal Set.thy
+val prems = Goal
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
\ (UN x:A. C(x)) = (UN x:B. D(x))";
by (REPEAT (etac UN_E 1
@@ -505,7 +500,7 @@
Addsimps [INT_iff];
-val prems = goalw Set.thy [INTER_def]
+val prems = Goalw [INTER_def]
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
qed "INT_I";
@@ -515,7 +510,7 @@
qed "INT_D";
(*"Classical" elimination -- by the Excluded Middle on a:A *)
-val major::prems = goalw Set.thy [INTER_def]
+val major::prems = Goalw [INTER_def]
"[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R";
by (rtac (major RS CollectD RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
@@ -524,7 +519,7 @@
AddSIs [INT_I];
AddEs [INT_D, INT_E];
-val prems = goal Set.thy
+val prems = Goal
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
\ (INT x:A. C(x)) = (INT x:B. D(x))";
by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
@@ -546,7 +541,7 @@
by Auto_tac;
qed "UnionI";
-val major::prems = goalw Set.thy [Union_def]
+val major::prems = Goalw [Union_def]
"[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R";
by (rtac (major RS UN_E) 1);
by (REPEAT (ares_tac prems 1));
@@ -564,7 +559,7 @@
Addsimps [Inter_iff];
-val prems = goalw Set.thy [Inter_def]
+val prems = Goalw [Inter_def]
"[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
by (REPEAT (ares_tac ([INT_I] @ prems) 1));
qed "InterI";
@@ -576,7 +571,7 @@
qed "InterD";
(*"Classical" elimination rule -- does not require proving X:C *)
-val major::prems = goalw Set.thy [Inter_def]
+val major::prems = Goalw [Inter_def]
"[| A : Inter(C); X~:C ==> R; A:X ==> R |] ==> R";
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
@@ -589,15 +584,15 @@
(*** Image of a set under a function ***)
(*Frequently b does not have the syntactic form of f(x).*)
-val prems = goalw thy [image_def] "[| b=f(x); x:A |] ==> b : f``A";
-by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
+Goalw [image_def] "[| b=f(x); x:A |] ==> b : f``A";
+by (Blast_tac 1);
qed "image_eqI";
Addsimps [image_eqI];
bind_thm ("imageI", refl RS image_eqI);
(*The eta-expansion gives variable-name preservation.*)
-val major::prems = goalw thy [image_def]
+val major::prems = Goalw [image_def]
"[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
by (rtac (major RS CollectD RS bexE) 1);
by (REPEAT (ares_tac prems 1));
@@ -621,7 +616,7 @@
(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
many existing proofs.*)
-val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
+val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
by (blast_tac (claset() addIs prems) 1);
qed "image_subsetI";
@@ -634,7 +629,7 @@
bind_thm ("rangeI", UNIV_I RS imageI);
-val [major,minor] = goal thy
+val [major,minor] = Goal
"[| b : range(%x. f(x)); !!x. b=f(x) ==> P |] ==> P";
by (rtac (major RS imageE) 1);
by (etac minor 1);
--- a/src/HOL/Sum.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Sum.ML Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-For Sum.thy. The disjoint sum of two types
+The disjoint sum of two types
*)
open Sum;
@@ -51,13 +51,13 @@
(** Injectiveness of Inl and Inr **)
-val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
-by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
by (Blast_tac 1);
qed "Inl_Rep_inject";
-val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
-by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
by (Blast_tac 1);
qed "Inr_Rep_inject";
@@ -101,7 +101,7 @@
(** Elimination rules **)
-val major::prems = goalw Sum.thy [sum_def]
+val major::prems = Goalw [sum_def]
"[| u: A Plus B; \
\ !!x. [| x:A; u=Inl(x) |] ==> P; \
\ !!y. [| y:B; u=Inr(y) |] ==> P \
@@ -130,7 +130,7 @@
(** Exhaustion rule for sums -- a degenerate form of induction **)
-val prems = goalw Sum.thy [Inl_def,Inr_def]
+val prems = Goalw [Inl_def,Inr_def]
"[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \
\ |] ==> P";
by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
@@ -140,7 +140,7 @@
rtac (Rep_Sum_inverse RS sym)]));
qed "sumE";
-val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
+val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
by (res_inst_tac [("s","x")] sumE 1);
by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
qed "sum_induct";
@@ -177,7 +177,7 @@
val PartI = refl RSN (2,Part_eqI);
-val major::prems = goalw Sum.thy [Part_def]
+val major::prems = Goalw [Part_def]
"[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \
\ |] ==> P";
by (rtac (major RS IntE) 1);
--- a/src/HOL/Trancl.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Trancl.ML Thu Aug 13 18:14:26 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For Trancl.thy. Theorems about the transitive closure of a relation
+Theorems about the transitive closure of a relation
*)
open Trancl;
@@ -46,7 +46,7 @@
(** standard induction rule **)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a,b) : r^*; \
\ !!x. P((x,x)); \
\ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \
@@ -56,7 +56,7 @@
qed "rtrancl_full_induct";
(*nice induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a::'a,b) : r^*; \
\ P(a); \
\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \
@@ -85,7 +85,7 @@
(*elimination of rtrancl -- by induction on a special formula*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a::'a,b) : r^*; (a = b) ==> P; \
\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \
\ |] ==> P";
@@ -133,8 +133,9 @@
qed "rtrancl_subset";
Goal "(R^* Un S^*)^* = (R Un S)^*";
-by (blast_tac (claset() addSIs [rtrancl_subset]
- addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
+(*Blast_tac: PROOF FAILED*)
+by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
+ addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
qed "rtrancl_Un_rtrancl";
Goal "(R^=)^* = R^*";
@@ -160,7 +161,7 @@
by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
qed "rtrancl_converse";
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a,b) : r^*; P(b); \
\ !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] \
\ ==> P(a)";
@@ -169,7 +170,7 @@
by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
qed "converse_rtrancl_induct";
-val prems = goal Trancl.thy
+val prems = Goal
"[| ((a,b),(c,d)) : r^*; P c d; \
\ !!x y z u.[| ((x,y),(z,u)) : r; ((z,u),(c,d)) : r^*; P z u |] ==> P x y\
\ |] ==> P a b";
@@ -183,7 +184,7 @@
by (REPEAT(ares_tac prems 1));
qed "converse_rtrancl_induct2";
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (x,z):r^*; \
\ x=z ==> P; \
\ !!y. [| (x,y):r; (y,z):r^* |] ==> P \
@@ -237,7 +238,7 @@
qed "rtrancl_into_trancl2";
(*Nice induction rule for trancl*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a,b) : r^+; \
\ !!y. [| (a,y) : r |] ==> P(y); \
\ !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) \
@@ -252,7 +253,7 @@
qed "trancl_induct";
(*elimination of r^+ -- NOT an induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| (a::'a,b) : r^+; \
\ (a,b) : r ==> P; \
\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \
--- a/src/HOL/Univ.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Univ.ML Thu Aug 13 18:14:26 1998 +0200
@@ -14,7 +14,7 @@
by (rtac split 1);
qed "apfst_conv";
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
"[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \
\ |] ==> R";
by (rtac PairE 1);
@@ -27,26 +27,27 @@
(** Push -- an injection, analogous to Cons on lists **)
-val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> i=j";
-by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
+Goalw [Push_def] "Push i f = Push j g ==> i=j";
+by (etac (fun_cong RS box_equals RS Suc_inject) 1);
by (rtac nat_case_0 1);
by (rtac nat_case_0 1);
qed "Push_inject1";
-val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> f=g";
-by (rtac (major RS fun_cong RS ext RS box_equals) 1);
+Goalw [Push_def] "Push i f = Push j g ==> f=g";
+by (rtac (ext RS box_equals) 1);
+by (etac fun_cong 1);
by (rtac (nat_case_Suc RS ext) 1);
by (rtac (nat_case_Suc RS ext) 1);
qed "Push_inject2";
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
"[| Push i f =Push j g; [| i=j; f=g |] ==> P \
\ |] ==> P";
by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
qed "Push_inject";
-val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
-by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
+Goalw [Push_def] "Push k f =(%z.0) ==> P";
+by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
by (rtac nat_case_0 1);
by (rtac refl 1);
qed "Push_neq_K0";
@@ -125,7 +126,7 @@
(** Injectiveness of Push_Node **)
-val [major,minor] = goalw Univ.thy [Push_Node_def]
+val [major,minor] = Goalw [Push_Node_def]
"[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P \
\ |] ==> P";
by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
@@ -150,17 +151,17 @@
by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
-val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> M=M'";
-by (rtac (major RS equalityE) 1);
+Goal "Scons M N = Scons M' N' ==> M=M'";
+by (etac equalityE 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
qed "Scons_inject1";
-val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> N=N'";
-by (rtac (major RS equalityE) 1);
+Goal "Scons M N = Scons M' N' ==> N=N'";
+by (etac equalityE 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
qed "Scons_inject2";
-val [major,minor] = goal Univ.thy
+val [major,minor] = Goal
"[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P \
\ |] ==> P";
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
@@ -302,7 +303,7 @@
qed "uprodI";
(*The general elimination rule*)
-val major::prems = goalw Univ.thy [uprod_def]
+val major::prems = Goalw [uprod_def]
"[| c : A<*>B; \
\ !!x y. [| x:A; y:B; c = Scons x y |] ==> P \
\ |] ==> P";
@@ -312,7 +313,7 @@
qed "uprodE";
(*Elimination of a pair -- introduces no eigenvariables*)
-val prems = goal Univ.thy
+val prems = Goal
"[| Scons M N : A<*>B; [| M:A; N:B |] ==> P \
\ |] ==> P";
by (rtac uprodE 1);
@@ -330,7 +331,7 @@
by (Blast_tac 1);
qed "usum_In1I";
-val major::prems = goalw Univ.thy [usum_def]
+val major::prems = Goalw [usum_def]
"[| u : A<+>B; \
\ !!x. [| x:A; u=In0(x) |] ==> P; \
\ !!y. [| y:B; u=In1(y) |] ==> P \
@@ -352,12 +353,12 @@
AddIffs [In0_not_In1, In1_not_In0];
-val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==> M=N";
-by (rtac (major RS Scons_inject2) 1);
+Goalw [In0_def] "In0(M) = In0(N) ==> M=N";
+by (etac (Scons_inject2) 1);
qed "In0_inject";
-val [major] = goalw Univ.thy [In1_def] "In1(M) = In1(N) ==> M=N";
-by (rtac (major RS Scons_inject2) 1);
+Goalw [In1_def] "In1(M) = In1(N) ==> M=N";
+by (etac (Scons_inject2) 1);
qed "In1_inject";
Goal "(In0 M = In0 N) = (M=N)";
@@ -385,14 +386,13 @@
by (Blast_tac 1);
qed "ntrunc_subsetI";
-val [major] = goalw Univ.thy [ntrunc_def]
- "(!!k. ntrunc k M <= N) ==> M<=N";
+val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2,
major RS subsetD]) 1);
qed "ntrunc_subsetD";
(*A generalized form of the take-lemma*)
-val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
+val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
by (rtac equalityI 1);
by (ALLGOALS (rtac ntrunc_subsetD));
by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
@@ -400,7 +400,7 @@
by (rtac (major RS equalityD2) 1);
qed "ntrunc_equality";
-val [major] = goalw Univ.thy [o_def]
+val [major] = Goalw [o_def]
"[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
by (rtac (major RS fun_cong) 1);
@@ -478,7 +478,7 @@
val diagI = refl RS diag_eqI |> standard;
(*The general elimination rule*)
-val major::prems = goalw Univ.thy [diag_def]
+val major::prems = Goalw [diag_def]
"[| c : diag(A); \
\ !!x y. [| x:A; c = (x,x) |] ==> P \
\ |] ==> P";
@@ -494,7 +494,7 @@
qed "dprodI";
(*The general elimination rule*)
-val major::prems = goalw Univ.thy [dprod_def]
+val major::prems = Goalw [dprod_def]
"[| c : r<**>s; \
\ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') |] ==> P \
\ |] ==> P";
@@ -514,7 +514,7 @@
by (Blast_tac 1);
qed "dsum_In1I";
-val major::prems = goalw Univ.thy [dsum_def]
+val major::prems = Goalw [dsum_def]
"[| w : r<++>s; \
\ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \
\ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \
--- a/src/HOL/WF.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/WF.ML Thu Aug 13 18:14:26 1998 +0200
@@ -12,7 +12,7 @@
val H_cong1 = refl RS H_cong;
(*Restriction to domain A. If r is well-founded over A then wf(r)*)
-val [prem1,prem2] = goalw WF.thy [wf_def]
+val [prem1,prem2] = Goalw [wf_def]
"[| r <= A Times A; \
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
\ ==> wf(r)";
@@ -22,7 +22,7 @@
by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
qed "wfI";
-val major::prems = goalw WF.thy [wf_def]
+val major::prems = Goalw [wf_def]
"[| wf(r); \
\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
@@ -36,26 +36,25 @@
rename_last_tac a ["1"] (i+1),
ares_tac prems i];
-val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P";
+Goal "[| wf(r); (a,x):r; (x,a):r |] ==> P";
by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (blast_tac (claset() addIs prems) 1);
-by (wf_ind_tac "a" prems 1);
+by (Blast_tac 1);
+by (wf_ind_tac "a" [] 1);
by (Blast_tac 1);
qed "wf_asym";
-val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P";
-by (rtac wf_asym 1);
-by (REPEAT (resolve_tac prems 1));
+Goal "[| wf(r); (a,a): r |] ==> P";
+by (blast_tac (claset() addEs [wf_asym]) 1);
qed "wf_irrefl";
(*transitive closure of a wf relation is wf! *)
-val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
-by (rewtac wf_def);
+Goal "wf(r) ==> wf(r^+)";
+by (stac wf_def 1);
by (Clarify_tac 1);
(*must retain the universal formula for later use!*)
by (rtac allE 1 THEN assume_tac 1);
by (etac mp 1);
-by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
+by (eres_inst_tac [("a","x")] wf_induct 1);
by (rtac (impI RS allI) 1);
by (etac tranclE 1);
by (Blast_tac 1);
@@ -72,14 +71,13 @@
* Minimal-element characterization of well-foundedness
*---------------------------------------------------------------------------*)
-val wfr::_ = goalw WF.thy [wf_def]
- "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
-by (rtac (wfr RS spec RS mp RS spec) 1);
+Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
+bd spec 1;
+by (etac (mp RS spec) 1);
by (Blast_tac 1);
val lemma1 = result();
-Goalw [wf_def]
- "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
+Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
by (Clarify_tac 1);
by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
by (Blast_tac 1);
@@ -138,11 +136,10 @@
* Wellfoundedness of `disjoint union'
*---------------------------------------------------------------------------*)
-Goal
- "[| !i:I. wf(r i); \
-\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
-\ Domain(r j) Int Range(r i) = {} \
-\ |] ==> wf(UN i:I. r i)";
+Goal "[| !i:I. wf(r i); \
+\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
+\ Domain(r j) Int Range(r i) = {} \
+\ |] ==> wf(UN i:I. r i)";
by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
by(Clarify_tac 1);
by(rename_tac "A a" 1);
@@ -181,9 +178,8 @@
by(Blast_tac 1);
qed "wf_Union";
-Goal
- "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
-\ |] ==> wf(r Un s)";
+Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
+\ |] ==> wf(r Un s)";
br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
by(Blast_tac 1);
by(Blast_tac 1);
@@ -251,10 +247,9 @@
eresolve_tac [transD, mp, allE]));
val wf_super_ss = HOL_ss addSolver indhyp_tac;
-val prems = goalw WF.thy [is_recfun_def,cut_def]
+Goalw [is_recfun_def,cut_def]
"[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \
\ (x,a):r --> (x,b):r --> f(x)=g(x)";
-by (cut_facts_tac prems 1);
by (etac wf_induct 1);
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
@@ -274,15 +269,13 @@
(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
-val prems = goalw WF.thy [the_recfun_def]
+Goalw [the_recfun_def]
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
-by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
-by (resolve_tac prems 1);
+by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
qed "is_the_recfun";
-val prems = goal WF.thy
- "!!r. [| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
-by (wf_ind_tac "a" prems 1);
+Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+by (wf_ind_tac "a" [] 1);
by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
is_the_recfun 1);
by (rewtac is_recfun_def);
@@ -309,7 +302,7 @@
val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
(*--------------Old proof-----------------------------------------------------
-val prems = goal WF.thy
+val prems = Goal
"[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
by (cut_facts_tac prems 1);
by (wf_ind_tac "a" prems 1);
@@ -376,7 +369,7 @@
(*---------------------------------------------------------------------------
* This form avoids giant explosions in proofs. NOTE USE OF ==
*---------------------------------------------------------------------------*)
-val rew::prems = goal WF.thy
+val rew::prems = goal thy
"[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a";
by (rewtac rew);
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
--- a/src/HOL/arith_data.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/arith_data.ML Thu Aug 13 18:14:26 1998 +0200
@@ -56,7 +56,7 @@
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun prove_conv expand_tac norm_tac sg (t, u) =
- meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
+ meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
(K [expand_tac, norm_tac]))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
(string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
--- a/src/HOL/equalities.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/equalities.ML Thu Aug 13 18:14:26 1998 +0200
@@ -136,7 +136,7 @@
qed "if_image_distrib";
Addsimps[if_image_distrib];
-val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
+val prems= Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
by (rtac set_ext 1);
by (simp_tac (simpset() addsimps image_def::prems) 1);
qed "image_cong";
@@ -212,10 +212,6 @@
by (Blast_tac 1);
qed "Int_Un_distrib2";
-Goal "(A<=B) = (A Int B = A)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
-qed "subset_Int_eq";
-
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
by (blast_tac (claset() addEs [equalityCE]) 1);
qed "Int_UNIV";
--- a/src/HOL/mono.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/mono.ML Thu Aug 13 18:14:26 1998 +0200
@@ -6,96 +6,96 @@
Monotonicity of various operations
*)
-goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
+Goal "A<=B ==> f``A <= f``B";
by (Blast_tac 1);
qed "image_mono";
-goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
+Goal "A<=B ==> Pow(A) <= Pow(B)";
by (Blast_tac 1);
qed "Pow_mono";
-goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
+Goal "A<=B ==> Union(A) <= Union(B)";
by (Blast_tac 1);
qed "Union_mono";
-goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
+Goal "B<=A ==> Inter(A) <= Inter(B)";
by (Blast_tac 1);
qed "Inter_anti_mono";
-val prems = goal Set.thy
+val prems = Goal
"[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (UN x:A. f(x)) <= (UN x:B. g(x))";
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "UN_mono";
(*The last inclusion is POSITIVE! *)
-val prems = goal Set.thy
+val prems = Goal
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (INT x:A. f(x)) <= (INT x:A. g(x))";
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "INT_anti_mono";
-goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
+Goal "C<=D ==> insert a C <= insert a D";
by (Blast_tac 1);
qed "insert_mono";
-goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D";
+Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D";
by (Blast_tac 1);
qed "Un_mono";
-goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D";
+Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D";
by (Blast_tac 1);
qed "Int_mono";
-goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
+Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
by (Blast_tac 1);
qed "Diff_mono";
-goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
+Goal "A<=B ==> Compl(B) <= Compl(A)";
by (Blast_tac 1);
qed "Compl_anti_mono";
(** Monotonicity of implications. For inductive definitions **)
-goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
+Goal "A<=B ==> x:A --> x:B";
by (rtac impI 1);
by (etac subsetD 1);
by (assume_tac 1);
qed "in_mono";
-goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
+Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
by (Blast_tac 1);
qed "conj_mono";
-goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
+Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
by (Blast_tac 1);
qed "disj_mono";
-goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
+Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
by (Blast_tac 1);
qed "imp_mono";
-goal HOL.thy "P-->P";
+Goal "P-->P";
by (rtac impI 1);
by (assume_tac 1);
qed "imp_refl";
-val [PQimp] = goal HOL.thy
+val [PQimp] = Goal
"[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
by (blast_tac (claset() addIs [PQimp RS mp]) 1);
qed "ex_mono";
-val [PQimp] = goal HOL.thy
+val [PQimp] = Goal
"[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
by (blast_tac (claset() addIs [PQimp RS mp]) 1);
qed "all_mono";
-val [PQimp] = goal Set.thy
+val [PQimp] = Goal
"[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
by (blast_tac (claset() addIs [PQimp RS mp]) 1);
qed "Collect_mono";
-val [subs,PQimp] = goal Set.thy
+val [subs,PQimp] = Goal
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
\ |] ==> A Int Collect(P) <= B Int Collect(Q)";
by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
--- a/src/HOL/subset.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/subset.ML Thu Aug 13 18:14:26 1998 +0200
@@ -12,32 +12,28 @@
qed_goal "subset_insertI" Set.thy "B <= insert a B"
(fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
-goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
+Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
by (Blast_tac 1);
qed "subset_insert";
(*** Big Union -- least upper bound of a set ***)
-val prems = goal Set.thy
- "B:A ==> B <= Union(A)";
-by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
+Goal "B:A ==> B <= Union(A)";
+by (REPEAT (ares_tac [subsetI,UnionI] 1));
qed "Union_upper";
-val [prem] = goal Set.thy
- "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
+val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
qed "Union_least";
(** General union **)
-val prems = goal Set.thy
- "a:A ==> B(a) <= (UN x:A. B(x))";
-by (REPEAT (ares_tac (prems@[UN_I RS subsetI]) 1));
+Goal "a:A ==> B(a) <= (UN x:A. B(x))";
+by (Blast_tac 1);
qed "UN_upper";
-val [prem] = goal Set.thy
- "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
+val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
qed "UN_least";
@@ -45,52 +41,49 @@
(*** Big Intersection -- greatest lower bound of a set ***)
-goal Set.thy "!!B. B:A ==> Inter(A) <= B";
+Goal "B:A ==> Inter(A) <= B";
by (Blast_tac 1);
qed "Inter_lower";
-val [prem] = goal Set.thy
- "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
+val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
by (rtac (InterI RS subsetI) 1);
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
qed "Inter_greatest";
-val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)";
-by (rtac subsetI 1);
-by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1));
+Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
+by (Blast_tac 1);
qed "INT_lower";
-val [prem] = goal Set.thy
- "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
+val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
by (rtac (INT_I RS subsetI) 1);
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
qed "INT_greatest";
(*** Finite Union -- the least upper bound of 2 sets ***)
-goal Set.thy "A <= A Un B";
+Goal "A <= A Un B";
by (Blast_tac 1);
qed "Un_upper1";
-goal Set.thy "B <= A Un B";
+Goal "B <= A Un B";
by (Blast_tac 1);
qed "Un_upper2";
-goal Set.thy "!!C. [| A<=C; B<=C |] ==> A Un B <= C";
+Goal "[| A<=C; B<=C |] ==> A Un B <= C";
by (Blast_tac 1);
qed "Un_least";
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
-goal Set.thy "A Int B <= A";
+Goal "A Int B <= A";
by (Blast_tac 1);
qed "Int_lower1";
-goal Set.thy "A Int B <= B";
+Goal "A Int B <= B";
by (Blast_tac 1);
qed "Int_lower2";
-goal Set.thy "!!C. [| C<=A; C<=B |] ==> C <= A Int B";
+Goal "[| C<=A; C<=B |] ==> C <= A Int B";
by (Blast_tac 1);
qed "Int_greatest";
@@ -101,14 +94,14 @@
(*** Monotonicity ***)
-val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
+Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
by (rtac Un_least 1);
-by (rtac (Un_upper1 RS (prem RS monoD)) 1);
-by (rtac (Un_upper2 RS (prem RS monoD)) 1);
+by (etac (Un_upper1 RSN (2,monoD)) 1);
+by (etac (Un_upper2 RSN (2,monoD)) 1);
qed "mono_Un";
-val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
+Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
by (rtac Int_greatest 1);
-by (rtac (Int_lower1 RS (prem RS monoD)) 1);
-by (rtac (Int_lower2 RS (prem RS monoD)) 1);
+by (etac (Int_lower1 RSN (2,monoD)) 1);
+by (etac (Int_lower2 RSN (2,monoD)) 1);
qed "mono_Int";