# HG changeset patch # User haftmann # Date 1276509690 -7200 # Node ID b5492f611129904a4fb8bbb80cb3edafe3bfe1b5 # Parent ed431cc99f170f3a30d7ad015416f20344fc0fcf explicitly name and note equations for class eq diff -r ed431cc99f17 -r b5492f611129 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Jun 14 12:01:30 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Jun 14 12:01:30 2010 +0200 @@ -105,12 +105,14 @@ in (thm', lthy') end; fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (ProofContext.fact_tac thms); + fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name; fun add_eq_thms dtco = Theory.checkpoint #> `(fn thy => mk_eq_eqns thy dtco) - #-> (fn (thms, thm) => - Code.add_nbe_eqn thm - #> fold_rev Code.add_eqn thms); + #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK + [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), + ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])]) + #> snd in thy |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq]) diff -r ed431cc99f17 -r b5492f611129 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jun 14 12:01:30 2010 +0200 +++ b/src/Pure/Isar/code.ML Mon Jun 14 12:01:30 2010 +0200 @@ -59,6 +59,9 @@ val add_default_eqn: thm -> theory -> theory val add_default_eqn_attribute: attribute val add_default_eqn_attrib: Attrib.src + val add_nbe_default_eqn: thm -> theory -> theory + val add_nbe_default_eqn_attribute: attribute + val add_nbe_default_eqn_attrib: Attrib.src val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory val add_case: thm -> theory -> theory @@ -1066,18 +1069,25 @@ of SOME eqn => gen_add_eqn false eqn thy | NONE => thy; +fun add_nbe_eqn thm thy = + gen_add_eqn false (mk_eqn thy (thm, false)) thy; + fun add_default_eqn thm thy = case mk_eqn_liberal thy thm of SOME eqn => gen_add_eqn true eqn thy | NONE => thy; -fun add_nbe_eqn thm thy = - gen_add_eqn false (mk_eqn thy (thm, false)) thy; - val add_default_eqn_attribute = Thm.declaration_attribute (fn thm => Context.mapping (add_default_eqn thm) I); val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); +fun add_nbe_default_eqn thm thy = + gen_add_eqn true (mk_eqn thy (thm, false)) thy; + +val add_nbe_default_eqn_attribute = Thm.declaration_attribute + (fn thm => Context.mapping (add_nbe_default_eqn thm) I); +val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute); + fun add_abs_eqn raw_thm thy = let val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;