# HG changeset patch
# User haftmann
# Date 1208845996 -7200
# Node ID 6ea9de67e57659eae6e54cd316706d23cb5dddf0
# Parent  48df747c8543ee54310fa5981de5de11f436af3d
constant HOL.eq now qualified

diff -r 48df747c8543 -r 6ea9de67e576 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -610,7 +610,7 @@
   Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces
   an explicit class @{text eq} with a corresponding operation
-  @{const eq} such that @{thm eq [no_vars]}.
+  @{const eq_class.eq} such that @{thm eq [no_vars]}.
   The preprocessing framework does the rest.
   For datatypes, instances of @{text eq} are implicitly derived
   when possible.  For other types, you may instantiate @{text eq}
@@ -934,7 +934,7 @@
 instantiation bar :: eq
 begin
 
-definition "eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
+definition "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
 
 instance by default (simp add: eq_bar_def)
 
diff -r 48df747c8543 -r 6ea9de67e576 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Apr 22 08:33:13 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Apr 22 08:33:16 2008 +0200
@@ -1322,7 +1322,7 @@
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ {\isachardoublequoteopen}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
 %
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -1694,9 +1694,11 @@
 
 end
 
+hide (open) const eq
+hide const eq
+
 setup {*
-  Sign.hide_const true "HOL.eq"
-  #> CodeUnit.add_const_alias @{thm equals_eq}
+  CodeUnit.add_const_alias @{thm equals_eq}
 *}
 
 lemma [code func]:
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Int.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -1818,33 +1818,33 @@
 instantiation int :: eq
 begin
 
-definition [code func del]: "eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
 
 instance by default (simp add: eq_int_def)
 
 end
 
 lemma eq_number_of_int_code [code func]:
-  "eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq k l"
+  "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
   unfolding eq_int_def number_of_is_id ..
 
 lemma eq_int_code [code func]:
-  "eq Int.Pls Int.Pls \<longleftrightarrow> True"
-  "eq Int.Pls Int.Min \<longleftrightarrow> False"
-  "eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq Int.Pls k2"
-  "eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
-  "eq Int.Min Int.Pls \<longleftrightarrow> False"
-  "eq Int.Min Int.Min \<longleftrightarrow> True"
-  "eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
-  "eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq Int.Min k2"
-  "eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq Int.Pls k1"
-  "eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
-  "eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
-  "eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq Int.Min k1"
-  "eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq k1 k2"
-  "eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
-  "eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
-  "eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq k1 k2"
+  "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
+  "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
+  "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
+  "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
+  "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
+  "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
+  "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
+  "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
+  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq Int.Pls k1"
+  "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
+  "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
+  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq Int.Min k1"
+  "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
+  "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
+  "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
+  "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
   unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
     eq_number_of_int_code [symmetric, of Int.Min]
     eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
@@ -2001,8 +2001,6 @@
 
 quickcheck_params [default_type = int]
 
-(*setup continues in theory Presburger*)
-
 hide (open) const Pls Min Bit0 Bit1 succ pred
 
 
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -42,7 +42,7 @@
 begin
 
 definition
-  "eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
+  "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
 
 instance by default
   (simp_all add: eq_fun_def enum_all expand_fun_eq)
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -527,20 +527,20 @@
 
 lemma [code func, code func del]:
   fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
-  shows "eq e1 e2 \<longleftrightarrow> eq e1 e2" ..
+  shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
 
 lemma eq_env_code [code func]:
   fixes x y :: "'a\<Colon>eq"
     and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
-  shows "eq (Env x f) (Env y g) \<longleftrightarrow>
-  eq x y \<and> (\<forall>z\<in>UNIV. case f z
+  shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
+  eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
    of None \<Rightarrow> (case g z
         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
     | Some a \<Rightarrow> (case g z
-        of None \<Rightarrow> False | Some b \<Rightarrow> eq a b))" (is ?env)
-    and "eq (Val a) (Val b) \<longleftrightarrow> eq a b"
-    and "eq (Val a) (Env y g) \<longleftrightarrow> False"
-    and "eq (Env x f) (Val b) \<longleftrightarrow> False"
+        of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
+    and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
+    and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
+    and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
 proof (unfold eq)
   have "f = g \<longleftrightarrow> (\<forall>z. case f z
    of None \<Rightarrow> (case g z
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -669,11 +669,11 @@
 instantiation rat :: eq
 begin
 
-definition [code func del]: "eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
+definition [code func del]: "eq_class.eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
 
 instance by default (simp add: eq_rat_def)
 
-lemma rat_eq_code [code]: "eq (Rational x) (Rational y) \<longleftrightarrow> eq (normNum x) (normNum y)"
+lemma rat_eq_code [code]: "eq_class.eq (Rational x) (Rational y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
   unfolding Rational_def INum_normNum_iff eq ..
 
 end
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -950,6 +950,13 @@
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
+instance real :: lordered_ring
+proof
+  fix a::real
+  show "abs a = sup a (-a)"
+    by (auto simp add: real_abs_def sup_real_def)
+qed
+
 
 subsection {* Implementation of rational real numbers as pairs of integers *}
 
@@ -981,11 +988,11 @@
 instantiation real :: eq
 begin
 
-definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
+definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x = y"
 
 instance by default (simp add: eq_real_def)
 
-lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
+lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
   unfolding Ratreal_def INum_normNum_iff eq ..
 
 end
@@ -1024,13 +1031,6 @@
 lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
   unfolding Ratreal_def by simp
 
-instance real :: lordered_ring
-proof
-  fix a::real
-  show "abs a = sup a (-a)"
-    by (auto simp add: real_abs_def sup_real_def)
-qed
-
 text {* Setup for SML code generator *}
 
 types_code
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Set.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -2275,7 +2275,7 @@
 begin
 
 definition
-  "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+  "eq_class.eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
 
 instance by default (auto simp add: eq_set_def)
 
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Apr 22 08:33:16 2008 +0200
@@ -439,7 +439,7 @@
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
+          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (("", []), def')) lthy;
@@ -455,7 +455,7 @@
     fun add_eq_thms dtco thy =
       let
         val thy_ref = Theory.check_thy thy;
-        val const = AxClass.param_of_inst thy (@{const_name eq}, dtco);
+        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
         val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
       in
         Code.add_funcl (const, Susp.delay get_thms) thy
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Tue Apr 22 08:33:16 2008 +0200
@@ -131,7 +131,7 @@
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
+          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (("", []), def')) lthy;
diff -r 48df747c8543 -r 6ea9de67e576 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -11,8 +11,7 @@
   below and constants declared in HOL!
 *}
 
-hide const subset member quotient eq
-hide const eq
+hide const subset member quotient
 
 text {*
   Test data for the MESON proof procedure