author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/bool 
0  2 
ID: $Id$ 
1461  3 
Author: Martin D Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
For ZF/bool.thy. Booleans in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
open Bool; 

10 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

11 
val bool_defs = [bool_def,cond_def]; 
0  12 

13 
(* Introduction rules *) 

14 

15 
goalw Bool.thy bool_defs "1 : bool"; 

16 
by (rtac (consI1 RS consI2) 1); 

760  17 
qed "bool_1I"; 
0  18 

19 
goalw Bool.thy bool_defs "0 : bool"; 

20 
by (rtac consI1 1); 

760  21 
qed "bool_0I"; 
0  22 

37  23 
goalw Bool.thy bool_defs "1~=0"; 
0  24 
by (rtac succ_not_0 1); 
760  25 
qed "one_not_0"; 
0  26 

27 
(** 1=0 ==> R **) 

28 
val one_neq_0 = one_not_0 RS notE; 

29 

119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

30 
val major::prems = goalw Bool.thy bool_defs 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

31 
"[ c: bool; c=1 ==> P; c=0 ==> P ] ==> P"; 
129  32 
by (rtac (major RS consE) 1); 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

33 
by (REPEAT (eresolve_tac (singletonE::prems) 1)); 
760  34 
qed "boolE"; 
0  35 

36 
(** cond **) 

37 

38 
(*1 means true*) 

39 
goalw Bool.thy bool_defs "cond(1,c,d) = c"; 

40 
by (rtac (refl RS if_P) 1); 

760  41 
qed "cond_1"; 
0  42 

43 
(*0 means false*) 

44 
goalw Bool.thy bool_defs "cond(0,c,d) = d"; 

45 
by (rtac (succ_not_0 RS not_sym RS if_not_P) 1); 

760  46 
qed "cond_0"; 
0  47 

48 
val major::prems = goal Bool.thy 

49 
"[ b: bool; c: A(1); d: A(0) ] ==> cond(b,c,d): A(b)"; 

50 
by (rtac (major RS boolE) 1); 

119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

51 
by (asm_simp_tac (ZF_ss addsimps (cond_1::prems)) 1); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

52 
by (asm_simp_tac (ZF_ss addsimps (cond_0::prems)) 1); 
760  53 
qed "cond_type"; 
0  54 

55 
val [rew] = goal Bool.thy "[ !!b. j(b)==cond(b,c,d) ] ==> j(1) = c"; 

56 
by (rewtac rew); 

57 
by (rtac cond_1 1); 

760  58 
qed "def_cond_1"; 
0  59 

60 
val [rew] = goal Bool.thy "[ !!b. j(b)==cond(b,c,d) ] ==> j(0) = d"; 

61 
by (rewtac rew); 

62 
by (rtac cond_0 1); 

760  63 
qed "def_cond_0"; 
0  64 

65 
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)]; 

66 

67 
val [not_1,not_0] = conds not_def; 

68 

69 
val [and_1,and_0] = conds and_def; 

70 

71 
val [or_1,or_0] = conds or_def; 

72 

73 
val [xor_1,xor_0] = conds xor_def; 

74 

760  75 
qed_goalw "not_type" Bool.thy [not_def] 
0  76 
"a:bool ==> not(a) : bool" 
77 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

78 

760  79 
qed_goalw "and_type" Bool.thy [and_def] 
0  80 
"[ a:bool; b:bool ] ==> a and b : bool" 
81 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

82 

760  83 
qed_goalw "or_type" Bool.thy [or_def] 
0  84 
"[ a:bool; b:bool ] ==> a or b : bool" 
85 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

86 

760  87 
qed_goalw "xor_type" Bool.thy [xor_def] 
0  88 
"[ a:bool; b:bool ] ==> a xor b : bool" 
89 
(fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]); 

90 

91 
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 

1461  92 
or_type, xor_type] 
0  93 

119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

94 
val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0]; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

95 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

96 
val bool_ss0 = ZF_ss addsimps bool_simps; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

97 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

98 
fun bool0_tac i = 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

99 
EVERY [etac boolE i, asm_simp_tac bool_ss0 (i+1), asm_simp_tac bool_ss0 i]; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

100 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

101 
(*** Laws for 'not' ***) 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

102 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

103 
goal Bool.thy "!!a. a:bool ==> not(not(a)) = a"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

104 
by (bool0_tac 1); 
760  105 
qed "not_not"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

106 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

107 
goal Bool.thy "!!a b. a:bool ==> not(a and b) = not(a) or not(b)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

108 
by (bool0_tac 1); 
760  109 
qed "not_and"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

110 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

111 
goal Bool.thy "!!a b. a:bool ==> not(a or b) = not(a) and not(b)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

112 
by (bool0_tac 1); 
760  113 
qed "not_or"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

114 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

115 
(*** Laws about 'and' ***) 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

116 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

117 
goal Bool.thy "!!a. a: bool ==> a and a = a"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

118 
by (bool0_tac 1); 
760  119 
qed "and_absorb"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

120 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

121 
goal Bool.thy "!!a b. [ a: bool; b:bool ] ==> a and b = b and a"; 
129  122 
by (etac boolE 1); 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

123 
by (bool0_tac 1); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

124 
by (bool0_tac 1); 
760  125 
qed "and_commute"; 
0  126 

119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

127 
goal Bool.thy 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

128 
"!!a. a: bool ==> (a and b) and c = a and (b and c)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

129 
by (bool0_tac 1); 
760  130 
qed "and_assoc"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

131 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

132 
goal Bool.thy 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

133 
"!!a. [ a: bool; b:bool; c:bool ] ==> \ 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

134 
\ (a or b) and c = (a and c) or (b and c)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

135 
by (REPEAT (bool0_tac 1)); 
760  136 
qed "and_or_distrib"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

137 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

138 
(** binary orion **) 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

139 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

140 
goal Bool.thy "!!a. a: bool ==> a or a = a"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

141 
by (bool0_tac 1); 
760  142 
qed "or_absorb"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

143 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

144 
goal Bool.thy "!!a b. [ a: bool; b:bool ] ==> a or b = b or a"; 
129  145 
by (etac boolE 1); 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

146 
by (bool0_tac 1); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

147 
by (bool0_tac 1); 
760  148 
qed "or_commute"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

149 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

150 
goal Bool.thy "!!a. a: bool ==> (a or b) or c = a or (b or c)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

151 
by (bool0_tac 1); 
760  152 
qed "or_assoc"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

153 

0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

154 
goal Bool.thy 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

155 
"!!a b c. [ a: bool; b: bool; c: bool ] ==> \ 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

156 
\ (a and b) or c = (a or c) and (b or c)"; 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

157 
by (REPEAT (bool0_tac 1)); 
760  158 
qed "or_and_distrib"; 
119
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

159 