# HG changeset patch
# User wenzelm
# Date 1435839042 -7200
# Node ID f758c40e0a9a10604cd8af82dd2e5bb0b305b910
# Parent  bfb14ff434911d8e81a22042cb9201016d3bbe2a# Parent  e096d5aaa0f8f88a6b7323bfd46891c049ffdb18
merged

diff -r bfb14ff43491 -r f758c40e0a9a CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Jul 01 13:09:56 2015 +0200
+++ b/CONTRIBUTORS	Thu Jul 02 14:10:42 2015 +0200
@@ -6,13 +6,16 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
+  Isar subgoal command for proof structure within unstructured proof
+  scripts.
+
 * Summer 2015: Florian Haftmann, TUM
-  Generic partial division in rings as inverse operation
-  of multiplication.
+  Generic partial division in rings as inverse operation of multiplication.
 
 * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
-  Type class hierarchy with common algebraic notions of
-  integral (semi)domains like units and associated elements.
+  Type class hierarchy with common algebraic notions of integral
+  (semi)domains like units and associated elements.
 
 
 Contributions to Isabelle2015
diff -r bfb14ff43491 -r f758c40e0a9a NEWS
--- a/NEWS	Wed Jul 01 13:09:56 2015 +0200
+++ b/NEWS	Thu Jul 02 14:10:42 2015 +0200
@@ -102,12 +102,27 @@
 is still available as legacy for some time. Documentation now explains
 '..' more accurately as "by standard" instead of "by rule".
 
+* Command 'subgoal' allows to impose some structure on backward
+refinements, to avoid proof scripts degenerating into long of 'apply'
+sequences. Further explanations and examples are given in the isar-ref
+manual.
+
 * Proof method "goals" turns the current subgoals into cases within the
 context; the conclusion is bound to variable ?case in each case.
 For example:
 
 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
-  and "\<And>y z. U y \<Longrightarrow> V u \<Longrightarrow> W y z"
+  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
+proof goals
+  case (1 x)
+  then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
+next
+  case (2 y z)
+  then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
+qed
+
+lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
+  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
 proof goals
   case prems: 1
   then show ?case using prems sorry
diff -r bfb14ff43491 -r f758c40e0a9a src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Jul 02 14:10:42 2015 +0200
@@ -438,6 +438,9 @@
   @{rail \<open>
     @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
     ;
+    @{syntax_def thmbind}:
+      @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
+    ;
     @{syntax_def thmdecl}: thmbind ':'
     ;
     @{syntax_def thmdef}: thmbind '='
@@ -449,9 +452,6 @@
     ;
     @{syntax_def thmrefs}: @{syntax thmref} +
     ;
-
-    thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
-    ;
     selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
   \<close>}
 \<close>
diff -r bfb14ff43491 -r f758c40e0a9a src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 14:10:42 2015 +0200
@@ -88,6 +88,103 @@
 \<close>
 
 
+section \<open>Explicit subgoal structure\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+  \end{matharray}
+
+  @{rail \<open>
+    @@{command subgoal} @{syntax thmbind}? prems? params?
+    ;
+    prems: @'premises' @{syntax thmbind}?
+    ;
+    params: @'for' '\<dots>'? (('_' | @{syntax name})+)
+  \<close>}
+
+  \begin{description}
+
+  \item @{command "subgoal"} allows to impose some structure on backward
+  refinements, to avoid proof scripts degenerating into long of @{command
+  apply} sequences.
+
+  The current goal state, which is essentially a hidden part of the Isar/VM
+  configurtation, is turned into a proof context and remaining conclusion.
+  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
+  structured proofs, but the text of the parameters, premises and conclusion
+  is not given explicitly.
+
+  Goal parameters may be specified separately, in order to allow referring
+  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
+  y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
+  "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
+  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
+  positions may be skipped via dummies (underscore). Unspecified names
+  remain internal, and thus inaccessible in the proof text.
+
+  ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
+  goal premises should be turned into assumptions of the context (otherwise
+  the remaining conclusion is a Pure implication). The fact name and
+  attributes are optional; the particular name ``@{text prems}'' is a common
+  convention for the premises of an arbitrary goal context in proof scripts.
+
+  ``@{command subgoal}~@{text result}'' indicates a fact name for the result
+  of a proven subgoal. Thus it may be re-used in further reasoning, similar
+  to the result of @{command show} in structured Isar proofs.
+
+  \end{description}
+
+  Here are some abstract examples:
+\<close>
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+  and "\<And>u v. X u \<Longrightarrow> Y v"
+  subgoal sorry
+  subgoal sorry
+  done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+  and "\<And>u v. X u \<Longrightarrow> Y v"
+  subgoal for x y z sorry
+  subgoal for u v sorry
+  done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+  and "\<And>u v. X u \<Longrightarrow> Y v"
+  subgoal premises for x y z
+    using \<open>A x\<close> \<open>B y\<close>
+    sorry
+  subgoal premises for u v
+    using \<open>X u\<close>
+    sorry
+  done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+  and "\<And>u v. X u \<Longrightarrow> Y v"
+  subgoal r premises prems for x y z
+  proof -
+    have "A x" by (fact prems)
+    moreover have "B y" by (fact prems)
+    ultimately show ?thesis sorry
+  qed
+  subgoal premises prems for u v
+  proof -
+    have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
+    moreover
+    have "X u" by (fact prems)
+    ultimately show ?thesis sorry
+  qed
+  done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+  subgoal premises prems for \<dots> z
+  proof -
+    from prems show "C z" sorry
+  qed
+  done
+
+
 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
 
 text \<open>
diff -r bfb14ff43491 -r f758c40e0a9a src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Thu Jul 02 14:10:42 2015 +0200
@@ -9,7 +9,6 @@
 keywords
   "method" :: thy_decl and
   "conclusion"
-  "premises"
   "declares"
   "methods"
   "\<bar>" "\<Rightarrow>"
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -679,6 +679,33 @@
         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 for_params =
+  Scan.optional
+    (@{keyword "for"} |--
+      Parse.!!! ((Scan.option Parse.dots >> is_some) --
+        (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
+    (false, []);
+
+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 bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/keyword.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -28,8 +28,9 @@
   val prf_decl: string
   val prf_asm: string
   val prf_asm_goal: string
-  val prf_asm_goal_script: string
   val prf_script: string
+  val prf_script_goal: string
+  val prf_script_asm_goal: string
   type spec = (string * string list) * string list
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
@@ -95,13 +96,15 @@
 val prf_decl = "prf_decl";
 val prf_asm = "prf_asm";
 val prf_asm_goal = "prf_asm_goal";
-val prf_asm_goal_script = "prf_asm_goal_script";
 val prf_script = "prf_script";
+val prf_script_goal = "prf_script_goal";
+val prf_script_asm_goal = "prf_script_asm_goal";
 
 val kinds =
   [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
     thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 
 (* specifications *)
@@ -239,19 +242,21 @@
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 val is_proof_body = command_category
   [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
 val is_proof_asm = command_category [prf_asm, prf_asm_goal];
-val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
 
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/keyword.scala	Thu Jul 02 14:10:42 2015 +0200
@@ -35,8 +35,9 @@
   val PRF_DECL = "prf_decl"
   val PRF_ASM = "prf_asm"
   val PRF_ASM_GOAL = "prf_asm_goal"
-  val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
   val PRF_SCRIPT = "prf_script"
+  val PRF_SCRIPT_GOAL = "prf_script_goal"
+  val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
 
 
   /* command categories */
@@ -63,14 +64,16 @@
 
   val proof =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+      PRF_SCRIPT_ASM_GOAL)
 
   val proof_body =
     Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+      PRF_SCRIPT_ASM_GOAL)
 
   val theory_goal = Set(THY_GOAL)
-  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   val qed_global = Set(QED_GLOBAL)
 
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -23,6 +23,7 @@
   val short_ident: string parser
   val long_ident: string parser
   val sym_ident: string parser
+  val dots: string parser
   val minus: string parser
   val term_var: string parser
   val type_ident: string parser
@@ -220,7 +221,10 @@
   group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
+val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;
 
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 02 14:10:42 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 bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -1241,7 +1241,7 @@
 
 val apply_case = apfst fst oo case_result;
 
-fun check_case ctxt internal (name, pos) fxs =
+fun check_case ctxt internal (name, pos) param_specs =
   let
     val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
@@ -1251,12 +1251,12 @@
           " -- use proof method \"goals\" instead")
       else ();
 
-    val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
+    val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] =
           error ("Too many parameters for case " ^ quote name ^ Position.here pos);
-    val fixes' = replace fxs fixes;
+    val fixes' = replace param_specs fixes;
     val binds' = map drop_schematic binds;
   in
     if null (fold (Term.add_tvarsT o snd) fixes []) andalso
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Isar/subgoal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/subgoal.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -0,0 +1,256 @@
+(*  Title:      Pure/Isar/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 =
+sig
+  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+  val focus_params: Proof.context -> int -> thm -> focus * thm
+  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
+  val focus_prems: Proof.context -> int -> thm -> focus * thm
+  val focus: Proof.context -> int -> thm -> focus * thm
+  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
+    int -> thm -> thm -> thm Seq.seq
+  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
+  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 ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+end;
+
+structure Subgoal: SUBGOAL =
+struct
+
+(* focus *)
+
+type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
+
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
+  let
+    val st = raw_st
+      |> Thm.transfer (Proof_Context.theory_of ctxt)
+      |> Raw_Simplifier.norm_hhf_protect ctxt;
+    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
+
+    val (asms, concl) =
+      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+      else ([], goal);
+    val text = asms @ (if do_concl then [concl] else []);
+
+    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
+
+    val schematics = (schematic_types, schematic_terms);
+    val asms' = map (Thm.instantiate_cterm schematics) asms;
+    val concl' = Thm.instantiate_cterm schematics concl;
+    val (prems, context) = Assumption.add_assumes asms' ctxt3;
+  in
+    ({context = context, params = params, prems = prems,
+      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
+  end;
+
+val focus_params = gen_focus (false, false);
+val focus_params_fixed = gen_focus (false, true);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
+
+
+(* lift and retrofit *)
+
+(*
+     B [?'b, ?y]
+  ----------------
+  B ['b, y params]
+*)
+fun lift_import idx params th ctxt =
+  let
+    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
+
+    val Ts = map Thm.typ_of_cterm params;
+    val ts = map Thm.term_of params;
+
+    val prop = Thm.full_prop_of th';
+    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+    val vars = rev (Term.add_vars prop []);
+    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
+
+    fun var_inst v y =
+      let
+        val ((x, i), T) = v;
+        val (U, args) =
+          if member (op =) concl_vars v then (T, [])
+          else (Ts ---> T, ts);
+        val u = Free (y, U);
+        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
+    val (inst1, inst2) =
+      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
+
+    val th'' = Thm.instantiate ([], inst1) th';
+  in ((inst2, th''), ctxt'') end;
+
+(*
+       [x, A x]
+          :
+       B x ==> C
+  ------------------
+  [!!x. A x ==> B x]
+          :
+          C
+*)
+fun lift_subgoals params asms th =
+  let
+    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
+    val unlift =
+      fold (Thm.elim_implies o Thm.assume) asms o
+      Drule.forall_elim_list (map #2 params) o Thm.assume;
+    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
+    val th' = fold (Thm.elim_implies o unlift) subgoals th;
+  in (subgoals, th') end;
+
+fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
+  let
+    val idx = Thm.maxidx_of st0 + 1;
+    val ps = map #2 params;
+    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
+    val (subgoals, st3) = lift_subgoals params asms st2;
+    val result = st3
+      |> Goal.conclude
+      |> Drule.implies_intr_list asms
+      |> Drule.forall_intr_list ps
+      |> Drule.implies_intr_list subgoals
+      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
+      |> fold (Thm.forall_elim o #2) subgoal_inst
+      |> Thm.adjust_maxidx_thm idx
+      |> singleton (Variable.export ctxt2 ctxt0);
+  in
+    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
+      (false, result, Thm.nprems_of st1) i st0
+  end;
+
+
+(* tacticals *)
+
+fun GEN_FOCUS flags tac ctxt i st =
+  if Thm.nprems_of st < i then Seq.empty
+  else
+    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
+    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
+
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
+
+fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
+
+
+(* Isar subgoal command *)
+
+local
+
+fun rename_params ctxt (param_suffix, raw_param_specs) st =
+  let
+    val _ = if Thm.no_prems st then error "No subgoals!" else ();
+    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
+    val subgoal_params =
+      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
+      |> Term.variant_frees subgoal |> map #1;
+
+    val n = length subgoal_params;
+    val m = length raw_param_specs;
+    val _ =
+      m <= n orelse
+        error ("Excessive subgoal parameter specification" ^
+          Position.here_list (map snd (drop n raw_param_specs)));
+
+    val param_specs =
+      raw_param_specs |> map
+        (fn (NONE, _) => NONE
+          | (SOME x, pos) =>
+              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
+              in SOME (Variable.check_name b) end)
+      |> param_suffix ? append (replicate (n - m) NONE);
+
+    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
+      | rename_list _ ys = ys;
+
+    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
+          (c $ Abs (x, T, rename_prop xs t))
+      | rename_prop [] t = t;
+
+    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
+  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
+
+fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+  let
+    val _ = Proof.assert_backward state;
+
+    val state1 = state |> Proof.refine_insert [];
+    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
+
+    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));
+
+    val (subgoal_focus, _) =
+      rename_params ctxt param_specs st
+      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
+
+    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)
+      #> Proof.reset_facts
+      #> Proof.enter_backward;
+  in
+    state1
+    |> 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_subgoal Attrib.attribute;
+val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
+
+end;
+
+end;
+
+val SUBPROOF = Subgoal.SUBPROOF;
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Pure.thy	Thu Jul 02 14:10:42 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
@@ -57,7 +57,7 @@
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
   and "consider" :: prf_goal % "proof"
   and "obtain" :: prf_asm_goal % "proof"
-  and "guess" :: prf_asm_goal_script % "proof"
+  and "guess" :: prf_script_asm_goal % "proof"
   and "let" "write" :: prf_decl % "proof"
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
@@ -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_script_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/ROOT	Thu Jul 02 14:10:42 2015 +0200
@@ -145,6 +145,7 @@
     "Isar/runtime.ML"
     "Isar/spec_rules.ML"
     "Isar/specification.ML"
+    "Isar/subgoal.ML"
     "Isar/token.ML"
     "Isar/toplevel.ML"
     "Isar/typedecl.ML"
@@ -253,7 +254,6 @@
     "simplifier.ML"
     "skip_proof.ML"
     "sorts.ML"
-    "subgoal.ML"
     "tactic.ML"
     "tactical.ML"
     "term.ML"
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 02 14:10:42 2015 +0200
@@ -262,6 +262,7 @@
 use "Isar/proof.ML";
 use "Isar/element.ML";
 use "Isar/obtain.ML";
+use "Isar/subgoal.ML";
 
 (*local theories and targets*)
 use "Isar/locale.ML";
@@ -317,8 +318,6 @@
 (*theory and proof operations*)
 use "Isar/isar_cmd.ML";
 
-use "subgoal.ML";
-
 
 (* Isabelle/Isar system *)
 
diff -r bfb14ff43491 -r f758c40e0a9a src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/conjunction.ML	Thu Jul 02 14:10:42 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 bfb14ff43491 -r f758c40e0a9a src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jul 01 13:09:56 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-(*  Title:      Pure/subgoal.ML
-    Author:     Makarius
-
-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.
-*)
-
-signature SUBGOAL =
-sig
-  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
-  val focus_params: Proof.context -> int -> thm -> focus * thm
-  val focus_prems: Proof.context -> int -> thm -> focus * thm
-  val focus: Proof.context -> int -> thm -> focus * thm
-  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
-    int -> thm -> thm -> thm Seq.seq
-  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
-  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
-end;
-
-structure Subgoal: SUBGOAL =
-struct
-
-(* focus *)
-
-type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
-
-fun gen_focus (do_prems, do_concl) ctxt i raw_st =
-  let
-    val st = raw_st
-      |> Thm.transfer (Proof_Context.theory_of ctxt)
-      |> Simplifier.norm_hhf_protect ctxt;
-    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
-    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
-
-    val (asms, concl) =
-      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
-      else ([], goal);
-    val text = asms @ (if do_concl then [concl] else []);
-
-    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
-    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
-
-    val schematics = (schematic_types, schematic_terms);
-    val asms' = map (Thm.instantiate_cterm schematics) asms;
-    val concl' = Thm.instantiate_cterm schematics concl;
-    val (prems, context) = Assumption.add_assumes asms' ctxt3;
-  in
-    ({context = context, params = params, prems = prems,
-      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
-  end;
-
-val focus_params = gen_focus (false, false);
-val focus_prems = gen_focus (true, false);
-val focus = gen_focus (true, true);
-
-
-(* lift and retrofit *)
-
-(*
-     B [?'b, ?y]
-  ----------------
-  B ['b, y params]
-*)
-fun lift_import idx params th ctxt =
-  let
-    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
-
-    val Ts = map Thm.typ_of_cterm params;
-    val ts = map Thm.term_of params;
-
-    val prop = Thm.full_prop_of th';
-    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
-    val vars = rev (Term.add_vars prop []);
-    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
-
-    fun var_inst v y =
-      let
-        val ((x, i), T) = v;
-        val (U, args) =
-          if member (op =) concl_vars v then (T, [])
-          else (Ts ---> T, ts);
-        val u = Free (y, U);
-        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
-    val (inst1, inst2) =
-      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
-
-    val th'' = Thm.instantiate ([], inst1) th';
-  in ((inst2, th''), ctxt'') end;
-
-(*
-       [x, A x]
-          :
-       B x ==> C
-  ------------------
-  [!!x. A x ==> B x]
-          :
-          C
-*)
-fun lift_subgoals params asms th =
-  let
-    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
-    val unlift =
-      fold (Thm.elim_implies o Thm.assume) asms o
-      Drule.forall_elim_list (map #2 params) o Thm.assume;
-    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
-    val th' = fold (Thm.elim_implies o unlift) subgoals th;
-  in (subgoals, th') end;
-
-fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
-  let
-    val idx = Thm.maxidx_of st0 + 1;
-    val ps = map #2 params;
-    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
-    val (subgoals, st3) = lift_subgoals params asms st2;
-    val result = st3
-      |> Goal.conclude
-      |> Drule.implies_intr_list asms
-      |> Drule.forall_intr_list ps
-      |> Drule.implies_intr_list subgoals
-      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
-      |> fold (Thm.forall_elim o #2) subgoal_inst
-      |> Thm.adjust_maxidx_thm idx
-      |> singleton (Variable.export ctxt2 ctxt0);
-  in
-    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
-      (false, result, Thm.nprems_of st1) i st0
-  end;
-
-
-(* tacticals *)
-
-fun GEN_FOCUS flags tac ctxt i st =
-  if Thm.nprems_of st < i then Seq.empty
-  else
-    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
-    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
-
-val FOCUS_PARAMS = GEN_FOCUS (false, false);
-val FOCUS_PREMS = GEN_FOCUS (true, false);
-val FOCUS = GEN_FOCUS (true, true);
-
-fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
-
-end;
-
-val SUBPROOF = Subgoal.SUBPROOF;
-