--- a/src/Pure/Isar/method.ML Thu Dec 10 21:39:33 2015 +0100
+++ b/src/Pure/Isar/method.ML Fri Dec 11 13:44:20 2015 +0100
@@ -4,8 +4,21 @@
Isar proof methods.
*)
+infix 1 THEN_ALL_NEW_CASES;
+
+signature BASIC_METHOD =
+sig
+ type cases_state = Rule_Cases.cases * thm
+ type cases_tactic = thm -> cases_state Seq.seq
+ val CASES: Rule_Cases.cases -> tactic -> cases_tactic
+ val EMPTY_CASES: tactic -> cases_tactic
+ val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
+ val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
+end;
+
signature METHOD =
sig
+ include BASIC_METHOD
type method = thm list -> cases_tactic
val METHOD_CASES: (thm list -> cases_tactic) -> method
val METHOD: (thm list -> tactic) -> method
@@ -92,7 +105,25 @@
(** proof methods **)
-(* method *)
+(* tactics with cases *)
+
+type cases_state = Rule_Cases.cases * thm;
+type cases_tactic = thm -> cases_state Seq.seq;
+
+fun CASES cases tac st = Seq.map (pair cases) (tac st);
+fun EMPTY_CASES tac = CASES [] tac;
+
+fun SUBGOAL_CASES tac i st =
+ (case try Logic.nth_prem (i, Thm.prop_of st) of
+ SOME goal => tac (goal, i) st
+ | NONE => Seq.empty);
+
+fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
+ st |> tac1 i |> Seq.maps (fn (cases, st') =>
+ CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
+
+
+(* type method *)
type method = thm list -> cases_tactic;
@@ -733,6 +764,9 @@
end;
+structure Basic_Method: BASIC_METHOD = Method;
+open Basic_Method;
+
val METHOD_CASES = Method.METHOD_CASES;
val METHOD = Method.METHOD;
val SIMPLE_METHOD = Method.SIMPLE_METHOD;