isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:0634d42bb69f
+:17b1512f51af
 functions @{ML RL} and @{ML MRL}. For example in the code below,
 every theorem in the second list is instantiated with every
 theorem in the first.
 @{ML_response_fake [display,gray]
-"[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
+"map (no_vars @{context})
+([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])"
 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
 \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
 (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
 Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
 apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
 done
 text {*
 If the simplifier cannot make any progress, then it leaves the goal unchanged,
-i.e.~does not raise any error message. That means if you use it to unfold a
+i.e., does not raise any error message. That means if you use it to unfold a
 definition for a constant and this constant is not present in the goal state,
 you can still safely apply the simplifier.
 When using the simplifier, the crucial information you have to provide is
 the simpset. If this information is not handled with care, then the
 @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
 @{ML_file  "Provers/splitter.ML"}.
 \end{readmore}
 \begin{readmore}
-FIXME: Find the right place Discrimination nets are implemented
+FIXME: Find the right place: Discrimination nets are implemented
 in @{ML_file "Pure/net.ML"}.
 \end{readmore}
-The most common combinators to modify simpsets are
+The most common combinators to modify simpsets are:
 \begin{isabelle}
 \begin{tabular}{ll}
 @{ML addsimps}   & @{ML delsimps}\\
 @{ML addcongs}   & @{ML delcongs}\\
 \end{figure} *}
 text {*
 To see how they work, consider the function in Figure~\ref{fig:printss}, which
 prints out some parts of a simpset. If you use it to print out the components of the
-empty simpset, i.e.~ @{ML empty_ss}
+empty simpset, i.e., @{ML empty_ss}
 @{ML_response_fake [display,gray]
 "print_ss @{context} empty_ss"
 "Simplification rules:
 Congruences rules:
 push permutations as far inside as possible, where they might disappear by
 Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
 it would be desirable to add also the lemma @{thm [source] perm_compose} to
 the simplifier for pushing permutations over other permutations. Unfortunately,
 the right-hand side of this lemma is again an instance of the left-hand side
-and so causes an infinite loop. The seems to be no easy way to reformulate
+and so causes an infinite loop. There 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"
 THEN' simp_tac (HOL_basic_ss addsimps thms2)
 THEN' simp_tac (HOL_basic_ss addsimps thms3)
 end*}
 text {*
-For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+For all three phases we have to build simpsets adding 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
 apply(tactic {* perm_simp_tac 1 *})
 done
 text {*
-in one step. This tactic can deal with most instances of normalising permutations;
+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
+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=>"}?)

changeset 209	17b1512f51af
parent 208	0634d42bb69f
child 210	db8e302f44c8