src/HOL/Product_Type.thy
changeset 21908 d02ba728cd56
parent 21454 a1937c51ed88
child 22349 a4e82dd93202
     1.1 --- a/src/HOL/Product_Type.thy	Wed Dec 27 19:09:56 2006 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Dec 27 19:09:57 2006 +0100
     1.3 @@ -773,27 +773,55 @@
     1.4  
     1.5  subsection {* Code generator setup *}
     1.6  
     1.7 +lemmas [code func] = fst_conv snd_conv
     1.8 +
     1.9  instance unit :: eq ..
    1.10  
    1.11  lemma [code func]:
    1.12    "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
    1.13  
    1.14 +code_type unit
    1.15 +  (SML "unit")
    1.16 +  (OCaml "unit")
    1.17 +  (Haskell "()")
    1.18 +
    1.19  code_instance unit :: eq
    1.20    (Haskell -)
    1.21  
    1.22 +code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.23 +  (Haskell infixl 4 "==")
    1.24 +
    1.25 +code_const Unity
    1.26 +  (SML "()")
    1.27 +  (OCaml "()")
    1.28 +  (Haskell "()")
    1.29 +
    1.30 +code_reserved SML
    1.31 +  unit
    1.32 +
    1.33 +code_reserved OCaml
    1.34 +  unit
    1.35 +
    1.36  instance * :: (eq, eq) eq ..
    1.37  
    1.38  lemma [code func]:
    1.39    "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
    1.40  
    1.41 +code_type *
    1.42 +  (SML infix 2 "*")
    1.43 +  (OCaml infix 2 "*")
    1.44 +  (Haskell "!((_),/ (_))")
    1.45 +
    1.46  code_instance * :: eq
    1.47    (Haskell -)
    1.48  
    1.49 -code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.50 +code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.51    (Haskell infixl 4 "==")
    1.52  
    1.53 -code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.54 -  (Haskell infixl 4 "==")
    1.55 +code_const Pair
    1.56 +  (SML "!((_),/ (_))")
    1.57 +  (OCaml "!((_),/ (_))")
    1.58 +  (Haskell "!((_),/ (_))")
    1.59  
    1.60  types_code
    1.61    "*"     ("(_ */ _)")
    1.62 @@ -807,7 +835,9 @@
    1.63  consts_code
    1.64    "Pair"    ("(_,/ _)")
    1.65  
    1.66 -ML {*
    1.67 +setup {*
    1.68 +
    1.69 +let
    1.70  
    1.71  fun strip_abs_split 0 t = ([], t)
    1.72    | strip_abs_split i (Abs (s, T, t)) =
    1.73 @@ -870,18 +900,17 @@
    1.74         | _ => NONE)
    1.75    | _ => NONE);
    1.76  
    1.77 -val prod_codegen_setup =
    1.78 +in
    1.79 +
    1.80    Codegen.add_codegen "let_codegen" let_codegen
    1.81    #> Codegen.add_codegen "split_codegen" split_codegen
    1.82    #> CodegenPackage.add_appconst
    1.83         ("Let", CodegenPackage.appgen_let)
    1.84  
    1.85 +end
    1.86  *}
    1.87  
    1.88 -setup prod_codegen_setup
    1.89 -
    1.90 -ML
    1.91 -{*
    1.92 +ML {*
    1.93  val Collect_split = thm "Collect_split";
    1.94  val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    1.95  val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";