cleaned up
authorhaftmann
Tue Oct 31 09:28:54 2006 +0100 (2006-10-31)
changeset 21111624ed9c7c4fe
parent 21110 fc98cb66c5c3
child 21112 c9e068f994ba
cleaned up
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Oct 31 09:28:53 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Oct 31 09:28:54 2006 +0100
     1.3 @@ -723,17 +723,18 @@
     1.4    by (rule ext) (simp split: sum.split)
     1.5  
     1.6  
     1.7 -subsubsection {* Codegenerator setup *}
     1.8 +subsubsection {* Code generator setup *}
     1.9  
    1.10 -consts
    1.11 +definition
    1.12    is_none :: "'a option \<Rightarrow> bool"
    1.13 -primrec
    1.14 -  "is_none None = True"
    1.15 -  "is_none (Some x) = False"
    1.16 +  is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    1.17  
    1.18 -lemma is_none_none [code inline, symmetric, normal post]:
    1.19 -    "(x = None) = (is_none x)" 
    1.20 -  by (cases x) simp_all
    1.21 +lemma is_none_code [code]:
    1.22 +  shows "is_none None \<longleftrightarrow> True"
    1.23 +    and "is_none (Some x) \<longleftrightarrow> False"
    1.24 +  unfolding is_none_none [symmetric] by simp_all
    1.25 +
    1.26 +hide (open) const is_none
    1.27  
    1.28  lemmas [code] = imp_conv_disj
    1.29  
    1.30 @@ -766,40 +767,40 @@
    1.31    by (simp add: expand_fun_eq split_def prod.cases)
    1.32  
    1.33  code_type bool
    1.34 -  (SML target_atom "bool")
    1.35 -  (Haskell target_atom "Bool")
    1.36 +  (SML "bool")
    1.37 +  (Haskell "Bool")
    1.38  
    1.39  code_const True and False and Not and "op &" and "op |" and If
    1.40 -  (SML target_atom "true" and target_atom "false" and target_atom "not"
    1.41 +  (SML "true" and "false" and "not"
    1.42      and infixl 1 "andalso" and infixl 0 "orelse"
    1.43 -    and target_atom "(if __/ then __/ else __)")
    1.44 -  (Haskell target_atom "True" and target_atom "False" and target_atom "not"
    1.45 +    and "!(if __/ then __/ else __)")
    1.46 +  (Haskell "True" and "False" and "not"
    1.47      and infixl 3 "&&" and infixl 2 "||"
    1.48 -    and target_atom "(if __/ then __/ else __)")
    1.49 +    and "!(if __/ then __/ else __)")
    1.50  
    1.51  code_type *
    1.52    (SML infix 2 "*")
    1.53 -  (Haskell target_atom "(__,/ __)")
    1.54 +  (Haskell "!(__,/ __)")
    1.55  
    1.56  code_const Pair
    1.57 -  (SML target_atom "(__,/ __)")
    1.58 -  (Haskell target_atom "(__,/ __)")
    1.59 +  (SML "!(__,/ __)")
    1.60 +  (Haskell "!(__,/ __)")
    1.61  
    1.62  code_type unit
    1.63 -  (SML target_atom "unit")
    1.64 -  (Haskell target_atom "()")
    1.65 +  (SML "unit")
    1.66 +  (Haskell "()")
    1.67  
    1.68  code_const Unity
    1.69 -  (SML target_atom "()")
    1.70 -  (Haskell target_atom "()")
    1.71 +  (SML "()")
    1.72 +  (Haskell "()")
    1.73  
    1.74  code_type option
    1.75    (SML "_ option")
    1.76    (Haskell "Maybe _")
    1.77  
    1.78  code_const None and Some
    1.79 -  (SML target_atom "NONE" and target_atom "SOME")
    1.80 -  (Haskell target_atom "Nothing" and target_atom "Just")
    1.81 +  (SML "NONE" and "SOME")
    1.82 +  (Haskell "Nothing" and "Just")
    1.83  
    1.84  code_instance option :: eq
    1.85    (Haskell -)