added operational equality

--- a/src/HOL/Datatype.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Datatype.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -9,6 +9,8 @@
 imports Datatype_Universe
 begin
 
+setup "DatatypeCodegen.setup2"
+
 subsection {* Representing primitive types *}
 
 rep_datatype bool
@@ -297,4 +299,10 @@
   (SML target_atom "NONE" and target_atom "SOME")
   (Haskell target_atom "Nothing" and target_atom "Just")
 
+code_instance option :: eq
+  (Haskell -)
+
+code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
 end

--- a/src/HOL/List.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/List.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -2282,7 +2282,8 @@
 
 text{* Defaults for generating efficient code for some standard functions. *}
 
-lemmas in_set_code[code unfold] = mem_iff[symmetric, THEN eq_reflection]
+lemmas in_set_code [code unfold] =
+  mem_iff [symmetric, THEN eq_reflection]
 
 lemma rev_code[code unfold]: "rev xs == itrev xs []"
 by simp
@@ -2760,6 +2761,15 @@
   (SML target_atom "(__,/ __)")
   (Haskell target_atom "(__,/ __)")
 
+code_instance list :: eq and char :: eq
+  (Haskell - and -)
+
+code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "OperationalEquality.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
 setup {*
 let
 

--- a/src/HOL/Nat.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Nat.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -1041,10 +1041,25 @@
   apply (fastsimp dest: mult_less_mono2)
   done
 
+
 subsection {* Code generator setup *}
 
 lemma one_is_suc_zero [code inline]:
   "1 = Suc 0"
   by simp
 
+instance nat :: eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (0\<Colon>nat) 0 = True" unfolding eq_def by auto
+
+lemma [code func]:
+  "OperationalEquality.eq (Suc n) (Suc m) = OperationalEquality.eq n m" unfolding eq_def by auto
+
+lemma [code func]:
+  "OperationalEquality.eq (Suc n) 0 = False" unfolding eq_def by auto
+
+lemma [code func]:
+  "OperationalEquality.eq 0 (Suc m) = False" unfolding eq_def by auto
+
 end

--- a/src/HOL/Orderings.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Orderings.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -8,18 +8,16 @@
 header {* Type classes for $\le$ *}
 
 theory Orderings
-imports Lattice_Locales
+imports OperationalEquality Lattice_Locales
 uses ("antisym_setup.ML")
 begin
 
 subsection {* Order signatures and orders *}
 
-axclass
-  ord < type
-
-consts
-  less  :: "['a::ord, 'a] => bool"
-  less_eq  :: "['a::ord, 'a] => bool"
+class ord = eq +
+  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 const_syntax
   less  ("op <")

--- a/src/HOL/Product_Type.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Product_Type.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -15,7 +15,7 @@
 
 typedef unit = "{True}"
 proof
-  show "True : ?unit" by blast
+  show "True : ?unit" ..
 qed
 
 constdefs
@@ -761,6 +761,29 @@
 
 subsection {* Code generator setup *}
 
+instance unit :: eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+
+code_instance unit :: eq
+  (Haskell -)
+
+instance * :: (eq, eq) eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
+  unfolding eq_def by auto
+
+code_instance * :: eq
+  (Haskell -)
+
+code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
 types_code
   "*"     ("(_ */ _)")
 attach (term_of) {*

--- a/src/HOL/Sum_Type.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Sum_Type.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -191,6 +191,27 @@
 lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"
 by blast
 
+
+subsection {* Code generator setup *}
+
+instance "+" :: (eq, eq) eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (Inl x) (Inl y) = OperationalEquality.eq x y"
+  unfolding eq_def Inl_eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (Inr x) (Inr y) = OperationalEquality.eq x y"
+  unfolding eq_def Inr_eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (Inl x) (Inr y) = False"
+  unfolding eq_def using Inl_not_Inr by auto
+
+lemma [code func]:
+  "OperationalEquality.eq (Inr x) (Inl y) = False"
+  unfolding eq_def using Inr_not_Inl by auto
+
 ML
 {*
 val Inl_RepI = thm "Inl_RepI";