--- a/src/ZF/AC/Cardinal_aux.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML Wed Jan 27 10:31:31 1999 +0100
@@ -142,8 +142,7 @@
by (rtac impE 1 THEN (assume_tac 3));
by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2
THEN (TRYALL assume_tac));
-by (Simp_tac 2);
-by (Asm_full_simp_tac 1);
+by Auto_tac;
qed "UN_lepoll";
Goal "Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))";
--- a/src/ZF/AC/WO6_WO1.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Wed Jan 27 10:31:31 1999 +0100
@@ -8,8 +8,6 @@
pages 2-5
*)
-open WO6_WO1;
-
goal OrderType.thy
"!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> \
\ k < i | (~ k<i & k = i ++ (k--i) & (k--i)<j)";
@@ -143,7 +141,7 @@
by (Blast_tac 1);
by (rtac vv1_subset 1);
by (dtac (ospec RS mp) 1);
-by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
+by (REPEAT (eresolve_tac [asm_rl, oexE, conjE] 1));
by (asm_simp_tac (simpset()
addsimps [vv1_def, Let_def, lt_Ord,
nested_Least_instance RS conjunct1]) 1);
--- a/src/ZF/Arith.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Arith.ML Wed Jan 27 10:31:31 1999 +0100
@@ -35,6 +35,7 @@
by Auto_tac;
qed "add_type";
Addsimps [add_type];
+AddTCs [add_type];
(** Multiplication **)
@@ -43,6 +44,7 @@
by Auto_tac;
qed "mult_type";
Addsimps [mult_type];
+AddTCs [mult_type];
(** Difference **)
@@ -53,6 +55,7 @@
by (fast_tac (claset() addIs [nat_case_type]) 1);
qed "diff_type";
Addsimps [diff_type];
+AddTCs [diff_type];
Goal "n:nat ==> 0 #- n = 0";
by (induct_tac "n" 1);
@@ -288,6 +291,7 @@
Goalw [mod_def] "[| 0<n; m:nat; n:nat |] ==> m mod n : nat";
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
qed "mod_type";
+AddTCs [mod_type];
Goal "[| 0<n; m<n |] ==> m mod n = m";
by (rtac (mod_def RS def_transrec RS trans) 1);
@@ -309,6 +313,7 @@
"[| 0<n; m:nat; n:nat |] ==> m div n : nat";
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
qed "div_type";
+AddTCs [div_type];
Goal "[| 0<n; m<n |] ==> m div n = 0";
by (rtac (div_def RS def_transrec RS trans) 1);
--- a/src/ZF/Bool.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Bool.ML Wed Jan 27 10:31:31 1999 +0100
@@ -6,8 +6,6 @@
Booleans in Zermelo-Fraenkel Set Theory
*)
-open Bool;
-
val bool_defs = [bool_def,cond_def];
Goalw [succ_def] "{0} = 1";
@@ -25,6 +23,7 @@
qed "bool_0I";
Addsimps [bool_1I, bool_0I];
+AddTCs [bool_1I, bool_0I];
Goalw bool_defs "1~=0";
by (rtac succ_not_0 1);
@@ -59,12 +58,12 @@
Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
by (bool_tac 1);
qed "cond_type";
+AddTCs [cond_type];
(*For Simp_tac and Blast_tac*)
Goal "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A";
by (bool_tac 1);
qed "cond_simple_type";
-Addsimps [cond_simple_type];
val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
by (rewtac rew);
@@ -85,25 +84,25 @@
Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
-qed_goalw "not_type" Bool.thy [not_def]
- "a:bool ==> not(a) : bool"
- (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
+Goalw [not_def] "a:bool ==> not(a) : bool";
+by (Asm_simp_tac 1);
+qed "not_type";
-qed_goalw "and_type" Bool.thy [and_def]
- "[| a:bool; b:bool |] ==> a and b : bool"
- (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
+Goalw [and_def] "[| a:bool; b:bool |] ==> a and b : bool";
+by (Asm_simp_tac 1);
+qed "and_type";
-qed_goalw "or_type" Bool.thy [or_def]
- "[| a:bool; b:bool |] ==> a or b : bool"
- (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
+Goalw [or_def] "[| a:bool; b:bool |] ==> a or b : bool";
+by (Asm_simp_tac 1);
+qed "or_type";
-Addsimps [not_type, and_type, or_type];
+AddTCs [not_type, and_type, or_type];
-qed_goalw "xor_type" Bool.thy [xor_def]
- "[| a:bool; b:bool |] ==> a xor b : bool"
- (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
+Goalw [xor_def] "[| a:bool; b:bool |] ==> a xor b : bool";
+by (Asm_simp_tac 1);
+qed "xor_type";
-Addsimps [xor_type];
+AddTCs [xor_type];
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type,
or_type, xor_type];
--- a/src/ZF/CardinalArith.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/CardinalArith.ML Wed Jan 27 10:31:31 1999 +0100
@@ -11,8 +11,6 @@
coincide with union (maximum). Either way we get most laws for free.
*)
-open CardinalArith;
-
(*** Cardinal addition ***)
(** Cardinal addition is commutative **)
@@ -65,7 +63,7 @@
Goalw [lepoll_def, inj_def] "A lepoll A+B";
by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1);
-by (asm_simp_tac (simpset() addsimps [lam_type]) 1);
+by (Asm_simp_tac 1);
qed "sum_lepoll_self";
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
@@ -86,7 +84,7 @@
by (res_inst_tac
[("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")]
lam_injective 1);
-by (typechk_tac ([inj_is_fun, case_type, InlI, InrI] @ ZF_typechecks));
+by (typecheck_tac (tcset() addTCs [inj_is_fun]));
by (etac sumE 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [left_inverse])));
qed "sum_lepoll_mono";
@@ -216,7 +214,7 @@
Goalw [lepoll_def, inj_def] "A lepoll A*A";
by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1);
-by (simp_tac (simpset() addsimps [lam_type]) 1);
+by (Simp_tac 1);
qed "prod_square_lepoll";
(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
@@ -233,7 +231,7 @@
Goalw [lepoll_def, inj_def] "b: B ==> A lepoll A*B";
by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1);
-by (asm_simp_tac (simpset() addsimps [lam_type]) 1);
+by (Asm_simp_tac 1);
qed "prod_lepoll_self";
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
@@ -252,7 +250,7 @@
by (res_inst_tac [("x", "lam <w,y>:A*B. <f`w, fa`y>")] exI 1);
by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")]
lam_injective 1);
-by (typechk_tac (inj_is_fun::ZF_typechecks));
+by (typecheck_tac (tcset() addTCs [inj_is_fun]));
by (etac SigmaE 1);
by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
qed "prod_lepoll_mono";
@@ -295,7 +293,7 @@
Goal "Card(n) ==> 2 |*| n = n |+| n";
by (asm_simp_tac
- (simpset() addsimps [Ord_0, Ord_succ, cmult_succ_lemma, Card_is_Ord,
+ (simpset() addsimps [cmult_succ_lemma, Card_is_Ord,
read_instantiate [("j","0")] cadd_commute]) 1);
qed "cmult_2";
@@ -552,7 +550,7 @@
(*Corollary 10.13 (1), for cardinal multiplication*)
Goal "[| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L";
by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
-by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
+by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord]));
by (resolve_tac [cmult_commute RS ssubst] 1);
by (resolve_tac [Un_commute RS ssubst] 1);
by (ALLGOALS
@@ -561,13 +559,12 @@
subset_Un_iff2 RS iffD1, le_imp_subset])));
qed "InfCard_cmult_eq";
-(*This proof appear to be the simplest!*)
Goal "InfCard(K) ==> K |+| K = K";
by (asm_simp_tac
(simpset() addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1);
-by (rtac InfCard_le_cmult_eq 1);
-by (typechk_tac [Ord_0, le_refl, leI]);
-by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]);
+by (asm_simp_tac
+ (simpset() addsimps [InfCard_le_cmult_eq, InfCard_is_Limit,
+ Limit_has_0, Limit_has_succ]) 1);
qed "InfCard_cdouble_eq";
(*Corollary 10.13 (1), for cardinal addition*)
@@ -582,7 +579,7 @@
Goal "[| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L";
by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
-by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
+by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord]));
by (resolve_tac [cadd_commute RS ssubst] 1);
by (resolve_tac [Un_commute RS ssubst] 1);
by (ALLGOALS
--- a/src/ZF/Cardinal_AC.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Cardinal_AC.ML Wed Jan 27 10:31:31 1999 +0100
@@ -8,8 +8,6 @@
These results help justify infinite-branching datatypes
*)
-open Cardinal_AC;
-
(*** Strengthened versions of existing theorems about cardinals ***)
Goal "|A| eqpoll A";
@@ -118,19 +116,21 @@
by (subgoal_tac
"ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
by (fast_tac (claset() addSIs [Least_le RS lt_trans1 RS ltD, ltI]
- addSEs [LeastI, Ord_in_Ord]) 2);
+ addSEs [LeastI, Ord_in_Ord]) 2);
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
("d", "%<i,j>. converse(f`i) ` j")]
lam_injective 1);
(*Instantiate the lemma proved above*)
by (ALLGOALS ball_tac);
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]
- addDs [apply_type]) 1);
+ addDs [apply_type]) 1);
by (dtac apply_type 1);
by (etac conjunct2 1);
by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
qed "cardinal_UN_le";
+
+
(*The same again, using csucc*)
Goal "[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \
\ |UN i:K. X(i)| < csucc(K)";
--- a/src/ZF/Integ/Bin.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Integ/Bin.ML Wed Jan 27 10:31:31 1999 +0100
@@ -7,18 +7,17 @@
*)
-Addsimps bin.intrs;
-Addsimps int_typechecks;
+AddTCs bin.intrs;
Goal "NCons(Pls,0) = Pls";
by (Asm_simp_tac 1);
qed "NCons_Pls_0";
-Goal "NCons(Pls,1) = Cons(Pls,1)";
+Goal "NCons(Pls,1) = Pls BIT 1";
by (Asm_simp_tac 1);
qed "NCons_Pls_1";
-Goal "NCons(Min,0) = Cons(Min,0)";
+Goal "NCons(Min,0) = Min BIT 0";
by (Asm_simp_tac 1);
qed "NCons_Min_0";
@@ -26,49 +25,47 @@
by (Asm_simp_tac 1);
qed "NCons_Min_1";
-Goal "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
+Goal "NCons(w BIT x,b) = w BIT x BIT b";
by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
-qed "NCons_Cons";
+qed "NCons_BIT";
val NCons_simps = [NCons_Pls_0, NCons_Pls_1,
NCons_Min_0, NCons_Min_1,
- NCons_Cons];
+ NCons_BIT];
Addsimps NCons_simps;
(** Type checking **)
-Addsimps [bool_into_nat];
-
Goal "w: bin ==> integ_of(w) : int";
by (induct_tac "w" 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [bool_into_nat])));
qed "integ_of_type";
-Addsimps [integ_of_type];
+AddTCs [integ_of_type];
Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
by (induct_tac "w" 1);
by Auto_tac;
qed "NCons_type";
-Addsimps [NCons_type];
+AddTCs [NCons_type];
Goal "w: bin ==> bin_succ(w) : bin";
by (induct_tac "w" 1);
by Auto_tac;
qed "bin_succ_type";
-Addsimps [bin_succ_type];
+AddTCs [bin_succ_type];
Goal "w: bin ==> bin_pred(w) : bin";
by (induct_tac "w" 1);
by Auto_tac;
qed "bin_pred_type";
-Addsimps [bin_pred_type];
+AddTCs [bin_pred_type];
Goal "w: bin ==> bin_minus(w) : bin";
by (induct_tac "w" 1);
by Auto_tac;
qed "bin_minus_type";
-Addsimps [bin_minus_type];
+AddTCs [bin_minus_type];
(*This proof is complicated by the mutual recursion*)
Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
@@ -76,22 +73,22 @@
by (rtac ballI 3);
by (rename_tac "w'" 3);
by (induct_tac "w'" 3);
-by Auto_tac;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [NCons_type])));
qed_spec_mp "bin_add_type";
-Addsimps [bin_add_type];
+AddTCs [bin_add_type];
Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
by (induct_tac "v" 1);
by Auto_tac;
qed "bin_mult_type";
-Addsimps [bin_mult_type];
+AddTCs [bin_mult_type];
(**** The carry/borrow functions, bin_succ and bin_pred ****)
(*NCons preserves the integer value of its argument*)
Goal "[| w: bin; b: bool |] ==> \
-\ integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
+\ integ_of(NCons(w,b)) = integ_of(w BIT b)";
by (etac bin.elim 1);
by (Asm_simp_tac 3);
by (ALLGOALS (etac boolE));
@@ -130,8 +127,6 @@
(asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib])));
qed "integ_of_minus";
-Addsimps [integ_of_minus];
-
(*** bin_add: binary addition ***)
@@ -143,22 +138,22 @@
by (Asm_simp_tac 1);
qed "bin_add_Min";
-Goal "bin_add(Cons(v,x),Pls) = Cons(v,x)";
+Goal "bin_add(v BIT x,Pls) = v BIT x";
by (Simp_tac 1);
-qed "bin_add_Cons_Pls";
+qed "bin_add_BIT_Pls";
-Goal "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
+Goal "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
by (Simp_tac 1);
-qed "bin_add_Cons_Min";
+qed "bin_add_BIT_Min";
Goal "[| w: bin; y: bool |] \
-\ ==> bin_add(Cons(v,x), Cons(w,y)) = \
+\ ==> bin_add(v BIT x, w BIT y) = \
\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
by (Asm_simp_tac 1);
-qed "bin_add_Cons_Cons";
+qed "bin_add_BIT_BIT";
-Addsimps [bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
- bin_add_Cons_Min, bin_add_Cons_Cons,
+Addsimps [bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
+ bin_add_BIT_Min, bin_add_BIT_BIT,
integ_of_succ, integ_of_pred];
Goal "v: bin ==> \
@@ -170,7 +165,6 @@
by (induct_tac "wa" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
qed_spec_mp "integ_of_add";
-Addsimps [integ_of_add];
(*** bin_add: binary multiplication ***)
@@ -179,87 +173,90 @@
\ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
by (induct_tac "v" 1);
by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [integ_of_minus]) 1);
by (etac boolE 1);
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
-by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1);
+by (asm_simp_tac (simpset() addsimps [integ_of_add,
+ zadd_zmult_distrib] @ zadd_ac) 1);
qed "integ_of_mult";
(**** Computations ****)
(** extra rules for bin_succ, bin_pred **)
-Goal "bin_succ(Cons(w,1)) = Cons(bin_succ(w), 0)";
+Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
by (Simp_tac 1);
-qed "bin_succ_Cons1";
+qed "bin_succ_BIT1";
-Goal "bin_succ(Cons(w,0)) = NCons(w,1)";
+Goal "bin_succ(w BIT 0) = NCons(w,1)";
by (Simp_tac 1);
-qed "bin_succ_Cons0";
+qed "bin_succ_BIT0";
-Goal "bin_pred(Cons(w,1)) = NCons(w,0)";
+Goal "bin_pred(w BIT 1) = NCons(w,0)";
by (Simp_tac 1);
-qed "bin_pred_Cons1";
+qed "bin_pred_BIT1";
-Goal "bin_pred(Cons(w,0)) = Cons(bin_pred(w), 1)";
+Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
by (Simp_tac 1);
-qed "bin_pred_Cons0";
+qed "bin_pred_BIT0";
(** extra rules for bin_minus **)
-Goal "bin_minus(Cons(w,1)) = bin_pred(NCons(bin_minus(w), 0))";
+Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
by (Simp_tac 1);
-qed "bin_minus_Cons1";
+qed "bin_minus_BIT1";
-Goal "bin_minus(Cons(w,0)) = Cons(bin_minus(w), 0)";
+Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
by (Simp_tac 1);
-qed "bin_minus_Cons0";
+qed "bin_minus_BIT0";
(** extra rules for bin_add **)
-Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,1)) = \
+Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
\ NCons(bin_add(v, bin_succ(w)), 0)";
by (Asm_simp_tac 1);
-qed "bin_add_Cons_Cons11";
+qed "bin_add_BIT_BIT11";
-Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,0)) = \
+Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) = \
\ NCons(bin_add(v,w), 1)";
by (Asm_simp_tac 1);
-qed "bin_add_Cons_Cons10";
+qed "bin_add_BIT_BIT10";
Goal "[| w: bin; y: bool |] ==> \
-\ bin_add(Cons(v,0), Cons(w,y)) = NCons(bin_add(v,w), y)";
+\ bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
by (Asm_simp_tac 1);
-qed "bin_add_Cons_Cons0";
+qed "bin_add_BIT_BIT0";
(** extra rules for bin_mult **)
-Goal "bin_mult(Cons(v,1), w) = bin_add(NCons(bin_mult(v,w),0), w)";
+Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
by (Simp_tac 1);
-qed "bin_mult_Cons1";
+qed "bin_mult_BIT1";
-Goal "bin_mult(Cons(v,0), w) = NCons(bin_mult(v,w),0)";
+Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
by (Simp_tac 1);
-qed "bin_mult_Cons0";
+qed "bin_mult_BIT0";
-(*** The computation simpset ***)
+(*Delete the original rewrites, with their clumsy conditional expressions*)
+Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,
+ NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
+
+(*Hide the binary representation of integer constants*)
+Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
+
-(*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
-val bin_comp_ss = simpset_of Int.thy
- addsimps [integ_of_add RS sym, (*invoke bin_add*)
- integ_of_minus RS sym, (*invoke bin_minus*)
- integ_of_mult RS sym, (*invoke bin_mult*)
- bin_succ_Pls, bin_succ_Min,
- bin_succ_Cons1, bin_succ_Cons0,
- bin_pred_Pls, bin_pred_Min,
- bin_pred_Cons1, bin_pred_Cons0,
- bin_minus_Pls, bin_minus_Min,
- bin_minus_Cons1, bin_minus_Cons0,
- bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
- bin_add_Cons_Min, bin_add_Cons_Cons0,
- bin_add_Cons_Cons10, bin_add_Cons_Cons11,
- bin_mult_Pls, bin_mult_Min,
- bin_mult_Cons1, bin_mult_Cons0]
- @ NCons_simps
- setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin.intrs));
+Addsimps [integ_of_add RS sym, (*invoke bin_add*)
+ integ_of_minus RS sym, (*invoke bin_minus*)
+ integ_of_mult RS sym, (*invoke bin_mult*)
+ bin_succ_Pls, bin_succ_Min,
+ bin_succ_BIT1, bin_succ_BIT0,
+ bin_pred_Pls, bin_pred_Min,
+ bin_pred_BIT1, bin_pred_BIT0,
+ bin_minus_Pls, bin_minus_Min,
+ bin_minus_BIT1, bin_minus_BIT0,
+ bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
+ bin_add_BIT_Min, bin_add_BIT_BIT0,
+ bin_add_BIT_BIT10, bin_add_BIT_BIT11,
+ bin_mult_Pls, bin_mult_Min,
+ bin_mult_BIT1, bin_mult_BIT0];
--- a/src/ZF/Integ/Bin.thy Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Integ/Bin.thy Wed Jan 27 10:31:31 1999 +0100
@@ -24,7 +24,7 @@
datatype
"bin" = Pls
| Min
- | Cons ("w: bin", "b: bool")
+ | BIT ("w: bin", "b: bool") (infixl 90)
syntax
"_Int" :: xnum => i ("_")
@@ -40,60 +40,59 @@
bin_mult :: [i,i]=>i
primrec
- "integ_of (Pls) = $# 0"
- "integ_of (Min) = $~($#1)"
- "integ_of (Cons(w,b)) = $#b $+ integ_of(w) $+ integ_of(w)"
+ integ_of_Pls "integ_of (Pls) = $# 0"
+ integ_of_Min "integ_of (Min) = $~($#1)"
+ integ_of_BIT "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
- "NCons (Pls,b) = cond(b,Cons(Pls,b),Pls)"
- "NCons (Min,b) = cond(b,Min,Cons(Min,b))"
- "NCons (Cons(w,c),b) = Cons(Cons(w,c),b)"
+ NCons_Pls "NCons (Pls,b) = cond(b,Pls BIT b,Pls)"
+ NCons_Min "NCons (Min,b) = cond(b,Min,Min BIT b)"
+ NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
-primrec (*successor. If a Cons, can change a 0 to a 1 without recursion.*)
- bin_succ_Pls
- "bin_succ (Pls) = Cons(Pls,1)"
- bin_succ_Min
- "bin_succ (Min) = Pls"
- "bin_succ (Cons(w,b)) = cond(b, Cons(bin_succ(w), 0),
- NCons(w,1))"
+primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*)
+ bin_succ_Pls "bin_succ (Pls) = Pls BIT 1"
+ bin_succ_Min "bin_succ (Min) = Pls"
+ bin_succ_BIT "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
primrec (*predecessor*)
- bin_pred_Pls
- "bin_pred (Pls) = Min"
- bin_pred_Min
- "bin_pred (Min) = Cons(Min,0)"
- "bin_pred (Cons(w,b)) = cond(b, NCons(w,0),
- Cons(bin_pred(w), 1))"
+ bin_pred_Pls "bin_pred (Pls) = Min"
+ bin_pred_Min "bin_pred (Min) = Min BIT 0"
+ bin_pred_BIT "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
primrec (*unary negation*)
bin_minus_Pls
"bin_minus (Pls) = Pls"
bin_minus_Min
- "bin_minus (Min) = Cons(Pls,1)"
- "bin_minus (Cons(w,b)) = cond(b, bin_pred(NCons(bin_minus(w),0)),
- Cons(bin_minus(w),0))"
+ "bin_minus (Min) = Pls BIT 1"
+ bin_minus_BIT
+ "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
+ bin_minus(w) BIT 0)"
(*Mutual recursion is not always sound, but it is for primitive recursion.*)
primrec (*sum*)
- "bin_add (Pls,w) = w"
- "bin_add (Min,w) = bin_pred(w)"
- "bin_add (Cons(v,x),w) = adding(v,x,w)"
+ bin_add_Pls
+ "bin_add (Pls,w) = w"
+ bin_add_Min
+ "bin_add (Min,w) = bin_pred(w)"
+ bin_add_BIT
+ "bin_add (v BIT x,w) = adding(v,x,w)"
primrec (*auxilliary function for sum*)
- "adding (v,x,Pls) = Cons(v,x)"
- "adding (v,x,Min) = bin_pred(Cons(v,x))"
- "adding (v,x,Cons(w,y)) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)),
- x xor y)"
+ "adding (v,x,Pls) = v BIT x"
+ "adding (v,x,Min) = bin_pred(v BIT x)"
+ "adding (v,x,w BIT y) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)),
+ x xor y)"
primrec
bin_mult_Pls
- "bin_mult (Pls,w) = Pls"
+ "bin_mult (Pls,w) = Pls"
bin_mult_Min
- "bin_mult (Min,w) = bin_minus(w)"
- "bin_mult (Cons(v,b),w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
- NCons(bin_mult(v,w),0))"
+ "bin_mult (Min,w) = bin_minus(w)"
+ bin_mult_BIT
+ "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
+ NCons(bin_mult(v,w),0))"
end
@@ -138,7 +137,7 @@
fun term_of [] = const "Pls"
| term_of [~1] = const "Min"
- | term_of (b :: bs) = const "Cons" $ term_of bs $ mk_bit b;
+ | term_of (b :: bs) = const "op BIT" $ term_of bs $ mk_bit b;
in
term_of (bin_of (sign * (#1 (read_int digs))))
end;
@@ -147,7 +146,7 @@
let
fun bin_of (Const ("Pls", _)) = []
| bin_of (Const ("Min", _)) = [~1]
- | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
fun integ_of [] = 0
--- a/src/ZF/Integ/EquivClass.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Integ/EquivClass.ML Wed Jan 27 10:31:31 1999 +0100
@@ -94,6 +94,7 @@
Goalw [quotient_def] "x:A ==> r``{x}: A/r";
by (etac RepFunI 1);
qed "quotientI";
+AddTCs [quotientI];
val major::prems = Goalw [quotient_def]
"[| X: A/r; !!x. [| X = r``{x}; x:A |] ==> P |] \
--- a/src/ZF/Integ/Int.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Integ/Int.ML Wed Jan 27 10:31:31 1999 +0100
@@ -20,13 +20,14 @@
val eqa::eqb::prems = goal Arith.thy
"[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \
\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1";
+by (cut_facts_tac prems 1);
by (res_inst_tac [("k","x2")] add_left_cancel 1);
-by (resolve_tac prems 2);
-by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
+by (rtac (add_left_commute RS trans) 1);
+by Auto_tac;
by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
-by (stac eqa 1);
-by (rtac (add_left_commute) 1 THEN typechk_tac prems);
+by (rtac (add_left_commute RS trans) 1);
+by (stac eqa 3);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
qed "int_trans_lemma";
(** Natural deduction for intrel **)
@@ -79,15 +80,15 @@
Goalw [int_def,quotient_def,int_of_def]
"m : nat ==> $#m : int";
-by (fast_tac (claset() addSIs [nat_0I]) 1);
+by Auto_tac;
qed "int_of_type";
Addsimps [int_of_type];
+AddTCs [int_of_type];
Goalw [int_of_def] "[| $#m = $#n; m: nat |] ==> m=n";
by (dtac (sym RS eq_intrelD) 1);
-by (typechk_tac [nat_0I, SigmaI]);
-by (Asm_full_simp_tac 1);
+by Auto_tac;
qed "int_of_inject";
AddSDs [int_of_inject];
@@ -108,9 +109,9 @@
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
Goalw [int_def,zminus_def] "z : int ==> $~z : int";
-by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
- quotientI]);
+by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
qed "zminus_type";
+AddTCs [zminus_type];
Goalw [int_def,zminus_def] "[| $~z = $~w; z: int; w: int |] ==> z=w";
by (etac (zminus_ize UN_equiv_class_inject) 1);
@@ -160,7 +161,7 @@
Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
-be natE 1;
+by (etac natE 1);
by (dres_inst_tac [("x","0")] spec 2);
by Auto_tac;
qed "not_znegative_imp_zero";
@@ -178,9 +179,10 @@
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
Goalw [zmagnitude_def] "zmagnitude(z) : nat";
-br theI2 1;
+by (rtac theI2 1);
by Auto_tac;
qed "zmagnitude_type";
+AddTCs [zmagnitude_type];
Goalw [int_def, znegative_def, int_of_def]
"[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n";
@@ -188,14 +190,14 @@
by (rename_tac "i j" 1);
by (dres_inst_tac [("x", "i")] spec 1);
by (dres_inst_tac [("x", "j")] spec 1);
-br bexI 1;
-br (add_diff_inverse2 RS sym) 1;
+by (rtac bexI 1);
+by (rtac (add_diff_inverse2 RS sym) 1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
qed "not_zneg_int_of";
Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z";
-bd not_zneg_int_of 1;
+by (dtac not_zneg_int_of 1);
by Auto_tac;
qed "not_zneg_mag";
@@ -214,7 +216,7 @@
qed "zneg_int_of";
Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z";
-bd zneg_int_of 1;
+by (dtac zneg_int_of 1);
by Auto_tac;
qed "zneg_mag";
@@ -236,7 +238,7 @@
add_ac does not help rewriting with the assumptions.*)
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
-by (typechk_tac [add_type]);
+by Auto_tac;
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
qed "zadd_congruent2";
@@ -248,6 +250,7 @@
by (simp_tac (simpset() addsimps [Let_def]) 3);
by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
qed "zadd_type";
+AddTCs [zadd_type];
Goalw [zadd_def]
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
@@ -282,7 +285,8 @@
(*For AC rewriting*)
Goal "[| z1:int; z2:int; z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
qed "zadd_left_commute";
(*Integer addition is an AC operator*)
@@ -343,6 +347,7 @@
split_type, add_type, mult_type,
quotientI, SigmaI] 1));
qed "zmult_type";
+AddTCs [zmult_type];
Goalw [zmult_def]
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
@@ -389,7 +394,8 @@
(*For AC rewriting*)
Goal "[| z1:int; z2:int; z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
-by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
qed "zmult_left_commute";
(*Integer multiplication is an AC operator*)
--- a/src/ZF/List.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/List.ML Wed Jan 27 10:31:31 1999 +0100
@@ -166,9 +166,7 @@
[list_rec_type, map_type, map_type2, app_type, length_type,
rev_type, flat_type, list_add_type];
-Addsimps list_typechecks;
-
-simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks);
+AddTCs list_typechecks;
(*** theorems about map ***)
--- a/src/ZF/Nat.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Nat.ML Wed Jan 27 10:31:31 1999 +0100
@@ -6,8 +6,6 @@
Natural numbers in Zermelo-Fraenkel Set Theory
*)
-open Nat;
-
Goal "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2));
@@ -40,10 +38,10 @@
Addsimps [nat_0I, nat_1I, nat_2I];
AddSIs [nat_0I, nat_1I, nat_2I, nat_succI];
+AddTCs [nat_0I, nat_1I, nat_2I, nat_succI];
Goal "bool <= nat";
-by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
- ORELSE eresolve_tac [boolE,ssubst] 1));
+by (blast_tac (claset() addSEs [boolE]) 1);
qed "bool_subset_nat";
val bool_into_nat = bool_subset_nat RS subsetD;
--- a/src/ZF/Order.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Order.ML Wed Jan 27 10:31:31 1999 +0100
@@ -253,8 +253,8 @@
(*Rewriting with bijections and converse (function inverse)*)
val bij_inverse_ss =
- simpset() setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type,
- bij_converse_bij, comp_fun, comp_bij])
+ simpset() setSolver
+ type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_fun, comp_fun, comp_bij])
addsimps [right_inverse_bij, left_inverse_bij];
(** Symmetry and Transitivity Rules **)
@@ -266,23 +266,22 @@
qed "ord_iso_refl";
(*Symmetry of similarity*)
-Goalw [ord_iso_def]
- "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
-by (fast_tac (claset() addss bij_inverse_ss) 1);
+Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
+by (force_tac (claset(), bij_inverse_ss) 1);
qed "ord_iso_sym";
(*Transitivity of similarity*)
Goalw [mono_map_def]
"[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \
\ (f O g): mono_map(A,r,C,t)";
-by (fast_tac (claset() addss bij_inverse_ss) 1);
+by (force_tac (claset(), bij_inverse_ss) 1);
qed "mono_map_trans";
(*Transitivity of similarity: the order-isomorphism relation*)
Goalw [ord_iso_def]
"[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \
\ (f O g): ord_iso(A,r,C,t)";
-by (fast_tac (claset() addss bij_inverse_ss) 1);
+by (force_tac (claset(), bij_inverse_ss) 1);
qed "ord_iso_trans";
(** Two monotone maps can make an order-isomorphism **)
@@ -373,16 +372,16 @@
(*Simple consequence of Lemma 6.1*)
Goal "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \
-\ a:A; c:A |] ==> a=c";
+\ a:A; c:A |] ==> a=c";
by (forward_tac [well_ord_is_trans_on] 1);
by (forward_tac [well_ord_is_linear] 1);
by (linear_case_tac 1);
by (dtac ord_iso_sym 1);
-by (REPEAT (*because there are two symmetric cases*)
- (EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS
- well_ord_iso_predE] 1,
- blast_tac (claset() addSIs [predI]) 2,
- asm_simp_tac (simpset() addsimps [trans_pred_pred_eq]) 1]));
+(*two symmetric cases*)
+by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS
+ well_ord_iso_predE]
+ addSIs [predI],
+ simpset() addsimps [trans_pred_pred_eq]));
qed "well_ord_iso_pred_eq";
(*Does not assume r is a wellordering!*)
--- a/src/ZF/OrderType.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/OrderType.ML Wed Jan 27 10:31:31 1999 +0100
@@ -10,8 +10,6 @@
*)
-open OrderType;
-
(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
@@ -499,8 +497,8 @@
qed "oadd_1";
Goal "[| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)";
- (*ZF_ss prevents looping*)
-by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
+ (*FOL_ss prevents looping*)
+by (asm_simp_tac (FOL_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
qed "oadd_succ";
@@ -766,8 +764,8 @@
qed "oadd_omult_distrib";
Goal "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i";
- (*ZF_ss prevents looping*)
-by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
+ (*FOL_ss prevents looping*)
+by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym]) 1);
by (asm_simp_tac
(simpset() addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
qed "omult_succ";
--- a/src/ZF/Ordinal.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Ordinal.ML Wed Jan 27 10:31:31 1999 +0100
@@ -6,8 +6,6 @@
Ordinals in Zermelo-Fraenkel Set Theory
*)
-open Ordinal;
-
(*** Rules for Transset ***)
(** Two neat characterisations of Transset **)
@@ -149,6 +147,7 @@
Addsimps [Ord_0, Ord_succ_iff];
AddSIs [Ord_0, Ord_succ];
+AddTCs [Ord_0, Ord_succ];
Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Un j)";
by (blast_tac (claset() addSIs [Transset_Un]) 1);
@@ -157,6 +156,7 @@
Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Int j)";
by (blast_tac (claset() addSIs [Transset_Int]) 1);
qed "Ord_Int";
+AddTCs [Ord_Un, Ord_Int];
val nonempty::prems = Goal
"[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
--- a/src/ZF/Perm.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Perm.ML Wed Jan 27 10:31:31 1999 +0100
@@ -9,8 +9,6 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-open Perm;
-
(** Surjective function space **)
Goalw [surj_def] "f: surj(A,B) ==> f: A->B";
@@ -93,7 +91,7 @@
qed "bij_is_surj";
(* f: bij(A,B) ==> f: A->B *)
-bind_thm ("bij_is_fun", (bij_is_inj RS inj_is_fun));
+bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
val prems = goalw Perm.thy [bij_def]
"[| !!x. x:A ==> c(x): B; \
@@ -225,6 +223,8 @@
qed "bij_converse_bij";
(*Adding this as an SI seems to cause looping*)
+AddTCs [bij_converse_bij];
+
(** Composition of two relations **)
@@ -342,17 +342,19 @@
by (rtac fun_extension 1);
by (rtac comp_fun 1);
by (rtac lam_funtype 2);
-by (typechk_tac (prem::ZF_typechecks));
+by (typecheck_tac (tcset() addTCs [prem]));
by (asm_simp_tac (simpset()
- setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
+ setSolver
+ type_solver_tac (tcset() addTCs [prem, lam_funtype])) 1);
qed "comp_lam";
Goal "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)";
by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
f_imp_injective 1);
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
-by (asm_simp_tac (simpset() addsimps [left_inverse]
- setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
+by (asm_simp_tac (simpset() addsimps [left_inverse]
+ setSolver
+ type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
qed "comp_inj";
Goalw [surj_def]
--- a/src/ZF/ROOT.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ROOT.ML Wed Jan 27 10:31:31 1999 +0100
@@ -20,7 +20,7 @@
use "thy_syntax";
use_thy "Let";
-use_thy "func";
+use_thy "ZF";
use "Tools/typechk";
use_thy "mono";
use "ind_syntax";
--- a/src/ZF/Sum.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Sum.ML Wed Jan 27 10:31:31 1999 +0100
@@ -6,8 +6,6 @@
Disjoint sums in Zermelo-Fraenkel Set Theory
*)
-open Sum;
-
(*** Rules for the Part primitive ***)
Goalw [Part_def]
@@ -102,6 +100,7 @@
AddSDs [Inl_inject, Inr_inject];
Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
+AddTCs [InlI, InrI];
Goal "Inl(a): A+B ==> a: A";
by (Blast_tac 1);
@@ -150,6 +149,7 @@
by (ALLGOALS (etac ssubst));
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "case_type";
+AddTCs [case_type];
Goal "u: A+B ==> \
\ R(case(c,d,u)) <-> \
--- a/src/ZF/Tools/typechk.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/Tools/typechk.ML Wed Jan 27 10:31:31 1999 +0100
@@ -1,11 +1,54 @@
(* Title: ZF/typechk
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
+ Copyright 1999 University of Cambridge
Tactics for type checking -- from CTT
*)
+infix 4 addTCs delTCs;
+
+structure TypeCheck =
+struct
+datatype tcset =
+ TC of {rules: thm list, (*the type-checking rules*)
+ net: thm Net.net}; (*discrimination net of the same rules*)
+
+
+
+val mem_thm = gen_mem eq_thm
+and rem_thm = gen_rem eq_thm;
+
+fun addTC (cs as TC{rules, net}, th) =
+ if mem_thm (th, rules) then
+ (warning ("Ignoring duplicate type-checking rule\n" ^
+ string_of_thm th);
+ cs)
+ else
+ TC{rules = th::rules,
+ net = Net.insert_term ((concl_of th, th), net, K false)};
+
+
+fun delTC (cs as TC{rules, net}, th) =
+ if mem_thm (th, rules) then
+ TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
+ rules = rem_thm (rules,th)}
+ else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
+ cs);
+
+val op addTCs = foldl addTC;
+val op delTCs = foldl delTC;
+
+
+(*resolution using a net rather than rules*)
+fun net_res_tac maxr net =
+ SUBGOAL
+ (fn (prem,i) =>
+ let val rls = Net.unify_term net (Logic.strip_assums_concl prem)
+ in
+ if length rls <= maxr then resolve_tac rls i else no_tac
+ end);
+
fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;
@@ -17,18 +60,75 @@
(*Type checking solves a:?A (a rigid, ?A maybe flexible).
match_tac is too strict; would refuse to instantiate ?A*)
-fun typechk_step_tac tyrls =
- FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 3);
+fun typecheck_step_tac (TC{net,...}) =
+ FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
-fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
+fun typecheck_tac tcset = REPEAT (typecheck_step_tac tcset);
-val ZF_typechecks =
- [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
+(*Compiles a term-net for speed*)
+val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
+ ballI,allI,conjI,impI];
(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
-fun type_auto_tac tyrls hyps = SELECT_GOAL
- (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
- ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
- ballI,allI,conjI,impI] 1));
+fun type_solver_tac tcset hyps = SELECT_GOAL
+ (DEPTH_SOLVE (etac FalseE 1
+ ORELSE basic_res_tac 1
+ ORELSE (ares_tac hyps 1
+ APPEND typecheck_step_tac tcset)));
+
+
+
+fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
+ TC {rules = gen_union eq_thm (rules,rules'),
+ net = Net.merge (net, net', eq_thm)};
+
+(*print tcsets*)
+fun print_tc (TC{rules,...}) =
+ Pretty.writeln
+ (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));
+
+
+structure TypecheckingArgs =
+ struct
+ val name = "ZF/type-checker";
+ type T = tcset ref;
+ val empty = ref (TC{rules=[], net=Net.empty});
+ fun prep_ext (ref ss) = (ref ss): T; (*create new reference!*)
+ fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
+ fun print _ (ref tc) = print_tc tc;
+ end;
+
+structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
+val setup = [TypecheckingData.init];
+
+val print_tcset = TypecheckingData.print;
+val tcset_ref_of_sg = TypecheckingData.get_sg;
+val tcset_ref_of = TypecheckingData.get;
+
+(* access global tcset *)
+
+val tcset_of_sg = ! o tcset_ref_of_sg;
+val tcset_of = tcset_of_sg o sign_of;
+
+val tcset = tcset_of o Context.the_context;
+val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
+
+(* change global tcset *)
+
+fun change_tcset f x = tcset_ref () := (f (tcset (), x));
+
+val AddTCs = change_tcset (op addTCs);
+val DelTCs = change_tcset (op delTCs);
+
+fun Typecheck_tac st = typecheck_tac (tcset()) st;
+
+fun Type_solver_tac hyps = type_solver_tac (tcset()) hyps;
+end;
+
+
+open TypeCheck;
+
+
+
--- a/src/ZF/ex/BinEx.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/BinEx.ML Wed Jan 27 10:31:31 1999 +0100
@@ -12,43 +12,43 @@
(*All runtimes below are on a 300MHz Pentium*)
Goal "#13 $+ #19 = #32";
-by (simp_tac bin_comp_ss 1); (*0 secs*)
+by (Simp_tac 1); (*0 secs*)
result();
Goal "#1234 $+ #5678 = #6912";
-by (simp_tac bin_comp_ss 1); (*190 msec*)
+by (Simp_tac 1); (*190 msec*)
result();
Goal "#1359 $+ #-2468 = #-1109";
-by (simp_tac bin_comp_ss 1); (*160 msec*)
+by (Simp_tac 1); (*160 msec*)
result();
Goal "#93746 $+ #-46375 = #47371";
-by (simp_tac bin_comp_ss 1); (*300 msec*)
+by (Simp_tac 1); (*300 msec*)
result();
Goal "$~ #65745 = #-65745";
-by (simp_tac bin_comp_ss 1); (*80 msec*)
+by (Simp_tac 1); (*80 msec*)
result();
(* negation of ~54321 *)
Goal "$~ #-54321 = #54321";
-by (simp_tac bin_comp_ss 1); (*90 msec*)
+by (Simp_tac 1); (*90 msec*)
result();
Goal "#13 $* #19 = #247";
-by (simp_tac bin_comp_ss 1); (*110 msec*)
+by (Simp_tac 1); (*110 msec*)
result();
Goal "#-84 $* #51 = #-4284";
-by (simp_tac bin_comp_ss 1); (*210 msec*)
+by (Simp_tac 1); (*210 msec*)
result();
(*The worst case for 8-bit operands *)
Goal "#255 $* #255 = #65025";
-by (simp_tac bin_comp_ss 1); (*730 msec*)
+by (Simp_tac 1); (*730 msec*)
result();
Goal "#1359 $* #-2468 = #-3354012";
-by (simp_tac bin_comp_ss 1); (*1.04 secs*)
+by (Simp_tac 1); (*1.04 secs*)
result();
--- a/src/ZF/ex/Limit.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/Limit.ML Wed Jan 27 10:31:31 1999 +0100
@@ -9,8 +9,6 @@
val nat_linear_le = [nat_into_Ord,nat_into_Ord] MRS Ord_linear_le;
-open Limit;
-
(*----------------------------------------------------------------------*)
(* Useful goal commands. *)
(*----------------------------------------------------------------------*)
@@ -797,6 +795,8 @@
by (asm_simp_tac(simpset() addsimps[id_thm, cpo_lub RS islub_in, chain_in, chain_fun RS eta]) 1);
qed "id_cont";
+AddTCs [id_cont];
+
val comp_cont_apply = cont_fun RSN(2,cont_fun RS comp_fun_apply);
Goal (* comp_pres_cont *)
@@ -814,6 +814,8 @@
by (auto_tac (claset() addIs [cpo_lub RS islub_in, cont_chain], simpset()));
qed "comp_pres_cont";
+AddTCs [comp_pres_cont];
+
Goal (* comp_mono *)
"[| f:cont(D',E); g:cont(D,D'); f':cont(D',E); g':cont(D,D'); \
\ rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |] ==> \
@@ -1017,9 +1019,11 @@
(* The following three theorems have cpo asms due to THE (uniqueness). *)
-val Rp_cont = embRp RS projpair_p_cont;
-val embRp_eq = embRp RS projpair_eq;
-val embRp_rel = embRp RS projpair_rel;
+bind_thm ("Rp_cont", embRp RS projpair_p_cont);
+bind_thm ("embRp_eq", embRp RS projpair_eq);
+bind_thm ("embRp_rel", embRp RS projpair_rel);
+
+AddTCs [Rp_cont];
val id_apply = prove_goalw Perm.thy [id_def]
"!!z. x:A ==> id(A)`x = x"
@@ -1356,6 +1360,8 @@
"!!x. [|emb_chain(DD,ee); n:nat|] ==> cpo(DD`n)"
(fn prems => [Fast_tac 1]);
+AddTCs [emb_chain_cpo];
+
val emb_chain_emb = prove_goalw Limit.thy [emb_chain_def]
"!!x. [|emb_chain(DD,ee); n:nat|] ==> emb(DD`n,DD`succ(n),ee`n)"
(fn prems => [Fast_tac 1]);
@@ -1952,7 +1958,7 @@
but since x le y is x<succ(y) simplification does too much with this thm. *)
by (stac eps_split_right_le 1);
by (assume_tac 2);
-by (asm_simp_tac(ZF_ss addsimps [add1]) 1);
+by (asm_simp_tac(FOL_ss addsimps [add1]) 1);
brr[add_le_self,nat_0I,nat_succI] 1;
by (asm_simp_tac(simpset() addsimps[eps_succ_Rp]) 1);
by (stac comp_fun_apply 1);
@@ -2377,7 +2383,8 @@
by (asm_simp_tac (simpset() addsimps[lemma]) 1);
by (rtac dominate_islub 1);
by (rtac cpo_lub 2);
-brr[commute_chain, commute_emb, islub_const, cont_cf, id_cont, cpo_cf, chain_fun,chain_const] 2;
+brr[commute_chain, commute_emb, islub_const, cont_cf, id_cont,
+ cpo_cf, chain_fun,chain_const] 2;
by (rtac dominateI 1);
by (assume_tac 1);
by (Asm_simp_tac 1);
@@ -2412,10 +2419,9 @@
\ (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
by (rtac fun_extension 1);
by (fast_tac (claset() addIs [lam_type]) 1);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() setSolver (type_auto_tac [lam_type, comp_pres_cont, Rp_cont,
- emb_cont, commute_emb, emb_chain_cpo]))));
+by (asm_simp_tac
+ (simpset() setSolver type_solver_tac (tcset() addTCs [emb_cont, commute_emb])) 2);
+by (Asm_simp_tac 1);
val lemma = result();
Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f); \
--- a/src/ZF/ex/ListN.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/ListN.ML Wed Jan 27 10:31:31 1999 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/listn
+(* Title: ZF/ex/ListN
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -19,7 +19,7 @@
by (rtac iffI 1);
by (blast_tac (claset() addIs [list_into_listn]) 2);
by (etac listn.induct 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "listn_iff";
Goal "listn(A)``{n} = {l:list(A). length(l)=n}";
--- a/src/ZF/ex/Primrec.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/Primrec.ML Wed Jan 27 10:31:31 1999 +0100
@@ -19,25 +19,20 @@
(* c: prim_rec ==> c: list(nat) -> nat *)
val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
-simpset_ref() := simpset() setSolver (type_auto_tac ([prim_rec_into_fun] @
- pr_typechecks @ prim_rec.intrs));
+AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
Goal "i:nat ==> ACK(i): prim_rec";
by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "ACK_in_prim_rec";
-val ack_typechecks =
- [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
- add_type, list_add_type, nat_into_Ord] @
- nat_typechecks @ list.intrs @ prim_rec.intrs;
-
-simpset_ref() := simpset() setSolver (type_auto_tac ack_typechecks);
+AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
+ list_add_type, nat_into_Ord, rec_type];
Goal "[| i:nat; j:nat |] ==> ack(i,j): nat";
by Auto_tac;
qed "ack_type";
-Addsimps [ack_type];
+AddTCs [ack_type];
(** Ackermann's function cases **)
@@ -84,7 +79,7 @@
by (etac succ_lt_induct 1);
by (assume_tac 1);
by (rtac lt_trans 2);
-by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr_typechecks) 1));
+by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset()));
qed "ack_lt_mono2";
(*PROPERTY A 5', monotonicity for le *)
@@ -99,14 +94,14 @@
by (ALLGOALS Asm_simp_tac);
by (rtac ack_le_mono2 1);
by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
-by (REPEAT (ares_tac (ack_typechecks) 1));
+by Auto_tac;
qed "ack2_le_ack1";
(*PROPERTY A 7-, the single-step lemma*)
Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
by (rtac (ack_lt_mono2 RS lt_trans2) 1);
by (rtac ack2_le_ack1 4);
-by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr_typechecks) 1));
+by Auto_tac;
qed "ack_lt_ack_succ1";
(*PROPERTY A 7, monotonicity for < *)
@@ -115,7 +110,7 @@
by (etac succ_lt_induct 1);
by (assume_tac 1);
by (rtac lt_trans 2);
-by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr_typechecks) 1));
+by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset()));
qed "ack_lt_mono1";
(*PROPERTY A 7', monotonicity for le *)
@@ -154,8 +149,8 @@
by (rtac (ack_nest_bound RS lt_trans2) 2);
by (Asm_simp_tac 5);
by (rtac (add_le_mono RS leI RS leI) 1);
-by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
- ack_typechecks) 1));
+by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1],
+ simpset()));
qed "ack_add_bound";
(*PROPERTY A 12. Article uses existential quantifier but the ALF proof
@@ -164,8 +159,8 @@
\ i#+j < ack(succ(succ(succ(succ(k)))), j)";
by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
by (rtac (ack_add_bound RS lt_trans2) 2);
-by (asm_simp_tac (simpset() addsimps [add_0_right]) 5);
-by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
+br add_lt_mono 1;
+by Auto_tac;
qed "ack_add_bound2";
(*** MAIN RESULT ***)
@@ -259,16 +254,14 @@
by (induct_tac "a" 1);
(*base case*)
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)]);
+ assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
+by Auto_tac;
(*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);
- (*Auto_tac is a little slow*)
-by (TRYALL (type_auto_tac ack_typechecks []));
+by Typecheck_tac;
by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
(*final part of the simplification*)
by (Asm_simp_tac 1);
@@ -284,19 +277,15 @@
\ |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))";
by (rtac (ballI RS bexI) 1);
by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
-by (REPEAT
- (SOMEGOAL
- (FIRST' [test_assume_tac,
- match_tac (ack_typechecks),
- rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
+by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
+by Typecheck_tac;
qed "PREC_case";
Goal "f:prim_rec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
by (etac prim_rec.induct 1);
-by Safe_tac;
-by (DEPTH_SOLVE
- (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
- bexI, ballI] @ nat_typechecks) 1));
+by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case,
+ PREC_case],
+ simpset()));
qed "ack_bounds_prim_rec";
Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : prim_rec";
@@ -304,7 +293,6 @@
by (etac (ack_bounds_prim_rec RS bexE) 1);
by (rtac lt_irrefl 1);
by (dres_inst_tac [("x", "[x]")] bspec 1);
-by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
+by Auto_tac;
qed "ack_not_prim_rec";
--- a/src/ZF/ex/Primrec_defs.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/Primrec_defs.ML Wed Jan 27 10:31:31 1999 +0100
@@ -9,37 +9,25 @@
(*Theory TF redeclares map_type*)
val map_type = Context.thm "List.map_type";
-val pr_typechecks =
- nat_typechecks @ list.intrs @
- [lam_type, list_case_type, drop_type, map_type,
- apply_type, rec_type];
-
(** Useful special cases of evaluation ***)
-simpset_ref() := simpset() setSolver (type_auto_tac pr_typechecks);
-
-Goalw [SC_def]
- "[| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+Goalw [SC_def] "[| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
by (Asm_simp_tac 1);
qed "SC";
-Goalw [CONST_def]
- "[| l: list(nat) |] ==> CONST(k) ` l = k";
+Goalw [CONST_def] "[| l: list(nat) |] ==> CONST(k) ` l = k";
by (Asm_simp_tac 1);
qed "CONST";
-Goalw [PROJ_def]
- "[| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+Goalw [PROJ_def] "[| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
by (Asm_simp_tac 1);
qed "PROJ_0";
-Goalw [COMP_def]
- "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+Goalw [COMP_def] "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
by (Asm_simp_tac 1);
qed "COMP_1";
-Goalw [PREC_def]
- "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+Goalw [PREC_def] "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
by (Asm_simp_tac 1);
qed "PREC_0";
--- a/src/ZF/ex/TF.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/TF.ML Wed Jan 27 10:31:31 1999 +0100
@@ -7,6 +7,7 @@
*)
Addsimps tree_forest.intrs;
+AddTCs tree_forest.intrs;
(** tree_forest(A) as the union of tree(A) and forest(A) **)
--- a/src/ZF/ex/Term.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/ex/Term.ML Wed Jan 27 10:31:31 1999 +0100
@@ -171,14 +171,11 @@
(** Term simplification **)
-val term_typechecks =
- [term.Apply_I, term_map_type, term_map_type2, term_size_type,
- reflect_type, preorder_type, postorder_type];
+AddTCs [term.Apply_I, term_map_type, term_map_type2, term_size_type,
+ reflect_type, preorder_type, postorder_type];
(*map_type2 and term_map_type2 instantiate variables*)
-simpset_ref() := simpset()
- addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]
- setSolver type_auto_tac (list_typechecks@term_typechecks);
+Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder];
(** theorems about term_map **)
--- a/src/ZF/func.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/func.ML Wed Jan 27 10:31:31 1999 +0100
@@ -104,6 +104,7 @@
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
by (REPEAT (ares_tac [apply_Pair] 1));
qed "apply_type";
+AddTCs [apply_type];
(*This version is acceptable to the simplifier*)
Goal "[| f: A->B; a:A |] ==> f`a : B";
@@ -165,6 +166,7 @@
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";
by (blast_tac (claset() addIs prems) 1);
qed "lam_type";
+AddTCs [lam_type];
Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
--- a/src/ZF/pair.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/pair.ML Wed Jan 27 10:31:31 1999 +0100
@@ -63,6 +63,7 @@
qed_goal "SigmaI" thy
"!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
(fn _ => [ Asm_simp_tac 1 ]);
+AddTCs [SigmaI];
bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);
bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
@@ -147,6 +148,7 @@
(fn major::prems=>
[ (rtac (major RS SigmaE) 1),
(asm_simp_tac (simpset() addsimps prems) 1) ]);
+AddTCs [split_type];
Goalw [split_def]
"u: A*B ==> \
--- a/src/ZF/simpdata.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/simpdata.ML Wed Jan 27 10:31:31 1999 +0100
@@ -106,6 +106,7 @@
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
- addsplits [split_if];
+ addsplits [split_if]
+ setSolver Type_solver_tac;
val ZF_ss = simpset();
--- a/src/ZF/upair.ML Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/upair.ML Wed Jan 27 10:31:31 1999 +0100
@@ -141,6 +141,8 @@
(fn _ => [ Simp_tac 1 ]);
Addsimps [consI1];
+AddTCs [consI1]; (*risky as a typechecking rule, but solves otherwise
+ unconstrained goals of the form x : ?A*)
qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
(fn _ => [ Asm_simp_tac 1 ]);
@@ -288,7 +290,7 @@
"[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A"
(fn prems=> [ (simp_tac
(simpset() addsimps prems addsplits [split_if]) 1) ]);
-
+AddTCs [if_type];
(*** Foundation lemmas ***)
--- a/src/ZF/upair.thy Mon Jan 25 20:35:19 1999 +0100
+++ b/src/ZF/upair.thy Wed Jan 27 10:31:31 1999 +0100
@@ -6,4 +6,10 @@
Dummy theory, but holds the standard ZF simpset.
*)
-upair = ZF
+upair = ZF +
+
+setup
+ TypeCheck.setup
+
+end
+