src/Pure/Isar/rule_cases.ML

 end
 
 signature RULE_CASES =
 sig
   include BASIC_RULE_CASES
-  type T
+  datatype T = Case of
+   {fixes: (string * typ) list,
+    assumes: (string * term list) list,
+    binds: (indexname * term option) list,
+    cases: (string * T) list}
+  val strip_params: term -> (string * typ) list
+  val make_common: bool -> theory * term -> (string * string list) list -> cases
+  val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
+  val make_simple: bool -> theory * term -> string -> cases
+  val apply: term list -> T -> T
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
   val add_consumes: int -> thm -> thm
   val consumes: int -> 'a attribute
   val consumes_default: int -> 'a attribute
   val name: string list -> thm -> thm
   val case_names: string list -> 'a attribute
   val case_conclusion: string * string list -> 'a attribute
   val save: thm -> thm -> thm
   val get: thm -> (string * string list) list * int
-  val strip_params: term -> (string * typ) list
-  val make: bool -> term option -> theory * term -> (string * string list) list -> cases
-  val simple: theory * term -> string -> cases
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
   val mutual_rule: thm list -> (int list * thm) option
   val strict_mutual_rule: thm list -> int list * thm
 end;
 
 structure RuleCases: RULE_CASES =
 struct
 
-(** tactics with cases **)
-
-type T =
+(** cases **)
+
+datatype T = Case of
  {fixes: (string * typ) list,
   assumes: (string * term list) list,
-  binds: (indexname * term option) list};
+  binds: (indexname * term option) list,
+  cases: (string * T) list};
 
 type cases = (string * T option) list;
+
+val case_conclN = "case";
+val case_hypsN = "hyps";
+val case_premsN = "prems";
+
+val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params;
+
+local
+
+fun abs xs t = Term.list_abs (xs, t);
+fun app us t = Term.betapplys (t, us);
+
+fun dest_binops cs tm =
+  let
+    val n = length cs;
+    fun dest 0 _ = []
+      | dest 1 t = [t]
+      | dest k (_ $ t $ u) = t :: dest (k - 1) u
+      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
+  in cs ~~ dest n tm end;
+
+fun extract_fixes NONE prop = (strip_params prop, [])
+  | extract_fixes (SOME outline) prop =
+      splitAt (length (Logic.strip_params outline), strip_params prop);
+
+fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
+  | extract_assumes qual (SOME outline) prop =
+      let val (hyps, prems) =
+        splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop)
+      in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
+
+fun extract_case is_open thy (case_outline, raw_prop) name concls =
+  let
+    val rename = if is_open then I else (apfst Syntax.internal);
+
+    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
+    val len = length props;
+    val nested = is_some case_outline andalso len > 1;
+
+    fun extract prop =
+      let
+        val (fixes1, fixes2) = extract_fixes case_outline prop
+          |> apfst (map rename);
+        val abs_fixes = abs (fixes1 @ fixes2);
+        fun abs_fixes1 t =
+          if not nested then abs_fixes t
+          else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
+
+        val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
+          |> pairself (map (apsnd (List.concat o map Logic.dest_conjunctions)));
+
+        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
+        val binds =
+          (case_conclN, concl) :: dest_binops concls concl
+          |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
+      in
+       ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
+        ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
+      end;
+
+    val cases = map extract props;
+
+    fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
+      Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
+    fun inner_case (_, ((fixes2, assumes2), binds)) =
+      Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
+    fun nested_case ((fixes1, assumes1), _) =
+      Case {fixes = fixes1, assumes = assumes1, binds = [],
+        cases = map string_of_int (1 upto len) ~~ map inner_case cases};
+  in
+    if len = 0 then NONE
+    else if len = 1 then SOME (common_case (hd cases))
+    else if is_none case_outline orelse length (gen_distinct (op =) (map fst cases)) > 1 then NONE
+    else SOME (nested_case (hd cases))
+  end;
+
+fun make is_open rule_struct (thy, prop) cases =
+  let
+    val n = length cases;
+    val nprems = Logic.count_prems (prop, 0);
+    fun add_case (name, concls) (cs, i) =
+      ((case try (fn () =>
+          (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
+        NONE => (name, NONE)
+      | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
+  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
+
+in
+
+fun make_common is_open = make is_open NONE;
+fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
+fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])];
+
+fun apply args =
+  let
+    fun appl (Case {fixes, assumes, binds, cases}) =
+      let
+        val assumes' = map (apsnd (map (app args))) assumes;
+        val binds' = map (apsnd (Option.map (app args))) binds;
+        val cases' = map (apsnd appl) cases;
+      in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end;
+  in appl end;
+
+end;
+
+
+
+(** tactics with cases **)
+
 type cases_tactic = thm -> (cases * thm) Seq.seq;
 
 fun CASES cases tac st = Seq.map (pair cases) (tac st);
 fun NO_CASES tac = CASES [] tac;
 

     val cases =
       (case lookup_case_names th of
         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
       | SOME names => map (fn name => (name, get_case_concls th name)) names);
   in (cases, n) end;
-
-
-(* extract cases *)
-
-val case_conclN = "case";
-val case_hypsN = "hyps";
-val case_premsN = "prems";
-
-val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params;
-
-local
-
-fun dest_binops cs tm =
-  let
-    val n = length cs;
-    fun dest 0 _ = []
-      | dest 1 t = [t]
-      | dest k (_ $ t $ u) = t :: dest (k - 1) u
-      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
-  in cs ~~ dest n tm end;
-
-fun extract_cases is_open thy (split, raw_prop) name concls =
-  let
-    fun extract prop idx =
-      let
-        val xs = strip_params prop;
-        val rename = if is_open then I else map (apfst Syntax.internal);
-        val fixes =
-          (case split of
-            NONE => rename xs
-          | SOME t =>
-              let val (us, vs) = splitAt (length (Logic.strip_params t), xs)
-              in rename us @ vs end);
-        fun abs_fixes t = Term.list_abs (fixes, t);
-        val dest_conjuncts = map abs_fixes o List.concat o map Logic.dest_conjunctions;
-
-        val asms = Logic.strip_assums_hyp prop;
-        val assumes =
-          (case split of
-            NONE => [("", dest_conjuncts asms)]
-          | SOME t =>
-              let val (hyps, prems) = splitAt (length (Logic.strip_assums_hyp t), asms) in
-               [(case_hypsN, dest_conjuncts hyps),
-                (case_premsN, dest_conjuncts prems)]
-              end);
-
-        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
-        val binds = (case_conclN, concl) :: dest_binops concls concl
-          |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
-      in (name ^ idx, SOME {fixes = fixes, assumes = assumes, binds = binds}) end;
-  in
-    (case Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop) of
-      [prop] => [extract prop ""]
-    | props => map2 extract props (map string_of_int (1 upto length props)))
-  end;
-
-in
-
-fun make is_open split (thy, prop) cases =
-  let
-    val n = length cases;
-    val nprems = Logic.count_prems (prop, 0);
-    fun add_case (name, concls) (cs, i) =
-      ((case try (fn () =>
-          (Option.map (curry Logic.nth_prem i) split, Logic.nth_prem (i, prop))) () of
-        NONE => [(name, NONE)]
-      | SOME sp => extract_cases is_open thy sp name concls) @ cs, i - 1);
-  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
-
-fun simple (thy, prop) name =
-  extract_cases true thy (NONE, prop) name [];
-
-end;
 
 
 (* params *)
 
 fun rename_params xss th =