# HG changeset patch
# User wenzelm
# Date 1006813467 -3600
# Node ID adf0eff5ea6207276104db6c6ec0d5ed76cd6447
# Parent  9fbce4042034e1ef559a269f247e060168de525d
added Pure/Isar/rule_context.ML;

diff -r 9fbce4042034 -r adf0eff5ea62 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Nov 26 23:23:33 2001 +0100
+++ b/src/Pure/IsaMakefile	Mon Nov 26 23:24:27 2001 +0100
@@ -36,11 +36,11 @@
   Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML	\
   Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
   Isar/proof.ML Isar/proof_context.ML Isar/proof_data.ML		\
-  Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML		\
-  Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML		\
-  ML-Systems/mlworks.ML ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML	\
-  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML		\
-  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
+  Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_context.ML		\
+  Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML			\
+  Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml-3.x.ML	\
+  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML	\
+  Proof/ROOT.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
   Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML	\
   Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML	\
   Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
diff -r 9fbce4042034 -r adf0eff5ea62 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Nov 26 23:23:33 2001 +0100
+++ b/src/Pure/Isar/ROOT.ML	Mon Nov 26 23:24:27 2001 +0100
@@ -17,6 +17,7 @@
 use "proof_history.ML";
 use "args.ML";
 use "attrib.ML";
+use "rule_context.ML";
 use "net_rules.ML";
 use "induct_attrib.ML";
 use "method.ML";
@@ -59,6 +60,7 @@
   structure ProofHistory = ProofHistory;
   structure Args = Args;
   structure Attrib = Attrib;
+  structure RuleContext = RuleContext;
   structure Method = Method;
   structure Calculation = Calculation;
   structure Obtain = Obtain;
diff -r 9fbce4042034 -r adf0eff5ea62 src/Pure/Isar/rule_context.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/rule_context.ML	Mon Nov 26 23:24:27 2001 +0100
@@ -0,0 +1,214 @@
+(*  Title:      Pure/Isar/rule_context.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Declarations of intro/elim/dest rules in Pure; see
+Provers/classical.ML for a more specialized version.
+
+TODO:
+  - del rules;
+  - tactics;
+  - add/del ML interface (?);
+*)
+
+signature RULE_CONTEXT =
+sig
+  type T
+  val empty_rules: T
+  val print_global_rules: theory -> unit
+  val print_local_rules: Proof.context -> unit
+  val intro_bang_global: int option -> theory attribute
+  val elim_bang_global: int option -> theory attribute
+  val dest_bang_global: int option -> theory attribute
+  val intro_global: int option -> theory attribute
+  val elim_global: int option -> theory attribute
+  val dest_global: int option -> theory attribute
+  val intro_query_global: int option -> theory attribute
+  val elim_query_global: int option -> theory attribute
+  val dest_query_global: int option -> theory attribute
+  val intro_bang_local: int option -> Proof.context attribute
+  val elim_bang_local: int option -> Proof.context attribute
+  val dest_bang_local: int option -> Proof.context attribute
+  val intro_local: int option -> Proof.context attribute
+  val elim_local: int option -> Proof.context attribute
+  val dest_local: int option -> Proof.context attribute
+  val intro_query_local: int option -> Proof.context attribute
+  val elim_query_local: int option -> Proof.context attribute
+  val dest_query_local: int option -> Proof.context attribute
+  val setup: (theory -> theory) list
+end;
+
+structure RuleContext: RULE_CONTEXT =
+struct
+
+
+(** rule declaration contexts **)
+
+(* rule kinds *)
+
+val intro_bangK = (0, false);
+val elim_bangK = (0, true);
+val introK = (1, false);
+val elimK = (1, true);
+val intro_queryK = (2, false);
+val elim_queryK = (2, true);
+
+val kind_names =
+ [(intro_bangK, "safe introduction rules (intro!)"),
+  (elim_bangK, "safe elimination rules (elim!)"),
+  (introK, "introduction rules (intro)"),
+  (elimK, "elimination rules (elim)"),
+  (intro_queryK, "extra introduction rules (intro?)"),
+  (elim_queryK, "extra elimination rules (elim?)")];
+
+val rule_kinds = map #1 kind_names;
+val rule_indexes = distinct (map #1 rule_kinds);
+
+
+(* netpairs *)
+
+type net = ((int * int) * (bool * thm)) Net.net;
+
+val empty_netpairs = replicate (length rule_indexes) (Net.empty: net, Net.empty: net);
+
+fun make_netpairs rules =
+  let
+    fun add (netpairs, (n, (w, ((i, b), th)))) =
+      map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) netpairs;
+    val next = ~ (length rules);
+  in (next - 1, foldl add (empty_netpairs, next upto ~1 ~~ rules)) end;
+
+
+(* rules *)
+
+datatype T = Rules of
+ {next: int,
+  rules: (int * ((int * bool) * thm)) list,
+  netpairs: (net * net) list,
+  wrappers: ((bool * ((int -> tactic) -> int -> tactic)) * stamp) list};
+
+val empty_rules = Rules {next = ~1, rules = [], netpairs = empty_netpairs, wrappers = []};
+
+fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
+  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
+    Rules {next = next - 1,
+      rules = (w, ((i, b), th)) :: rules,
+      netpairs = map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs,
+      wrappers = wrappers}
+  end;
+
+fun print_rules prt x (Rules {rules, ...}) =
+  let
+    fun prt_kind (i, b) =
+      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
+        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None) rules);
+  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+
+
+(* theory and proof data *)
+
+structure GlobalRulesArgs =
+struct
+  val name = "Isar/rule_context";
+  type T = T;
+
+  val empty = empty_rules;
+  val copy = I;
+  val finish = I;
+  val prep_ext = I;
+
+  fun merge (Rules {rules = rules1, wrappers = wrappers1, ...},
+      Rules {rules = rules2, wrappers = wrappers2, ...}) =
+    let
+      val wrappers = gen_merge_lists' eq_snd wrappers1 wrappers2;
+      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
+          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
+      val next = ~ (length rules);
+      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
+          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
+        (empty_netpairs, next upto ~1 ~~ rules);
+    in Rules {next = next - 1, rules = rules, netpairs = netpairs, wrappers = wrappers} end;
+
+  val print = print_rules Display.pretty_thm_sg;
+end;
+
+structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
+val print_global_rules = GlobalRules.print;
+
+structure LocalRulesArgs =
+struct
+  val name = GlobalRulesArgs.name;
+  type T = GlobalRulesArgs.T;
+  val init = GlobalRules.get;
+  val print = print_rules ProofContext.pretty_thm;
+end;
+
+structure LocalRules = ProofDataFun(LocalRulesArgs);
+val print_local_rules = LocalRules.print;
+
+
+
+(** attributes **)
+
+(* add rules *)
+
+local
+
+fun mk_att k view map_data opt_w (x, th) = (map_data (add_rule k opt_w th) x, th);
+
+in
+
+val intro_bang_global  = mk_att intro_bangK I GlobalRules.map;
+val elim_bang_global   = mk_att elim_bangK I GlobalRules.map;
+val dest_bang_global   = mk_att elim_bangK Tactic.make_elim GlobalRules.map;
+val intro_global       = mk_att introK I GlobalRules.map;
+val elim_global        = mk_att elimK I GlobalRules.map;
+val dest_global        = mk_att elimK Tactic.make_elim GlobalRules.map;
+val intro_query_global = mk_att intro_queryK I GlobalRules.map;
+val elim_query_global  = mk_att elim_queryK I GlobalRules.map;
+val dest_query_global  = mk_att elim_queryK Tactic.make_elim GlobalRules.map;
+
+val intro_bang_local   = mk_att intro_bangK I LocalRules.map;
+val elim_bang_local    = mk_att elim_bangK I LocalRules.map;
+val dest_bang_local    = mk_att elim_bangK Tactic.make_elim LocalRules.map;
+val intro_local        = mk_att introK I LocalRules.map;
+val elim_local         = mk_att elimK I LocalRules.map;
+val dest_local         = mk_att elimK Tactic.make_elim LocalRules.map;
+val intro_query_local  = mk_att intro_queryK I LocalRules.map;
+val elim_query_local   = mk_att elim_queryK I LocalRules.map;
+val dest_query_local   = mk_att elim_queryK Tactic.make_elim LocalRules.map;
+
+end;
+
+
+(* concrete syntax *)
+
+fun add_args a b c x = Attrib.syntax
+  (Scan.lift (Scan.option (Args.bracks Args.nat) --
+    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
+
+val rule_atts =
+ [("intro",
+   (add_args intro_bang_global intro_global intro_query_global,
+    add_args intro_bang_local intro_local intro_query_local),
+    "declaration of introduction rule"),
+  ("elim",
+   (add_args elim_bang_global elim_global elim_query_global,
+    add_args elim_bang_local elim_local elim_query_local),
+    "declaration of elimination rule"),
+  ("dest",
+   (add_args dest_bang_global dest_global dest_query_global,
+    add_args dest_bang_local dest_local dest_query_local),
+    "declaration of destruction rule")];
+
+
+
+(** theory setup **)
+
+val setup =
+ [GlobalRules.init, LocalRules.init
+  (*FIXME Attrib.add_attributes rule_atts*)];
+
+
+end;
diff -r 9fbce4042034 -r adf0eff5ea62 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Mon Nov 26 23:23:33 2001 +0100
+++ b/src/Pure/pure.ML	Mon Nov 26 23:24:27 2001 +0100
@@ -13,6 +13,7 @@
     ProofContext.setup @
     Locale.setup @
     Attrib.setup @
+    RuleContext.setup @
     InductAttrib.setup @
     Method.setup @
     Calculation.setup @