# HG changeset patch
# User wenzelm
# Date 1435838983 -7200
# Node ID 441fdbfbb2d3dd874cbc6b869377e4346cc00964
# Parent  fc7625ec742748b95adc13796a631b97baf53734
documentation for 'subgoal' command;

diff -r fc7625ec7427 -r 441fdbfbb2d3 NEWS
--- a/NEWS	Thu Jul 02 12:39:08 2015 +0200
+++ b/NEWS	Thu Jul 02 14:09:43 2015 +0200
@@ -102,6 +102,11 @@
 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:
diff -r fc7625ec7427 -r 441fdbfbb2d3 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Jul 02 12:39:08 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Jul 02 14:09:43 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 fc7625ec7427 -r 441fdbfbb2d3 src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 12:39:08 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 14:09:43 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>