removal of DO_GOAL
authorpaulson
Fri Jan 08 13:20:59 1999 +0100 (1999-01-08)
changeset 60711b2392ac5752
parent 6070 032babd0120b
child 6072 5583261db33d
removal of DO_GOAL
src/ZF/Epsilon.ML
src/ZF/ROOT.ML
src/ZF/Univ.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/Primrec_defs.thy
     1.1 --- a/src/ZF/Epsilon.ML	Thu Jan 07 18:30:55 1999 +0100
     1.2 +++ b/src/ZF/Epsilon.ML	Fri Jan 08 13:20:59 1999 +0100
     1.3 @@ -185,6 +185,7 @@
     1.4  by (etac bspec 1);
     1.5  by (assume_tac 1);
     1.6  qed "Ord_rank";
     1.7 +Addsimps [Ord_rank];
     1.8  
     1.9  val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
    1.10  by (rtac (major RS trans_induct) 1);
    1.11 @@ -195,8 +196,8 @@
    1.12  Goal "a:b ==> rank(a) < rank(b)";
    1.13  by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
    1.14  by (etac (UN_I RS ltI) 1);
    1.15 -by (rtac succI1 1);
    1.16 -by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
    1.17 +by (rtac Ord_UN 2);
    1.18 +by Auto_tac;
    1.19  qed "rank_lt";
    1.20  
    1.21  val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
    1.22 @@ -210,17 +211,15 @@
    1.23  by (rtac subset_imp_le 1);
    1.24  by (stac rank 1);
    1.25  by (stac rank 1);
    1.26 -by (etac UN_mono 1);
    1.27 -by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
    1.28 +by Auto_tac;
    1.29  qed "rank_mono";
    1.30  
    1.31  Goal "rank(Pow(a)) = succ(rank(a))";
    1.32  by (rtac (rank RS trans) 1);
    1.33  by (rtac le_anti_sym 1);
    1.34 -by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
    1.35 -             etac (PowD RS rank_mono RS succ_leI)] 1);
    1.36 -by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
    1.37 -             REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
    1.38 +br UN_upper_le 2;
    1.39 +br UN_least_le 1;
    1.40 +by (auto_tac (claset() addIs [rank_mono], simpset()));
    1.41  qed "rank_Pow";
    1.42  
    1.43  Goal "rank(0) = 0";
     2.1 --- a/src/ZF/ROOT.ML	Thu Jan 07 18:30:55 1999 +0100
     2.2 +++ b/src/ZF/ROOT.ML	Fri Jan 08 13:20:59 1999 +0100
     2.3 @@ -13,20 +13,6 @@
     2.4  
     2.5  eta_contract:=false;
     2.6  
     2.7 -(*For Pure/tactic??  A crude way of adding structure to rules*)
     2.8 -fun CHECK_SOLVED tac st =
     2.9 -    case Seq.pull (tac st) of
    2.10 -        None => error"DO_GOAL: tactic list failed"
    2.11 -      | Some(x,_) => 
    2.12 -                if has_fewer_prems 1 x then
    2.13 -                    Seq.cons(x, Seq.empty)
    2.14 -                else (writeln"DO_GOAL: unsolved goals!!";
    2.15 -                      writeln"Final proof state was ...";
    2.16 -                      print_goals (!goals_limit) x;
    2.17 -                      raise ERROR);
    2.18 -
    2.19 -fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    2.20 -
    2.21  print_depth 1;
    2.22  
    2.23  (*Add user sections for inductive/datatype definitions*)
     3.1 --- a/src/ZF/Univ.ML	Thu Jan 07 18:30:55 1999 +0100
     3.2 +++ b/src/ZF/Univ.ML	Fri Jan 08 13:20:59 1999 +0100
     3.3 @@ -324,7 +324,7 @@
     3.4  by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
     3.5  by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
     3.6  by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
     3.7 -by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
     3.8 +by (blast_tac (claset() addIs [Limit_VfromI, limiti]) 5);
     3.9  by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
    3.10  by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
    3.11  by (rtac (succI1 RS UnI2) 2);
     4.1 --- a/src/ZF/ex/Primrec.ML	Thu Jan 07 18:30:55 1999 +0100
     4.2 +++ b/src/ZF/ex/Primrec.ML	Fri Jan 08 13:20:59 1999 +0100
     4.3 @@ -22,7 +22,7 @@
     4.4  simpset_ref() := simpset() setSolver (type_auto_tac ([prim_rec_into_fun] @ 
     4.5  					      pr_typechecks @ prim_rec.intrs));
     4.6  
     4.7 -Goalw [ACK_def] "i:nat ==> ACK(i): prim_rec";
     4.8 +Goal "i:nat ==> ACK(i): prim_rec";
     4.9  by (induct_tac "i" 1);
    4.10  by (ALLGOALS Asm_simp_tac);
    4.11  qed "ACK_in_prim_rec";
    4.12 @@ -32,35 +32,34 @@
    4.13       add_type, list_add_type, nat_into_Ord] @ 
    4.14      nat_typechecks @ list.intrs @ prim_rec.intrs;
    4.15  
    4.16 -(*strict typechecking for the Ackermann proof; instantiates no vars*)
    4.17 -fun tc_tac rls =
    4.18 -    REPEAT
    4.19 -      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
    4.20 +simpset_ref() := simpset() setSolver (type_auto_tac ack_typechecks);
    4.21  
    4.22  Goal "[| i:nat;  j:nat |] ==>  ack(i,j): nat";
    4.23 -by (tc_tac []);
    4.24 +by Auto_tac;
    4.25  qed "ack_type";
    4.26 +Addsimps [ack_type];
    4.27  
    4.28  (** Ackermann's function cases **)
    4.29  
    4.30  (*PROPERTY A 1*)
    4.31 -Goalw [ACK_def] "j:nat ==> ack(0,j) = succ(j)";
    4.32 +Goal "j:nat ==> ack(0,j) = succ(j)";
    4.33  by (asm_simp_tac (simpset() addsimps [SC]) 1);
    4.34  qed "ack_0";
    4.35  
    4.36  (*PROPERTY A 2*)
    4.37 -Goalw [ACK_def] "ack(succ(i), 0) = ack(i,1)";
    4.38 +Goal "ack(succ(i), 0) = ack(i,1)";
    4.39  by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1);
    4.40  qed "ack_succ_0";
    4.41  
    4.42  (*PROPERTY A 3*)
    4.43 -Goalw [ACK_def]
    4.44 -    "[| i:nat;  j:nat |] ==> \
    4.45 -\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
    4.46 +Goal "[| i:nat;  j:nat |]  \
    4.47 +\     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
    4.48  by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
    4.49  qed "ack_succ_succ";
    4.50  
    4.51  Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type, nat_into_Ord];
    4.52 +Delsimps [ACK_0, ACK_succ];
    4.53 +
    4.54  
    4.55  (*PROPERTY A 4*)
    4.56  Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
    4.57 @@ -68,10 +67,9 @@
    4.58  by (Asm_simp_tac 1);
    4.59  by (rtac ballI 1);
    4.60  by (induct_tac "j" 1);
    4.61 -by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
    4.62 -             Asm_simp_tac] 1);
    4.63 -by (DO_GOAL [etac (succ_leI RS lt_trans1),
    4.64 -             Asm_simp_tac] 1);
    4.65 +by (etac (succ_leI RS lt_trans1) 2);
    4.66 +by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
    4.67 +by Auto_tac;
    4.68  qed "lt_ack2_lemma";
    4.69  bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
    4.70  
    4.71 @@ -146,7 +144,7 @@
    4.72  by (Asm_simp_tac 1);
    4.73  by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
    4.74  by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
    4.75 -by (tc_tac []);
    4.76 +by Auto_tac;
    4.77  qed "ack_nest_bound";
    4.78  
    4.79  (*PROPERTY A 11*)
    4.80 @@ -186,7 +184,7 @@
    4.81  by (induct_tac "i" 1);
    4.82  by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
    4.83  by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
    4.84 -by (tc_tac []);
    4.85 +by Auto_tac;
    4.86  qed "lt_ack1";
    4.87  
    4.88  Goalw [CONST_def]
    4.89 @@ -206,7 +204,7 @@
    4.90  by (Asm_simp_tac 1);
    4.91  by (etac (bspec RS lt_trans2) 1);
    4.92  by (rtac (add_le_self2 RS succ_leI) 2);
    4.93 -by (tc_tac []);
    4.94 +by Auto_tac;
    4.95  qed "PROJ_case_lemma";
    4.96  val PROJ_case = PROJ_case_lemma RS bspec;
    4.97  
    4.98 @@ -218,16 +216,14 @@
    4.99  \      ==> EX k:nat. ALL l: list(nat).                          \
   4.100  \                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
   4.101  by (etac list.induct 1);
   4.102 -by (DO_GOAL [res_inst_tac [("x","0")] bexI,
   4.103 -             asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]),
   4.104 -             resolve_tac nat_typechecks] 1);
   4.105 -by Safe_tac;
   4.106 -by (Asm_simp_tac 1);
   4.107 +by (res_inst_tac [("x","0")] bexI 1);
   4.108 +by (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]) 1);
   4.109 +by Auto_tac;
   4.110  by (rtac (ballI RS bexI) 1);
   4.111  by (rtac (add_lt_mono RS lt_trans) 1);
   4.112  by (REPEAT (FIRSTGOAL (etac bspec)));
   4.113  by (rtac ack_add_bound 5);
   4.114 -by (tc_tac []);
   4.115 +by Auto_tac;
   4.116  qed "COMP_map_lemma";
   4.117  
   4.118  Goalw [COMP_def]
   4.119 @@ -245,7 +241,7 @@
   4.120  by (rtac lt_trans 2);
   4.121  by (rtac ack_nest_bound 3);
   4.122  by (etac (bspec RS ack_lt_mono2) 2);
   4.123 -by (tc_tac [map_type]);
   4.124 +by Auto_tac;
   4.125  qed "COMP_case";
   4.126  
   4.127  (** PREC case **)
   4.128 @@ -263,22 +259,23 @@
   4.129  by (etac ssubst 1);  (*get rid of the needless assumption*)
   4.130  by (induct_tac "a" 1);
   4.131  (*base case*)
   4.132 -by (DO_GOAL [Asm_simp_tac, rtac lt_trans, etac bspec,
   4.133 +by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
   4.134               assume_tac, rtac (add_le_self RS ack_lt_mono1),
   4.135 -             REPEAT o ares_tac (ack_typechecks)] 1);
   4.136 +             REPEAT o ares_tac (ack_typechecks)]);
   4.137  (*ind step*)
   4.138  by (Asm_simp_tac 1);
   4.139  by (rtac (succ_leI RS lt_trans1) 1);
   4.140  by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
   4.141  by (etac bspec 2);
   4.142  by (rtac (nat_le_refl RS add_le_mono) 1);
   4.143 -by (tc_tac []);
   4.144 +	(*Auto_tac is a little slow*)
   4.145 +by (TRYALL (type_auto_tac ack_typechecks []));
   4.146  by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
   4.147  (*final part of the simplification*)
   4.148  by (Asm_simp_tac 1);
   4.149  by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
   4.150  by (etac ack_lt_mono2 5);
   4.151 -by (tc_tac []);
   4.152 +by Auto_tac;
   4.153  qed "PREC_case_lemma";
   4.154  
   4.155  Goal "[| f: prim_rec;  kf: nat;                               \
     5.1 --- a/src/ZF/ex/Primrec_defs.thy	Thu Jan 07 18:30:55 1999 +0100
     5.2 +++ b/src/ZF/ex/Primrec_defs.thy	Fri Jan 08 13:20:59 1999 +0100
     5.3 @@ -38,8 +38,9 @@
     5.4              lam l:list(nat). list_case(0, 
     5.5                        %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
     5.6    
     5.7 -  ACK_def   "ACK(i) == rec(i, SC, 
     5.8 -                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
     5.9 -
    5.10 +primrec
    5.11 +  ACK_0     "ACK(0) = SC"
    5.12 +  ACK_succ  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
    5.13 +				  COMP(ACK(i), [PROJ(0)]))"
    5.14  
    5.15  end