author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 13356 | c9cfe1638bf2 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/bool.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
13328 | 6 |
*) |
837 | 7 |
|
13328 | 8 |
header{*Booleans in Zermelo-Fraenkel Set Theory*} |
0 | 9 |
|
13239 | 10 |
theory Bool = pair: |
0 | 11 |
|
2539 | 12 |
syntax |
13 |
"1" :: i ("1") |
|
14 |
"2" :: i ("2") |
|
15 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
16 |
translations |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
17 |
"1" == "succ(0)" |
837 | 18 |
"2" == "succ(1)" |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
19 |
|
13328 | 20 |
text{*2 is equal to bool, but is used as a number rather than a type.*} |
21 |
||
13239 | 22 |
constdefs |
23 |
bool :: i |
|
24 |
"bool == {0,1}" |
|
25 |
||
26 |
cond :: "[i,i,i]=>i" |
|
27 |
"cond(b,c,d) == if(b=1,c,d)" |
|
28 |
||
29 |
not :: "i=>i" |
|
30 |
"not(b) == cond(b,0,1)" |
|
31 |
||
32 |
"and" :: "[i,i]=>i" (infixl "and" 70) |
|
33 |
"a and b == cond(a,b,0)" |
|
34 |
||
35 |
or :: "[i,i]=>i" (infixl "or" 65) |
|
36 |
"a or b == cond(a,1,b)" |
|
37 |
||
38 |
xor :: "[i,i]=>i" (infixl "xor" 65) |
|
39 |
"a xor b == cond(a,not(b),b)" |
|
40 |
||
41 |
||
42 |
lemmas bool_defs = bool_def cond_def |
|
43 |
||
44 |
lemma singleton_0: "{0} = 1" |
|
45 |
by (simp add: succ_def) |
|
46 |
||
47 |
(* Introduction rules *) |
|
48 |
||
49 |
lemma bool_1I [simp,TC]: "1 : bool" |
|
50 |
by (simp add: bool_defs ) |
|
51 |
||
52 |
lemma bool_0I [simp,TC]: "0 : bool" |
|
53 |
by (simp add: bool_defs) |
|
54 |
||
55 |
lemma one_not_0: "1~=0" |
|
56 |
by (simp add: bool_defs ) |
|
57 |
||
58 |
(** 1=0 ==> R **) |
|
59 |
lemmas one_neq_0 = one_not_0 [THEN notE, standard] |
|
60 |
||
61 |
lemma boolE: |
|
62 |
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P" |
|
63 |
by (simp add: bool_defs, blast) |
|
64 |
||
65 |
(** cond **) |
|
66 |
||
67 |
(*1 means true*) |
|
68 |
lemma cond_1 [simp]: "cond(1,c,d) = c" |
|
69 |
by (simp add: bool_defs ) |
|
70 |
||
71 |
(*0 means false*) |
|
72 |
lemma cond_0 [simp]: "cond(0,c,d) = d" |
|
73 |
by (simp add: bool_defs ) |
|
74 |
||
75 |
lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)" |
|
13269 | 76 |
by (simp add: bool_defs, blast) |
13239 | 77 |
|
78 |
(*For Simp_tac and Blast_tac*) |
|
79 |
lemma cond_simple_type: "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A" |
|
80 |
by (simp add: bool_defs ) |
|
81 |
||
82 |
lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c" |
|
83 |
by simp |
|
84 |
||
85 |
lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d" |
|
86 |
by simp |
|
87 |
||
88 |
lemmas not_1 = not_def [THEN def_cond_1, standard, simp] |
|
89 |
lemmas not_0 = not_def [THEN def_cond_0, standard, simp] |
|
90 |
||
91 |
lemmas and_1 = and_def [THEN def_cond_1, standard, simp] |
|
92 |
lemmas and_0 = and_def [THEN def_cond_0, standard, simp] |
|
93 |
||
94 |
lemmas or_1 = or_def [THEN def_cond_1, standard, simp] |
|
95 |
lemmas or_0 = or_def [THEN def_cond_0, standard, simp] |
|
96 |
||
97 |
lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp] |
|
98 |
lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp] |
|
99 |
||
100 |
lemma not_type [TC]: "a:bool ==> not(a) : bool" |
|
101 |
by (simp add: not_def) |
|
102 |
||
103 |
lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b : bool" |
|
104 |
by (simp add: and_def) |
|
105 |
||
106 |
lemma or_type [TC]: "[| a:bool; b:bool |] ==> a or b : bool" |
|
107 |
by (simp add: or_def) |
|
108 |
||
109 |
lemma xor_type [TC]: "[| a:bool; b:bool |] ==> a xor b : bool" |
|
110 |
by (simp add: xor_def) |
|
111 |
||
112 |
lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type |
|
113 |
or_type xor_type |
|
114 |
||
13356 | 115 |
subsection{*Laws About 'not' *} |
13239 | 116 |
|
117 |
lemma not_not [simp]: "a:bool ==> not(not(a)) = a" |
|
118 |
by (elim boolE, auto) |
|
119 |
||
120 |
lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)" |
|
121 |
by (elim boolE, auto) |
|
122 |
||
123 |
lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" |
|
124 |
by (elim boolE, auto) |
|
125 |
||
13356 | 126 |
subsection{*Laws About 'and' *} |
13239 | 127 |
|
128 |
lemma and_absorb [simp]: "a: bool ==> a and a = a" |
|
129 |
by (elim boolE, auto) |
|
130 |
||
131 |
lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a" |
|
132 |
by (elim boolE, auto) |
|
133 |
||
134 |
lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)" |
|
135 |
by (elim boolE, auto) |
|
136 |
||
137 |
lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==> |
|
138 |
(a or b) and c = (a and c) or (b and c)" |
|
139 |
by (elim boolE, auto) |
|
140 |
||
13356 | 141 |
subsection{*Laws About 'or' *} |
13239 | 142 |
|
143 |
lemma or_absorb [simp]: "a: bool ==> a or a = a" |
|
144 |
by (elim boolE, auto) |
|
145 |
||
146 |
lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a" |
|
147 |
by (elim boolE, auto) |
|
148 |
||
149 |
lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)" |
|
150 |
by (elim boolE, auto) |
|
151 |
||
152 |
lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==> |
|
153 |
(a and b) or c = (a or c) and (b or c)" |
|
154 |
by (elim boolE, auto) |
|
155 |
||
13269 | 156 |
|
157 |
constdefs bool_of_o :: "o=>i" |
|
158 |
"bool_of_o(P) == (if P then 1 else 0)" |
|
159 |
||
160 |
lemma [simp]: "bool_of_o(True) = 1" |
|
161 |
by (simp add: bool_of_o_def) |
|
162 |
||
163 |
lemma [simp]: "bool_of_o(False) = 0" |
|
164 |
by (simp add: bool_of_o_def) |
|
165 |
||
166 |
lemma [simp,TC]: "bool_of_o(P) \<in> bool" |
|
167 |
by (simp add: bool_of_o_def) |
|
168 |
||
169 |
lemma [simp]: "(bool_of_o(P) = 1) <-> P" |
|
170 |
by (simp add: bool_of_o_def) |
|
171 |
||
172 |
lemma [simp]: "(bool_of_o(P) = 0) <-> ~P" |
|
173 |
by (simp add: bool_of_o_def) |
|
174 |
||
13239 | 175 |
ML |
176 |
{* |
|
177 |
val bool_def = thm "bool_def"; |
|
178 |
||
179 |
val bool_defs = thms "bool_defs"; |
|
180 |
val singleton_0 = thm "singleton_0"; |
|
181 |
val bool_1I = thm "bool_1I"; |
|
182 |
val bool_0I = thm "bool_0I"; |
|
183 |
val one_not_0 = thm "one_not_0"; |
|
184 |
val one_neq_0 = thm "one_neq_0"; |
|
185 |
val boolE = thm "boolE"; |
|
186 |
val cond_1 = thm "cond_1"; |
|
187 |
val cond_0 = thm "cond_0"; |
|
188 |
val cond_type = thm "cond_type"; |
|
189 |
val cond_simple_type = thm "cond_simple_type"; |
|
190 |
val def_cond_1 = thm "def_cond_1"; |
|
191 |
val def_cond_0 = thm "def_cond_0"; |
|
192 |
val not_1 = thm "not_1"; |
|
193 |
val not_0 = thm "not_0"; |
|
194 |
val and_1 = thm "and_1"; |
|
195 |
val and_0 = thm "and_0"; |
|
196 |
val or_1 = thm "or_1"; |
|
197 |
val or_0 = thm "or_0"; |
|
198 |
val xor_1 = thm "xor_1"; |
|
199 |
val xor_0 = thm "xor_0"; |
|
200 |
val not_type = thm "not_type"; |
|
201 |
val and_type = thm "and_type"; |
|
202 |
val or_type = thm "or_type"; |
|
203 |
val xor_type = thm "xor_type"; |
|
204 |
val bool_typechecks = thms "bool_typechecks"; |
|
205 |
val not_not = thm "not_not"; |
|
206 |
val not_and = thm "not_and"; |
|
207 |
val not_or = thm "not_or"; |
|
208 |
val and_absorb = thm "and_absorb"; |
|
209 |
val and_commute = thm "and_commute"; |
|
210 |
val and_assoc = thm "and_assoc"; |
|
211 |
val and_or_distrib = thm "and_or_distrib"; |
|
212 |
val or_absorb = thm "or_absorb"; |
|
213 |
val or_commute = thm "or_commute"; |
|
214 |
val or_assoc = thm "or_assoc"; |
|
215 |
val or_and_distrib = thm "or_and_distrib"; |
|
216 |
*} |
|
217 |
||
0 | 218 |
end |