tidied

--- a/src/HOL/Algebra/abstract/Ideal.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -226,31 +226,31 @@
 (* Divisor chain condition *)
 (* proofs not finished *)
 
-Goal "(ALL i. I i <= I (Suc i)) --> (n <= m & a : I n --> a : I m)";
-by (rtac impI 1);
-by (nat_ind_tac "m" 1);
+Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)";
+by (induct_tac "m" 1);
 by (Blast_tac 1);
 (* induction step *)
+by (rename_tac "m" 1);
 by (case_tac "n <= m" 1);
 by Auto_tac;
 by (subgoal_tac "n = Suc m" 1);
-by (hyp_subst_tac 1);
-by Auto_tac;
-qed "subset_chain_lemma";
+by (arith_tac 2);
+by (Force_tac 1);
+qed_spec_mp "subset_chain_lemma";
 
-Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] ==> \
-\    is_ideal (Union (I``UNIV))";
+Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
+\     ==> is_ideal (Union (I``UNIV))";
 by (rtac is_idealI 1);
 by Auto_tac;
 by (res_inst_tac [("x", "max x xa")] exI 1);
 by (rtac is_ideal_add 1);
 by (Asm_simp_tac 1);
-by (rtac (subset_chain_lemma RS mp RS mp) 1);
+by (rtac subset_chain_lemma 1);
 by (assume_tac 1);
 by (rtac conjI 1);
 by (assume_tac 2);
 by (arith_tac 1);
-by (rtac (subset_chain_lemma RS mp RS mp) 1);
+by (rtac subset_chain_lemma 1);
 by (assume_tac 1);
 by (rtac conjI 1);
 by (assume_tac 2);

--- a/src/HOL/Algebra/abstract/NatSum.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/abstract/NatSum.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -19,7 +19,7 @@
 
 Goal
   "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -51,7 +51,7 @@
 section "Ring Properties";
 
 Goal "SUM n (%i. <0>) = (<0>::'a::ring)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "SUM_zero";
@@ -60,7 +60,7 @@
 
 Goal
   "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -69,7 +69,7 @@
 
 Goal
   "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -78,7 +78,7 @@
 
 Goal
   "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -97,7 +97,7 @@
   "!!a::nat=>'a::ring. k <= n --> \
 \  SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
 \  SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 (* Base case *)
 by (simp_tac (simpset() addsimps [m_assoc]) 1);
 (* Induction step *)
@@ -135,7 +135,7 @@
 Goal
   "!! a::nat=>'a::ring. j <= n --> \
 \    SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
-by (nat_ind_tac "j" 1);
+by (induct_tac "j" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -160,7 +160,7 @@
 Goal
   "!! f::(nat=>'a::ring). \
 \    SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
@@ -174,20 +174,17 @@
   "!! f::(nat=>'a::ring). \
 \    m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \
 \    SUM m f = SUM n f";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (case_tac "m <= n" 1);
 by (rtac impI 1);
 by (etac impE 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 by (etac conjE 1);
 by (dres_inst_tac [("x", "Suc n")] spec 1);
-by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
-(* case n < m, in fact m = Suc n *)
-by (rtac impI 1);
-by (etac conjE 1);
+by Auto_tac;
 by (subgoal_tac "m = Suc n" 1);
 by (Asm_simp_tac 1);
 by (fast_arith_tac 1);
@@ -212,16 +209,11 @@
 Goal
   "!! f::(nat=>'a::ring). \
 \    (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";
-by (nat_ind_tac "d" 1);
+by (induct_tac "d" 1);
 (* Base case *)
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (Simp_tac 1);
-by (rtac impI 1);
-by (etac impE 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "SUM m f = <0>" 1);
-by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
+by (Force_tac 1);
 (* Induction step *)
 by (asm_simp_tac (simpset() addsimps add_ac) 1);
 val SUM_shrink_below_lemma = result();
@@ -230,8 +222,8 @@
   "!! f::(nat=>'a::ring). \
 \    [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \
 \    P (SUM n f)";
-by (asm_full_simp_tac (simpset() addsimps
-  [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
+by (asm_full_simp_tac 
+    (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
 qed "SUM_extend_below";
 
 section "Result for the Univeral Property of Polynomials";
@@ -240,7 +232,7 @@
   "!!f::nat=>'a::ring. j <= n + m --> \
 \    SUM j (%k. SUM k (%i. f i * g (k - i))) = \
 \    SUM j (%k. SUM (j - k) (%i. f k * g i))";
-by (nat_ind_tac "j" 1);
+by (induct_tac "j" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)

--- a/src/HOL/Algebra/abstract/Ring.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -176,22 +176,20 @@
 Addsimps [power_0, power_Suc];
 
 Goal "<1> ^ n = (<1>::'a::ring)";
-by (nat_ind_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
 qed "power_one";
 
 Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)";
 by (etac rev_mp 1);
-by (nat_ind_tac "n" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
 qed "power_zero";
 
 Addsimps [power_zero, power_one];
 
 Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps m_ac) 1);
 qed "power_mult";

--- a/src/HOL/Algebra/abstract/RingHomo.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/abstract/RingHomo.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -39,7 +39,7 @@
 qed "homo_uminus";
 
 Goal "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (dtac homo_one 1);
 by (Asm_simp_tac 1);
 by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
@@ -48,7 +48,7 @@
 
 Goal
   "!! f::('a::ring=>'b::ring). homo f ==> f (SUM n g) = SUM n (f o g)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (Simp_tac 1);
 by (dres_inst_tac [("a", "g (Suc n)"), ("b", "SUM n g")] homo_add 1);

--- a/src/HOL/Algebra/poly/Degree.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/poly/Degree.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -272,11 +272,8 @@
 
 goal PolyRing.thy
   "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))";
-by (nat_ind_tac "n" 1);
-(* Base case *)
-by (Simp_tac 1);
-(* Induction step *)
-by (Asm_simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
 qed "coeff_SUM";
 
 goal UnivPoly.thy
@@ -284,8 +281,8 @@
 \    bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x";
 by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
 by (auto_tac
-  (claset() addDs [not_leE],
-   simpset()));
+    (claset() addDs [not_leE],
+     simpset()));
 qed "bound_SUM_if";
 
 Goal
@@ -331,12 +328,11 @@
 by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
 by (Asm_simp_tac 1);
 by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1);
-by (SELECT_GOAL (auto_tac (claset() addIs [up_eqI], simpset())) 1);
+by (force_tac (claset() addIs [up_eqI], simpset()) 1);
 by (rtac integral 1);
 by (subgoal_tac "coeff 0 (p * q) = <0>" 1);
+by (Asm_simp_tac 2);
 by (Full_simp_tac 1);
-by (Asm_simp_tac 1);
-
 by (dres_inst_tac [("f", "deg")] arg_cong 1);
 by (Asm_full_simp_tac 1);
 qed "up_integral";

--- a/src/HOL/Algebra/poly/LongDiv.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -77,7 +77,7 @@
   by (rtac add_le_mono1 1);
   by (rtac deg_smult_ring 1);
   by (asm_simp_tac (simpset() addsimps [leI]) 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 by (Simp_tac 1);
 by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
 by (Simp_tac 1);
@@ -156,18 +156,18 @@
 (* r1 = <0> *)
 by (etac disjE 1);
 (* r2 = <0> *)
-by (SELECT_GOAL (auto_tac (claset() addDs [integral], simpset())) 1);
+by (force_tac (claset() addDs [integral], simpset()) 1);
 (* r2 ~= <0> *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 (* r1 ~=<0> *)
 by (etac disjE 1);
 (* r2 = <0> *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 (* r2 ~= <0> *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Asm_full_simp_tac 1);
 by (dtac (order_eq_refl RS add_leD2) 1);
 by (dtac leD 1);
 by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);

--- a/src/HOL/Algebra/poly/PolyHomo.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -81,9 +81,8 @@
 Goalw [EVAL2_def]
   "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1);  (* really a case split *)
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by (case_tac "n" 1); 
+by Auto_tac;
 qed "EVAL2_monom";
 
 Goal

--- a/src/HOL/Algebra/poly/UnivPoly.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -8,46 +8,33 @@
 (* Closure of UP under +, *s, monom, const and * *)
 
 Goalw [UP_def]
-  "!! f g. [| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
-by (Step_tac 1);
+  "[| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
+by Auto_tac;
 (* instantiate bound for the sum and do case split *)
 by (res_inst_tac [("x", "if n<=na then na else n")] exI 1);
-by (case_tac "n <= na" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 2);
+by Auto_tac;
 (* first case, bound of g higher *)
-by (etac (make_elim le_bound) 1 THEN atac 1);
-by (REPEAT (Step_tac 1));
-by (Asm_simp_tac 1);
+by (dtac le_bound 1 THEN assume_tac 1);
+by (Force_tac 1);
 (* second case is identical,
   apart from we have to massage the inequality *)
 by (dtac (not_leE RS less_imp_le) 1);
-by (etac (make_elim le_bound) 1 THEN atac 1);
-by (REPEAT (Step_tac 1));
-by (Asm_simp_tac 1);
+by (dtac le_bound 1 THEN assume_tac 1);
+by (Force_tac 1);
 qed "UP_closed_add";
 
 Goalw [UP_def]
-  "!! f. f : UP ==> (%n. (a * f n::'a::ring)) : UP";
-by (REPEAT (Step_tac 1));
-by (Asm_simp_tac 1);
+  "f : UP ==> (%n. (a * f n::'a::ring)) : UP";
+by (Force_tac 1);
 qed "UP_closed_smult";
 
 Goalw [UP_def]
-  "!! m. (%n. if m = n then <1> else <0>) : UP";
-by (Step_tac 1);
-by (res_inst_tac [("x", "m")] exI 1);
-by (Step_tac 1);
-by (dtac (less_not_refl2 RS not_sym) 1);
-by (Asm_simp_tac 1);
+  "(%n. if m = n then <1> else <0>) : UP";
+by Auto_tac;
 qed "UP_closed_monom";
 
-Goalw [UP_def]
-  "!! a. (%n. if n = 0 then a else <0>) : UP";
-by (Step_tac 1);
-by (res_inst_tac [("x", "0")] exI 1);
-by (rtac boundI 1);
-by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
+Goalw [UP_def] "(%n. if n = 0 then a else <0>) : UP";
+by Auto_tac;
 qed "UP_closed_const";
 
 Goal
@@ -56,21 +43,15 @@
 (* Case split: either f i or g (k - i) is zero *)
 by (case_tac "n<i" 1);
 (* First case, f i is zero *)
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 (* Second case, we have to derive m < k-i *)
 by (subgoal_tac "m < k-i" 1);
-by (SELECT_GOAL Auto_tac 1);
-(* More inequalities, quite nasty *)
-by (rtac add_less_imp_less_diff 1);
-by (stac add_commute 1);
-by (dtac leI 1);
-by (rtac le_less_trans 1);
-by (assume_tac 2);
-by (asm_simp_tac (simpset() addsimps [add_le_mono1]) 1);
+by (arith_tac 2);
+by (Force_tac 1);
 qed "bound_mult_zero";
 
 Goalw [UP_def]
-  "!! f g. [| f : UP; g : UP |] ==> \
+  "[| f : UP; g : UP |] ==> \
 \      (%n. (SUM n (%i. f i * g (n-i))::'a::ring)) : UP";
 by (Step_tac 1);
 (* Instantiate bound for the product, and remove bound in goal *)
@@ -118,7 +99,7 @@
 qed "coeff_zero";
 
 Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const, 
-  coeff_mult, coeff_zero];
+	  coeff_mult, coeff_zero];
 
 Goalw [up_one_def]
   "coeff n <1> = (if n=0 then <1> else <0>)";
@@ -133,17 +114,16 @@
 
 (* Polynomials form a ring *)
 
-Goalw [coeff_def]
-  "!! p q. [| !! n. coeff n p = coeff n q |] ==> p = q";
+val prems = Goalw [coeff_def]
+  "(!! n. coeff n p = coeff n q) ==> p = q";
 by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1);
 by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1);
-by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "up_eqI";
 
 Goalw [coeff_def]
-  "!! p q. coeff n p ~= coeff n q ==> p ~= q";
-by (etac contrapos 1);
-by (Asm_simp_tac 1);
+  "coeff n p ~= coeff n q ==> p ~= q";
+by Auto_tac;
 qed "up_neqI";
 
 Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)";
@@ -177,11 +157,11 @@
 Goal "!! a::('a::ring) up. <1> * a = a";
 by (rtac up_eqI 1);
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1); (* this is only a case split *)
-(* Base case *)
-by (Simp_tac 1);
-(* Induction step *)
-by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
+by (case_tac "n" 1); 
+(* 0 case *)
+by (Asm_simp_tac 1);
+(* Suc case *)
+by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
 qed "up_l_one";
 
 Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c";
@@ -205,9 +185,9 @@
 
 Goal "!! a::'a::ring. const a * p = a *s p";
 by (rtac up_eqI 1);
-by (nat_ind_tac "n" 1);  (* really only a case split *)
-by (Simp_tac 1);
-by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
+by (case_tac "n" 1); 
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
 qed "const_mult_is_smult";
 
 Goal "!! a::'a::ring. const (a + b) = const a + const b";
@@ -238,7 +218,7 @@
 by (strip_tac 1);
 by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1);
 by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const,
-  expand_fun_eq]) 1);
+				       expand_fun_eq]) 1);
 by (dres_inst_tac [("x", "0")] spec 1);
 by (Full_simp_tac 1);
 qed "const_inj";
@@ -252,11 +232,10 @@
 by (simp_tac (simpset() addsimps [SUM_rdistr]) 1);
 by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
 by (rtac le_add1 1);
-by (SELECT_GOAL Auto_tac 1);
+by (Force_tac 1);
 by (rtac SUM_cong 1);
 by (rtac refl 1);
 by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
 by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
-by (SELECT_GOAL Auto_tac 1);
-by (rtac refl 1);
+by Auto_tac;
 qed "CauchySum";

--- a/src/HOL/UNITY/Token.ML	Thu Apr 13 15:11:41 2000 +0200
+++ b/src/HOL/UNITY/Token.ML	Thu Apr 13 15:16:32 2000 +0200
@@ -50,20 +50,12 @@
 
 Goalw [nodeOrder_def, next_def, inv_image_def]
     "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
-by (auto_tac (claset(),
-	      simpset() addsimps [Suc_lessI, mod_Suc, mod_geq]));
-by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le,
-                                      diff_add_assoc]) 2);
-by (full_simp_tac (simpset() addsimps [linorder_neq_iff]) 1);
-by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
+by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
 by (auto_tac (claset(), 
-              simpset() addsimps [diff_add_assoc2, linorder_neq_iff, 
-                                  Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, 
-                                  add_diff_less, mod_geq]));
+              simpset() addsplits [nat_diff_split']
+                        addsimps [linorder_neq_iff, mod_geq]));
 qed "nodeOrder_eq";
 
-
 (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
 Goal "[| i<N; j<N |] ==>   \