added Pure/Isar/rule_context.ML;
authorwenzelm
Mon Nov 26 23:24:27 2001 +0100 (2001-11-26)
changeset 12301adf0eff5ea62
parent 12300 9fbce4042034
child 12302 87d1bddcdfe7
added Pure/Isar/rule_context.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/rule_context.ML
src/Pure/pure.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Nov 26 23:23:33 2001 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Nov 26 23:24:27 2001 +0100
     1.3 @@ -36,11 +36,11 @@
     1.4    Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML	\
     1.5    Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
     1.6    Isar/proof.ML Isar/proof_context.ML Isar/proof_data.ML		\
     1.7 -  Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML		\
     1.8 -  Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML		\
     1.9 -  ML-Systems/mlworks.ML ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML	\
    1.10 -  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML		\
    1.11 -  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    1.12 +  Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_context.ML		\
    1.13 +  Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML			\
    1.14 +  Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml-3.x.ML	\
    1.15 +  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML	\
    1.16 +  Proof/ROOT.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
    1.17    Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML	\
    1.18    Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML	\
    1.19    Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
     2.1 --- a/src/Pure/Isar/ROOT.ML	Mon Nov 26 23:23:33 2001 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Nov 26 23:24:27 2001 +0100
     2.3 @@ -17,6 +17,7 @@
     2.4  use "proof_history.ML";
     2.5  use "args.ML";
     2.6  use "attrib.ML";
     2.7 +use "rule_context.ML";
     2.8  use "net_rules.ML";
     2.9  use "induct_attrib.ML";
    2.10  use "method.ML";
    2.11 @@ -59,6 +60,7 @@
    2.12    structure ProofHistory = ProofHistory;
    2.13    structure Args = Args;
    2.14    structure Attrib = Attrib;
    2.15 +  structure RuleContext = RuleContext;
    2.16    structure Method = Method;
    2.17    structure Calculation = Calculation;
    2.18    structure Obtain = Obtain;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/rule_context.ML	Mon Nov 26 23:24:27 2001 +0100
     3.3 @@ -0,0 +1,214 @@
     3.4 +(*  Title:      Pure/Isar/rule_context.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8 +
     3.9 +Declarations of intro/elim/dest rules in Pure; see
    3.10 +Provers/classical.ML for a more specialized version.
    3.11 +
    3.12 +TODO:
    3.13 +  - del rules;
    3.14 +  - tactics;
    3.15 +  - add/del ML interface (?);
    3.16 +*)
    3.17 +
    3.18 +signature RULE_CONTEXT =
    3.19 +sig
    3.20 +  type T
    3.21 +  val empty_rules: T
    3.22 +  val print_global_rules: theory -> unit
    3.23 +  val print_local_rules: Proof.context -> unit
    3.24 +  val intro_bang_global: int option -> theory attribute
    3.25 +  val elim_bang_global: int option -> theory attribute
    3.26 +  val dest_bang_global: int option -> theory attribute
    3.27 +  val intro_global: int option -> theory attribute
    3.28 +  val elim_global: int option -> theory attribute
    3.29 +  val dest_global: int option -> theory attribute
    3.30 +  val intro_query_global: int option -> theory attribute
    3.31 +  val elim_query_global: int option -> theory attribute
    3.32 +  val dest_query_global: int option -> theory attribute
    3.33 +  val intro_bang_local: int option -> Proof.context attribute
    3.34 +  val elim_bang_local: int option -> Proof.context attribute
    3.35 +  val dest_bang_local: int option -> Proof.context attribute
    3.36 +  val intro_local: int option -> Proof.context attribute
    3.37 +  val elim_local: int option -> Proof.context attribute
    3.38 +  val dest_local: int option -> Proof.context attribute
    3.39 +  val intro_query_local: int option -> Proof.context attribute
    3.40 +  val elim_query_local: int option -> Proof.context attribute
    3.41 +  val dest_query_local: int option -> Proof.context attribute
    3.42 +  val setup: (theory -> theory) list
    3.43 +end;
    3.44 +
    3.45 +structure RuleContext: RULE_CONTEXT =
    3.46 +struct
    3.47 +
    3.48 +
    3.49 +(** rule declaration contexts **)
    3.50 +
    3.51 +(* rule kinds *)
    3.52 +
    3.53 +val intro_bangK = (0, false);
    3.54 +val elim_bangK = (0, true);
    3.55 +val introK = (1, false);
    3.56 +val elimK = (1, true);
    3.57 +val intro_queryK = (2, false);
    3.58 +val elim_queryK = (2, true);
    3.59 +
    3.60 +val kind_names =
    3.61 + [(intro_bangK, "safe introduction rules (intro!)"),
    3.62 +  (elim_bangK, "safe elimination rules (elim!)"),
    3.63 +  (introK, "introduction rules (intro)"),
    3.64 +  (elimK, "elimination rules (elim)"),
    3.65 +  (intro_queryK, "extra introduction rules (intro?)"),
    3.66 +  (elim_queryK, "extra elimination rules (elim?)")];
    3.67 +
    3.68 +val rule_kinds = map #1 kind_names;
    3.69 +val rule_indexes = distinct (map #1 rule_kinds);
    3.70 +
    3.71 +
    3.72 +(* netpairs *)
    3.73 +
    3.74 +type net = ((int * int) * (bool * thm)) Net.net;
    3.75 +
    3.76 +val empty_netpairs = replicate (length rule_indexes) (Net.empty: net, Net.empty: net);
    3.77 +
    3.78 +fun make_netpairs rules =
    3.79 +  let
    3.80 +    fun add (netpairs, (n, (w, ((i, b), th)))) =
    3.81 +      map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) netpairs;
    3.82 +    val next = ~ (length rules);
    3.83 +  in (next - 1, foldl add (empty_netpairs, next upto ~1 ~~ rules)) end;
    3.84 +
    3.85 +
    3.86 +(* rules *)
    3.87 +
    3.88 +datatype T = Rules of
    3.89 + {next: int,
    3.90 +  rules: (int * ((int * bool) * thm)) list,
    3.91 +  netpairs: (net * net) list,
    3.92 +  wrappers: ((bool * ((int -> tactic) -> int -> tactic)) * stamp) list};
    3.93 +
    3.94 +val empty_rules = Rules {next = ~1, rules = [], netpairs = empty_netpairs, wrappers = []};
    3.95 +
    3.96 +fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
    3.97 +  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
    3.98 +    Rules {next = next - 1,
    3.99 +      rules = (w, ((i, b), th)) :: rules,
   3.100 +      netpairs = map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs,
   3.101 +      wrappers = wrappers}
   3.102 +  end;
   3.103 +
   3.104 +fun print_rules prt x (Rules {rules, ...}) =
   3.105 +  let
   3.106 +    fun prt_kind (i, b) =
   3.107 +      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
   3.108 +        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None) rules);
   3.109 +  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   3.110 +
   3.111 +
   3.112 +(* theory and proof data *)
   3.113 +
   3.114 +structure GlobalRulesArgs =
   3.115 +struct
   3.116 +  val name = "Isar/rule_context";
   3.117 +  type T = T;
   3.118 +
   3.119 +  val empty = empty_rules;
   3.120 +  val copy = I;
   3.121 +  val finish = I;
   3.122 +  val prep_ext = I;
   3.123 +
   3.124 +  fun merge (Rules {rules = rules1, wrappers = wrappers1, ...},
   3.125 +      Rules {rules = rules2, wrappers = wrappers2, ...}) =
   3.126 +    let
   3.127 +      val wrappers = gen_merge_lists' eq_snd wrappers1 wrappers2;
   3.128 +      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
   3.129 +          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
   3.130 +      val next = ~ (length rules);
   3.131 +      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
   3.132 +          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
   3.133 +        (empty_netpairs, next upto ~1 ~~ rules);
   3.134 +    in Rules {next = next - 1, rules = rules, netpairs = netpairs, wrappers = wrappers} end;
   3.135 +
   3.136 +  val print = print_rules Display.pretty_thm_sg;
   3.137 +end;
   3.138 +
   3.139 +structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
   3.140 +val print_global_rules = GlobalRules.print;
   3.141 +
   3.142 +structure LocalRulesArgs =
   3.143 +struct
   3.144 +  val name = GlobalRulesArgs.name;
   3.145 +  type T = GlobalRulesArgs.T;
   3.146 +  val init = GlobalRules.get;
   3.147 +  val print = print_rules ProofContext.pretty_thm;
   3.148 +end;
   3.149 +
   3.150 +structure LocalRules = ProofDataFun(LocalRulesArgs);
   3.151 +val print_local_rules = LocalRules.print;
   3.152 +
   3.153 +
   3.154 +
   3.155 +(** attributes **)
   3.156 +
   3.157 +(* add rules *)
   3.158 +
   3.159 +local
   3.160 +
   3.161 +fun mk_att k view map_data opt_w (x, th) = (map_data (add_rule k opt_w th) x, th);
   3.162 +
   3.163 +in
   3.164 +
   3.165 +val intro_bang_global  = mk_att intro_bangK I GlobalRules.map;
   3.166 +val elim_bang_global   = mk_att elim_bangK I GlobalRules.map;
   3.167 +val dest_bang_global   = mk_att elim_bangK Tactic.make_elim GlobalRules.map;
   3.168 +val intro_global       = mk_att introK I GlobalRules.map;
   3.169 +val elim_global        = mk_att elimK I GlobalRules.map;
   3.170 +val dest_global        = mk_att elimK Tactic.make_elim GlobalRules.map;
   3.171 +val intro_query_global = mk_att intro_queryK I GlobalRules.map;
   3.172 +val elim_query_global  = mk_att elim_queryK I GlobalRules.map;
   3.173 +val dest_query_global  = mk_att elim_queryK Tactic.make_elim GlobalRules.map;
   3.174 +
   3.175 +val intro_bang_local   = mk_att intro_bangK I LocalRules.map;
   3.176 +val elim_bang_local    = mk_att elim_bangK I LocalRules.map;
   3.177 +val dest_bang_local    = mk_att elim_bangK Tactic.make_elim LocalRules.map;
   3.178 +val intro_local        = mk_att introK I LocalRules.map;
   3.179 +val elim_local         = mk_att elimK I LocalRules.map;
   3.180 +val dest_local         = mk_att elimK Tactic.make_elim LocalRules.map;
   3.181 +val intro_query_local  = mk_att intro_queryK I LocalRules.map;
   3.182 +val elim_query_local   = mk_att elim_queryK I LocalRules.map;
   3.183 +val dest_query_local   = mk_att elim_queryK Tactic.make_elim LocalRules.map;
   3.184 +
   3.185 +end;
   3.186 +
   3.187 +
   3.188 +(* concrete syntax *)
   3.189 +
   3.190 +fun add_args a b c x = Attrib.syntax
   3.191 +  (Scan.lift (Scan.option (Args.bracks Args.nat) --
   3.192 +    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
   3.193 +
   3.194 +val rule_atts =
   3.195 + [("intro",
   3.196 +   (add_args intro_bang_global intro_global intro_query_global,
   3.197 +    add_args intro_bang_local intro_local intro_query_local),
   3.198 +    "declaration of introduction rule"),
   3.199 +  ("elim",
   3.200 +   (add_args elim_bang_global elim_global elim_query_global,
   3.201 +    add_args elim_bang_local elim_local elim_query_local),
   3.202 +    "declaration of elimination rule"),
   3.203 +  ("dest",
   3.204 +   (add_args dest_bang_global dest_global dest_query_global,
   3.205 +    add_args dest_bang_local dest_local dest_query_local),
   3.206 +    "declaration of destruction rule")];
   3.207 +
   3.208 +
   3.209 +
   3.210 +(** theory setup **)
   3.211 +
   3.212 +val setup =
   3.213 + [GlobalRules.init, LocalRules.init
   3.214 +  (*FIXME Attrib.add_attributes rule_atts*)];
   3.215 +
   3.216 +
   3.217 +end;
     4.1 --- a/src/Pure/pure.ML	Mon Nov 26 23:23:33 2001 +0100
     4.2 +++ b/src/Pure/pure.ML	Mon Nov 26 23:24:27 2001 +0100
     4.3 @@ -13,6 +13,7 @@
     4.4      ProofContext.setup @
     4.5      Locale.setup @
     4.6      Attrib.setup @
     4.7 +    RuleContext.setup @
     4.8      InductAttrib.setup @
     4.9      Method.setup @
    4.10      Calculation.setup @