# HG changeset patch
# User wenzelm
# Date 1257108147 -3600
# Node ID 8099185908a4ce6d14f5a6643c492e6d60d3e94e
# Parent  674df68d4df0c93e5634d4e95a50a95bf80c305d
Rules that characterize functional/relational specifications.

diff -r 674df68d4df0 -r 8099185908a4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Nov 01 20:59:34 2009 +0100
+++ b/src/Pure/IsaMakefile	Sun Nov 01 21:42:27 2009 +0100
@@ -68,19 +68,20 @@
   Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML		\
   Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
   Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
-  Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML		\
-  Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML		\
-  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
-  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
-  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
-  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
-  Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
-  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
-  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
-  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
-  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
-  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
-  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
+  Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML		\
+  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
+  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML		\
+  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
+  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
+  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
+  ML-Systems/use_context.ML Proof/extraction.ML				\
+  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
+  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
+  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
+  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
+  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
+  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
+  ProofGeneral/proof_general_emacs.ML					\
   ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
diff -r 674df68d4df0 -r 8099185908a4 src/Pure/Isar/spec_rules.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/spec_rules.ML	Sun Nov 01 21:42:27 2009 +0100
@@ -0,0 +1,49 @@
+(*  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.
+*)
+
+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
+end;
+
+structure Spec_Rules: SPEC_RULES =
+struct
+
+(* maintain rules *)
+
+datatype kind = Functional | Relational | Co_Relational;
+
+structure Rules = GenericDataFun
+(
+  type T = (kind * (term * thm list) list) 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);
+  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;
+
+fun add (kind, specs) = 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);
+
+fun add_global entry =
+  Context.theory_map (Rules.map (Item_Net.update entry));
+
+end;
diff -r 674df68d4df0 -r 8099185908a4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Nov 01 20:59:34 2009 +0100
+++ b/src/Pure/ROOT.ML	Sun Nov 01 21:42:27 2009 +0100
@@ -212,6 +212,7 @@
 
 (*specifications*)
 use "Isar/spec_parse.ML";
+use "Isar/spec_rules.ML";
 use "Isar/specification.ML";
 use "Isar/constdefs.ML";