equal
deleted
inserted
replaced
47 lemma If_case_cert: |
47 lemma If_case_cert: |
48 assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
48 assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
49 shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)" |
49 shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)" |
50 using assms by simp_all |
50 using assms by simp_all |
51 |
51 |
52 setup \<open>Code.add_case @{thm If_case_cert}\<close> |
52 setup \<open>Code.declare_case_global @{thm If_case_cert}\<close> |
53 |
53 |
54 code_printing |
54 code_printing |
55 constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "==" |
55 constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "==" |
56 | class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) - |
56 | class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) - |
57 |
57 |