# HG changeset patch # User wenzelm # Date 936213577 -7200 # Node ID 5a1035047bae8470586ba3a7f14c2144b5766fe9 # Parent 87c12d352babff441a5f980ecf33e5369118f2ab tuned; renamed same_tac to insert_tac; improved assumption; removed Repeat; immediate_proof: assumption; diff -r 87c12d352bab -r 5a1035047bae src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Sep 01 21:17:37 1999 +0200 +++ b/src/Pure/Isar/method.ML Wed Sep 01 21:19:37 1999 +0200 @@ -14,23 +14,25 @@ signature METHOD = sig include BASIC_METHOD - val help_methods: theory -> unit - val multi_resolve: thm list -> thm -> thm Seq.seq - val FINISHED: tactic -> tactic val METHOD: (thm list -> tactic) -> Proof.method val METHOD0: tactic -> Proof.method val fail: Proof.method val succeed: Proof.method - val same_tac: thm list -> int -> tactic - val same: Proof.method - val assumption_tac: thm list -> int -> tactic - val assumption: Proof.method - val forward_chain: thm list -> thm list -> thm Seq.seq + val insert_tac: thm list -> int -> tactic + val insert: Proof.method + val fold: thm list -> Proof.method + val unfold: thm list -> Proof.method + val multi_resolve: thm list -> thm -> thm Seq.seq + val multi_resolves: thm list -> thm list -> thm Seq.seq val rule_tac: thm list -> thm list -> int -> tactic val erule_tac: thm list -> thm list -> int -> tactic val rule: thm list -> Proof.method val erule: thm list -> Proof.method + val assumption: Proof.method + val FINISHED: tactic -> tactic + val finish: Proof.method exception METHOD_FAIL of (string * Position.T) * exn + val help_methods: theory -> unit val method: theory -> Args.src -> Proof.context -> Proof.method val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list -> theory -> theory @@ -54,7 +56,6 @@ Then of text list | Orelse of text list | Try of text | - Repeat of text | Repeat1 of text val refine: text -> Proof.state -> Proof.state Seq.seq val tac: text -> Proof.state -> Proof.state Seq.seq @@ -82,12 +83,6 @@ struct -(** utils **) - -val FINISHED = FILTER (equal 0 o Thm.nprems_of); - - - (** proof methods **) (* method from tactic *) @@ -102,7 +97,9 @@ val succeed = METHOD (K all_tac); -(* same *) +(* insert *) + +local fun cut_rule_tac raw_rule = let @@ -110,17 +107,14 @@ val revcut_rl = Drule.incr_indexes_wrt [] [] [] [rule] Drule.revcut_rl; in Tactic.rtac (rule COMP revcut_rl) THEN' Tactic.rotate_tac ~1 end; -fun same_tac [] i = all_tac - | same_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); - -val same = METHOD (ALLGOALS o same_tac); - +in -(* assumption *) +fun insert_tac [] i = all_tac + | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); -fun assumption_tac facts = same_tac facts THEN' assume_tac; -val assumption = METHOD (FIRSTGOAL o assumption_tac); -val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac))); +val insert = METHOD (ALLGOALS o insert_tac); + +end; (* fold / unfold definitions *) @@ -129,31 +123,60 @@ val unfold = METHOD0 o rewrite_goals_tac; +(* multi_resolve *) + +local + +fun res th i rule = + Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; + +fun multi_res _ [] rule = Seq.single rule + | multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule)); + +in + +val multi_resolve = multi_res 1; +fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); + +end; + + (* rule *) -fun res th i rule = Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; - -fun multi_resolve facts rule = - let - fun multi_res i [] = Seq.single rule - | multi_res i (th :: ths) = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths)) - in multi_res 1 facts end; - -fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); +local fun gen_rule_tac tac rules [] = tac rules | gen_rule_tac tac erules facts = let - val rules = forward_chain facts erules; + val rules = multi_resolves facts erules; fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules); in tactic end; +in + val rule_tac = gen_rule_tac Tactic.resolve_tac; val erule_tac = gen_rule_tac Tactic.eresolve_tac; fun rule rules = METHOD (FIRSTGOAL o rule_tac rules); fun erule rules = METHOD (FIRSTGOAL o erule_tac rules); +end; + + +(* assumption *) + +fun assumption_tac [] = assume_tac + | assumption_tac [fact] = resolve_tac [fact] + | assumption_tac _ = K no_tac; + +val assumption = METHOD (FIRSTGOAL o assumption_tac); + + +(* finish *) + +val FINISHED = FILTER (equal 0 o Thm.nprems_of); +val finish = METHOD (K (FINISHED (ALLGOALS assume_tac))); + (** methods theory data **) @@ -289,7 +312,6 @@ Then of text list | Orelse of text list | Try of text | - Repeat of text | Repeat1 of text; @@ -304,7 +326,6 @@ | eval (Then txts) = Seq.EVERY (map eval txts) | eval (Orelse txts) = Seq.FIRST (map eval txts) | eval (Try txt) = Seq.TRY (eval txt) - | eval (Repeat txt) = Seq.REPEAT (eval txt) | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt); in eval text state end; @@ -338,7 +359,7 @@ fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text)); fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr); -val local_immediate_proof = local_terminal_proof (Basic (K same), None); +val local_immediate_proof = local_terminal_proof (Basic (K assumption), None); val local_default_proof = local_terminal_proof (default_text, None); @@ -358,7 +379,7 @@ |> Proof.check_result "Failed to finish proof (after successful terminal method)" state |> Seq.hd; -val global_immediate_proof = global_terminal_proof (Basic (K same), None); +val global_immediate_proof = global_terminal_proof (Basic (K assumption), None); val global_default_proof = global_terminal_proof (default_text, None); @@ -370,13 +391,13 @@ val pure_methods = [("fail", no_args fail, "force failure"), ("succeed", no_args succeed, "succeed"), - ("-", no_args same, "insert facts, nothing else"), - ("assumption", no_args assumption, "proof by assumption"), - ("finish", no_args asm_finish, "finish proof by assumption"), + ("-", no_args insert, "insert facts, nothing else"), ("fold", thms_args fold, "fold definitions"), ("unfold", thms_args unfold, "unfold definitions"), ("rule", thms_args rule, "apply some rule"), - ("erule", thms_args erule, "apply some erule (improper!)")]; + ("erule", thms_args erule, "apply some erule (improper!)"), + ("assumption", no_args assumption, "proof by assumption"), + ("finish", no_args finish, "finish proof by assumption")]; (* setup *)