src/HOL/Product_Type.thy
changeset 24844 98c006a30218
parent 24699 c6674504103f
child 25511 54db9b5080b8
     1.1 --- a/src/HOL/Product_Type.thy	Thu Oct 04 19:46:09 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 04 19:54:44 2007 +0200
     1.3 @@ -807,12 +807,10 @@
     1.4  declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
     1.5  declare prod_caseE' [elim!] prod_caseE [elim!]
     1.6  
     1.7 -lemma prod_case_split [code post]:
     1.8 +lemma prod_case_split:
     1.9    "prod_case = split"
    1.10    by (auto simp add: expand_fun_eq)
    1.11  
    1.12 -lemmas [code inline] = prod_case_split [symmetric]
    1.13 -
    1.14  
    1.15  subsection {* Further cases/induct rules for tuples *}
    1.16  
    1.17 @@ -902,6 +900,15 @@
    1.18  lemma [code func]:
    1.19    "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
    1.20  
    1.21 +lemma split_case_cert:
    1.22 +  assumes "CASE \<equiv> split f"
    1.23 +  shows "CASE (a, b) \<equiv> f a b"
    1.24 +  using assms by simp
    1.25 +
    1.26 +setup {*
    1.27 +  Code.add_case @{thm split_case_cert}
    1.28 +*}
    1.29 +
    1.30  code_type *
    1.31    (SML infix 2 "*")
    1.32    (OCaml infix 2 "*")