# HG changeset patch # User bulwahn # Date 1282574877 -7200 # Node ID e92223c886f8b7f91510ea7097b266e80490cec8 # Parent 7215ae18f44b6b72cd237577c18f2d58887ac372 introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets diff -r 7215ae18f44b -r e92223c886f8 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Aug 23 16:47:55 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Mon Aug 23 16:47:57 2010 +0200 @@ -195,6 +195,21 @@ +(** equations **) + +structure Equation_Data = Generic_Data +( + type T = thm Item_Net.T; + val empty = Item_Net.init (op aconv o pairself Thm.prop_of) + (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); + val extend = I; + val merge = Item_Net.merge; +); + +val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update) + + + (** misc utilities **) fun message quiet_mode s = if quiet_mode then () else writeln s; @@ -548,16 +563,20 @@ fun mk_simp_eq ctxt prop = let + val thy = ProofContext.theory_of ctxt val ctxt' = Variable.auto_fixes prop ctxt - val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop)))) - val info = the_inductive ctxt cname - val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info))) - val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))) - val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop) - (Vartab.empty, Vartab.empty) - val certify = cterm_of (ProofContext.theory_of ctxt) - val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v)))) - (Term.add_vars lhs_eq []) + val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of + val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) + |> map_filter + (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop) + (Vartab.empty, Vartab.empty), eq) + handle Pattern.MATCH => NONE) + val (subst, eq) = case substs of + [s] => s + | _ => error + ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique") + val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) + (Term.add_vars (lhs_of eq) []) in cterm_instantiate inst eq |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv @@ -833,7 +852,8 @@ val (eqs', lthy3) = lthy2 |> fold_map (fn (name, eq) => Local_Theory.note - ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq]) + ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), + [Attrib.internal (K add_equation)]), [eq]) #> apfst (hd o snd)) (if null eqs then [] else (cnames ~~ eqs)) val (inducts, lthy4) = diff -r 7215ae18f44b -r e92223c886f8 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Mon Aug 23 16:47:55 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Mon Aug 23 16:47:57 2010 +0200 @@ -477,7 +477,7 @@ eta_contract (member op = cs' orf is_pred pred_arities))) intros; val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn; val monos' = map (to_pred [] (Context.Proof lthy)) monos; - val ({preds, intrs, elims, raw_induct, ...}, lthy1) = + val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) = Inductive.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty, coind = coind, no_elim = no_elim, no_ind = no_ind, @@ -520,14 +520,13 @@ val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *) val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct; - val eqs = [] (* TODO: define equations *) val (intrs', elims', eqs', induct, inducts, lthy4) = Inductive.declare_rules rec_name coind no_ind cnames (map fst defs) (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof lthy3) th, map fst (fst (Rule_Cases.get th)), Rule_Cases.get_constraints th)) elims) - eqs raw_induct' lthy3; + (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3; in ({intrs = intrs', elims = elims', induct = induct, inducts = inducts, raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},