1 (* Title: ZF/bool |
|
2 ID: $Id$ |
|
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Booleans in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 bind_thms ("bool_defs", [bool_def,cond_def]); |
|
10 |
|
11 Goalw [succ_def] "{0} = 1"; |
|
12 by (rtac refl 1); |
|
13 qed "singleton_0"; |
|
14 |
|
15 (* Introduction rules *) |
|
16 |
|
17 Goalw bool_defs "1 : bool"; |
|
18 by (rtac (consI1 RS consI2) 1); |
|
19 qed "bool_1I"; |
|
20 |
|
21 Goalw bool_defs "0 : bool"; |
|
22 by (rtac consI1 1); |
|
23 qed "bool_0I"; |
|
24 |
|
25 Addsimps [bool_1I, bool_0I]; |
|
26 AddTCs [bool_1I, bool_0I]; |
|
27 |
|
28 Goalw bool_defs "1~=0"; |
|
29 by (rtac succ_not_0 1); |
|
30 qed "one_not_0"; |
|
31 |
|
32 (** 1=0 ==> R **) |
|
33 bind_thm ("one_neq_0", one_not_0 RS notE); |
|
34 |
|
35 val major::prems = Goalw bool_defs |
|
36 "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"; |
|
37 by (rtac (major RS consE) 1); |
|
38 by (REPEAT (eresolve_tac (singletonE::prems) 1)); |
|
39 qed "boolE"; |
|
40 |
|
41 (** cond **) |
|
42 |
|
43 (*1 means true*) |
|
44 Goalw bool_defs "cond(1,c,d) = c"; |
|
45 by (rtac (refl RS if_P) 1); |
|
46 qed "cond_1"; |
|
47 |
|
48 (*0 means false*) |
|
49 Goalw bool_defs "cond(0,c,d) = d"; |
|
50 by (rtac (succ_not_0 RS not_sym RS if_not_P) 1); |
|
51 qed "cond_0"; |
|
52 |
|
53 Addsimps [cond_1, cond_0]; |
|
54 |
|
55 fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i; |
|
56 |
|
57 |
|
58 Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)"; |
|
59 by (bool_tac 1); |
|
60 qed "cond_type"; |
|
61 AddTCs [cond_type]; |
|
62 |
|
63 (*For Simp_tac and Blast_tac*) |
|
64 Goal "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A"; |
|
65 by (bool_tac 1); |
|
66 qed "cond_simple_type"; |
|
67 |
|
68 val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"; |
|
69 by (rewtac rew); |
|
70 by (rtac cond_1 1); |
|
71 qed "def_cond_1"; |
|
72 |
|
73 val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"; |
|
74 by (rewtac rew); |
|
75 by (rtac cond_0 1); |
|
76 qed "def_cond_0"; |
|
77 |
|
78 fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)]; |
|
79 |
|
80 val [not_1, not_0] = conds not_def; |
|
81 val [and_1, and_0] = conds and_def; |
|
82 val [or_1, or_0] = conds or_def; |
|
83 val [xor_1, xor_0] = conds xor_def; |
|
84 |
|
85 bind_thm ("not_1", not_1); |
|
86 bind_thm ("not_0", not_0); |
|
87 bind_thm ("and_1", and_1); |
|
88 bind_thm ("and_0", and_0); |
|
89 bind_thm ("or_1", or_1); |
|
90 bind_thm ("or_0", or_0); |
|
91 bind_thm ("xor_1", xor_1); |
|
92 bind_thm ("xor_0", xor_0); |
|
93 |
|
94 Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0]; |
|
95 |
|
96 Goalw [not_def] "a:bool ==> not(a) : bool"; |
|
97 by (Asm_simp_tac 1); |
|
98 qed "not_type"; |
|
99 |
|
100 Goalw [and_def] "[| a:bool; b:bool |] ==> a and b : bool"; |
|
101 by (Asm_simp_tac 1); |
|
102 qed "and_type"; |
|
103 |
|
104 Goalw [or_def] "[| a:bool; b:bool |] ==> a or b : bool"; |
|
105 by (Asm_simp_tac 1); |
|
106 qed "or_type"; |
|
107 |
|
108 AddTCs [not_type, and_type, or_type]; |
|
109 |
|
110 Goalw [xor_def] "[| a:bool; b:bool |] ==> a xor b : bool"; |
|
111 by (Asm_simp_tac 1); |
|
112 qed "xor_type"; |
|
113 |
|
114 AddTCs [xor_type]; |
|
115 |
|
116 bind_thms ("bool_typechecks", |
|
117 [bool_1I, bool_0I, cond_type, not_type, and_type, or_type, xor_type]); |
|
118 |
|
119 (*** Laws for 'not' ***) |
|
120 |
|
121 Goal "a:bool ==> not(not(a)) = a"; |
|
122 by (bool_tac 1); |
|
123 qed "not_not"; |
|
124 |
|
125 Goal "a:bool ==> not(a and b) = not(a) or not(b)"; |
|
126 by (bool_tac 1); |
|
127 qed "not_and"; |
|
128 |
|
129 Goal "a:bool ==> not(a or b) = not(a) and not(b)"; |
|
130 by (bool_tac 1); |
|
131 qed "not_or"; |
|
132 |
|
133 Addsimps [not_not, not_and, not_or]; |
|
134 |
|
135 (*** Laws about 'and' ***) |
|
136 |
|
137 Goal "a: bool ==> a and a = a"; |
|
138 by (bool_tac 1); |
|
139 qed "and_absorb"; |
|
140 |
|
141 Addsimps [and_absorb]; |
|
142 |
|
143 Goal "[| a: bool; b:bool |] ==> a and b = b and a"; |
|
144 by (bool_tac 1); |
|
145 qed "and_commute"; |
|
146 |
|
147 Goal "a: bool ==> (a and b) and c = a and (b and c)"; |
|
148 by (bool_tac 1); |
|
149 qed "and_assoc"; |
|
150 |
|
151 Goal "[| a: bool; b:bool; c:bool |] ==> \ |
|
152 \ (a or b) and c = (a and c) or (b and c)"; |
|
153 by (bool_tac 1); |
|
154 qed "and_or_distrib"; |
|
155 |
|
156 (** binary orion **) |
|
157 |
|
158 Goal "a: bool ==> a or a = a"; |
|
159 by (bool_tac 1); |
|
160 qed "or_absorb"; |
|
161 |
|
162 Addsimps [or_absorb]; |
|
163 |
|
164 Goal "[| a: bool; b:bool |] ==> a or b = b or a"; |
|
165 by (bool_tac 1); |
|
166 qed "or_commute"; |
|
167 |
|
168 Goal "a: bool ==> (a or b) or c = a or (b or c)"; |
|
169 by (bool_tac 1); |
|
170 qed "or_assoc"; |
|
171 |
|
172 Goal "[| a: bool; b: bool; c: bool |] ==> \ |
|
173 \ (a and b) or c = (a or c) and (b or c)"; |
|
174 by (bool_tac 1); |
|
175 qed "or_and_distrib"; |
|
176 |
|