explicit class "eq" for operational equality
authorhaftmann
Wed Apr 02 15:58:32 2008 +0200 (2008-04-02)
changeset 265136f306c8c2c54
parent 26512 682dfb674df3
child 26514 eff55c0a6d34
explicit class "eq" for operational equality
NEWS
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
src/HOL/HOL.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/SizeChange/Correctness.thy
src/HOL/SizeChange/Criterion.thy
src/HOL/SizeChange/Interpretation.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/Meson_Test.thy
src/HOL/ex/NormalForm.thy
     1.1 --- a/NEWS	Wed Apr 02 15:58:31 2008 +0200
     1.2 +++ b/NEWS	Wed Apr 02 15:58:32 2008 +0200
     1.3 @@ -57,6 +57,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Explicit class "eq" for executable equality.  INCOMPATIBILITY.
     1.8 +
     1.9  * Class finite no longer treats UNIV as class parameter.  Use class enum from
    1.10  theory Library/Enum instead to achieve a similar effect.  INCOMPATIBILITY.
    1.11  
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed Apr 02 15:58:31 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed Apr 02 15:58:32 2008 +0200
     2.3 @@ -1,3 +1,4 @@
     2.4 +
     2.5  (* $Id$ *)
     2.6  
     2.7  (*<*)
     2.8 @@ -607,21 +608,13 @@
     2.9  
    2.10  text {*
    2.11    Obviously, polymorphic equality is implemented the Haskell
    2.12 -  way using a type class.  How is this achieved?  By an
    2.13 -  almost trivial definition in the HOL setup:
    2.14 -*}
    2.15 -(*<*)
    2.16 -setup {* Sign.add_path "foo" *}
    2.17 -consts "op =" :: "'a"
    2.18 -(*>*)
    2.19 -class eq (attach "op =") = type
    2.20 -
    2.21 -text {*
    2.22 -  This merely introduces a class @{text eq} with corresponding
    2.23 -  operation @{text "op ="};
    2.24 -  the preprocessing framework does the rest.
    2.25 +  way using a type class.  How is this achieved?  HOL introduces
    2.26 +  an explicit class @{text eq} with a corresponding operation
    2.27 +  @{const eq} such that @{thm eq [no_vars]}.
    2.28 +  The preprocessing framework does the rest.
    2.29    For datatypes, instances of @{text eq} are implicitly derived
    2.30 -  when possible.
    2.31 +  when possible.  For other types, you may instantiate @{text eq}
    2.32 +  manually like any other type class.
    2.33  
    2.34    Though this @{text eq} class is designed to get rarely in
    2.35    the way, a subtlety
    2.36 @@ -629,11 +622,7 @@
    2.37    are dependent on operational equality.  For example, let
    2.38    us define a lexicographic ordering on tuples:
    2.39  *}
    2.40 -(*<*)
    2.41 -hide (open) "class" eq
    2.42 -hide (open) const "op ="
    2.43 -setup {* Sign.parent_path *}
    2.44 -(*>*)
    2.45 +
    2.46  instantiation * :: (ord, ord) ord
    2.47  begin
    2.48  
    2.49 @@ -942,7 +931,14 @@
    2.50  
    2.51  typedecl bar
    2.52  
    2.53 -instance bar :: eq ..
    2.54 +instantiation bar :: eq
    2.55 +begin
    2.56 +
    2.57 +definition "eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
    2.58 +
    2.59 +instance by default (simp add: eq_bar_def)
    2.60 +
    2.61 +end
    2.62  
    2.63  code_type %tt bar
    2.64    (Haskell "Integer")
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed Apr 02 15:58:31 2008 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed Apr 02 15:58:32 2008 +0200
     3.3 @@ -4,6 +4,7 @@
     3.4  %
     3.5  \isadelimtheory
     3.6  \isanewline
     3.7 +\isanewline
     3.8  %
     3.9  \endisadelimtheory
    3.10  %
    3.11 @@ -761,31 +762,13 @@
    3.12  %
    3.13  \begin{isamarkuptext}%
    3.14  Obviously, polymorphic equality is implemented the Haskell
    3.15 -  way using a type class.  How is this achieved?  By an
    3.16 -  almost trivial definition in the HOL setup:%
    3.17 -\end{isamarkuptext}%
    3.18 -\isamarkuptrue%
    3.19 -%
    3.20 -\isadelimML
    3.21 -%
    3.22 -\endisadelimML
    3.23 -%
    3.24 -\isatagML
    3.25 -%
    3.26 -\endisatagML
    3.27 -{\isafoldML}%
    3.28 -%
    3.29 -\isadelimML
    3.30 -%
    3.31 -\endisadelimML
    3.32 -\isacommand{class}\isamarkupfalse%
    3.33 -\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
    3.34 -\begin{isamarkuptext}%
    3.35 -This merely introduces a class \isa{eq} with corresponding
    3.36 -  operation \isa{op\ {\isacharequal}};
    3.37 -  the preprocessing framework does the rest.
    3.38 +  way using a type class.  How is this achieved?  HOL introduces
    3.39 +  an explicit class \isa{eq} with a corresponding operation
    3.40 +  \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}.
    3.41 +  The preprocessing framework does the rest.
    3.42    For datatypes, instances of \isa{eq} are implicitly derived
    3.43 -  when possible.
    3.44 +  when possible.  For other types, you may instantiate \isa{eq}
    3.45 +  manually like any other type class.
    3.46  
    3.47    Though this \isa{eq} class is designed to get rarely in
    3.48    the way, a subtlety
    3.49 @@ -794,19 +777,6 @@
    3.50    us define a lexicographic ordering on tuples:%
    3.51  \end{isamarkuptext}%
    3.52  \isamarkuptrue%
    3.53 -%
    3.54 -\isadelimML
    3.55 -%
    3.56 -\endisadelimML
    3.57 -%
    3.58 -\isatagML
    3.59 -%
    3.60 -\endisatagML
    3.61 -{\isafoldML}%
    3.62 -%
    3.63 -\isadelimML
    3.64 -%
    3.65 -\endisadelimML
    3.66  \isacommand{instantiation}\isamarkupfalse%
    3.67  \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
    3.68  \isakeyword{begin}\isanewline
    3.69 @@ -1347,15 +1317,22 @@
    3.70  \isacommand{typedecl}\isamarkupfalse%
    3.71  \ bar\isanewline
    3.72  \isanewline
    3.73 +\isacommand{instantiation}\isamarkupfalse%
    3.74 +\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
    3.75 +\isakeyword{begin}\isanewline
    3.76 +\isanewline
    3.77 +\isacommand{definition}\isamarkupfalse%
    3.78 +\ {\isachardoublequoteopen}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
    3.79 +\isanewline
    3.80  \isacommand{instance}\isamarkupfalse%
    3.81 -\ bar\ {\isacharcolon}{\isacharcolon}\ eq%
    3.82 +%
    3.83  \isadelimproof
    3.84  \ %
    3.85  \endisadelimproof
    3.86  %
    3.87  \isatagproof
    3.88 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
    3.89 -%
    3.90 +\isacommand{by}\isamarkupfalse%
    3.91 +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}%
    3.92  \endisatagproof
    3.93  {\isafoldproof}%
    3.94  %
    3.95 @@ -1363,6 +1340,9 @@
    3.96  %
    3.97  \endisadelimproof
    3.98  \isanewline
    3.99 +\isanewline
   3.100 +\isacommand{end}\isamarkupfalse%
   3.101 +\isanewline
   3.102  %
   3.103  \isadelimtt
   3.104  \isanewline
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Apr 02 15:58:31 2008 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Apr 02 15:58:32 2008 +0200
     4.3 @@ -1,8 +1,10 @@
     4.4  structure HOL = 
     4.5  struct
     4.6  
     4.7 -type 'a eq = {eqop : 'a -> 'a -> bool};
     4.8 -fun eqop (A_:'a eq) = #eqop A_;
     4.9 +type 'a eq = {eq : 'a -> 'a -> bool};
    4.10 +fun eq (A_:'a eq) = #eq A_;
    4.11 +
    4.12 +fun eqop A_ a = eq A_ a;
    4.13  
    4.14  end; (*struct HOL*)
    4.15  
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Wed Apr 02 15:58:31 2008 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Wed Apr 02 15:58:32 2008 +0200
     5.3 @@ -1,8 +1,8 @@
     5.4  structure HOL = 
     5.5  struct
     5.6  
     5.7 -type 'a eq = {eqop : 'a -> 'a -> bool};
     5.8 -fun eqop (A_:'a eq) = #eqop A_;
     5.9 +type 'a eq = {eq : 'a -> 'a -> bool};
    5.10 +fun eq (A_:'a eq) = #eq A_;
    5.11  
    5.12  type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
    5.13  fun less_eq (A_:'a ord) = #less_eq A_;
    5.14 @@ -14,7 +14,6 @@
    5.15  struct
    5.16  
    5.17  fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) =
    5.18 -  HOL.less A2_ x1 x2 orelse
    5.19 -    HOL.eqop A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
    5.20 +  HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
    5.21  
    5.22  end; (*struct Codegen*)
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Wed Apr 02 15:58:31 2008 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Wed Apr 02 15:58:32 2008 +0200
     6.3 @@ -3,10 +3,10 @@
     6.4  
     6.5  datatype nat = Suc of nat | Zero_nat;
     6.6  
     6.7 -fun eqop_nat Zero_nat Zero_nat = true
     6.8 -  | eqop_nat (Suc m) (Suc n) = eqop_nat m n
     6.9 -  | eqop_nat Zero_nat (Suc a) = false
    6.10 -  | eqop_nat (Suc a) Zero_nat = false;
    6.11 +fun eq_nat Zero_nat Zero_nat = true
    6.12 +  | eq_nat (Suc m) (Suc n) = eq_nat m n
    6.13 +  | eq_nat Zero_nat (Suc a) = false
    6.14 +  | eq_nat (Suc a) Zero_nat = false;
    6.15  
    6.16  end; (*struct Nat*)
    6.17  
    6.18 @@ -27,8 +27,8 @@
    6.19  
    6.20  datatype monotype = Mono of Nat.nat * monotype list;
    6.21  
    6.22 -fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    6.23 -  Nat.eqop_nat tyco1 tyco2 andalso
    6.24 -    List.list_all2 eqop_monotype typargs1 typargs2;
    6.25 +fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    6.26 +  Nat.eq_nat tyco1 tyco2 andalso
    6.27 +    List.list_all2 eq_monotype typargs1 typargs2;
    6.28  
    6.29  end; (*struct Codegen*)
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Wed Apr 02 15:58:31 2008 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Wed Apr 02 15:58:32 2008 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4  structure Product_Type = 
     7.5  struct
     7.6  
     7.7 -fun split c (a, b) = c a b;
     7.8 +fun split f (a, b) = f a b;
     7.9  
    7.10  end; (*struct Product_Type*)
    7.11  
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Wed Apr 02 15:58:31 2008 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Wed Apr 02 15:58:32 2008 +0200
     8.3 @@ -1,8 +1,10 @@
     8.4  structure HOL = 
     8.5  struct
     8.6  
     8.7 -type 'a eq = {eqop : 'a -> 'a -> bool};
     8.8 -fun eqop (A_:'a eq) = #eqop A_;
     8.9 +type 'a eq = {eq : 'a -> 'a -> bool};
    8.10 +fun eq (A_:'a eq) = #eq A_;
    8.11 +
    8.12 +fun eqop A_ a = eq A_ a;
    8.13  
    8.14  end; (*struct HOL*)
    8.15  
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Wed Apr 02 15:58:31 2008 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Wed Apr 02 15:58:32 2008 +0200
     9.3 @@ -1,13 +1,15 @@
     9.4  structure HOL = 
     9.5  struct
     9.6  
     9.7 -type 'a eq = {eqop : 'a -> 'a -> bool};
     9.8 -fun eqop (A_:'a eq) = #eqop A_;
     9.9 +type 'a eq = {eq : 'a -> 'a -> bool};
    9.10 +fun eq (A_:'a eq) = #eq A_;
    9.11  
    9.12  type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
    9.13  fun less_eq (A_:'a ord) = #less_eq A_;
    9.14  fun less (A_:'a ord) = #less A_;
    9.15  
    9.16 +fun eqop A_ a = eq A_ a;
    9.17 +
    9.18  end; (*struct HOL*)
    9.19  
    9.20  structure Orderings = 
    9.21 @@ -26,12 +28,12 @@
    9.22  
    9.23  datatype nat = Suc of nat | Zero_nat;
    9.24  
    9.25 -fun eqop_nat Zero_nat Zero_nat = true
    9.26 -  | eqop_nat (Suc m) (Suc n) = eqop_nat m n
    9.27 -  | eqop_nat Zero_nat (Suc a) = false
    9.28 -  | eqop_nat (Suc a) Zero_nat = false;
    9.29 +fun eq_nat Zero_nat Zero_nat = true
    9.30 +  | eq_nat (Suc m) (Suc n) = eq_nat m n
    9.31 +  | eq_nat Zero_nat (Suc a) = false
    9.32 +  | eq_nat (Suc a) Zero_nat = false;
    9.33  
    9.34 -val eq_nat = {eqop = eqop_nat} : nat HOL.eq;
    9.35 +val eq_nata = {eq = eq_nat} : nat HOL.eq;
    9.36  
    9.37  fun less_nat m (Suc n) = less_eq_nat m n
    9.38    | less_nat n Zero_nat = false
    9.39 @@ -68,13 +70,13 @@
    9.40               else Branch (Leaf (key, vala), it, Leaf (it, entry))));
    9.41  
    9.42  val example : (Nat.nat, (Nat.nat list)) searchtree =
    9.43 -  update (Nat.eq_nat, Nat.linorder_nat)
    9.44 +  update (Nat.eq_nata, Nat.linorder_nat)
    9.45      (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
    9.46        [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
    9.47 -    (update (Nat.eq_nat, Nat.linorder_nat)
    9.48 +    (update (Nat.eq_nata, Nat.linorder_nat)
    9.49        (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
    9.50          [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
    9.51 -      (update (Nat.eq_nat, Nat.linorder_nat)
    9.52 +      (update (Nat.eq_nata, Nat.linorder_nat)
    9.53          (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
    9.54          (Leaf (Nat.Suc Nat.Zero_nat, []))));
    9.55  
    10.1 --- a/src/HOL/HOL.thy	Wed Apr 02 15:58:31 2008 +0200
    10.2 +++ b/src/HOL/HOL.thy	Wed Apr 02 15:58:32 2008 +0200
    10.3 @@ -1644,24 +1644,6 @@
    10.4  
    10.5  setup "CodeName.setup #> CodeTarget.setup #> Nbe.setup"
    10.6  
    10.7 -class eq (attach "op =") = type
    10.8 -
    10.9 -lemma [code func]:
   10.10 -  shows "False \<and> x \<longleftrightarrow> False"
   10.11 -    and "True \<and> x \<longleftrightarrow> x"
   10.12 -    and "x \<and> False \<longleftrightarrow> False"
   10.13 -    and "x \<and> True \<longleftrightarrow> x" by simp_all
   10.14 -
   10.15 -lemma [code func]:
   10.16 -  shows "False \<or> x \<longleftrightarrow> x"
   10.17 -    and "True \<or> x \<longleftrightarrow> True"
   10.18 -    and "x \<or> False \<longleftrightarrow> x"
   10.19 -    and "x \<or> True \<longleftrightarrow> True" by simp_all
   10.20 -
   10.21 -lemma [code func]:
   10.22 -  shows "\<not> True \<longleftrightarrow> False"
   10.23 -    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
   10.24 -
   10.25  code_datatype Trueprop "prop"
   10.26  
   10.27  code_datatype "TYPE('a\<Colon>{})"
   10.28 @@ -1683,6 +1665,37 @@
   10.29    #> Code.add_undefined @{const_name undefined}
   10.30  *}
   10.31  
   10.32 +class eq = type +
   10.33 +  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   10.34 +  assumes eq: "eq x y \<longleftrightarrow> x = y "
   10.35 +begin
   10.36 +
   10.37 +lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
   10.38 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
   10.39 +
   10.40 +end
   10.41 +
   10.42 +setup {*
   10.43 +  CodeUnit.add_const_alias @{thm equals_eq}
   10.44 +*}
   10.45 +
   10.46 +lemma [code func]:
   10.47 +  shows "False \<and> x \<longleftrightarrow> False"
   10.48 +    and "True \<and> x \<longleftrightarrow> x"
   10.49 +    and "x \<and> False \<longleftrightarrow> False"
   10.50 +    and "x \<and> True \<longleftrightarrow> x" by simp_all
   10.51 +
   10.52 +lemma [code func]:
   10.53 +  shows "False \<or> x \<longleftrightarrow> x"
   10.54 +    and "True \<or> x \<longleftrightarrow> True"
   10.55 +    and "x \<or> False \<longleftrightarrow> x"
   10.56 +    and "x \<or> True \<longleftrightarrow> True" by simp_all
   10.57 +
   10.58 +lemma [code func]:
   10.59 +  shows "\<not> True \<longleftrightarrow> False"
   10.60 +    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
   10.61 +
   10.62 +
   10.63  
   10.64  subsection {* Legacy tactics and ML bindings *}
   10.65  
    11.1 --- a/src/HOL/Library/Enum.thy	Wed Apr 02 15:58:31 2008 +0200
    11.2 +++ b/src/HOL/Library/Enum.thy	Wed Apr 02 15:58:32 2008 +0200
    11.3 @@ -38,12 +38,16 @@
    11.4  
    11.5  subsection {* Equality and order on functions *}
    11.6  
    11.7 -instance "fun" :: (enum, eq) eq ..
    11.8 +instantiation "fun" :: (enum, eq) eq
    11.9 +begin
   11.10  
   11.11 -lemma eq_fun [code func]:
   11.12 -  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>eq"
   11.13 -  shows "f = g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
   11.14 -  by (simp add: enum_all expand_fun_eq)
   11.15 +definition
   11.16 +  "eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
   11.17 +
   11.18 +instance by default
   11.19 +  (simp_all add: eq_fun_def enum_all expand_fun_eq)
   11.20 +
   11.21 +end
   11.22  
   11.23  lemma order_fun [code func]:
   11.24    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    12.1 --- a/src/HOL/Library/Nested_Environment.thy	Wed Apr 02 15:58:31 2008 +0200
    12.2 +++ b/src/HOL/Library/Nested_Environment.thy	Wed Apr 02 15:58:32 2008 +0200
    12.3 @@ -527,21 +527,21 @@
    12.4  
    12.5  lemma [code func, code func del]:
    12.6    fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
    12.7 -  shows "e1 = e2 \<longleftrightarrow> e1 = e2" ..
    12.8 +  shows "eq e1 e2 \<longleftrightarrow> eq e1 e2" ..
    12.9  
   12.10  lemma eq_env_code [code func]:
   12.11    fixes x y :: "'a\<Colon>eq"
   12.12      and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
   12.13 -  shows "Env x f = Env y g \<longleftrightarrow>
   12.14 -  x = y \<and> (\<forall>z\<in>UNIV. case f z
   12.15 +  shows "eq (Env x f) (Env y g) \<longleftrightarrow>
   12.16 +  eq x y \<and> (\<forall>z\<in>UNIV. case f z
   12.17     of None \<Rightarrow> (case g z
   12.18          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   12.19      | Some a \<Rightarrow> (case g z
   12.20 -        of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is ?env)
   12.21 -    and "Val a = Val b \<longleftrightarrow> a = b"
   12.22 -    and "Val a = Env y g \<longleftrightarrow> False"
   12.23 -    and "Env x f = Val b \<longleftrightarrow> False"
   12.24 -proof -
   12.25 +        of None \<Rightarrow> False | Some b \<Rightarrow> eq a b))" (is ?env)
   12.26 +    and "eq (Val a) (Val b) \<longleftrightarrow> eq a b"
   12.27 +    and "eq (Val a) (Env y g) \<longleftrightarrow> False"
   12.28 +    and "eq (Env x f) (Val b) \<longleftrightarrow> False"
   12.29 +proof (unfold eq)
   12.30    have "f = g \<longleftrightarrow> (\<forall>z. case f z
   12.31     of None \<Rightarrow> (case g z
   12.32          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   12.33 @@ -559,7 +559,12 @@
   12.34        then show "f z = g z" by (auto split: option.splits)
   12.35      qed
   12.36    qed
   12.37 -  then show ?env by simp
   12.38 +  then show "Env x f = Env y g \<longleftrightarrow>
   12.39 +    x = y \<and> (\<forall>z\<in>UNIV. case f z
   12.40 +     of None \<Rightarrow> (case g z
   12.41 +          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   12.42 +      | Some a \<Rightarrow> (case g z
   12.43 +          of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
   12.44  qed simp_all
   12.45  
   12.46  end
    13.1 --- a/src/HOL/Real/Rational.thy	Wed Apr 02 15:58:31 2008 +0200
    13.2 +++ b/src/HOL/Real/Rational.thy	Wed Apr 02 15:58:32 2008 +0200
    13.3 @@ -666,10 +666,17 @@
    13.4    by (cases "l = 0")
    13.5      (auto simp add: Rational_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
    13.6  
    13.7 -instance rat :: eq ..
    13.8 +instantiation rat :: eq
    13.9 +begin
   13.10 +
   13.11 +definition [code func del]: "eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
   13.12  
   13.13 -lemma rat_eq_code [code]: "Rational x = Rational y \<longleftrightarrow> normNum x = normNum y"
   13.14 -  unfolding Rational_def INum_normNum_iff ..
   13.15 +instance by default (simp add: eq_rat_def)
   13.16 +
   13.17 +lemma rat_eq_code [code]: "eq (Rational x) (Rational y) \<longleftrightarrow> eq (normNum x) (normNum y)"
   13.18 +  unfolding Rational_def INum_normNum_iff eq ..
   13.19 +
   13.20 +end
   13.21  
   13.22  lemma rat_less_eq_code [code]: "Rational x \<le> Rational y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   13.23  proof -
    14.1 --- a/src/HOL/Real/RealDef.thy	Wed Apr 02 15:58:31 2008 +0200
    14.2 +++ b/src/HOL/Real/RealDef.thy	Wed Apr 02 15:58:32 2008 +0200
    14.3 @@ -978,10 +978,17 @@
    14.4    "1 = Ratreal 1\<^sub>N" by simp
    14.5  declare one_real_code [symmetric, code post]
    14.6  
    14.7 -instance real :: eq ..
    14.8 +instantiation real :: eq
    14.9 +begin
   14.10 +
   14.11 +definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
   14.12 +
   14.13 +instance by default (simp add: eq_real_def)
   14.14  
   14.15  lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
   14.16 -  unfolding Ratreal_def INum_normNum_iff ..
   14.17 +  unfolding Ratreal_def INum_normNum_iff eq ..
   14.18 +
   14.19 +end
   14.20  
   14.21  lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   14.22  proof -
    15.1 --- a/src/HOL/Set.thy	Wed Apr 02 15:58:31 2008 +0200
    15.2 +++ b/src/HOL/Set.thy	Wed Apr 02 15:58:32 2008 +0200
    15.3 @@ -2261,13 +2261,6 @@
    15.4    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
    15.5    by simp
    15.6  
    15.7 -instance set :: (eq) eq ..
    15.8 -
    15.9 -lemma eq_set_code [code func]:
   15.10 -  fixes A B :: "'a\<Colon>eq set"
   15.11 -  shows "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   15.12 -  by auto
   15.13 -
   15.14  lemma subset_eq_code [code func]:
   15.15    fixes A B :: "'a\<Colon>eq set"
   15.16    shows "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   15.17 @@ -2278,6 +2271,16 @@
   15.18    shows "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
   15.19    by auto
   15.20  
   15.21 +instantiation set :: (eq) eq
   15.22 +begin
   15.23 +
   15.24 +definition
   15.25 +  "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   15.26 +
   15.27 +instance by default (auto simp add: eq_set_def)
   15.28 +
   15.29 +end
   15.30 +
   15.31  
   15.32  subsubsection {* Derived operations *}
   15.33  
   15.34 @@ -2302,7 +2305,7 @@
   15.35    "Union A = UNION A (\<lambda>x. x)"
   15.36    by auto
   15.37  
   15.38 -code_reserved SML union inter (* Avoid clashes with ML infixes *)
   15.39 +code_reserved SML union inter -- {* avoid clashes with ML infixes *}
   15.40  
   15.41  subsection {* Basic ML bindings *}
   15.42  
    16.1 --- a/src/HOL/SizeChange/Correctness.thy	Wed Apr 02 15:58:31 2008 +0200
    16.2 +++ b/src/HOL/SizeChange/Correctness.thy	Wed Apr 02 15:58:32 2008 +0200
    16.3 @@ -637,7 +637,7 @@
    16.4  
    16.5  lemma desc_scgcomp:
    16.6    "dsc (G * H) m r =
    16.7 -  (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R")
    16.8 +  (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eqp G m n \<and> dsc H n r))" (is "?L = ?R")
    16.9  proof
   16.10    show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
   16.11  
    17.1 --- a/src/HOL/SizeChange/Criterion.thy	Wed Apr 02 15:58:31 2008 +0200
    17.2 +++ b/src/HOL/SizeChange/Criterion.thy	Wed Apr 02 15:58:32 2008 +0200
    17.3 @@ -44,7 +44,7 @@
    17.4  instance sedge :: finite
    17.5  proof
    17.6    show "finite (UNIV::sedge set)"
    17.7 -    by (simp add: sedge_UNIV)
    17.8 +  by (simp add: sedge_UNIV)
    17.9  qed
   17.10  
   17.11  
   17.12 @@ -62,7 +62,7 @@
   17.13    "dsc G i j \<equiv> has_edge G i LESS j"
   17.14  
   17.15  abbreviation (input)
   17.16 -  "eq G i j \<equiv> has_edge G i LEQ j"
   17.17 +  "eqp G i j \<equiv> has_edge G i LEQ j"
   17.18  
   17.19  abbreviation
   17.20    eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    18.1 --- a/src/HOL/SizeChange/Interpretation.thy	Wed Apr 02 15:58:31 2008 +0200
    18.2 +++ b/src/HOL/SizeChange/Interpretation.thy	Wed Apr 02 15:58:32 2008 +0200
    18.3 @@ -190,7 +190,7 @@
    18.4    where
    18.5    "approx G C C' M M'
    18.6    = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
    18.7 -  \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
    18.8 +  \<and>(eqp G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
    18.9  
   18.10  
   18.11  
   18.12 @@ -360,7 +360,7 @@
   18.13  	assume "n < i"
   18.14  	
   18.15  	with fr	have "eqlat ?p th i" by simp 
   18.16 -	hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2" 
   18.17 +	hence "dsc (Gs i) ?q1 ?q2 \<or> eqp (Gs i) ?q1 ?q2" 
   18.18        by simp
   18.19  	thus "?seq (Suc i) \<le> ?seq i"
   18.20  	proof
   18.21 @@ -376,7 +376,7 @@
   18.22  		apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
   18.23  		by (rule ird a)+
   18.24  	next
   18.25 -	  assume "eq (Gs i) ?q1 ?q2"
   18.26 +	  assume "eqp (Gs i) ?q1 ?q2"
   18.27  	  
   18.28  	  with approx
   18.29  	  have a:"decreq (cs i) (cs (Suc i)) 
    19.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Apr 02 15:58:31 2008 +0200
    19.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Apr 02 15:58:32 2008 +0200
    19.3 @@ -431,26 +431,44 @@
    19.4  
    19.5  fun add_datatypes_equality vs dtcos thy =
    19.6    let
    19.7 +    val vs' = (map o apsnd)
    19.8 +      (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
    19.9 +    fun add_def tyco lthy =
   19.10 +      let
   19.11 +        val ty = Type (tyco, map TFree vs');
   19.12 +        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   19.13 +          $ Free ("x", ty) $ Free ("y", ty);
   19.14 +        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   19.15 +          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
   19.16 +        val def' = Syntax.check_term lthy def;
   19.17 +        val ((_, (_, thm)), lthy') = Specification.definition
   19.18 +          (NONE, (("", []), def')) lthy;
   19.19 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   19.20 +        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   19.21 +      in (thm', lthy') end;
   19.22 +    fun tac thms = Class.intro_classes_tac []
   19.23 +      THEN ALLGOALS (ProofContext.fact_tac thms);
   19.24      fun get_eq' thy dtco = get_eq thy dtco
   19.25        |> map (CodeUnit.constrain_thm [HOLogic.class_eq])
   19.26 -      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy);
   19.27 +      |> map Simpdata.mk_eq
   19.28 +      |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
   19.29      fun add_eq_thms dtco thy =
   19.30        let
   19.31          val thy_ref = Theory.check_thy thy;
   19.32 -        val const = AxClass.param_of_inst thy ("op =", dtco);
   19.33 +        val const = AxClass.param_of_inst thy (@{const_name eq}, dtco);
   19.34          val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
   19.35        in
   19.36          Code.add_funcl (const, Susp.delay get_thms) thy
   19.37        end;
   19.38 -    val vs' = (map o apsnd)
   19.39 -      (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
   19.40    in
   19.41      thy
   19.42      |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
   19.43 -    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   19.44 -    |> LocalTheory.exit
   19.45 -    |> ProofContext.theory_of
   19.46 -    |> fold add_eq_thms dtcos
   19.47 +    |> fold_map add_def dtcos
   19.48 +    |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
   19.49 +    #> LocalTheory.exit
   19.50 +    #> ProofContext.theory_of
   19.51 +    #> fold Code.del_func thms
   19.52 +    #> fold add_eq_thms dtcos)
   19.53    end;
   19.54  
   19.55  
    20.1 --- a/src/HOL/Tools/typecopy_package.ML	Wed Apr 02 15:58:31 2008 +0200
    20.2 +++ b/src/HOL/Tools/typecopy_package.ML	Wed Apr 02 15:58:32 2008 +0200
    20.3 @@ -125,15 +125,39 @@
    20.4      val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
    20.5      val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
    20.6      val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
    20.7 +    fun add_def tyco lthy =
    20.8 +      let
    20.9 +        val ty = Type (tyco, map TFree vs');
   20.10 +        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   20.11 +          $ Free ("x", ty) $ Free ("y", ty);
   20.12 +        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   20.13 +          (mk_side @{const_name eq}, mk_side @{const_name "op ="}));
   20.14 +        val def' = Syntax.check_term lthy def;
   20.15 +        val ((_, (_, thm)), lthy') = Specification.definition
   20.16 +          (NONE, (("", []), def')) lthy;
   20.17 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   20.18 +        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   20.19 +      in (thm', lthy') end;
   20.20 +    fun tac thms = Class.intro_classes_tac []
   20.21 +      THEN ALLGOALS (ProofContext.fact_tac thms);
   20.22 +    fun add_eq_thm thy = 
   20.23 +      let
   20.24 +        val eq = inject
   20.25 +          |> CodeUnit.constrain_thm [HOLogic.class_eq]
   20.26 +          |> Simpdata.mk_eq
   20.27 +          |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
   20.28 +      in Code.add_func eq thy end;
   20.29    in
   20.30      thy
   20.31      |> Code.add_datatype [(constr, ty)]
   20.32      |> Code.add_func proj_def
   20.33      |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
   20.34 -    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   20.35 -    |> LocalTheory.exit
   20.36 -    |> ProofContext.theory_of
   20.37 -    |> Code.add_func (CodeUnit.constrain_thm [HOLogic.class_eq] inject)
   20.38 +    |> add_def tyco
   20.39 +    |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
   20.40 +    #> LocalTheory.exit
   20.41 +    #> ProofContext.theory_of
   20.42 +    #> Code.del_func thm
   20.43 +    #> add_eq_thm)
   20.44    end;
   20.45  
   20.46  val setup =
    21.1 --- a/src/HOL/ex/Meson_Test.thy	Wed Apr 02 15:58:31 2008 +0200
    21.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed Apr 02 15:58:32 2008 +0200
    21.3 @@ -11,8 +11,8 @@
    21.4    below and constants declared in HOL!
    21.5  *}
    21.6  
    21.7 -hide const subset member quotient 
    21.8 -
    21.9 +hide const subset member quotient eq
   21.10 +hide const eq
   21.11  
   21.12  text {*
   21.13    Test data for the MESON proof procedure
    22.1 --- a/src/HOL/ex/NormalForm.thy	Wed Apr 02 15:58:31 2008 +0200
    22.2 +++ b/src/HOL/ex/NormalForm.thy	Wed Apr 02 15:58:32 2008 +0200
    22.3 @@ -8,6 +8,8 @@
    22.4  imports Main "~~/src/HOL/Real/Rational"
    22.5  begin
    22.6  
    22.7 +declare equals_eq [symmetric, code post]
    22.8 +
    22.9  lemma "True" by normalization
   22.10  lemma "p \<longrightarrow> True" by normalization
   22.11  declare disj_assoc [code func]
   22.12 @@ -58,19 +60,19 @@
   22.13  lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
   22.14  
   22.15  lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
   22.16 -lemma "split (%x y. x) (a, b) = a" by normalization rule
   22.17 +lemma "split (%(x\<Colon>'a\<Colon>eq) y. x) (a, b) = a" by normalization rule
   22.18  lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
   22.19  
   22.20  lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
   22.21  
   22.22  lemma "[] @ [] = []" by normalization
   22.23 -lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization rule+
   22.24 -lemma "[a, b, c] @ xs = a # b # c # xs" by normalization rule+
   22.25 -lemma "[] @ xs = xs" by normalization rule
   22.26 +lemma "map f [x,y,z::'x] = [f x \<Colon> 'a\<Colon>eq, f y, f z]" by normalization rule+
   22.27 +lemma "[a \<Colon> 'a\<Colon>eq, b, c] @ xs = a # b # c # xs" by normalization rule+
   22.28 +lemma "[] @ xs = (xs \<Colon> 'a\<Colon>eq list)" by normalization rule
   22.29  lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization rule+
   22.30  lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
   22.31 -lemma "rev [a, b, c] = [c, b, a]" by normalization rule+
   22.32 -normal_form "rev (a#b#cs) = rev cs @ [b, a]"
   22.33 +lemma "rev [a, b, c] = [c \<Colon> 'a\<Colon>eq, b, a]" by normalization rule+
   22.34 +normal_form "rev (a#b#cs) = rev cs @ [b, a \<Colon> 'a\<Colon>eq]"
   22.35  normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
   22.36  normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
   22.37  normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
   22.38 @@ -78,19 +80,19 @@
   22.39    by normalization
   22.40  normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
   22.41  normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
   22.42 -lemma "let x = y in [x, x] = [y, y]" by normalization rule+
   22.43 -lemma "Let y (%x. [x,x]) = [y, y]" by normalization rule+
   22.44 +lemma "let x = y in [x, x] = [y \<Colon> 'a\<Colon>eq, y]" by normalization rule+
   22.45 +lemma "Let y (%x. [x,x]) = [y \<Colon> 'a\<Colon>eq, y]" by normalization rule+
   22.46  normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
   22.47  lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization rule+
   22.48  normal_form "filter (%x. x) ([True,False,x]@xs)"
   22.49  normal_form "filter Not ([True,False,x]@xs)"
   22.50  
   22.51 -lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]" by normalization rule+
   22.52 -lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization rule+
   22.53 +lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c \<Colon> 'a\<Colon>eq]" by normalization rule+
   22.54 +lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f \<Colon> 'a\<Colon>eq]" by normalization rule+
   22.55  lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
   22.56  
   22.57 -lemma "last [a, b, c] = c" by normalization rule
   22.58 -lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
   22.59 +lemma "last [a, b, c \<Colon> 'a\<Colon>eq] = c" by normalization rule
   22.60 +lemma "last ([a, b, c \<Colon> 'a\<Colon>eq] @ xs) = (if null xs then c else last xs)"
   22.61    by normalization rule
   22.62  
   22.63  lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization rule
   22.64 @@ -111,10 +113,10 @@
   22.65  lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
   22.66  normal_form "Suc 0 \<in> set ms"
   22.67  
   22.68 -lemma "f = f" by normalization rule+
   22.69 -lemma "f x = f x" by normalization rule+
   22.70 -lemma "(f o g) x = f (g x)" by normalization rule+
   22.71 -lemma "(f o id) x = f x" by normalization rule+
   22.72 +lemma "f = (f \<Colon> 'a\<Colon>eq)" by normalization rule+
   22.73 +lemma "f x = (f x \<Colon> 'a\<Colon>eq)" by normalization rule+
   22.74 +lemma "(f o g) x = (f (g x) \<Colon> 'a\<Colon>eq)" by normalization rule+
   22.75 +lemma "(f o id) x = (f x \<Colon> 'a\<Colon>eq)" by normalization rule+
   22.76  normal_form "(\<lambda>x. x)"
   22.77  
   22.78  (* Church numerals: *)