src/HOL/Tools/recfun_codegen.ML
changeset 18702 7dc7dcd63224
parent 18220 43cf5767f992
child 18708 4b3dadb4fe33
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jan 17 16:36:57 2006 +0100
@@ -10,6 +10,7 @@
   val add: string option -> theory attribute
   val del: theory attribute
   val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
+  val get_thm_equations: theory -> string * typ -> (thm list * typ) option
   val setup: (theory -> theory) list
 end;
 
@@ -93,6 +94,17 @@
   |> apfst (map prop_of)
   |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
 
+fun get_thm_equations thy (c, ty) =
+  Symtab.lookup (CodegenData.get thy) c
+  |> Option.map (fn thms => 
+       List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms
+       |> del_redundant thy [])
+  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
+  |> Option.map (fn thms =>
+       (preprocess thy (map fst thms),
+          (snd o const_of o prop_of o fst o hd) thms))
+  |> (Option.map o apfst o map) (fn thm => thm RS HOL.eq_reflection);
+
 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
 
@@ -185,8 +197,8 @@
   add_attribute ""
     (   Args.del |-- Scan.succeed del
      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
-  CodegenPackage.add_defgen
-    ("rec", CodegenPackage.defgen_recfun get_rec_equations)
+  CodegenPackage.add_eqextr
+    ("rec", fn thy => fn _ => get_thm_equations thy)
 ];
 
 end;