48 val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic |
48 val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic |
49 val rule: thm list -> method |
49 val rule: thm list -> method |
50 val erule: int -> thm list -> method |
50 val erule: int -> thm list -> method |
51 val drule: int -> thm list -> method |
51 val drule: int -> thm list -> method |
52 val frule: int -> thm list -> method |
52 val frule: int -> thm list -> method |
53 val rules_tac: ProofContext.context -> int option -> int -> tactic |
53 val iprover_tac: ProofContext.context -> int option -> int -> tactic |
54 val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list -> |
54 val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list -> |
55 thm -> int -> tactic |
55 thm -> int -> tactic |
56 val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit |
56 val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit |
57 val tactic: string -> ProofContext.context -> method |
57 val tactic: string -> ProofContext.context -> method |
58 type src |
58 type src |
669 |
669 |
670 fun modifier name kind kind' att = |
670 fun modifier name kind kind' att = |
671 Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME) |
671 Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME) |
672 >> (pair (I: ProofContext.context -> ProofContext.context) o att); |
672 >> (pair (I: ProofContext.context -> ProofContext.context) o att); |
673 |
673 |
674 val rules_modifiers = |
674 val iprover_modifiers = |
675 [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local, |
675 [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local, |
676 modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local, |
676 modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local, |
677 modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local, |
677 modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local, |
678 modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local, |
678 modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local, |
679 modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local, |
679 modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local, |
680 modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local, |
680 modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local, |
681 Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)]; |
681 Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)]; |
682 |
682 |
683 in |
683 in |
684 |
684 |
685 fun rules_args m = bang_sectioned_args' rules_modifiers (Scan.lift (Scan.option Args.nat)) m; |
685 fun iprover_args m = bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat)) m; |
686 |
686 |
687 fun rules_meth n prems ctxt = METHOD (fn facts => |
687 fun iprover_meth n prems ctxt = METHOD (fn facts => |
688 HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' rules_tac ctxt n)); |
688 HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)); |
689 |
689 |
690 end; |
690 end; |
691 |
691 |
692 |
692 |
693 (* tactic syntax *) |
693 (* tactic syntax *) |
741 ("intro", thms_args intro, "repeatedly apply introduction rules"), |
741 ("intro", thms_args intro, "repeatedly apply introduction rules"), |
742 ("elim", thms_args elim, "repeatedly apply elimination rules"), |
742 ("elim", thms_args elim, "repeatedly apply elimination rules"), |
743 ("fold", thms_args fold_meth, "fold definitions"), |
743 ("fold", thms_args fold_meth, "fold definitions"), |
744 ("atomize", (atomize o #2) oo syntax (Args.mode "full"), |
744 ("atomize", (atomize o #2) oo syntax (Args.mode "full"), |
745 "present local premises as object-level statements"), |
745 "present local premises as object-level statements"), |
746 ("rules", rules_args rules_meth, "apply many rules, including proof search"), |
746 ("iprover", iprover_args iprover_meth, "intuitionistic proof search"), |
747 ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), |
747 ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), |
748 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
748 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
749 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
749 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
750 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |
750 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |
751 ("this", no_args this, "apply current facts as rules"), |
751 ("this", no_args this, "apply current facts as rules"), |