isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:83f36a1c62f2
+:3fb9f820a294
 theory Tactical
 imports Base FirstSteps
 begin
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 text {*
 The main reason for descending to the ML-level of Isabelle is to be able to
 \begin{readmore}
 To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
 and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
 "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
 tactics and tactic combinators; see also Chapters 3 and 4 in the old
-Isabelle Reference Manual.
+Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual.
 \end{readmore}
 Note that in the code above we use antiquotations for referencing the theorems. Many theorems
 also have ML-bindings with the same name. Therefore, we could also just have
 written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
 section {* Simplifier Tactics *}
 text {*
 A lot of convenience in the reasoning with Isabelle derives from its
-powerful simplifier. The power of simplifier is at the same time a
+powerful simplifier. The power of simplifier is a strength and a weakness at
-strength and a weakness, because you can easily make the simplifier to
+the same time, because you can easily make the simplifier to run into a  loop and its
-loop and its behaviour can sometimes be difficult to predict. There is also
+behaviour can be difficult to predict. There is also a multitude
-a multitude of options that configurate the behaviour of the simplifier. We
+of options that you can configurate to control the behaviour of the simplifier.
-describe some of them in this and the next section.
+We describe some of them in this and the next section.
 There are the following five main tactics behind
-the simplifier (in parentheses is their user-level counterparts):
+the simplifier (in parentheses is their user-level counterpart):
 \begin{isabelle}
 \begin{center}
 \begin{tabular}{l@ {\hspace{2cm}}l}
 @{ML simp_tac}            & @{text "(simp (no_asm))"} \\
 @{ML asm_full_simp_tac}   & @{text "(simp)"}
 \end{tabular}
 \end{center}
 \end{isabelle}
-All of them take a simpset and an interger as argument (the latter to specify the goal
+All of the tactics take a simpset and an interger as argument (the latter as usual
-to be analysed). So the proof
+to specify  the goal to be analysed). So the proof
 *}
 lemma "Suc (1 + 2) < 3 + 2"
 apply(simp)
 done
 lemma "Suc (1 + 2) < 3 + 2"
 apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
 done
 text {*
-If the simplifier cannot make any progress, then it leaves the goal unchanged
+If the simplifier cannot make any progress, then it leaves the goal unchanged,
-and does not raise any error message. That means if you use it to unfold a definition
+i.e.~does not raise any error message. That means if you use it to unfold a
-for a constant and this constant is not present in a goal state, you can still
+definition for a constant and this constant is not present in the goal state,
-safely apply the simplifier.
+you can still safely apply the simplifier.
-When using the simplifier, the crucial information you have to control is
+When using the simplifier, the crucial information you have to provide is
-the simpset. If not handled with care, then the simplifier can easily run
+the simpset. If this information is not handled with care, then the
-into a loop. It might be surprising that a simpset is more complex than just a
+simplifier can easily run into a loop. Therefore a good rule of thumb is to
-simple collection of theorems used as simplification rules. One reason for
+use simpsets that are as minimal as possible. It might be surprising that a
-the complexity is that the simplifier must be able to rewrite inside terms
+simpset is more complex than just a simple collection of theorems used as
-and should also be able to rewrite according to rules that have
+simplification rules. One reason for the complexity is that the simplifier
-precoditions.
+must be able to rewrite inside terms and should also be able to rewrite
+according to rules that have precoditions.
 The rewriting inside terms requires congruence rules, which
 are meta-equalities typical of the form
 \begin{isabelle}
 \begin{center}
-\mbox{\inferrule{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}
+\mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
 {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
 \end{center}
 \end{isabelle}
-with @{text "constr"} being a term-constructor. Every simpset contains only
+with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+Every simpset contains only
 one concruence rule for each term-constructor, which however can be
 overwritten. The user can declare lemmas to be congruence rules using the
 attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
 equations, which are then internally transformed into meta-equations.
 The rewriting with rules involving preconditions requires what is in
 Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
-tactics that can be installed in a simpset. However, simpsets also include
+tactics that can be installed in a simpset and which are called during
+various stages during simplification. However, simpsets also include
 simprocs, which can produce rewrite rules on demand (see next
 section). Another component are split-rules, which can simplify for example
 the ``then'' and ``else'' branches of if-statements under the corresponding
 precoditions.
 \begin{readmore}
 For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
 and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
 @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
 \end{figure} *}
 text {*
 To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which
 print out some parts of a simpset. If you use them to print out the components of the
-empty simpset, the most primitive simpset
+empty simpset, in ML @{ML empty_ss} and the most primitive simpset
 @{ML_response_fake [display,gray]
 "print_parts @{context} empty_ss"
 "Simplification rules:
 Congruences rules:"}
 *}
 ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
 text {*
-Printing out the components of this simpset gives:
+Printing then out the components of the simpset gives:
 @{ML_response_fake [display,gray]
 "print_parts @{context} ss1"
 "Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:"}
 (FIXME: Why does it print out ??.unknown)
-Adding the congruence rule @{thm [source] UN_cong}
+Adding also the congruence rule @{thm [source] UN_cong}
 *}
 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
 text {*
 Congruences rules:
 UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"}
 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
 expects this form of the simplification and congruence rules. However, even
-adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
+when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
-In the context of HOL the first useful simpset is @{ML HOL_basic_ss}. While
+In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
 printing out the components of this simpset
 @{ML_response_fake [display,gray]
 "print_parts @{context} HOL_basic_ss"
 "Simplification rules:
 Congruences rules:"}
 also produces ``nothing'', the printout is misleading. In fact
-the simpset @{ML HOL_basic_ss} is setup so that it can be used to solve goals of the
+the @{ML HOL_basic_ss} is setup so that it can solve goals of the
-form  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]},
+form  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
-and resolve with assumptions.
+and also resolve with assumptions. For example:
 *}
 lemma
 "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
 done
 text {*
-This is because how the tactics for the subgoaler, solver and looper are set
+This behaviour is not because of simplification rules, but how the subgoaler, solver
-up.
+and looper are set up. @{ML HOL_basic_ss} is usually a good start to build your
+own simpsets, because of the low danger of causing loops via interacting simplifiction
-The simpset @{ML HOL_ss}, which is an extention of @{ML HOL_basic_ss}, contains
+rules.
-already many useful simplification rules for the logical connectives in HOL.
+The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+already many useful simplification and congruence rules for the logical
+connectives in HOL.
 @{ML_response_fake [display,gray]
 "print_parts @{context} HOL_ss"
 "Simplification rules:
 Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
 HOL.simp_implies: \<dots>
 \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
 op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"}
-The main point of these simpsets is that they are small enough to
+The simplifier is often used to unfold definitions in a proof. For this the
-not cause any loops with most of the simplification rules that
+simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
-you might like to add.
+definition
+*}
+definition "MyTrue \<equiv> True"
+lemma shows "MyTrue \<Longrightarrow> True \<and> True"
+apply(rule conjI)
+apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+txt{* then the tactic produces the goal state
+\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage} *}
+(*<*)oops(*>*)
+text {*
+As you can see, the tactic unfolds the definitions in all subgoals.
 *}
 text_raw {*
 \begin{figure}[tp]
 types  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 primrec (perm_nat)
 "[]\<bullet>c = c"
-"(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab
+"(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab
-then snd ab
+else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
-else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
 primrec (perm_prod)
 "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
 primrec (perm_list)
 (FIXME: Uses old primrec.)}
 \end{figure} *}
 text {*
-Often the situation arises that simplification rules will cause the
+The simplifier is often used in order to bring terms into a normal form.
-simplifier to run into an infinite loop. Consider for example the simple
+Unfortunately, often the situation arises that the corresponding
-theory about permutations shown in Figure~\ref{fig:perms}. The purpose of
+simplification rules will cause the simplifier to run into an infinite
-the lemmas is to pus permutations as far inside a term where they might
+loop. Consider for example the simple theory about permutations over natural
-disappear using the lemma @{thm [source] perm_rev}. However, to fully
+numbers shown in Figure~\ref{fig:perms}. The purpose of the lemmas is to
-simplifiy all instances, it would be desirable to add also the lemma @{thm
+push permutations as far inside as possible, where they might disappear by
-[source] perm_compose} to the simplifier in order to push permutations over
+Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
-other permutations. Unfortunately, the right-hand side of this lemma is
+it would be desirable to add also the lemma @{thm [source] perm_compose} to
-again an instance of the left-hand side and so causes an infinite
+the simplifier for pushing permutations over other permutations. Unfortunately,
-loop. On the user-level it is difficult to work around such situations
+the right-hand side of this lemma is again an instance of the left-hand side
-and we end up with clunky proofs such as:
+and so causes an infinite loop. The seems to be no easy way to reformulate
+this rule and so one ends up with clunky proofs like:
 *}
 lemma
 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(rule perm_compose)
 apply(simp)
 done
 text {*
-On the ML-level, we can however generate a single simplifier tactic that solves
+It is however possible to create a single simplifier tactic that solves
 such proofs. The trick is to introduce an auxiliary constant for permutations
-and split the simplification into two phases. Let us say the auxiliary constant is
+and split the simplification into two phases (below actually three). Let
+assume the auxiliary constant is
 *}
 definition
 perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)
 where
 "pi \<bullet>aux c \<equiv> pi \<bullet> c"
-text {* Now the lemmas *}
+text {* Now the two lemmas *}
 lemma perm_aux_expand:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)"
 unfolding perm_aux_def by (rule refl)
 text {*
 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. So you can write
+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
+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
+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.
 *}
 ML %linenosgray{*val perm_simp_tac =
 let
 val thms1 = [@{thm perm_aux_expand}]
 THEN' simp_tac (HOL_basic_ss addsimps thms2)
 THEN' simp_tac (HOL_basic_ss addsimps thms3)
 end*}
 text {*
-This trick is not noticable for the user.
+For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+the desired results. Now we can solve the following lemma
 *}
 lemma
 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(tactic {* perm_simp_tac 1 *})
 done
 text {*
+in one step. This tactic can deal with most instances of normalising permutations;
+in order to solve all cases we have to deal with corner-cases such as the
+lemma being an exact instance of the permutation composition lemma. This can
+often be done easier by implementing a simproc or a conversion. Both will be
+explained in the next two chapters.
 (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
 (FIXME: Unfortunately one cannot access any simproc, as there is
 no @{text rep_proc} in function @{ML get_parts}.)
 (FIXME: What are the second components of the congruence rules---something to
 do with weak congruence constants?)
 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
-(FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac},
+(FIXME: @{ML ObjectLogic.full_atomize_tac},
 @{ML ObjectLogic.rulify_tac})
 *}
 section {* Simprocs *}

changeset 162	3fb9f820a294
parent 161	83f36a1c62f2
child 163	2319cff107f0