# HG changeset patch # User wenzelm # Date 1006995050 -3600 # Node ID 5db4b4596d1a7e63f0d70d1630794f62506f8a80 # Parent e151ee6e820fee6fbeac85d247a3c22708f459f0 rule context and attributes moved to rule_context.ML; diff -r e151ee6e820f -r 5db4b4596d1a src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Nov 29 01:50:19 2001 +0100 +++ b/src/Pure/Isar/method.ML Thu Nov 29 01:50:50 2001 +0100 @@ -17,22 +17,6 @@ sig include BASIC_METHOD val trace: Proof.context -> thm list -> unit - val print_global_rules: theory -> unit - val print_local_rules: Proof.context -> unit - val dest_global: theory attribute - val elim_global: theory attribute - val intro_global: theory attribute - val dest_bang_global: theory attribute - val elim_bang_global: theory attribute - val intro_bang_global: theory attribute - val rule_del_global: theory attribute - val dest_local: Proof.context attribute - val elim_local: Proof.context attribute - val intro_local: Proof.context attribute - val dest_bang_local: Proof.context attribute - val elim_bang_local: Proof.context attribute - val intro_bang_local: Proof.context attribute - val rule_del_local: Proof.context attribute val RAW_METHOD: (thm list -> tactic) -> Proof.method val RAW_METHOD_CASES: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method @@ -133,7 +117,9 @@ struct -(** tracing *) +(** proof methods **) + +(* tracing *) val trace_rules = ref false; @@ -143,127 +129,6 @@ |> Pretty.string_of |> tracing); - -(** global and local rule data **) - -val intro_bangK = 0; -val elim_bangK = 1; -val introK = 2; -val elimK = 3; - -local - -fun kind_name 0 = "safe introduction rules (intro!)" - | kind_name 1 = "safe elimination rules (elim!)" - | kind_name 2 = "introduction rules (intro)" - | kind_name 3 = "elimination rules (elim)" - | kind_name _ = "unknown"; - -fun prt_rules prt x (k, rs) = - Pretty.writeln (Pretty.big_list (kind_name k ^ ":") (map (prt x) (NetRules.rules rs))); - -in - fun print_rules prt x rules = seq (prt_rules prt x) (0 upto length rules - 1 ~~ rules); -end; - - -(* theory data kind 'Isar/rules' *) - -structure GlobalRulesArgs = -struct - val name = "Isar/rules"; - type T = thm NetRules.T list; - - val empty = [NetRules.intro, NetRules.elim, NetRules.intro, NetRules.elim]; - val copy = I; - val prep_ext = I; - fun merge x = map2 NetRules.merge x; - val print = print_rules Display.pretty_thm_sg; -end; - -structure GlobalRules = TheoryDataFun(GlobalRulesArgs); -val print_global_rules = GlobalRules.print; - - -(* proof data kind 'Isar/rules' *) - -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 add_rule k view th = Library.map_nth_elem k (NetRules.insert (view th)); - -val add_intro = add_rule introK I; -val add_elim = add_rule elimK I; -val add_dest = add_rule elimK Tactic.make_elim; -val add_intro_bang = add_rule intro_bangK I; -val add_elim_bang = add_rule elim_bangK I; -val add_dest_bang = add_rule elim_bangK Tactic.make_elim; - -fun del_rule th = map (NetRules.delete th o NetRules.delete (Tactic.make_elim th)); - -fun mk_att f g (x, th) = (f (g th) x, th); - -in - -val dest_global = mk_att GlobalRules.map add_dest; -val elim_global = mk_att GlobalRules.map add_elim; -val intro_global = mk_att GlobalRules.map add_intro; -val dest_bang_global = mk_att GlobalRules.map add_dest_bang; -val elim_bang_global = mk_att GlobalRules.map add_elim_bang; -val intro_bang_global = mk_att GlobalRules.map add_intro_bang; -val rule_del_global = mk_att GlobalRules.map del_rule; - -val dest_local = mk_att LocalRules.map add_dest; -val elim_local = mk_att LocalRules.map add_elim; -val intro_local = mk_att LocalRules.map add_intro; -val dest_bang_local = mk_att LocalRules.map add_dest_bang; -val elim_bang_local = mk_att LocalRules.map add_elim_bang; -val intro_bang_local = mk_att LocalRules.map add_intro_bang; -val rule_del_local = mk_att LocalRules.map del_rule; - -fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att); - -end; - - -(* concrete syntax *) - -val rule_atts = - [("dest", - (Attrib.bang_args dest_bang_global dest_global, - Attrib.bang_args dest_bang_local dest_local), - "declaration of destruction rule"), - ("elim", - (Attrib.bang_args elim_bang_global elim_global, - Attrib.bang_args elim_bang_local elim_local), - "declaration of elimination rule"), - ("intro", - (Attrib.bang_args intro_bang_global intro_global, - Attrib.bang_args intro_bang_local intro_local), - "declaration of introduction rule"), - ("rule", (del_args rule_del_global, del_args rule_del_local), - "remove declaration of elim/intro rule")]; - - - -(** proof methods **) - (* make methods *) val RAW_METHOD = Proof.method; @@ -304,14 +169,11 @@ val insert_facts = METHOD (ALLGOALS o insert_tac); fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); -end; - - -(* simple methods *) - fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); +end; + (* unfold / fold definitions *) @@ -337,30 +199,31 @@ end; -(* basic rules *) +(* single rules *) local +fun may_unify t nets = RuleContext.orderlist (flat (map (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))); + +fun find_rules goal = may_unify (Logic.strip_assums_concl goal); + + fun gen_rule_tac tac rules [] i st = tac rules i st - | gen_rule_tac tac erules facts i st = - Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts erules)); + | gen_rule_tac tac rules facts i st = + Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts rules)); fun gen_arule_tac tac j rules facts = EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac); -fun find_erules [] _ = [] - | find_erules (fact :: _) rs = - NetRules.retrieve rs (Logic.strip_assums_concl (#prop (Thm.rep_thm fact))); - -fun find_rules goal rs = NetRules.retrieve rs (Logic.strip_assums_concl goal); - fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) => let - fun get k = nth_elem (k, LocalRules.get ctxt); + val netpairs = RuleContext.netpairs ctxt; val rules = if not (null arg_rules) then arg_rules - else find_erules facts (get elim_bangK) @ find_erules facts (get elimK) @ - find_rules goal (get intro_bangK) @ find_rules goal (get introK); + else map #2 (find_erules facts (map #2 netpairs) @ find_rules goal (map #1 netpairs)); in trace ctxt rules; tac rules facts i end); fun meth tac x = METHOD (HEADGOAL o tac x); @@ -674,6 +537,7 @@ val global_done_proof = global_term_proof false (done_text, None); + (** theory setup **) (* misc tactic emulations *) @@ -717,9 +581,8 @@ (* setup *) val setup = - [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts, - MethodsData.init, add_methods pure_methods, - (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_global])])]; + [MethodsData.init, add_methods pure_methods, + (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [RuleContext.intro_query_global None])])]; end;