new typechecking solver for the simplifier
authorpaulson
Wed Jan 27 10:31:31 1999 +0100 (1999-01-27)
changeset 6153bff90585cce5
parent 6152 bc1e27bcc195
child 6154 6a00a5baef2b
new typechecking solver for the simplifier
src/ZF/AC/Cardinal_aux.ML
src/ZF/AC/WO6_WO1.ML
src/ZF/Arith.ML
src/ZF/Bool.ML
src/ZF/CardinalArith.ML
src/ZF/Cardinal_AC.ML
src/ZF/Integ/Bin.ML
src/ZF/Integ/Bin.thy
src/ZF/Integ/EquivClass.ML
src/ZF/Integ/Int.ML
src/ZF/List.ML
src/ZF/Nat.ML
src/ZF/Order.ML
src/ZF/OrderType.ML
src/ZF/Ordinal.ML
src/ZF/Perm.ML
src/ZF/ROOT.ML
src/ZF/Sum.ML
src/ZF/Tools/typechk.ML
src/ZF/ex/BinEx.ML
src/ZF/ex/Limit.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/Primrec_defs.ML
src/ZF/ex/TF.ML
src/ZF/ex/Term.ML
src/ZF/func.ML
src/ZF/pair.ML
src/ZF/simpdata.ML
src/ZF/upair.ML
src/ZF/upair.thy
     1.1 --- a/src/ZF/AC/Cardinal_aux.ML	Mon Jan 25 20:35:19 1999 +0100
     1.2 +++ b/src/ZF/AC/Cardinal_aux.ML	Wed Jan 27 10:31:31 1999 +0100
     1.3 @@ -142,8 +142,7 @@
     1.4  by (rtac impE 1 THEN (assume_tac 3));
     1.5  by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2 
     1.6          THEN (TRYALL assume_tac));
     1.7 -by (Simp_tac 2);
     1.8 -by (Asm_full_simp_tac 1);
     1.9 +by Auto_tac;
    1.10  qed "UN_lepoll";
    1.11  
    1.12  Goal "Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))";
     2.1 --- a/src/ZF/AC/WO6_WO1.ML	Mon Jan 25 20:35:19 1999 +0100
     2.2 +++ b/src/ZF/AC/WO6_WO1.ML	Wed Jan 27 10:31:31 1999 +0100
     2.3 @@ -8,8 +8,6 @@
     2.4  pages 2-5
     2.5  *)
     2.6  
     2.7 -open WO6_WO1;
     2.8 -
     2.9  goal OrderType.thy 
    2.10        "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==>  \
    2.11  \                  k < i  |  (~ k<i & k = i ++ (k--i) & (k--i)<j)";
    2.12 @@ -143,7 +141,7 @@
    2.13  by (Blast_tac 1);
    2.14  by (rtac vv1_subset 1);
    2.15  by (dtac (ospec RS mp) 1);
    2.16 -by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
    2.17 +by (REPEAT (eresolve_tac [asm_rl, oexE, conjE] 1));
    2.18  by (asm_simp_tac (simpset()
    2.19          addsimps [vv1_def, Let_def, lt_Ord, 
    2.20                    nested_Least_instance RS conjunct1]) 1);
     3.1 --- a/src/ZF/Arith.ML	Mon Jan 25 20:35:19 1999 +0100
     3.2 +++ b/src/ZF/Arith.ML	Wed Jan 27 10:31:31 1999 +0100
     3.3 @@ -35,6 +35,7 @@
     3.4  by Auto_tac;
     3.5  qed "add_type";
     3.6  Addsimps [add_type];
     3.7 +AddTCs [add_type];
     3.8  
     3.9  (** Multiplication **)
    3.10  
    3.11 @@ -43,6 +44,7 @@
    3.12  by Auto_tac;
    3.13  qed "mult_type";
    3.14  Addsimps [mult_type];
    3.15 +AddTCs [mult_type];
    3.16  
    3.17  
    3.18  (** Difference **)
    3.19 @@ -53,6 +55,7 @@
    3.20  by (fast_tac (claset() addIs [nat_case_type]) 1);
    3.21  qed "diff_type";
    3.22  Addsimps [diff_type];
    3.23 +AddTCs [diff_type];
    3.24  
    3.25  Goal "n:nat ==> 0 #- n = 0";
    3.26  by (induct_tac "n" 1);
    3.27 @@ -288,6 +291,7 @@
    3.28  Goalw [mod_def] "[| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
    3.29  by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
    3.30  qed "mod_type";
    3.31 +AddTCs [mod_type];
    3.32  
    3.33  Goal "[| 0<n;  m<n |] ==> m mod n = m";
    3.34  by (rtac (mod_def RS def_transrec RS trans) 1);
    3.35 @@ -309,6 +313,7 @@
    3.36      "[| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
    3.37  by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
    3.38  qed "div_type";
    3.39 +AddTCs [div_type];
    3.40  
    3.41  Goal "[| 0<n;  m<n |] ==> m div n = 0";
    3.42  by (rtac (div_def RS def_transrec RS trans) 1);
     4.1 --- a/src/ZF/Bool.ML	Mon Jan 25 20:35:19 1999 +0100
     4.2 +++ b/src/ZF/Bool.ML	Wed Jan 27 10:31:31 1999 +0100
     4.3 @@ -6,8 +6,6 @@
     4.4  Booleans in Zermelo-Fraenkel Set Theory 
     4.5  *)
     4.6  
     4.7 -open Bool;
     4.8 -
     4.9  val bool_defs = [bool_def,cond_def];
    4.10  
    4.11  Goalw [succ_def] "{0} = 1";
    4.12 @@ -25,6 +23,7 @@
    4.13  qed "bool_0I";
    4.14  
    4.15  Addsimps [bool_1I, bool_0I];
    4.16 +AddTCs   [bool_1I, bool_0I];
    4.17  
    4.18  Goalw bool_defs "1~=0";
    4.19  by (rtac succ_not_0 1);
    4.20 @@ -59,12 +58,12 @@
    4.21  Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    4.22  by (bool_tac 1);
    4.23  qed "cond_type";
    4.24 +AddTCs [cond_type];
    4.25  
    4.26  (*For Simp_tac and Blast_tac*)
    4.27  Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
    4.28  by (bool_tac 1);
    4.29  qed "cond_simple_type";
    4.30 -Addsimps [cond_simple_type];
    4.31  
    4.32  val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    4.33  by (rewtac rew);
    4.34 @@ -85,25 +84,25 @@
    4.35  
    4.36  Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
    4.37  
    4.38 -qed_goalw "not_type" Bool.thy [not_def]
    4.39 -    "a:bool ==> not(a) : bool"
    4.40 - (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    4.41 +Goalw [not_def] "a:bool ==> not(a) : bool";
    4.42 +by (Asm_simp_tac 1);
    4.43 +qed "not_type";
    4.44  
    4.45 -qed_goalw "and_type" Bool.thy [and_def]
    4.46 -    "[| a:bool;  b:bool |] ==> a and b : bool"
    4.47 - (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    4.48 +Goalw [and_def] "[| a:bool;  b:bool |] ==> a and b : bool";
    4.49 +by (Asm_simp_tac 1);
    4.50 +qed "and_type";
    4.51  
    4.52 -qed_goalw "or_type" Bool.thy [or_def]
    4.53 -    "[| a:bool;  b:bool |] ==> a or b : bool"
    4.54 - (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    4.55 +Goalw [or_def] "[| a:bool;  b:bool |] ==> a or b : bool";
    4.56 +by (Asm_simp_tac 1);
    4.57 +qed "or_type";
    4.58  
    4.59 -Addsimps [not_type, and_type, or_type];
    4.60 +AddTCs [not_type, and_type, or_type];
    4.61  
    4.62 -qed_goalw "xor_type" Bool.thy [xor_def]
    4.63 -    "[| a:bool;  b:bool |] ==> a xor b : bool"
    4.64 - (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
    4.65 +Goalw [xor_def] "[| a:bool;  b:bool |] ==> a xor b : bool";
    4.66 +by (Asm_simp_tac 1);
    4.67 +qed "xor_type";
    4.68  
    4.69 -Addsimps [xor_type];
    4.70 +AddTCs [xor_type];
    4.71  
    4.72  val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
    4.73                         or_type, xor_type];
     5.1 --- a/src/ZF/CardinalArith.ML	Mon Jan 25 20:35:19 1999 +0100
     5.2 +++ b/src/ZF/CardinalArith.ML	Wed Jan 27 10:31:31 1999 +0100
     5.3 @@ -11,8 +11,6 @@
     5.4  coincide with union (maximum).  Either way we get most laws for free.
     5.5  *)
     5.6  
     5.7 -open CardinalArith;
     5.8 -
     5.9  (*** Cardinal addition ***)
    5.10  
    5.11  (** Cardinal addition is commutative **)
    5.12 @@ -65,7 +63,7 @@
    5.13  
    5.14  Goalw [lepoll_def, inj_def] "A lepoll A+B";
    5.15  by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1);
    5.16 -by (asm_simp_tac (simpset() addsimps [lam_type]) 1);
    5.17 +by (Asm_simp_tac 1);
    5.18  qed "sum_lepoll_self";
    5.19  
    5.20  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    5.21 @@ -86,7 +84,7 @@
    5.22  by (res_inst_tac 
    5.23        [("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")] 
    5.24        lam_injective 1);
    5.25 -by (typechk_tac ([inj_is_fun, case_type, InlI, InrI] @ ZF_typechecks));
    5.26 +by (typecheck_tac (tcset() addTCs [inj_is_fun]));
    5.27  by (etac sumE 1);
    5.28  by (ALLGOALS (asm_simp_tac (simpset() addsimps [left_inverse])));
    5.29  qed "sum_lepoll_mono";
    5.30 @@ -216,7 +214,7 @@
    5.31  
    5.32  Goalw [lepoll_def, inj_def] "A lepoll A*A";
    5.33  by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1);
    5.34 -by (simp_tac (simpset() addsimps [lam_type]) 1);
    5.35 +by (Simp_tac 1);
    5.36  qed "prod_square_lepoll";
    5.37  
    5.38  (*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
    5.39 @@ -233,7 +231,7 @@
    5.40  
    5.41  Goalw [lepoll_def, inj_def] "b: B ==> A lepoll A*B";
    5.42  by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1);
    5.43 -by (asm_simp_tac (simpset() addsimps [lam_type]) 1);
    5.44 +by (Asm_simp_tac 1);
    5.45  qed "prod_lepoll_self";
    5.46  
    5.47  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    5.48 @@ -252,7 +250,7 @@
    5.49  by (res_inst_tac [("x", "lam <w,y>:A*B. <f`w, fa`y>")] exI 1);
    5.50  by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")] 
    5.51                    lam_injective 1);
    5.52 -by (typechk_tac (inj_is_fun::ZF_typechecks));
    5.53 +by (typecheck_tac (tcset() addTCs [inj_is_fun]));
    5.54  by (etac SigmaE 1);
    5.55  by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
    5.56  qed "prod_lepoll_mono";
    5.57 @@ -295,7 +293,7 @@
    5.58  
    5.59  Goal "Card(n) ==> 2 |*| n = n |+| n";
    5.60  by (asm_simp_tac 
    5.61 -    (simpset() addsimps [Ord_0, Ord_succ, cmult_succ_lemma, Card_is_Ord,
    5.62 +    (simpset() addsimps [cmult_succ_lemma, Card_is_Ord,
    5.63  			 read_instantiate [("j","0")] cadd_commute]) 1);
    5.64  qed "cmult_2";
    5.65  
    5.66 @@ -552,7 +550,7 @@
    5.67  (*Corollary 10.13 (1), for cardinal multiplication*)
    5.68  Goal "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L";
    5.69  by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
    5.70 -by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
    5.71 +by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord]));
    5.72  by (resolve_tac [cmult_commute RS ssubst] 1);
    5.73  by (resolve_tac [Un_commute RS ssubst] 1);
    5.74  by (ALLGOALS
    5.75 @@ -561,13 +559,12 @@
    5.76  			  subset_Un_iff2 RS iffD1, le_imp_subset])));
    5.77  qed "InfCard_cmult_eq";
    5.78  
    5.79 -(*This proof appear to be the simplest!*)
    5.80  Goal "InfCard(K) ==> K |+| K = K";
    5.81  by (asm_simp_tac
    5.82      (simpset() addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1);
    5.83 -by (rtac InfCard_le_cmult_eq 1);
    5.84 -by (typechk_tac [Ord_0, le_refl, leI]);
    5.85 -by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]);
    5.86 +by (asm_simp_tac 
    5.87 +    (simpset() addsimps [InfCard_le_cmult_eq, InfCard_is_Limit, 
    5.88 +			 Limit_has_0, Limit_has_succ]) 1);
    5.89  qed "InfCard_cdouble_eq";
    5.90  
    5.91  (*Corollary 10.13 (1), for cardinal addition*)
    5.92 @@ -582,7 +579,7 @@
    5.93  
    5.94  Goal "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L";
    5.95  by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
    5.96 -by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
    5.97 +by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord]));
    5.98  by (resolve_tac [cadd_commute RS ssubst] 1);
    5.99  by (resolve_tac [Un_commute RS ssubst] 1);
   5.100  by (ALLGOALS
     6.1 --- a/src/ZF/Cardinal_AC.ML	Mon Jan 25 20:35:19 1999 +0100
     6.2 +++ b/src/ZF/Cardinal_AC.ML	Wed Jan 27 10:31:31 1999 +0100
     6.3 @@ -8,8 +8,6 @@
     6.4  These results help justify infinite-branching datatypes
     6.5  *)
     6.6  
     6.7 -open Cardinal_AC;
     6.8 -
     6.9  (*** Strengthened versions of existing theorems about cardinals ***)
    6.10  
    6.11  Goal "|A| eqpoll A";
    6.12 @@ -118,19 +116,21 @@
    6.13  by (subgoal_tac
    6.14      "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
    6.15  by (fast_tac (claset() addSIs [Least_le RS lt_trans1 RS ltD, ltI]
    6.16 -                      addSEs [LeastI, Ord_in_Ord]) 2);
    6.17 +                       addSEs [LeastI, Ord_in_Ord]) 2);
    6.18  by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
    6.19                    ("d", "%<i,j>. converse(f`i) ` j")] 
    6.20          lam_injective 1);
    6.21  (*Instantiate the lemma proved above*)
    6.22  by (ALLGOALS ball_tac);
    6.23  by (blast_tac (claset() addIs [inj_is_fun RS apply_type]
    6.24 -                       addDs [apply_type]) 1);
    6.25 +                        addDs [apply_type]) 1);
    6.26  by (dtac apply_type 1);
    6.27  by (etac conjunct2 1);
    6.28  by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
    6.29  qed "cardinal_UN_le";
    6.30  
    6.31 +
    6.32 +
    6.33  (*The same again, using csucc*)
    6.34  Goal "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
    6.35  \         |UN i:K. X(i)| < csucc(K)";
     7.1 --- a/src/ZF/Integ/Bin.ML	Mon Jan 25 20:35:19 1999 +0100
     7.2 +++ b/src/ZF/Integ/Bin.ML	Wed Jan 27 10:31:31 1999 +0100
     7.3 @@ -7,18 +7,17 @@
     7.4  *)
     7.5  
     7.6  
     7.7 -Addsimps bin.intrs;
     7.8 -Addsimps int_typechecks;
     7.9 +AddTCs bin.intrs;
    7.10  
    7.11  Goal "NCons(Pls,0) = Pls";
    7.12  by (Asm_simp_tac 1);
    7.13  qed "NCons_Pls_0";
    7.14  
    7.15 -Goal "NCons(Pls,1) = Cons(Pls,1)";
    7.16 +Goal "NCons(Pls,1) = Pls BIT 1";
    7.17  by (Asm_simp_tac 1);
    7.18  qed "NCons_Pls_1";
    7.19  
    7.20 -Goal "NCons(Min,0) = Cons(Min,0)";
    7.21 +Goal "NCons(Min,0) = Min BIT 0";
    7.22  by (Asm_simp_tac 1);
    7.23  qed "NCons_Min_0";
    7.24  
    7.25 @@ -26,49 +25,47 @@
    7.26  by (Asm_simp_tac 1);
    7.27  qed "NCons_Min_1";
    7.28  
    7.29 -Goal "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
    7.30 +Goal "NCons(w BIT x,b) = w BIT x BIT b";
    7.31  by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
    7.32 -qed "NCons_Cons";
    7.33 +qed "NCons_BIT";
    7.34  
    7.35  val NCons_simps = [NCons_Pls_0, NCons_Pls_1, 
    7.36  		   NCons_Min_0, NCons_Min_1,
    7.37 -		   NCons_Cons];
    7.38 +		   NCons_BIT];
    7.39  Addsimps NCons_simps;
    7.40  
    7.41  
    7.42  (** Type checking **)
    7.43  
    7.44 -Addsimps [bool_into_nat];
    7.45 -
    7.46  Goal "w: bin ==> integ_of(w) : int";
    7.47  by (induct_tac "w" 1);
    7.48 -by (ALLGOALS (Asm_simp_tac));
    7.49 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [bool_into_nat])));
    7.50  qed "integ_of_type";
    7.51 -Addsimps [integ_of_type];
    7.52 +AddTCs [integ_of_type];
    7.53  
    7.54  Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
    7.55  by (induct_tac "w" 1);
    7.56  by Auto_tac;
    7.57  qed "NCons_type";
    7.58 -Addsimps [NCons_type];
    7.59 +AddTCs [NCons_type];
    7.60  
    7.61  Goal "w: bin ==> bin_succ(w) : bin";
    7.62  by (induct_tac "w" 1);
    7.63  by Auto_tac;
    7.64  qed "bin_succ_type";
    7.65 -Addsimps [bin_succ_type];
    7.66 +AddTCs [bin_succ_type];
    7.67  
    7.68  Goal "w: bin ==> bin_pred(w) : bin";
    7.69  by (induct_tac "w" 1);
    7.70  by Auto_tac;
    7.71  qed "bin_pred_type";
    7.72 -Addsimps [bin_pred_type];
    7.73 +AddTCs [bin_pred_type];
    7.74  
    7.75  Goal "w: bin ==> bin_minus(w) : bin";
    7.76  by (induct_tac "w" 1);
    7.77  by Auto_tac;
    7.78  qed "bin_minus_type";
    7.79 -Addsimps [bin_minus_type];
    7.80 +AddTCs [bin_minus_type];
    7.81  
    7.82  (*This proof is complicated by the mutual recursion*)
    7.83  Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
    7.84 @@ -76,22 +73,22 @@
    7.85  by (rtac ballI 3);
    7.86  by (rename_tac "w'" 3);
    7.87  by (induct_tac "w'" 3);
    7.88 -by Auto_tac;
    7.89 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [NCons_type])));
    7.90  qed_spec_mp "bin_add_type";
    7.91 -Addsimps [bin_add_type];
    7.92 +AddTCs [bin_add_type];
    7.93  
    7.94  Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
    7.95  by (induct_tac "v" 1);
    7.96  by Auto_tac;
    7.97  qed "bin_mult_type";
    7.98 -Addsimps [bin_mult_type];
    7.99 +AddTCs [bin_mult_type];
   7.100  
   7.101  
   7.102  (**** The carry/borrow functions, bin_succ and bin_pred ****)
   7.103  
   7.104  (*NCons preserves the integer value of its argument*)
   7.105  Goal "[| w: bin; b: bool |] ==>     \
   7.106 -\         integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
   7.107 +\         integ_of(NCons(w,b)) = integ_of(w BIT b)";
   7.108  by (etac bin.elim 1);
   7.109  by (Asm_simp_tac 3);
   7.110  by (ALLGOALS (etac boolE));
   7.111 @@ -130,8 +127,6 @@
   7.112      (asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib])));
   7.113  qed "integ_of_minus";
   7.114  
   7.115 -Addsimps [integ_of_minus];
   7.116 -
   7.117  
   7.118  (*** bin_add: binary addition ***)
   7.119  
   7.120 @@ -143,22 +138,22 @@
   7.121  by (Asm_simp_tac 1);
   7.122  qed "bin_add_Min";
   7.123  
   7.124 -Goal "bin_add(Cons(v,x),Pls) = Cons(v,x)";
   7.125 +Goal "bin_add(v BIT x,Pls) = v BIT x";
   7.126  by (Simp_tac 1);
   7.127 -qed "bin_add_Cons_Pls";
   7.128 +qed "bin_add_BIT_Pls";
   7.129  
   7.130 -Goal "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
   7.131 +Goal "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
   7.132  by (Simp_tac 1);
   7.133 -qed "bin_add_Cons_Min";
   7.134 +qed "bin_add_BIT_Min";
   7.135  
   7.136  Goal "[| w: bin;  y: bool |]              \
   7.137 -\     ==> bin_add(Cons(v,x), Cons(w,y)) = \
   7.138 +\     ==> bin_add(v BIT x, w BIT y) = \
   7.139  \         NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
   7.140  by (Asm_simp_tac 1);
   7.141 -qed "bin_add_Cons_Cons";
   7.142 +qed "bin_add_BIT_BIT";
   7.143  
   7.144 -Addsimps [bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
   7.145 -	  bin_add_Cons_Min, bin_add_Cons_Cons,
   7.146 +Addsimps [bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
   7.147 +	  bin_add_BIT_Min, bin_add_BIT_BIT,
   7.148  	  integ_of_succ, integ_of_pred];
   7.149  
   7.150  Goal "v: bin ==> \
   7.151 @@ -170,7 +165,6 @@
   7.152  by (induct_tac "wa" 1);
   7.153  by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
   7.154  qed_spec_mp "integ_of_add";
   7.155 -Addsimps [integ_of_add];
   7.156  
   7.157  
   7.158  (*** bin_add: binary multiplication ***)
   7.159 @@ -179,87 +173,90 @@
   7.160  \     ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
   7.161  by (induct_tac "v" 1);
   7.162  by (Asm_simp_tac 1);
   7.163 -by (Asm_simp_tac 1);
   7.164 +by (asm_simp_tac (simpset() addsimps [integ_of_minus]) 1);
   7.165  by (etac boolE 1);
   7.166  by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
   7.167 -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1);
   7.168 +by (asm_simp_tac (simpset() addsimps [integ_of_add,
   7.169 +				      zadd_zmult_distrib] @ zadd_ac) 1);
   7.170  qed "integ_of_mult";
   7.171  
   7.172  (**** Computations ****)
   7.173  
   7.174  (** extra rules for bin_succ, bin_pred **)
   7.175  
   7.176 -Goal "bin_succ(Cons(w,1)) = Cons(bin_succ(w), 0)";
   7.177 +Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
   7.178  by (Simp_tac 1);
   7.179 -qed "bin_succ_Cons1";
   7.180 +qed "bin_succ_BIT1";
   7.181  
   7.182 -Goal "bin_succ(Cons(w,0)) = NCons(w,1)";
   7.183 +Goal "bin_succ(w BIT 0) = NCons(w,1)";
   7.184  by (Simp_tac 1);
   7.185 -qed "bin_succ_Cons0";
   7.186 +qed "bin_succ_BIT0";
   7.187  
   7.188 -Goal "bin_pred(Cons(w,1)) = NCons(w,0)";
   7.189 +Goal "bin_pred(w BIT 1) = NCons(w,0)";
   7.190  by (Simp_tac 1);
   7.191 -qed "bin_pred_Cons1";
   7.192 +qed "bin_pred_BIT1";
   7.193  
   7.194 -Goal "bin_pred(Cons(w,0)) = Cons(bin_pred(w), 1)";
   7.195 +Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
   7.196  by (Simp_tac 1);
   7.197 -qed "bin_pred_Cons0";
   7.198 +qed "bin_pred_BIT0";
   7.199  
   7.200  (** extra rules for bin_minus **)
   7.201  
   7.202 -Goal "bin_minus(Cons(w,1)) = bin_pred(NCons(bin_minus(w), 0))";
   7.203 +Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
   7.204  by (Simp_tac 1);
   7.205 -qed "bin_minus_Cons1";
   7.206 +qed "bin_minus_BIT1";
   7.207  
   7.208 -Goal "bin_minus(Cons(w,0)) = Cons(bin_minus(w), 0)";
   7.209 +Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
   7.210  by (Simp_tac 1);
   7.211 -qed "bin_minus_Cons0";
   7.212 +qed "bin_minus_BIT0";
   7.213  
   7.214  (** extra rules for bin_add **)
   7.215  
   7.216 -Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,1)) = \
   7.217 +Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
   7.218  \                    NCons(bin_add(v, bin_succ(w)), 0)";
   7.219  by (Asm_simp_tac 1);
   7.220 -qed "bin_add_Cons_Cons11";
   7.221 +qed "bin_add_BIT_BIT11";
   7.222  
   7.223 -Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,0)) =  \
   7.224 +Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) =  \
   7.225  \                    NCons(bin_add(v,w), 1)";
   7.226  by (Asm_simp_tac 1);
   7.227 -qed "bin_add_Cons_Cons10";
   7.228 +qed "bin_add_BIT_BIT10";
   7.229  
   7.230  Goal "[| w: bin;  y: bool |] ==> \
   7.231 -\           bin_add(Cons(v,0), Cons(w,y)) = NCons(bin_add(v,w), y)";
   7.232 +\           bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
   7.233  by (Asm_simp_tac 1);
   7.234 -qed "bin_add_Cons_Cons0";
   7.235 +qed "bin_add_BIT_BIT0";
   7.236  
   7.237  (** extra rules for bin_mult **)
   7.238  
   7.239 -Goal "bin_mult(Cons(v,1), w) = bin_add(NCons(bin_mult(v,w),0), w)";
   7.240 +Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
   7.241  by (Simp_tac 1);
   7.242 -qed "bin_mult_Cons1";
   7.243 +qed "bin_mult_BIT1";
   7.244  
   7.245 -Goal "bin_mult(Cons(v,0), w) = NCons(bin_mult(v,w),0)";
   7.246 +Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
   7.247  by (Simp_tac 1);
   7.248 -qed "bin_mult_Cons0";
   7.249 +qed "bin_mult_BIT0";
   7.250  
   7.251  
   7.252 -(*** The computation simpset ***)
   7.253 +(*Delete the original rewrites, with their clumsy conditional expressions*)
   7.254 +Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   7.255 +          NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
   7.256 +
   7.257 +(*Hide the binary representation of integer constants*)
   7.258 +Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
   7.259 +
   7.260  
   7.261 -(*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
   7.262 -val bin_comp_ss = simpset_of Int.thy 
   7.263 -    addsimps [integ_of_add RS sym,   (*invoke bin_add*)
   7.264 -              integ_of_minus RS sym, (*invoke bin_minus*)
   7.265 -              integ_of_mult RS sym,  (*invoke bin_mult*)
   7.266 -              bin_succ_Pls, bin_succ_Min,
   7.267 -              bin_succ_Cons1, bin_succ_Cons0,
   7.268 -              bin_pred_Pls, bin_pred_Min,
   7.269 -              bin_pred_Cons1, bin_pred_Cons0,
   7.270 -              bin_minus_Pls, bin_minus_Min,
   7.271 -              bin_minus_Cons1, bin_minus_Cons0,
   7.272 -              bin_add_Pls, bin_add_Min, bin_add_Cons_Pls, 
   7.273 -              bin_add_Cons_Min, bin_add_Cons_Cons0, 
   7.274 -              bin_add_Cons_Cons10, bin_add_Cons_Cons11,
   7.275 -              bin_mult_Pls, bin_mult_Min,
   7.276 -              bin_mult_Cons1, bin_mult_Cons0]
   7.277 -             @ NCons_simps
   7.278 -    setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin.intrs));
   7.279 +Addsimps [integ_of_add RS sym,   (*invoke bin_add*)
   7.280 +	  integ_of_minus RS sym, (*invoke bin_minus*)
   7.281 +	  integ_of_mult RS sym,  (*invoke bin_mult*)
   7.282 +	  bin_succ_Pls, bin_succ_Min,
   7.283 +	  bin_succ_BIT1, bin_succ_BIT0,
   7.284 +	  bin_pred_Pls, bin_pred_Min,
   7.285 +	  bin_pred_BIT1, bin_pred_BIT0,
   7.286 +	  bin_minus_Pls, bin_minus_Min,
   7.287 +	  bin_minus_BIT1, bin_minus_BIT0,
   7.288 +	  bin_add_Pls, bin_add_Min, bin_add_BIT_Pls, 
   7.289 +	  bin_add_BIT_Min, bin_add_BIT_BIT0, 
   7.290 +	  bin_add_BIT_BIT10, bin_add_BIT_BIT11,
   7.291 +	  bin_mult_Pls, bin_mult_Min,
   7.292 +	  bin_mult_BIT1, bin_mult_BIT0];
     8.1 --- a/src/ZF/Integ/Bin.thy	Mon Jan 25 20:35:19 1999 +0100
     8.2 +++ b/src/ZF/Integ/Bin.thy	Wed Jan 27 10:31:31 1999 +0100
     8.3 @@ -24,7 +24,7 @@
     8.4  datatype
     8.5    "bin" = Pls
     8.6          | Min
     8.7 -        | Cons ("w: bin", "b: bool")
     8.8 +        | BIT ("w: bin", "b: bool")	(infixl 90)
     8.9  
    8.10  syntax
    8.11    "_Int"           :: xnum => i        ("_")
    8.12 @@ -40,60 +40,59 @@
    8.13    bin_mult  :: [i,i]=>i
    8.14  
    8.15  primrec
    8.16 -  "integ_of (Pls)       = $# 0"
    8.17 -  "integ_of (Min)       = $~($#1)"
    8.18 -  "integ_of (Cons(w,b)) = $#b $+ integ_of(w) $+ integ_of(w)"
    8.19 +  integ_of_Pls  "integ_of (Pls)     = $# 0"
    8.20 +  integ_of_Min  "integ_of (Min)     = $~($#1)"
    8.21 +  integ_of_BIT  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
    8.22  
    8.23      (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
    8.24  
    8.25  primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
    8.26 -  "NCons (Pls,b)       = cond(b,Cons(Pls,b),Pls)"
    8.27 -  "NCons (Min,b)       = cond(b,Min,Cons(Min,b))"
    8.28 -  "NCons (Cons(w,c),b) = Cons(Cons(w,c),b)"
    8.29 +  NCons_Pls "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
    8.30 +  NCons_Min "NCons (Min,b)     = cond(b,Min,Min BIT b)"
    8.31 +  NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
    8.32  
    8.33 -primrec (*successor.  If a Cons, can change a 0 to a 1 without recursion.*)
    8.34 -  bin_succ_Pls
    8.35 -    "bin_succ (Pls)       = Cons(Pls,1)"
    8.36 -  bin_succ_Min
    8.37 -    "bin_succ (Min)       = Pls"
    8.38 -      "bin_succ (Cons(w,b)) = cond(b, Cons(bin_succ(w), 0),
    8.39 -				    NCons(w,1))"
    8.40 +primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
    8.41 +  bin_succ_Pls  "bin_succ (Pls)     = Pls BIT 1"
    8.42 +  bin_succ_Min  "bin_succ (Min)     = Pls"
    8.43 +  bin_succ_BIT  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
    8.44  
    8.45  primrec (*predecessor*)
    8.46 -  bin_pred_Pls
    8.47 -    "bin_pred (Pls)       = Min"
    8.48 -  bin_pred_Min
    8.49 -    "bin_pred (Min)       = Cons(Min,0)"
    8.50 -    "bin_pred (Cons(w,b)) = cond(b, NCons(w,0),
    8.51 -				    Cons(bin_pred(w), 1))"
    8.52 +  bin_pred_Pls  "bin_pred (Pls)     = Min"
    8.53 +  bin_pred_Min  "bin_pred (Min)     = Min BIT 0"
    8.54 +  bin_pred_BIT  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
    8.55  
    8.56  primrec (*unary negation*)
    8.57    bin_minus_Pls
    8.58      "bin_minus (Pls)       = Pls"
    8.59    bin_minus_Min
    8.60 -    "bin_minus (Min)       = Cons(Pls,1)"
    8.61 -    "bin_minus (Cons(w,b)) = cond(b, bin_pred(NCons(bin_minus(w),0)),
    8.62 -				     Cons(bin_minus(w),0))"
    8.63 +    "bin_minus (Min)       = Pls BIT 1"
    8.64 +  bin_minus_BIT
    8.65 +    "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
    8.66 +				bin_minus(w) BIT 0)"
    8.67  
    8.68  (*Mutual recursion is not always sound, but it is for primitive recursion.*)
    8.69  primrec (*sum*)
    8.70 -  "bin_add (Pls,w)       = w"
    8.71 -  "bin_add (Min,w)       = bin_pred(w)"
    8.72 -  "bin_add (Cons(v,x),w) = adding(v,x,w)"
    8.73 +  bin_add_Pls
    8.74 +    "bin_add (Pls,w)     = w"
    8.75 +  bin_add_Min
    8.76 +    "bin_add (Min,w)     = bin_pred(w)"
    8.77 +  bin_add_BIT
    8.78 +    "bin_add (v BIT x,w) = adding(v,x,w)"
    8.79  
    8.80  primrec (*auxilliary function for sum*)
    8.81 -  "adding (v,x,Pls)       = Cons(v,x)"
    8.82 -  "adding (v,x,Min)       = bin_pred(Cons(v,x))"
    8.83 -  "adding (v,x,Cons(w,y)) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)), 
    8.84 -				  x xor y)"
    8.85 +  "adding (v,x,Pls)     = v BIT x"
    8.86 +  "adding (v,x,Min)     = bin_pred(v BIT x)"
    8.87 +  "adding (v,x,w BIT y) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)), 
    8.88 +				x xor y)"
    8.89  
    8.90  primrec
    8.91    bin_mult_Pls
    8.92 -    "bin_mult (Pls,w)       = Pls"
    8.93 +    "bin_mult (Pls,w)     = Pls"
    8.94    bin_mult_Min
    8.95 -    "bin_mult (Min,w)       = bin_minus(w)"
    8.96 -    "bin_mult (Cons(v,b),w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
    8.97 -				      NCons(bin_mult(v,w),0))"
    8.98 +    "bin_mult (Min,w)     = bin_minus(w)"
    8.99 +  bin_mult_BIT
   8.100 +    "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
   8.101 +				 NCons(bin_mult(v,w),0))"
   8.102  
   8.103  end
   8.104  
   8.105 @@ -138,7 +137,7 @@
   8.106  
   8.107        fun term_of [] = const "Pls"
   8.108          | term_of [~1] = const "Min"
   8.109 -        | term_of (b :: bs) = const "Cons" $ term_of bs $ mk_bit b;
   8.110 +        | term_of (b :: bs) = const "op BIT" $ term_of bs $ mk_bit b;
   8.111      in
   8.112        term_of (bin_of (sign * (#1 (read_int digs))))
   8.113      end;
   8.114 @@ -147,7 +146,7 @@
   8.115      let
   8.116        fun bin_of (Const ("Pls", _)) = []
   8.117          | bin_of (Const ("Min", _)) = [~1]
   8.118 -        | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
   8.119 +        | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
   8.120          | bin_of _ = raise Match;
   8.121  
   8.122        fun integ_of [] = 0
     9.1 --- a/src/ZF/Integ/EquivClass.ML	Mon Jan 25 20:35:19 1999 +0100
     9.2 +++ b/src/ZF/Integ/EquivClass.ML	Wed Jan 27 10:31:31 1999 +0100
     9.3 @@ -94,6 +94,7 @@
     9.4  Goalw [quotient_def] "x:A ==> r``{x}: A/r";
     9.5  by (etac RepFunI 1);
     9.6  qed "quotientI";
     9.7 +AddTCs [quotientI];
     9.8  
     9.9  val major::prems = Goalw [quotient_def]
    9.10      "[| X: A/r;  !!x. [| X = r``{x};  x:A |] ==> P |]   \
    10.1 --- a/src/ZF/Integ/Int.ML	Mon Jan 25 20:35:19 1999 +0100
    10.2 +++ b/src/ZF/Integ/Int.ML	Wed Jan 27 10:31:31 1999 +0100
    10.3 @@ -20,13 +20,14 @@
    10.4  val eqa::eqb::prems = goal Arith.thy 
    10.5      "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    10.6  \       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    10.7 +by (cut_facts_tac prems 1);
    10.8  by (res_inst_tac [("k","x2")] add_left_cancel 1);
    10.9 -by (resolve_tac prems 2);
   10.10 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
   10.11 +by (rtac (add_left_commute RS trans) 1);
   10.12 +by Auto_tac;
   10.13  by (stac eqb 1);
   10.14 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
   10.15 -by (stac eqa 1);
   10.16 -by (rtac (add_left_commute) 1 THEN typechk_tac prems);
   10.17 +by (rtac (add_left_commute RS trans) 1);
   10.18 +by (stac eqa 3);
   10.19 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
   10.20  qed "int_trans_lemma";
   10.21  
   10.22  (** Natural deduction for intrel **)
   10.23 @@ -79,15 +80,15 @@
   10.24  
   10.25  Goalw [int_def,quotient_def,int_of_def]
   10.26      "m : nat ==> $#m : int";
   10.27 -by (fast_tac (claset() addSIs [nat_0I]) 1);
   10.28 +by Auto_tac;
   10.29  qed "int_of_type";
   10.30  
   10.31  Addsimps [int_of_type];
   10.32 +AddTCs   [int_of_type];
   10.33  
   10.34  Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
   10.35  by (dtac (sym RS eq_intrelD) 1);
   10.36 -by (typechk_tac [nat_0I, SigmaI]);
   10.37 -by (Asm_full_simp_tac 1);
   10.38 +by Auto_tac;
   10.39  qed "int_of_inject";
   10.40  
   10.41  AddSDs [int_of_inject];
   10.42 @@ -108,9 +109,9 @@
   10.43  val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   10.44  
   10.45  Goalw [int_def,zminus_def] "z : int ==> $~z : int";
   10.46 -by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
   10.47 -                 quotientI]);
   10.48 +by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   10.49  qed "zminus_type";
   10.50 +AddTCs [zminus_type];
   10.51  
   10.52  Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   10.53  by (etac (zminus_ize UN_equiv_class_inject) 1);
   10.54 @@ -160,7 +161,7 @@
   10.55  
   10.56  Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   10.57  by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   10.58 -be natE 1;
   10.59 +by (etac natE 1);
   10.60  by (dres_inst_tac [("x","0")] spec 2);
   10.61  by Auto_tac;
   10.62  qed "not_znegative_imp_zero";
   10.63 @@ -178,9 +179,10 @@
   10.64  Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   10.65  
   10.66  Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   10.67 -br theI2 1;
   10.68 +by (rtac theI2 1);
   10.69  by Auto_tac;
   10.70  qed "zmagnitude_type";
   10.71 +AddTCs [zmagnitude_type];
   10.72  
   10.73  Goalw [int_def, znegative_def, int_of_def]
   10.74       "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   10.75 @@ -188,14 +190,14 @@
   10.76  by (rename_tac "i j" 1);
   10.77  by (dres_inst_tac [("x", "i")] spec 1);
   10.78  by (dres_inst_tac [("x", "j")] spec 1);
   10.79 -br bexI 1;
   10.80 -br (add_diff_inverse2 RS sym) 1;
   10.81 +by (rtac bexI 1);
   10.82 +by (rtac (add_diff_inverse2 RS sym) 1);
   10.83  by Auto_tac;
   10.84  by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
   10.85  qed "not_zneg_int_of";
   10.86  
   10.87  Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   10.88 -bd not_zneg_int_of 1;
   10.89 +by (dtac not_zneg_int_of 1);
   10.90  by Auto_tac;
   10.91  qed "not_zneg_mag"; 
   10.92  
   10.93 @@ -214,7 +216,7 @@
   10.94  qed "zneg_int_of";
   10.95  
   10.96  Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   10.97 -bd zneg_int_of 1;
   10.98 +by (dtac zneg_int_of 1);
   10.99  by Auto_tac;
  10.100  qed "zneg_mag"; 
  10.101  
  10.102 @@ -236,7 +238,7 @@
  10.103    add_ac does not help rewriting with the assumptions.*)
  10.104  by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
  10.105  by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
  10.106 -by (typechk_tac [add_type]);
  10.107 +by Auto_tac;
  10.108  by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
  10.109  qed "zadd_congruent2";
  10.110  
  10.111 @@ -248,6 +250,7 @@
  10.112  by (simp_tac (simpset() addsimps [Let_def]) 3);
  10.113  by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
  10.114  qed "zadd_type";
  10.115 +AddTCs [zadd_type];
  10.116  
  10.117  Goalw [zadd_def]
  10.118    "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
  10.119 @@ -282,7 +285,8 @@
  10.120  
  10.121  (*For AC rewriting*)
  10.122  Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
  10.123 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
  10.124 +by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
  10.125 +by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
  10.126  qed "zadd_left_commute";
  10.127  
  10.128  (*Integer addition is an AC operator*)
  10.129 @@ -343,6 +347,7 @@
  10.130                        split_type, add_type, mult_type, 
  10.131                        quotientI, SigmaI] 1));
  10.132  qed "zmult_type";
  10.133 +AddTCs [zmult_type];
  10.134  
  10.135  Goalw [zmult_def]
  10.136       "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
  10.137 @@ -389,7 +394,8 @@
  10.138  
  10.139  (*For AC rewriting*)
  10.140  Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
  10.141 -by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
  10.142 +by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
  10.143 +by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
  10.144  qed "zmult_left_commute";
  10.145  
  10.146  (*Integer multiplication is an AC operator*)
    11.1 --- a/src/ZF/List.ML	Mon Jan 25 20:35:19 1999 +0100
    11.2 +++ b/src/ZF/List.ML	Wed Jan 27 10:31:31 1999 +0100
    11.3 @@ -166,9 +166,7 @@
    11.4      [list_rec_type, map_type, map_type2, app_type, length_type, 
    11.5       rev_type, flat_type, list_add_type];
    11.6  
    11.7 -Addsimps list_typechecks;
    11.8 -
    11.9 -simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
   11.10 +AddTCs list_typechecks;
   11.11  
   11.12  
   11.13  (*** theorems about map ***)
    12.1 --- a/src/ZF/Nat.ML	Mon Jan 25 20:35:19 1999 +0100
    12.2 +++ b/src/ZF/Nat.ML	Wed Jan 27 10:31:31 1999 +0100
    12.3 @@ -6,8 +6,6 @@
    12.4  Natural numbers in Zermelo-Fraenkel Set Theory 
    12.5  *)
    12.6  
    12.7 -open Nat;
    12.8 -
    12.9  Goal "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";
   12.10  by (rtac bnd_monoI 1);
   12.11  by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); 
   12.12 @@ -40,10 +38,10 @@
   12.13  
   12.14  Addsimps [nat_0I, nat_1I, nat_2I];
   12.15  AddSIs   [nat_0I, nat_1I, nat_2I, nat_succI];
   12.16 +AddTCs   [nat_0I, nat_1I, nat_2I, nat_succI];
   12.17  
   12.18  Goal "bool <= nat";
   12.19 -by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
   12.20 -            ORELSE eresolve_tac [boolE,ssubst] 1));
   12.21 +by (blast_tac (claset() addSEs [boolE]) 1);
   12.22  qed "bool_subset_nat";
   12.23  
   12.24  val bool_into_nat = bool_subset_nat RS subsetD;
    13.1 --- a/src/ZF/Order.ML	Mon Jan 25 20:35:19 1999 +0100
    13.2 +++ b/src/ZF/Order.ML	Wed Jan 27 10:31:31 1999 +0100
    13.3 @@ -253,8 +253,8 @@
    13.4  
    13.5  (*Rewriting with bijections and converse (function inverse)*)
    13.6  val bij_inverse_ss = 
    13.7 -    simpset() setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
    13.8 -                                       bij_converse_bij, comp_fun, comp_bij])
    13.9 +    simpset() setSolver 
   13.10 +      type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_fun, comp_fun, comp_bij])
   13.11            addsimps [right_inverse_bij, left_inverse_bij];
   13.12  
   13.13  (** Symmetry and Transitivity Rules **)
   13.14 @@ -266,23 +266,22 @@
   13.15  qed "ord_iso_refl";
   13.16  
   13.17  (*Symmetry of similarity*)
   13.18 -Goalw [ord_iso_def] 
   13.19 -    "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
   13.20 -by (fast_tac (claset() addss bij_inverse_ss) 1);
   13.21 +Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
   13.22 +by (force_tac (claset(), bij_inverse_ss) 1);
   13.23  qed "ord_iso_sym";
   13.24  
   13.25  (*Transitivity of similarity*)
   13.26  Goalw [mono_map_def] 
   13.27      "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |] ==> \
   13.28  \         (f O g): mono_map(A,r,C,t)";
   13.29 -by (fast_tac (claset() addss bij_inverse_ss) 1);
   13.30 +by (force_tac (claset(), bij_inverse_ss) 1);
   13.31  qed "mono_map_trans";
   13.32  
   13.33  (*Transitivity of similarity: the order-isomorphism relation*)
   13.34  Goalw [ord_iso_def] 
   13.35      "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |] ==> \
   13.36  \         (f O g): ord_iso(A,r,C,t)";
   13.37 -by (fast_tac (claset() addss bij_inverse_ss) 1);
   13.38 +by (force_tac (claset(), bij_inverse_ss) 1);
   13.39  qed "ord_iso_trans";
   13.40  
   13.41  (** Two monotone maps can make an order-isomorphism **)
   13.42 @@ -373,16 +372,16 @@
   13.43  
   13.44  (*Simple consequence of Lemma 6.1*)
   13.45  Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
   13.46 -\         a:A;  c:A |] ==> a=c";
   13.47 +\        a:A;  c:A |] ==> a=c";
   13.48  by (forward_tac [well_ord_is_trans_on] 1);
   13.49  by (forward_tac [well_ord_is_linear] 1);
   13.50  by (linear_case_tac 1);
   13.51  by (dtac ord_iso_sym 1);
   13.52 -by (REPEAT   (*because there are two symmetric cases*)
   13.53 -    (EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS
   13.54 -                          well_ord_iso_predE] 1,
   13.55 -            blast_tac (claset() addSIs [predI]) 2,
   13.56 -            asm_simp_tac (simpset() addsimps [trans_pred_pred_eq]) 1]));
   13.57 +(*two symmetric cases*)
   13.58 +by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS
   13.59 +			       well_ord_iso_predE]
   13.60 +	               addSIs [predI], 
   13.61 +	      simpset() addsimps [trans_pred_pred_eq]));
   13.62  qed "well_ord_iso_pred_eq";
   13.63  
   13.64  (*Does not assume r is a wellordering!*)
    14.1 --- a/src/ZF/OrderType.ML	Mon Jan 25 20:35:19 1999 +0100
    14.2 +++ b/src/ZF/OrderType.ML	Wed Jan 27 10:31:31 1999 +0100
    14.3 @@ -10,8 +10,6 @@
    14.4  *)
    14.5  
    14.6  
    14.7 -open OrderType;
    14.8 -
    14.9  (**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
   14.10  
   14.11  val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
   14.12 @@ -499,8 +497,8 @@
   14.13  qed "oadd_1";
   14.14  
   14.15  Goal "[| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
   14.16 -                (*ZF_ss prevents looping*)
   14.17 -by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
   14.18 +                (*FOL_ss prevents looping*)
   14.19 +by (asm_simp_tac (FOL_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
   14.20  by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
   14.21  qed "oadd_succ";
   14.22  
   14.23 @@ -766,8 +764,8 @@
   14.24  qed "oadd_omult_distrib";
   14.25  
   14.26  Goal "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
   14.27 -                (*ZF_ss prevents looping*)
   14.28 -by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
   14.29 +                (*FOL_ss prevents looping*)
   14.30 +by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym]) 1);
   14.31  by (asm_simp_tac 
   14.32      (simpset() addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
   14.33  qed "omult_succ";
    15.1 --- a/src/ZF/Ordinal.ML	Mon Jan 25 20:35:19 1999 +0100
    15.2 +++ b/src/ZF/Ordinal.ML	Wed Jan 27 10:31:31 1999 +0100
    15.3 @@ -6,8 +6,6 @@
    15.4  Ordinals in Zermelo-Fraenkel Set Theory 
    15.5  *)
    15.6  
    15.7 -open Ordinal;
    15.8 -
    15.9  (*** Rules for Transset ***)
   15.10  
   15.11  (** Two neat characterisations of Transset **)
   15.12 @@ -149,6 +147,7 @@
   15.13  
   15.14  Addsimps [Ord_0, Ord_succ_iff];
   15.15  AddSIs   [Ord_0, Ord_succ];
   15.16 +AddTCs   [Ord_0, Ord_succ];
   15.17  
   15.18  Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Un j)";
   15.19  by (blast_tac (claset() addSIs [Transset_Un]) 1);
   15.20 @@ -157,6 +156,7 @@
   15.21  Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Int j)";
   15.22  by (blast_tac (claset() addSIs [Transset_Int]) 1);
   15.23  qed "Ord_Int";
   15.24 +AddTCs   [Ord_Un, Ord_Int];
   15.25  
   15.26  val nonempty::prems = Goal
   15.27      "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
    16.1 --- a/src/ZF/Perm.ML	Mon Jan 25 20:35:19 1999 +0100
    16.2 +++ b/src/ZF/Perm.ML	Wed Jan 27 10:31:31 1999 +0100
    16.3 @@ -9,8 +9,6 @@
    16.4    -- Lemmas for the Schroeder-Bernstein Theorem
    16.5  *)
    16.6  
    16.7 -open Perm;
    16.8 -
    16.9  (** Surjective function space **)
   16.10  
   16.11  Goalw [surj_def] "f: surj(A,B) ==> f: A->B";
   16.12 @@ -93,7 +91,7 @@
   16.13  qed "bij_is_surj";
   16.14  
   16.15  (* f: bij(A,B) ==> f: A->B *)
   16.16 -bind_thm ("bij_is_fun", (bij_is_inj RS inj_is_fun));
   16.17 +bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
   16.18  
   16.19  val prems = goalw Perm.thy [bij_def]
   16.20      "[| !!x. x:A ==> c(x): B;           \
   16.21 @@ -225,6 +223,8 @@
   16.22  qed "bij_converse_bij";
   16.23  (*Adding this as an SI seems to cause looping*)
   16.24  
   16.25 +AddTCs [bij_converse_bij];
   16.26 +
   16.27  
   16.28  (** Composition of two relations **)
   16.29  
   16.30 @@ -342,17 +342,19 @@
   16.31  by (rtac fun_extension 1);
   16.32  by (rtac comp_fun 1);
   16.33  by (rtac lam_funtype 2);
   16.34 -by (typechk_tac (prem::ZF_typechecks));
   16.35 +by (typecheck_tac (tcset() addTCs [prem]));
   16.36  by (asm_simp_tac (simpset() 
   16.37 -             setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
   16.38 +                   setSolver 
   16.39 +                   type_solver_tac (tcset() addTCs [prem, lam_funtype])) 1);
   16.40  qed "comp_lam";
   16.41  
   16.42  Goal "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
   16.43  by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
   16.44      f_imp_injective 1);
   16.45  by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
   16.46 -by (asm_simp_tac (simpset()  addsimps [left_inverse] 
   16.47 -                        setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
   16.48 +by (asm_simp_tac (simpset() addsimps [left_inverse] 
   16.49 +		  setSolver
   16.50 +		  type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
   16.51  qed "comp_inj";
   16.52  
   16.53  Goalw [surj_def]
    17.1 --- a/src/ZF/ROOT.ML	Mon Jan 25 20:35:19 1999 +0100
    17.2 +++ b/src/ZF/ROOT.ML	Wed Jan 27 10:31:31 1999 +0100
    17.3 @@ -20,7 +20,7 @@
    17.4  use     "thy_syntax";
    17.5  
    17.6  use_thy "Let";
    17.7 -use_thy "func";
    17.8 +use_thy "ZF";
    17.9  use     "Tools/typechk";
   17.10  use_thy "mono";
   17.11  use     "ind_syntax";
    18.1 --- a/src/ZF/Sum.ML	Mon Jan 25 20:35:19 1999 +0100
    18.2 +++ b/src/ZF/Sum.ML	Wed Jan 27 10:31:31 1999 +0100
    18.3 @@ -6,8 +6,6 @@
    18.4  Disjoint sums in Zermelo-Fraenkel Set Theory 
    18.5  *)
    18.6  
    18.7 -open Sum;
    18.8 -
    18.9  (*** Rules for the Part primitive ***)
   18.10  
   18.11  Goalw [Part_def]
   18.12 @@ -102,6 +100,7 @@
   18.13  AddSDs [Inl_inject, Inr_inject];
   18.14  
   18.15  Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
   18.16 +AddTCs   [InlI, InrI];
   18.17  
   18.18  Goal "Inl(a): A+B ==> a: A";
   18.19  by (Blast_tac 1);
   18.20 @@ -150,6 +149,7 @@
   18.21  by (ALLGOALS (etac ssubst));
   18.22  by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   18.23  qed "case_type";
   18.24 +AddTCs [case_type];
   18.25  
   18.26  Goal "u: A+B ==>   \
   18.27  \       R(case(c,d,u)) <-> \
    19.1 --- a/src/ZF/Tools/typechk.ML	Mon Jan 25 20:35:19 1999 +0100
    19.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jan 27 10:31:31 1999 +0100
    19.3 @@ -1,11 +1,54 @@
    19.4  (*  Title:      ZF/typechk
    19.5      ID:         $Id$
    19.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7 -    Copyright   1991  University of Cambridge
    19.8 +    Copyright   1999  University of Cambridge
    19.9  
   19.10  Tactics for type checking -- from CTT
   19.11  *)
   19.12  
   19.13 +infix 4 addTCs delTCs;
   19.14 +
   19.15 +structure TypeCheck =
   19.16 +struct
   19.17 +datatype tcset =
   19.18 +    TC of {rules: thm list,	(*the type-checking rules*)
   19.19 +	   net: thm Net.net};   (*discrimination net of the same rules*)     
   19.20 +
   19.21 +
   19.22 +
   19.23 +val mem_thm = gen_mem eq_thm
   19.24 +and rem_thm = gen_rem eq_thm;
   19.25 +
   19.26 +fun addTC (cs as TC{rules, net}, th) =
   19.27 +  if mem_thm (th, rules) then 
   19.28 +	 (warning ("Ignoring duplicate type-checking rule\n" ^ 
   19.29 +		   string_of_thm th);
   19.30 +	  cs)
   19.31 +  else
   19.32 +      TC{rules	= th::rules,
   19.33 +	 net = Net.insert_term ((concl_of th, th), net, K false)};
   19.34 +
   19.35 +
   19.36 +fun delTC (cs as TC{rules, net}, th) =
   19.37 +  if mem_thm (th, rules) then
   19.38 +      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
   19.39 +	 rules	= rem_thm (rules,th)}
   19.40 +  else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); 
   19.41 +	cs);
   19.42 +
   19.43 +val op addTCs = foldl addTC;
   19.44 +val op delTCs = foldl delTC;
   19.45 +
   19.46 +
   19.47 +(*resolution using a net rather than rules*)
   19.48 +fun net_res_tac maxr net =
   19.49 +  SUBGOAL
   19.50 +    (fn (prem,i) =>
   19.51 +      let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
   19.52 +      in 
   19.53 +	 if length rls <= maxr then resolve_tac rls i else no_tac
   19.54 +      end);
   19.55 +
   19.56  fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) = 
   19.57        not (is_Var (head_of a))
   19.58    | is_rigid_elem _ = false;
   19.59 @@ -17,18 +60,75 @@
   19.60  
   19.61  (*Type checking solves a:?A (a rigid, ?A maybe flexible).  
   19.62    match_tac is too strict; would refuse to instantiate ?A*)
   19.63 -fun typechk_step_tac tyrls =
   19.64 -    FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
   19.65 +fun typecheck_step_tac (TC{net,...}) =
   19.66 +    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
   19.67  
   19.68 -fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
   19.69 +fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
   19.70  
   19.71 -val ZF_typechecks =
   19.72 -    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
   19.73 +(*Compiles a term-net for speed*)
   19.74 +val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
   19.75 +				     ballI,allI,conjI,impI];
   19.76  
   19.77  (*Instantiates variables in typing conditions.
   19.78    drawback: does not simplify conjunctions*)
   19.79 -fun type_auto_tac tyrls hyps = SELECT_GOAL
   19.80 -    (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
   19.81 -           ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
   19.82 -			    ballI,allI,conjI,impI] 1));
   19.83 +fun type_solver_tac tcset hyps = SELECT_GOAL
   19.84 +    (DEPTH_SOLVE (etac FalseE 1
   19.85 +		  ORELSE basic_res_tac 1
   19.86 +		  ORELSE (ares_tac hyps 1
   19.87 +			  APPEND typecheck_step_tac tcset)));
   19.88 +
   19.89 +
   19.90 +
   19.91 +fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
   19.92 +    TC {rules = gen_union eq_thm (rules,rules'),
   19.93 +	net = Net.merge (net, net', eq_thm)};
   19.94 +
   19.95 +(*print tcsets*)
   19.96 +fun print_tc (TC{rules,...}) =
   19.97 +    Pretty.writeln
   19.98 +       (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
   19.99 +
  19.100 +
  19.101 +structure TypecheckingArgs =
  19.102 +  struct
  19.103 +  val name = "ZF/type-checker";
  19.104 +  type T = tcset ref;
  19.105 +  val empty = ref (TC{rules=[], net=Net.empty});
  19.106 +  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
  19.107 +  fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
  19.108 +  fun print _ (ref tc) = print_tc tc;
  19.109 +  end;
  19.110 +
  19.111 +structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
  19.112  
  19.113 +val setup = [TypecheckingData.init];
  19.114 +
  19.115 +val print_tcset = TypecheckingData.print;
  19.116 +val tcset_ref_of_sg = TypecheckingData.get_sg;
  19.117 +val tcset_ref_of = TypecheckingData.get;
  19.118 +
  19.119 +(* access global tcset *)
  19.120 +
  19.121 +val tcset_of_sg = ! o tcset_ref_of_sg;
  19.122 +val tcset_of = tcset_of_sg o sign_of;
  19.123 +
  19.124 +val tcset = tcset_of o Context.the_context;
  19.125 +val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
  19.126 +
  19.127 +(* change global tcset *)
  19.128 +
  19.129 +fun change_tcset f x = tcset_ref () := (f (tcset (), x));
  19.130 +
  19.131 +val AddTCs = change_tcset (op addTCs);
  19.132 +val DelTCs = change_tcset (op delTCs);
  19.133 +
  19.134 +fun Typecheck_tac st = typecheck_tac (tcset()) st;
  19.135 +
  19.136 +fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
  19.137 +end;
  19.138 +
  19.139 +
  19.140 +open TypeCheck;
  19.141 +
  19.142 +
  19.143 +
    20.1 --- a/src/ZF/ex/BinEx.ML	Mon Jan 25 20:35:19 1999 +0100
    20.2 +++ b/src/ZF/ex/BinEx.ML	Wed Jan 27 10:31:31 1999 +0100
    20.3 @@ -12,43 +12,43 @@
    20.4  (*All runtimes below are on a 300MHz Pentium*)
    20.5  
    20.6  Goal "#13  $+  #19 = #32";
    20.7 -by (simp_tac bin_comp_ss 1);    (*0 secs*)
    20.8 +by (Simp_tac 1);    (*0 secs*)
    20.9  result();
   20.10  
   20.11  Goal "#1234  $+  #5678 = #6912";
   20.12 -by (simp_tac bin_comp_ss 1);    (*190 msec*)
   20.13 +by (Simp_tac 1);    (*190 msec*)
   20.14  result();
   20.15  
   20.16  Goal "#1359  $+  #-2468 = #-1109";
   20.17 -by (simp_tac bin_comp_ss 1);    (*160 msec*)
   20.18 +by (Simp_tac 1);    (*160 msec*)
   20.19  result();
   20.20  
   20.21  Goal "#93746  $+  #-46375 = #47371";
   20.22 -by (simp_tac bin_comp_ss 1);    (*300 msec*)
   20.23 +by (Simp_tac 1);    (*300 msec*)
   20.24  result();
   20.25  
   20.26  Goal "$~ #65745 = #-65745";
   20.27 -by (simp_tac bin_comp_ss 1);    (*80 msec*)
   20.28 +by (Simp_tac 1);    (*80 msec*)
   20.29  result();
   20.30  
   20.31  (* negation of ~54321 *)
   20.32  Goal "$~ #-54321 = #54321";
   20.33 -by (simp_tac bin_comp_ss 1);    (*90 msec*)
   20.34 +by (Simp_tac 1);    (*90 msec*)
   20.35  result();
   20.36  
   20.37  Goal "#13  $*  #19 = #247";
   20.38 -by (simp_tac bin_comp_ss 1);    (*110 msec*)
   20.39 +by (Simp_tac 1);    (*110 msec*)
   20.40  result();
   20.41  
   20.42  Goal "#-84  $*  #51 = #-4284";
   20.43 -by (simp_tac bin_comp_ss 1);    (*210 msec*)
   20.44 +by (Simp_tac 1);    (*210 msec*)
   20.45  result();
   20.46  
   20.47  (*The worst case for 8-bit operands *)
   20.48  Goal "#255  $*  #255 = #65025";
   20.49 -by (simp_tac bin_comp_ss 1);    (*730 msec*)
   20.50 +by (Simp_tac 1);    (*730 msec*)
   20.51  result();
   20.52  
   20.53  Goal "#1359  $*  #-2468 = #-3354012";
   20.54 -by (simp_tac bin_comp_ss 1);    (*1.04 secs*)
   20.55 +by (Simp_tac 1);    (*1.04 secs*)
   20.56  result();
    21.1 --- a/src/ZF/ex/Limit.ML	Mon Jan 25 20:35:19 1999 +0100
    21.2 +++ b/src/ZF/ex/Limit.ML	Wed Jan 27 10:31:31 1999 +0100
    21.3 @@ -9,8 +9,6 @@
    21.4     
    21.5  val nat_linear_le = [nat_into_Ord,nat_into_Ord] MRS Ord_linear_le;
    21.6  
    21.7 -open Limit; 
    21.8 -
    21.9  (*----------------------------------------------------------------------*)
   21.10  (* Useful goal commands.                                                *)
   21.11  (*----------------------------------------------------------------------*)
   21.12 @@ -797,6 +795,8 @@
   21.13  by (asm_simp_tac(simpset() addsimps[id_thm, cpo_lub RS islub_in, chain_in, chain_fun RS eta]) 1);
   21.14  qed "id_cont";
   21.15  
   21.16 +AddTCs [id_cont];
   21.17 +
   21.18  val comp_cont_apply = cont_fun RSN(2,cont_fun RS comp_fun_apply);
   21.19  
   21.20  Goal  (* comp_pres_cont *)
   21.21 @@ -814,6 +814,8 @@
   21.22  by (auto_tac (claset() addIs [cpo_lub RS islub_in, cont_chain], simpset()));
   21.23  qed "comp_pres_cont";
   21.24  
   21.25 +AddTCs [comp_pres_cont];
   21.26 +
   21.27  Goal  (* comp_mono *)
   21.28      "[| f:cont(D',E); g:cont(D,D'); f':cont(D',E); g':cont(D,D');   \
   21.29  \       rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |] ==>   \
   21.30 @@ -1017,9 +1019,11 @@
   21.31  
   21.32  (* The following three theorems have cpo asms due to THE (uniqueness). *)
   21.33  
   21.34 -val Rp_cont = embRp RS projpair_p_cont;
   21.35 -val embRp_eq = embRp RS projpair_eq;
   21.36 -val embRp_rel = embRp RS projpair_rel;
   21.37 +bind_thm ("Rp_cont", embRp RS projpair_p_cont);
   21.38 +bind_thm ("embRp_eq", embRp RS projpair_eq);
   21.39 +bind_thm ("embRp_rel", embRp RS projpair_rel);
   21.40 +
   21.41 +AddTCs [Rp_cont];
   21.42  
   21.43  val id_apply = prove_goalw Perm.thy [id_def]
   21.44      "!!z. x:A ==> id(A)`x = x"
   21.45 @@ -1356,6 +1360,8 @@
   21.46      "!!x. [|emb_chain(DD,ee); n:nat|] ==> cpo(DD`n)"
   21.47    (fn prems => [Fast_tac 1]);
   21.48  
   21.49 +AddTCs [emb_chain_cpo];
   21.50 +
   21.51  val emb_chain_emb = prove_goalw Limit.thy [emb_chain_def] 
   21.52      "!!x. [|emb_chain(DD,ee); n:nat|] ==> emb(DD`n,DD`succ(n),ee`n)"
   21.53    (fn prems => [Fast_tac 1]);
   21.54 @@ -1952,7 +1958,7 @@
   21.55     but since x le y is x<succ(y) simplification does too much with this thm. *)
   21.56  by (stac eps_split_right_le 1);
   21.57  by (assume_tac 2);
   21.58 -by (asm_simp_tac(ZF_ss addsimps [add1]) 1);
   21.59 +by (asm_simp_tac(FOL_ss addsimps [add1]) 1);
   21.60  brr[add_le_self,nat_0I,nat_succI] 1;
   21.61  by (asm_simp_tac(simpset() addsimps[eps_succ_Rp]) 1);
   21.62  by (stac comp_fun_apply 1);
   21.63 @@ -2377,7 +2383,8 @@
   21.64  by (asm_simp_tac (simpset() addsimps[lemma]) 1);
   21.65  by (rtac dominate_islub 1);
   21.66  by (rtac cpo_lub 2);
   21.67 -brr[commute_chain, commute_emb, islub_const, cont_cf, id_cont, cpo_cf, chain_fun,chain_const] 2;
   21.68 +brr[commute_chain, commute_emb, islub_const, cont_cf, id_cont,
   21.69 +    cpo_cf, chain_fun,chain_const] 2;
   21.70  by (rtac dominateI 1);
   21.71  by (assume_tac 1); 
   21.72  by (Asm_simp_tac 1);
   21.73 @@ -2412,10 +2419,9 @@
   21.74  \     (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
   21.75  by (rtac fun_extension 1);
   21.76  by (fast_tac (claset() addIs [lam_type]) 1);
   21.77 -by (ALLGOALS 
   21.78 -    (asm_simp_tac 
   21.79 -     (simpset() setSolver (type_auto_tac [lam_type, comp_pres_cont, Rp_cont, 
   21.80 -			        emb_cont, commute_emb, emb_chain_cpo]))));
   21.81 +by (asm_simp_tac 
   21.82 +     (simpset() setSolver type_solver_tac (tcset() addTCs [emb_cont, commute_emb])) 2);
   21.83 +by (Asm_simp_tac 1);
   21.84  val lemma = result();
   21.85  
   21.86  Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
    22.1 --- a/src/ZF/ex/ListN.ML	Mon Jan 25 20:35:19 1999 +0100
    22.2 +++ b/src/ZF/ex/ListN.ML	Wed Jan 27 10:31:31 1999 +0100
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      ZF/ex/listn
    22.5 +(*  Title:      ZF/ex/ListN
    22.6      ID:         $Id$
    22.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.8      Copyright   1993  University of Cambridge
    22.9 @@ -19,7 +19,7 @@
   22.10  by (rtac iffI 1);
   22.11  by (blast_tac (claset() addIs [list_into_listn]) 2);
   22.12  by (etac listn.induct 1);
   22.13 -by (ALLGOALS Asm_simp_tac);
   22.14 +by Auto_tac;
   22.15  qed "listn_iff";
   22.16  
   22.17  Goal "listn(A)``{n} = {l:list(A). length(l)=n}";
    23.1 --- a/src/ZF/ex/Primrec.ML	Mon Jan 25 20:35:19 1999 +0100
    23.2 +++ b/src/ZF/ex/Primrec.ML	Wed Jan 27 10:31:31 1999 +0100
    23.3 @@ -19,25 +19,20 @@
    23.4  (* c: prim_rec ==> c: list(nat) -> nat *)
    23.5  val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
    23.6  
    23.7 -simpset_ref() := simpset() setSolver (type_auto_tac ([prim_rec_into_fun] @ 
    23.8 -					      pr_typechecks @ prim_rec.intrs));
    23.9 +AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
   23.10  
   23.11  Goal "i:nat ==> ACK(i): prim_rec";
   23.12  by (induct_tac "i" 1);
   23.13  by (ALLGOALS Asm_simp_tac);
   23.14  qed "ACK_in_prim_rec";
   23.15  
   23.16 -val ack_typechecks =
   23.17 -    [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
   23.18 -     add_type, list_add_type, nat_into_Ord] @ 
   23.19 -    nat_typechecks @ list.intrs @ prim_rec.intrs;
   23.20 -
   23.21 -simpset_ref() := simpset() setSolver (type_auto_tac ack_typechecks);
   23.22 +AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
   23.23 +	list_add_type, nat_into_Ord, rec_type];
   23.24  
   23.25  Goal "[| i:nat;  j:nat |] ==>  ack(i,j): nat";
   23.26  by Auto_tac;
   23.27  qed "ack_type";
   23.28 -Addsimps [ack_type];
   23.29 +AddTCs [ack_type];
   23.30  
   23.31  (** Ackermann's function cases **)
   23.32  
   23.33 @@ -84,7 +79,7 @@
   23.34  by (etac succ_lt_induct 1);
   23.35  by (assume_tac 1);
   23.36  by (rtac lt_trans 2);
   23.37 -by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr_typechecks) 1));
   23.38 +by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset()));
   23.39  qed "ack_lt_mono2";
   23.40  
   23.41  (*PROPERTY A 5', monotonicity for le *)
   23.42 @@ -99,14 +94,14 @@
   23.43  by (ALLGOALS Asm_simp_tac);
   23.44  by (rtac ack_le_mono2 1);
   23.45  by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
   23.46 -by (REPEAT (ares_tac (ack_typechecks) 1));
   23.47 +by Auto_tac;
   23.48  qed "ack2_le_ack1";
   23.49  
   23.50  (*PROPERTY A 7-, the single-step lemma*)
   23.51  Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
   23.52  by (rtac (ack_lt_mono2 RS lt_trans2) 1);
   23.53  by (rtac ack2_le_ack1 4);
   23.54 -by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr_typechecks) 1));
   23.55 +by Auto_tac;
   23.56  qed "ack_lt_ack_succ1";
   23.57  
   23.58  (*PROPERTY A 7, monotonicity for < *)
   23.59 @@ -115,7 +110,7 @@
   23.60  by (etac succ_lt_induct 1);
   23.61  by (assume_tac 1);
   23.62  by (rtac lt_trans 2);
   23.63 -by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr_typechecks) 1));
   23.64 +by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset()));
   23.65  qed "ack_lt_mono1";
   23.66  
   23.67  (*PROPERTY A 7', monotonicity for le *)
   23.68 @@ -154,8 +149,8 @@
   23.69  by (rtac (ack_nest_bound RS lt_trans2) 2);
   23.70  by (Asm_simp_tac 5);
   23.71  by (rtac (add_le_mono RS leI RS leI) 1);
   23.72 -by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
   23.73 -                      ack_typechecks) 1));
   23.74 +by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1], 
   23.75 +	      simpset()));
   23.76  qed "ack_add_bound";
   23.77  
   23.78  (*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   23.79 @@ -164,8 +159,8 @@
   23.80  \             i#+j < ack(succ(succ(succ(succ(k)))), j)";
   23.81  by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
   23.82  by (rtac (ack_add_bound RS lt_trans2) 2);
   23.83 -by (asm_simp_tac (simpset() addsimps [add_0_right]) 5);
   23.84 -by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
   23.85 +br add_lt_mono 1;
   23.86 +by Auto_tac;
   23.87  qed "ack_add_bound2";
   23.88  
   23.89  (*** MAIN RESULT ***)
   23.90 @@ -259,16 +254,14 @@
   23.91  by (induct_tac "a" 1);
   23.92  (*base case*)
   23.93  by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
   23.94 -             assume_tac, rtac (add_le_self RS ack_lt_mono1),
   23.95 -             REPEAT o ares_tac (ack_typechecks)]);
   23.96 +	    assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
   23.97 +by Auto_tac;
   23.98  (*ind step*)
   23.99 -by (Asm_simp_tac 1);
  23.100  by (rtac (succ_leI RS lt_trans1) 1);
  23.101  by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
  23.102  by (etac bspec 2);
  23.103  by (rtac (nat_le_refl RS add_le_mono) 1);
  23.104 -	(*Auto_tac is a little slow*)
  23.105 -by (TRYALL (type_auto_tac ack_typechecks []));
  23.106 +by Typecheck_tac;
  23.107  by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
  23.108  (*final part of the simplification*)
  23.109  by (Asm_simp_tac 1);
  23.110 @@ -284,19 +277,15 @@
  23.111  \     |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))";
  23.112  by (rtac (ballI RS bexI) 1);
  23.113  by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
  23.114 -by (REPEAT
  23.115 -    (SOMEGOAL
  23.116 -     (FIRST' [test_assume_tac,
  23.117 -              match_tac (ack_typechecks),
  23.118 -              rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
  23.119 +by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
  23.120 +by Typecheck_tac;
  23.121  qed "PREC_case";
  23.122  
  23.123  Goal "f:prim_rec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
  23.124  by (etac prim_rec.induct 1);
  23.125 -by Safe_tac;
  23.126 -by (DEPTH_SOLVE
  23.127 -    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
  23.128 -                       bexI, ballI] @ nat_typechecks) 1));
  23.129 +by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
  23.130 +			      PREC_case], 
  23.131 +	      simpset()));
  23.132  qed "ack_bounds_prim_rec";
  23.133  
  23.134  Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : prim_rec";
  23.135 @@ -304,7 +293,6 @@
  23.136  by (etac (ack_bounds_prim_rec RS bexE) 1);
  23.137  by (rtac lt_irrefl 1);
  23.138  by (dres_inst_tac [("x", "[x]")] bspec 1);
  23.139 -by (Asm_simp_tac 1);
  23.140 -by (Asm_full_simp_tac 1);
  23.141 +by Auto_tac;
  23.142  qed "ack_not_prim_rec";
  23.143  
    24.1 --- a/src/ZF/ex/Primrec_defs.ML	Mon Jan 25 20:35:19 1999 +0100
    24.2 +++ b/src/ZF/ex/Primrec_defs.ML	Wed Jan 27 10:31:31 1999 +0100
    24.3 @@ -9,37 +9,25 @@
    24.4  (*Theory TF redeclares map_type*)
    24.5  val map_type = Context.thm "List.map_type";
    24.6  
    24.7 -val pr_typechecks = 
    24.8 -    nat_typechecks @ list.intrs @ 
    24.9 -    [lam_type, list_case_type, drop_type, map_type, 
   24.10 -     apply_type, rec_type];
   24.11 -
   24.12  (** Useful special cases of evaluation ***)
   24.13  
   24.14 -simpset_ref() := simpset() setSolver (type_auto_tac pr_typechecks);
   24.15 -
   24.16 -Goalw [SC_def]
   24.17 -    "[| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
   24.18 +Goalw [SC_def] "[| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
   24.19  by (Asm_simp_tac 1);
   24.20  qed "SC";
   24.21  
   24.22 -Goalw [CONST_def]
   24.23 -    "[| l: list(nat) |] ==> CONST(k) ` l = k";
   24.24 +Goalw [CONST_def] "[| l: list(nat) |] ==> CONST(k) ` l = k";
   24.25  by (Asm_simp_tac 1);
   24.26  qed "CONST";
   24.27  
   24.28 -Goalw [PROJ_def]
   24.29 -    "[| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
   24.30 +Goalw [PROJ_def] "[| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
   24.31  by (Asm_simp_tac 1);
   24.32  qed "PROJ_0";
   24.33  
   24.34 -Goalw [COMP_def]
   24.35 -    "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
   24.36 +Goalw [COMP_def] "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
   24.37  by (Asm_simp_tac 1);
   24.38  qed "COMP_1";
   24.39  
   24.40 -Goalw [PREC_def]
   24.41 -    "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
   24.42 +Goalw [PREC_def] "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
   24.43  by (Asm_simp_tac 1);
   24.44  qed "PREC_0";
   24.45  
    25.1 --- a/src/ZF/ex/TF.ML	Mon Jan 25 20:35:19 1999 +0100
    25.2 +++ b/src/ZF/ex/TF.ML	Wed Jan 27 10:31:31 1999 +0100
    25.3 @@ -7,6 +7,7 @@
    25.4  *)
    25.5  
    25.6  Addsimps tree_forest.intrs;
    25.7 +AddTCs   tree_forest.intrs;
    25.8  
    25.9  (** tree_forest(A) as the union of tree(A) and forest(A) **)
   25.10  
    26.1 --- a/src/ZF/ex/Term.ML	Mon Jan 25 20:35:19 1999 +0100
    26.2 +++ b/src/ZF/ex/Term.ML	Wed Jan 27 10:31:31 1999 +0100
    26.3 @@ -171,14 +171,11 @@
    26.4  
    26.5  (** Term simplification **)
    26.6  
    26.7 -val term_typechecks =
    26.8 -    [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
    26.9 -     reflect_type, preorder_type, postorder_type];
   26.10 +AddTCs [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
   26.11 +	reflect_type, preorder_type, postorder_type];
   26.12  
   26.13  (*map_type2 and term_map_type2 instantiate variables*)
   26.14 -simpset_ref() := simpset()
   26.15 -      addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]
   26.16 -      setSolver type_auto_tac (list_typechecks@term_typechecks);
   26.17 +Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder];
   26.18  
   26.19  
   26.20  (** theorems about term_map **)
    27.1 --- a/src/ZF/func.ML	Mon Jan 25 20:35:19 1999 +0100
    27.2 +++ b/src/ZF/func.ML	Wed Jan 27 10:31:31 1999 +0100
    27.3 @@ -104,6 +104,7 @@
    27.4  by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
    27.5  by (REPEAT (ares_tac [apply_Pair] 1));
    27.6  qed "apply_type";
    27.7 +AddTCs [apply_type];
    27.8  
    27.9  (*This version is acceptable to the simplifier*)
   27.10  Goal "[| f: A->B;  a:A |] ==> f`a : B"; 
   27.11 @@ -165,6 +166,7 @@
   27.12      "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";  
   27.13  by (blast_tac (claset() addIs prems) 1);
   27.14  qed "lam_type";
   27.15 +AddTCs [lam_type];
   27.16  
   27.17  Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
   27.18  by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
    28.1 --- a/src/ZF/pair.ML	Mon Jan 25 20:35:19 1999 +0100
    28.2 +++ b/src/ZF/pair.ML	Wed Jan 27 10:31:31 1999 +0100
    28.3 @@ -63,6 +63,7 @@
    28.4  qed_goal "SigmaI" thy
    28.5      "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    28.6   (fn _ => [ Asm_simp_tac 1 ]);
    28.7 +AddTCs [SigmaI];
    28.8  
    28.9  bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);
   28.10  bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
   28.11 @@ -147,6 +148,7 @@
   28.12   (fn major::prems=>
   28.13    [ (rtac (major RS SigmaE) 1),
   28.14      (asm_simp_tac (simpset() addsimps prems) 1) ]);
   28.15 +AddTCs [split_type];
   28.16  
   28.17  Goalw [split_def]
   28.18    "u: A*B ==>   \
    29.1 --- a/src/ZF/simpdata.ML	Mon Jan 25 20:35:19 1999 +0100
    29.2 +++ b/src/ZF/simpdata.ML	Wed Jan 27 10:31:31 1999 +0100
    29.3 @@ -106,6 +106,7 @@
    29.4  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    29.5  
    29.6  simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    29.7 -                           addsplits [split_if];
    29.8 +                           addsplits [split_if]
    29.9 +                           setSolver Type_solver_tac;
   29.10  
   29.11  val ZF_ss = simpset();
    30.1 --- a/src/ZF/upair.ML	Mon Jan 25 20:35:19 1999 +0100
    30.2 +++ b/src/ZF/upair.ML	Wed Jan 27 10:31:31 1999 +0100
    30.3 @@ -141,6 +141,8 @@
    30.4   (fn _ => [ Simp_tac 1 ]);
    30.5  
    30.6  Addsimps [consI1];
    30.7 +AddTCs   [consI1];   (*risky as a typechecking rule, but solves otherwise
    30.8 +		       unconstrained goals of the form  x : ?A*)
    30.9  
   30.10  qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
   30.11   (fn _ => [ Asm_simp_tac 1 ]);
   30.12 @@ -288,7 +290,7 @@
   30.13      "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A"
   30.14   (fn prems=> [ (simp_tac 
   30.15                  (simpset() addsimps prems addsplits [split_if]) 1) ]);
   30.16 -
   30.17 +AddTCs [if_type];
   30.18  
   30.19  (*** Foundation lemmas ***)
   30.20  
    31.1 --- a/src/ZF/upair.thy	Mon Jan 25 20:35:19 1999 +0100
    31.2 +++ b/src/ZF/upair.thy	Wed Jan 27 10:31:31 1999 +0100
    31.3 @@ -6,4 +6,10 @@
    31.4  Dummy theory, but holds the standard ZF simpset.
    31.5  *)
    31.6  
    31.7 -upair = ZF
    31.8 +upair = ZF +
    31.9 +
   31.10 +setup
   31.11 +  TypeCheck.setup
   31.12 +
   31.13 +end
   31.14 +