--- a/src/Doc/Isar_Ref/Framework.thy Wed Feb 10 10:53:30 2016 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Wed Feb 10 11:22:57 2016 +0100
@@ -204,9 +204,9 @@
been spelled out more explicitly as ``\<^theory_text>\<open>proof (rule InterI)\<close>''. Note that
the rule involves both a local parameter \<open>A\<close> and an assumption \<open>A \<in> \<A>\<close> in
the nested reasoning. Such compound rules typically demands a genuine
- sub-proof in Isar, working backwards rather than forwards as seen before. In
+ subproof in Isar, working backwards rather than forwards as seen before. In
the proof body we encounter the \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> outline of nested
- sub-proofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close>
+ subproofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close>
followed by an additional refinement of the enclosing claim, using the rule
derived from the proof body.
@@ -384,7 +384,7 @@
\<^medskip>
Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the
- sub-goals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is
+ subgoals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is
finished. To allow \<open>C\<close> being a rule statement itself, there is an internal
protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and
hidden from the user. We initialize and finish goal states as follows:
@@ -398,8 +398,8 @@
Goal states are refined in intermediate proof steps until a finished form is
achieved. Here the two main reasoning principles are @{inference
- resolution}, for back-chaining a rule against a sub-goal (replacing it by
- zero or more sub-goals), and @{inference assumption}, for solving a sub-goal
+ resolution}, for back-chaining a rule against a subgoal (replacing it by
+ zero or more subgoals), and @{inference assumption}, for solving a subgoal
(finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands
for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (for \<open>n \<ge> 0\<close>).
@@ -447,33 +447,34 @@
Compositions of @{inference assumption} after @{inference resolution} occurs
quite often, typically in elimination steps. Traditional Isabelle tactics
accommodate this by a combined @{inference_def elim_resolution} principle.
- In contrast, Isar uses a slightly more refined combination, where the
- assumptions to be closed are marked explicitly, using again the protective
- marker \<open>#\<close>:
+ In contrast, Isar uses a combined refinement rule as follows:\footnote{For
+ simplicity and clarity, the presentation ignores \<^emph>\<open>weak premises\<close> as
+ introduced via \<^theory_text>\<open>presume\<close> or \<^theory_text>\<open>show \<dots> when\<close>.}
+ {\small
\[
\infer[(@{inference refinement})]
- {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
+ {\<open>C\<vartheta>\<close>}
{\begin{tabular}{rl}
- \<open>sub\<hyphen>proof:\<close> &
- \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\
- \<open>goal:\<close> &
+ \<open>subgoal:\<close> &
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\
- \<open>goal unifier:\<close> &
+ \<open>subproof:\<close> &
+ \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \quad for schematic \<open>\<^vec>a\<close> \\
+ \<open>concl unifier:\<close> &
\<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\
\<open>assm unifiers:\<close> &
- \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>\<close> \\
- & \quad (for each marked \<open>G\<^sub>j\<close> some \<open>#H\<^sub>i\<close>) \\
+ \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = H\<^sub>i\<vartheta>\<close> \quad for each \<open>G\<^sub>j\<close> some \<open>H\<^sub>i\<close> \\
\end{tabular}}
- \]
+ \]}
- Here the \<open>sub\<hyphen>proof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close>
+ Here the \<open>subproof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close>
outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption
- indicated in the text results in a marked premise \<open>G\<close> above. The marking
- enforces resolution against one of the sub-goal's premises. Consequently,
- \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a sub-proof quite
- robustly into a pending sub-goal, while maintaining a good measure of
- flexibility.
+ indicated in the text results in a marked premise \<open>G\<close> above. Consequently,
+ \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a subproof quite
+ robustly into a pending subgoal, while maintaining a good measure of
+ flexibility: the subproof only needs to fit modulo unification, and its
+ assumptions may be a proper subset of the subgoal premises (see
+ \secref{sec:framework-subproof}).
\<close>
@@ -566,14 +567,14 @@
\<^medskip>
Block structure can be indicated explicitly by ``@{command
- "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof already involves
+ "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a subproof already involves
implicit nesting. In any case, @{command next} jumps into the next section
of a block, i.e.\ it acts like closing an implicit block scope and opening
another one; there is no direct correspondence to subgoals here.
The remaining elements @{command fix} and @{command assume} build up a local
context (see \secref{sec:framework-context}), while @{command show} refines
- a pending sub-goal by the rule resulting from a nested sub-proof (see
+ a pending subgoal by the rule resulting from a nested subproof (see
\secref{sec:framework-subproof}). Further derived concepts will support
calculational reasoning (see \secref{sec:framework-calc}).
\<close>
@@ -661,7 +662,7 @@
that \<open>A x\<close> may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note that
``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters is similar to
``@{command have}~\<open>A \<AND> B\<close>'', but the latter involves multiple
- sub-goals.
+ subgoals.
\<^medskip>
The subsequent Isar proof texts explain all context elements introduced
@@ -824,7 +825,7 @@
like @{command have}, @{command show}. A goal statement changes the mode to
\<open>prove\<close>, which means that we may now refine the problem via @{command
unfolding} or @{command proof}. Then we are again in \<open>state\<close> mode of a proof
- body, which may issue @{command show} statements to solve pending sub-goals.
+ body, which may issue @{command show} statements to solve pending subgoals.
A concluding @{command qed} will return to the original \<open>state\<close> mode one
level upwards. The subsequent Isar/VM trace indicates block structure,
linguistic mode, goal state, and inferences:
@@ -878,11 +879,11 @@
text \<open>
Here the @{inference refinement} inference from
- \secref{sec:framework-resolution} mediates composition of Isar sub-proofs
+ \secref{sec:framework-resolution} mediates composition of Isar subproofs
nicely. Observe that this principle incorporates some degree of freedom in
proof composition. In particular, the proof body allows parameters and
assumptions to be re-ordered, or commuted according to Hereditary Harrop
- Form. Moreover, context elements that are not used in a sub-proof may be
+ Form. Moreover, context elements that are not used in a subproof may be
omitted altogether. For example:
\<close>