# HG changeset patch
# User wenzelm
# Date 1435778997 -7200
# Node ID be39fe6c5620ee74f565975a6bec8248e865438e
# Parent  57b5293bceacc38d2ff9d1ec5d5e845e8dc28aa8
support for subgoal focus command;

diff -r 57b5293bceac -r be39fe6c5620 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Wed Jul 01 21:29:57 2015 +0200
@@ -9,7 +9,6 @@
 keywords
   "method" :: thy_decl and
   "conclusion"
-  "premises"
   "declares"
   "methods"
   "\<bar>" "\<Rightarrow>"
diff -r 57b5293bceac -r be39fe6c5620 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 01 21:29:57 2015 +0200
@@ -679,6 +679,32 @@
         Toplevel.skip_proof (fn i => i + 1))));
 
 
+(* subgoal focus *)
+
+local
+
+val opt_fact_binding =
+  Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+    Attrib.empty_binding;
+
+val params =
+  Parse.binding -- Parse.mixfix' >> single || Scan.repeat1 Parse.binding >> map (rpair NoSyn);
+
+val for_params =
+  Scan.optional (@{keyword "for"} |-- Parse.!!! (Parse.and_list1 params >> flat)) [];
+
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword subgoal}
+    "focus on first subgoal within backward refinement"
+    (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+      for_params >> (fn ((a, b), c) =>
+        Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
+
+end;
+
+
 (* proof navigation *)
 
 fun report_back () =
diff -r 57b5293bceac -r be39fe6c5620 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 01 21:29:57 2015 +0200
@@ -33,10 +33,12 @@
   val enter_chain: state -> state
   val enter_backward: state -> state
   val has_bottom_goal: state -> bool
+  val using_facts: thm list -> state -> state
   val pretty_state: state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
+  val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
@@ -430,6 +432,9 @@
 fun refine_insert ths =
   Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
+fun refine_primitive r =  (* FIXME Seq.Error!? *)
+  Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+
 end;
 
 
diff -r 57b5293bceac -r be39fe6c5620 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Pure.thy	Wed Jul 01 21:29:57 2015 +0200
@@ -11,7 +11,7 @@
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "private" "qualified" "shows"
+    "overloaded" "pervasive" "premises" "private" "qualified" "shows"
     "structure" "unchecked" "where" "when" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
@@ -69,6 +69,7 @@
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof" == ""
+  and "subgoal" :: prf_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
diff -r 57b5293bceac -r be39fe6c5620 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/conjunction.ML	Wed Jul 01 21:29:57 2015 +0200
@@ -19,6 +19,7 @@
   val intr: thm -> thm -> thm
   val intr_balanced: thm list -> thm
   val elim: thm -> thm * thm
+  val elim_conjunctions: thm -> thm list
   val elim_balanced: int -> thm -> thm list
   val curry_balanced: int -> thm -> thm
   val uncurry_balanced: int -> thm -> thm
@@ -118,6 +119,11 @@
 
 end;
 
+fun elim_conjunctions th =
+  (case try elim th of
+    NONE => [th]
+  | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
+
 
 (* balanced conjuncts *)
 
diff -r 57b5293bceac -r be39fe6c5620 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/subgoal.ML	Wed Jul 01 21:29:57 2015 +0200
@@ -1,9 +1,13 @@
 (*  Title:      Pure/subgoal.ML
     Author:     Makarius
+    Author:     Daniel Matichuk, NICTA/UNSW
 
 Tactical operations with explicit subgoal focus, based on canonical
 proof decomposition.  The "visible" part of the text within the
 context is fixed, the remaining goal may be schematic.
+
+Isar subgoal command for proof structure within unstructured proof
+scripts.
 *)
 
 signature SUBGOAL =
@@ -19,6 +23,10 @@
   val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
+  val subgoal: Attrib.binding -> Attrib.binding option -> (binding * mixfix) list ->
+    Proof.state -> focus * Proof.state
+  val subgoal_cmd: Attrib.binding -> Attrib.binding option -> (binding * mixfix) list ->
+    Proof.state -> focus * Proof.state
 end;
 
 structure Subgoal: SUBGOAL =
@@ -146,7 +154,64 @@
 
 fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
 
+
+(* Isar subgoal command *)
+
+local
+
+fun gen_focus prep_atts raw_result_binding raw_prems_binding params state =
+  let
+    val _ = Proof.assert_backward state;
+    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state;
+
+    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
+    val (prems_binding, do_prems) =
+      (case raw_prems_binding of
+        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
+      | NONE => ((Binding.empty, []), false));
+
+    fun check_param (b, mx) = ignore (Proof_Context.cert_var (b, NONE, mx) ctxt);
+    val _ = List.app check_param params;
+
+    val _ = if Thm.no_prems st then error "No subgoals!" else ();
+    val subgoal_focus = #1 (focus ctxt 1 st);  (* FIXME clarify prems/params *)
+
+    fun after_qed (ctxt'', [[result]]) =
+      Proof.end_block #> (fn state' =>
+        let
+          val ctxt' = Proof.context_of state';
+          val results' =
+            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
+        in
+          state'
+          |> Proof.refine_primitive (fn _ => fn _ =>
+            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
+              (Goal.protect 0 result) st
+            |> Seq.hd)
+          |> Proof.map_context
+            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
+        end);
+  in
+    state
+    |> Proof.enter_forward
+    |> Proof.using_facts []
+    |> Proof.begin_block
+    |> Proof.map_context (fn _ =>
+      #context subgoal_focus
+      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
+        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
+    |> Proof.using_facts facts
+    |> pair subgoal_focus
+  end;
+
+in
+
+val subgoal = gen_focus Attrib.attribute;
+val subgoal_cmd = gen_focus Attrib.attribute_cmd;
+
+end;
+
 end;
 
 val SUBPROOF = Subgoal.SUBPROOF;
-