src/Doc/Isar_Ref/Proof_Script.thy
changeset 60631 441fdbfbb2d3
parent 60484 98ee86354354
child 61439 2bf52eec4e8a
     1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 12:39:08 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Jul 02 14:09:43 2015 +0200
     1.3 @@ -88,6 +88,103 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 +section \<open>Explicit subgoal structure\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  \begin{matharray}{rcl}
    1.11 +    @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    1.12 +  \end{matharray}
    1.13 +
    1.14 +  @{rail \<open>
    1.15 +    @@{command subgoal} @{syntax thmbind}? prems? params?
    1.16 +    ;
    1.17 +    prems: @'premises' @{syntax thmbind}?
    1.18 +    ;
    1.19 +    params: @'for' '\<dots>'? (('_' | @{syntax name})+)
    1.20 +  \<close>}
    1.21 +
    1.22 +  \begin{description}
    1.23 +
    1.24 +  \item @{command "subgoal"} allows to impose some structure on backward
    1.25 +  refinements, to avoid proof scripts degenerating into long of @{command
    1.26 +  apply} sequences.
    1.27 +
    1.28 +  The current goal state, which is essentially a hidden part of the Isar/VM
    1.29 +  configurtation, is turned into a proof context and remaining conclusion.
    1.30 +  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
    1.31 +  structured proofs, but the text of the parameters, premises and conclusion
    1.32 +  is not given explicitly.
    1.33 +
    1.34 +  Goal parameters may be specified separately, in order to allow referring
    1.35 +  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
    1.36 +  y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
    1.37 +  "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
    1.38 +  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
    1.39 +  positions may be skipped via dummies (underscore). Unspecified names
    1.40 +  remain internal, and thus inaccessible in the proof text.
    1.41 +
    1.42 +  ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
    1.43 +  goal premises should be turned into assumptions of the context (otherwise
    1.44 +  the remaining conclusion is a Pure implication). The fact name and
    1.45 +  attributes are optional; the particular name ``@{text prems}'' is a common
    1.46 +  convention for the premises of an arbitrary goal context in proof scripts.
    1.47 +
    1.48 +  ``@{command subgoal}~@{text result}'' indicates a fact name for the result
    1.49 +  of a proven subgoal. Thus it may be re-used in further reasoning, similar
    1.50 +  to the result of @{command show} in structured Isar proofs.
    1.51 +
    1.52 +  \end{description}
    1.53 +
    1.54 +  Here are some abstract examples:
    1.55 +\<close>
    1.56 +
    1.57 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    1.58 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    1.59 +  subgoal sorry
    1.60 +  subgoal sorry
    1.61 +  done
    1.62 +
    1.63 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    1.64 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    1.65 +  subgoal for x y z sorry
    1.66 +  subgoal for u v sorry
    1.67 +  done
    1.68 +
    1.69 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    1.70 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    1.71 +  subgoal premises for x y z
    1.72 +    using \<open>A x\<close> \<open>B y\<close>
    1.73 +    sorry
    1.74 +  subgoal premises for u v
    1.75 +    using \<open>X u\<close>
    1.76 +    sorry
    1.77 +  done
    1.78 +
    1.79 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    1.80 +  and "\<And>u v. X u \<Longrightarrow> Y v"
    1.81 +  subgoal r premises prems for x y z
    1.82 +  proof -
    1.83 +    have "A x" by (fact prems)
    1.84 +    moreover have "B y" by (fact prems)
    1.85 +    ultimately show ?thesis sorry
    1.86 +  qed
    1.87 +  subgoal premises prems for u v
    1.88 +  proof -
    1.89 +    have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
    1.90 +    moreover
    1.91 +    have "X u" by (fact prems)
    1.92 +    ultimately show ?thesis sorry
    1.93 +  qed
    1.94 +  done
    1.95 +
    1.96 +lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
    1.97 +  subgoal premises prems for \<dots> z
    1.98 +  proof -
    1.99 +    from prems show "C z" sorry
   1.100 +  qed
   1.101 +  done
   1.102 +
   1.103 +
   1.104  section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
   1.105  
   1.106  text \<open>