renamed rule_context.ML to context_rules.ML;
authorwenzelm
Mon Dec 03 21:31:55 2001 +0100 (2001-12-03)
changeset 123505fad0e7129c3
parent 12349 94e812f9683e
child 12351 54aef8e41437
renamed rule_context.ML to context_rules.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/rule_context.ML
src/Pure/pure.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Dec 03 21:03:06 2001 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Dec 03 21:31:55 2001 +0100
     1.3 @@ -31,16 +31,17 @@
     1.4    Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML	\
     1.5    Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
     1.6    Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML			\
     1.7 -  Isar/induct_attrib.ML Isar/isar.ML Isar/isar_cmd.ML			\
     1.8 -  Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML	\
     1.9 -  Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML	\
    1.10 -  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    1.11 -  Isar/proof.ML Isar/proof_context.ML Isar/proof_data.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 +  Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
    1.18 +  Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML			\
    1.19 +  Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
    1.20 +  Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML			\
    1.21 +  Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML		\
    1.22 +  Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML	\
    1.23 +  Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML			\
    1.24 +  Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML		\
    1.25 +  ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML				\
    1.26 +  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML		\
    1.27 +  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    1.28    Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML	\
    1.29    Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML	\
    1.30    Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
    1.31 @@ -53,6 +54,7 @@
    1.32    pattern.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML		\
    1.33    sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML	\
    1.34    thm.ML type.ML type_infer.ML unify.ML
    1.35 +
    1.36  	@./mk
    1.37  
    1.38  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Mon Dec 03 21:03:06 2001 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Dec 03 21:31:55 2001 +0100
     2.3 @@ -17,7 +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 "context_rules.ML";
     2.9  use "net_rules.ML";
    2.10  use "induct_attrib.ML";
    2.11  use "method.ML";
    2.12 @@ -60,7 +60,7 @@
    2.13    structure ProofHistory = ProofHistory;
    2.14    structure Args = Args;
    2.15    structure Attrib = Attrib;
    2.16 -  structure RuleContext = RuleContext;
    2.17 +  structure ContextRules = ContextRules;
    2.18    structure Method = Method;
    2.19    structure Calculation = Calculation;
    2.20    structure Obtain = Obtain;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Mon Dec 03 21:31:55 2001 +0100
     3.3 @@ -0,0 +1,260 @@
     3.4 +(*  Title:      Pure/Isar/context_rules.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 of the same idea.
    3.11 +*)
    3.12 +
    3.13 +signature CONTEXT_RULES =
    3.14 +sig
    3.15 +  type netpair
    3.16 +  type T
    3.17 +  val netpair_bang: Proof.context -> netpair
    3.18 +  val netpair: Proof.context -> netpair
    3.19 +  val netpairs: Proof.context -> netpair list
    3.20 +  val orderlist: ((int * int) * 'a) list -> 'a list
    3.21 +  val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
    3.22 +  val print_global_rules: theory -> unit
    3.23 +  val print_local_rules: Proof.context -> unit
    3.24 +  val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    3.25 +  val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    3.26 +  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    3.27 +  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
    3.28 +  val intro_bang_global: int option -> theory attribute
    3.29 +  val elim_bang_global: int option -> theory attribute
    3.30 +  val dest_bang_global: int option -> theory attribute
    3.31 +  val intro_global: int option -> theory attribute
    3.32 +  val elim_global: int option -> theory attribute
    3.33 +  val dest_global: int option -> theory attribute
    3.34 +  val intro_query_global: int option -> theory attribute
    3.35 +  val elim_query_global: int option -> theory attribute
    3.36 +  val dest_query_global: int option -> theory attribute
    3.37 +  val rule_del_global: theory attribute
    3.38 +  val intro_bang_local: int option -> Proof.context attribute
    3.39 +  val elim_bang_local: int option -> Proof.context attribute
    3.40 +  val dest_bang_local: int option -> Proof.context attribute
    3.41 +  val intro_local: int option -> Proof.context attribute
    3.42 +  val elim_local: int option -> Proof.context attribute
    3.43 +  val dest_local: int option -> Proof.context attribute
    3.44 +  val intro_query_local: int option -> Proof.context attribute
    3.45 +  val elim_query_local: int option -> Proof.context attribute
    3.46 +  val dest_query_local: int option -> Proof.context attribute
    3.47 +  val rule_del_local: Proof.context attribute
    3.48 +  val setup: (theory -> theory) list
    3.49 +end;
    3.50 +
    3.51 +structure ContextRules: CONTEXT_RULES =
    3.52 +struct
    3.53 +
    3.54 +
    3.55 +(** rule declaration contexts **)
    3.56 +
    3.57 +(* rule kinds *)
    3.58 +
    3.59 +val intro_bangK = (0, false);
    3.60 +val elim_bangK = (0, true);
    3.61 +val introK = (1, false);
    3.62 +val elimK = (1, true);
    3.63 +val intro_queryK = (2, false);
    3.64 +val elim_queryK = (2, true);
    3.65 +
    3.66 +val kind_names =
    3.67 + [(intro_bangK, "safe introduction rules (intro!)"),
    3.68 +  (elim_bangK, "safe elimination rules (elim!)"),
    3.69 +  (introK, "introduction rules (intro)"),
    3.70 +  (elimK, "elimination rules (elim)"),
    3.71 +  (intro_queryK, "extra introduction rules (intro?)"),
    3.72 +  (elim_queryK, "extra elimination rules (elim?)")];
    3.73 +
    3.74 +val rule_kinds = map #1 kind_names;
    3.75 +val rule_indexes = distinct (map #1 rule_kinds);
    3.76 +
    3.77 +
    3.78 +(* raw data *)
    3.79 +
    3.80 +type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
    3.81 +val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
    3.82 +
    3.83 +datatype T = Rules of
    3.84 + {next: int,
    3.85 +  rules: (int * ((int * bool) * thm)) list,
    3.86 +  netpairs: netpair list,
    3.87 +  wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
    3.88 +    (((int -> tactic) -> int -> tactic) * stamp) list};
    3.89 +
    3.90 +fun make_rules next rules netpairs wrappers =
    3.91 +  Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
    3.92 +
    3.93 +fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
    3.94 +  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
    3.95 +    make_rules (next - 1) ((w, ((i, b), th)) :: rules)
    3.96 +      (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
    3.97 +  end;
    3.98 +
    3.99 +fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
   3.100 +  let
   3.101 +    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
   3.102 +    fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
   3.103 +  in
   3.104 +    if not (exists eq_th rules) then rs
   3.105 +    else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   3.106 +  end;
   3.107 +
   3.108 +fun print_rules prt x (Rules {rules, ...}) =
   3.109 +  let
   3.110 +    fun prt_kind (i, b) =
   3.111 +      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
   3.112 +        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
   3.113 +          (sort (int_ord o pairself fst) rules));
   3.114 +  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   3.115 +
   3.116 +
   3.117 +(* theory and proof data *)
   3.118 +
   3.119 +structure GlobalRulesArgs =
   3.120 +struct
   3.121 +  val name = "Isar/rule_context";
   3.122 +  type T = T;
   3.123 +
   3.124 +  val empty = make_rules ~1 [] empty_netpairs ([], []);
   3.125 +  val copy = I;
   3.126 +  val prep_ext = I;
   3.127 +
   3.128 +  fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
   3.129 +      Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
   3.130 +    let
   3.131 +      val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
   3.132 +      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
   3.133 +          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
   3.134 +      val next = ~ (length rules);
   3.135 +      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
   3.136 +          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
   3.137 +        (empty_netpairs, next upto ~1 ~~ rules);
   3.138 +    in make_rules (next - 1) rules netpairs wrappers end;
   3.139 +
   3.140 +  val print = print_rules Display.pretty_thm_sg;
   3.141 +end;
   3.142 +
   3.143 +structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
   3.144 +val print_global_rules = GlobalRules.print;
   3.145 +
   3.146 +structure LocalRulesArgs =
   3.147 +struct
   3.148 +  val name = GlobalRulesArgs.name;
   3.149 +  type T = GlobalRulesArgs.T;
   3.150 +  val init = GlobalRules.get;
   3.151 +  val print = print_rules ProofContext.pretty_thm;
   3.152 +end;
   3.153 +
   3.154 +structure LocalRules = ProofDataFun(LocalRulesArgs);
   3.155 +val print_local_rules = LocalRules.print;
   3.156 +
   3.157 +
   3.158 +(* access data *)
   3.159 +
   3.160 +fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
   3.161 +val netpair_bang = hd o netpairs;
   3.162 +val netpair = hd o tl o netpairs;
   3.163 +
   3.164 +
   3.165 +fun untaglist [] = []
   3.166 +  | untaglist [(k : int * int, x)] = [x]
   3.167 +  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
   3.168 +      if k = k' then untaglist rest
   3.169 +      else x :: untaglist rest;
   3.170 +
   3.171 +fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
   3.172 +fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
   3.173 +
   3.174 +
   3.175 +fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   3.176 +  make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
   3.177 +
   3.178 +val addSWrapper = gen_add_wrapper Library.apfst;
   3.179 +val addWrapper = gen_add_wrapper Library.apsnd;
   3.180 +
   3.181 +
   3.182 +fun gen_wrap which ctxt =
   3.183 +  let val Rules {wrappers, ...} = LocalRules.get ctxt
   3.184 +  in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
   3.185 +
   3.186 +val Swrap = gen_wrap #1;
   3.187 +val wrap = gen_wrap #2;
   3.188 +
   3.189 +
   3.190 +
   3.191 +(** attributes **)
   3.192 +
   3.193 +(* add and del rules *)
   3.194 +
   3.195 +local
   3.196 +
   3.197 +fun del map_data (x, th) =
   3.198 +  (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
   3.199 +
   3.200 +fun add k view map_data opt_w =
   3.201 +  (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
   3.202 +
   3.203 +in
   3.204 +
   3.205 +val intro_bang_global  = add intro_bangK I GlobalRules.map;
   3.206 +val elim_bang_global   = add elim_bangK I GlobalRules.map;
   3.207 +val dest_bang_global   = add elim_bangK Tactic.make_elim GlobalRules.map;
   3.208 +val intro_global       = add introK I GlobalRules.map;
   3.209 +val elim_global        = add elimK I GlobalRules.map;
   3.210 +val dest_global        = add elimK Tactic.make_elim GlobalRules.map;
   3.211 +val intro_query_global = add intro_queryK I GlobalRules.map;
   3.212 +val elim_query_global  = add elim_queryK I GlobalRules.map;
   3.213 +val dest_query_global  = add elim_queryK Tactic.make_elim GlobalRules.map;
   3.214 +val rule_del_global    = del GlobalRules.map;
   3.215 +
   3.216 +val intro_bang_local   = add intro_bangK I LocalRules.map;
   3.217 +val elim_bang_local    = add elim_bangK I LocalRules.map;
   3.218 +val dest_bang_local    = add elim_bangK Tactic.make_elim LocalRules.map;
   3.219 +val intro_local        = add introK I LocalRules.map;
   3.220 +val elim_local         = add elimK I LocalRules.map;
   3.221 +val dest_local         = add elimK Tactic.make_elim LocalRules.map;
   3.222 +val intro_query_local  = add intro_queryK I LocalRules.map;
   3.223 +val elim_query_local   = add elim_queryK I LocalRules.map;
   3.224 +val dest_query_local   = add elim_queryK Tactic.make_elim LocalRules.map;
   3.225 +val rule_del_local     = del LocalRules.map;
   3.226 +
   3.227 +end;
   3.228 +
   3.229 +
   3.230 +(* concrete syntax *)
   3.231 +
   3.232 +fun add_args a b c x = Attrib.syntax
   3.233 +  (Scan.lift (Scan.option Args.nat --
   3.234 +    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
   3.235 +
   3.236 +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
   3.237 +
   3.238 +
   3.239 +val rule_atts =
   3.240 + [("intro",
   3.241 +   (add_args intro_bang_global intro_global intro_query_global,
   3.242 +    add_args intro_bang_local intro_local intro_query_local),
   3.243 +    "declaration of introduction rule"),
   3.244 +  ("elim",
   3.245 +   (add_args elim_bang_global elim_global elim_query_global,
   3.246 +    add_args elim_bang_local elim_local elim_query_local),
   3.247 +    "declaration of elimination rule"),
   3.248 +  ("dest",
   3.249 +   (add_args dest_bang_global dest_global dest_query_global,
   3.250 +    add_args dest_bang_local dest_local dest_query_local),
   3.251 +    "declaration of destruction rule"),
   3.252 +  ("rule", (del_args rule_del_global, del_args rule_del_local),
   3.253 +    "remove declaration of intro/elim/dest rule")];
   3.254 +
   3.255 +
   3.256 +
   3.257 +(** theory setup **)
   3.258 +
   3.259 +val setup =
   3.260 + [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
   3.261 +
   3.262 +
   3.263 +end;
     4.1 --- a/src/Pure/Isar/method.ML	Mon Dec 03 21:03:06 2001 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Mon Dec 03 21:31:55 2001 +0100
     4.3 @@ -36,7 +36,6 @@
     4.4    val fold: thm list -> Proof.method
     4.5    val multi_resolve: thm list -> thm -> thm Seq.seq
     4.6    val multi_resolves: thm list -> thm list -> thm Seq.seq
     4.7 -  val debug_rules: bool ref
     4.8    val rules_tac: Proof.context -> int option -> int -> tactic
     4.9    val rule_tac: thm list -> thm list -> int -> tactic
    4.10    val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
    4.11 @@ -217,15 +216,18 @@
    4.12    length s1 = length s2 andalso
    4.13    gen_subset e (s1, s2) andalso gen_subset e (s2, s1);
    4.14  
    4.15 -val bires_tac = Tactic.biresolution_from_nets_tac RuleContext.orderlist;
    4.16 +val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    4.17  
    4.18  fun safe_step_tac ctxt =
    4.19 -  RuleContext.Swrap ctxt (eq_assume_tac ORELSE' bires_tac true (RuleContext.Snetpair ctxt));
    4.20 +  ContextRules.Swrap ctxt
    4.21 +   (eq_assume_tac ORELSE'
    4.22 +    bires_tac true (ContextRules.netpair_bang ctxt));
    4.23  
    4.24  fun unsafe_step_tac ctxt =
    4.25 -  RuleContext.wrap ctxt (assume_tac APPEND'
    4.26 -    bires_tac false (RuleContext.Snetpair ctxt) APPEND'
    4.27 -    bires_tac false (RuleContext.netpair ctxt));
    4.28 +  ContextRules.wrap ctxt
    4.29 +   (assume_tac APPEND'
    4.30 +    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
    4.31 +    bires_tac false (ContextRules.netpair ctxt));
    4.32  
    4.33  fun step_tac ctxt i =
    4.34    REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    4.35 @@ -243,11 +245,7 @@
    4.36  
    4.37  in
    4.38  
    4.39 -val debug_rules = ref false;
    4.40 -
    4.41 -fun rules_tac ctxt opt_lim =
    4.42 - (conditional (! debug_rules) (fn () => RuleContext.print_local_rules ctxt);
    4.43 -  DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4);
    4.44 +fun rules_tac ctxt opt_lim = DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4;
    4.45  
    4.46  end;
    4.47  
    4.48 @@ -256,8 +254,8 @@
    4.49  
    4.50  local
    4.51  
    4.52 -fun may_unify t nets = RuleContext.orderlist_no_weight
    4.53 -  (flat (map (fn net => Net.unify_term net t) nets));
    4.54 +fun may_unify t nets =
    4.55 +  flat (map (ContextRules.orderlist_no_weight o (fn net => Net.unify_term net t)) nets);
    4.56  
    4.57  fun find_erules [] = K []
    4.58    | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
    4.59 @@ -274,7 +272,7 @@
    4.60  
    4.61  fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
    4.62    let
    4.63 -    val netpairs = RuleContext.netpairs ctxt;
    4.64 +    val netpairs = ContextRules.netpairs ctxt;
    4.65      val rules =
    4.66        if not (null arg_rules) then arg_rules
    4.67        else map #2 (find_erules facts (map #2 netpairs) @ find_rules goal (map #1 netpairs));
    4.68 @@ -505,23 +503,23 @@
    4.69      >> (pair (I: Proof.context -> Proof.context) o att);
    4.70  
    4.71  val rules_modifiers =
    4.72 - [modifier destN Args.query_colon Args.query RuleContext.dest_query_local,
    4.73 -  modifier destN Args.bang_colon Args.bang RuleContext.dest_bang_local,
    4.74 -  modifier destN Args.colon (Scan.succeed ()) RuleContext.dest_local,
    4.75 -  modifier elimN Args.query_colon Args.query RuleContext.elim_query_local,
    4.76 -  modifier elimN Args.bang_colon Args.bang RuleContext.elim_bang_local,
    4.77 -  modifier elimN Args.colon (Scan.succeed ()) RuleContext.elim_local,
    4.78 -  modifier introN Args.query_colon Args.query RuleContext.intro_query_local,
    4.79 -  modifier introN Args.bang_colon Args.bang RuleContext.intro_bang_local,
    4.80 -  modifier introN Args.colon (Scan.succeed ()) RuleContext.intro_local,
    4.81 -  Args.del -- Args.colon >> K (I, RuleContext.rule_del_local)];
    4.82 + [modifier destN Args.query_colon Args.query ContextRules.dest_query_local,
    4.83 +  modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
    4.84 +  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local,
    4.85 +  modifier elimN Args.query_colon Args.query ContextRules.elim_query_local,
    4.86 +  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local,
    4.87 +  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local,
    4.88 +  modifier introN Args.query_colon Args.query ContextRules.intro_query_local,
    4.89 +  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local,
    4.90 +  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local,
    4.91 +  Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)];
    4.92  
    4.93  in
    4.94  
    4.95  fun rules_args m = bang_sectioned_args' rules_modifiers (Scan.lift (Scan.option Args.nat)) m;
    4.96  
    4.97  fun rules_meth n prems ctxt = METHOD (fn facts =>
    4.98 -  HEADGOAL (insert_tac (prems @ facts) THEN' rules_tac ctxt n));
    4.99 +  HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' rules_tac ctxt n));
   4.100  
   4.101  end;
   4.102  
   4.103 @@ -672,7 +670,7 @@
   4.104  
   4.105  val setup =
   4.106   [MethodsData.init, add_methods pure_methods,
   4.107 -  (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [RuleContext.intro_query_global None])])];
   4.108 +  (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [ContextRules.intro_query_global None])])];
   4.109  
   4.110  
   4.111  end;
     5.1 --- a/src/Pure/Isar/obtain.ML	Mon Dec 03 21:03:06 2001 +0100
     5.2 +++ b/src/Pure/Isar/obtain.ML	Mon Dec 03 21:31:55 2001 +0100
     5.3 @@ -107,7 +107,7 @@
     5.4      |> Proof.enter_forward
     5.5      |> Proof.begin_block
     5.6      |> Proof.fix_i [([thesisN], None)]
     5.7 -    |> Proof.assume_i [((thatN, [RuleContext.intro_query_local None]), [(that_prop, ([], []))])]
     5.8 +    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
     5.9      |> (fn state' =>
    5.10        state'
    5.11        |> Proof.from_facts chain_facts
     6.1 --- a/src/Pure/Isar/rule_context.ML	Mon Dec 03 21:03:06 2001 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,259 +0,0 @@
     6.4 -(*  Title:      Pure/Isar/rule_context.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     6.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.8 -
     6.9 -Declarations of intro/elim/dest rules in Pure; see
    6.10 -Provers/classical.ML for a more specialized version.
    6.11 -*)
    6.12 -
    6.13 -signature RULE_CONTEXT =
    6.14 -sig
    6.15 -  type netpair
    6.16 -  type T
    6.17 -  val Snetpair: Proof.context -> netpair
    6.18 -  val netpair: Proof.context -> netpair
    6.19 -  val netpairs: Proof.context -> netpair list
    6.20 -  val orderlist: ((int * int) * 'a) list -> 'a list
    6.21 -  val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
    6.22 -  val print_global_rules: theory -> unit
    6.23 -  val print_local_rules: Proof.context -> unit
    6.24 -  val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    6.25 -  val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    6.26 -  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    6.27 -  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
    6.28 -  val intro_bang_global: int option -> theory attribute
    6.29 -  val elim_bang_global: int option -> theory attribute
    6.30 -  val dest_bang_global: int option -> theory attribute
    6.31 -  val intro_global: int option -> theory attribute
    6.32 -  val elim_global: int option -> theory attribute
    6.33 -  val dest_global: int option -> theory attribute
    6.34 -  val intro_query_global: int option -> theory attribute
    6.35 -  val elim_query_global: int option -> theory attribute
    6.36 -  val dest_query_global: int option -> theory attribute
    6.37 -  val rule_del_global: theory attribute
    6.38 -  val intro_bang_local: int option -> Proof.context attribute
    6.39 -  val elim_bang_local: int option -> Proof.context attribute
    6.40 -  val dest_bang_local: int option -> Proof.context attribute
    6.41 -  val intro_local: int option -> Proof.context attribute
    6.42 -  val elim_local: int option -> Proof.context attribute
    6.43 -  val dest_local: int option -> Proof.context attribute
    6.44 -  val intro_query_local: int option -> Proof.context attribute
    6.45 -  val elim_query_local: int option -> Proof.context attribute
    6.46 -  val dest_query_local: int option -> Proof.context attribute
    6.47 -  val rule_del_local: Proof.context attribute
    6.48 -  val setup: (theory -> theory) list
    6.49 -end;
    6.50 -
    6.51 -structure RuleContext: RULE_CONTEXT =
    6.52 -struct
    6.53 -
    6.54 -
    6.55 -(** rule declaration contexts **)
    6.56 -
    6.57 -(* rule kinds *)
    6.58 -
    6.59 -val intro_bangK = (0, false);
    6.60 -val elim_bangK = (0, true);
    6.61 -val introK = (1, false);
    6.62 -val elimK = (1, true);
    6.63 -val intro_queryK = (2, false);
    6.64 -val elim_queryK = (2, true);
    6.65 -
    6.66 -val kind_names =
    6.67 - [(intro_bangK, "safe introduction rules (intro!)"),
    6.68 -  (elim_bangK, "safe elimination rules (elim!)"),
    6.69 -  (introK, "introduction rules (intro)"),
    6.70 -  (elimK, "elimination rules (elim)"),
    6.71 -  (intro_queryK, "extra introduction rules (intro?)"),
    6.72 -  (elim_queryK, "extra elimination rules (elim?)")];
    6.73 -
    6.74 -val rule_kinds = map #1 kind_names;
    6.75 -val rule_indexes = distinct (map #1 rule_kinds);
    6.76 -
    6.77 -
    6.78 -(* raw data *)
    6.79 -
    6.80 -type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
    6.81 -val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
    6.82 -
    6.83 -datatype T = Rules of
    6.84 - {next: int,
    6.85 -  rules: (int * ((int * bool) * thm)) list,
    6.86 -  netpairs: netpair list,
    6.87 -  wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
    6.88 -    (((int -> tactic) -> int -> tactic) * stamp) list};
    6.89 -
    6.90 -fun make_rules next rules netpairs wrappers =
    6.91 -  Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
    6.92 -
    6.93 -fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
    6.94 -  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
    6.95 -    make_rules (next - 1) ((w, ((i, b), th)) :: rules)
    6.96 -      (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
    6.97 -  end;
    6.98 -
    6.99 -fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
   6.100 -  let
   6.101 -    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
   6.102 -    fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
   6.103 -  in
   6.104 -    if not (exists eq_th rules) then rs
   6.105 -    else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   6.106 -  end;
   6.107 -
   6.108 -fun print_rules prt x (Rules {rules, ...}) =
   6.109 -  let
   6.110 -    fun prt_kind (i, b) =
   6.111 -      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
   6.112 -        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
   6.113 -          (sort (int_ord o pairself fst) rules));
   6.114 -  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   6.115 -
   6.116 -
   6.117 -(* theory and proof data *)
   6.118 -
   6.119 -structure GlobalRulesArgs =
   6.120 -struct
   6.121 -  val name = "Isar/rule_context";
   6.122 -  type T = T;
   6.123 -
   6.124 -  val empty = make_rules ~1 [] empty_netpairs ([], []);
   6.125 -  val copy = I;
   6.126 -  val prep_ext = I;
   6.127 -
   6.128 -  fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
   6.129 -      Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
   6.130 -    let
   6.131 -      val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
   6.132 -      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
   6.133 -          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
   6.134 -      val next = ~ (length rules);
   6.135 -      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
   6.136 -          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
   6.137 -        (empty_netpairs, next upto ~1 ~~ rules);
   6.138 -    in make_rules (next - 1) rules netpairs wrappers end;
   6.139 -
   6.140 -  val print = print_rules Display.pretty_thm_sg;
   6.141 -end;
   6.142 -
   6.143 -structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
   6.144 -val print_global_rules = GlobalRules.print;
   6.145 -
   6.146 -structure LocalRulesArgs =
   6.147 -struct
   6.148 -  val name = GlobalRulesArgs.name;
   6.149 -  type T = GlobalRulesArgs.T;
   6.150 -  val init = GlobalRules.get;
   6.151 -  val print = print_rules ProofContext.pretty_thm;
   6.152 -end;
   6.153 -
   6.154 -structure LocalRules = ProofDataFun(LocalRulesArgs);
   6.155 -val print_local_rules = LocalRules.print;
   6.156 -
   6.157 -fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
   6.158 -val Snetpair = hd o netpairs;
   6.159 -val netpair = hd o tl o netpairs;
   6.160 -
   6.161 -
   6.162 -fun untaglist [] = []
   6.163 -  | untaglist [(k : int * int, x)] = [x]
   6.164 -  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
   6.165 -      if k = k' then untaglist rest
   6.166 -      else x :: untaglist rest;
   6.167 -
   6.168 -fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
   6.169 -fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
   6.170 -
   6.171 -
   6.172 -(* wrappers *)
   6.173 -
   6.174 -fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   6.175 -  make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
   6.176 -
   6.177 -val addSWrapper = gen_add_wrapper Library.apfst;
   6.178 -val addWrapper = gen_add_wrapper Library.apsnd;
   6.179 -
   6.180 -
   6.181 -fun gen_wrap which ctxt =
   6.182 -  let val Rules {wrappers, ...} = LocalRules.get ctxt
   6.183 -  in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
   6.184 -
   6.185 -val Swrap = gen_wrap #1;
   6.186 -val wrap = gen_wrap #2;
   6.187 -
   6.188 -
   6.189 -
   6.190 -(** attributes **)
   6.191 -
   6.192 -(* add and del rules *)
   6.193 -
   6.194 -local
   6.195 -
   6.196 -fun del map_data (x, th) =
   6.197 -  (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
   6.198 -
   6.199 -fun add k view map_data opt_w =
   6.200 -  (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
   6.201 -
   6.202 -in
   6.203 -
   6.204 -val intro_bang_global  = add intro_bangK I GlobalRules.map;
   6.205 -val elim_bang_global   = add elim_bangK I GlobalRules.map;
   6.206 -val dest_bang_global   = add elim_bangK Tactic.make_elim GlobalRules.map;
   6.207 -val intro_global       = add introK I GlobalRules.map;
   6.208 -val elim_global        = add elimK I GlobalRules.map;
   6.209 -val dest_global        = add elimK Tactic.make_elim GlobalRules.map;
   6.210 -val intro_query_global = add intro_queryK I GlobalRules.map;
   6.211 -val elim_query_global  = add elim_queryK I GlobalRules.map;
   6.212 -val dest_query_global  = add elim_queryK Tactic.make_elim GlobalRules.map;
   6.213 -val rule_del_global    = del GlobalRules.map;
   6.214 -
   6.215 -val intro_bang_local   = add intro_bangK I LocalRules.map;
   6.216 -val elim_bang_local    = add elim_bangK I LocalRules.map;
   6.217 -val dest_bang_local    = add elim_bangK Tactic.make_elim LocalRules.map;
   6.218 -val intro_local        = add introK I LocalRules.map;
   6.219 -val elim_local         = add elimK I LocalRules.map;
   6.220 -val dest_local         = add elimK Tactic.make_elim LocalRules.map;
   6.221 -val intro_query_local  = add intro_queryK I LocalRules.map;
   6.222 -val elim_query_local   = add elim_queryK I LocalRules.map;
   6.223 -val dest_query_local   = add elim_queryK Tactic.make_elim LocalRules.map;
   6.224 -val rule_del_local     = del LocalRules.map;
   6.225 -
   6.226 -end;
   6.227 -
   6.228 -
   6.229 -(* concrete syntax *)
   6.230 -
   6.231 -fun add_args a b c x = Attrib.syntax
   6.232 -  (Scan.lift (Scan.option Args.nat --
   6.233 -    (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
   6.234 -
   6.235 -fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
   6.236 -
   6.237 -
   6.238 -val rule_atts =
   6.239 - [("intro",
   6.240 -   (add_args intro_bang_global intro_global intro_query_global,
   6.241 -    add_args intro_bang_local intro_local intro_query_local),
   6.242 -    "declaration of introduction rule"),
   6.243 -  ("elim",
   6.244 -   (add_args elim_bang_global elim_global elim_query_global,
   6.245 -    add_args elim_bang_local elim_local elim_query_local),
   6.246 -    "declaration of elimination rule"),
   6.247 -  ("dest",
   6.248 -   (add_args dest_bang_global dest_global dest_query_global,
   6.249 -    add_args dest_bang_local dest_local dest_query_local),
   6.250 -    "declaration of destruction rule"),
   6.251 -  ("rule", (del_args rule_del_global, del_args rule_del_local),
   6.252 -    "remove declaration of intro/elim/dest rule")];
   6.253 -
   6.254 -
   6.255 -
   6.256 -(** theory setup **)
   6.257 -
   6.258 -val setup =
   6.259 - [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
   6.260 -
   6.261 -
   6.262 -end;
     7.1 --- a/src/Pure/pure.ML	Mon Dec 03 21:03:06 2001 +0100
     7.2 +++ b/src/Pure/pure.ML	Mon Dec 03 21:31:55 2001 +0100
     7.3 @@ -13,7 +13,7 @@
     7.4      ProofContext.setup @
     7.5      Locale.setup @
     7.6      Attrib.setup @
     7.7 -    RuleContext.setup @
     7.8 +    ContextRules.setup @
     7.9      InductAttrib.setup @
    7.10      Method.setup @
    7.11      Calculation.setup @