# HG changeset patch
# User wenzelm
# Date 1435261500 -7200
# Node ID c708dafe2220d65ba674ffbbd1d1a4fcaca29999
# Parent  4c9401fbbdf7c5dbed204535d4aff50df89c5945
added method "goals" for proper subgoal cases;

diff -r 4c9401fbbdf7 -r c708dafe2220 NEWS
--- a/NEWS	Thu Jun 25 16:56:04 2015 +0200
+++ b/NEWS	Thu Jun 25 21:45:00 2015 +0200
@@ -77,6 +77,9 @@
 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
 and always put attributes in front.
 
+* Proof method "goals" turns the current subgoals into cases within the
+context; the conclusion is bound to variable ?case in each case.
+
 * Nesting of Isar goal structure has been clarified: the context after
 the initial backwards refinement is retained for the whole proof, within
 all its context sections (as indicated via 'next'). This is e.g.
diff -r 4c9401fbbdf7 -r c708dafe2220 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 16:56:04 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Thu Jun 25 21:45:00 2015 +0200
@@ -818,6 +818,7 @@
   \begin{matharray}{rcl}
     @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     @{method_def "-"} & : & @{text method} \\
+    @{method_def "goals"} & : & @{text method} \\
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
@@ -832,6 +833,8 @@
   \end{matharray}
 
   @{rail \<open>
+    @@{method goals} (@{syntax name}*)
+    ;
     @@{method fact} @{syntax thmrefs}?
     ;
     @@{method (Pure) rule} @{syntax thmrefs}?
@@ -861,12 +864,23 @@
   rule declarations of the classical reasoner
   (\secref{sec:classical}).
 
-  \item ``@{method "-"}'' (minus) does nothing but insert the forward
-  chaining facts as premises into the goal.  Note that command
-  @{command_ref "proof"} without any method actually performs a single
-  reduction step using the @{method_ref (Pure) rule} method; thus a plain
-  \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
-  "-"}'' rather than @{command "proof"} alone.
+  \item ``@{method "-"}'' (minus) inserts the forward chaining facts as
+  premises into the goal, and nothing else.
+
+  Note that command @{command_ref "proof"} without any method actually
+  performs a single reduction step using the @{method_ref (Pure) rule}
+  method; thus a plain \emph{do-nothing} proof step would be ``@{command
+  "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
+
+  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} is like ``@{method "-"}'', but
+  the current subgoals are turned into cases within the context (see also
+  \secref{sec:cases-induct}). The specified case names are used if present;
+  otherwise cases are numbered starting from 1.
+
+  Invoking cases in the subsequent proof body via the @{command_ref case}
+  command will @{command fix} goal parameters, @{command assume} goal
+  premises, and @{command let} variable @{variable_ref ?case} refer to the
+  conclusion.
 
   \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
   @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
diff -r 4c9401fbbdf7 -r c708dafe2220 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jun 25 16:56:04 2015 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jun 25 21:45:00 2015 +0200
@@ -17,6 +17,7 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
+  val goals_tac: Proof.context -> string list -> cases_tactic
   val cheating: Proof.context -> bool -> method
   val intro: Proof.context -> thm list -> method
   val elim: Proof.context -> thm list -> method
@@ -126,6 +127,17 @@
 end;
 
 
+(* goals as cases *)
+
+fun goals_tac ctxt case_names st =
+  let
+    val cases =
+      (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
+      |> map (rpair [] o rpair [])
+      |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
+  in Seq.single (cases, st) end;
+
+
 (* cheating *)
 
 fun cheating ctxt int = METHOD (fn _ => fn st =>
@@ -676,9 +688,21 @@
   setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
     "succeed after delay (in seconds)" #>
   setup @{binding "-"} (Scan.succeed (K insert_facts))
-    "do nothing (insert current facts only)" #>
+    "insert current facts, nothing else" #>
+  setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
+    METHOD_CASES (fn facts =>
+      Seq.THEN (ALLGOALS (insert_tac facts), fn st =>
+        let
+          val _ =
+            (case drop (Thm.nprems_of st) names of
+              [] => ()
+            | bad => (* FIXME Seq.Error *)
+                error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+                  Position.here (Position.set_range (Token.range_of bad))));
+        in goals_tac ctxt (map Token.content_of names) st end))))
+    "insert facts and bind cases for goals" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))
-    "insert theorems, ignoring facts (improper)" #>
+    "insert theorems, ignoring facts" #>
   setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
     "repeatedly apply introduction rules" #>
   setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))