--- a/src/Pure/IsaMakefile Mon Dec 03 21:03:06 2001 +0100
+++ b/src/Pure/IsaMakefile Mon Dec 03 21:31:55 2001 +0100
@@ -31,16 +31,17 @@
Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML \
Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML \
- Isar/induct_attrib.ML Isar/isar.ML Isar/isar_cmd.ML \
- Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML \
- 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/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 \
+ Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \
+ Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML \
+ Isar/isar_thy.ML Isar/locale.ML 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 \
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 \
@@ -53,6 +54,7 @@
pattern.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML \
sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \
thm.ML type.ML type_infer.ML unify.ML
+
@./mk
--- a/src/Pure/Isar/ROOT.ML Mon Dec 03 21:03:06 2001 +0100
+++ b/src/Pure/Isar/ROOT.ML Mon Dec 03 21:31:55 2001 +0100
@@ -17,7 +17,7 @@
use "proof_history.ML";
use "args.ML";
use "attrib.ML";
-use "rule_context.ML";
+use "context_rules.ML";
use "net_rules.ML";
use "induct_attrib.ML";
use "method.ML";
@@ -60,7 +60,7 @@
structure ProofHistory = ProofHistory;
structure Args = Args;
structure Attrib = Attrib;
- structure RuleContext = RuleContext;
+ structure ContextRules = ContextRules;
structure Method = Method;
structure Calculation = Calculation;
structure Obtain = Obtain;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/context_rules.ML Mon Dec 03 21:31:55 2001 +0100
@@ -0,0 +1,260 @@
+(* Title: Pure/Isar/context_rules.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 of the same idea.
+*)
+
+signature CONTEXT_RULES =
+sig
+ type netpair
+ type T
+ val netpair_bang: Proof.context -> netpair
+ val netpair: Proof.context -> netpair
+ val netpairs: Proof.context -> netpair list
+ val orderlist: ((int * int) * 'a) list -> 'a list
+ val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
+ val print_global_rules: theory -> unit
+ val print_local_rules: Proof.context -> unit
+ val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
+ val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
+ val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
+ val wrap: Proof.context -> (int -> tactic) -> int -> tactic
+ 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 rule_del_global: 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 rule_del_local: Proof.context attribute
+ val setup: (theory -> theory) list
+end;
+
+structure ContextRules: CONTEXT_RULES =
+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);
+
+
+(* raw data *)
+
+type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
+val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
+
+datatype T = Rules of
+ {next: int,
+ rules: (int * ((int * bool) * thm)) list,
+ netpairs: netpair list,
+ wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
+ (((int -> tactic) -> int -> tactic) * stamp) list};
+
+fun make_rules next rules netpairs wrappers =
+ Rules {next = next, rules = rules, netpairs = netpairs, wrappers = 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
+ make_rules (next - 1) ((w, ((i, b), th)) :: rules)
+ (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
+ end;
+
+fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
+ let
+ fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
+ fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
+ in
+ if not (exists eq_th rules) then rs
+ else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) 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)
+ (sort (int_ord o pairself fst) 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 = make_rules ~1 [] empty_netpairs ([], []);
+ val copy = I;
+ val prep_ext = I;
+
+ fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
+ Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
+ let
+ val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
+ 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 make_rules (next - 1) rules netpairs 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;
+
+
+(* access data *)
+
+fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
+val netpair_bang = hd o netpairs;
+val netpair = hd o tl o netpairs;
+
+
+fun untaglist [] = []
+ | untaglist [(k : int * int, x)] = [x]
+ | untaglist ((k, x) :: (rest as (k', x') :: _)) =
+ if k = k' then untaglist rest
+ else x :: untaglist rest;
+
+fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
+fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
+
+
+fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+ make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
+
+val addSWrapper = gen_add_wrapper Library.apfst;
+val addWrapper = gen_add_wrapper Library.apsnd;
+
+
+fun gen_wrap which ctxt =
+ let val Rules {wrappers, ...} = LocalRules.get ctxt
+ in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
+
+val Swrap = gen_wrap #1;
+val wrap = gen_wrap #2;
+
+
+
+(** attributes **)
+
+(* add and del rules *)
+
+local
+
+fun del map_data (x, th) =
+ (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
+
+fun add k view map_data opt_w =
+ (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
+
+in
+
+val intro_bang_global = add intro_bangK I GlobalRules.map;
+val elim_bang_global = add elim_bangK I GlobalRules.map;
+val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map;
+val intro_global = add introK I GlobalRules.map;
+val elim_global = add elimK I GlobalRules.map;
+val dest_global = add elimK Tactic.make_elim GlobalRules.map;
+val intro_query_global = add intro_queryK I GlobalRules.map;
+val elim_query_global = add elim_queryK I GlobalRules.map;
+val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map;
+val rule_del_global = del GlobalRules.map;
+
+val intro_bang_local = add intro_bangK I LocalRules.map;
+val elim_bang_local = add elim_bangK I LocalRules.map;
+val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map;
+val intro_local = add introK I LocalRules.map;
+val elim_local = add elimK I LocalRules.map;
+val dest_local = add elimK Tactic.make_elim LocalRules.map;
+val intro_query_local = add intro_queryK I LocalRules.map;
+val elim_query_local = add elim_queryK I LocalRules.map;
+val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map;
+val rule_del_local = del LocalRules.map;
+
+end;
+
+
+(* concrete syntax *)
+
+fun add_args a b c x = Attrib.syntax
+ (Scan.lift (Scan.option Args.nat --
+ (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
+
+fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
+
+
+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"),
+ ("rule", (del_args rule_del_global, del_args rule_del_local),
+ "remove declaration of intro/elim/dest rule")];
+
+
+
+(** theory setup **)
+
+val setup =
+ [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
+
+
+end;
--- a/src/Pure/Isar/method.ML Mon Dec 03 21:03:06 2001 +0100
+++ b/src/Pure/Isar/method.ML Mon Dec 03 21:31:55 2001 +0100
@@ -36,7 +36,6 @@
val fold: thm list -> Proof.method
val multi_resolve: thm list -> thm -> thm Seq.seq
val multi_resolves: thm list -> thm list -> thm Seq.seq
- val debug_rules: bool ref
val rules_tac: Proof.context -> int option -> int -> tactic
val rule_tac: thm list -> thm list -> int -> tactic
val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
@@ -217,15 +216,18 @@
length s1 = length s2 andalso
gen_subset e (s1, s2) andalso gen_subset e (s2, s1);
-val bires_tac = Tactic.biresolution_from_nets_tac RuleContext.orderlist;
+val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
fun safe_step_tac ctxt =
- RuleContext.Swrap ctxt (eq_assume_tac ORELSE' bires_tac true (RuleContext.Snetpair ctxt));
+ ContextRules.Swrap ctxt
+ (eq_assume_tac ORELSE'
+ bires_tac true (ContextRules.netpair_bang ctxt));
fun unsafe_step_tac ctxt =
- RuleContext.wrap ctxt (assume_tac APPEND'
- bires_tac false (RuleContext.Snetpair ctxt) APPEND'
- bires_tac false (RuleContext.netpair ctxt));
+ ContextRules.wrap ctxt
+ (assume_tac APPEND'
+ bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
+ bires_tac false (ContextRules.netpair ctxt));
fun step_tac ctxt i =
REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
@@ -243,11 +245,7 @@
in
-val debug_rules = ref false;
-
-fun rules_tac ctxt opt_lim =
- (conditional (! debug_rules) (fn () => RuleContext.print_local_rules ctxt);
- DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4);
+fun rules_tac ctxt opt_lim = DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4;
end;
@@ -256,8 +254,8 @@
local
-fun may_unify t nets = RuleContext.orderlist_no_weight
- (flat (map (fn net => Net.unify_term net t) nets));
+fun may_unify t nets =
+ flat (map (ContextRules.orderlist_no_weight o (fn net => Net.unify_term net t)) nets);
fun find_erules [] = K []
| find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
@@ -274,7 +272,7 @@
fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
let
- val netpairs = RuleContext.netpairs ctxt;
+ val netpairs = ContextRules.netpairs ctxt;
val rules =
if not (null arg_rules) then arg_rules
else map #2 (find_erules facts (map #2 netpairs) @ find_rules goal (map #1 netpairs));
@@ -505,23 +503,23 @@
>> (pair (I: Proof.context -> Proof.context) o att);
val rules_modifiers =
- [modifier destN Args.query_colon Args.query RuleContext.dest_query_local,
- modifier destN Args.bang_colon Args.bang RuleContext.dest_bang_local,
- modifier destN Args.colon (Scan.succeed ()) RuleContext.dest_local,
- modifier elimN Args.query_colon Args.query RuleContext.elim_query_local,
- modifier elimN Args.bang_colon Args.bang RuleContext.elim_bang_local,
- modifier elimN Args.colon (Scan.succeed ()) RuleContext.elim_local,
- modifier introN Args.query_colon Args.query RuleContext.intro_query_local,
- modifier introN Args.bang_colon Args.bang RuleContext.intro_bang_local,
- modifier introN Args.colon (Scan.succeed ()) RuleContext.intro_local,
- Args.del -- Args.colon >> K (I, RuleContext.rule_del_local)];
+ [modifier destN Args.query_colon Args.query ContextRules.dest_query_local,
+ modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
+ modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local,
+ modifier elimN Args.query_colon Args.query ContextRules.elim_query_local,
+ modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local,
+ modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local,
+ modifier introN Args.query_colon Args.query ContextRules.intro_query_local,
+ modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local,
+ modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local,
+ Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)];
in
fun rules_args m = bang_sectioned_args' rules_modifiers (Scan.lift (Scan.option Args.nat)) m;
fun rules_meth n prems ctxt = METHOD (fn facts =>
- HEADGOAL (insert_tac (prems @ facts) THEN' rules_tac ctxt n));
+ HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' rules_tac ctxt n));
end;
@@ -672,7 +670,7 @@
val setup =
[MethodsData.init, add_methods pure_methods,
- (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [RuleContext.intro_query_global None])])];
+ (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [ContextRules.intro_query_global None])])];
end;
--- a/src/Pure/Isar/obtain.ML Mon Dec 03 21:03:06 2001 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Dec 03 21:31:55 2001 +0100
@@ -107,7 +107,7 @@
|> Proof.enter_forward
|> Proof.begin_block
|> Proof.fix_i [([thesisN], None)]
- |> Proof.assume_i [((thatN, [RuleContext.intro_query_local None]), [(that_prop, ([], []))])]
+ |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
|> (fn state' =>
state'
|> Proof.from_facts chain_facts
--- a/src/Pure/Isar/rule_context.ML Mon Dec 03 21:03:06 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,259 +0,0 @@
-(* 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.
-*)
-
-signature RULE_CONTEXT =
-sig
- type netpair
- type T
- val Snetpair: Proof.context -> netpair
- val netpair: Proof.context -> netpair
- val netpairs: Proof.context -> netpair list
- val orderlist: ((int * int) * 'a) list -> 'a list
- val orderlist_no_weight: ((int * int) * 'a) list -> 'a list
- val print_global_rules: theory -> unit
- val print_local_rules: Proof.context -> unit
- val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
- val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
- val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
- val wrap: Proof.context -> (int -> tactic) -> int -> tactic
- 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 rule_del_global: 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 rule_del_local: 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);
-
-
-(* raw data *)
-
-type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
-val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
-
-datatype T = Rules of
- {next: int,
- rules: (int * ((int * bool) * thm)) list,
- netpairs: netpair list,
- wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
- (((int -> tactic) -> int -> tactic) * stamp) list};
-
-fun make_rules next rules netpairs wrappers =
- Rules {next = next, rules = rules, netpairs = netpairs, wrappers = 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
- make_rules (next - 1) ((w, ((i, b), th)) :: rules)
- (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
- end;
-
-fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
- let
- fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
- fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
- in
- if not (exists eq_th rules) then rs
- else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) 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)
- (sort (int_ord o pairself fst) 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 = make_rules ~1 [] empty_netpairs ([], []);
- val copy = I;
- val prep_ext = I;
-
- fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
- Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
- let
- val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
- 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 make_rules (next - 1) rules netpairs 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;
-
-fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
-val Snetpair = hd o netpairs;
-val netpair = hd o tl o netpairs;
-
-
-fun untaglist [] = []
- | untaglist [(k : int * int, x)] = [x]
- | untaglist ((k, x) :: (rest as (k', x') :: _)) =
- if k = k' then untaglist rest
- else x :: untaglist rest;
-
-fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
-fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls);
-
-
-(* wrappers *)
-
-fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
- make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
-
-val addSWrapper = gen_add_wrapper Library.apfst;
-val addWrapper = gen_add_wrapper Library.apsnd;
-
-
-fun gen_wrap which ctxt =
- let val Rules {wrappers, ...} = LocalRules.get ctxt
- in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
-
-val Swrap = gen_wrap #1;
-val wrap = gen_wrap #2;
-
-
-
-(** attributes **)
-
-(* add and del rules *)
-
-local
-
-fun del map_data (x, th) =
- (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th);
-
-fun add k view map_data opt_w =
- (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data;
-
-in
-
-val intro_bang_global = add intro_bangK I GlobalRules.map;
-val elim_bang_global = add elim_bangK I GlobalRules.map;
-val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map;
-val intro_global = add introK I GlobalRules.map;
-val elim_global = add elimK I GlobalRules.map;
-val dest_global = add elimK Tactic.make_elim GlobalRules.map;
-val intro_query_global = add intro_queryK I GlobalRules.map;
-val elim_query_global = add elim_queryK I GlobalRules.map;
-val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map;
-val rule_del_global = del GlobalRules.map;
-
-val intro_bang_local = add intro_bangK I LocalRules.map;
-val elim_bang_local = add elim_bangK I LocalRules.map;
-val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map;
-val intro_local = add introK I LocalRules.map;
-val elim_local = add elimK I LocalRules.map;
-val dest_local = add elimK Tactic.make_elim LocalRules.map;
-val intro_query_local = add intro_queryK I LocalRules.map;
-val elim_query_local = add elim_queryK I LocalRules.map;
-val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map;
-val rule_del_local = del LocalRules.map;
-
-end;
-
-
-(* concrete syntax *)
-
-fun add_args a b c x = Attrib.syntax
- (Scan.lift (Scan.option Args.nat --
- (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x;
-
-fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
-
-
-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"),
- ("rule", (del_args rule_del_global, del_args rule_del_local),
- "remove declaration of intro/elim/dest rule")];
-
-
-
-(** theory setup **)
-
-val setup =
- [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
-
-
-end;
--- a/src/Pure/pure.ML Mon Dec 03 21:03:06 2001 +0100
+++ b/src/Pure/pure.ML Mon Dec 03 21:31:55 2001 +0100
@@ -13,7 +13,7 @@
ProofContext.setup @
Locale.setup @
Attrib.setup @
- RuleContext.setup @
+ ContextRules.setup @
InductAttrib.setup @
Method.setup @
Calculation.setup @