# HG changeset patch # User wenzelm # Date 937927435 -7200 # Node ID dd281afb33d751c440803cb3179934f91416d7ee # Parent 30327f9f6b4aed053f89b4ac22539e7dbca7f9c5 setup for refined facts handling; tuned insert_facts, assumption, (un)fold; insert_tac: no rotate_tac, order was OK in the first place; added ctxt_args, bang_sectioned_args; added assm_tac; diff -r 30327f9f6b4a -r dd281afb33d7 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Sep 21 17:07:28 1999 +0200 +++ b/src/Pure/Isar/method.ML Tue Sep 21 17:23:55 1999 +0200 @@ -19,7 +19,7 @@ val fail: Proof.method val succeed: Proof.method val insert_tac: thm list -> int -> tactic - val insert: Proof.method + val insert_facts: Proof.method val fold: thm list -> Proof.method val unfold: thm list -> Proof.method val multi_resolve: thm list -> thm -> thm Seq.seq @@ -28,7 +28,7 @@ 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 assumption: Proof.context -> Proof.method exception METHOD_FAIL of (string * Position.T) * exn val help_methods: theory -> unit val method: theory -> Args.src -> Proof.context -> Proof.method @@ -36,15 +36,15 @@ -> theory -> theory val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> Proof.context -> Args.src -> Proof.context * 'a + val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method type modifier val sectioned_args: ((Args.T list -> modifier * Args.T list) list -> Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> (Args.T list -> modifier * Args.T list) list -> ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method - val default_sectioned_args: modifier -> - (Args.T list -> modifier * Args.T list) list -> - (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method + val bang_sectioned_args: (Args.T list -> modifier * Args.T list) list -> + (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method val only_sectioned_args: (Args.T list -> modifier * Args.T list) list -> (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method @@ -102,22 +102,22 @@ let val rule = Drule.forall_intr_vars raw_rule; val revcut_rl = Drule.incr_indexes_wrt [] [] [] [rule] Drule.revcut_rl; - in Tactic.rtac (rule COMP revcut_rl) THEN' Tactic.rotate_tac ~1 end; + in Tactic.rtac (rule COMP revcut_rl) end; in fun insert_tac [] i = all_tac | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); -val insert = METHOD (ALLGOALS o insert_tac); +val insert_facts = METHOD (ALLGOALS o insert_tac); end; (* fold / unfold definitions *) -fun fold thms = METHOD (fn _ => fold_goals_tac thms); -fun unfold thms = METHOD (fn _ => rewrite_goals_tac thms); +fun fold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN fold_goals_tac thms); +fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms); (* multi_resolve *) @@ -160,13 +160,17 @@ end; -(* assumption *) +(* assumption / finish *) + +fun assm_tac ctxt = + assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt)); -fun assumption_tac [] = assume_tac - | assumption_tac [fact] = resolve_tac [fact] - | assumption_tac _ = K no_tac; +fun assumption_tac ctxt [] = assm_tac ctxt + | assumption_tac _ [fact] = resolve_tac [fact] + | assumption_tac _ _ = K no_tac; -val assumption = METHOD (FIRSTGOAL o assumption_tac); +fun assumption ctxt = METHOD (FIRSTGOAL o assumption_tac ctxt); +fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt)))); @@ -256,7 +260,10 @@ fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) = Args.syntax "method" scan; -fun no_args (x: Proof.method) src ctxt = #2 (syntax (Scan.succeed x) ctxt src); +fun ctxt_args (f: Proof.context -> Proof.method) src ctxt = + #2 (syntax (Scan.succeed (f ctxt)) ctxt src); + +fun no_args m = ctxt_args (K m); (* sections *) @@ -282,9 +289,7 @@ let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src in f x ctxt' end; -fun default_sectioned_args m ss f src ctxt = - sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply m (ctxt', ths)))) src ctxt; - +fun bang_sectioned_args ss f = sectioned_args (K Args.bang_facts) ss f; fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f); fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths); @@ -326,20 +331,12 @@ |> refine text; -(* finish *) - -val FINISHED = FILTER (equal 0 o Thm.nprems_of); -val finish = METHOD (K (FINISHED (ALLGOALS assume_tac))); -val basic_finish = Basic (K finish); - -fun finish_text None = basic_finish - | finish_text (Some txt) = Then [txt, basic_finish]; - - (* structured proof steps *) val default_text = Source (Args.src (("default", []), Position.none)); -val assumption_text = Basic (K assumption); + +fun finish_text None = Basic finish + | finish_text (Some txt) = Then [txt, Basic finish]; fun proof opt_text state = state @@ -349,7 +346,7 @@ fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_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 (assumption_text, None); +val local_immediate_proof = local_terminal_proof (Basic assumption, None); val local_default_proof = local_terminal_proof (default_text, None); @@ -369,7 +366,7 @@ |> Proof.check_result "Failed to finish proof (after successful terminal method)" state |> Seq.hd; -val global_immediate_proof = global_terminal_proof (assumption_text, None); +val global_immediate_proof = global_terminal_proof (Basic assumption, None); val global_default_proof = global_terminal_proof (default_text, None); @@ -381,12 +378,12 @@ val pure_methods = [("fail", no_args fail, "force failure"), ("succeed", no_args succeed, "succeed"), - ("-", no_args insert, "insert facts, nothing else"), - ("fold", thms_args fold, "fold definitions"), - ("unfold", thms_args unfold, "unfold definitions"), + ("-", no_args insert_facts, "insert facts"), + ("fold", thms_args fold, "fold definitions, ignoring facts"), + ("unfold", thms_args unfold, "unfold definitions, ignoring facts"), ("rule", thms_args rule, "apply some rule"), ("erule", thms_args erule, "apply some erule (improper!)"), - ("assumption", no_args assumption, "proof by assumption")]; + ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")]; (* setup *)