# HG changeset patch
# User haftmann
# Date 1140877187 -3600
# Node ID 42ff710d432f49176641d0fb8fb0e16ebdc374fd
# Parent  f92919b141b2ead08e2d9763337d38ec266a5d3d
improved codegen bootstrap

diff -r f92919b141b2 -r 42ff710d432f src/HOL/Datatype.thy
--- 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*}")
 
diff -r f92919b141b2 -r 42ff710d432f src/HOL/HOL.thy
--- 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 "==")
diff -r f92919b141b2 -r 42ff710d432f src/HOL/Integ/IntDef.thy
--- 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")
 
diff -r f92919b141b2 -r 42ff710d432f src/HOL/List.thy
--- 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")
diff -r f92919b141b2 -r 42ff710d432f src/HOL/Product_Type.thy
--- 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)