# HG changeset patch
# User haftmann
# Date 1164187212 -3600
# Node ID a1937c51ed884889c4ac3d1b32a6813f469e206f
# Parent  03ca07d478be74d97cf46202cb1568f0c016f859
dropped eq const

diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -192,13 +192,8 @@
 
 subsubsection {* eq class *}
 
-class eq =
-  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
-  eq_def [normal post]: "eq \<equiv> (op =)"
-
-lemmas [symmetric, code inline, code func] = eq_def
+axclass eq \<subseteq> type
+  attach "op ="
 
 
 subsubsection {* bool type *}
@@ -206,36 +201,36 @@
 instance bool :: eq ..
 
 lemma [code func]:
-  "eq True p = p" unfolding eq_def by auto
+  "True = P \<longleftrightarrow> P" by simp
 
 lemma [code func]:
-  "eq False p = (\<not> p)" unfolding eq_def by auto
+  "False = P \<longleftrightarrow> \<not> P" by simp
 
 lemma [code func]:
-  "eq p True = p" unfolding eq_def by auto
+  "P = True \<longleftrightarrow> P" by simp
 
 lemma [code func]:
-  "eq p False = (\<not> p)" unfolding eq_def by auto
+  "P = False \<longleftrightarrow> \<not> P" by simp
 
 
 subsubsection {* Haskell *}
 
 code_class eq
-  (Haskell "Eq" where eq \<equiv> "(==)")
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
 
-code_const eq
+code_const "op ="
   (Haskell infixl 4 "==")
 
 code_instance bool :: eq
   (Haskell -)
 
-code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved Haskell
   Eq eq
 
 
-hide (open) const eq if_delayed
+hide (open) const if_delayed
 
 end
\ No newline at end of file
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Datatype.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -799,7 +799,7 @@
 code_instance option :: eq
   (Haskell -)
 
-code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -917,7 +917,7 @@
 code_instance int :: eq
   (Haskell -)
 
-code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (Haskell infixl 4 "==")
 
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Integ/Presburger.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -1090,12 +1090,12 @@
 text {* Code generator setup *}
 
 text {*
-  Presburger arithmetic is neccesary to prove some
+  Presburger arithmetic is necessary (at least convenient) to prove some
   of the following code lemmas on integer numerals.
 *}
 
 lemma eq_number_of [code func]:
-  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
+  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
   unfolding number_of_is_id ..
 
 lemma less_eq_number_of [code func]:
@@ -1103,57 +1103,55 @@
   unfolding number_of_is_id ..
 
 lemma eq_Pls_Pls:
-  "Code_Generator.eq Numeral.Pls Numeral.Pls"
-  unfolding eq_def ..
+  "Numeral.Pls = Numeral.Pls" ..
 
 lemma eq_Pls_Min:
-  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
-  unfolding eq_def Pls_def Min_def by auto
+  "Numeral.Pls \<noteq> Numeral.Min"
+  unfolding Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
-  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
-  unfolding eq_def Pls_def Bit_def bit.cases by auto
+  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
+  unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Pls_Bit1:
-  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
-  unfolding eq_def Pls_def Bit_def bit.cases by arith
+  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+  unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
-  unfolding eq_def Pls_def Min_def by auto
+  "Numeral.Min \<noteq> Numeral.Pls"
+  unfolding Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "Code_Generator.eq Numeral.Min Numeral.Min"
-  unfolding eq_def ..
+  "Numeral.Min = Numeral.Min" ..
 
 lemma eq_Min_Bit0:
-  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
-  unfolding eq_def Min_def Bit_def bit.cases by arith
+  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+  unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
-  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
-  unfolding eq_def Min_def Bit_def bit.cases by auto
+  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
+  unfolding Min_def Bit_def bit.cases by auto
 
 lemma eq_Bit0_Pls:
-  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
-  unfolding eq_def Pls_def Bit_def bit.cases by auto
+  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
+  unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Bit1_Pls:
-  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
-  unfolding eq_def Pls_def Bit_def bit.cases by arith
+  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
+  unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
-  unfolding eq_def Min_def Bit_def bit.cases by arith
+  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+  unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
-  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
-  unfolding eq_def Min_def Bit_def bit.cases by auto
+  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
+  unfolding Min_def Bit_def bit.cases by auto
 
 lemma eq_Bit_Bit:
-  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
-    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
-  unfolding eq_def Bit_def
+  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
+    v1 = v2 \<and> k1 = k2"
+  unfolding Bit_def
   apply (cases v1)
   apply (cases v2)
   apply auto
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -50,8 +50,8 @@
 qed
 
 lemma [code inline]:
-  "nat_case f g n = (if Code_Generator.eq n 0 then f else g (nat_of_int (int n - 1)))"
-  by (cases n) (simp_all add: eq_def nat_of_int_int)
+  "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
+  by (cases n) (simp_all add: nat_of_int_int)
 
 text {*
   Most standard arithmetic functions on natural numbers are implemented
@@ -97,8 +97,8 @@
   by simp
 lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
   by simp
-lemma [code func, code inline]: "Code_Generator.eq m n \<longleftrightarrow> Code_Generator.eq (int m) (int n)"
-  unfolding eq_def by simp
+lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
+  by simp
 lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
 proof (cases "k < 0")
   case True then show ?thesis by simp
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -121,7 +121,7 @@
   "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
-  "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
+  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
 
 code_const div_zero
   (SML "raise/ (Fail/ \"Division by zero\")")
@@ -136,7 +136,7 @@
   "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
   "inverse \<Colon> rat \<Rightarrow> rat"
   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
-   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
+  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
   (SML *)
 
 
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -32,10 +32,6 @@
   by blast
 
 lemma [code func]:
-  "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A"
-  unfolding eq_def subset_def by blast
-
-lemma [code func]:
   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   unfolding subset_def Set.subset_def ..
 
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Presburger.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -1090,12 +1090,12 @@
 text {* Code generator setup *}
 
 text {*
-  Presburger arithmetic is neccesary to prove some
+  Presburger arithmetic is necessary (at least convenient) to prove some
   of the following code lemmas on integer numerals.
 *}
 
 lemma eq_number_of [code func]:
-  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
+  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
   unfolding number_of_is_id ..
 
 lemma less_eq_number_of [code func]:
@@ -1103,57 +1103,55 @@
   unfolding number_of_is_id ..
 
 lemma eq_Pls_Pls:
-  "Code_Generator.eq Numeral.Pls Numeral.Pls"
-  unfolding eq_def ..
+  "Numeral.Pls = Numeral.Pls" ..
 
 lemma eq_Pls_Min:
-  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
-  unfolding eq_def Pls_def Min_def by auto
+  "Numeral.Pls \<noteq> Numeral.Min"
+  unfolding Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
-  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
-  unfolding eq_def Pls_def Bit_def bit.cases by auto
+  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
+  unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Pls_Bit1:
-  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
-  unfolding eq_def Pls_def Bit_def bit.cases by arith
+  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+  unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
-  unfolding eq_def Pls_def Min_def by auto
+  "Numeral.Min \<noteq> Numeral.Pls"
+  unfolding Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "Code_Generator.eq Numeral.Min Numeral.Min"
-  unfolding eq_def ..
+  "Numeral.Min = Numeral.Min" ..
 
 lemma eq_Min_Bit0:
-  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
-  unfolding eq_def Min_def Bit_def bit.cases by arith
+  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+  unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
-  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
-  unfolding eq_def Min_def Bit_def bit.cases by auto
+  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
+  unfolding Min_def Bit_def bit.cases by auto
 
 lemma eq_Bit0_Pls:
-  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
-  unfolding eq_def Pls_def Bit_def bit.cases by auto
+  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
+  unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Bit1_Pls:
-  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
-  unfolding eq_def Pls_def Bit_def bit.cases by arith
+  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
+  unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
-  unfolding eq_def Min_def Bit_def bit.cases by arith
+  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+  unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
-  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
-  unfolding eq_def Min_def Bit_def bit.cases by auto
+  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
+  unfolding Min_def Bit_def bit.cases by auto
 
 lemma eq_Bit_Bit:
-  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
-    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
-  unfolding eq_def Bit_def
+  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
+    v1 = v2 \<and> k1 = k2"
+  unfolding Bit_def
   apply (cases v1)
   apply (cases v2)
   apply auto
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Product_Type.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -776,7 +776,7 @@
 instance unit :: eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
 
 code_instance unit :: eq
   (Haskell -)
@@ -784,16 +784,15 @@
 instance * :: (eq, eq) eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
-  unfolding eq_def by auto
+  "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
 
 code_instance * :: eq
   (Haskell -)
 
-code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 types_code
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -197,20 +197,20 @@
 instance "+" :: (eq, eq) eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
-  unfolding eq_def Inl_eq ..
+  "(Inl x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inl y \<longleftrightarrow> x = y"
+  unfolding Inl_eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
-  unfolding eq_def Inr_eq ..
+  "(Inr x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inr y \<longleftrightarrow> x = y"
+  unfolding Inr_eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (Inl x) (Inr y) = False"
-  unfolding eq_def using Inl_not_Inr by auto
+  "Inl (x\<Colon>'a\<Colon>eq) = Inr (y\<Colon>'b\<Colon>eq) \<longleftrightarrow> False"
+  using Inl_not_Inr by auto
 
 lemma [code func]:
-  "Code_Generator.eq (Inr x) (Inl y) = False"
-  unfolding eq_def using Inr_not_Inl by auto
+  "Inr (x\<Colon>'b\<Colon>eq) = Inl (y\<Colon>'a\<Colon>eq) \<longleftrightarrow> False"
+  using Inr_not_Inl by auto
 
 ML
 {*
diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:12 2006 +0100
@@ -489,7 +489,6 @@
   | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
 
 local
-  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
   fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    of SOME _ => get_eq_datatype thy tyco
     | NONE => [TypecopyPackage.get_eq thy tyco];
@@ -498,7 +497,6 @@
     get_eq_thms thy tyco
     |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
     |> HOL.constrain_op_eq_thms thy
-    |> map (Tactic.rewrite_rule [eq_def_sym])
 end;
 
 type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
@@ -605,7 +603,7 @@
       let
         val thy_ref = Theory.self_ref thy;
         val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
-        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
+        val c = CodegenConsts.norm thy ("op =", [ty]);
         val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in
         CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy