19 |
19 |
20 code_datatype Trueprop "prop" |
20 code_datatype Trueprop "prop" |
21 |
21 |
22 text {* Code equations *} |
22 text {* Code equations *} |
23 |
23 |
24 lemma [code func]: |
24 lemma [code]: |
25 shows "False \<and> x \<longleftrightarrow> False" |
25 shows "False \<and> x \<longleftrightarrow> False" |
26 and "True \<and> x \<longleftrightarrow> x" |
26 and "True \<and> x \<longleftrightarrow> x" |
27 and "x \<and> False \<longleftrightarrow> False" |
27 and "x \<and> False \<longleftrightarrow> False" |
28 and "x \<and> True \<longleftrightarrow> x" by simp_all |
28 and "x \<and> True \<longleftrightarrow> x" by simp_all |
29 |
29 |
30 lemma [code func]: |
30 lemma [code]: |
31 shows "False \<or> x \<longleftrightarrow> x" |
31 shows "False \<or> x \<longleftrightarrow> x" |
32 and "True \<or> x \<longleftrightarrow> True" |
32 and "True \<or> x \<longleftrightarrow> True" |
33 and "x \<or> False \<longleftrightarrow> x" |
33 and "x \<or> False \<longleftrightarrow> x" |
34 and "x \<or> True \<longleftrightarrow> True" by simp_all |
34 and "x \<or> True \<longleftrightarrow> True" by simp_all |
35 |
35 |
36 lemma [code func]: |
36 lemma [code]: |
37 shows "\<not> True \<longleftrightarrow> False" |
37 shows "\<not> True \<longleftrightarrow> False" |
38 and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+ |
38 and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+ |
39 |
39 |
40 lemmas [code func] = Let_def if_True if_False |
40 lemmas [code] = Let_def if_True if_False |
41 |
41 |
42 lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj |
42 lemmas [code, code unfold, symmetric, code post] = imp_conv_disj |
43 |
43 |
44 text {* Equality *} |
44 text {* Equality *} |
45 |
45 |
46 context eq |
46 context eq |
47 begin |
47 begin |
48 |
48 |
49 lemma equals_eq [code inline, code func]: "op = \<equiv> eq" |
49 lemma equals_eq [code inline, code]: "op = \<equiv> eq" |
50 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) |
50 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) |
51 |
51 |
52 declare eq [code unfold, code inline del] |
52 declare eq [code unfold, code inline del] |
53 |
53 |
54 declare equals_eq [symmetric, code post] |
54 declare equals_eq [symmetric, code post] |