# HG changeset patch # User wenzelm # Date 1257450105 -3600 # Node ID 485fd398dd33b7a803984ce19b23831b9003b120 # Parent fe551dc9d4bd86fc3be69adbdd23e556b3ce2987 misc tuning and clarification; diff -r fe551dc9d4bd -r 485fd398dd33 src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Thu Nov 05 20:40:16 2009 +0100 +++ b/src/Pure/Isar/spec_rules.ML Thu Nov 05 20:41:45 2009 +0100 @@ -1,18 +1,19 @@ (* Title: Pure/Isar/spec_rules.ML Author: Makarius -Rules that characterize functional/relational specifications. NB: In -the face of arbitrary morphisms, the original shape of specifications -may get transformed almost arbitrarily. +Rules that characterize specifications, with rough classification. +NB: In the face of arbitrary morphisms, the original shape of +specifications may get lost. *) signature SPEC_RULES = sig - datatype kind = Functional | Relational | Co_Relational - val dest: Proof.context -> (kind * (term * thm list) list) list - val dest_global: theory -> (kind * (term * thm list) list) list - val add: kind * (term * thm list) list -> local_theory -> local_theory - val add_global: kind * (term * thm list) list -> theory -> theory + datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive + type spec = rough_classification * (term list * thm list) + val get: Proof.context -> spec list + val get_global: theory -> spec list + val add: rough_classification -> term list * thm list -> local_theory -> local_theory + val add_global: rough_classification -> term list * thm list -> theory -> theory end; structure Spec_Rules: SPEC_RULES = @@ -20,30 +21,34 @@ (* maintain rules *) -datatype kind = Functional | Relational | Co_Relational; +datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive; +type spec = rough_classification * (term list * thm list); structure Rules = GenericDataFun ( - type T = (kind * (term * thm list) list) Item_Net.T; + type T = spec Item_Net.T; val empty : T = Item_Net.init - (fn ((k1, spec1), (k2, spec2)) => k1 = k2 andalso - eq_list (fn ((t1, ths1), (t2, ths2)) => - t1 aconv t2 andalso eq_list Thm.eq_thm_prop (ths1, ths2)) (spec1, spec2)) - (map #1 o #2); + (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) => + class1 = class2 andalso + eq_list (op aconv) (ts1, ts2) andalso + eq_list Thm.eq_thm_prop (ths1, ths2)) + (#1 o #2); val extend = I; fun merge _ = Item_Net.merge; ); -val dest = Item_Net.content o Rules.get o Context.Proof; -val dest_global = Item_Net.content o Rules.get o Context.Theory; +val get = Item_Net.content o Rules.get o Context.Proof; +val get_global = Item_Net.content o Rules.get o Context.Theory; -fun add (kind, specs) = LocalTheory.declaration +fun add class (ts, ths) = LocalTheory.declaration (fn phi => - let val specs' = map (fn (t, ths) => (Morphism.term phi t, Morphism.fact phi ths)) specs; - in Rules.map (Item_Net.update (kind, specs')) end); + let + val ts' = map (Morphism.term phi) ts; + val ths' = map (Morphism.thm phi) ths; + in Rules.map (Item_Net.update (class, (ts', ths'))) end); -fun add_global entry = - Context.theory_map (Rules.map (Item_Net.update entry)); +fun add_global class spec = + Context.theory_map (Rules.map (Item_Net.update (class, spec))); end;