--- a/src/HOL/Eisbach/match_method.ML Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML Fri Dec 11 13:44:20 2015 +0100
@@ -776,7 +776,7 @@
val goal' =
DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
|> Seq.maps (DETERM (do_retrofit ctxt'))
- |> Seq.map (fn goal => ([]: cases, goal));
+ |> Seq.map (fn goal => ([]: Rule_Cases.cases, goal));
in goal' end;
in
Seq.map apply_text texts
--- a/src/HOL/Nominal/nominal_induct.ML Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Dec 11 13:44:20 2015 +0100
@@ -7,7 +7,7 @@
sig
val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
- thm list -> int -> Rule_Cases.cases_tactic
+ thm list -> int -> cases_tactic
val nominal_induct_method: (Proof.context -> Proof.method) context_parser
end =
struct
--- 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;
--- a/src/Pure/Isar/rule_cases.ML Thu Dec 10 21:39:33 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML Fri Dec 11 13:44:20 2015 +0100
@@ -4,27 +4,14 @@
Annotations and local contexts of rules.
*)
-infix 1 THEN_ALL_NEW_CASES;
-
-signature BASIC_RULE_CASES =
-sig
- type cases
- type cases_state = cases * thm
- type cases_tactic = thm -> cases_state Seq.seq
- val 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 RULE_CASES =
sig
- include BASIC_RULE_CASES
datatype T = Case of
{fixes: (binding * typ) list,
assumes: (string * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list}
+ type cases = (string * T option) list
val case_hypsN: string
val strip_params: term -> (string * typ) list
type info = ((string * string list) * string list) list
@@ -184,25 +171,6 @@
-(** tactics with cases **)
-
-type cases_state = 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');
-
-
-
(** annotations and operations on rules **)
(* consume facts *)
@@ -483,6 +451,3 @@
| SOME res => res);
end;
-
-structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
-open Basic_Rule_Cases;