--- a/src/ZF/Bool.ML Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Bool.ML Mon Dec 28 16:59:28 1998 +0100
@@ -24,6 +24,8 @@
by (rtac consI1 1);
qed "bool_0I";
+Addsimps [bool_1I, bool_0I];
+
Goalw bool_defs "1~=0";
by (rtac succ_not_0 1);
qed "one_not_0";
@@ -54,10 +56,16 @@
fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
-Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
+Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
by (bool_tac 1);
qed "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);
by (rtac cond_1 1);
@@ -89,10 +97,14 @@
"[| a:bool; b:bool |] ==> a or b : bool"
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
+Addsimps [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])) ]);
+Addsimps [xor_type];
+
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type,
or_type, xor_type];