replaced add_def by more elaborate add_defs;
authorwenzelm
Sat Oct 07 01:31:15 2006 +0200 (2006-10-07 ago)
changeset 20887ec9a1bb086da
parent 20886 f26672c248ee
child 20888 0ddd2f297ae7
replaced add_def by more elaborate add_defs;
added find_def (based on educated guesses);
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sat Oct 07 01:31:14 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Oct 07 01:31:15 2006 +0200
     1.3 @@ -11,7 +11,9 @@
     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 add_def: string * term -> Proof.context -> ((string * typ) * thm) * Proof.context
     1.8 +  val find_def: Proof.context -> string -> thm option
     1.9 +  val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
    1.10 +    (term * (bstring * thm)) list * Proof.context
    1.11    val print_rules: Context.generic -> unit
    1.12    val defn_add: attribute
    1.13    val defn_del: attribute
    1.14 @@ -56,34 +58,47 @@
    1.15  (* export defs *)
    1.16  
    1.17  val head_of_def =
    1.18 -  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body o Thm.term_of;
    1.19 +  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
    1.20  
    1.21  
    1.22  (*
    1.23 -  [x, x == t]
    1.24 +  [x, x == a]
    1.25         :
    1.26        B x
    1.27    -----------
    1.28 -      B t
    1.29 +      B a
    1.30  *)
    1.31  fun def_export _ defs thm =
    1.32    thm
    1.33    |> Drule.implies_intr_list defs
    1.34 -  |> Drule.generalize ([], map head_of_def defs)
    1.35 +  |> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
    1.36    |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    1.37  
    1.38  
    1.39 +(* find def *)
    1.40 +
    1.41 +fun find_def ctxt x =
    1.42 +  Assumption.prems_of ctxt |> find_first (fn th =>
    1.43 +    (case try (head_of_def o Thm.prop_of) th of
    1.44 +      SOME y => x = y
    1.45 +    | NONE => false));
    1.46 +
    1.47 +
    1.48  (* add defs *)
    1.49  
    1.50 -fun add_def (x, t) ctxt =
    1.51 +fun add_defs defs ctxt =
    1.52    let
    1.53 -    val [eq] = mk_def ctxt [(x, t)];
    1.54 -    val x' = Term.dest_Free (fst (Logic.dest_equals eq));
    1.55 +    val ((xs, mxs), specs) = defs |> split_list |>> split_list;
    1.56 +    val ((names, atts), rhss) = specs |> split_list |>> split_list;
    1.57 +    val names' = map2 Thm.def_name_optional xs names;
    1.58 +    val eqs = mk_def ctxt (xs ~~ rhss);
    1.59 +    val lhss = map (fst o Logic.dest_equals) eqs;
    1.60    in
    1.61      ctxt
    1.62 -    |> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
    1.63 -    |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
    1.64 -    |>> (fn [(_, [th])] => (x', th))
    1.65 +    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
    1.66 +    |> ProofContext.add_assms_i def_export
    1.67 +      (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
    1.68 +    |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
    1.69    end;
    1.70  
    1.71  
    1.72 @@ -149,9 +164,9 @@
    1.73        |> (snd o Logic.dest_equals o Thm.prop_of)
    1.74        |> K conditional ? Logic.strip_imp_concl
    1.75        |> (abs_def o #2 o cert_def ctxt);
    1.76 -    fun prove ctxt' t def =
    1.77 +    fun prove ctxt' lhs def =   (* FIXME check/simplify *)
    1.78        let
    1.79 -        val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
    1.80 +        val prop' = Term.subst_atomic [(Free (c, T), lhs)] prop;   (* FIXME !? *)
    1.81          val frees = Term.fold_aterms (fn Free (x, _) =>
    1.82            if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.83        in