src/HOL/Code_Setup.thy
changeset 28856 5e009a80fe6d
parent 28740 22a8125d66fa
child 29105 8f38bf68d42e
equal deleted inserted replaced
28855:5d21a3e7303c 28856:5e009a80fe6d
    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}