# HG changeset patch
# User lcp
# Date 753370420 -3600
# Node ID 0e58da397b1d3a76119e10341b09cb9727b8b3b1
# Parent  96d2c0fc2cd5cfb353182069f011d433c04d095a
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws

diff -r 96d2c0fc2cd5 -r 0e58da397b1d src/ZF/Bool.ML
--- a/src/ZF/Bool.ML	Mon Nov 15 12:58:21 1993 +0100
+++ b/src/ZF/Bool.ML	Mon Nov 15 14:33:40 1993 +0100
@@ -27,9 +27,10 @@
 (** 1=0 ==> R **)
 val one_neq_0 = one_not_0 RS notE;
 
-val prems = goalw Bool.thy bool_defs "[| c: bool;  P(1);  P(0) |] ==> P(c)";
-by (cut_facts_tac prems 1);
-by (fast_tac ZF_cs 1);
+val major::prems = goalw Bool.thy bool_defs
+    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
+br (major RS consE) 1;
+by (REPEAT (eresolve_tac (singletonE::prems) 1));
 val boolE = result();
 
 (** cond **)
@@ -47,10 +48,8 @@
 val major::prems = goal Bool.thy 
     "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
 by (rtac (major RS boolE) 1);
-by (rtac (cond_0 RS ssubst) 2);
-by (resolve_tac prems 2);
-by (rtac (cond_1 RS ssubst) 1);
-by (resolve_tac prems 1);
+by (asm_simp_tac (ZF_ss addsimps (cond_1::prems)) 1);
+by (asm_simp_tac (ZF_ss addsimps (cond_0::prems)) 1);
 val cond_type = result();
 
 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
@@ -92,5 +91,69 @@
 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
 		       or_type, xor_type]
 
-val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
+val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
+
+val bool_ss0 = ZF_ss addsimps bool_simps;
+
+fun bool0_tac i =
+    EVERY [etac boolE i, asm_simp_tac bool_ss0 (i+1), asm_simp_tac bool_ss0 i];
+
+(*** Laws for 'not' ***)
+
+goal Bool.thy "!!a. a:bool ==> not(not(a)) = a";
+by (bool0_tac 1);
+val not_not = result();
+
+goal Bool.thy "!!a b. a:bool ==> not(a and b) = not(a) or not(b)";
+by (bool0_tac 1);
+val not_and = result();
+
+goal Bool.thy "!!a b. a:bool ==> not(a or b) = not(a) and not(b)";
+by (bool0_tac 1);
+val not_or = result();
+
+(*** Laws about 'and' ***)
+
+goal Bool.thy "!!a. a: bool ==> a and a = a";
+by (bool0_tac 1);
+val and_absorb = result();
+
+goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
+be boolE 1;
+by (bool0_tac 1);
+by (bool0_tac 1);
+val and_commute = result();
 
+goal Bool.thy
+ "!!a. a: bool ==> (a and b) and c  =  a and (b and c)";
+by (bool0_tac 1);
+val and_assoc = result();
+
+goal Bool.thy
+ "!!a. [| a: bool; b:bool; c:bool |] ==> \
+\      (a or b) and c  =  (a and c) or (b and c)";
+by (REPEAT (bool0_tac 1));
+val and_or_distrib = result();
+
+(** binary orion **)
+
+goal Bool.thy "!!a. a: bool ==> a or a = a";
+by (bool0_tac 1);
+val or_absorb = result();
+
+goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
+be boolE 1;
+by (bool0_tac 1);
+by (bool0_tac 1);
+val or_commute = result();
+
+goal Bool.thy "!!a. a: bool ==> (a or b) or c  =  a or (b or c)";
+by (bool0_tac 1);
+val or_assoc = result();
+
+goal Bool.thy
+ "!!a b c. [| a: bool; b: bool; c: bool |] ==> \
+\          (a and b) or c  =  (a or c) and (b or c)";
+by (REPEAT (bool0_tac 1));
+val or_and_distrib = result();
+
diff -r 96d2c0fc2cd5 -r 0e58da397b1d src/ZF/bool.ML
--- a/src/ZF/bool.ML	Mon Nov 15 12:58:21 1993 +0100
+++ b/src/ZF/bool.ML	Mon Nov 15 14:33:40 1993 +0100
@@ -27,9 +27,10 @@
 (** 1=0 ==> R **)
 val one_neq_0 = one_not_0 RS notE;
 
-val prems = goalw Bool.thy bool_defs "[| c: bool;  P(1);  P(0) |] ==> P(c)";
-by (cut_facts_tac prems 1);
-by (fast_tac ZF_cs 1);
+val major::prems = goalw Bool.thy bool_defs
+    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
+br (major RS consE) 1;
+by (REPEAT (eresolve_tac (singletonE::prems) 1));
 val boolE = result();
 
 (** cond **)
@@ -47,10 +48,8 @@
 val major::prems = goal Bool.thy 
     "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
 by (rtac (major RS boolE) 1);
-by (rtac (cond_0 RS ssubst) 2);
-by (resolve_tac prems 2);
-by (rtac (cond_1 RS ssubst) 1);
-by (resolve_tac prems 1);
+by (asm_simp_tac (ZF_ss addsimps (cond_1::prems)) 1);
+by (asm_simp_tac (ZF_ss addsimps (cond_0::prems)) 1);
 val cond_type = result();
 
 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
@@ -92,5 +91,69 @@
 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
 		       or_type, xor_type]
 
-val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
+val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
+
+val bool_ss0 = ZF_ss addsimps bool_simps;
+
+fun bool0_tac i =
+    EVERY [etac boolE i, asm_simp_tac bool_ss0 (i+1), asm_simp_tac bool_ss0 i];
+
+(*** Laws for 'not' ***)
+
+goal Bool.thy "!!a. a:bool ==> not(not(a)) = a";
+by (bool0_tac 1);
+val not_not = result();
+
+goal Bool.thy "!!a b. a:bool ==> not(a and b) = not(a) or not(b)";
+by (bool0_tac 1);
+val not_and = result();
+
+goal Bool.thy "!!a b. a:bool ==> not(a or b) = not(a) and not(b)";
+by (bool0_tac 1);
+val not_or = result();
+
+(*** Laws about 'and' ***)
+
+goal Bool.thy "!!a. a: bool ==> a and a = a";
+by (bool0_tac 1);
+val and_absorb = result();
+
+goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
+be boolE 1;
+by (bool0_tac 1);
+by (bool0_tac 1);
+val and_commute = result();
 
+goal Bool.thy
+ "!!a. a: bool ==> (a and b) and c  =  a and (b and c)";
+by (bool0_tac 1);
+val and_assoc = result();
+
+goal Bool.thy
+ "!!a. [| a: bool; b:bool; c:bool |] ==> \
+\      (a or b) and c  =  (a and c) or (b and c)";
+by (REPEAT (bool0_tac 1));
+val and_or_distrib = result();
+
+(** binary orion **)
+
+goal Bool.thy "!!a. a: bool ==> a or a = a";
+by (bool0_tac 1);
+val or_absorb = result();
+
+goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
+be boolE 1;
+by (bool0_tac 1);
+by (bool0_tac 1);
+val or_commute = result();
+
+goal Bool.thy "!!a. a: bool ==> (a or b) or c  =  a or (b or c)";
+by (bool0_tac 1);
+val or_assoc = result();
+
+goal Bool.thy
+ "!!a b c. [| a: bool; b: bool; c: bool |] ==> \
+\          (a and b) or c  =  (a or c) and (b or c)";
+by (REPEAT (bool0_tac 1));
+val or_and_distrib = result();
+