--- 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)
--- 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%
%
--- 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]:
--- 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
--- 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)
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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;
--- 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