documentation for 'subgoal' command;
authorwenzelm
Thu Jul 02 14:09:43 2015 +0200 (2015-07-02)
changeset 60631441fdbfbb2d3
parent 60630 fc7625ec7427
child 60632 e096d5aaa0f8
documentation for 'subgoal' command;
NEWS
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/Proof_Script.thy
     1.1 --- a/NEWS	Thu Jul 02 12:39:08 2015 +0200
     1.2 +++ b/NEWS	Thu Jul 02 14:09:43 2015 +0200
     1.3 @@ -102,6 +102,11 @@
     1.4  is still available as legacy for some time. Documentation now explains
     1.5  '..' more accurately as "by standard" instead of "by rule".
     1.6  
     1.7 +* Command 'subgoal' allows to impose some structure on backward
     1.8 +refinements, to avoid proof scripts degenerating into long of 'apply'
     1.9 +sequences. Further explanations and examples are given in the isar-ref
    1.10 +manual.
    1.11 +
    1.12  * Proof method "goals" turns the current subgoals into cases within the
    1.13  context; the conclusion is bound to variable ?case in each case.
    1.14  For example:
     2.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Jul 02 12:39:08 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Jul 02 14:09:43 2015 +0200
     2.3 @@ -438,6 +438,9 @@
     2.4    @{rail \<open>
     2.5      @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
     2.6      ;
     2.7 +    @{syntax_def thmbind}:
     2.8 +      @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
     2.9 +    ;
    2.10      @{syntax_def thmdecl}: thmbind ':'
    2.11      ;
    2.12      @{syntax_def thmdef}: thmbind '='
    2.13 @@ -449,9 +452,6 @@
    2.14      ;
    2.15      @{syntax_def thmrefs}: @{syntax thmref} +
    2.16      ;
    2.17 -
    2.18 -    thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
    2.19 -    ;
    2.20      selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
    2.21    \<close>}
    2.22  \<close>
     3.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 12:39:08 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 14:09:43 2015 +0200
     3.3 @@ -88,6 +88,103 @@
     3.4  \<close>
     3.5  
     3.6  
     3.7 +section \<open>Explicit subgoal structure\<close>
     3.8 +
     3.9 +text \<open>
    3.10 +  \begin{matharray}{rcl}
    3.11 +    @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    3.12 +  \end{matharray}
    3.13 +
    3.14 +  @{rail \<open>
    3.15 +    @@{command subgoal} @{syntax thmbind}? prems? params?
    3.16 +    ;
    3.17 +    prems: @'premises' @{syntax thmbind}?
    3.18 +    ;
    3.19 +    params: @'for' '\<dots>'? (('_' | @{syntax name})+)
    3.20 +  \<close>}
    3.21 +
    3.22 +  \begin{description}
    3.23 +
    3.24 +  \item @{command "subgoal"} allows to impose some structure on backward
    3.25 +  refinements, to avoid proof scripts degenerating into long of @{command
    3.26 +  apply} sequences.
    3.27 +
    3.28 +  The current goal state, which is essentially a hidden part of the Isar/VM
    3.29 +  configurtation, is turned into a proof context and remaining conclusion.
    3.30 +  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
    3.31 +  structured proofs, but the text of the parameters, premises and conclusion
    3.32 +  is not given explicitly.
    3.33 +
    3.34 +  Goal parameters may be specified separately, in order to allow referring
    3.35 +  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
    3.36 +  y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
    3.37 +  "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
    3.38 +  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
    3.39 +  positions may be skipped via dummies (underscore). Unspecified names
    3.40 +  remain internal, and thus inaccessible in the proof text.
    3.41 +
    3.42 +  ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
    3.43 +  goal premises should be turned into assumptions of the context (otherwise
    3.44 +  the remaining conclusion is a Pure implication). The fact name and
    3.45 +  attributes are optional; the particular name ``@{text prems}'' is a common
    3.46 +  convention for the premises of an arbitrary goal context in proof scripts.
    3.47 +
    3.48 +  ``@{command subgoal}~@{text result}'' indicates a fact name for the result
    3.49 +  of a proven subgoal. Thus it may be re-used in further reasoning, similar
    3.50 +  to the result of @{command show} in structured Isar proofs.
    3.51 +
    3.52 +  \end{description}
    3.53 +
    3.54 +  Here are some abstract examples:
    3.55 +\<close>
    3.56 +
    3.57 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    3.58 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    3.59 +  subgoal sorry
    3.60 +  subgoal sorry
    3.61 +  done
    3.62 +
    3.63 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    3.64 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    3.65 +  subgoal for x y z sorry
    3.66 +  subgoal for u v sorry
    3.67 +  done
    3.68 +
    3.69 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    3.70 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    3.71 +  subgoal premises for x y z
    3.72 +    using \<open>A x\<close> \<open>B y\<close>
    3.73 +    sorry
    3.74 +  subgoal premises for u v
    3.75 +    using \<open>X u\<close>
    3.76 +    sorry
    3.77 +  done
    3.78 +
    3.79 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    3.80 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    3.81 +  subgoal r premises prems for x y z
    3.82 +  proof -
    3.83 +    have "A x" by (fact prems)
    3.84 +    moreover have "B y" by (fact prems)
    3.85 +    ultimately show ?thesis sorry
    3.86 +  qed
    3.87 +  subgoal premises prems for u v
    3.88 +  proof -
    3.89 +    have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
    3.90 +    moreover
    3.91 +    have "X u" by (fact prems)
    3.92 +    ultimately show ?thesis sorry
    3.93 +  qed
    3.94 +  done
    3.95 +
    3.96 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    3.97 +  subgoal premises prems for \<dots> z
    3.98 +  proof -
    3.99 +    from prems show "C z" sorry
   3.100 +  qed
   3.101 +  done
   3.102 +
   3.103 +
   3.104  section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
   3.105  
   3.106  text \<open>