isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:ac01ddb285f6
+:e60dbcba719d
 begin
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 text {*
-The main reason for descending to the ML-level of Isabelle is to be able to
+One of the main reason for descending to the ML-level of Isabelle is to be able to
 implement automatic proof procedures. Such proof procedures usually lessen
 considerably the burden of manual reasoning, for example, when introducing
 new definitions. These proof procedures are centred around refining a goal
 state using tactics. This is similar to the \isacommand{apply}-style
 reasoning at the user-level, where goals are modified in a sequence of proof
 THEN' atac
 THEN' rtac @{thm disjI1}
 THEN' atac)*}
 text {*
-and then give the number for the subgoal explicitly when the tactic is
+where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+the number for the subgoal explicitly when the tactic is
 called. So in the next proof you can first discharge the second subgoal, and
 subsequently the first.
 *}
 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
 the subgoals. So after setting up the lemma, the goal state is always of the
 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
 "(C)"}. Since the goal @{term C} can potentially be an implication, there is
-a ``protector'' wrapped around it (in from of an outermost constant @{text
+a ``protector'' wrapped around it (the wrapper is the outermost constant @{text
 "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
 is invisible in the figure). This wrapper prevents that premises of @{text C} are
 mis-interpreted as open subgoals. While tactics can operate on the subgoals
 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
 @{term C} intact, with the exception of possibly instantiating schematic
 \end{minipage}
 *}
 (*<*)oops(*>*)
 text {*
-A simple tactic for ``easily'' discharging proof obligations is
+A simple tactic for easy discharge of any proof obligations is
 @{ML SkipProof.cheat_tac}. This tactic corresponds to
 the Isabelle command \isacommand{sorry} and is sometimes useful
 during the development of tactics.
 *}
-lemma shows "False" and "something_else_obviously_false"
+lemma shows "False" and "Goldbach_conjecture"
 apply(tactic {* SkipProof.cheat_tac @{theory} *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 (*<*)oops(*>*)
 text {*
 Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
 to @{text rule}, @{text drule}, @{text erule} and @{text frule},
-respectively. Each of them takes a theorem as argument and attempts to
+respectively. Each of them take a theorem as argument and attempt to
 apply it to a goal. Below are three self-explanatory examples.
 *}
 lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
 lemma shows "False \<and> True \<Longrightarrow> False"
 apply(tactic {* dtac @{thm conjunct2} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
-(*<*)oops(*>*)
-text {*
-Note the number in each tactic call. Also as mentioned in the previous section, most
-basic tactics take such a number as argument: this argument addresses the subgoal
-the tacics are analysing. In the proof below, we first split up the conjunction in
-the second subgoal by focusing on this subgoal first.
-*}
-lemma shows "Foo" and "P \<and> Q"
-apply(tactic {* rtac @{thm conjI} 2 *})
-txt {*\begin{minipage}{\textwidth}
-@{subgoals [display]}
-\end{minipage}*}
 (*<*)oops(*>*)
 text {*
 The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
 expects a list of theorems as arguments. From this list it will apply the
 then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but
 takes an additional number as argument that makes explicit which premise
 should be instantiated.
-To improve readability of the theorems we produce below, we shall use the
+To improve readability of the theorems we shall produce below, we will use the
 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
 schematic variables into free ones.  Using this function for the first @{ML
 RS}-expression above produces the more readable result:
 @{ML_response_fake [display,gray]
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-If you want to avoid the hard-coded subgoal addressing, then you can use
+If you want to avoid the hard-coded subgoal addressing, then, as
+seen earlier, you can use
 the ``primed'' version of @{ML THEN}. For example:
 *}
 lemma shows "(Foo \<and> Bar) \<and> False"
 apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-Here you only have to specify the subgoal of interest only once and
+Here you have to specify the subgoal of interest only once and
 it is consistently applied to the component tactics.
 For most tactic combinators such a ``primed'' version exists and
 in what follows we will usually prefer it over the ``unprimed'' one.
 If there is a list of tactics that should all be tried out in
 then in the following proof we can unfold this constant
 *}
 lemma shows "MyTrue \<Longrightarrow> True \<and> True"
 apply(rule conjI)
-apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *})
 txt{* producing the goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 are simple consequence of the definition and @{thm [source] perm_compose}.
 More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
 added to the simplifier, because now the right-hand side is not anymore an instance
 of the left-hand side. In a sense it freezes all redexes of permutation compositions
 after one step. In this way, we can split simplification of permutations
-into three phases without the user not noticing anything about the auxiliary
+into three phases without the user noticing anything about the auxiliary
 contant. We first freeze any instance of permutation compositions in the term using
 lemma @{thm [source] "perm_aux_expand"} (Line 9);
-then simplifiy all other permutations including pusing permutations over
+then simplifiy all other permutations including pushing permutations over
 other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
 finally ``unfreeze'' all instances of permutation compositions by unfolding
 the definition of the auxiliary constant.
 *}
 lemma shows "Suc 0 = 1"
 apply(simp)
 (*<*)oops(*>*)
 text {*
+\begin{isabelle}
+@{text "> The redex: Suc 0"}\\
+@{text "> The redex: Suc 0"}\\
+\end{isabelle}
 This will print out the message twice: once for the left-hand side and
 once for the right-hand side. The reason is that during simplification the
 simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
 0"}, and then the simproc ``fires'' also on that term.

changeset 213	e60dbcba719d
parent 210	db8e302f44c8
child 214	7e04dc2368b0