simplified '?' operator;
authorwenzelm
Tue Nov 28 00:35:25 2006 +0100 (2006-11-28 ago)
changeset 21568a8070c4b6d43
parent 21567 c097a926ba78
child 21569 a0d0ea84521d
simplified '?' operator;
added expand_defs;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Nov 28 00:35:23 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Nov 28 00:35:25 2006 +0100
     1.3 @@ -11,9 +11,10 @@
     1.4    val abs_def: term -> (string * typ) * term
     1.5    val mk_def: Proof.context -> (string * term) list -> term list
     1.6    val def_export: Assumption.export
     1.7 -  val find_def: Proof.context -> string -> thm option
     1.8    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     1.9      (term * (bstring * thm)) list * Proof.context
    1.10 +  val find_def: Proof.context -> string -> thm option
    1.11 +  val expand_defs: Proof.context -> Proof.context -> thm -> thm list * thm
    1.12    val print_rules: Proof.context -> unit
    1.13    val defn_add: attribute
    1.14    val defn_del: attribute
    1.15 @@ -75,15 +76,6 @@
    1.16    |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    1.17  
    1.18  
    1.19 -(* find def *)
    1.20 -
    1.21 -fun find_def ctxt x =
    1.22 -  Assumption.prems_of ctxt |> find_first (fn th =>
    1.23 -    (case try (head_of_def o Thm.prop_of) th of
    1.24 -      SOME y => x = y
    1.25 -    | NONE => false));
    1.26 -
    1.27 -
    1.28  (* add defs *)
    1.29  
    1.30  fun add_defs defs ctxt =
    1.31 @@ -103,6 +95,23 @@
    1.32    end;
    1.33  
    1.34  
    1.35 +(* find/expand defs -- based on educated guessing *)
    1.36 +
    1.37 +fun find_def ctxt x =
    1.38 +  Assumption.prems_of ctxt |> find_first (fn th =>
    1.39 +    (case try (head_of_def o Thm.prop_of) th of
    1.40 +      SOME y => x = y
    1.41 +    | NONE => false));
    1.42 +
    1.43 +fun expand_defs inner outer th =
    1.44 +  let
    1.45 +    val th' = Assumption.export false inner outer th;
    1.46 +    val xs = map #1 (Drule.fold_terms Term.add_frees th []);
    1.47 +    val ys = map #1 (Drule.fold_terms Term.add_frees th' []);
    1.48 +    val defs = map_filter (find_def inner) (subtract (op =) ys xs);
    1.49 +  in (defs, th') end;
    1.50 +
    1.51 +
    1.52  
    1.53  (** defived definitions **)
    1.54  
    1.55 @@ -163,7 +172,7 @@
    1.56        |> Thm.cterm_of (ProofContext.theory_of ctxt)
    1.57        |> meta_rewrite ctxt
    1.58        |> (snd o Logic.dest_equals o Thm.prop_of)
    1.59 -      |> K conditional ? Logic.strip_imp_concl
    1.60 +      |> conditional ? Logic.strip_imp_concl
    1.61        |> (abs_def o #2 o cert_def ctxt);
    1.62      fun prove ctxt' def =
    1.63        let