# HG changeset patch # User haftmann # Date 1207144712 -7200 # Node ID 6f306c8c2c5495adf1e367de9c020e2117dfedf7 # Parent 682dfb674df35c68fd791f227afd89fdeaa57729 explicit class "eq" for operational equality diff -r 682dfb674df3 -r 6f306c8c2c54 NEWS --- 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. diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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\bar) y \ x = y" + +instance by default (simp add: eq_bar_def) + +end code_type %tt bar (Haskell "Integer") diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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 diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- 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*) diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- 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*) diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- 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*) diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- 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*) diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML --- 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*) diff -r 682dfb674df3 -r 6f306c8c2c54 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- 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, [])))); diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/HOL.thy --- 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 \ x \ False" - and "True \ x \ x" - and "x \ False \ False" - and "x \ True \ x" by simp_all - -lemma [code func]: - shows "False \ x \ x" - and "True \ x \ True" - and "x \ False \ x" - and "x \ True \ True" by simp_all - -lemma [code func]: - shows "\ True \ False" - and "\ False \ True" by (rule HOL.simp_thms)+ - code_datatype Trueprop "prop" code_datatype "TYPE('a\{})" @@ -1683,6 +1665,37 @@ #> Code.add_undefined @{const_name undefined} *} +class eq = type + + fixes eq :: "'a \ 'a \ bool" + assumes eq: "eq x y \ x = y " +begin + +lemma equals_eq [code inline, code func]: "op = \ 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 \ x \ False" + and "True \ x \ x" + and "x \ False \ False" + and "x \ True \ x" by simp_all + +lemma [code func]: + shows "False \ x \ x" + and "True \ x \ True" + and "x \ False \ x" + and "x \ True \ True" by simp_all + +lemma [code func]: + shows "\ True \ False" + and "\ False \ True" by (rule HOL.simp_thms)+ + + subsection {* Legacy tactics and ML bindings *} diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Library/Enum.thy --- 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\enum \ 'b\eq" - shows "f = g \ (\x \ set enum. f x = g x)" - by (simp add: enum_all expand_fun_eq) +definition + "eq f g \ (\x \ 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\enum \ 'b\order" diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Library/Nested_Environment.thy --- 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\eq, 'a\eq, 'c\eq) env" - shows "e1 = e2 \ e1 = e2" .. + shows "eq e1 e2 \ eq e1 e2" .. lemma eq_env_code [code func]: fixes x y :: "'a\eq" and f g :: "'c\{eq, finite} \ ('b\eq, 'a, 'c) env option" - shows "Env x f = Env y g \ - x = y \ (\z\UNIV. case f z + shows "eq (Env x f) (Env y g) \ + eq x y \ (\z\UNIV. case f z of None \ (case g z of None \ True | Some _ \ False) | Some a \ (case g z - of None \ False | Some b \ a = b))" (is ?env) - and "Val a = Val b \ a = b" - and "Val a = Env y g \ False" - and "Env x f = Val b \ False" -proof - + of None \ False | Some b \ eq a b))" (is ?env) + and "eq (Val a) (Val b) \ eq a b" + and "eq (Val a) (Env y g) \ False" + and "eq (Env x f) (Val b) \ False" +proof (unfold eq) have "f = g \ (\z. case f z of None \ (case g z of None \ True | Some _ \ 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 \ + x = y \ (\z\UNIV. case f z + of None \ (case g z + of None \ True | Some _ \ False) + | Some a \ (case g z + of None \ False | Some b \ a = b))" by simp qed simp_all end diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Real/Rational.thy --- 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\rat) s \ r = s" -lemma rat_eq_code [code]: "Rational x = Rational y \ 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) \ eq (normNum x) (normNum y)" + unfolding Rational_def INum_normNum_iff eq .. + +end lemma rat_less_eq_code [code]: "Rational x \ Rational y \ normNum x \\<^sub>N normNum y" proof - diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Real/RealDef.thy --- 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\real) y \ x = y" + +instance by default (simp add: eq_real_def) lemma real_eq_code [code]: "Ratreal x = Ratreal y \ 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 \ Ratreal y \ normNum x \\<^sub>N normNum y" proof - diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Set.thy --- 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 \ A \ (\x\A. a = x)" by simp -instance set :: (eq) eq .. - -lemma eq_set_code [code func]: - fixes A B :: "'a\eq set" - shows "A = B \ A \ B \ B \ A" - by auto - lemma subset_eq_code [code func]: fixes A B :: "'a\eq set" shows "A \ B \ (\x\A. x \ B)" @@ -2278,6 +2271,16 @@ shows "A \ B \ A \ B \ \ B \ A" by auto +instantiation set :: (eq) eq +begin + +definition + "eq A B \ A \ B \ B \ A" + +instance by default (auto simp add: eq_set_def) + +end + subsubsection {* Derived operations *} @@ -2302,7 +2305,7 @@ "Union A = UNION A (\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 *} diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/SizeChange/Correctness.thy --- 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 = - (\n. (dsc G m n \ eql H n r) \ (eq G m n \ dsc H n r))" (is "?L = ?R") + (\n. (dsc G m n \ eql H n r) \ (eqp G m n \ dsc H n r))" (is "?L = ?R") proof show "?R \ ?L" by (auto simp:in_grcomp mult_sedge_def) diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/SizeChange/Criterion.thy --- 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 \ has_edge G i LESS j" abbreviation (input) - "eq G i j \ has_edge G i LEQ j" + "eqp G i j \ has_edge G i LEQ j" abbreviation eql :: "'a scg \ 'a \ 'a \ bool" diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/SizeChange/Interpretation.thy --- 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' = (\i j. (dsc G i j \ decr C C' (M i) (M' j)) - \(eq G i j \ decreq C C' (M i) (M' j)))" + \(eqp G i j \ 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 \ eq (Gs i) ?q1 ?q2" + hence "dsc (Gs i) ?q1 ?q2 \ eqp (Gs i) ?q1 ?q2" by simp thus "?seq (Suc i) \ ?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)) diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/Tools/typecopy_package.ML --- 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 = diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/ex/Meson_Test.thy --- 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 diff -r 682dfb674df3 -r 6f306c8c2c54 src/HOL/ex/NormalForm.thy --- 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 \ 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\'a\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 \ True | S x \ 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 \ 'a\eq, f y, f z]" by normalization rule+ +lemma "[a \ 'a\eq, b, c] @ xs = a # b # c # xs" by normalization rule+ +lemma "[] @ xs = (xs \ 'a\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 \ 'a\eq, b, a]" by normalization rule+ +normal_form "rev (a#b#cs) = rev cs @ [b, a \ 'a\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 [] \ True | x#xs \ False" normal_form "map (%x. case x of None \ False | Some y \ 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 \ 'a\eq, y]" by normalization rule+ +lemma "Let y (%x. [x,x]) = [y \ 'a\eq, y]" by normalization rule+ normal_form "case n of Z \ True | S x \ 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 \ 'a\eq]" by normalization rule+ +lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f \ 'a\eq]" by normalization rule+ lemma "map (%x. case x of None \ False | Some y \ 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 \ 'a\eq] = c" by normalization rule +lemma "last ([a, b, c \ 'a\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 \ 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 \ 'a\eq)" by normalization rule+ +lemma "f x = (f x \ 'a\eq)" by normalization rule+ +lemma "(f o g) x = (f (g x) \ 'a\eq)" by normalization rule+ +lemma "(f o id) x = (f x \ 'a\eq)" by normalization rule+ normal_form "(\x. x)" (* Church numerals: *)