# HG changeset patch # User paulson # Date 917429491 -3600 # Node ID bff90585cce590ac4822e14cc5bc2c1f0e5de188 # Parent bc1e27bcc1957c35a1714e4b3ece6b00764f3f28 new typechecking solver for the simplifier diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/AC/Cardinal_aux.ML --- 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)))"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/AC/WO6_WO1.ML --- 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 0 #- n = 0"; by (induct_tac "n" 1); @@ -288,6 +291,7 @@ Goalw [mod_def] "[| 0 m mod n : nat"; by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); qed "mod_type"; +AddTCs [mod_type]; Goal "[| 0 m mod n = m"; by (rtac (mod_def RS def_transrec RS trans) 1); @@ -309,6 +313,7 @@ "[| 0 m div n : nat"; by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); qed "div_type"; +AddTCs [div_type]; Goal "[| 0 m div n = 0"; by (rtac (div_def RS def_transrec RS trans) 1); diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Bool.ML --- 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]; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/CardinalArith.ML --- 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. ")] 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. ")] 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 :A*B. ")] exI 1); by (res_inst_tac [("d", "%.")] 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 diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Cardinal_AC.ML --- 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. "), ("d", "%. 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)"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Integ/Bin.ML --- 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]; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Integ/Bin.thy --- 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 diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Integ/EquivClass.ML --- 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 |] \ diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Integ/Int.ML --- 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*) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/List.ML --- 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 ***) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Nat.ML --- 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; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Order.ML --- 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!*) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/OrderType.ML --- 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"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Ordinal.ML --- 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))"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Perm.ML --- 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] diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ROOT.ML --- 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"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Sum.ML --- 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)) <-> \ diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/Tools/typechk.ML --- 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; + + + diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ex/BinEx.ML --- 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(); diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ex/Limit.ML --- 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 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"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ex/Primrec_defs.ML --- 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"; diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ex/TF.ML --- 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) **) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/ex/Term.ML --- 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 **) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/func.ML --- 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)); diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/pair.ML --- 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) |] ==> : 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 ==> \ diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/simpdata.ML --- 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(); diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/upair.ML --- 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 ***) diff -r bc1e27bcc195 -r bff90585cce5 src/ZF/upair.thy --- 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 +