src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Tue Nov 28 00:35:23 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Nov 28 00:35:25 2006 +0100
@@ -11,9 +11,10 @@
   val abs_def: term -> (string * typ) * term
   val mk_def: Proof.context -> (string * term) list -> term list
   val def_export: Assumption.export
-  val find_def: Proof.context -> string -> thm option
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
+  val find_def: Proof.context -> string -> thm option
+  val expand_defs: Proof.context -> Proof.context -> thm -> thm list * thm
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -75,15 +76,6 @@
   |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 
-(* find def *)
-
-fun find_def ctxt x =
-  Assumption.prems_of ctxt |> find_first (fn th =>
-    (case try (head_of_def o Thm.prop_of) th of
-      SOME y => x = y
-    | NONE => false));
-
-
 (* add defs *)
 
 fun add_defs defs ctxt =
@@ -103,6 +95,23 @@
   end;
 
 
+(* find/expand defs -- based on educated guessing *)
+
+fun find_def ctxt x =
+  Assumption.prems_of ctxt |> find_first (fn th =>
+    (case try (head_of_def o Thm.prop_of) th of
+      SOME y => x = y
+    | NONE => false));
+
+fun expand_defs inner outer th =
+  let
+    val th' = Assumption.export false inner outer th;
+    val xs = map #1 (Drule.fold_terms Term.add_frees th []);
+    val ys = map #1 (Drule.fold_terms Term.add_frees th' []);
+    val defs = map_filter (find_def inner) (subtract (op =) ys xs);
+  in (defs, th') end;
+
+
 
 (** defived definitions **)
 
@@ -163,7 +172,7 @@
       |> Thm.cterm_of (ProofContext.theory_of ctxt)
       |> meta_rewrite ctxt
       |> (snd o Logic.dest_equals o Thm.prop_of)
-      |> K conditional ? Logic.strip_imp_concl
+      |> conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt);
     fun prove ctxt' def =
       let