author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 129  dc50a4b96d7b 
permissions  rwrr 
0  1 
(* Title: ZF/bool 
2 
ID: $Id$ 

3 
Author: Martin D Coen, Cambridge University Computer Laboratory 

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); 

17 
val bool_1I = result(); 

18 

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

20 
by (rtac consI1 1); 

21 
val bool_0I = result(); 

22 

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

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)); 
0  34 
val boolE = result(); 
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); 

41 
val cond_1 = result(); 

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); 

46 
val cond_0 = result(); 

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); 
0  53 
val cond_type = result(); 
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); 

58 
val def_cond_1 = result(); 

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); 

63 
val def_cond_0 = result(); 

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 

75 
val not_type = prove_goalw Bool.thy [not_def] 

76 
"a:bool ==> not(a) : bool" 

77 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

78 

79 
val and_type = prove_goalw Bool.thy [and_def] 

80 
"[ a:bool; b:bool ] ==> a and b : bool" 

81 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

82 

83 
val or_type = prove_goalw Bool.thy [or_def] 

84 
"[ a:bool; b:bool ] ==> a or b : bool" 

85 
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); 

86 

87 
val xor_type = prove_goalw Bool.thy [xor_def] 

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, 

92 
or_type, xor_type] 

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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

105 
val not_not = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

109 
val not_and = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

113 
val not_or = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

119 
val and_absorb = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

125 
val and_commute = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

130 
val and_assoc = result(); 
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)); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

136 
val and_or_distrib = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

142 
val or_absorb = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

148 
val or_commute = result(); 
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); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

152 
val or_assoc = result(); 
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)); 
0e58da397b1d
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents:
37
diff
changeset

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

159 