author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46821  ff6b0c1087f2 
child 58871  c399ae4b836f 
permissions  rwrr 
41777  1 
(* Title: ZF/Bool.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1992 University of Cambridge 
13328  4 
*) 
837  5 

13328  6 
header{*Booleans in ZermeloFraenkel Set Theory*} 
0  7 

16417  8 
theory Bool imports pair begin 
0  9 

24892  10 
abbreviation 
11 
one ("1") where 

12 
"1 == succ(0)" 

2539  13 

24892  14 
abbreviation 
15 
two ("2") where 

16 
"2 == succ(1)" 

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

17 

13328  18 
text{*2 is equal to bool, but is used as a number rather than a type.*} 
19 

24893  20 
definition "bool == {0,1}" 
21 

22 
definition "cond(b,c,d) == if(b=1,c,d)" 

13239  23 

24893  24 
definition "not(b) == cond(b,0,1)" 
13239  25 

24893  26 
definition 
27 
"and" :: "[i,i]=>i" (infixl "and" 70) where 

13239  28 
"a and b == cond(a,b,0)" 
29 

24893  30 
definition 
31 
or :: "[i,i]=>i" (infixl "or" 65) where 

13239  32 
"a or b == cond(a,1,b)" 
33 

24893  34 
definition 
35 
xor :: "[i,i]=>i" (infixl "xor" 65) where 

13239  36 
"a xor b == cond(a,not(b),b)" 
37 

38 

39 
lemmas bool_defs = bool_def cond_def 

40 

41 
lemma singleton_0: "{0} = 1" 

42 
by (simp add: succ_def) 

43 

44 
(* Introduction rules *) 

45 

46820  46 
lemma bool_1I [simp,TC]: "1 \<in> bool" 
13239  47 
by (simp add: bool_defs ) 
48 

46820  49 
lemma bool_0I [simp,TC]: "0 \<in> bool" 
13239  50 
by (simp add: bool_defs) 
51 

46820  52 
lemma one_not_0: "1\<noteq>0" 
13239  53 
by (simp add: bool_defs ) 
54 

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

45602  56 
lemmas one_neq_0 = one_not_0 [THEN notE] 
13239  57 

58 
lemma boolE: 

59 
"[ c: bool; c=1 ==> P; c=0 ==> P ] ==> P" 

24892  60 
by (simp add: bool_defs, blast) 
13239  61 

62 
(** cond **) 

63 

64 
(*1 means true*) 

65 
lemma cond_1 [simp]: "cond(1,c,d) = c" 

66 
by (simp add: bool_defs ) 

67 

68 
(*0 means false*) 

69 
lemma cond_0 [simp]: "cond(0,c,d) = d" 

70 
by (simp add: bool_defs ) 

71 

72 
lemma cond_type [TC]: "[ b: bool; c: A(1); d: A(0) ] ==> cond(b,c,d): A(b)" 

13269  73 
by (simp add: bool_defs, blast) 
13239  74 

75 
(*For Simp_tac and Blast_tac*) 

76 
lemma cond_simple_type: "[ b: bool; c: A; d: A ] ==> cond(b,c,d): A" 

77 
by (simp add: bool_defs ) 

78 

79 
lemma def_cond_1: "[ !!b. j(b)==cond(b,c,d) ] ==> j(1) = c" 

80 
by simp 

81 

82 
lemma def_cond_0: "[ !!b. j(b)==cond(b,c,d) ] ==> j(0) = d" 

83 
by simp 

84 

45602  85 
lemmas not_1 = not_def [THEN def_cond_1, simp] 
86 
lemmas not_0 = not_def [THEN def_cond_0, simp] 

13239  87 

45602  88 
lemmas and_1 = and_def [THEN def_cond_1, simp] 
89 
lemmas and_0 = and_def [THEN def_cond_0, simp] 

13239  90 

45602  91 
lemmas or_1 = or_def [THEN def_cond_1, simp] 
92 
lemmas or_0 = or_def [THEN def_cond_0, simp] 

13239  93 

45602  94 
lemmas xor_1 = xor_def [THEN def_cond_1, simp] 
95 
lemmas xor_0 = xor_def [THEN def_cond_0, simp] 

13239  96 

46820  97 
lemma not_type [TC]: "a:bool ==> not(a) \<in> bool" 
13239  98 
by (simp add: not_def) 
99 

46820  100 
lemma and_type [TC]: "[ a:bool; b:bool ] ==> a and b \<in> bool" 
13239  101 
by (simp add: and_def) 
102 

46820  103 
lemma or_type [TC]: "[ a:bool; b:bool ] ==> a or b \<in> bool" 
13239  104 
by (simp add: or_def) 
105 

46820  106 
lemma xor_type [TC]: "[ a:bool; b:bool ] ==> a xor b \<in> bool" 
13239  107 
by (simp add: xor_def) 
108 

109 
lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type 

110 
or_type xor_type 

111 

13356  112 
subsection{*Laws About 'not' *} 
13239  113 

114 
lemma not_not [simp]: "a:bool ==> not(not(a)) = a" 

115 
by (elim boolE, auto) 

116 

117 
lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)" 

118 
by (elim boolE, auto) 

119 

120 
lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" 

121 
by (elim boolE, auto) 

122 

13356  123 
subsection{*Laws About 'and' *} 
13239  124 

125 
lemma and_absorb [simp]: "a: bool ==> a and a = a" 

126 
by (elim boolE, auto) 

127 

128 
lemma and_commute: "[ a: bool; b:bool ] ==> a and b = b and a" 

129 
by (elim boolE, auto) 

130 

131 
lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)" 

132 
by (elim boolE, auto) 

133 

24892  134 
lemma and_or_distrib: "[ a: bool; b:bool; c:bool ] ==> 
13239  135 
(a or b) and c = (a and c) or (b and c)" 
136 
by (elim boolE, auto) 

137 

13356  138 
subsection{*Laws About 'or' *} 
13239  139 

140 
lemma or_absorb [simp]: "a: bool ==> a or a = a" 

141 
by (elim boolE, auto) 

142 

143 
lemma or_commute: "[ a: bool; b:bool ] ==> a or b = b or a" 

144 
by (elim boolE, auto) 

145 

146 
lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)" 

147 
by (elim boolE, auto) 

148 

24892  149 
lemma or_and_distrib: "[ a: bool; b: bool; c: bool ] ==> 
13239  150 
(a and b) or c = (a or c) and (b or c)" 
151 
by (elim boolE, auto) 

152 

13269  153 

24893  154 
definition 
155 
bool_of_o :: "o=>i" where 

13269  156 
"bool_of_o(P) == (if P then 1 else 0)" 
157 

158 
lemma [simp]: "bool_of_o(True) = 1" 

24892  159 
by (simp add: bool_of_o_def) 
13269  160 

161 
lemma [simp]: "bool_of_o(False) = 0" 

24892  162 
by (simp add: bool_of_o_def) 
13269  163 

164 
lemma [simp,TC]: "bool_of_o(P) \<in> bool" 

24892  165 
by (simp add: bool_of_o_def) 
13269  166 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

167 
lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P" 
24892  168 
by (simp add: bool_of_o_def) 
13269  169 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

170 
lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P" 
24892  171 
by (simp add: bool_of_o_def) 
13269  172 

0  173 
end 