src/HOL/Datatype.thy
changeset 19138 42ff710d432f
parent 19111 1f6112de1d0f
child 19150 1457d810b408
     1.1 --- a/src/HOL/Datatype.thy	Sat Feb 25 15:19:19 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sat Feb 25 15:19:47 2006 +0100
     1.3 @@ -222,6 +222,38 @@
     1.4  
     1.5  subsubsection {* Codegenerator setup *}
     1.6  
     1.7 +lemma [code]:
     1.8 +  "(\<not> True) = False" by (rule HOL.simp_thms)
     1.9 +
    1.10 +lemma [code]:
    1.11 +  "(\<not> False) = True" by (rule HOL.simp_thms)
    1.12 +
    1.13 +lemma [code]:
    1.14 +  fixes x shows "(True \<and> True) = True"
    1.15 +  and "(False \<and> x) = False"
    1.16 +  and "(x \<and> False) = False" by simp_all
    1.17 +
    1.18 +lemma [code]:
    1.19 +  fixes x shows "(False \<or> False) = False"
    1.20 +  and "(True \<or> x) = True"
    1.21 +  and "(x \<or> True) = True" by simp_all
    1.22 +
    1.23 +declare
    1.24 +  if_True [code]
    1.25 +  if_False [code]
    1.26 +
    1.27 +lemma [code]:
    1.28 +  "fst (x, y) = x" by simp
    1.29 +
    1.30 +lemma [code]:
    1.31 +  "snd (x, y) = y" by simp
    1.32 +
    1.33 +code_generate True False Not "op &" "op |" If
    1.34 +
    1.35 +code_syntax_tyco bool
    1.36 +  ml (target_atom "bool")
    1.37 +  haskell (target_atom "Bool")
    1.38 +
    1.39  code_syntax_const
    1.40    True
    1.41      ml (target_atom "true")
    1.42 @@ -229,20 +261,33 @@
    1.43    False
    1.44      ml (target_atom "false")
    1.45      haskell (target_atom "False")
    1.46 +  Not
    1.47 +    ml (target_atom "not")
    1.48 +    haskell (target_atom "not")
    1.49 +  "op &"
    1.50 +    ml (infixl 1 "andalso")
    1.51 +    haskell (infixl 3 "&&")
    1.52 +  "op |"
    1.53 +    ml (infixl 0 "orelse")
    1.54 +    haskell (infixl 2 "||")
    1.55 +  If
    1.56 +    ml (target_atom "(if __/ then __/ else __)")
    1.57 +    haskell (target_atom "(if __/ then __/ else __)")
    1.58 +
    1.59 +code_generate Pair
    1.60 +
    1.61 +code_syntax_tyco
    1.62 +  *
    1.63 +    ml (infix 2 "*")
    1.64 +    haskell (target_atom "(__,/ __)")
    1.65  
    1.66  code_syntax_const
    1.67    Pair
    1.68      ml (target_atom "(__,/ __)")
    1.69      haskell (target_atom "(__,/ __)")
    1.70  
    1.71 -lemma [code]:
    1.72 -  "fst (x, y) = x" by simp
    1.73 -
    1.74 -lemma [code]:
    1.75 -  "snd (x, y) = y" by simp
    1.76 -
    1.77  code_syntax_const
    1.78 -  1 :: "nat"
    1.79 +  "1 :: nat"
    1.80      ml ("{*Suc 0*}")
    1.81      haskell ("{*Suc 0*}")
    1.82