# HG changeset patch # User wenzelm # Date 1006991112 -3600 # Node ID 3b31490191d8e65b703690c5d2f72f17a11595f2 # Parent 6e70d870ddf08222fcc8ad409be4d03f24858e25 added deletion of rules; tuned; diff -r 6e70d870ddf0 -r 3b31490191d8 src/Pure/Isar/rule_context.ML --- a/src/Pure/Isar/rule_context.ML Thu Nov 29 00:44:34 2001 +0100 +++ b/src/Pure/Isar/rule_context.ML Thu Nov 29 00:45:12 2001 +0100 @@ -5,17 +5,11 @@ 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 @@ -27,6 +21,7 @@ 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 @@ -36,6 +31,7 @@ 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; @@ -69,33 +65,30 @@ (* 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 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 - 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} + 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); + 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, ...}) = @@ -113,7 +106,7 @@ val name = "Isar/rule_context"; type T = T; - val empty = empty_rules; + val empty = make_rules ~1 [] empty_netpairs []; val copy = I; val prep_ext = I; @@ -127,7 +120,7 @@ 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; + in make_rules (next - 1) rules netpairs wrappers end; val print = print_rules Display.pretty_thm_sg; end; @@ -150,33 +143,39 @@ (** attributes **) -(* add rules *) +(* add and del rules *) local -fun mk_att k view map_data opt_w (x, th) = (map_data (add_rule k opt_w th) x, th); +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 = 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_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 = 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; +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; @@ -187,6 +186,9 @@ (Scan.lift (Scan.option (Args.bracks 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, @@ -199,7 +201,9 @@ ("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")]; + "declaration of destruction rule"), + ("rule", (del_args rule_del_global, del_args rule_del_local), + "remove declaration of intro/elim/dest rule")];