constant HOL.eq now qualified
authorhaftmann
Tue Apr 22 08:33:16 2008 +0200 (2008-04-22)
changeset 267326ea9de67e576
parent 26731 48df747c8543
child 26733 47224a933c14
constant HOL.eq now qualified
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/Meson_Test.thy
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Apr 22 08:33:13 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Apr 22 08:33:16 2008 +0200
     1.3 @@ -610,7 +610,7 @@
     1.4    Obviously, polymorphic equality is implemented the Haskell
     1.5    way using a type class.  How is this achieved?  HOL introduces
     1.6    an explicit class @{text eq} with a corresponding operation
     1.7 -  @{const eq} such that @{thm eq [no_vars]}.
     1.8 +  @{const eq_class.eq} such that @{thm eq [no_vars]}.
     1.9    The preprocessing framework does the rest.
    1.10    For datatypes, instances of @{text eq} are implicitly derived
    1.11    when possible.  For other types, you may instantiate @{text eq}
    1.12 @@ -934,7 +934,7 @@
    1.13  instantiation bar :: eq
    1.14  begin
    1.15  
    1.16 -definition "eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
    1.17 +definition "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
    1.18  
    1.19  instance by default (simp add: eq_bar_def)
    1.20  
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Apr 22 08:33:13 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Apr 22 08:33:16 2008 +0200
     2.3 @@ -1322,7 +1322,7 @@
     2.4  \isakeyword{begin}\isanewline
     2.5  \isanewline
     2.6  \isacommand{definition}\isamarkupfalse%
     2.7 -\ {\isachardoublequoteopen}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
     2.8 +\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
     2.9  \isanewline
    2.10  \isacommand{instance}\isamarkupfalse%
    2.11  %
     3.1 --- a/src/HOL/HOL.thy	Tue Apr 22 08:33:13 2008 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Apr 22 08:33:16 2008 +0200
     3.3 @@ -1694,9 +1694,11 @@
     3.4  
     3.5  end
     3.6  
     3.7 +hide (open) const eq
     3.8 +hide const eq
     3.9 +
    3.10  setup {*
    3.11 -  Sign.hide_const true "HOL.eq"
    3.12 -  #> CodeUnit.add_const_alias @{thm equals_eq}
    3.13 +  CodeUnit.add_const_alias @{thm equals_eq}
    3.14  *}
    3.15  
    3.16  lemma [code func]:
     4.1 --- a/src/HOL/Int.thy	Tue Apr 22 08:33:13 2008 +0200
     4.2 +++ b/src/HOL/Int.thy	Tue Apr 22 08:33:16 2008 +0200
     4.3 @@ -1818,33 +1818,33 @@
     4.4  instantiation int :: eq
     4.5  begin
     4.6  
     4.7 -definition [code func del]: "eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
     4.8 +definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
     4.9  
    4.10  instance by default (simp add: eq_int_def)
    4.11  
    4.12  end
    4.13  
    4.14  lemma eq_number_of_int_code [code func]:
    4.15 -  "eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq k l"
    4.16 +  "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
    4.17    unfolding eq_int_def number_of_is_id ..
    4.18  
    4.19  lemma eq_int_code [code func]:
    4.20 -  "eq Int.Pls Int.Pls \<longleftrightarrow> True"
    4.21 -  "eq Int.Pls Int.Min \<longleftrightarrow> False"
    4.22 -  "eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq Int.Pls k2"
    4.23 -  "eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
    4.24 -  "eq Int.Min Int.Pls \<longleftrightarrow> False"
    4.25 -  "eq Int.Min Int.Min \<longleftrightarrow> True"
    4.26 -  "eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
    4.27 -  "eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq Int.Min k2"
    4.28 -  "eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq Int.Pls k1"
    4.29 -  "eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
    4.30 -  "eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
    4.31 -  "eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq Int.Min k1"
    4.32 -  "eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq k1 k2"
    4.33 -  "eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
    4.34 -  "eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
    4.35 -  "eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq k1 k2"
    4.36 +  "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
    4.37 +  "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
    4.38 +  "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
    4.39 +  "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
    4.40 +  "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
    4.41 +  "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
    4.42 +  "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
    4.43 +  "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
    4.44 +  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq Int.Pls k1"
    4.45 +  "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
    4.46 +  "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
    4.47 +  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq Int.Min k1"
    4.48 +  "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
    4.49 +  "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
    4.50 +  "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
    4.51 +  "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
    4.52    unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
    4.53      eq_number_of_int_code [symmetric, of Int.Min]
    4.54      eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
    4.55 @@ -2001,8 +2001,6 @@
    4.56  
    4.57  quickcheck_params [default_type = int]
    4.58  
    4.59 -(*setup continues in theory Presburger*)
    4.60 -
    4.61  hide (open) const Pls Min Bit0 Bit1 succ pred
    4.62  
    4.63  
     5.1 --- a/src/HOL/Library/Enum.thy	Tue Apr 22 08:33:13 2008 +0200
     5.2 +++ b/src/HOL/Library/Enum.thy	Tue Apr 22 08:33:16 2008 +0200
     5.3 @@ -42,7 +42,7 @@
     5.4  begin
     5.5  
     5.6  definition
     5.7 -  "eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
     5.8 +  "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
     5.9  
    5.10  instance by default
    5.11    (simp_all add: eq_fun_def enum_all expand_fun_eq)
     6.1 --- a/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:13 2008 +0200
     6.2 +++ b/src/HOL/Library/Nested_Environment.thy	Tue Apr 22 08:33:16 2008 +0200
     6.3 @@ -527,20 +527,20 @@
     6.4  
     6.5  lemma [code func, code func del]:
     6.6    fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
     6.7 -  shows "eq e1 e2 \<longleftrightarrow> eq e1 e2" ..
     6.8 +  shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
     6.9  
    6.10  lemma eq_env_code [code func]:
    6.11    fixes x y :: "'a\<Colon>eq"
    6.12      and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
    6.13 -  shows "eq (Env x f) (Env y g) \<longleftrightarrow>
    6.14 -  eq x y \<and> (\<forall>z\<in>UNIV. case f z
    6.15 +  shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
    6.16 +  eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
    6.17     of None \<Rightarrow> (case g z
    6.18          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    6.19      | Some a \<Rightarrow> (case g z
    6.20 -        of None \<Rightarrow> False | Some b \<Rightarrow> eq a b))" (is ?env)
    6.21 -    and "eq (Val a) (Val b) \<longleftrightarrow> eq a b"
    6.22 -    and "eq (Val a) (Env y g) \<longleftrightarrow> False"
    6.23 -    and "eq (Env x f) (Val b) \<longleftrightarrow> False"
    6.24 +        of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
    6.25 +    and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
    6.26 +    and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
    6.27 +    and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
    6.28  proof (unfold eq)
    6.29    have "f = g \<longleftrightarrow> (\<forall>z. case f z
    6.30     of None \<Rightarrow> (case g z
     7.1 --- a/src/HOL/Real/Rational.thy	Tue Apr 22 08:33:13 2008 +0200
     7.2 +++ b/src/HOL/Real/Rational.thy	Tue Apr 22 08:33:16 2008 +0200
     7.3 @@ -669,11 +669,11 @@
     7.4  instantiation rat :: eq
     7.5  begin
     7.6  
     7.7 -definition [code func del]: "eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
     7.8 +definition [code func del]: "eq_class.eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
     7.9  
    7.10  instance by default (simp add: eq_rat_def)
    7.11  
    7.12 -lemma rat_eq_code [code]: "eq (Rational x) (Rational y) \<longleftrightarrow> eq (normNum x) (normNum y)"
    7.13 +lemma rat_eq_code [code]: "eq_class.eq (Rational x) (Rational y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
    7.14    unfolding Rational_def INum_normNum_iff eq ..
    7.15  
    7.16  end
     8.1 --- a/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:13 2008 +0200
     8.2 +++ b/src/HOL/Real/RealDef.thy	Tue Apr 22 08:33:16 2008 +0200
     8.3 @@ -950,6 +950,13 @@
     8.4  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
     8.5  by simp
     8.6  
     8.7 +instance real :: lordered_ring
     8.8 +proof
     8.9 +  fix a::real
    8.10 +  show "abs a = sup a (-a)"
    8.11 +    by (auto simp add: real_abs_def sup_real_def)
    8.12 +qed
    8.13 +
    8.14  
    8.15  subsection {* Implementation of rational real numbers as pairs of integers *}
    8.16  
    8.17 @@ -981,11 +988,11 @@
    8.18  instantiation real :: eq
    8.19  begin
    8.20  
    8.21 -definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
    8.22 +definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x = y"
    8.23  
    8.24  instance by default (simp add: eq_real_def)
    8.25  
    8.26 -lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
    8.27 +lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq (normNum x) (normNum y)"
    8.28    unfolding Ratreal_def INum_normNum_iff eq ..
    8.29  
    8.30  end
    8.31 @@ -1024,13 +1031,6 @@
    8.32  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
    8.33    unfolding Ratreal_def by simp
    8.34  
    8.35 -instance real :: lordered_ring
    8.36 -proof
    8.37 -  fix a::real
    8.38 -  show "abs a = sup a (-a)"
    8.39 -    by (auto simp add: real_abs_def sup_real_def)
    8.40 -qed
    8.41 -
    8.42  text {* Setup for SML code generator *}
    8.43  
    8.44  types_code
     9.1 --- a/src/HOL/Set.thy	Tue Apr 22 08:33:13 2008 +0200
     9.2 +++ b/src/HOL/Set.thy	Tue Apr 22 08:33:16 2008 +0200
     9.3 @@ -2275,7 +2275,7 @@
     9.4  begin
     9.5  
     9.6  definition
     9.7 -  "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
     9.8 +  "eq_class.eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
     9.9  
    9.10  instance by default (auto simp add: eq_set_def)
    9.11  
    10.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Apr 22 08:33:13 2008 +0200
    10.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Apr 22 08:33:16 2008 +0200
    10.3 @@ -439,7 +439,7 @@
    10.4          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
    10.5            $ Free ("x", ty) $ Free ("y", ty);
    10.6          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
    10.7 -          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
    10.8 +          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
    10.9          val def' = Syntax.check_term lthy def;
   10.10          val ((_, (_, thm)), lthy') = Specification.definition
   10.11            (NONE, (("", []), def')) lthy;
   10.12 @@ -455,7 +455,7 @@
   10.13      fun add_eq_thms dtco thy =
   10.14        let
   10.15          val thy_ref = Theory.check_thy thy;
   10.16 -        val const = AxClass.param_of_inst thy (@{const_name eq}, dtco);
   10.17 +        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
   10.18          val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
   10.19        in
   10.20          Code.add_funcl (const, Susp.delay get_thms) thy
    11.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Apr 22 08:33:13 2008 +0200
    11.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Apr 22 08:33:16 2008 +0200
    11.3 @@ -131,7 +131,7 @@
    11.4          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
    11.5            $ Free ("x", ty) $ Free ("y", ty);
    11.6          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
    11.7 -          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
    11.8 +          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
    11.9          val def' = Syntax.check_term lthy def;
   11.10          val ((_, (_, thm)), lthy') = Specification.definition
   11.11            (NONE, (("", []), def')) lthy;
    12.1 --- a/src/HOL/ex/Meson_Test.thy	Tue Apr 22 08:33:13 2008 +0200
    12.2 +++ b/src/HOL/ex/Meson_Test.thy	Tue Apr 22 08:33:16 2008 +0200
    12.3 @@ -11,8 +11,7 @@
    12.4    below and constants declared in HOL!
    12.5  *}
    12.6  
    12.7 -hide const subset member quotient eq
    12.8 -hide const eq
    12.9 +hide const subset member quotient
   12.10  
   12.11  text {*
   12.12    Test data for the MESON proof procedure