src/Doc/Isar_Ref/Proof_Script.thy
 changeset 62269 c56cff1c0e73 parent 61866 6fa60a4f7e48 child 62271 4cfe65cfd369
equal inserted replaced
62268:3d86222b4a94 62269:c56cff1c0e73
    11   scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof
    11   scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof
    12   documents\<close> instead (see also \chref{ch:proofs}).
    12   documents\<close> instead (see also \chref{ch:proofs}).
    13
    13
    14   Nonetheless, it is possible to emulate proof scripts by sequential
    14   Nonetheless, it is possible to emulate proof scripts by sequential
    15   refinements of a proof state in backwards mode, notably with the @{command
    15   refinements of a proof state in backwards mode, notably with the @{command
    16   apply} command (see \secref{sec:tactic-commands}). There are also various
    16   apply} command (see \secref{sec:tactic-commands}).
    17   proof methods that allow to refer to implicit goal state information that is
    17
    18   normally not accessible to structured Isar proofs (see
    18   There are also various proof methods that allow to refer to implicit goal
    19   \secref{sec:tactics}).
    19   state information that is not accessible to structured Isar proofs (see

    20   \secref{sec:tactics}). Note that the @{command subgoal}

    21   (\secref{sec:subgoal}) command usually eliminates the need for implicit goal

    22   state references.
    20 \<close>
    23 \<close>
    21
    24
    22
    25
    23 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
    26 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
    24
    27
    80   for experimentation and interactive exploration, and should be avoided in
    83   for experimentation and interactive exploration, and should be avoided in
    81   finished proofs.
    84   finished proofs.
    82 \<close>
    85 \<close>
    83
    86
    84
    87
    85 section \<open>Explicit subgoal structure\<close>
    88 section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>
    86
    89
    87 text \<open>
    90 text \<open>
    88   \begin{matharray}{rcl}
    91   \begin{matharray}{rcl}
    89     @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
    92     @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
    90   \end{matharray}
    93   \end{matharray}