src/HOL/Product_Type.thy
changeset 22886 cdff6ef76009
parent 22838 466599ecf610
child 23247 b99dce43d252
     1.1 --- a/src/HOL/Product_Type.thy	Wed May 09 07:53:04 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed May 09 07:53:06 2007 +0200
     1.3 @@ -231,10 +231,10 @@
     1.4  lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
     1.5    by (blast elim!: Pair_inject)
     1.6  
     1.7 -lemma fst_conv [simp]: "fst (a, b) = a"
     1.8 +lemma fst_conv [simp, code]: "fst (a, b) = a"
     1.9    unfolding fst_def by blast
    1.10  
    1.11 -lemma snd_conv [simp]: "snd (a, b) = b"
    1.12 +lemma snd_conv [simp, code]: "snd (a, b) = b"
    1.13    unfolding snd_def by blast
    1.14  
    1.15  lemma fst_eqD: "fst (x, y) = a ==> x = a"
    1.16 @@ -602,18 +602,18 @@
    1.17  definition
    1.18    upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
    1.19  where
    1.20 -  "upd_fst f = prod_fun f id"
    1.21 +  [code func del]: "upd_fst f = prod_fun f id"
    1.22  
    1.23  definition
    1.24    upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
    1.25  where
    1.26 -  "upd_snd f = prod_fun id f"
    1.27 +  [code func del]: "upd_snd f = prod_fun id f"
    1.28  
    1.29 -lemma upd_fst_conv [simp, code func]:
    1.30 +lemma upd_fst_conv [simp, code]:
    1.31    "upd_fst f (x, y) = (f x, y)" 
    1.32    by (simp add: upd_fst_def)
    1.33  
    1.34 -lemma upd_snd_conv [simp, code func]:
    1.35 +lemma upd_snd_conv [simp, code]:
    1.36    "upd_snd f (x, y) = (x, f y)" 
    1.37    by (simp add: upd_snd_def)
    1.38  
    1.39 @@ -776,8 +776,6 @@
    1.40  
    1.41  subsection {* Code generator setup *}
    1.42  
    1.43 -lemmas [code func] = fst_conv snd_conv
    1.44 -
    1.45  instance unit :: eq ..
    1.46  
    1.47  lemma [code func]:
    1.48 @@ -910,8 +908,7 @@
    1.49  
    1.50    Codegen.add_codegen "let_codegen" let_codegen
    1.51    #> Codegen.add_codegen "split_codegen" split_codegen
    1.52 -  #> CodegenPackage.add_appconst
    1.53 -       ("Let", CodegenPackage.appgen_let)
    1.54 +  #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let)
    1.55  
    1.56  end
    1.57  *}