--- a/NEWS Wed Apr 02 15:58:31 2008 +0200
+++ b/NEWS Wed Apr 02 15:58:32 2008 +0200
@@ -57,6 +57,8 @@
*** HOL ***
+* Explicit class "eq" for executable equality. INCOMPATIBILITY.
+
* Class finite no longer treats UNIV as class parameter. Use class enum from
theory Library/Enum instead to achieve a similar effect. INCOMPATIBILITY.
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Apr 02 15:58:32 2008 +0200
@@ -1,3 +1,4 @@
+
(* $Id$ *)
(*<*)
@@ -607,21 +608,13 @@
text {*
Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? By an
- almost trivial definition in the HOL setup:
-*}
-(*<*)
-setup {* Sign.add_path "foo" *}
-consts "op =" :: "'a"
-(*>*)
-class eq (attach "op =") = type
-
-text {*
- This merely introduces a class @{text eq} with corresponding
- operation @{text "op ="};
- the preprocessing framework does the rest.
+ 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]}.
+ The preprocessing framework does the rest.
For datatypes, instances of @{text eq} are implicitly derived
- when possible.
+ when possible. For other types, you may instantiate @{text eq}
+ manually like any other type class.
Though this @{text eq} class is designed to get rarely in
the way, a subtlety
@@ -629,11 +622,7 @@
are dependent on operational equality. For example, let
us define a lexicographic ordering on tuples:
*}
-(*<*)
-hide (open) "class" eq
-hide (open) const "op ="
-setup {* Sign.parent_path *}
-(*>*)
+
instantiation * :: (ord, ord) ord
begin
@@ -942,7 +931,14 @@
typedecl bar
-instance bar :: eq ..
+instantiation bar :: eq
+begin
+
+definition "eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
+
+instance by default (simp add: eq_bar_def)
+
+end
code_type %tt bar
(Haskell "Integer")
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Apr 02 15:58:32 2008 +0200
@@ -4,6 +4,7 @@
%
\isadelimtheory
\isanewline
+\isanewline
%
\endisadelimtheory
%
@@ -761,31 +762,13 @@
%
\begin{isamarkuptext}%
Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? By an
- almost trivial definition in the HOL setup:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isacommand{class}\isamarkupfalse%
-\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
-\begin{isamarkuptext}%
-This merely introduces a class \isa{eq} with corresponding
- operation \isa{op\ {\isacharequal}};
- the preprocessing framework does the rest.
+ way using a type class. How is this achieved? HOL introduces
+ an explicit class \isa{eq} with a corresponding operation
+ \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}.
+ The preprocessing framework does the rest.
For datatypes, instances of \isa{eq} are implicitly derived
- when possible.
+ when possible. For other types, you may instantiate \isa{eq}
+ manually like any other type class.
Though this \isa{eq} class is designed to get rarely in
the way, a subtlety
@@ -794,19 +777,6 @@
us define a lexicographic ordering on tuples:%
\end{isamarkuptext}%
\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
\isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
\isakeyword{begin}\isanewline
@@ -1347,15 +1317,22 @@
\isacommand{typedecl}\isamarkupfalse%
\ bar\isanewline
\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isachardoublequoteopen}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
+\isanewline
\isacommand{instance}\isamarkupfalse%
-\ bar\ {\isacharcolon}{\isacharcolon}\ eq%
+%
\isadelimproof
\ %
\endisadelimproof
%
\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
+\isacommand{by}\isamarkupfalse%
+\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -1363,6 +1340,9 @@
%
\endisadelimproof
\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+\isanewline
%
\isadelimtt
\isanewline
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Wed Apr 02 15:58:32 2008 +0200
@@ -1,8 +1,10 @@
structure HOL =
struct
-type 'a eq = {eqop : 'a -> 'a -> bool};
-fun eqop (A_:'a eq) = #eqop A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
+
+fun eqop A_ a = eq A_ a;
end; (*struct HOL*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Wed Apr 02 15:58:32 2008 +0200
@@ -1,8 +1,8 @@
structure HOL =
struct
-type 'a eq = {eqop : 'a -> 'a -> bool};
-fun eqop (A_:'a eq) = #eqop A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
fun less_eq (A_:'a ord) = #less_eq A_;
@@ -14,7 +14,6 @@
struct
fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) =
- HOL.less A2_ x1 x2 orelse
- HOL.eqop A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
+ HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Wed Apr 02 15:58:32 2008 +0200
@@ -3,10 +3,10 @@
datatype nat = Suc of nat | Zero_nat;
-fun eqop_nat Zero_nat Zero_nat = true
- | eqop_nat (Suc m) (Suc n) = eqop_nat m n
- | eqop_nat Zero_nat (Suc a) = false
- | eqop_nat (Suc a) Zero_nat = false;
+fun eq_nat Zero_nat Zero_nat = true
+ | eq_nat (Suc m) (Suc n) = eq_nat m n
+ | eq_nat Zero_nat (Suc a) = false
+ | eq_nat (Suc a) Zero_nat = false;
end; (*struct Nat*)
@@ -27,8 +27,8 @@
datatype monotype = Mono of Nat.nat * monotype list;
-fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
- Nat.eqop_nat tyco1 tyco2 andalso
- List.list_all2 eqop_monotype typargs1 typargs2;
+fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
+ Nat.eq_nat tyco1 tyco2 andalso
+ List.list_all2 eq_monotype typargs1 typargs2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Wed Apr 02 15:58:32 2008 +0200
@@ -24,7 +24,7 @@
structure Product_Type =
struct
-fun split c (a, b) = c a b;
+fun split f (a, b) = f a b;
end; (*struct Product_Type*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Wed Apr 02 15:58:32 2008 +0200
@@ -1,8 +1,10 @@
structure HOL =
struct
-type 'a eq = {eqop : 'a -> 'a -> bool};
-fun eqop (A_:'a eq) = #eqop A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
+
+fun eqop A_ a = eq A_ a;
end; (*struct HOL*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed Apr 02 15:58:32 2008 +0200
@@ -1,13 +1,15 @@
structure HOL =
struct
-type 'a eq = {eqop : 'a -> 'a -> bool};
-fun eqop (A_:'a eq) = #eqop A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
fun less_eq (A_:'a ord) = #less_eq A_;
fun less (A_:'a ord) = #less A_;
+fun eqop A_ a = eq A_ a;
+
end; (*struct HOL*)
structure Orderings =
@@ -26,12 +28,12 @@
datatype nat = Suc of nat | Zero_nat;
-fun eqop_nat Zero_nat Zero_nat = true
- | eqop_nat (Suc m) (Suc n) = eqop_nat m n
- | eqop_nat Zero_nat (Suc a) = false
- | eqop_nat (Suc a) Zero_nat = false;
+fun eq_nat Zero_nat Zero_nat = true
+ | eq_nat (Suc m) (Suc n) = eq_nat m n
+ | eq_nat Zero_nat (Suc a) = false
+ | eq_nat (Suc a) Zero_nat = false;
-val eq_nat = {eqop = eqop_nat} : nat HOL.eq;
+val eq_nata = {eq = eq_nat} : nat HOL.eq;
fun less_nat m (Suc n) = less_eq_nat m n
| less_nat n Zero_nat = false
@@ -68,13 +70,13 @@
else Branch (Leaf (key, vala), it, Leaf (it, entry))));
val example : (Nat.nat, (Nat.nat list)) searchtree =
- update (Nat.eq_nat, Nat.linorder_nat)
+ update (Nat.eq_nata, Nat.linorder_nat)
(Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
[Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
- (update (Nat.eq_nat, Nat.linorder_nat)
+ (update (Nat.eq_nata, Nat.linorder_nat)
(Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
[Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
- (update (Nat.eq_nat, Nat.linorder_nat)
+ (update (Nat.eq_nata, Nat.linorder_nat)
(Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
(Leaf (Nat.Suc Nat.Zero_nat, []))));
--- a/src/HOL/HOL.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/HOL.thy Wed Apr 02 15:58:32 2008 +0200
@@ -1644,24 +1644,6 @@
setup "CodeName.setup #> CodeTarget.setup #> Nbe.setup"
-class eq (attach "op =") = type
-
-lemma [code func]:
- shows "False \<and> x \<longleftrightarrow> False"
- and "True \<and> x \<longleftrightarrow> x"
- and "x \<and> False \<longleftrightarrow> False"
- and "x \<and> True \<longleftrightarrow> x" by simp_all
-
-lemma [code func]:
- shows "False \<or> x \<longleftrightarrow> x"
- and "True \<or> x \<longleftrightarrow> True"
- and "x \<or> False \<longleftrightarrow> x"
- and "x \<or> True \<longleftrightarrow> True" by simp_all
-
-lemma [code func]:
- shows "\<not> True \<longleftrightarrow> False"
- and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-
code_datatype Trueprop "prop"
code_datatype "TYPE('a\<Colon>{})"
@@ -1683,6 +1665,37 @@
#> Code.add_undefined @{const_name undefined}
*}
+class eq = type +
+ fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ assumes eq: "eq x y \<longleftrightarrow> x = y "
+begin
+
+lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+
+end
+
+setup {*
+ CodeUnit.add_const_alias @{thm equals_eq}
+*}
+
+lemma [code func]:
+ shows "False \<and> x \<longleftrightarrow> False"
+ and "True \<and> x \<longleftrightarrow> x"
+ and "x \<and> False \<longleftrightarrow> False"
+ and "x \<and> True \<longleftrightarrow> x" by simp_all
+
+lemma [code func]:
+ shows "False \<or> x \<longleftrightarrow> x"
+ and "True \<or> x \<longleftrightarrow> True"
+ and "x \<or> False \<longleftrightarrow> x"
+ and "x \<or> True \<longleftrightarrow> True" by simp_all
+
+lemma [code func]:
+ shows "\<not> True \<longleftrightarrow> False"
+ and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
+
+
subsection {* Legacy tactics and ML bindings *}
--- a/src/HOL/Library/Enum.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Library/Enum.thy Wed Apr 02 15:58:32 2008 +0200
@@ -38,12 +38,16 @@
subsection {* Equality and order on functions *}
-instance "fun" :: (enum, eq) eq ..
+instantiation "fun" :: (enum, eq) eq
+begin
-lemma eq_fun [code func]:
- fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>eq"
- shows "f = g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
- by (simp add: enum_all expand_fun_eq)
+definition
+ "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)
+
+end
lemma order_fun [code func]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
--- a/src/HOL/Library/Nested_Environment.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Wed Apr 02 15:58:32 2008 +0200
@@ -527,21 +527,21 @@
lemma [code func, code func del]:
fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
- shows "e1 = e2 \<longleftrightarrow> e1 = e2" ..
+ shows "eq e1 e2 \<longleftrightarrow> 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 "Env x f = Env y g \<longleftrightarrow>
- x = y \<and> (\<forall>z\<in>UNIV. case f z
+ shows "eq (Env x f) (Env y g) \<longleftrightarrow>
+ 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> a = b))" (is ?env)
- and "Val a = Val b \<longleftrightarrow> a = b"
- and "Val a = Env y g \<longleftrightarrow> False"
- and "Env x f = Val b \<longleftrightarrow> False"
-proof -
+ 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"
+proof (unfold eq)
have "f = g \<longleftrightarrow> (\<forall>z. case f z
of None \<Rightarrow> (case g z
of None \<Rightarrow> True | Some _ \<Rightarrow> False)
@@ -559,7 +559,12 @@
then show "f z = g z" by (auto split: option.splits)
qed
qed
- then show ?env by simp
+ then show "Env x f = Env y g \<longleftrightarrow>
+ 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> a = b))" by simp
qed simp_all
end
--- a/src/HOL/Real/Rational.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Real/Rational.thy Wed Apr 02 15:58:32 2008 +0200
@@ -666,10 +666,17 @@
by (cases "l = 0")
(auto simp add: Rational_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
-instance rat :: eq ..
+instantiation rat :: eq
+begin
+
+definition [code func del]: "eq (r\<Colon>rat) s \<longleftrightarrow> r = s"
-lemma rat_eq_code [code]: "Rational x = Rational y \<longleftrightarrow> normNum x = normNum y"
- unfolding Rational_def INum_normNum_iff ..
+instance by default (simp add: eq_rat_def)
+
+lemma rat_eq_code [code]: "eq (Rational x) (Rational y) \<longleftrightarrow> eq (normNum x) (normNum y)"
+ unfolding Rational_def INum_normNum_iff eq ..
+
+end
lemma rat_less_eq_code [code]: "Rational x \<le> Rational y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
proof -
--- a/src/HOL/Real/RealDef.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Apr 02 15:58:32 2008 +0200
@@ -978,10 +978,17 @@
"1 = Ratreal 1\<^sub>N" by simp
declare one_real_code [symmetric, code post]
-instance real :: eq ..
+instantiation real :: eq
+begin
+
+definition "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"
- unfolding Ratreal_def INum_normNum_iff ..
+ unfolding Ratreal_def INum_normNum_iff eq ..
+
+end
lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
proof -
--- a/src/HOL/Set.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Set.thy Wed Apr 02 15:58:32 2008 +0200
@@ -2261,13 +2261,6 @@
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
by simp
-instance set :: (eq) eq ..
-
-lemma eq_set_code [code func]:
- fixes A B :: "'a\<Colon>eq set"
- shows "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by auto
-
lemma subset_eq_code [code func]:
fixes A B :: "'a\<Colon>eq set"
shows "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
@@ -2278,6 +2271,16 @@
shows "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
by auto
+instantiation set :: (eq) eq
+begin
+
+definition
+ "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+
+instance by default (auto simp add: eq_set_def)
+
+end
+
subsubsection {* Derived operations *}
@@ -2302,7 +2305,7 @@
"Union A = UNION A (\<lambda>x. x)"
by auto
-code_reserved SML union inter (* Avoid clashes with ML infixes *)
+code_reserved SML union inter -- {* avoid clashes with ML infixes *}
subsection {* Basic ML bindings *}
--- a/src/HOL/SizeChange/Correctness.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/SizeChange/Correctness.thy Wed Apr 02 15:58:32 2008 +0200
@@ -637,7 +637,7 @@
lemma desc_scgcomp:
"dsc (G * H) m r =
- (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R")
+ (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eqp G m n \<and> dsc H n r))" (is "?L = ?R")
proof
show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
--- a/src/HOL/SizeChange/Criterion.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/SizeChange/Criterion.thy Wed Apr 02 15:58:32 2008 +0200
@@ -44,7 +44,7 @@
instance sedge :: finite
proof
show "finite (UNIV::sedge set)"
- by (simp add: sedge_UNIV)
+ by (simp add: sedge_UNIV)
qed
@@ -62,7 +62,7 @@
"dsc G i j \<equiv> has_edge G i LESS j"
abbreviation (input)
- "eq G i j \<equiv> has_edge G i LEQ j"
+ "eqp G i j \<equiv> has_edge G i LEQ j"
abbreviation
eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/SizeChange/Interpretation.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/SizeChange/Interpretation.thy Wed Apr 02 15:58:32 2008 +0200
@@ -190,7 +190,7 @@
where
"approx G C C' M M'
= (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
- \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
+ \<and>(eqp G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
@@ -360,7 +360,7 @@
assume "n < i"
with fr have "eqlat ?p th i" by simp
- hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2"
+ hence "dsc (Gs i) ?q1 ?q2 \<or> eqp (Gs i) ?q1 ?q2"
by simp
thus "?seq (Suc i) \<le> ?seq i"
proof
@@ -376,7 +376,7 @@
apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
by (rule ird a)+
next
- assume "eq (Gs i) ?q1 ?q2"
+ assume "eqp (Gs i) ?q1 ?q2"
with approx
have a:"decreq (cs i) (cs (Suc i))
--- a/src/HOL/Tools/datatype_codegen.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Wed Apr 02 15:58:32 2008 +0200
@@ -431,26 +431,44 @@
fun add_datatypes_equality vs dtcos thy =
let
+ val vs' = (map o apsnd)
+ (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
+ fun add_def tyco lthy =
+ let
+ val ty = Type (tyco, map TFree vs');
+ 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 ="}));
+ val def' = Syntax.check_term lthy def;
+ val ((_, (_, thm)), lthy') = Specification.definition
+ (NONE, (("", []), def')) lthy;
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
+ fun tac thms = Class.intro_classes_tac []
+ THEN ALLGOALS (ProofContext.fact_tac thms);
fun get_eq' thy dtco = get_eq thy dtco
|> map (CodeUnit.constrain_thm [HOLogic.class_eq])
- |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy);
+ |> map Simpdata.mk_eq
+ |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
fun add_eq_thms dtco thy =
let
val thy_ref = Theory.check_thy thy;
- val const = AxClass.param_of_inst thy ("op =", dtco);
+ val const = AxClass.param_of_inst thy (@{const_name eq}, dtco);
val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
in
Code.add_funcl (const, Susp.delay get_thms) thy
end;
- val vs' = (map o apsnd)
- (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
in
thy
|> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit
- |> ProofContext.theory_of
- |> fold add_eq_thms dtcos
+ |> fold_map add_def dtcos
+ |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
+ #> LocalTheory.exit
+ #> ProofContext.theory_of
+ #> fold Code.del_func thms
+ #> fold add_eq_thms dtcos)
end;
--- a/src/HOL/Tools/typecopy_package.ML Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Wed Apr 02 15:58:32 2008 +0200
@@ -125,15 +125,39 @@
val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
+ fun add_def tyco lthy =
+ let
+ val ty = Type (tyco, map TFree vs');
+ 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 ="}));
+ val def' = Syntax.check_term lthy def;
+ val ((_, (_, thm)), lthy') = Specification.definition
+ (NONE, (("", []), def')) lthy;
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
+ fun tac thms = Class.intro_classes_tac []
+ THEN ALLGOALS (ProofContext.fact_tac thms);
+ fun add_eq_thm thy =
+ let
+ val eq = inject
+ |> CodeUnit.constrain_thm [HOLogic.class_eq]
+ |> Simpdata.mk_eq
+ |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
+ in Code.add_func eq thy end;
in
thy
|> Code.add_datatype [(constr, ty)]
|> Code.add_func proj_def
|> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit
- |> ProofContext.theory_of
- |> Code.add_func (CodeUnit.constrain_thm [HOLogic.class_eq] inject)
+ |> add_def tyco
+ |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
+ #> LocalTheory.exit
+ #> ProofContext.theory_of
+ #> Code.del_func thm
+ #> add_eq_thm)
end;
val setup =
--- a/src/HOL/ex/Meson_Test.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/ex/Meson_Test.thy Wed Apr 02 15:58:32 2008 +0200
@@ -11,8 +11,8 @@
below and constants declared in HOL!
*}
-hide const subset member quotient
-
+hide const subset member quotient eq
+hide const eq
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/NormalForm.thy Wed Apr 02 15:58:31 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Wed Apr 02 15:58:32 2008 +0200
@@ -8,6 +8,8 @@
imports Main "~~/src/HOL/Real/Rational"
begin
+declare equals_eq [symmetric, code post]
+
lemma "True" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code func]
@@ -58,19 +60,19 @@
lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
-lemma "split (%x y. x) (a, b) = a" by normalization rule
+lemma "split (%(x\<Colon>'a\<Colon>eq) y. x) (a, b) = a" by normalization rule
lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
lemma "[] @ [] = []" by normalization
-lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization rule+
-lemma "[a, b, c] @ xs = a # b # c # xs" by normalization rule+
-lemma "[] @ xs = xs" by normalization rule
+lemma "map f [x,y,z::'x] = [f x \<Colon> 'a\<Colon>eq, f y, f z]" by normalization rule+
+lemma "[a \<Colon> 'a\<Colon>eq, b, c] @ xs = a # b # c # xs" by normalization rule+
+lemma "[] @ xs = (xs \<Colon> 'a\<Colon>eq list)" by normalization rule
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization rule+
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
-lemma "rev [a, b, c] = [c, b, a]" by normalization rule+
-normal_form "rev (a#b#cs) = rev cs @ [b, a]"
+lemma "rev [a, b, c] = [c \<Colon> 'a\<Colon>eq, b, a]" by normalization rule+
+normal_form "rev (a#b#cs) = rev cs @ [b, a \<Colon> 'a\<Colon>eq]"
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
@@ -78,19 +80,19 @@
by normalization
normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
-lemma "let x = y in [x, x] = [y, y]" by normalization rule+
-lemma "Let y (%x. [x,x]) = [y, y]" by normalization rule+
+lemma "let x = y in [x, x] = [y \<Colon> 'a\<Colon>eq, y]" by normalization rule+
+lemma "Let y (%x. [x,x]) = [y \<Colon> 'a\<Colon>eq, y]" by normalization rule+
normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization rule+
normal_form "filter (%x. x) ([True,False,x]@xs)"
normal_form "filter Not ([True,False,x]@xs)"
-lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]" by normalization rule+
-lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization rule+
+lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c \<Colon> 'a\<Colon>eq]" by normalization rule+
+lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f \<Colon> 'a\<Colon>eq]" by normalization rule+
lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
-lemma "last [a, b, c] = c" by normalization rule
-lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
+lemma "last [a, b, c \<Colon> 'a\<Colon>eq] = c" by normalization rule
+lemma "last ([a, b, c \<Colon> 'a\<Colon>eq] @ xs) = (if null xs then c else last xs)"
by normalization rule
lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization rule
@@ -111,10 +113,10 @@
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
normal_form "Suc 0 \<in> set ms"
-lemma "f = f" by normalization rule+
-lemma "f x = f x" by normalization rule+
-lemma "(f o g) x = f (g x)" by normalization rule+
-lemma "(f o id) x = f x" by normalization rule+
+lemma "f = (f \<Colon> 'a\<Colon>eq)" by normalization rule+
+lemma "f x = (f x \<Colon> 'a\<Colon>eq)" by normalization rule+
+lemma "(f o g) x = (f (g x) \<Colon> 'a\<Colon>eq)" by normalization rule+
+lemma "(f o id) x = (f x \<Colon> 'a\<Colon>eq)" by normalization rule+
normal_form "(\<lambda>x. x)"
(* Church numerals: *)