1.1 --- a/src/HOL/Arith.ML Thu Aug 13 18:07:56 1998 +0200
1.2 +++ b/src/HOL/Arith.ML Thu Aug 13 18:14:26 1998 +0200
1.3 @@ -221,7 +221,7 @@
1.4 qed "add_less_mono";
1.5
1.6 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
1.7 -val [lt_mono,le] = goal thy
1.8 +val [lt_mono,le] = Goal
1.9 "[| !!i j::nat. i<j ==> f(i) < f(j); \
1.10 \ i <= j \
1.11 \ |] ==> f(i) <= (f(j)::nat)";
1.12 @@ -331,8 +331,8 @@
1.13
1.14 (*** More results about difference ***)
1.15
1.16 -val [prem] = goal thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
1.17 -by (rtac (prem RS rev_mp) 1);
1.18 +Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
1.19 +by (etac rev_mp 1);
1.20 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.21 by (ALLGOALS Asm_simp_tac);
1.22 qed "Suc_diff_n";
1.23 @@ -411,20 +411,20 @@
1.24 by (ALLGOALS Asm_simp_tac);
1.25 qed "le_imp_diff_is_add";
1.26
1.27 -val [prem] = goal thy "m < Suc(n) ==> m-n = 0";
1.28 -by (rtac (prem RS rev_mp) 1);
1.29 +Goal "m < Suc(n) ==> m-n = 0";
1.30 +by (etac rev_mp 1);
1.31 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.32 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
1.33 by (ALLGOALS Asm_simp_tac);
1.34 qed "less_imp_diff_is_0";
1.35
1.36 -val prems = goal thy "m-n = 0 --> n-m = 0 --> m=n";
1.37 +Goal "m-n = 0 --> n-m = 0 --> m=n";
1.38 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.39 by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
1.40 qed_spec_mp "diffs0_imp_equal";
1.41
1.42 -val [prem] = goal thy "m<n ==> 0<n-m";
1.43 -by (rtac (prem RS rev_mp) 1);
1.44 +Goal "m<n ==> 0<n-m";
1.45 +by (etac rev_mp 1);
1.46 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.47 by (ALLGOALS Asm_simp_tac);
1.48 qed "less_imp_diff_positive";
1.49 @@ -448,7 +448,7 @@
1.50 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
1.51 qed "zero_induct_lemma";
1.52
1.53 -val prems = goal thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
1.54 +val prems = Goal "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
1.55 by (rtac (diff_self_eq_0 RS subst) 1);
1.56 by (rtac (zero_induct_lemma RS mp RS mp) 1);
1.57 by (REPEAT (ares_tac ([impI,allI]@prems) 1));
2.1 --- a/src/HOL/Divides.ML Thu Aug 13 18:07:56 1998 +0200
2.2 +++ b/src/HOL/Divides.ML Thu Aug 13 18:14:26 1998 +0200
2.3 @@ -10,7 +10,7 @@
2.4 (** Less-then properties **)
2.5
2.6 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
2.7 -goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
2.8 +Goal "[| 0<n; ~ m<n |] ==> m - n < m";
2.9 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
2.10 by (Blast_tac 1);
2.11 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
2.12 @@ -200,9 +200,10 @@
2.13 by (trans_tac 2);
2.14 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
2.15 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
2.16 - by (best_tac (claset() addIs [le_trans]
2.17 - addss (simpset() addsimps [diff_less])) 1);
2.18 -by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
2.19 +by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
2.20 +br le_trans 1;
2.21 +by (Asm_simp_tac 1);
2.22 +by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
2.23 qed "div_le_mono2";
2.24
2.25 Goal "0<n ==> m div n <= m";
3.1 --- a/src/HOL/Finite.ML Thu Aug 13 18:07:56 1998 +0200
3.2 +++ b/src/HOL/Finite.ML Thu Aug 13 18:14:26 1998 +0200
3.3 @@ -11,7 +11,7 @@
3.4 section "finite";
3.5
3.6 (*Discharging ~ x:y entails extra work*)
3.7 -val major::prems = goal Finite.thy
3.8 +val major::prems = Goal
3.9 "[| finite F; P({}); \
3.10 \ !!F x. [| finite F; x ~: F; P(F) |] ==> P(insert x F) \
3.11 \ |] ==> P(F)";
3.12 @@ -21,7 +21,7 @@
3.13 by (REPEAT (ares_tac prems 1));
3.14 qed "finite_induct";
3.15
3.16 -val major::subs::prems = goal Finite.thy
3.17 +val major::subs::prems = Goal
3.18 "[| finite F; F <= A; \
3.19 \ P({}); \
3.20 \ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
3.21 @@ -35,10 +35,9 @@
3.22 AddSIs Finites.intrs;
3.23
3.24 (*The union of two finite sets is finite*)
3.25 -val major::prems = goal Finite.thy
3.26 - "[| finite F; finite G |] ==> finite(F Un G)";
3.27 -by (rtac (major RS finite_induct) 1);
3.28 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
3.29 +Goal "[| finite F; finite G |] ==> finite(F Un G)";
3.30 +by (etac finite_induct 1);
3.31 +by (ALLGOALS Asm_simp_tac);
3.32 qed "finite_UnI";
3.33
3.34 (*Every subset of a finite set is finite*)
3.35 @@ -76,7 +75,7 @@
3.36 by (Asm_simp_tac 1);
3.37 qed "finite_imageI";
3.38
3.39 -val major::prems = goal Finite.thy
3.40 +val major::prems = Goal
3.41 "[| finite c; finite b; \
3.42 \ P(b); \
3.43 \ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \
3.44 @@ -87,7 +86,7 @@
3.45 (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
3.46 val lemma = result();
3.47
3.48 -val prems = goal Finite.thy
3.49 +val prems = Goal
3.50 "[| finite A; \
3.51 \ P(A); \
3.52 \ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \
3.53 @@ -134,9 +133,8 @@
3.54
3.55 (** The finite UNION of finite sets **)
3.56
3.57 -val [prem] = goal Finite.thy
3.58 - "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
3.59 -by (rtac (prem RS finite_induct) 1);
3.60 +Goal "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
3.61 +by (etac finite_induct 1);
3.62 by (ALLGOALS Asm_simp_tac);
3.63 bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
3.64 Addsimps [finite_UnionI];
3.65 @@ -187,7 +185,7 @@
3.66
3.67 section "Finite cardinality -- 'card'";
3.68
3.69 -goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
3.70 +Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
3.71 by (Blast_tac 1);
3.72 val Collect_conv_insert = result();
3.73
3.74 @@ -197,9 +195,8 @@
3.75 qed "card_empty";
3.76 Addsimps [card_empty];
3.77
3.78 -val [major] = goal Finite.thy
3.79 - "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
3.80 -by (rtac (major RS finite_induct) 1);
3.81 +Goal "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
3.82 +by (etac finite_induct 1);
3.83 by (res_inst_tac [("x","0")] exI 1);
3.84 by (Simp_tac 1);
3.85 by (etac exE 1);
4.1 --- a/src/HOL/Fun.ML Thu Aug 13 18:07:56 1998 +0200
4.2 +++ b/src/HOL/Fun.ML Thu Aug 13 18:14:26 1998 +0200
4.3 @@ -13,7 +13,7 @@
4.4 by (rtac ext 1 THEN Asm_simp_tac 1);
4.5 qed "expand_fun_eq";
4.6
4.7 -val prems = goal thy
4.8 +val prems = Goal
4.9 "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)";
4.10 by (rtac (arg_cong RS box_equals) 1);
4.11 by (REPEAT (resolve_tac (prems@[refl]) 1));
4.12 @@ -22,11 +22,11 @@
4.13
4.14 (** "Axiom" of Choice, proved using the description operator **)
4.15
4.16 -goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
4.17 +Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
4.18 by (fast_tac (claset() addEs [selectI]) 1);
4.19 qed "choice";
4.20
4.21 -goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
4.22 +Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
4.23 by (fast_tac (claset() addEs [selectI]) 1);
4.24 qed "bchoice";
4.25
4.26 @@ -57,44 +57,43 @@
4.27
4.28 (*** inj(f): f is a one-to-one function ***)
4.29
4.30 -val prems = goalw thy [inj_def]
4.31 +val prems = Goalw [inj_def]
4.32 "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
4.33 by (blast_tac (claset() addIs prems) 1);
4.34 qed "injI";
4.35
4.36 -val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
4.37 +val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
4.38 by (rtac injI 1);
4.39 by (etac (arg_cong RS box_equals) 1);
4.40 by (rtac major 1);
4.41 by (rtac major 1);
4.42 qed "inj_inverseI";
4.43
4.44 -val [major,minor] = goalw thy [inj_def]
4.45 - "[| inj(f); f(x) = f(y) |] ==> x=y";
4.46 -by (rtac (major RS spec RS spec RS mp) 1);
4.47 -by (rtac minor 1);
4.48 +Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
4.49 +by (Blast_tac 1);
4.50 qed "injD";
4.51
4.52 (*Useful with the simplifier*)
4.53 -val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
4.54 +Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
4.55 by (rtac iffI 1);
4.56 -by (etac (major RS injD) 1);
4.57 -by (etac arg_cong 1);
4.58 +by (etac arg_cong 2);
4.59 +by (etac injD 1);
4.60 +ba 1;
4.61 qed "inj_eq";
4.62
4.63 -val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
4.64 -by (rtac (major RS injD) 1);
4.65 +Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
4.66 +by (etac injD 1);
4.67 by (rtac selectI 1);
4.68 by (rtac refl 1);
4.69 qed "inj_select";
4.70
4.71 (*A one-to-one function has an inverse (given using select).*)
4.72 -val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
4.73 -by (EVERY1 [rtac (major RS inj_select)]);
4.74 +Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
4.75 +by (etac inj_select 1);
4.76 qed "inv_f_f";
4.77
4.78 (* Useful??? *)
4.79 -val [oneone,minor] = goal thy
4.80 +val [oneone,minor] = Goal
4.81 "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
4.82 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
4.83 by (rtac (rangeI RS minor) 1);
4.84 @@ -103,60 +102,52 @@
4.85
4.86 (*** inj_on f A: f is one-to-one over A ***)
4.87
4.88 -val prems = goalw thy [inj_on_def]
4.89 +val prems = Goalw [inj_on_def]
4.90 "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A";
4.91 by (blast_tac (claset() addIs prems) 1);
4.92 qed "inj_onI";
4.93
4.94 -val [major] = goal thy
4.95 +val [major] = Goal
4.96 "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
4.97 by (rtac inj_onI 1);
4.98 by (etac (apply_inverse RS trans) 1);
4.99 by (REPEAT (eresolve_tac [asm_rl,major] 1));
4.100 qed "inj_on_inverseI";
4.101
4.102 -val major::prems = goalw thy [inj_on_def]
4.103 - "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y";
4.104 -by (rtac (major RS bspec RS bspec RS mp) 1);
4.105 -by (REPEAT (resolve_tac prems 1));
4.106 +Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y";
4.107 +by (Blast_tac 1);
4.108 qed "inj_onD";
4.109
4.110 Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
4.111 by (blast_tac (claset() addSDs [inj_onD]) 1);
4.112 qed "inj_on_iff";
4.113
4.114 -val major::prems = goal thy
4.115 - "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
4.116 -by (rtac contrapos 1);
4.117 -by (etac (major RS inj_onD) 2);
4.118 -by (REPEAT (resolve_tac prems 1));
4.119 +Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
4.120 +by (Blast_tac 1);
4.121 qed "inj_on_contraD";
4.122
4.123 -Goalw [inj_on_def]
4.124 - "[| A<=B; inj_on f B |] ==> inj_on f A";
4.125 +Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
4.126 by (Blast_tac 1);
4.127 qed "subset_inj_on";
4.128
4.129
4.130 (*** Lemmas about inj ***)
4.131
4.132 -Goalw [o_def]
4.133 - "[| inj(f); inj_on g (range f) |] ==> inj(g o f)";
4.134 +Goalw [o_def] "[| inj(f); inj_on g (range f) |] ==> inj(g o f)";
4.135 by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
4.136 qed "comp_inj";
4.137
4.138 -val [prem] = goal thy "inj(f) ==> inj_on f A";
4.139 -by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
4.140 +Goal "inj(f) ==> inj_on f A";
4.141 +by (blast_tac (claset() addIs [injD, inj_onI]) 1);
4.142 qed "inj_imp";
4.143
4.144 -val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
4.145 -by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
4.146 +Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
4.147 +by (fast_tac (claset() addIs [selectI]) 1);
4.148 qed "f_inv_f";
4.149
4.150 -val prems = goal thy
4.151 - "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y";
4.152 +Goal "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y";
4.153 by (rtac (arg_cong RS box_equals) 1);
4.154 -by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
4.155 +by (REPEAT (ares_tac [f_inv_f] 1));
4.156 qed "inv_injective";
4.157
4.158 Goal "[| inj(f); A<=range(f) |] ==> inj_on (inv f) A";
5.1 --- a/src/HOL/Gfp.ML Thu Aug 13 18:07:56 1998 +0200
5.2 +++ b/src/HOL/Gfp.ML Thu Aug 13 18:14:26 1998 +0200
5.3 @@ -22,18 +22,18 @@
5.4 by (etac CollectD 1);
5.5 qed "gfp_least";
5.6
5.7 -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
5.8 +Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
5.9 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
5.10 - rtac (mono RS monoD), rtac gfp_upperbound, atac]);
5.11 + etac monoD, rtac gfp_upperbound, atac]);
5.12 qed "gfp_lemma2";
5.13
5.14 -val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
5.15 -by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD),
5.16 - rtac gfp_lemma2, rtac mono]);
5.17 +Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
5.18 +by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
5.19 + etac gfp_lemma2]);
5.20 qed "gfp_lemma3";
5.21
5.22 -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
5.23 -by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
5.24 +Goal "mono(f) ==> gfp(f) = f(gfp(f))";
5.25 +by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
5.26 qed "gfp_Tarski";
5.27
5.28 (*** Coinduction rules for greatest fixed points ***)
5.29 @@ -70,8 +70,8 @@
5.30 - instead of the condition X <= f(X)
5.31 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
5.32
5.33 -val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)";
5.34 -by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
5.35 +Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
5.36 +by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
5.37 qed "coinduct3_mono_lemma";
5.38
5.39 val [prem,mono] = goal Gfp.thy
5.40 @@ -88,12 +88,11 @@
5.41 by (rtac Un_upper2 1);
5.42 qed "coinduct3_lemma";
5.43
5.44 -val prems = goal Gfp.thy
5.45 - "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
5.46 +Goal
5.47 + "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
5.48 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
5.49 -by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
5.50 -by (rtac (UnI2 RS UnI1) 1);
5.51 -by (REPEAT (resolve_tac prems 1));
5.52 +by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1);
5.53 +by Auto_tac;
5.54 qed "coinduct3";
5.55
5.56
5.57 @@ -111,7 +110,7 @@
5.58 qed "def_coinduct";
5.59
5.60 (*The version used in the induction/coinduction package*)
5.61 -val prems = goal Gfp.thy
5.62 +val prems = Goal
5.63 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \
5.64 \ a: X; !!z. z: X ==> P (X Un A) z |] ==> \
5.65 \ a : A";
5.66 @@ -126,7 +125,7 @@
5.67 qed "def_coinduct3";
5.68
5.69 (*Monotonicity of gfp!*)
5.70 -val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
5.71 +val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
5.72 by (rtac (gfp_upperbound RS gfp_least) 1);
5.73 by (etac (prem RSN (2,subset_trans)) 1);
5.74 qed "gfp_mono";
6.1 --- a/src/HOL/Integ/Integ.ML Thu Aug 13 18:07:56 1998 +0200
6.2 +++ b/src/HOL/Integ/Integ.ML Thu Aug 13 18:14:26 1998 +0200
6.3 @@ -32,10 +32,8 @@
6.4
6.5 (** Natural deduction for intrel **)
6.6
6.7 -val prems = goalw Integ.thy [intrel_def]
6.8 - "[| x1+y2 = x2+y1|] ==> \
6.9 -\ ((x1,y1),(x2,y2)): intrel";
6.10 -by (fast_tac (claset() addIs prems) 1);
6.11 +Goalw [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
6.12 +by (Fast_tac 1);
6.13 qed "intrelI";
6.14
6.15 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
6.16 @@ -45,7 +43,7 @@
6.17 by (Fast_tac 1);
6.18 qed "intrelE_lemma";
6.19
6.20 -val [major,minor] = goal Integ.thy
6.21 +val [major,minor] = Goal
6.22 "[| p: intrel; \
6.23 \ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \
6.24 \ ==> Q";
6.25 @@ -130,8 +128,7 @@
6.26 qed "zminus";
6.27
6.28 (*by lcp*)
6.29 -val [prem] = goal Integ.thy
6.30 - "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
6.31 +val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
6.32 by (res_inst_tac [("x1","z")]
6.33 (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
6.34 by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
6.35 @@ -159,8 +156,7 @@
6.36 (**** znegative: the test for negative integers ****)
6.37
6.38
6.39 -Goalw [znegative_def, znat_def]
6.40 - "~ znegative($# n)";
6.41 +Goalw [znegative_def, znat_def] "~ znegative($# n)";
6.42 by (Simp_tac 1);
6.43 by Safe_tac;
6.44 qed "not_znegative_znat";
6.45 @@ -445,13 +441,11 @@
6.46 by (Simp_tac 1);
6.47 qed "zminus_zpred";
6.48
6.49 -Goalw [zsuc_def,zpred_def,zdiff_def]
6.50 - "zpred(zsuc(z)) = z";
6.51 +Goalw [zsuc_def,zpred_def,zdiff_def] "zpred(zsuc(z)) = z";
6.52 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
6.53 qed "zpred_zsuc";
6.54
6.55 -Goalw [zsuc_def,zpred_def,zdiff_def]
6.56 - "zsuc(zpred(z)) = z";
6.57 +Goalw [zsuc_def,zpred_def,zdiff_def] "zsuc(zpred(z)) = z";
6.58 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
6.59 qed "zsuc_zpred";
6.60
6.61 @@ -473,13 +467,13 @@
6.62 by (rtac zminus_zminus 1);
6.63 qed "zminus_exchange";
6.64
6.65 -Goal"(zsuc(z)=zsuc(w)) = (z=w)";
6.66 +Goal "(zsuc(z)=zsuc(w)) = (z=w)";
6.67 by Safe_tac;
6.68 by (dres_inst_tac [("f","zpred")] arg_cong 1);
6.69 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
6.70 qed "bijective_zsuc";
6.71
6.72 -Goal"(zpred(z)=zpred(w)) = (z=w)";
6.73 +Goal "(zpred(z)=zpred(w)) = (z=w)";
6.74 by Safe_tac;
6.75 by (dres_inst_tac [("f","zsuc")] arg_cong 1);
6.76 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
6.77 @@ -579,7 +573,7 @@
6.78
6.79 val zless_zsucI = zlessI RSN (2,zless_trans);
6.80
6.81 -Goal "!!z w::int. z<w ==> ~w<z";
6.82 +Goal "!!w::int. z<w ==> ~w<z";
6.83 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
6.84 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
6.85 by Safe_tac;
6.86 @@ -611,7 +605,7 @@
6.87 by (asm_full_simp_tac
6.88 (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
6.89 by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
6.90 -by (REPEAT (fast_tac (claset() addss (simpset() addsimps add_ac)) 1));
6.91 +by (auto_tac (claset(), simpset() addsimps add_ac));
6.92 qed "zless_linear";
6.93
6.94
6.95 @@ -664,14 +658,15 @@
6.96 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
6.97 qed "zle_refl";
6.98
6.99 -val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
6.100 +Goal "[| i <= j; j < k |] ==> i < (k::int)";
6.101 by (dtac zle_imp_zless_or_eq 1);
6.102 by (fast_tac (claset() addIs [zless_trans]) 1);
6.103 qed "zle_zless_trans";
6.104
6.105 Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
6.106 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
6.107 - rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
6.108 + rtac zless_or_eq_imp_zle,
6.109 + fast_tac (claset() addIs [zless_trans])]);
6.110 qed "zle_trans";
6.111
6.112 Goal "[| z <= w; w <= z |] ==> z = (w::int)";
6.113 @@ -680,7 +675,7 @@
6.114 qed "zle_anti_sym";
6.115
6.116
6.117 -Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
6.118 +Goal "!!w::int. z + w' = z + w ==> w' = w";
6.119 by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
6.120 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
6.121 qed "zadd_left_cancel";
6.122 @@ -688,19 +683,19 @@
6.123
6.124 (*** Monotonicity results ***)
6.125
6.126 -Goal "!!v w z::int. v < w ==> v + z < w + z";
6.127 +Goal "!!z::int. v < w ==> v + z < w + z";
6.128 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
6.129 by (simp_tac (simpset() addsimps zadd_ac) 1);
6.130 by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
6.131 qed "zadd_zless_mono1";
6.132
6.133 -Goal "!!v w z::int. (v+z < w+z) = (v < w)";
6.134 +Goal "!!z::int. (v+z < w+z) = (v < w)";
6.135 by (safe_tac (claset() addSEs [zadd_zless_mono1]));
6.136 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
6.137 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
6.138 qed "zadd_left_cancel_zless";
6.139
6.140 -Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
6.141 +Goal "!!z::int. (v+z <= w+z) = (v <= w)";
6.142 by (asm_full_simp_tac
6.143 (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
6.144 qed "zadd_left_cancel_zle";
6.145 @@ -709,14 +704,14 @@
6.146 bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
6.147
6.148
6.149 -Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
6.150 +Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
6.151 by (etac (zadd_zle_mono1 RS zle_trans) 1);
6.152 by (simp_tac (simpset() addsimps [zadd_commute]) 1);
6.153 (*w moves to the end because it is free while z', z are bound*)
6.154 by (etac zadd_zle_mono1 1);
6.155 qed "zadd_zle_mono";
6.156
6.157 -Goal "!!w z::int. z<=$#0 ==> w+z <= w";
6.158 +Goal "!!z::int. z<=$#0 ==> w+z <= w";
6.159 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
6.160 by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
6.161 qed "zadd_zle_self";
6.162 @@ -726,7 +721,7 @@
6.163
6.164 (** One auxiliary theorem...**)
6.165
6.166 -goal HOL.thy "(x = False) = (~ x)";
6.167 +Goal "(x = False) = (~ x)";
6.168 by (fast_tac HOL_cs 1);
6.169 qed "eq_False_conv";
6.170
6.171 @@ -848,8 +843,7 @@
6.172
6.173 (* a case theorem distinguishing positive and negative int *)
6.174
6.175 -val prems = goal Integ.thy
6.176 - "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z";
6.177 +val prems = Goal "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z";
6.178 by (cut_inst_tac [("P","znegative z")] excluded_middle 1);
6.179 by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1);
6.180 qed "int_cases";
7.1 --- a/src/HOL/Lfp.ML Thu Aug 13 18:07:56 1998 +0200
7.2 +++ b/src/HOL/Lfp.ML Thu Aug 13 18:14:26 1998 +0200
7.3 @@ -3,7 +3,7 @@
7.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.5 Copyright 1992 University of Cambridge
7.6
7.7 -For lfp.thy. The Knaster-Tarski Theorem
7.8 +The Knaster-Tarski Theorem
7.9 *)
7.10
7.11 open Lfp;
7.12 @@ -12,34 +12,34 @@
7.13
7.14 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
7.15
7.16 -val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
7.17 +Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
7.18 by (rtac (CollectI RS Inter_lower) 1);
7.19 -by (resolve_tac prems 1);
7.20 +by (assume_tac 1);
7.21 qed "lfp_lowerbound";
7.22
7.23 -val prems = goalw Lfp.thy [lfp_def]
7.24 +val prems = Goalw [lfp_def]
7.25 "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
7.26 by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
7.27 by (etac CollectD 1);
7.28 qed "lfp_greatest";
7.29
7.30 -val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
7.31 +Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
7.32 by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
7.33 - rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
7.34 + etac monoD, rtac lfp_lowerbound, atac, atac]);
7.35 qed "lfp_lemma2";
7.36
7.37 -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
7.38 -by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD),
7.39 - rtac lfp_lemma2, rtac mono]);
7.40 +Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
7.41 +by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
7.42 + etac lfp_lemma2]);
7.43 qed "lfp_lemma3";
7.44
7.45 -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
7.46 -by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
7.47 +Goal "mono(f) ==> lfp(f) = f(lfp(f))";
7.48 +by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
7.49 qed "lfp_Tarski";
7.50
7.51 (*** General induction rule for least fixed points ***)
7.52
7.53 -val [lfp,mono,indhyp] = goal Lfp.thy
7.54 +val [lfp,mono,indhyp] = Goal
7.55 "[| a: lfp(f); mono(f); \
7.56 \ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \
7.57 \ |] ==> P(a)";
7.58 @@ -62,7 +62,7 @@
7.59 by (rtac (mono RS lfp_Tarski) 1);
7.60 qed "def_lfp_Tarski";
7.61
7.62 -val rew::prems = goal Lfp.thy
7.63 +val rew::prems = Goal
7.64 "[| A == lfp(f); mono(f); a:A; \
7.65 \ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \
7.66 \ |] ==> P(a)";
7.67 @@ -71,7 +71,7 @@
7.68 qed "def_induct";
7.69
7.70 (*Monotonicity of lfp!*)
7.71 -val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
7.72 +val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
7.73 by (rtac (lfp_lowerbound RS lfp_greatest) 1);
7.74 by (etac (prem RS subset_trans) 1);
7.75 qed "lfp_mono";
8.1 --- a/src/HOL/List.ML Thu Aug 13 18:07:56 1998 +0200
8.2 +++ b/src/HOL/List.ML Thu Aug 13 18:14:26 1998 +0200
8.3 @@ -8,14 +8,14 @@
8.4
8.5 Goal "!x. xs ~= x#xs";
8.6 by (induct_tac "xs" 1);
8.7 -by (Auto_tac);
8.8 +by Auto_tac;
8.9 qed_spec_mp "not_Cons_self";
8.10 bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
8.11 Addsimps [not_Cons_self,not_Cons_self2];
8.12
8.13 Goal "(xs ~= []) = (? y ys. xs = y#ys)";
8.14 by (induct_tac "xs" 1);
8.15 -by (Auto_tac);
8.16 +by Auto_tac;
8.17 qed "neq_Nil_conv";
8.18
8.19 (* Induction over the length of a list: *)
8.20 @@ -71,43 +71,43 @@
8.21
8.22 Goal "length(xs@ys) = length(xs)+length(ys)";
8.23 by (induct_tac "xs" 1);
8.24 -by (Auto_tac);
8.25 +by Auto_tac;
8.26 qed"length_append";
8.27 Addsimps [length_append];
8.28
8.29 Goal "length (map f xs) = length xs";
8.30 by (induct_tac "xs" 1);
8.31 -by (Auto_tac);
8.32 +by Auto_tac;
8.33 qed "length_map";
8.34 Addsimps [length_map];
8.35
8.36 Goal "length(rev xs) = length(xs)";
8.37 by (induct_tac "xs" 1);
8.38 -by (Auto_tac);
8.39 +by Auto_tac;
8.40 qed "length_rev";
8.41 Addsimps [length_rev];
8.42
8.43 Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
8.44 by (exhaust_tac "xs" 1);
8.45 -by (Auto_tac);
8.46 +by Auto_tac;
8.47 qed "length_tl";
8.48 Addsimps [length_tl];
8.49
8.50 Goal "(length xs = 0) = (xs = [])";
8.51 by (induct_tac "xs" 1);
8.52 -by (Auto_tac);
8.53 +by Auto_tac;
8.54 qed "length_0_conv";
8.55 AddIffs [length_0_conv];
8.56
8.57 Goal "(0 = length xs) = (xs = [])";
8.58 by (induct_tac "xs" 1);
8.59 -by (Auto_tac);
8.60 +by Auto_tac;
8.61 qed "zero_length_conv";
8.62 AddIffs [zero_length_conv];
8.63
8.64 Goal "(0 < length xs) = (xs ~= [])";
8.65 by (induct_tac "xs" 1);
8.66 -by (Auto_tac);
8.67 +by Auto_tac;
8.68 qed "length_greater_0_conv";
8.69 AddIffs [length_greater_0_conv];
8.70
8.71 @@ -123,36 +123,36 @@
8.72
8.73 Goal "(xs@ys)@zs = xs@(ys@zs)";
8.74 by (induct_tac "xs" 1);
8.75 -by (Auto_tac);
8.76 +by Auto_tac;
8.77 qed "append_assoc";
8.78 Addsimps [append_assoc];
8.79
8.80 Goal "xs @ [] = xs";
8.81 by (induct_tac "xs" 1);
8.82 -by (Auto_tac);
8.83 +by Auto_tac;
8.84 qed "append_Nil2";
8.85 Addsimps [append_Nil2];
8.86
8.87 Goal "(xs@ys = []) = (xs=[] & ys=[])";
8.88 by (induct_tac "xs" 1);
8.89 -by (Auto_tac);
8.90 +by Auto_tac;
8.91 qed "append_is_Nil_conv";
8.92 AddIffs [append_is_Nil_conv];
8.93
8.94 Goal "([] = xs@ys) = (xs=[] & ys=[])";
8.95 by (induct_tac "xs" 1);
8.96 -by (Auto_tac);
8.97 +by Auto_tac;
8.98 qed "Nil_is_append_conv";
8.99 AddIffs [Nil_is_append_conv];
8.100
8.101 Goal "(xs @ ys = xs) = (ys=[])";
8.102 by (induct_tac "xs" 1);
8.103 -by (Auto_tac);
8.104 +by Auto_tac;
8.105 qed "append_self_conv";
8.106
8.107 Goal "(xs = xs @ ys) = (ys=[])";
8.108 by (induct_tac "xs" 1);
8.109 -by (Auto_tac);
8.110 +by Auto_tac;
8.111 qed "self_append_conv";
8.112 AddIffs [append_self_conv,self_append_conv];
8.113
8.114 @@ -192,7 +192,7 @@
8.115
8.116 Goal "(xs @ ys = ys) = (xs=[])";
8.117 by (cut_inst_tac [("zs","[]")] append_same_eq 1);
8.118 -by (Auto_tac);
8.119 +by Auto_tac;
8.120 qed "append_self_conv2";
8.121
8.122 Goal "(ys = xs @ ys) = (xs=[])";
8.123 @@ -204,13 +204,13 @@
8.124
8.125 Goal "xs ~= [] --> hd xs # tl xs = xs";
8.126 by (induct_tac "xs" 1);
8.127 -by (Auto_tac);
8.128 +by Auto_tac;
8.129 qed_spec_mp "hd_Cons_tl";
8.130 Addsimps [hd_Cons_tl];
8.131
8.132 Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
8.133 by (induct_tac "xs" 1);
8.134 -by (Auto_tac);
8.135 +by Auto_tac;
8.136 qed "hd_append";
8.137
8.138 Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
8.139 @@ -252,31 +252,31 @@
8.140
8.141 Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
8.142 by (induct_tac "xs" 1);
8.143 -by (Auto_tac);
8.144 +by Auto_tac;
8.145 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
8.146
8.147 Goal "map (%x. x) = (%xs. xs)";
8.148 by (rtac ext 1);
8.149 by (induct_tac "xs" 1);
8.150 -by (Auto_tac);
8.151 +by Auto_tac;
8.152 qed "map_ident";
8.153 Addsimps[map_ident];
8.154
8.155 Goal "map f (xs@ys) = map f xs @ map f ys";
8.156 by (induct_tac "xs" 1);
8.157 -by (Auto_tac);
8.158 +by Auto_tac;
8.159 qed "map_append";
8.160 Addsimps[map_append];
8.161
8.162 Goalw [o_def] "map (f o g) xs = map f (map g xs)";
8.163 by (induct_tac "xs" 1);
8.164 -by (Auto_tac);
8.165 +by Auto_tac;
8.166 qed "map_compose";
8.167 Addsimps[map_compose];
8.168
8.169 Goal "rev(map f xs) = map f (rev xs)";
8.170 by (induct_tac "xs" 1);
8.171 -by (Auto_tac);
8.172 +by Auto_tac;
8.173 qed "rev_map";
8.174
8.175 (* a congruence rule for map: *)
8.176 @@ -284,19 +284,19 @@
8.177 by (rtac impI 1);
8.178 by (hyp_subst_tac 1);
8.179 by (induct_tac "ys" 1);
8.180 -by (Auto_tac);
8.181 +by Auto_tac;
8.182 val lemma = result();
8.183 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
8.184
8.185 Goal "(map f xs = []) = (xs = [])";
8.186 by (induct_tac "xs" 1);
8.187 -by (Auto_tac);
8.188 +by Auto_tac;
8.189 qed "map_is_Nil_conv";
8.190 AddIffs [map_is_Nil_conv];
8.191
8.192 Goal "([] = map f xs) = (xs = [])";
8.193 by (induct_tac "xs" 1);
8.194 -by (Auto_tac);
8.195 +by Auto_tac;
8.196 qed "Nil_is_map_conv";
8.197 AddIffs [Nil_is_map_conv];
8.198
8.199 @@ -307,25 +307,25 @@
8.200
8.201 Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
8.202 by (induct_tac "xs" 1);
8.203 -by (Auto_tac);
8.204 +by Auto_tac;
8.205 qed "rev_append";
8.206 Addsimps[rev_append];
8.207
8.208 Goal "rev(rev l) = l";
8.209 by (induct_tac "l" 1);
8.210 -by (Auto_tac);
8.211 +by Auto_tac;
8.212 qed "rev_rev_ident";
8.213 Addsimps[rev_rev_ident];
8.214
8.215 Goal "(rev xs = []) = (xs = [])";
8.216 by (induct_tac "xs" 1);
8.217 -by (Auto_tac);
8.218 +by Auto_tac;
8.219 qed "rev_is_Nil_conv";
8.220 AddIffs [rev_is_Nil_conv];
8.221
8.222 Goal "([] = rev xs) = (xs = [])";
8.223 by (induct_tac "xs" 1);
8.224 -by (Auto_tac);
8.225 +by Auto_tac;
8.226 qed "Nil_is_rev_conv";
8.227 AddIffs [Nil_is_rev_conv];
8.228
8.229 @@ -341,7 +341,7 @@
8.230
8.231 Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";
8.232 by (res_inst_tac [("xs","xs")] rev_induct 1);
8.233 -by (Auto_tac);
8.234 +by Auto_tac;
8.235 bind_thm ("rev_exhaust",
8.236 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
8.237
8.238 @@ -352,13 +352,13 @@
8.239
8.240 Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
8.241 by (induct_tac "xs" 1);
8.242 -by (Auto_tac);
8.243 +by Auto_tac;
8.244 qed "mem_append";
8.245 Addsimps[mem_append];
8.246
8.247 Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
8.248 by (induct_tac "xs" 1);
8.249 -by (Auto_tac);
8.250 +by Auto_tac;
8.251 qed "mem_filter";
8.252 Addsimps[mem_filter];
8.253
8.254 @@ -373,40 +373,40 @@
8.255
8.256 Goal "set (xs@ys) = (set xs Un set ys)";
8.257 by (induct_tac "xs" 1);
8.258 -by (Auto_tac);
8.259 +by Auto_tac;
8.260 qed "set_append";
8.261 Addsimps[set_append];
8.262
8.263 Goal "(x mem xs) = (x: set xs)";
8.264 by (induct_tac "xs" 1);
8.265 -by (Auto_tac);
8.266 +by Auto_tac;
8.267 qed "set_mem_eq";
8.268
8.269 Goal "set l <= set (x#l)";
8.270 -by (Auto_tac);
8.271 +by Auto_tac;
8.272 qed "set_subset_Cons";
8.273
8.274 Goal "(set xs = {}) = (xs = [])";
8.275 by (induct_tac "xs" 1);
8.276 -by (Auto_tac);
8.277 +by Auto_tac;
8.278 qed "set_empty";
8.279 Addsimps [set_empty];
8.280
8.281 Goal "set(rev xs) = set(xs)";
8.282 by (induct_tac "xs" 1);
8.283 -by (Auto_tac);
8.284 +by Auto_tac;
8.285 qed "set_rev";
8.286 Addsimps [set_rev];
8.287
8.288 Goal "set(map f xs) = f``(set xs)";
8.289 by (induct_tac "xs" 1);
8.290 -by (Auto_tac);
8.291 +by Auto_tac;
8.292 qed "set_map";
8.293 Addsimps [set_map];
8.294
8.295 Goal "(x : set(filter P xs)) = (x : set xs & P x)";
8.296 by (induct_tac "xs" 1);
8.297 -by (Auto_tac);
8.298 +by Auto_tac;
8.299 qed "in_set_filter";
8.300 Addsimps [in_set_filter];
8.301
8.302 @@ -418,14 +418,14 @@
8.303 by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
8.304 by(REPEAT(etac exE 1));
8.305 by(exhaust_tac "ys" 1);
8.306 -by(Auto_tac);
8.307 +by Auto_tac;
8.308 qed "in_set_conv_decomp";
8.309
8.310 (* eliminate `lists' in favour of `set' *)
8.311
8.312 Goal "(xs : lists A) = (!x : set xs. x : A)";
8.313 by(induct_tac "xs" 1);
8.314 -by(Auto_tac);
8.315 +by Auto_tac;
8.316 qed "in_lists_conv_set";
8.317
8.318 bind_thm("in_listsD",in_lists_conv_set RS iffD1);
8.319 @@ -439,19 +439,19 @@
8.320
8.321 Goal "list_all (%x. True) xs = True";
8.322 by (induct_tac "xs" 1);
8.323 -by (Auto_tac);
8.324 +by Auto_tac;
8.325 qed "list_all_True";
8.326 Addsimps [list_all_True];
8.327
8.328 Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
8.329 by (induct_tac "xs" 1);
8.330 -by (Auto_tac);
8.331 +by Auto_tac;
8.332 qed "list_all_append";
8.333 Addsimps [list_all_append];
8.334
8.335 Goal "list_all P xs = (!x. x mem xs --> P(x))";
8.336 by (induct_tac "xs" 1);
8.337 -by (Auto_tac);
8.338 +by Auto_tac;
8.339 qed "list_all_mem_conv";
8.340
8.341
8.342 @@ -461,25 +461,25 @@
8.343
8.344 Goal "filter P (xs@ys) = filter P xs @ filter P ys";
8.345 by (induct_tac "xs" 1);
8.346 -by (Auto_tac);
8.347 +by Auto_tac;
8.348 qed "filter_append";
8.349 Addsimps [filter_append];
8.350
8.351 Goal "filter (%x. True) xs = xs";
8.352 by (induct_tac "xs" 1);
8.353 -by (Auto_tac);
8.354 +by Auto_tac;
8.355 qed "filter_True";
8.356 Addsimps [filter_True];
8.357
8.358 Goal "filter (%x. False) xs = []";
8.359 by (induct_tac "xs" 1);
8.360 -by (Auto_tac);
8.361 +by Auto_tac;
8.362 qed "filter_False";
8.363 Addsimps [filter_False];
8.364
8.365 Goal "length (filter P xs) <= length xs";
8.366 by (induct_tac "xs" 1);
8.367 -by (Auto_tac);
8.368 +by Auto_tac;
8.369 qed "length_filter";
8.370
8.371
8.372 @@ -489,41 +489,41 @@
8.373
8.374 Goal "concat(xs@ys) = concat(xs)@concat(ys)";
8.375 by (induct_tac "xs" 1);
8.376 -by (Auto_tac);
8.377 +by Auto_tac;
8.378 qed"concat_append";
8.379 Addsimps [concat_append];
8.380
8.381 Goal "(concat xss = []) = (!xs:set xss. xs=[])";
8.382 by (induct_tac "xss" 1);
8.383 -by (Auto_tac);
8.384 +by Auto_tac;
8.385 qed "concat_eq_Nil_conv";
8.386 AddIffs [concat_eq_Nil_conv];
8.387
8.388 Goal "([] = concat xss) = (!xs:set xss. xs=[])";
8.389 by (induct_tac "xss" 1);
8.390 -by (Auto_tac);
8.391 +by Auto_tac;
8.392 qed "Nil_eq_concat_conv";
8.393 AddIffs [Nil_eq_concat_conv];
8.394
8.395 Goal "set(concat xs) = Union(set `` set xs)";
8.396 by (induct_tac "xs" 1);
8.397 -by (Auto_tac);
8.398 +by Auto_tac;
8.399 qed"set_concat";
8.400 Addsimps [set_concat];
8.401
8.402 Goal "map f (concat xs) = concat (map (map f) xs)";
8.403 by (induct_tac "xs" 1);
8.404 -by (Auto_tac);
8.405 +by Auto_tac;
8.406 qed "map_concat";
8.407
8.408 Goal "filter p (concat xs) = concat (map (filter p) xs)";
8.409 by (induct_tac "xs" 1);
8.410 -by (Auto_tac);
8.411 +by Auto_tac;
8.412 qed"filter_concat";
8.413
8.414 Goal "rev(concat xs) = concat (map rev (rev xs))";
8.415 by (induct_tac "xs" 1);
8.416 -by (Auto_tac);
8.417 +by Auto_tac;
8.418 qed "rev_concat";
8.419
8.420 (** nth **)
8.421 @@ -535,7 +535,7 @@
8.422 by (Asm_simp_tac 1);
8.423 by (rtac allI 1);
8.424 by (exhaust_tac "xs" 1);
8.425 - by (Auto_tac);
8.426 + by Auto_tac;
8.427 qed_spec_mp "nth_append";
8.428
8.429 Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
8.430 @@ -545,7 +545,7 @@
8.431 (* case x#xl *)
8.432 by (rtac allI 1);
8.433 by (induct_tac "n" 1);
8.434 -by (Auto_tac);
8.435 +by Auto_tac;
8.436 qed_spec_mp "nth_map";
8.437 Addsimps [nth_map];
8.438
8.439 @@ -556,7 +556,7 @@
8.440 (* case x#xl *)
8.441 by (rtac allI 1);
8.442 by (induct_tac "n" 1);
8.443 -by (Auto_tac);
8.444 +by Auto_tac;
8.445 qed_spec_mp "list_all_nth";
8.446
8.447 Goal "!n. n < length xs --> xs!n mem xs";
8.448 @@ -589,30 +589,30 @@
8.449
8.450 Goal "last(xs@[x]) = x";
8.451 by (induct_tac "xs" 1);
8.452 -by (Auto_tac);
8.453 +by Auto_tac;
8.454 qed "last_snoc";
8.455 Addsimps [last_snoc];
8.456
8.457 Goal "butlast(xs@[x]) = xs";
8.458 by (induct_tac "xs" 1);
8.459 -by (Auto_tac);
8.460 +by Auto_tac;
8.461 qed "butlast_snoc";
8.462 Addsimps [butlast_snoc];
8.463
8.464 Goal "length(butlast xs) = length xs - 1";
8.465 by (res_inst_tac [("xs","xs")] rev_induct 1);
8.466 -by (Auto_tac);
8.467 +by Auto_tac;
8.468 qed "length_butlast";
8.469 Addsimps [length_butlast];
8.470
8.471 Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
8.472 by (induct_tac "xs" 1);
8.473 -by (Auto_tac);
8.474 +by Auto_tac;
8.475 qed_spec_mp "butlast_append";
8.476
8.477 Goal "x:set(butlast xs) --> x:set xs";
8.478 by (induct_tac "xs" 1);
8.479 -by (Auto_tac);
8.480 +by Auto_tac;
8.481 qed_spec_mp "in_set_butlastD";
8.482
8.483 Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
8.484 @@ -631,12 +631,12 @@
8.485
8.486 Goal "take 0 xs = []";
8.487 by (induct_tac "xs" 1);
8.488 -by (Auto_tac);
8.489 +by Auto_tac;
8.490 qed "take_0";
8.491
8.492 Goal "drop 0 xs = xs";
8.493 by (induct_tac "xs" 1);
8.494 -by (Auto_tac);
8.495 +by Auto_tac;
8.496 qed "drop_0";
8.497
8.498 Goal "take (Suc n) (x#xs) = x # take n xs";
8.499 @@ -652,102 +652,102 @@
8.500
8.501 Goal "!xs. length(take n xs) = min (length xs) n";
8.502 by (induct_tac "n" 1);
8.503 - by (Auto_tac);
8.504 + by Auto_tac;
8.505 by (exhaust_tac "xs" 1);
8.506 - by (Auto_tac);
8.507 + by Auto_tac;
8.508 qed_spec_mp "length_take";
8.509 Addsimps [length_take];
8.510
8.511 Goal "!xs. length(drop n xs) = (length xs - n)";
8.512 by (induct_tac "n" 1);
8.513 - by (Auto_tac);
8.514 + by Auto_tac;
8.515 by (exhaust_tac "xs" 1);
8.516 - by (Auto_tac);
8.517 + by Auto_tac;
8.518 qed_spec_mp "length_drop";
8.519 Addsimps [length_drop];
8.520
8.521 Goal "!xs. length xs <= n --> take n xs = xs";
8.522 by (induct_tac "n" 1);
8.523 - by (Auto_tac);
8.524 + by Auto_tac;
8.525 by (exhaust_tac "xs" 1);
8.526 - by (Auto_tac);
8.527 + by Auto_tac;
8.528 qed_spec_mp "take_all";
8.529
8.530 Goal "!xs. length xs <= n --> drop n xs = []";
8.531 by (induct_tac "n" 1);
8.532 - by (Auto_tac);
8.533 + by Auto_tac;
8.534 by (exhaust_tac "xs" 1);
8.535 - by (Auto_tac);
8.536 + by Auto_tac;
8.537 qed_spec_mp "drop_all";
8.538
8.539 Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
8.540 by (induct_tac "n" 1);
8.541 - by (Auto_tac);
8.542 + by Auto_tac;
8.543 by (exhaust_tac "xs" 1);
8.544 - by (Auto_tac);
8.545 + by Auto_tac;
8.546 qed_spec_mp "take_append";
8.547 Addsimps [take_append];
8.548
8.549 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
8.550 by (induct_tac "n" 1);
8.551 - by (Auto_tac);
8.552 + by Auto_tac;
8.553 by (exhaust_tac "xs" 1);
8.554 - by (Auto_tac);
8.555 + by Auto_tac;
8.556 qed_spec_mp "drop_append";
8.557 Addsimps [drop_append];
8.558
8.559 Goal "!xs n. take n (take m xs) = take (min n m) xs";
8.560 by (induct_tac "m" 1);
8.561 - by (Auto_tac);
8.562 + by Auto_tac;
8.563 by (exhaust_tac "xs" 1);
8.564 - by (Auto_tac);
8.565 + by Auto_tac;
8.566 by (exhaust_tac "na" 1);
8.567 - by (Auto_tac);
8.568 + by Auto_tac;
8.569 qed_spec_mp "take_take";
8.570
8.571 Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
8.572 by (induct_tac "m" 1);
8.573 - by (Auto_tac);
8.574 + by Auto_tac;
8.575 by (exhaust_tac "xs" 1);
8.576 - by (Auto_tac);
8.577 + by Auto_tac;
8.578 qed_spec_mp "drop_drop";
8.579
8.580 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
8.581 by (induct_tac "m" 1);
8.582 - by (Auto_tac);
8.583 + by Auto_tac;
8.584 by (exhaust_tac "xs" 1);
8.585 - by (Auto_tac);
8.586 + by Auto_tac;
8.587 qed_spec_mp "take_drop";
8.588
8.589 Goal "!xs. take n (map f xs) = map f (take n xs)";
8.590 by (induct_tac "n" 1);
8.591 - by (Auto_tac);
8.592 + by Auto_tac;
8.593 by (exhaust_tac "xs" 1);
8.594 - by (Auto_tac);
8.595 + by Auto_tac;
8.596 qed_spec_mp "take_map";
8.597
8.598 Goal "!xs. drop n (map f xs) = map f (drop n xs)";
8.599 by (induct_tac "n" 1);
8.600 - by (Auto_tac);
8.601 + by Auto_tac;
8.602 by (exhaust_tac "xs" 1);
8.603 - by (Auto_tac);
8.604 + by Auto_tac;
8.605 qed_spec_mp "drop_map";
8.606
8.607 Goal "!n i. i < n --> (take n xs)!i = xs!i";
8.608 by (induct_tac "xs" 1);
8.609 - by (Auto_tac);
8.610 + by Auto_tac;
8.611 by (exhaust_tac "n" 1);
8.612 by (Blast_tac 1);
8.613 by (exhaust_tac "i" 1);
8.614 - by (Auto_tac);
8.615 + by Auto_tac;
8.616 qed_spec_mp "nth_take";
8.617 Addsimps [nth_take];
8.618
8.619 Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
8.620 by (induct_tac "n" 1);
8.621 - by (Auto_tac);
8.622 + by Auto_tac;
8.623 by (exhaust_tac "xs" 1);
8.624 - by (Auto_tac);
8.625 + by Auto_tac;
8.626 qed_spec_mp "nth_drop";
8.627 Addsimps [nth_drop];
8.628
8.629 @@ -757,37 +757,37 @@
8.630
8.631 Goal "takeWhile P xs @ dropWhile P xs = xs";
8.632 by (induct_tac "xs" 1);
8.633 -by (Auto_tac);
8.634 +by Auto_tac;
8.635 qed "takeWhile_dropWhile_id";
8.636 Addsimps [takeWhile_dropWhile_id];
8.637
8.638 Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
8.639 by (induct_tac "xs" 1);
8.640 -by (Auto_tac);
8.641 +by Auto_tac;
8.642 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
8.643 Addsimps [takeWhile_append1];
8.644
8.645 Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
8.646 by (induct_tac "xs" 1);
8.647 -by (Auto_tac);
8.648 +by Auto_tac;
8.649 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
8.650 Addsimps [takeWhile_append2];
8.651
8.652 Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
8.653 by (induct_tac "xs" 1);
8.654 -by (Auto_tac);
8.655 +by Auto_tac;
8.656 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
8.657 Addsimps [dropWhile_append1];
8.658
8.659 Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
8.660 by (induct_tac "xs" 1);
8.661 -by (Auto_tac);
8.662 +by Auto_tac;
8.663 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
8.664 Addsimps [dropWhile_append2];
8.665
8.666 Goal "x:set(takeWhile P xs) --> x:set xs & P x";
8.667 by (induct_tac "xs" 1);
8.668 -by (Auto_tac);
8.669 +by Auto_tac;
8.670 qed_spec_mp"set_take_whileD";
8.671
8.672 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);
8.673 @@ -800,7 +800,7 @@
8.674
8.675 Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
8.676 by(induct_tac "xs" 1);
8.677 -by(Auto_tac);
8.678 +by Auto_tac;
8.679 qed_spec_mp "foldl_append";
8.680 Addsimps [foldl_append];
8.681
8.682 @@ -821,7 +821,7 @@
8.683
8.684 Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
8.685 by(induct_tac "ns" 1);
8.686 -by(Auto_tac);
8.687 +by Auto_tac;
8.688 qed_spec_mp "sum_eq_0_conv";
8.689 AddIffs [sum_eq_0_conv];
8.690
8.691 @@ -838,12 +838,12 @@
8.692
8.693 Goal "nodups(remdups xs)";
8.694 by (induct_tac "xs" 1);
8.695 -by (Auto_tac);
8.696 +by Auto_tac;
8.697 qed "nodups_remdups";
8.698
8.699 Goal "nodups xs --> nodups (filter P xs)";
8.700 by (induct_tac "xs" 1);
8.701 -by (Auto_tac);
8.702 +by Auto_tac;
8.703 qed_spec_mp "nodups_filter";
8.704
8.705 (** replicate **)
8.706 @@ -851,7 +851,7 @@
8.707
8.708 Goal "set(replicate (Suc n) x) = {x}";
8.709 by (induct_tac "n" 1);
8.710 -by (Auto_tac);
8.711 +by Auto_tac;
8.712 val lemma = result();
8.713
8.714 Goal "n ~= 0 ==> set(replicate n x) = {x}";
9.1 --- a/src/HOL/Nat.ML Thu Aug 13 18:07:56 1998 +0200
9.2 +++ b/src/HOL/Nat.ML Thu Aug 13 18:14:26 1998 +0200
9.3 @@ -9,12 +9,12 @@
9.4 val [nat_rec_0, nat_rec_Suc] = nat.recs;
9.5
9.6 (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
9.7 -val prems = goal thy
9.8 +val prems = Goal
9.9 "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
9.10 by (simp_tac (simpset() addsimps prems) 1);
9.11 qed "def_nat_rec_0";
9.12
9.13 -val prems = goal thy
9.14 +val prems = Goal
9.15 "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
9.16 by (simp_tac (simpset() addsimps prems) 1);
9.17 qed "def_nat_rec_Suc";
9.18 @@ -26,9 +26,8 @@
9.19 by (REPEAT (Blast_tac 1));
9.20 qed "not0_implies_Suc";
9.21
9.22 -val prems = goal thy "m<n ==> n ~= 0";
9.23 +Goal "m<n ==> n ~= 0";
9.24 by (exhaust_tac "n" 1);
9.25 -by (cut_facts_tac prems 1);
9.26 by (ALLGOALS Asm_full_simp_tac);
9.27 qed "gr_implies_not0";
9.28
10.1 --- a/src/HOL/NatDef.ML Thu Aug 13 18:07:56 1998 +0200
10.2 +++ b/src/HOL/NatDef.ML Thu Aug 13 18:14:26 1998 +0200
10.3 @@ -20,22 +20,22 @@
10.4 by (rtac (singletonI RS UnI1) 1);
10.5 qed "Zero_RepI";
10.6
10.7 -val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat";
10.8 +Goal "i: Nat ==> Suc_Rep(i) : Nat";
10.9 by (stac Nat_unfold 1);
10.10 by (rtac (imageI RS UnI2) 1);
10.11 -by (resolve_tac prems 1);
10.12 +by (assume_tac 1);
10.13 qed "Suc_RepI";
10.14
10.15 (*** Induction ***)
10.16
10.17 -val major::prems = goal thy
10.18 +val major::prems = Goal
10.19 "[| i: Nat; P(Zero_Rep); \
10.20 \ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)";
10.21 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
10.22 by (blast_tac (claset() addIs prems) 1);
10.23 qed "Nat_induct";
10.24
10.25 -val prems = goalw thy [Zero_def,Suc_def]
10.26 +val prems = Goalw [Zero_def,Suc_def]
10.27 "[| P(0); \
10.28 \ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)";
10.29 by (rtac (Rep_Nat_inverse RS subst) 1); (*types force good instantiation*)
10.30 @@ -49,7 +49,7 @@
10.31 res_inst_tac [("n",a)] nat_induct i THEN rename_last_tac a [""] (i+1);
10.32
10.33 (*A special form of induction for reasoning about m<n and m-n*)
10.34 -val prems = goal thy
10.35 +val prems = Goal
10.36 "[| !!x. P x 0; \
10.37 \ !!y. P 0 (Suc y); \
10.38 \ !!x y. [| P x y |] ==> P (Suc x) (Suc y) \
10.39 @@ -131,10 +131,10 @@
10.40
10.41 (** Introduction properties **)
10.42
10.43 -val prems = goalw thy [less_def] "[| i<j; j<k |] ==> i<(k::nat)";
10.44 +Goalw [less_def] "[| i<j; j<k |] ==> i<(k::nat)";
10.45 by (rtac (trans_trancl RS transD) 1);
10.46 -by (resolve_tac prems 1);
10.47 -by (resolve_tac prems 1);
10.48 +by (assume_tac 1);
10.49 +by (assume_tac 1);
10.50 qed "less_trans";
10.51
10.52 Goalw [less_def, pred_nat_def] "n < Suc(n)";
10.53 @@ -156,8 +156,8 @@
10.54
10.55 (** Elimination properties **)
10.56
10.57 -val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
10.58 -by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
10.59 +Goalw [less_def] "n<m ==> ~ m<(n::nat)";
10.60 +by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1);
10.61 qed "less_not_sym";
10.62
10.63 (* [| n<m; m<n |] ==> R *)
10.64 @@ -176,7 +176,7 @@
10.65 qed "less_not_refl2";
10.66
10.67
10.68 -val major::prems = goalw thy [less_def, pred_nat_def]
10.69 +val major::prems = Goalw [less_def, pred_nat_def]
10.70 "[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \
10.71 \ |] ==> P";
10.72 by (rtac (major RS tranclE) 1);
10.73 @@ -197,7 +197,7 @@
10.74 (* n<0 ==> R *)
10.75 bind_thm ("less_zeroE", not_less0 RS notE);
10.76
10.77 -val [major,less,eq] = goal thy
10.78 +val [major,less,eq] = Goal
10.79 "[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P";
10.80 by (rtac (major RS lessE) 1);
10.81 by (rtac eq 1);
10.82 @@ -254,14 +254,14 @@
10.83 by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
10.84 qed "Suc_lessI";
10.85
10.86 -val [prem] = goal thy "Suc(m) < n ==> m<n";
10.87 -by (rtac (prem RS rev_mp) 1);
10.88 +Goal "Suc(m) < n ==> m<n";
10.89 +by (etac rev_mp 1);
10.90 by (nat_ind_tac "n" 1);
10.91 by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI]
10.92 addEs [less_trans, lessE])));
10.93 qed "Suc_lessD";
10.94
10.95 -val [major,minor] = goal thy
10.96 +val [major,minor] = Goal
10.97 "[| Suc(i)<k; !!j. [| i<j; k=Suc(j) |] ==> P \
10.98 \ |] ==> P";
10.99 by (rtac (major RS lessE) 1);
10.100 @@ -299,7 +299,7 @@
10.101 qed "not_less_eq";
10.102
10.103 (*Complete induction, aka course-of-values induction*)
10.104 -val prems = goalw thy [less_def]
10.105 +val prems = Goalw [less_def]
10.106 "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |] ==> P(n)";
10.107 by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
10.108 by (eresolve_tac prems 1);
10.109 @@ -350,12 +350,12 @@
10.110 but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
10.111 *)
10.112
10.113 -val prems = goalw thy [le_def] "~n<m ==> m<=(n::nat)";
10.114 -by (resolve_tac prems 1);
10.115 +Goalw [le_def] "~n<m ==> m<=(n::nat)";
10.116 +by (assume_tac 1);
10.117 qed "leI";
10.118
10.119 -val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)";
10.120 -by (resolve_tac prems 1);
10.121 +Goalw [le_def] "m<=n ==> ~ n < (m::nat)";
10.122 +by (assume_tac 1);
10.123 qed "leD";
10.124
10.125 val leE = make_elim leD;
10.126 @@ -505,7 +505,7 @@
10.127 by (simp_tac (simpset() addsimps [lemma]) 1);
10.128 qed "Least_nat_def";
10.129
10.130 -val [prem1,prem2] = goalw thy [Least_nat_def]
10.131 +val [prem1,prem2] = Goalw [Least_nat_def]
10.132 "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
10.133 by (rtac select_equality 1);
10.134 by (blast_tac (claset() addSIs [prem1,prem2]) 1);
10.135 @@ -513,8 +513,8 @@
10.136 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
10.137 qed "Least_equality";
10.138
10.139 -val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
10.140 -by (rtac (prem RS rev_mp) 1);
10.141 +Goal "P(k::nat) ==> P(LEAST x. P(x))";
10.142 +by (etac rev_mp 1);
10.143 by (res_inst_tac [("n","k")] less_induct 1);
10.144 by (rtac impI 1);
10.145 by (rtac classical 1);
10.146 @@ -525,8 +525,8 @@
10.147 qed "LeastI";
10.148
10.149 (*Proof is almost identical to the one above!*)
10.150 -val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
10.151 -by (rtac (prem RS rev_mp) 1);
10.152 +Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
10.153 +by (etac rev_mp 1);
10.154 by (res_inst_tac [("n","k")] less_induct 1);
10.155 by (rtac impI 1);
10.156 by (rtac classical 1);
10.157 @@ -536,10 +536,9 @@
10.158 by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1);
10.159 qed "Least_le";
10.160
10.161 -val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
10.162 +Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)";
10.163 by (rtac notI 1);
10.164 -by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
10.165 -by (rtac prem 1);
10.166 +by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
10.167 qed "not_less_Least";
10.168
10.169 (*** Instantiation of transitivity prover ***)
11.1 --- a/src/HOL/Ord.ML Thu Aug 13 18:07:56 1998 +0200
11.2 +++ b/src/HOL/Ord.ML Thu Aug 13 18:14:26 1998 +0200
11.3 @@ -8,15 +8,13 @@
11.4
11.5 (** mono **)
11.6
11.7 -val [prem] = goalw Ord.thy [mono_def]
11.8 +val [prem] = Goalw [mono_def]
11.9 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
11.10 by (REPEAT (ares_tac [allI, impI, prem] 1));
11.11 qed "monoI";
11.12
11.13 -val [major,minor] = goalw Ord.thy [mono_def]
11.14 - "[| mono(f); A <= B |] ==> f(A) <= f(B)";
11.15 -by (rtac (major RS spec RS spec RS mp) 1);
11.16 -by (rtac minor 1);
11.17 +Goalw [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)";
11.18 +by (Fast_tac 1);
11.19 qed "monoD";
11.20
11.21
11.22 @@ -46,7 +44,7 @@
11.23 by (simp_tac (simpset() addsimps prems) 1);
11.24 qed "min_leastL";
11.25
11.26 -val prems = goalw thy [min_def]
11.27 +val prems = Goalw [min_def]
11.28 "(!!x::'a::order. least <= x) ==> min x least = least";
11.29 by (cut_facts_tac prems 1);
11.30 by (Asm_simp_tac 1);
12.1 --- a/src/HOL/Prod.ML Thu Aug 13 18:07:56 1998 +0200
12.2 +++ b/src/HOL/Prod.ML Thu Aug 13 18:14:26 1998 +0200
12.3 @@ -24,7 +24,7 @@
12.4 by (etac Abs_Prod_inverse 1);
12.5 qed "inj_on_Abs_Prod";
12.6
12.7 -val prems = goalw Prod.thy [Pair_def]
12.8 +val prems = Goalw [Pair_def]
12.9 "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R";
12.10 by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
12.11 by (REPEAT (ares_tac (prems@[ProdI]) 1));
12.12 @@ -49,7 +49,7 @@
12.13 rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]);
12.14 qed "PairE_lemma";
12.15
12.16 -val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
12.17 +val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
12.18 by (rtac (PairE_lemma RS exE) 1);
12.19 by (REPEAT (eresolve_tac [prem,exE] 1));
12.20 qed "PairE";
12.21 @@ -222,7 +222,7 @@
12.22 by (Asm_simp_tac 1);
12.23 qed "splitI";
12.24
12.25 -val prems = goalw Prod.thy [split_def]
12.26 +val prems = Goalw [split_def]
12.27 "[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q";
12.28 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
12.29 qed "splitE";
12.30 @@ -246,7 +246,7 @@
12.31 by (Asm_simp_tac 1);
12.32 qed "mem_splitI2";
12.33
12.34 -val prems = goalw Prod.thy [split_def]
12.35 +val prems = Goalw [split_def]
12.36 "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q";
12.37 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
12.38 qed "mem_splitE";
12.39 @@ -298,13 +298,13 @@
12.40 qed "prod_fun_ident";
12.41 Addsimps [prod_fun_ident];
12.42
12.43 -val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
12.44 +Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
12.45 by (rtac image_eqI 1);
12.46 by (rtac (prod_fun RS sym) 1);
12.47 -by (resolve_tac prems 1);
12.48 +by (assume_tac 1);
12.49 qed "prod_fun_imageI";
12.50
12.51 -val major::prems = goal Prod.thy
12.52 +val major::prems = Goal
12.53 "[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
12.54 \ |] ==> P";
12.55 by (rtac (major RS imageE) 1);
12.56 @@ -354,7 +354,7 @@
12.57
12.58 AddSEs [SigmaE2, SigmaE];
12.59
12.60 -val prems = goal Prod.thy
12.61 +val prems = Goal
12.62 "[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
12.63 by (cut_facts_tac prems 1);
12.64 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
12.65 @@ -384,14 +384,14 @@
12.66
12.67 (*** Domain of a relation ***)
12.68
12.69 -val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
12.70 +Goalw [image_def] "(a,b) : r ==> a : fst``r";
12.71 by (rtac CollectI 1);
12.72 by (rtac bexI 1);
12.73 by (rtac (fst_conv RS sym) 1);
12.74 -by (resolve_tac prems 1);
12.75 +by (assume_tac 1);
12.76 qed "fst_imageI";
12.77
12.78 -val major::prems = goal Prod.thy
12.79 +val major::prems = Goal
12.80 "[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P";
12.81 by (rtac (major RS imageE) 1);
12.82 by (resolve_tac prems 1);
12.83 @@ -402,15 +402,14 @@
12.84
12.85 (*** Range of a relation ***)
12.86
12.87 -val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
12.88 +Goalw [image_def] "(a,b) : r ==> b : snd``r";
12.89 by (rtac CollectI 1);
12.90 by (rtac bexI 1);
12.91 by (rtac (snd_conv RS sym) 1);
12.92 -by (resolve_tac prems 1);
12.93 +by (assume_tac 1);
12.94 qed "snd_imageI";
12.95
12.96 -val major::prems = goal Prod.thy
12.97 - "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P";
12.98 +val major::prems = Goal "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P";
12.99 by (rtac (major RS imageE) 1);
12.100 by (resolve_tac prems 1);
12.101 by (etac ssubst 1);
13.1 --- a/src/HOL/RelPow.ML Thu Aug 13 18:07:56 1998 +0200
13.2 +++ b/src/HOL/RelPow.ML Thu Aug 13 18:14:26 1998 +0200
13.3 @@ -31,14 +31,14 @@
13.4 by (Asm_full_simp_tac 1);
13.5 qed "rel_pow_0_E";
13.6
13.7 -val [major,minor] = goal RelPow.thy
13.8 +val [major,minor] = Goal
13.9 "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
13.10 by (cut_facts_tac [major] 1);
13.11 by (Asm_full_simp_tac 1);
13.12 by (blast_tac (claset() addIs [minor]) 1);
13.13 qed "rel_pow_Suc_E";
13.14
13.15 -val [p1,p2,p3] = goal RelPow.thy
13.16 +val [p1,p2,p3] = Goal
13.17 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
13.18 \ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \
13.19 \ |] ==> P";
13.20 @@ -52,18 +52,20 @@
13.21
13.22 Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
13.23 by (nat_ind_tac "n" 1);
13.24 -by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
13.25 -by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
13.26 +by (blast_tac (claset() addIs [rel_pow_0_I]
13.27 + addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
13.28 +by (blast_tac (claset() addIs [rel_pow_Suc_I]
13.29 + addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
13.30 qed_spec_mp "rel_pow_Suc_D2";
13.31
13.32
13.33 Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
13.34 by (nat_ind_tac "n" 1);
13.35 -by (fast_tac (claset() addss (simpset())) 1);
13.36 -by (fast_tac (claset() addss (simpset())) 1);
13.37 +by (ALLGOALS Asm_simp_tac);
13.38 +by (Blast_tac 1);
13.39 qed_spec_mp "rel_pow_Suc_D2'";
13.40
13.41 -val [p1,p2,p3] = goal RelPow.thy
13.42 +val [p1,p2,p3] = Goal
13.43 "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
13.44 \ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \
13.45 \ |] ==> P";
14.1 --- a/src/HOL/Relation.ML Thu Aug 13 18:07:56 1998 +0200
14.2 +++ b/src/HOL/Relation.ML Thu Aug 13 18:14:26 1998 +0200
14.3 @@ -12,7 +12,7 @@
14.4 by (Blast_tac 1);
14.5 qed "idI";
14.6
14.7 -val major::prems = goalw thy [id_def]
14.8 +val major::prems = Goalw [id_def]
14.9 "[| p: id; !!x.[| p = (x,x) |] ==> P \
14.10 \ |] ==> P";
14.11 by (rtac (major RS CollectE) 1);
14.12 @@ -34,7 +34,7 @@
14.13 qed "compI";
14.14
14.15 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
14.16 -val prems = goalw thy [comp_def]
14.17 +val prems = Goalw [comp_def]
14.18 "[| xz : r O s; \
14.19 \ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \
14.20 \ |] ==> P";
14.21 @@ -43,7 +43,7 @@
14.22 ORELSE ares_tac prems 1));
14.23 qed "compE";
14.24
14.25 -val prems = goal thy
14.26 +val prems = Goal
14.27 "[| (a,c) : r O s; \
14.28 \ !!y. [| (a,y):s; (y,c):r |] ==> P \
14.29 \ |] ==> P";
14.30 @@ -78,7 +78,7 @@
14.31
14.32 (** Natural deduction for trans(r) **)
14.33
14.34 -val prems = goalw thy [trans_def]
14.35 +val prems = Goalw [trans_def]
14.36 "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)";
14.37 by (REPEAT (ares_tac (prems@[allI,impI]) 1));
14.38 qed "transI";
15.1 --- a/src/HOL/Set.ML Thu Aug 13 18:07:56 1998 +0200
15.2 +++ b/src/HOL/Set.ML Thu Aug 13 18:14:26 1998 +0200
15.3 @@ -17,17 +17,17 @@
15.4 by (Asm_simp_tac 1);
15.5 qed "CollectI";
15.6
15.7 -val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
15.8 +Goal "a : {x. P(x)} ==> P(a)";
15.9 by (Asm_full_simp_tac 1);
15.10 qed "CollectD";
15.11
15.12 -val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
15.13 +val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
15.14 by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
15.15 by (rtac Collect_mem_eq 1);
15.16 by (rtac Collect_mem_eq 1);
15.17 qed "set_ext";
15.18
15.19 -val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
15.20 +val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
15.21 by (rtac (prem RS ext RS arg_cong) 1);
15.22 qed "Collect_cong";
15.23
15.24 @@ -39,17 +39,16 @@
15.25
15.26 section "Bounded quantifiers";
15.27
15.28 -val prems = goalw Set.thy [Ball_def]
15.29 +val prems = Goalw [Ball_def]
15.30 "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
15.31 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
15.32 qed "ballI";
15.33
15.34 -val [major,minor] = goalw Set.thy [Ball_def]
15.35 - "[| ! x:A. P(x); x:A |] ==> P(x)";
15.36 -by (rtac (minor RS (major RS spec RS mp)) 1);
15.37 +Goalw [Ball_def] "[| ! x:A. P(x); x:A |] ==> P(x)";
15.38 +by (Blast_tac 1);
15.39 qed "bspec";
15.40
15.41 -val major::prems = goalw Set.thy [Ball_def]
15.42 +val major::prems = Goalw [Ball_def]
15.43 "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
15.44 by (rtac (major RS spec RS impCE) 1);
15.45 by (REPEAT (eresolve_tac prems 1));
15.46 @@ -61,9 +60,8 @@
15.47 AddSIs [ballI];
15.48 AddEs [ballE];
15.49
15.50 -val prems = goalw Set.thy [Bex_def]
15.51 - "[| P(x); x:A |] ==> ? x:A. P(x)";
15.52 -by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
15.53 +Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)";
15.54 +by (Blast_tac 1);
15.55 qed "bexI";
15.56
15.57 qed_goal "bexCI" Set.thy
15.58 @@ -72,7 +70,7 @@
15.59 [ (rtac classical 1),
15.60 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
15.61
15.62 -val major::prems = goalw Set.thy [Bex_def]
15.63 +val major::prems = Goalw [Bex_def]
15.64 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q";
15.65 by (rtac (major RS exE) 1);
15.66 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
15.67 @@ -95,7 +93,7 @@
15.68
15.69 (** Congruence rules **)
15.70
15.71 -val prems = goal Set.thy
15.72 +val prems = Goal
15.73 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
15.74 \ (! x:A. P(x)) = (! x:B. Q(x))";
15.75 by (resolve_tac (prems RL [ssubst]) 1);
15.76 @@ -103,7 +101,7 @@
15.77 ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
15.78 qed "ball_cong";
15.79
15.80 -val prems = goal Set.thy
15.81 +val prems = Goal
15.82 "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \
15.83 \ (? x:A. P(x)) = (? x:B. Q(x))";
15.84 by (resolve_tac (prems RL [ssubst]) 1);
15.85 @@ -113,7 +111,7 @@
15.86
15.87 section "Subsets";
15.88
15.89 -val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
15.90 +val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
15.91 by (REPEAT (ares_tac (prems @ [ballI]) 1));
15.92 qed "subsetI";
15.93
15.94 @@ -130,9 +128,8 @@
15.95 Blast.overloaded ("op ``", domain_type o domain_type);
15.96
15.97 (*Rule in Modus Ponens style*)
15.98 -val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B";
15.99 -by (rtac (major RS bspec) 1);
15.100 -by (resolve_tac prems 1);
15.101 +Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";
15.102 +by (Blast_tac 1);
15.103 qed "subsetD";
15.104
15.105 (*The same, with reversed premises for use with etac -- cf rev_mp*)
15.106 @@ -149,7 +146,7 @@
15.107 (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
15.108
15.109 (*Classical elimination rule*)
15.110 -val major::prems = goalw Set.thy [subset_def]
15.111 +val major::prems = Goalw [subset_def]
15.112 "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
15.113 by (rtac (major RS ballE) 1);
15.114 by (REPEAT (eresolve_tac prems 1));
15.115 @@ -164,7 +161,7 @@
15.116 qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
15.117 (fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*)
15.118
15.119 -val prems = goal Set.thy "!!B. [| A<=B; B<=C |] ==> A<=(C::'a set)";
15.120 +Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)";
15.121 by (Blast_tac 1);
15.122 qed "subset_trans";
15.123
15.124 @@ -172,32 +169,32 @@
15.125 section "Equality";
15.126
15.127 (*Anti-symmetry of the subset relation*)
15.128 -val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)";
15.129 -by (rtac (iffI RS set_ext) 1);
15.130 -by (REPEAT (ares_tac (prems RL [subsetD]) 1));
15.131 +Goal "[| A <= B; B <= A |] ==> A = (B::'a set)";
15.132 +br set_ext 1;
15.133 +by (blast_tac (claset() addIs [subsetD]) 1);
15.134 qed "subset_antisym";
15.135 val equalityI = subset_antisym;
15.136
15.137 AddSIs [equalityI];
15.138
15.139 (* Equality rules from ZF set theory -- are they appropriate here? *)
15.140 -val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
15.141 -by (resolve_tac (prems RL [subst]) 1);
15.142 +Goal "A = B ==> A<=(B::'a set)";
15.143 +by (etac ssubst 1);
15.144 by (rtac subset_refl 1);
15.145 qed "equalityD1";
15.146
15.147 -val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
15.148 -by (resolve_tac (prems RL [subst]) 1);
15.149 +Goal "A = B ==> B<=(A::'a set)";
15.150 +by (etac ssubst 1);
15.151 by (rtac subset_refl 1);
15.152 qed "equalityD2";
15.153
15.154 -val prems = goal Set.thy
15.155 +val prems = Goal
15.156 "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P";
15.157 by (resolve_tac prems 1);
15.158 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
15.159 qed "equalityE";
15.160
15.161 -val major::prems = goal Set.thy
15.162 +val major::prems = Goal
15.163 "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
15.164 by (rtac (major RS equalityE) 1);
15.165 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
15.166 @@ -206,7 +203,7 @@
15.167 (*Lemma for creating induction formulae -- for "pattern matching" on p
15.168 To make the induction hypotheses usable, apply "spec" or "bspec" to
15.169 put universal quantifiers over the free variables in p. *)
15.170 -val prems = goal Set.thy
15.171 +val prems = Goal
15.172 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R";
15.173 by (rtac mp 1);
15.174 by (REPEAT (resolve_tac (refl::prems) 1));
15.175 @@ -305,17 +302,15 @@
15.176
15.177 Addsimps [Compl_iff];
15.178
15.179 -val prems = goalw Set.thy [Compl_def]
15.180 - "[| c:A ==> False |] ==> c : Compl(A)";
15.181 +val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
15.182 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
15.183 qed "ComplI";
15.184
15.185 (*This form, with negated conclusion, works well with the Classical prover.
15.186 Negated assumptions behave like formulae on the right side of the notional
15.187 turnstile...*)
15.188 -val major::prems = goalw Set.thy [Compl_def]
15.189 - "c : Compl(A) ==> c~:A";
15.190 -by (rtac (major RS CollectD) 1);
15.191 +Goalw [Compl_def] "c : Compl(A) ==> c~:A";
15.192 +by (etac CollectD 1);
15.193 qed "ComplD";
15.194
15.195 val ComplE = make_elim ComplD;
15.196 @@ -345,7 +340,7 @@
15.197 [ (Simp_tac 1),
15.198 (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
15.199
15.200 -val major::prems = goalw Set.thy [Un_def]
15.201 +val major::prems = Goalw [Un_def]
15.202 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
15.203 by (rtac (major RS CollectD RS disjE) 1);
15.204 by (REPEAT (eresolve_tac prems 1));
15.205 @@ -374,7 +369,7 @@
15.206 by (Asm_full_simp_tac 1);
15.207 qed "IntD2";
15.208
15.209 -val [major,minor] = goal Set.thy
15.210 +val [major,minor] = Goal
15.211 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P";
15.212 by (rtac minor 1);
15.213 by (rtac (major RS IntD1) 1);
15.214 @@ -479,7 +474,7 @@
15.215 by Auto_tac;
15.216 qed "UN_I";
15.217
15.218 -val major::prems = goalw Set.thy [UNION_def]
15.219 +val major::prems = Goalw [UNION_def]
15.220 "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R";
15.221 by (rtac (major RS CollectD RS bexE) 1);
15.222 by (REPEAT (ares_tac prems 1));
15.223 @@ -488,7 +483,7 @@
15.224 AddIs [UN_I];
15.225 AddSEs [UN_E];
15.226
15.227 -val prems = goal Set.thy
15.228 +val prems = Goal
15.229 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
15.230 \ (UN x:A. C(x)) = (UN x:B. D(x))";
15.231 by (REPEAT (etac UN_E 1
15.232 @@ -505,7 +500,7 @@
15.233
15.234 Addsimps [INT_iff];
15.235
15.236 -val prems = goalw Set.thy [INTER_def]
15.237 +val prems = Goalw [INTER_def]
15.238 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
15.239 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
15.240 qed "INT_I";
15.241 @@ -515,7 +510,7 @@
15.242 qed "INT_D";
15.243
15.244 (*"Classical" elimination -- by the Excluded Middle on a:A *)
15.245 -val major::prems = goalw Set.thy [INTER_def]
15.246 +val major::prems = Goalw [INTER_def]
15.247 "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R";
15.248 by (rtac (major RS CollectD RS ballE) 1);
15.249 by (REPEAT (eresolve_tac prems 1));
15.250 @@ -524,7 +519,7 @@
15.251 AddSIs [INT_I];
15.252 AddEs [INT_D, INT_E];
15.253
15.254 -val prems = goal Set.thy
15.255 +val prems = Goal
15.256 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
15.257 \ (INT x:A. C(x)) = (INT x:B. D(x))";
15.258 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
15.259 @@ -546,7 +541,7 @@
15.260 by Auto_tac;
15.261 qed "UnionI";
15.262
15.263 -val major::prems = goalw Set.thy [Union_def]
15.264 +val major::prems = Goalw [Union_def]
15.265 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R";
15.266 by (rtac (major RS UN_E) 1);
15.267 by (REPEAT (ares_tac prems 1));
15.268 @@ -564,7 +559,7 @@
15.269
15.270 Addsimps [Inter_iff];
15.271
15.272 -val prems = goalw Set.thy [Inter_def]
15.273 +val prems = Goalw [Inter_def]
15.274 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
15.275 by (REPEAT (ares_tac ([INT_I] @ prems) 1));
15.276 qed "InterI";
15.277 @@ -576,7 +571,7 @@
15.278 qed "InterD";
15.279
15.280 (*"Classical" elimination rule -- does not require proving X:C *)
15.281 -val major::prems = goalw Set.thy [Inter_def]
15.282 +val major::prems = Goalw [Inter_def]
15.283 "[| A : Inter(C); X~:C ==> R; A:X ==> R |] ==> R";
15.284 by (rtac (major RS INT_E) 1);
15.285 by (REPEAT (eresolve_tac prems 1));
15.286 @@ -589,15 +584,15 @@
15.287 (*** Image of a set under a function ***)
15.288
15.289 (*Frequently b does not have the syntactic form of f(x).*)
15.290 -val prems = goalw thy [image_def] "[| b=f(x); x:A |] ==> b : f``A";
15.291 -by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
15.292 +Goalw [image_def] "[| b=f(x); x:A |] ==> b : f``A";
15.293 +by (Blast_tac 1);
15.294 qed "image_eqI";
15.295 Addsimps [image_eqI];
15.296
15.297 bind_thm ("imageI", refl RS image_eqI);
15.298
15.299 (*The eta-expansion gives variable-name preservation.*)
15.300 -val major::prems = goalw thy [image_def]
15.301 +val major::prems = Goalw [image_def]
15.302 "[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
15.303 by (rtac (major RS CollectD RS bexE) 1);
15.304 by (REPEAT (ares_tac prems 1));
15.305 @@ -621,7 +616,7 @@
15.306
15.307 (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
15.308 many existing proofs.*)
15.309 -val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
15.310 +val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
15.311 by (blast_tac (claset() addIs prems) 1);
15.312 qed "image_subsetI";
15.313
15.314 @@ -634,7 +629,7 @@
15.315
15.316 bind_thm ("rangeI", UNIV_I RS imageI);
15.317
15.318 -val [major,minor] = goal thy
15.319 +val [major,minor] = Goal
15.320 "[| b : range(%x. f(x)); !!x. b=f(x) ==> P |] ==> P";
15.321 by (rtac (major RS imageE) 1);
15.322 by (etac minor 1);
16.1 --- a/src/HOL/Sum.ML Thu Aug 13 18:07:56 1998 +0200
16.2 +++ b/src/HOL/Sum.ML Thu Aug 13 18:14:26 1998 +0200
16.3 @@ -3,7 +3,7 @@
16.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
16.5 Copyright 1991 University of Cambridge
16.6
16.7 -For Sum.thy. The disjoint sum of two types
16.8 +The disjoint sum of two types
16.9 *)
16.10
16.11 open Sum;
16.12 @@ -51,13 +51,13 @@
16.13
16.14 (** Injectiveness of Inl and Inr **)
16.15
16.16 -val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
16.17 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
16.18 +Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
16.19 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
16.20 by (Blast_tac 1);
16.21 qed "Inl_Rep_inject";
16.22
16.23 -val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
16.24 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
16.25 +Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
16.26 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
16.27 by (Blast_tac 1);
16.28 qed "Inr_Rep_inject";
16.29
16.30 @@ -101,7 +101,7 @@
16.31
16.32 (** Elimination rules **)
16.33
16.34 -val major::prems = goalw Sum.thy [sum_def]
16.35 +val major::prems = Goalw [sum_def]
16.36 "[| u: A Plus B; \
16.37 \ !!x. [| x:A; u=Inl(x) |] ==> P; \
16.38 \ !!y. [| y:B; u=Inr(y) |] ==> P \
16.39 @@ -130,7 +130,7 @@
16.40
16.41 (** Exhaustion rule for sums -- a degenerate form of induction **)
16.42
16.43 -val prems = goalw Sum.thy [Inl_def,Inr_def]
16.44 +val prems = Goalw [Inl_def,Inr_def]
16.45 "[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \
16.46 \ |] ==> P";
16.47 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
16.48 @@ -140,7 +140,7 @@
16.49 rtac (Rep_Sum_inverse RS sym)]));
16.50 qed "sumE";
16.51
16.52 -val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
16.53 +val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
16.54 by (res_inst_tac [("s","x")] sumE 1);
16.55 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
16.56 qed "sum_induct";
16.57 @@ -177,7 +177,7 @@
16.58
16.59 val PartI = refl RSN (2,Part_eqI);
16.60
16.61 -val major::prems = goalw Sum.thy [Part_def]
16.62 +val major::prems = Goalw [Part_def]
16.63 "[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \
16.64 \ |] ==> P";
16.65 by (rtac (major RS IntE) 1);
17.1 --- a/src/HOL/Trancl.ML Thu Aug 13 18:07:56 1998 +0200
17.2 +++ b/src/HOL/Trancl.ML Thu Aug 13 18:14:26 1998 +0200
17.3 @@ -3,7 +3,7 @@
17.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
17.5 Copyright 1992 University of Cambridge
17.6
17.7 -For Trancl.thy. Theorems about the transitive closure of a relation
17.8 +Theorems about the transitive closure of a relation
17.9 *)
17.10
17.11 open Trancl;
17.12 @@ -46,7 +46,7 @@
17.13
17.14 (** standard induction rule **)
17.15
17.16 -val major::prems = goal Trancl.thy
17.17 +val major::prems = Goal
17.18 "[| (a,b) : r^*; \
17.19 \ !!x. P((x,x)); \
17.20 \ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \
17.21 @@ -56,7 +56,7 @@
17.22 qed "rtrancl_full_induct";
17.23
17.24 (*nice induction rule*)
17.25 -val major::prems = goal Trancl.thy
17.26 +val major::prems = Goal
17.27 "[| (a::'a,b) : r^*; \
17.28 \ P(a); \
17.29 \ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \
17.30 @@ -85,7 +85,7 @@
17.31
17.32
17.33 (*elimination of rtrancl -- by induction on a special formula*)
17.34 -val major::prems = goal Trancl.thy
17.35 +val major::prems = Goal
17.36 "[| (a::'a,b) : r^*; (a = b) ==> P; \
17.37 \ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \
17.38 \ |] ==> P";
17.39 @@ -133,8 +133,9 @@
17.40 qed "rtrancl_subset";
17.41
17.42 Goal "(R^* Un S^*)^* = (R Un S)^*";
17.43 -by (blast_tac (claset() addSIs [rtrancl_subset]
17.44 - addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
17.45 +(*Blast_tac: PROOF FAILED*)
17.46 +by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
17.47 + addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
17.48 qed "rtrancl_Un_rtrancl";
17.49
17.50 Goal "(R^=)^* = R^*";
17.51 @@ -160,7 +161,7 @@
17.52 by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
17.53 qed "rtrancl_converse";
17.54
17.55 -val major::prems = goal Trancl.thy
17.56 +val major::prems = Goal
17.57 "[| (a,b) : r^*; P(b); \
17.58 \ !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] \
17.59 \ ==> P(a)";
17.60 @@ -169,7 +170,7 @@
17.61 by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
17.62 qed "converse_rtrancl_induct";
17.63
17.64 -val prems = goal Trancl.thy
17.65 +val prems = Goal
17.66 "[| ((a,b),(c,d)) : r^*; P c d; \
17.67 \ !!x y z u.[| ((x,y),(z,u)) : r; ((z,u),(c,d)) : r^*; P z u |] ==> P x y\
17.68 \ |] ==> P a b";
17.69 @@ -183,7 +184,7 @@
17.70 by (REPEAT(ares_tac prems 1));
17.71 qed "converse_rtrancl_induct2";
17.72
17.73 -val major::prems = goal Trancl.thy
17.74 +val major::prems = Goal
17.75 "[| (x,z):r^*; \
17.76 \ x=z ==> P; \
17.77 \ !!y. [| (x,y):r; (y,z):r^* |] ==> P \
17.78 @@ -237,7 +238,7 @@
17.79 qed "rtrancl_into_trancl2";
17.80
17.81 (*Nice induction rule for trancl*)
17.82 -val major::prems = goal Trancl.thy
17.83 +val major::prems = Goal
17.84 "[| (a,b) : r^+; \
17.85 \ !!y. [| (a,y) : r |] ==> P(y); \
17.86 \ !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) \
17.87 @@ -252,7 +253,7 @@
17.88 qed "trancl_induct";
17.89
17.90 (*elimination of r^+ -- NOT an induction rule*)
17.91 -val major::prems = goal Trancl.thy
17.92 +val major::prems = Goal
17.93 "[| (a::'a,b) : r^+; \
17.94 \ (a,b) : r ==> P; \
17.95 \ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \
18.1 --- a/src/HOL/Univ.ML Thu Aug 13 18:07:56 1998 +0200
18.2 +++ b/src/HOL/Univ.ML Thu Aug 13 18:14:26 1998 +0200
18.3 @@ -14,7 +14,7 @@
18.4 by (rtac split 1);
18.5 qed "apfst_conv";
18.6
18.7 -val [major,minor] = goal Univ.thy
18.8 +val [major,minor] = Goal
18.9 "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \
18.10 \ |] ==> R";
18.11 by (rtac PairE 1);
18.12 @@ -27,26 +27,27 @@
18.13
18.14 (** Push -- an injection, analogous to Cons on lists **)
18.15
18.16 -val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> i=j";
18.17 -by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
18.18 +Goalw [Push_def] "Push i f = Push j g ==> i=j";
18.19 +by (etac (fun_cong RS box_equals RS Suc_inject) 1);
18.20 by (rtac nat_case_0 1);
18.21 by (rtac nat_case_0 1);
18.22 qed "Push_inject1";
18.23
18.24 -val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g ==> f=g";
18.25 -by (rtac (major RS fun_cong RS ext RS box_equals) 1);
18.26 +Goalw [Push_def] "Push i f = Push j g ==> f=g";
18.27 +by (rtac (ext RS box_equals) 1);
18.28 +by (etac fun_cong 1);
18.29 by (rtac (nat_case_Suc RS ext) 1);
18.30 by (rtac (nat_case_Suc RS ext) 1);
18.31 qed "Push_inject2";
18.32
18.33 -val [major,minor] = goal Univ.thy
18.34 +val [major,minor] = Goal
18.35 "[| Push i f =Push j g; [| i=j; f=g |] ==> P \
18.36 \ |] ==> P";
18.37 by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
18.38 qed "Push_inject";
18.39
18.40 -val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
18.41 -by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
18.42 +Goalw [Push_def] "Push k f =(%z.0) ==> P";
18.43 +by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
18.44 by (rtac nat_case_0 1);
18.45 by (rtac refl 1);
18.46 qed "Push_neq_K0";
18.47 @@ -125,7 +126,7 @@
18.48
18.49 (** Injectiveness of Push_Node **)
18.50
18.51 -val [major,minor] = goalw Univ.thy [Push_Node_def]
18.52 +val [major,minor] = Goalw [Push_Node_def]
18.53 "[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P \
18.54 \ |] ==> P";
18.55 by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
18.56 @@ -150,17 +151,17 @@
18.57 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
18.58 qed "Scons_inject_lemma2";
18.59
18.60 -val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> M=M'";
18.61 -by (rtac (major RS equalityE) 1);
18.62 +Goal "Scons M N = Scons M' N' ==> M=M'";
18.63 +by (etac equalityE 1);
18.64 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
18.65 qed "Scons_inject1";
18.66
18.67 -val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> N=N'";
18.68 -by (rtac (major RS equalityE) 1);
18.69 +Goal "Scons M N = Scons M' N' ==> N=N'";
18.70 +by (etac equalityE 1);
18.71 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
18.72 qed "Scons_inject2";
18.73
18.74 -val [major,minor] = goal Univ.thy
18.75 +val [major,minor] = Goal
18.76 "[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P \
18.77 \ |] ==> P";
18.78 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
18.79 @@ -302,7 +303,7 @@
18.80 qed "uprodI";
18.81
18.82 (*The general elimination rule*)
18.83 -val major::prems = goalw Univ.thy [uprod_def]
18.84 +val major::prems = Goalw [uprod_def]
18.85 "[| c : A<*>B; \
18.86 \ !!x y. [| x:A; y:B; c = Scons x y |] ==> P \
18.87 \ |] ==> P";
18.88 @@ -312,7 +313,7 @@
18.89 qed "uprodE";
18.90
18.91 (*Elimination of a pair -- introduces no eigenvariables*)
18.92 -val prems = goal Univ.thy
18.93 +val prems = Goal
18.94 "[| Scons M N : A<*>B; [| M:A; N:B |] ==> P \
18.95 \ |] ==> P";
18.96 by (rtac uprodE 1);
18.97 @@ -330,7 +331,7 @@
18.98 by (Blast_tac 1);
18.99 qed "usum_In1I";
18.100
18.101 -val major::prems = goalw Univ.thy [usum_def]
18.102 +val major::prems = Goalw [usum_def]
18.103 "[| u : A<+>B; \
18.104 \ !!x. [| x:A; u=In0(x) |] ==> P; \
18.105 \ !!y. [| y:B; u=In1(y) |] ==> P \
18.106 @@ -352,12 +353,12 @@
18.107
18.108 AddIffs [In0_not_In1, In1_not_In0];
18.109
18.110 -val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==> M=N";
18.111 -by (rtac (major RS Scons_inject2) 1);
18.112 +Goalw [In0_def] "In0(M) = In0(N) ==> M=N";
18.113 +by (etac (Scons_inject2) 1);
18.114 qed "In0_inject";
18.115
18.116 -val [major] = goalw Univ.thy [In1_def] "In1(M) = In1(N) ==> M=N";
18.117 -by (rtac (major RS Scons_inject2) 1);
18.118 +Goalw [In1_def] "In1(M) = In1(N) ==> M=N";
18.119 +by (etac (Scons_inject2) 1);
18.120 qed "In1_inject";
18.121
18.122 Goal "(In0 M = In0 N) = (M=N)";
18.123 @@ -385,14 +386,13 @@
18.124 by (Blast_tac 1);
18.125 qed "ntrunc_subsetI";
18.126
18.127 -val [major] = goalw Univ.thy [ntrunc_def]
18.128 - "(!!k. ntrunc k M <= N) ==> M<=N";
18.129 +val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
18.130 by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2,
18.131 major RS subsetD]) 1);
18.132 qed "ntrunc_subsetD";
18.133
18.134 (*A generalized form of the take-lemma*)
18.135 -val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
18.136 +val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
18.137 by (rtac equalityI 1);
18.138 by (ALLGOALS (rtac ntrunc_subsetD));
18.139 by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
18.140 @@ -400,7 +400,7 @@
18.141 by (rtac (major RS equalityD2) 1);
18.142 qed "ntrunc_equality";
18.143
18.144 -val [major] = goalw Univ.thy [o_def]
18.145 +val [major] = Goalw [o_def]
18.146 "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
18.147 by (rtac (ntrunc_equality RS ext) 1);
18.148 by (rtac (major RS fun_cong) 1);
18.149 @@ -478,7 +478,7 @@
18.150 val diagI = refl RS diag_eqI |> standard;
18.151
18.152 (*The general elimination rule*)
18.153 -val major::prems = goalw Univ.thy [diag_def]
18.154 +val major::prems = Goalw [diag_def]
18.155 "[| c : diag(A); \
18.156 \ !!x y. [| x:A; c = (x,x) |] ==> P \
18.157 \ |] ==> P";
18.158 @@ -494,7 +494,7 @@
18.159 qed "dprodI";
18.160
18.161 (*The general elimination rule*)
18.162 -val major::prems = goalw Univ.thy [dprod_def]
18.163 +val major::prems = Goalw [dprod_def]
18.164 "[| c : r<**>s; \
18.165 \ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') |] ==> P \
18.166 \ |] ==> P";
18.167 @@ -514,7 +514,7 @@
18.168 by (Blast_tac 1);
18.169 qed "dsum_In1I";
18.170
18.171 -val major::prems = goalw Univ.thy [dsum_def]
18.172 +val major::prems = Goalw [dsum_def]
18.173 "[| w : r<++>s; \
18.174 \ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \
18.175 \ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \
19.1 --- a/src/HOL/WF.ML Thu Aug 13 18:07:56 1998 +0200
19.2 +++ b/src/HOL/WF.ML Thu Aug 13 18:14:26 1998 +0200
19.3 @@ -12,7 +12,7 @@
19.4 val H_cong1 = refl RS H_cong;
19.5
19.6 (*Restriction to domain A. If r is well-founded over A then wf(r)*)
19.7 -val [prem1,prem2] = goalw WF.thy [wf_def]
19.8 +val [prem1,prem2] = Goalw [wf_def]
19.9 "[| r <= A Times A; \
19.10 \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
19.11 \ ==> wf(r)";
19.12 @@ -22,7 +22,7 @@
19.13 by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
19.14 qed "wfI";
19.15
19.16 -val major::prems = goalw WF.thy [wf_def]
19.17 +val major::prems = Goalw [wf_def]
19.18 "[| wf(r); \
19.19 \ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
19.20 \ |] ==> P(a)";
19.21 @@ -36,26 +36,25 @@
19.22 rename_last_tac a ["1"] (i+1),
19.23 ares_tac prems i];
19.24
19.25 -val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P";
19.26 +Goal "[| wf(r); (a,x):r; (x,a):r |] ==> P";
19.27 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
19.28 -by (blast_tac (claset() addIs prems) 1);
19.29 -by (wf_ind_tac "a" prems 1);
19.30 +by (Blast_tac 1);
19.31 +by (wf_ind_tac "a" [] 1);
19.32 by (Blast_tac 1);
19.33 qed "wf_asym";
19.34
19.35 -val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P";
19.36 -by (rtac wf_asym 1);
19.37 -by (REPEAT (resolve_tac prems 1));
19.38 +Goal "[| wf(r); (a,a): r |] ==> P";
19.39 +by (blast_tac (claset() addEs [wf_asym]) 1);
19.40 qed "wf_irrefl";
19.41
19.42 (*transitive closure of a wf relation is wf! *)
19.43 -val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
19.44 -by (rewtac wf_def);
19.45 +Goal "wf(r) ==> wf(r^+)";
19.46 +by (stac wf_def 1);
19.47 by (Clarify_tac 1);
19.48 (*must retain the universal formula for later use!*)
19.49 by (rtac allE 1 THEN assume_tac 1);
19.50 by (etac mp 1);
19.51 -by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
19.52 +by (eres_inst_tac [("a","x")] wf_induct 1);
19.53 by (rtac (impI RS allI) 1);
19.54 by (etac tranclE 1);
19.55 by (Blast_tac 1);
19.56 @@ -72,14 +71,13 @@
19.57 * Minimal-element characterization of well-foundedness
19.58 *---------------------------------------------------------------------------*)
19.59
19.60 -val wfr::_ = goalw WF.thy [wf_def]
19.61 - "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
19.62 -by (rtac (wfr RS spec RS mp RS spec) 1);
19.63 +Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
19.64 +bd spec 1;
19.65 +by (etac (mp RS spec) 1);
19.66 by (Blast_tac 1);
19.67 val lemma1 = result();
19.68
19.69 -Goalw [wf_def]
19.70 - "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
19.71 +Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
19.72 by (Clarify_tac 1);
19.73 by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
19.74 by (Blast_tac 1);
19.75 @@ -138,11 +136,10 @@
19.76 * Wellfoundedness of `disjoint union'
19.77 *---------------------------------------------------------------------------*)
19.78
19.79 -Goal
19.80 - "[| !i:I. wf(r i); \
19.81 -\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
19.82 -\ Domain(r j) Int Range(r i) = {} \
19.83 -\ |] ==> wf(UN i:I. r i)";
19.84 +Goal "[| !i:I. wf(r i); \
19.85 +\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
19.86 +\ Domain(r j) Int Range(r i) = {} \
19.87 +\ |] ==> wf(UN i:I. r i)";
19.88 by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
19.89 by(Clarify_tac 1);
19.90 by(rename_tac "A a" 1);
19.91 @@ -181,9 +178,8 @@
19.92 by(Blast_tac 1);
19.93 qed "wf_Union";
19.94
19.95 -Goal
19.96 - "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
19.97 -\ |] ==> wf(r Un s)";
19.98 +Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
19.99 +\ |] ==> wf(r Un s)";
19.100 br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
19.101 by(Blast_tac 1);
19.102 by(Blast_tac 1);
19.103 @@ -251,10 +247,9 @@
19.104 eresolve_tac [transD, mp, allE]));
19.105 val wf_super_ss = HOL_ss addSolver indhyp_tac;
19.106
19.107 -val prems = goalw WF.thy [is_recfun_def,cut_def]
19.108 +Goalw [is_recfun_def,cut_def]
19.109 "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \
19.110 \ (x,a):r --> (x,b):r --> f(x)=g(x)";
19.111 -by (cut_facts_tac prems 1);
19.112 by (etac wf_induct 1);
19.113 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
19.114 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
19.115 @@ -274,15 +269,13 @@
19.116
19.117 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
19.118
19.119 -val prems = goalw WF.thy [the_recfun_def]
19.120 +Goalw [the_recfun_def]
19.121 "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
19.122 -by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
19.123 -by (resolve_tac prems 1);
19.124 +by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
19.125 qed "is_the_recfun";
19.126
19.127 -val prems = goal WF.thy
19.128 - "!!r. [| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
19.129 -by (wf_ind_tac "a" prems 1);
19.130 +Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
19.131 +by (wf_ind_tac "a" [] 1);
19.132 by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
19.133 is_the_recfun 1);
19.134 by (rewtac is_recfun_def);
19.135 @@ -309,7 +302,7 @@
19.136 val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
19.137
19.138 (*--------------Old proof-----------------------------------------------------
19.139 -val prems = goal WF.thy
19.140 +val prems = Goal
19.141 "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
19.142 by (cut_facts_tac prems 1);
19.143 by (wf_ind_tac "a" prems 1);
19.144 @@ -376,7 +369,7 @@
19.145 (*---------------------------------------------------------------------------
19.146 * This form avoids giant explosions in proofs. NOTE USE OF ==
19.147 *---------------------------------------------------------------------------*)
19.148 -val rew::prems = goal WF.thy
19.149 +val rew::prems = goal thy
19.150 "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a";
19.151 by (rewtac rew);
19.152 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
20.1 --- a/src/HOL/arith_data.ML Thu Aug 13 18:07:56 1998 +0200
20.2 +++ b/src/HOL/arith_data.ML Thu Aug 13 18:14:26 1998 +0200
20.3 @@ -56,7 +56,7 @@
20.4 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
20.5
20.6 fun prove_conv expand_tac norm_tac sg (t, u) =
20.7 - meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
20.8 + meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
20.9 (K [expand_tac, norm_tac]))
20.10 handle ERROR => error ("The error(s) above occurred while trying to prove " ^
20.11 (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
21.1 --- a/src/HOL/equalities.ML Thu Aug 13 18:07:56 1998 +0200
21.2 +++ b/src/HOL/equalities.ML Thu Aug 13 18:14:26 1998 +0200
21.3 @@ -136,7 +136,7 @@
21.4 qed "if_image_distrib";
21.5 Addsimps[if_image_distrib];
21.6
21.7 -val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
21.8 +val prems= Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
21.9 by (rtac set_ext 1);
21.10 by (simp_tac (simpset() addsimps image_def::prems) 1);
21.11 qed "image_cong";
21.12 @@ -212,10 +212,6 @@
21.13 by (Blast_tac 1);
21.14 qed "Int_Un_distrib2";
21.15
21.16 -Goal "(A<=B) = (A Int B = A)";
21.17 -by (blast_tac (claset() addSEs [equalityCE]) 1);
21.18 -qed "subset_Int_eq";
21.19 -
21.20 Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
21.21 by (blast_tac (claset() addEs [equalityCE]) 1);
21.22 qed "Int_UNIV";
22.1 --- a/src/HOL/mono.ML Thu Aug 13 18:07:56 1998 +0200
22.2 +++ b/src/HOL/mono.ML Thu Aug 13 18:14:26 1998 +0200
22.3 @@ -6,96 +6,96 @@
22.4 Monotonicity of various operations
22.5 *)
22.6
22.7 -goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
22.8 +Goal "A<=B ==> f``A <= f``B";
22.9 by (Blast_tac 1);
22.10 qed "image_mono";
22.11
22.12 -goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
22.13 +Goal "A<=B ==> Pow(A) <= Pow(B)";
22.14 by (Blast_tac 1);
22.15 qed "Pow_mono";
22.16
22.17 -goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
22.18 +Goal "A<=B ==> Union(A) <= Union(B)";
22.19 by (Blast_tac 1);
22.20 qed "Union_mono";
22.21
22.22 -goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
22.23 +Goal "B<=A ==> Inter(A) <= Inter(B)";
22.24 by (Blast_tac 1);
22.25 qed "Inter_anti_mono";
22.26
22.27 -val prems = goal Set.thy
22.28 +val prems = Goal
22.29 "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
22.30 \ (UN x:A. f(x)) <= (UN x:B. g(x))";
22.31 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
22.32 qed "UN_mono";
22.33
22.34 (*The last inclusion is POSITIVE! *)
22.35 -val prems = goal Set.thy
22.36 +val prems = Goal
22.37 "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
22.38 \ (INT x:A. f(x)) <= (INT x:A. g(x))";
22.39 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
22.40 qed "INT_anti_mono";
22.41
22.42 -goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
22.43 +Goal "C<=D ==> insert a C <= insert a D";
22.44 by (Blast_tac 1);
22.45 qed "insert_mono";
22.46
22.47 -goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D";
22.48 +Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D";
22.49 by (Blast_tac 1);
22.50 qed "Un_mono";
22.51
22.52 -goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D";
22.53 +Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D";
22.54 by (Blast_tac 1);
22.55 qed "Int_mono";
22.56
22.57 -goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
22.58 +Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
22.59 by (Blast_tac 1);
22.60 qed "Diff_mono";
22.61
22.62 -goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
22.63 +Goal "A<=B ==> Compl(B) <= Compl(A)";
22.64 by (Blast_tac 1);
22.65 qed "Compl_anti_mono";
22.66
22.67 (** Monotonicity of implications. For inductive definitions **)
22.68
22.69 -goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
22.70 +Goal "A<=B ==> x:A --> x:B";
22.71 by (rtac impI 1);
22.72 by (etac subsetD 1);
22.73 by (assume_tac 1);
22.74 qed "in_mono";
22.75
22.76 -goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
22.77 +Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
22.78 by (Blast_tac 1);
22.79 qed "conj_mono";
22.80
22.81 -goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
22.82 +Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
22.83 by (Blast_tac 1);
22.84 qed "disj_mono";
22.85
22.86 -goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
22.87 +Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
22.88 by (Blast_tac 1);
22.89 qed "imp_mono";
22.90
22.91 -goal HOL.thy "P-->P";
22.92 +Goal "P-->P";
22.93 by (rtac impI 1);
22.94 by (assume_tac 1);
22.95 qed "imp_refl";
22.96
22.97 -val [PQimp] = goal HOL.thy
22.98 +val [PQimp] = Goal
22.99 "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
22.100 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
22.101 qed "ex_mono";
22.102
22.103 -val [PQimp] = goal HOL.thy
22.104 +val [PQimp] = Goal
22.105 "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
22.106 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
22.107 qed "all_mono";
22.108
22.109 -val [PQimp] = goal Set.thy
22.110 +val [PQimp] = Goal
22.111 "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
22.112 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
22.113 qed "Collect_mono";
22.114
22.115 -val [subs,PQimp] = goal Set.thy
22.116 +val [subs,PQimp] = Goal
22.117 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
22.118 \ |] ==> A Int Collect(P) <= B Int Collect(Q)";
22.119 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
23.1 --- a/src/HOL/subset.ML Thu Aug 13 18:07:56 1998 +0200
23.2 +++ b/src/HOL/subset.ML Thu Aug 13 18:14:26 1998 +0200
23.3 @@ -12,32 +12,28 @@
23.4 qed_goal "subset_insertI" Set.thy "B <= insert a B"
23.5 (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
23.6
23.7 -goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
23.8 +Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
23.9 by (Blast_tac 1);
23.10 qed "subset_insert";
23.11
23.12 (*** Big Union -- least upper bound of a set ***)
23.13
23.14 -val prems = goal Set.thy
23.15 - "B:A ==> B <= Union(A)";
23.16 -by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
23.17 +Goal "B:A ==> B <= Union(A)";
23.18 +by (REPEAT (ares_tac [subsetI,UnionI] 1));
23.19 qed "Union_upper";
23.20
23.21 -val [prem] = goal Set.thy
23.22 - "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
23.23 +val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
23.24 by (rtac subsetI 1);
23.25 by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
23.26 qed "Union_least";
23.27
23.28 (** General union **)
23.29
23.30 -val prems = goal Set.thy
23.31 - "a:A ==> B(a) <= (UN x:A. B(x))";
23.32 -by (REPEAT (ares_tac (prems@[UN_I RS subsetI]) 1));
23.33 +Goal "a:A ==> B(a) <= (UN x:A. B(x))";
23.34 +by (Blast_tac 1);
23.35 qed "UN_upper";
23.36
23.37 -val [prem] = goal Set.thy
23.38 - "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
23.39 +val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
23.40 by (rtac subsetI 1);
23.41 by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
23.42 qed "UN_least";
23.43 @@ -45,52 +41,49 @@
23.44
23.45 (*** Big Intersection -- greatest lower bound of a set ***)
23.46
23.47 -goal Set.thy "!!B. B:A ==> Inter(A) <= B";
23.48 +Goal "B:A ==> Inter(A) <= B";
23.49 by (Blast_tac 1);
23.50 qed "Inter_lower";
23.51
23.52 -val [prem] = goal Set.thy
23.53 - "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
23.54 +val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
23.55 by (rtac (InterI RS subsetI) 1);
23.56 by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
23.57 qed "Inter_greatest";
23.58
23.59 -val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)";
23.60 -by (rtac subsetI 1);
23.61 -by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1));
23.62 +Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
23.63 +by (Blast_tac 1);
23.64 qed "INT_lower";
23.65
23.66 -val [prem] = goal Set.thy
23.67 - "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
23.68 +val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
23.69 by (rtac (INT_I RS subsetI) 1);
23.70 by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
23.71 qed "INT_greatest";
23.72
23.73 (*** Finite Union -- the least upper bound of 2 sets ***)
23.74
23.75 -goal Set.thy "A <= A Un B";
23.76 +Goal "A <= A Un B";
23.77 by (Blast_tac 1);
23.78 qed "Un_upper1";
23.79
23.80 -goal Set.thy "B <= A Un B";
23.81 +Goal "B <= A Un B";
23.82 by (Blast_tac 1);
23.83 qed "Un_upper2";
23.84
23.85 -goal Set.thy "!!C. [| A<=C; B<=C |] ==> A Un B <= C";
23.86 +Goal "[| A<=C; B<=C |] ==> A Un B <= C";
23.87 by (Blast_tac 1);
23.88 qed "Un_least";
23.89
23.90 (*** Finite Intersection -- the greatest lower bound of 2 sets *)
23.91
23.92 -goal Set.thy "A Int B <= A";
23.93 +Goal "A Int B <= A";
23.94 by (Blast_tac 1);
23.95 qed "Int_lower1";
23.96
23.97 -goal Set.thy "A Int B <= B";
23.98 +Goal "A Int B <= B";
23.99 by (Blast_tac 1);
23.100 qed "Int_lower2";
23.101
23.102 -goal Set.thy "!!C. [| C<=A; C<=B |] ==> C <= A Int B";
23.103 +Goal "[| C<=A; C<=B |] ==> C <= A Int B";
23.104 by (Blast_tac 1);
23.105 qed "Int_greatest";
23.106
23.107 @@ -101,14 +94,14 @@
23.108
23.109 (*** Monotonicity ***)
23.110
23.111 -val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
23.112 +Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
23.113 by (rtac Un_least 1);
23.114 -by (rtac (Un_upper1 RS (prem RS monoD)) 1);
23.115 -by (rtac (Un_upper2 RS (prem RS monoD)) 1);
23.116 +by (etac (Un_upper1 RSN (2,monoD)) 1);
23.117 +by (etac (Un_upper2 RSN (2,monoD)) 1);
23.118 qed "mono_Un";
23.119
23.120 -val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
23.121 +Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
23.122 by (rtac Int_greatest 1);
23.123 -by (rtac (Int_lower1 RS (prem RS monoD)) 1);
23.124 -by (rtac (Int_lower2 RS (prem RS monoD)) 1);
23.125 +by (etac (Int_lower1 RSN (2,monoD)) 1);
23.126 +by (etac (Int_lower2 RSN (2,monoD)) 1);
23.127 qed "mono_Int";