src/HOL/Datatype.thy
changeset 21905 500f91bf992c
parent 21669 c68717c16013
child 22230 bdec4a82f385
     1.1 --- a/src/HOL/Datatype.thy	Wed Dec 27 19:09:53 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Dec 27 19:09:54 2006 +0100
     1.3 @@ -719,6 +719,8 @@
     1.4  
     1.5  subsubsection {* Code generator setup *}
     1.6  
     1.7 +lemmas [code] = fst_conv snd_conv imp_conv_disj
     1.8 +
     1.9  definition
    1.10    is_none :: "'a option \<Rightarrow> bool" where
    1.11    is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    1.12 @@ -728,72 +730,20 @@
    1.13      and "is_none (Some x) \<longleftrightarrow> False"
    1.14    unfolding is_none_none [symmetric] by simp_all
    1.15  
    1.16 -hide (open) const is_none
    1.17 -
    1.18 -lemmas [code] = imp_conv_disj
    1.19 -
    1.20 -lemma [code func]:
    1.21 -  "(\<not> True) = False" by (rule HOL.simp_thms)
    1.22 -
    1.23 -lemma [code func]:
    1.24 -  "(\<not> False) = True" by (rule HOL.simp_thms)
    1.25 -
    1.26 -lemma [code func]:
    1.27 -  shows "(False \<and> x) = False"
    1.28 -    and "(True \<and> x) = x"
    1.29 -    and "(x \<and> False) = False"
    1.30 -    and "(x \<and> True) = x" by simp_all
    1.31 -
    1.32 -lemma [code func]:
    1.33 -  shows "(False \<or> x) = x"
    1.34 -    and "(True \<or> x) = True"
    1.35 -    and "(x \<or> False) = x"
    1.36 -    and "(x \<or> True) = True" by simp_all
    1.37 -
    1.38 -declare
    1.39 -  if_True [code func]
    1.40 -  if_False [code func]
    1.41 -  fst_conv [code]
    1.42 -  snd_conv [code]
    1.43 -
    1.44  lemma split_is_prod_case [code inline]:
    1.45 -    "split = prod_case"
    1.46 +  "split = prod_case"
    1.47    by (simp add: expand_fun_eq split_def prod.cases)
    1.48  
    1.49 -code_type bool
    1.50 -  (SML "bool")
    1.51 -  (Haskell "Bool")
    1.52 -
    1.53 -code_const True and False and Not and "op &" and "op |" and If
    1.54 -  (SML "true" and "false" and "not"
    1.55 -    and infixl 1 "andalso" and infixl 0 "orelse"
    1.56 -    and "!(if (_)/ then (_)/ else (_))")
    1.57 -  (Haskell "True" and "False" and "not"
    1.58 -    and infixl 3 "&&" and infixl 2 "||"
    1.59 -    and "!(if (_)/ then (_)/ else (_))")
    1.60 -
    1.61 -code_type *
    1.62 -  (SML infix 2 "*")
    1.63 -  (Haskell "!((_),/ (_))")
    1.64 -
    1.65 -code_const Pair
    1.66 -  (SML "!((_),/ (_))")
    1.67 -  (Haskell "!((_),/ (_))")
    1.68 -
    1.69 -code_type unit
    1.70 -  (SML "unit")
    1.71 -  (Haskell "()")
    1.72 -
    1.73 -code_const Unity
    1.74 -  (SML "()")
    1.75 -  (Haskell "()")
    1.76 +hide (open) const is_none
    1.77  
    1.78  code_type option
    1.79    (SML "_ option")
    1.80 +  (OCaml "_ option")
    1.81    (Haskell "Maybe _")
    1.82  
    1.83  code_const None and Some
    1.84    (SML "NONE" and "SOME")
    1.85 +  (OCaml "None" and "Some _")
    1.86    (Haskell "Nothing" and "Just")
    1.87  
    1.88  code_instance option :: eq
    1.89 @@ -803,10 +753,10 @@
    1.90    (Haskell infixl 4 "==")
    1.91  
    1.92  code_reserved SML
    1.93 -  bool true false not unit option NONE SOME
    1.94 +  option NONE SOME
    1.95  
    1.96 -code_reserved Haskell
    1.97 -  Bool True False not Maybe Nothing Just
    1.98 +code_reserved OCaml
    1.99 +  option None Some
   1.100  
   1.101  
   1.102  subsection {* Basic ML bindings *}