# HG changeset patch
# User wenzelm
# Date 1468622313 -7200
# Node ID 9f8d06f23c09828e4317c83a04a58580836118d2
# Parent  1c7b1e294fb5fd47494b99aac6efef8366b65a6f
information about proof outline with cases (sendback);

diff -r 1c7b1e294fb5 -r 9f8d06f23c09 NEWS
--- a/NEWS	Sat Jul 16 00:11:03 2016 +0200
+++ b/NEWS	Sat Jul 16 00:38:33 2016 +0200
@@ -100,6 +100,9 @@
 established at the end of a proof are properly identified in the theorem
 statement.
 
+* Command 'proof' provides information about proof outline with cases,
+e.g. for proof methods "cases", "induct", "goal_cases".
+
 
 *** Isar ***
 
diff -r 1c7b1e294fb5 -r 9f8d06f23c09 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jul 16 00:11:03 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jul 16 00:38:33 2016 +0200
@@ -144,7 +144,7 @@
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val dest_cases: Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
+  val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -188,6 +188,7 @@
   val pretty_local_facts: bool -> Proof.context -> Pretty.T list
   val print_local_facts: bool -> Proof.context -> unit
   val pretty_cases: Proof.context -> Pretty.T list
+  val print_cases_proof: Proof.context -> Proof.context -> string
   val debug: bool Config.T
   val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
@@ -1272,9 +1273,18 @@
 
 (** cases **)
 
-fun dest_cases ctxt =
-  Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
-  |> sort (int_ord o apply2 #1) |> map #2;
+fun dest_cases prev_ctxt ctxt =
+  let
+    val ignored =
+      (case prev_ctxt of
+        NONE => Inttab.empty
+      | SOME ctxt0 =>
+          Name_Space.fold_table (Inttab.insert_set o #2 o #2) (cases_of ctxt0) Inttab.empty);
+  in
+    Name_Space.fold_table (fn (a, (c, i)) =>
+      not (Inttab.defined ignored i) ? cons (i, (a, c))) (cases_of ctxt) []
+    |> sort (int_ord o apply2 #1) |> map #2
+  end;
 
 local
 
@@ -1469,7 +1479,7 @@
   Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
 
 
-(* local contexts *)
+(* named local contexts *)
 
 local
 
@@ -1508,7 +1518,7 @@
     fun mk_case (_, (_, {legacy = true})) = NONE
       | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
           SOME (name, (fixes, case_result c ctxt));
-    val cases = dest_cases ctxt |> map_filter mk_case;
+    val cases = dest_cases NONE ctxt |> map_filter mk_case;
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]
@@ -1516,6 +1526,34 @@
 
 end;
 
+fun print_cases_proof ctxt0 ctxt =
+  let
+    fun print_case name [] = name
+      | print_case name xs = enclose "(" ")" (space_implode " " (name :: map Name.clean xs));
+
+    fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
+      if legacy then NONE
+      else
+        let
+          val concl =
+            if exists (fn ((x, _), SOME t) =>
+              x = Rule_Cases.case_conclN andalso Term.maxidx_of_term t = ~1 | _ => false) binds
+            then Rule_Cases.case_conclN
+            else Auto_Bind.thesisN;
+        in
+          SOME (cat_lines
+            ["  case " ^ print_case name (map (Name.clean o Binding.name_of o #1) fixes),
+             "  then show ?" ^ concl ^ " sorry"])
+        end;
+  in
+    (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
+      [] => ""
+    | proofs =>
+        "Proof outline with cases:\n" ^
+        Active.sendback_markup [Markup.padding_command]
+          (space_implode "\nnext\n" proofs ^ "\nqed"))
+  end;
+
 
 (* core context *)
 
diff -r 1c7b1e294fb5 -r 9f8d06f23c09 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Jul 16 00:11:03 2016 +0200
+++ b/src/Pure/Pure.thy	Sat Jul 16 00:38:33 2016 +0200
@@ -902,7 +902,14 @@
 val _ =
   Outer_Syntax.command @{command_keyword proof} "backward proof step"
     (Scan.option Method.parse >> (fn m =>
-      (Option.map Method.report m; Toplevel.proof (Proof.proof m #> Seq.the_result ""))));
+      (Option.map Method.report m;
+       Toplevel.proof (fn state =>
+         let
+          val state' = state |> Proof.proof m |> Seq.the_result "";
+          val _ =
+            Output.information
+              (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
+        in state' end))))
 
 in end\<close>