110 by (simp add: xor_def) |
110 by (simp add: xor_def) |
111 |
111 |
112 lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type |
112 lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type |
113 or_type xor_type |
113 or_type xor_type |
114 |
114 |
115 (*** Laws for 'not' ***) |
115 subsection{*Laws About 'not' *} |
116 |
116 |
117 lemma not_not [simp]: "a:bool ==> not(not(a)) = a" |
117 lemma not_not [simp]: "a:bool ==> not(not(a)) = a" |
118 by (elim boolE, auto) |
118 by (elim boolE, auto) |
119 |
119 |
120 lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)" |
120 lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)" |
121 by (elim boolE, auto) |
121 by (elim boolE, auto) |
122 |
122 |
123 lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" |
123 lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" |
124 by (elim boolE, auto) |
124 by (elim boolE, auto) |
125 |
125 |
126 (*** Laws about 'and' ***) |
126 subsection{*Laws About 'and' *} |
127 |
127 |
128 lemma and_absorb [simp]: "a: bool ==> a and a = a" |
128 lemma and_absorb [simp]: "a: bool ==> a and a = a" |
129 by (elim boolE, auto) |
129 by (elim boolE, auto) |
130 |
130 |
131 lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a" |
131 lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a" |
136 |
136 |
137 lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==> |
137 lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==> |
138 (a or b) and c = (a and c) or (b and c)" |
138 (a or b) and c = (a and c) or (b and c)" |
139 by (elim boolE, auto) |
139 by (elim boolE, auto) |
140 |
140 |
141 (** binary 'or' **) |
141 subsection{*Laws About 'or' *} |
142 |
142 |
143 lemma or_absorb [simp]: "a: bool ==> a or a = a" |
143 lemma or_absorb [simp]: "a: bool ==> a or a = a" |
144 by (elim boolE, auto) |
144 by (elim boolE, auto) |
145 |
145 |
146 lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a" |
146 lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a" |