# HG changeset patch
# User wenzelm
# Date 1434208445 -7200
# Node ID 0c4077939278df9ebc5765d7c0cf0c4ded1c647c
# Parent  a4c6b278f3a7edeeb3a4bd55d95efc727ab89391
implicit rule for method "cases";

diff -r a4c6b278f3a7 -r 0c4077939278 NEWS
--- a/NEWS	Sat Jun 13 16:35:27 2015 +0200
+++ b/NEWS	Sat Jun 13 17:14:05 2015 +0200
@@ -38,6 +38,22 @@
 * New command 'supply' supports fact definitions during goal refinement
 ('apply' scripts).
 
+* Proof method "cases" allows to specify the rule as first entry of
+chained facts.  This is particularly useful with 'consider':
+
+  consider (a) A | (b) B | (c) C <proof>
+  then have something
+  proof cases
+    case a
+    then show ?thesis <proof>
+  next
+    case b
+    then show ?thesis <proof>
+  next
+    case c
+    then show ?thesis <proof>
+  qed
+
 
 *** Pure ***
 
diff -r a4c6b278f3a7 -r 0c4077939278 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 16:35:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 17:14:05 2015 +0200
@@ -1370,6 +1370,7 @@
   \medskip
   \begin{tabular}{llll}
     facts           &                 & arguments   & rule \\\hline
+    @{text "\<turnstile> R"}   & @{method cases} &             & implicit rule @{text R} \\
                     & @{method cases} &             & classical case split \\
                     & @{method cases} & @{text t}   & datatype exhaustion (type of @{text t}) \\
     @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
diff -r a4c6b278f3a7 -r 0c4077939278 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Jun 13 16:35:27 2015 +0200
+++ b/src/Tools/induct.ML	Sat Jun 13 17:14:05 2015 +0200
@@ -483,25 +483,32 @@
       |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
       |> pair (Rule_Cases.get r);
 
+    val (opt_rule', facts') =
+      (case (opt_rule, facts) of
+        (NONE, th :: ths) =>
+          if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
+          else (opt_rule, facts)
+      | _ => (opt_rule, facts));
+
     val ruleq =
-      (case opt_rule of
+      (case opt_rule' of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
-          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
+          (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
           |> tap (trace_rules ctxt casesN)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   in
     fn i => fn st =>
       ruleq
-      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
-      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
+      |> Seq.maps (Rule_Cases.consume ctxt [] facts')
+      |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
         let
           val rule' = rule
             |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
         in
           CASES (Rule_Cases.make_common ctxt
               (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
+            ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
                 (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
         end)
   end;