43 val delrules: Proof.context * thm list -> Proof.context |
43 val delrules: Proof.context * thm list -> Proof.context |
44 val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
44 val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
45 val delSWrapper: Proof.context * string -> Proof.context |
45 val delSWrapper: Proof.context * string -> Proof.context |
46 val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
46 val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context |
47 val delWrapper: Proof.context * string -> Proof.context |
47 val delWrapper: Proof.context * string -> Proof.context |
48 val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context |
48 val addSbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
49 val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context |
49 val addSafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
50 val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context |
50 val addbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
51 val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context |
51 val addafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context |
52 val addD2: Proof.context * (string * thm) -> Proof.context |
52 val addD2: Proof.context * (string * thm) -> Proof.context |
53 val addE2: Proof.context * (string * thm) -> Proof.context |
53 val addE2: Proof.context * (string * thm) -> Proof.context |
54 val addSD2: Proof.context * (string * thm) -> Proof.context |
54 val addSD2: Proof.context * (string * thm) -> Proof.context |
55 val addSE2: Proof.context * (string * thm) -> Proof.context |
55 val addSE2: Proof.context * (string * thm) -> Proof.context |
56 val appSWrappers: Proof.context -> wrapper |
56 val appSWrappers: Proof.context -> wrapper |
668 (*Remove an unsafe wrapper*) |
668 (*Remove an unsafe wrapper*) |
669 fun ctxt delWrapper name = ctxt |> map_claset |
669 fun ctxt delWrapper name = ctxt |> map_claset |
670 (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); |
670 (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); |
671 |
671 |
672 (* compose a safe tactic alternatively before/after safe_step_tac *) |
672 (* compose a safe tactic alternatively before/after safe_step_tac *) |
673 fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2); |
673 fun ctxt addSbefore (name, tac1) = |
674 fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2); |
674 ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); |
|
675 fun ctxt addSafter (name, tac2) = |
|
676 ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); |
675 |
677 |
676 (*compose a tactic alternatively before/after the step tactic *) |
678 (*compose a tactic alternatively before/after the step tactic *) |
677 fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2); |
679 fun ctxt addbefore (name, tac1) = |
678 fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2); |
680 ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); |
679 |
681 fun ctxt addafter (name, tac2) = |
680 fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac); |
682 ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); |
681 fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac); |
683 |
682 fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); |
684 fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac); |
683 fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); |
685 fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac); |
|
686 fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac); |
|
687 fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac); |
684 |
688 |
685 |
689 |
686 |
690 |
687 (**** Simple tactics for theorem proving ****) |
691 (**** Simple tactics for theorem proving ****) |
688 |
692 |