equal
deleted
inserted
replaced
76 assumes "CASE \<equiv> (\<lambda>x. Let x f)" |
76 assumes "CASE \<equiv> (\<lambda>x. Let x f)" |
77 shows "CASE x \<equiv> f x" |
77 shows "CASE x \<equiv> f x" |
78 using assms by simp_all |
78 using assms by simp_all |
79 |
79 |
80 lemma If_case_cert: |
80 lemma If_case_cert: |
81 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
|
82 assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
81 assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
83 shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)" |
82 shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)" |
84 using assms by simp_all |
83 using assms by simp_all |
85 |
84 |
86 setup {* |
85 setup {* |
87 Code.add_case @{thm Let_case_cert} |
86 Code.add_case @{thm Let_case_cert} |
88 #> Code.add_case @{thm If_case_cert} |
87 #> Code.add_case @{thm If_case_cert} |