220 |
220 |
221 lemmas [code] = imp_conv_disj |
221 lemmas [code] = imp_conv_disj |
222 |
222 |
223 subsubsection {* Codegenerator setup *} |
223 subsubsection {* Codegenerator setup *} |
224 |
224 |
225 lemma [code]: |
225 lemma [code fun]: |
226 "(\<not> True) = False" by (rule HOL.simp_thms) |
226 "(\<not> True) = False" by (rule HOL.simp_thms) |
227 |
227 |
228 lemma [code]: |
228 lemma [code fun]: |
229 "(\<not> False) = True" by (rule HOL.simp_thms) |
229 "(\<not> False) = True" by (rule HOL.simp_thms) |
230 |
230 |
231 lemma [code]: |
231 lemma [code fun]: |
232 shows "(False \<and> x) = False" |
232 shows "(False \<and> x) = False" |
233 and "(True \<and> x) = x" |
233 and "(True \<and> x) = x" |
234 and "(x \<and> False) = False" |
234 and "(x \<and> False) = False" |
235 and "(x \<and> True) = x" by simp_all |
235 and "(x \<and> True) = x" by simp_all |
236 |
236 |
237 lemma [code]: |
237 lemma [code fun]: |
238 shows "(False \<or> x) = x" |
238 shows "(False \<or> x) = x" |
239 and "(True \<or> x) = True" |
239 and "(True \<or> x) = True" |
240 and "(x \<or> False) = x" |
240 and "(x \<or> False) = x" |
241 and "(x \<or> True) = True" by simp_all |
241 and "(x \<or> True) = True" by simp_all |
242 |
242 |
243 declare |
243 declare |
244 if_True [code] |
244 if_True [code fun] |
245 if_False [code] |
245 if_False [code fun] |
246 fst_conv [code] |
246 fst_conv [code] |
247 snd_conv [code] |
247 snd_conv [code] |
248 |
248 |
249 lemma [code unfold]: |
249 lemma [code unfolt]: |
250 "1 == Suc 0" by simp |
250 "1 == Suc 0" by simp |
251 |
251 |
252 code_generate True False Not "op &" "op |" If |
252 code_generate True False Not "op &" "op |" If |
253 |
253 |
254 code_syntax_tyco bool |
254 code_syntax_tyco bool |