# HG changeset patch
# User paulson
# Date 915798059 -3600
# Node ID 1b2392ac575237639c07a77c60ce5ac630a93bed
# Parent  032babd0120b0e43d52e2699f6816677ae0d0a31
removal of DO_GOAL

diff -r 032babd0120b -r 1b2392ac5752 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/Epsilon.ML	Fri Jan 08 13:20:59 1999 +0100
@@ -185,6 +185,7 @@
 by (etac bspec 1);
 by (assume_tac 1);
 qed "Ord_rank";
+Addsimps [Ord_rank];
 
 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
 by (rtac (major RS trans_induct) 1);
@@ -195,8 +196,8 @@
 Goal "a:b ==> rank(a) < rank(b)";
 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
 by (etac (UN_I RS ltI) 1);
-by (rtac succI1 1);
-by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
+by (rtac Ord_UN 2);
+by Auto_tac;
 qed "rank_lt";
 
 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
@@ -210,17 +211,15 @@
 by (rtac subset_imp_le 1);
 by (stac rank 1);
 by (stac rank 1);
-by (etac UN_mono 1);
-by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
+by Auto_tac;
 qed "rank_mono";
 
 Goal "rank(Pow(a)) = succ(rank(a))";
 by (rtac (rank RS trans) 1);
 by (rtac le_anti_sym 1);
-by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
-             etac (PowD RS rank_mono RS succ_leI)] 1);
-by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
-             REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
+br UN_upper_le 2;
+br UN_least_le 1;
+by (auto_tac (claset() addIs [rank_mono], simpset()));
 qed "rank_Pow";
 
 Goal "rank(0) = 0";
diff -r 032babd0120b -r 1b2392ac5752 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/ROOT.ML	Fri Jan 08 13:20:59 1999 +0100
@@ -13,20 +13,6 @@
 
 eta_contract:=false;
 
-(*For Pure/tactic??  A crude way of adding structure to rules*)
-fun CHECK_SOLVED tac st =
-    case Seq.pull (tac st) of
-        None => error"DO_GOAL: tactic list failed"
-      | Some(x,_) => 
-                if has_fewer_prems 1 x then
-                    Seq.cons(x, Seq.empty)
-                else (writeln"DO_GOAL: unsolved goals!!";
-                      writeln"Final proof state was ...";
-                      print_goals (!goals_limit) x;
-                      raise ERROR);
-
-fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
-
 print_depth 1;
 
 (*Add user sections for inductive/datatype definitions*)
diff -r 032babd0120b -r 1b2392ac5752 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/Univ.ML	Fri Jan 08 13:20:59 1999 +0100
@@ -324,7 +324,7 @@
 by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
 by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
 by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
-by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
+by (blast_tac (claset() addIs [Limit_VfromI, limiti]) 5);
 by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
 by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
 by (rtac (succI1 RS UnI2) 2);
diff -r 032babd0120b -r 1b2392ac5752 src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/ex/Primrec.ML	Fri Jan 08 13:20:59 1999 +0100
@@ -22,7 +22,7 @@
 simpset_ref() := simpset() setSolver (type_auto_tac ([prim_rec_into_fun] @ 
 					      pr_typechecks @ prim_rec.intrs));
 
-Goalw [ACK_def] "i:nat ==> ACK(i): prim_rec";
+Goal "i:nat ==> ACK(i): prim_rec";
 by (induct_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ACK_in_prim_rec";
@@ -32,35 +32,34 @@
      add_type, list_add_type, nat_into_Ord] @ 
     nat_typechecks @ list.intrs @ prim_rec.intrs;
 
-(*strict typechecking for the Ackermann proof; instantiates no vars*)
-fun tc_tac rls =
-    REPEAT
-      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
+simpset_ref() := simpset() setSolver (type_auto_tac ack_typechecks);
 
 Goal "[| i:nat;  j:nat |] ==>  ack(i,j): nat";
-by (tc_tac []);
+by Auto_tac;
 qed "ack_type";
+Addsimps [ack_type];
 
 (** Ackermann's function cases **)
 
 (*PROPERTY A 1*)
-Goalw [ACK_def] "j:nat ==> ack(0,j) = succ(j)";
+Goal "j:nat ==> ack(0,j) = succ(j)";
 by (asm_simp_tac (simpset() addsimps [SC]) 1);
 qed "ack_0";
 
 (*PROPERTY A 2*)
-Goalw [ACK_def] "ack(succ(i), 0) = ack(i,1)";
+Goal "ack(succ(i), 0) = ack(i,1)";
 by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1);
 qed "ack_succ_0";
 
 (*PROPERTY A 3*)
-Goalw [ACK_def]
-    "[| i:nat;  j:nat |] ==> \
-\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
+Goal "[| i:nat;  j:nat |]  \
+\     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
 by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
 qed "ack_succ_succ";
 
 Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type, nat_into_Ord];
+Delsimps [ACK_0, ACK_succ];
+
 
 (*PROPERTY A 4*)
 Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
@@ -68,10 +67,9 @@
 by (Asm_simp_tac 1);
 by (rtac ballI 1);
 by (induct_tac "j" 1);
-by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
-             Asm_simp_tac] 1);
-by (DO_GOAL [etac (succ_leI RS lt_trans1),
-             Asm_simp_tac] 1);
+by (etac (succ_leI RS lt_trans1) 2);
+by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
+by Auto_tac;
 qed "lt_ack2_lemma";
 bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
 
@@ -146,7 +144,7 @@
 by (Asm_simp_tac 1);
 by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
 by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
-by (tc_tac []);
+by Auto_tac;
 qed "ack_nest_bound";
 
 (*PROPERTY A 11*)
@@ -186,7 +184,7 @@
 by (induct_tac "i" 1);
 by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
 by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
-by (tc_tac []);
+by Auto_tac;
 qed "lt_ack1";
 
 Goalw [CONST_def]
@@ -206,7 +204,7 @@
 by (Asm_simp_tac 1);
 by (etac (bspec RS lt_trans2) 1);
 by (rtac (add_le_self2 RS succ_leI) 2);
-by (tc_tac []);
+by Auto_tac;
 qed "PROJ_case_lemma";
 val PROJ_case = PROJ_case_lemma RS bspec;
 
@@ -218,16 +216,14 @@
 \      ==> EX k:nat. ALL l: list(nat).                          \
 \                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
 by (etac list.induct 1);
-by (DO_GOAL [res_inst_tac [("x","0")] bexI,
-             asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]),
-             resolve_tac nat_typechecks] 1);
-by Safe_tac;
-by (Asm_simp_tac 1);
+by (res_inst_tac [("x","0")] bexI 1);
+by (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]) 1);
+by Auto_tac;
 by (rtac (ballI RS bexI) 1);
 by (rtac (add_lt_mono RS lt_trans) 1);
 by (REPEAT (FIRSTGOAL (etac bspec)));
 by (rtac ack_add_bound 5);
-by (tc_tac []);
+by Auto_tac;
 qed "COMP_map_lemma";
 
 Goalw [COMP_def]
@@ -245,7 +241,7 @@
 by (rtac lt_trans 2);
 by (rtac ack_nest_bound 3);
 by (etac (bspec RS ack_lt_mono2) 2);
-by (tc_tac [map_type]);
+by Auto_tac;
 qed "COMP_case";
 
 (** PREC case **)
@@ -263,22 +259,23 @@
 by (etac ssubst 1);  (*get rid of the needless assumption*)
 by (induct_tac "a" 1);
 (*base case*)
-by (DO_GOAL [Asm_simp_tac, rtac lt_trans, etac bspec,
+by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
              assume_tac, rtac (add_le_self RS ack_lt_mono1),
-             REPEAT o ares_tac (ack_typechecks)] 1);
+             REPEAT o ares_tac (ack_typechecks)]);
 (*ind step*)
 by (Asm_simp_tac 1);
 by (rtac (succ_leI RS lt_trans1) 1);
 by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
 by (etac bspec 2);
 by (rtac (nat_le_refl RS add_le_mono) 1);
-by (tc_tac []);
+	(*Auto_tac is a little slow*)
+by (TRYALL (type_auto_tac ack_typechecks []));
 by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
 (*final part of the simplification*)
 by (Asm_simp_tac 1);
 by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
 by (etac ack_lt_mono2 5);
-by (tc_tac []);
+by Auto_tac;
 qed "PREC_case_lemma";
 
 Goal "[| f: prim_rec;  kf: nat;                               \
diff -r 032babd0120b -r 1b2392ac5752 src/ZF/ex/Primrec_defs.thy
--- a/src/ZF/ex/Primrec_defs.thy	Thu Jan 07 18:30:55 1999 +0100
+++ b/src/ZF/ex/Primrec_defs.thy	Fri Jan 08 13:20:59 1999 +0100
@@ -38,8 +38,9 @@
             lam l:list(nat). list_case(0, 
                       %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   
-  ACK_def   "ACK(i) == rec(i, SC, 
-                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
-
+primrec
+  ACK_0     "ACK(0) = SC"
+  ACK_succ  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
+				  COMP(ACK(i), [PROJ(0)]))"
 
 end