1.1 --- a/src/HOL/Tools/inductive.ML	Mon Aug 23 16:47:55 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Aug 23 16:47:57 2010 +0200
     1.3 @@ -195,6 +195,21 @@
     1.4  
     1.5  
     1.6  
     1.7 +(** equations **)
     1.8 +
     1.9 +structure Equation_Data = Generic_Data
    1.10 +(
    1.11 +  type T = thm Item_Net.T;
    1.12 +  val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
    1.13 +    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
    1.14 +  val extend = I;
    1.15 +  val merge = Item_Net.merge;
    1.16 +);
    1.17 +
    1.18 +val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update)
    1.19 +
    1.20 +
    1.21 +
    1.22  (** misc utilities **)
    1.23  
    1.24  fun message quiet_mode s = if quiet_mode then () else writeln s;
    1.25 @@ -548,16 +563,20 @@
    1.26  
    1.27  fun mk_simp_eq ctxt prop =
    1.28    let
    1.29 +    val thy = ProofContext.theory_of ctxt
    1.30      val ctxt' = Variable.auto_fixes prop ctxt
    1.31 -    val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
    1.32 -    val info = the_inductive ctxt cname
    1.33 -    val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
    1.34 -    val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
    1.35 -    val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
    1.36 -      (Vartab.empty, Vartab.empty)
    1.37 -    val certify = cterm_of (ProofContext.theory_of ctxt)
    1.38 -    val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
    1.39 -      (Term.add_vars lhs_eq [])
    1.40 +    val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
    1.41 +    val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) 
    1.42 +      |> map_filter
    1.43 +        (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
    1.44 +            (Vartab.empty, Vartab.empty), eq)
    1.45 +          handle Pattern.MATCH => NONE)
    1.46 +    val (subst, eq) = case substs of
    1.47 +        [s] => s
    1.48 +      | _ => error
    1.49 +        ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")
    1.50 +    val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
    1.51 +      (Term.add_vars (lhs_of eq) [])
    1.52     in
    1.53      cterm_instantiate inst eq
    1.54      |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
    1.55 @@ -833,7 +852,8 @@
    1.56  
    1.57      val (eqs', lthy3) = lthy2 |> 
    1.58        fold_map (fn (name, eq) => Local_Theory.note
    1.59 -          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq])
    1.60 +          ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
    1.61 +            [Attrib.internal (K add_equation)]), [eq])
    1.62            #> apfst (hd o snd))
    1.63          (if null eqs then [] else (cnames ~~ eqs))
    1.64      val (inducts, lthy4) =

     2.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Aug 23 16:47:55 2010 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Aug 23 16:47:57 2010 +0200
     2.3 @@ -477,7 +477,7 @@
     2.4          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     2.5      val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
     2.6      val monos' = map (to_pred [] (Context.Proof lthy)) monos;
     2.7 -    val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
     2.8 +    val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
     2.9        Inductive.add_ind_def
    2.10          {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
    2.11            coind = coind, no_elim = no_elim, no_ind = no_ind,
    2.12 @@ -520,14 +520,13 @@
    2.13      val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
    2.14      val (intr_names, intr_atts) = split_list (map fst intros);
    2.15      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
    2.16 -    val eqs = [] (* TODO: define equations *)
    2.17      val (intrs', elims', eqs', induct, inducts, lthy4) =
    2.18        Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
    2.19          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    2.20          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    2.21             map fst (fst (Rule_Cases.get th)),
    2.22             Rule_Cases.get_constraints th)) elims)
    2.23 -        eqs raw_induct' lthy3;
    2.24 +        (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
    2.25    in
    2.26      ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
    2.27        raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},