# HG changeset patch
# User bulwahn
# Date 1268392470 -3600
# Node ID cfde251d03a53c55c606cd89dc47b18358779616
# Parent  19eefc0655b64de18ee77527d7258c3b73d37019
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function

diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -81,7 +81,7 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts,
+        val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
           termination, domintros, cases, ...} =
           cont (Thm.close_derivation proof)
 
@@ -97,7 +97,7 @@
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
           ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
-          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o (pair fs)) trsimps
+          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
           ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes 1)),
@@ -165,7 +165,7 @@
               simps=SOME simps, inducts=SOME inducts, termination=termination }
             in
               Local_Theory.declaration false (add_function_data o morph_function_data info')
-              #> Spec_Rules.add Spec_Rules.Equational (fs, simps)
+              #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
             end)
         end
   in
diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -130,8 +130,9 @@
     fun define_overloaded (def_name, eq) lthy =
       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
-        val ((_, (_, thm)), lthy') = lthy
-          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
+        val (thm, lthy') = lthy
+          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
+          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -8,9 +8,9 @@
 signature TFL =
 sig
   val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
-    term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
+    term -> term list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list}
   val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
-    string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
+    string -> string list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list}
   val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
   val defer: theory -> thm list -> xstring -> string list -> theory * thm
 end;
@@ -204,12 +204,13 @@
 fun define_i strict thy cs ss congs wfs fid R eqs =
   let val {functional,pats} = Prim.mk_functional thy eqs
       val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
+      val (lhs, _) = Logic.dest_equals (prop_of def)
       val {induct, rules, tcs} = 
           simplify_defn strict thy cs ss congs wfs fid pats def
       val rules' = 
           if strict then derive_init_eqs thy rules eqs
           else rules
-  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
+  in (thy, {lhs = lhs, rules = rules', induct = induct, tcs = tcs}) end;
 
 fun define strict thy cs ss congs wfs fid R seqs =
   define_i strict thy cs ss congs wfs fid
diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -281,14 +281,13 @@
       thy'
       |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     val simps'' = maps snd simps';
-    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
-    val specs = (distinct (op =) (map dest_eqn simps''), simps'')
+    val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
   in
     thy''
     |> note (("simps",
         [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
     |> snd
-    |> Spec_Rules.add_global Spec_Rules.Equational specs
+    |> Spec_Rules.add_global Spec_Rules.Equational (lhss, simps)
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd
     |> Sign.parent_path
diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/primrec.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -265,15 +265,6 @@
 
 local
 
-fun specs_of simps =
-  let
-    val eqns = maps snd simps
-    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
-    val t = distinct (op =) (map dest_eqn eqns)
-  in
-    (t, eqns)
-  end
-
 fun gen_primrec prep_spec raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
@@ -285,10 +276,11 @@
   in
     lthy
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, (ts, simps)) => fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
+    |-> (fn (prefix, (ts, simps)) =>
+      Spec_Rules.add Spec_Rules.Equational (ts, simps)
+      #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
-      #>> (fn (_, simps'') => (ts, simps''))
-      ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps'))))
+      #>> (fn (_, simps'') => (ts, simps''))))
   end;
 
 in
diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/recdef.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -7,7 +7,7 @@
 signature RECDEF =
 sig
   val get_recdef: theory -> string
-    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
+    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   val simp_add: attribute
   val simp_del: attribute
@@ -17,9 +17,9 @@
   val wf_del: attribute
   val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
     Attrib.src option -> theory -> theory
-      * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
+      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
-    theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
+    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
@@ -84,7 +84,7 @@
 
 (* theory data *)
 
-type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
+type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
 structure GlobalRecdefData = Theory_Data
 (
@@ -198,7 +198,7 @@
     (*We must remove imp_cong to prevent looping when the induction rule
       is simplified. Many induction rules have nested implications that would
       give rise to looping conditional rewriting.*)
-    val (thy, {rules = rules_idx, induct, tcs}) =
+    val (thy, {lhs, rules = rules_idx, induct, tcs}) =
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
@@ -211,8 +211,8 @@
       |> PureThy.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules);
-    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
+      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
+    val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
       |> put_recdef name result