--- a/src/HOL/Datatype.thy Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/Datatype.thy Sat Feb 25 15:19:47 2006 +0100
@@ -222,6 +222,38 @@
subsubsection {* Codegenerator setup *}
+lemma [code]:
+ "(\<not> True) = False" by (rule HOL.simp_thms)
+
+lemma [code]:
+ "(\<not> False) = True" by (rule HOL.simp_thms)
+
+lemma [code]:
+ fixes x shows "(True \<and> True) = True"
+ and "(False \<and> x) = False"
+ and "(x \<and> False) = False" by simp_all
+
+lemma [code]:
+ fixes x shows "(False \<or> False) = False"
+ and "(True \<or> x) = True"
+ and "(x \<or> True) = True" by simp_all
+
+declare
+ if_True [code]
+ if_False [code]
+
+lemma [code]:
+ "fst (x, y) = x" by simp
+
+lemma [code]:
+ "snd (x, y) = y" by simp
+
+code_generate True False Not "op &" "op |" If
+
+code_syntax_tyco bool
+ ml (target_atom "bool")
+ haskell (target_atom "Bool")
+
code_syntax_const
True
ml (target_atom "true")
@@ -229,20 +261,33 @@
False
ml (target_atom "false")
haskell (target_atom "False")
+ Not
+ ml (target_atom "not")
+ haskell (target_atom "not")
+ "op &"
+ ml (infixl 1 "andalso")
+ haskell (infixl 3 "&&")
+ "op |"
+ ml (infixl 0 "orelse")
+ haskell (infixl 2 "||")
+ If
+ ml (target_atom "(if __/ then __/ else __)")
+ haskell (target_atom "(if __/ then __/ else __)")
+
+code_generate Pair
+
+code_syntax_tyco
+ *
+ ml (infix 2 "*")
+ haskell (target_atom "(__,/ __)")
code_syntax_const
Pair
ml (target_atom "(__,/ __)")
haskell (target_atom "(__,/ __)")
-lemma [code]:
- "fst (x, y) = x" by simp
-
-lemma [code]:
- "snd (x, y) = y" by simp
-
code_syntax_const
- 1 :: "nat"
+ "1 :: nat"
ml ("{*Suc 0*}")
haskell ("{*Suc 0*}")
--- a/src/HOL/HOL.thy Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/HOL.thy Sat Feb 25 15:19:47 2006 +0100
@@ -1407,23 +1407,7 @@
uminus "HOL.uminus"
arbitrary "HOL.arbitrary"
-code_syntax_tyco bool
- ml (target_atom "bool")
- haskell (target_atom "Bool")
-
code_syntax_const
- Not
- ml (target_atom "not")
- haskell (target_atom "not")
- "op &"
- ml (infixl 1 "andalso")
- haskell (infixl 3 "&&")
- "op |"
- ml (infixl 0 "orelse")
- haskell (infixl 2 "||")
- If
- ml (target_atom "(if __/ then __/ else __)")
- haskell (target_atom "(if __/ then __/ else __)")
"op =" (* an intermediate solution for polymorphic equality *)
ml (infixl 6 "=")
haskell (infixl 4 "==")
--- a/src/HOL/Integ/IntDef.thy Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Sat Feb 25 15:19:47 2006 +0100
@@ -900,28 +900,28 @@
haskell (target_atom "Integer")
code_syntax_const
- 0 :: "int"
+ "0 :: int"
ml (target_atom "(0:IntInf.int)")
haskell (target_atom "0")
- 1 :: "int"
+ "1 :: int"
ml (target_atom "(1:IntInf.int)")
haskell (target_atom "1")
- "op +" :: "int \<Rightarrow> int \<Rightarrow> int"
+ "op + :: int \<Rightarrow> int \<Rightarrow> int"
ml (infixl 8 "+")
haskell (infixl 6 "+")
- "op *" :: "int \<Rightarrow> int \<Rightarrow> int"
+ "op * :: int \<Rightarrow> int \<Rightarrow> int"
ml (infixl 9 "*")
haskell (infixl 7 "*")
- uminus :: "int \<Rightarrow> int"
+ "uminus :: int \<Rightarrow> int"
ml (target_atom "~")
haskell (target_atom "negate")
- "op <" :: "int \<Rightarrow> int \<Rightarrow> bool"
+ "op < :: int \<Rightarrow> int \<Rightarrow> bool"
ml (infix 6 "<")
haskell (infix 4 "<")
- "op <=" :: "int \<Rightarrow> int \<Rightarrow> bool"
+ "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
ml (infix 6 "<=")
haskell (infix 4 "<=")
- "neg" :: "int \<Rightarrow> bool"
+ "neg :: int \<Rightarrow> bool"
ml ("_/ </ 0")
haskell ("_/ </ 0")
--- a/src/HOL/List.thy Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/List.thy Sat Feb 25 15:19:47 2006 +0100
@@ -2691,6 +2691,8 @@
"List.op @" "List.append"
"List.op mem" "List.member"
+code_generate Nil Cons
+
code_syntax_tyco
list
ml ("_ list")
--- a/src/HOL/Product_Type.thy Sat Feb 25 15:19:19 2006 +0100
+++ b/src/HOL/Product_Type.thy Sat Feb 25 15:19:47 2006 +0100
@@ -785,11 +785,6 @@
"fst" "Product_Type.fst"
"snd" "Product_Type.snd"
-code_syntax_tyco
- *
- ml (infix 2 "*")
- haskell (target_atom "(__,/ __)")
-
ML {*
fun strip_abs_split 0 t = ([], t)