--- a/ProgTutorial/Tactical.thy Fri Oct 30 09:42:17 2009 +0100
+++ b/ProgTutorial/Tactical.thy Sat Oct 31 11:37:41 2009 +0100
@@ -23,7 +23,6 @@
tactic combinators. We also describe the simplifier, simprocs and conversions.
*}
-
section {* Basics of Reasoning with Tactics*}
text {*
@@ -99,9 +98,13 @@
lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name
in the theorem database, the string can stand for a dynamically updatable
theorem list. Also in this case we cannot be sure which theorem is applied.
- These problems can be nicely prevented by using antiquotations, because then
- the theorems are fixed statically at compile-time.
-
+ These problems can be nicely prevented by using antiquotations
+
+ @{ML_response_fake [gray,display]
+ "@{thm \"disjE\"}"
+ "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
+
+ because then the theorems are fixed statically at compile-time.
During the development of automatic proof procedures, you will often find it
necessary to test a tactic on examples. This can be conveniently done with
@@ -391,7 +394,7 @@
section {* Simple Tactics\label{sec:simpletacs} *}
text {*
- In this section we will introduce more simple tactics. The
+ In this section we will introduce more of the simple tactics in Isabelle. The
first one is @{ML_ind print_tac in Tactical}, which is quite useful
for low-level debugging of tactics. It just prints out a message and the current
goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
@@ -401,13 +404,12 @@
lemma
shows "False \<Longrightarrow> True"
apply(tactic {* print_tac "foo message" *})
-txt{*gives:\medskip
-
- \begin{minipage}{\textwidth}\small
+txt{*gives:
+ \begin{isabelle}
@{text "foo message"}\\[3mm]
@{prop "False \<Longrightarrow> True"}\\
@{text " 1. False \<Longrightarrow> True"}\\
- \end{minipage}
+ \end{isabelle}
*}
(*<*)oops(*>*)
@@ -430,7 +432,7 @@
This tactic works however only if the quick-and-dirty mode of Isabelle
is switched on. This is done automatically in the ``interactive
mode'' of Isabelle, but must be done manually in the ``batch mode''
- with for example the assignment
+ with the assignment
*}
ML{*quick_and_dirty := true*}
@@ -518,11 +520,10 @@
lemma
shows "True \<noteq> False"
apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
-txt{*produces the goal state\medskip
-
- \begin{minipage}{\textwidth}
+txt{*produces the goal state
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage}*}
+ \end{isabelle}*}
(*<*)oops(*>*)
text {*
@@ -593,7 +594,7 @@
\end{tabular}
\end{quote}
- The @{text params} and @{text schematics} stand or list of pairs where the
+ The @{text params} and @{text schematics} stand for list of pairs where the
left-hand side of @{text ":="} is replaced by the right-hand side inside the
tactic. Notice that in the actual output the variables @{term x} and @{term
y} have a brown colour. Although they are parameters in the original goal,
@@ -756,10 +757,16 @@
explain in the next section. But before that we will show how
tactic application can be constrained.
- Since rules are applied using higher-order unification, an automatic proof
- procedure might become too fragile, if it just applies inference rules as
- shown above. The reason is that a number of rules introduce schematic variables
- into the goal state. Consider for example the proof
+ \begin{readmore}
+ The functions @{ML SUBGOAL} and @{ML CSUBGOAL} are defined in @{ML_file "Pure/tactical.ML"}.
+ \end{readmore}
+
+
+ Since @{ML_ind rtac in Tactic} and the like use higher-order unification, an
+ automatic proof procedure based on them might become too fragile, if it just
+ applies theorems as shown above. The reason is that a number of theorems
+ introduce schematic variables into the goal state. Consider for example the
+ proof
*}
lemma
@@ -771,20 +778,20 @@
(*<*)oops(*>*)
text {*
- where the application of rule @{text bspec} generates two subgoals involving the
- schematic variable @{text "?x"}. Now, if you are not careful, tactics
+ where the application of theorem @{text bspec} generates two subgoals involving the
+ new schematic variable @{text "?x"}. Now, if you are not careful, tactics
applied to the first subgoal might instantiate this schematic variable in such a
way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
should be, then this situation can be avoided by introducing a more
- constrained version of the @{text bspec}-rule. One way to give such
+ constrained version of the @{text bspec}-theorem. One way to give such
constraints is by pre-instantiating theorems with other theorems.
The function @{ML_ind RS in Drule}, for example, does this.
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
- In this example it instantiates the first premise of the @{text conjI}-rule
- with the rule @{text disjI1}. If the instantiation is impossible, as in the
+ In this example it instantiates the first premise of the @{text conjI}-theorem
+ with the theorem @{text disjI1}. If the instantiation is impossible, as in the
case of
@{ML_response_fake_both [display,gray]
@@ -829,7 +836,8 @@
Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
\begin{readmore}
- The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
+ The combinators for instantiating theorems with other theorems are
+ defined in @{ML_file "Pure/drule.ML"}.
\end{readmore}
Higher-order unification is also often in the way when applying certain
@@ -861,7 +869,7 @@
intended one. While we can use \isacommand{back} to interactively find the
intended instantiation, this is not an option for an automatic proof
procedure. Fortunately, the tactic @{ML_ind cong_tac in Cong_Tac} helps
- with applying congruence rules and finding the intended instantiation.
+ with applying congruence theorems and finding the intended instantiation.
For example
*}
@@ -875,7 +883,7 @@
(*<*)oops(*>*)
text {*
- However, frequently it is necessary to explicitly match a theorem against a proof
+ However, frequently it is necessary to explicitly match a theorem against a goal
state and in doing so construct manually an appropriate instantiation. Imagine
you have the theorem
*}
@@ -928,9 +936,15 @@
text {*
We obtain the intended subgoals and also the parameters are correctly
introduced in both of them. Such manual instantiations are quite frequently
- necessary in order to appropriately constrain the application of inference
- rules. Otherwise one would end up with ``wild'' higher-order unification
- problems that make automatic proofs fail.
+ necessary in order to appropriately constrain the application of theorems.
+ Otherwise one can end up with ``wild'' higher-order unification problems
+ that make automatic proofs fail.
+
+ \begin{readmore}
+ Functions for matching @{ML_type cterm}s are defined in @{ML_file "Pure/thm.ML"}.
+ Functions for instantiating schematic variables in theorems are defined
+ in @{ML_file "Pure/drule.ML"}.
+ \end{readmore}
*}
section {* Tactic Combinators *}
@@ -950,9 +964,9 @@
(*<*)oops(*>*)
text {*
- 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:
+ If you want to avoid the hard-coded subgoal addressing in each component,
+ then, as seen earlier, you can use the ``primed'' version of @{ML THEN}.
+ For example:
*}
lemma
@@ -965,7 +979,7 @@
text {*
Here you have to specify the subgoal of interest only once and
- it is consistently applied to the component tactics.
+ it is consistently applied to the component.
For most tactic combinators such a ``primed'' version exists and
in what follows we will usually prefer it over the ``unprimed'' one.
@@ -1003,7 +1017,7 @@
ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
text {*
- will first try out whether rule @{text disjI} applies and in case of failure
+ will first try out whether theorem @{text disjI} applies and in case of failure
will try @{text conjI}. To see this consider the proof
*}
@@ -1012,10 +1026,9 @@
apply(tactic {* orelse_xmp_tac 2 *})
apply(tactic {* orelse_xmp_tac 1 *})
txt {* which results in the goal state
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage}
+ \end{isabelle}
*}
(*<*)oops(*>*)
@@ -1031,7 +1044,7 @@
text {*
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
we must include @{ML all_tac} at the end of the list, otherwise the tactic will
- fail if no rule applies (we also have to wrap @{ML all_tac} using the
+ fail if no theorem applies (we also have to wrap @{ML all_tac} using the
@{ML K}-combinator, because it does not take a subgoal number as argument). You can
test the tactic on the same goals:
*}
@@ -1063,7 +1076,7 @@
text {*
Remember that we chose to implement @{ML select_tac'} so that it
- always succeeds by adding @{ML all_tac} at the end of the tactic
+ always succeeds by fact of having @{ML all_tac} at the end of the tactic
list. The same can be achieved with the tactic combinator @{ML_ind TRY in Tactical}.
For example:
*}
@@ -1089,18 +1102,18 @@
(*<*)oops(*>*)
text {*
- In this case no rule applies, but because of @{ML TRY} or the inclusion of @{ML all_tac}
- the tactics do not fail. The problem with this is that for the user there is little
- chance to see whether or not progress in the proof has been made. By convention
- therefore, tactics visible to the user should either change something or fail.
-
+ In this case no theorem applies. But because we wrapped the tactic in a @{ML
+ TRY}, it does not fail anymore. The problem is that for the user there is
+ little chance to see whether progress in the proof has been made, or not. By
+ convention therefore, tactics visible to the user should either change
+ something or fail.
+
To comply with this convention, we could simply delete the @{ML "K all_tac"}
- from the end of the theorem list. As a result @{ML select_tac'} would only
- succeed on goals where it can make progress. But for the sake of argument,
- let us suppose that this deletion is \emph{not} an option. In such cases, you can
- use the combinator @{ML_ind CHANGED in Tactical} to make sure the subgoal has been changed
- by the tactic. Because now
-
+ in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
+ the sake of argument, let us suppose that this deletion is \emph{not} an
+ option. In such cases, you can use the combinator @{ML_ind CHANGED in
+ Tactical} to make sure the subgoal has been changed by the tactic. Because
+ now
*}
lemma
@@ -1115,9 +1128,9 @@
text {*
- We can further extend @{ML select_tac'} so that it not just applies to the topmost
+ We can further extend the @{ML select_tac}s so that they not just apply to the topmost
connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
- completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example
+ completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example
suppose the following tactic
*}
@@ -1129,18 +1142,17 @@
shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
apply(tactic {* repeat_xmp_tac *})
txt{* produces
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage} *}
+ \end{isabelle} *}
(*<*)oops(*>*)
text {*
- Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
+ Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
- tactic as long as it succeeds). The function
- @{ML_ind REPEAT1 in Tactical} is similar, but runs the tactic at least once (failing if
- this is not possible).
+ tactic as long as it succeeds). The function @{ML_ind REPEAT1 in Tactical}
+ is similar, but runs the tactic at least once (failing if this is not
+ possible).
If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
can implement it as
@@ -1156,13 +1168,13 @@
that goals 2 and 3 are not analysed. This is because the tactic
is applied repeatedly only to the first subgoal. To analyse also all
resulting subgoals, you can use the tactic combinator @{ML_ind REPEAT_ALL_NEW in Tactical}.
- Suppose the tactic
+ Supposing the tactic
*}
ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
text {*
- you see that the following goal
+ you can see that the following goal
*}
lemma
@@ -1185,11 +1197,10 @@
lemma
shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
apply(tactic {* etac @{thm disjE} 1 *})
-txt{* applies the rule to the first assumption yielding the goal state:\smallskip
-
- \begin{minipage}{\textwidth}
+txt{* applies the rule to the first assumption yielding the goal state:
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage}\smallskip
+ \end{isabelle}
After typing
*}
@@ -1200,11 +1211,10 @@
apply(tactic {* etac @{thm disjE} 1 *})
(*>*)
back
-txt{* the rule now applies to the second assumption.\smallskip
-
- \begin{minipage}{\textwidth}
+txt{* the rule now applies to the second assumption.
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage} *}
+ \end{isabelle} *}
(*<*)oops(*>*)
text {*
@@ -1231,36 +1241,9 @@
@{text "*** At command \"back\"."}
\end{isabelle}
- Recall that we implemented @{ML select_tac'} on Page~\pageref{tac:selectprime} specifically
- so that it always succeeds. We achieved this by adding at the end the tactic @{ML all_tac}.
- We can achieve this also by using the combinator @{ML TRY}. Suppose, for example the
- tactic
-*}
-
-ML{*val select_tac'' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
- rtac @{thm notI}, rtac @{thm allI}]*}
-
-text {*
- which will fail if none of the rules applies. However, if you prefix it as follows
-*}
-
-ML{*val select_tac''' = TRY o select_tac''*}
-
-text {*
- then the tactic @{ML select_tac''} will be tried out and any failure is harnessed.
- We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is
- no primed version of @{ML_ind TRY}. The tactic combinator @{ML_ind TRYALL} will try out
- a tactic on all subgoals. For example the tactic
-*}
-
-ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
-
-text {*
- will solve all trivial subgoals involving @{term True} or @{term "False"}.
-
- (FIXME: say something about @{ML_ind COND} and COND')
-
- (FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
+
+ \footnote{\bf FIXME: say something about @{ML_ind COND} and COND'}
+ \footnote{\bf FIXME: PARALLEL-CHOICE PARALLEL-GOALS}
\begin{readmore}
Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
@@ -1271,9 +1254,11 @@
text {*
\begin{exercise}\label{ex:dyckhoff}
Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent
- calculus, called G4ip, in which no contraction rule is needed in order to be
- complete. As a result the rules applied in any order give a simple decision
- procedure for propositional intuitionistic logic. His rules are
+ calculus, called G4ip, for intuitionistic propositional logic. The
+ interesting feature of this calculus is that no contraction rule is needed
+ in order to be complete. As a result applying the rules exhaustively leads
+ to simple decision procedure for propositional intuitionistic logic. The task
+ is to implement this decision procedure as a tactic. His rules are
\begin{center}
\def\arraystretch{2.3}
@@ -1313,39 +1298,42 @@
\end{tabular}
\end{center}
- Implement a tactic that explores all possibilites of applying these rules to
- a propositional formula until a goal state is reached in which all subgoals
- are discharged. Note that in Isabelle the left-rules need to be implemented
- as elimination rules. You need to prove separate lemmas corresponding to
- $\longrightarrow_{L_{1..4}}$. In order to explore all possibilities of applying
- the rules, use the tactic combinator @{ML_ind DEPTH_SOLVE in Search}, which searches
- for a state in which all subgoals are solved. Add also rules for equality and
- run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
+ Note that in Isabelle the left-rules need to be implemented as elimination
+ rules. You need to prove separate lemmas corresponding to
+ $\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of
+ applying these rules to a propositional formula until a goal state is
+ reached in which all subgoals are discharged. For this you can use the tactic
+ combinator @{ML_ind DEPTH_SOLVE in Search}.
+ \end{exercise}
+
+ \begin{exercise}
+ Add to the previous exercise also rules for equality and run your tactic on
+ the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
\end{exercise}
*}
section {* Simplifier Tactics *}
text {*
- A lot of convenience in the reasoning with Isabelle derives from its
- powerful simplifier. The power of the simplifier is a strength and a weakness at
- the same time, because you can easily make the simplifier run into a loop and
- in general its
- behaviour can be difficult to predict. There is also a multitude
- of options that you can configure to control the behaviour of the simplifier.
- 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 counterpart):
+ A lot of convenience in reasoning with Isabelle derives from its
+ powerful simplifier. We will describe it in this section, whereby
+ we can, however, only scratch the surface due to its complexity.
+
+ The power of the simplifier is a strength and a weakness at the same time,
+ because you can easily make the simplifier run into a loop and in general
+ its behaviour can be difficult to predict. There is also a multitude of
+ options that you can configure to change the behaviour of the
+ simplifier. There are the following five main tactics behind the simplifier
+ (in parentheses is their user-level counterpart):
\begin{isabelle}
\begin{center}
\begin{tabular}{l@ {\hspace{2cm}}l}
- @{ML_ind simp_tac} & @{text "(simp (no_asm))"} \\
- @{ML_ind asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
- @{ML_ind full_simp_tac} & @{text "(simp (no_asm_use))"} \\
- @{ML_ind asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
- @{ML_ind asm_full_simp_tac} & @{text "(simp)"}
+ @{ML_ind simp_tac in Simplifier} & @{text "(simp (no_asm))"} \\
+ @{ML_ind asm_simp_tac in Simplifier} & @{text "(simp (no_asm_simp))"} \\
+ @{ML_ind full_simp_tac in Simplifier} & @{text "(simp (no_asm_use))"} \\
+ @{ML_ind asm_lr_simp_tac in Simplifier} & @{text "(simp (asm_lr))"} \\
+ @{ML_ind asm_full_simp_tac in Simplifier} & @{text "(simp)"}
\end{tabular}
\end{center}
\end{isabelle}
@@ -1374,21 +1362,19 @@
definition for a constant and this constant is not present in the goal state,
you can still safely apply the simplifier.
- (FIXME: show rewriting of cterms)
-
+ \footnote{\bf FIXME: show rewriting of cterms}
When using the simplifier, the crucial information you have to provide is
- the simpset. If this information is not handled with care, then the
- simplifier can easily run into a loop. Therefore a good rule of thumb is to
- use simpsets that are as minimal as possible. It might be surprising that a
- simpset is more complex than just a simple collection of theorems used as
- simplification rules. One reason for the complexity is that the simplifier
- must be able to rewrite inside terms and should also be able to rewrite
- according to rules that have preconditions.
-
-
- The rewriting inside terms requires congruence rules, which
- are meta-equalities typical of the form
+ the simpset. If this information is not handled with care, then, as
+ mentioned above, the simplifier can easily run into a loop. Therefore a good
+ rule of thumb is to use simpsets that are as minimal as possible. It might
+ be surprising that a simpset is more complex than just a simple collection
+ of theorems. One reason for the complexity is that the simplifier must be
+ able to rewrite inside terms and should also be able to rewrite according to
+ theorems that have premises.
+
+ The rewriting inside terms requires congruence theorems, which
+ are typically meta-equalities of the form
\begin{isabelle}
\begin{center}
@@ -1397,47 +1383,42 @@
\end{center}
\end{isabelle}
- with @{text "constr"} being a constant, like @{const "If"} or @{const "Let"}.
- Every simpset contains only
- one congruence 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 and which are called at
- 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
- preconditions.
-
+ with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
+ and so on. Every simpset contains only one congruence 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 theorems involving premises 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 and which are executed at 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 preconditions.
\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"}. The generic splitter is implemented in
- @{ML_file "Provers/splitter.ML"}.
+ and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in
+ @{ML_file "Provers/splitter.ML"}.
\end{readmore}
- \begin{readmore}
- FIXME: Find the right place: Discrimination nets are implemented
- in @{ML_file "Pure/net.ML"}.
- \end{readmore}
+
+ \footnote{\bf FIXME: Find the right place to mention this: Discrimination
+ nets are implemented in @{ML_file "Pure/net.ML"}.}
The most common combinators to modify simpsets are:
\begin{isabelle}
\begin{tabular}{ll}
- @{ML_ind addsimps} & @{ML_ind delsimps}\\
- @{ML_ind addcongs} & @{ML_ind delcongs}\\
- @{ML_ind addsimprocs} & @{ML_ind delsimprocs}\\
+ @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\
+ @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\
+ @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
\end{tabular}
\end{isabelle}
- (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+ \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}}
*}
text_raw {*
@@ -1472,7 +1453,7 @@
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_ind empty_ss}
+ empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier}
@{ML_response_fake [display,gray]
"print_ss @{context} empty_ss"
@@ -1497,7 +1478,7 @@
Congruences rules:
Simproc patterns:"}
- (FIXME: Why does it print out ??.unknown)
+ \footnote{\bf FIXME: Why does it print out ??.unknown}
Adding also the congruence rule @{thm [source] UN_cong}
*}
@@ -1519,8 +1500,8 @@
expects this form of the simplification and congruence rules. However, even
when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
- In the context of HOL, the first really useful simpset is @{ML_ind HOL_basic_ss}. While
- printing out the components of this simpset
+ In the context of HOL, the first really useful simpset is @{ML_ind
+ HOL_basic_ss in Simpdata}. While printing out the components of this simpset
@{ML_response_fake [display,gray]
"print_ss @{context} HOL_basic_ss"
@@ -1540,15 +1521,19 @@
*}
lemma
- "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
+ shows "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 behaviour is not because of simplification rules, but how the subgoaler, solver
- and looper are set up in @{ML_ind HOL_basic_ss}.
-
- The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+ and looper are set up in @{ML_ind HOL_basic_ss}.
+
+ The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
already many useful simplification and congruence rules for the logical
connectives in HOL.
@@ -1566,9 +1551,13 @@
Simproc patterns:
\<dots>"}
-
+ \begin{readmore}
+ The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
+ The simpset @{ML HOL_ss} is implemented in @{ML_file "HOL/HOL.thy"}.
+ \end{readmore}
+
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier implements the tactic @{ML_ind rewrite_goal_tac}.\footnote{\bf FIXME:
+ simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME:
see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1583,15 +1572,14 @@
shows "MyTrue \<Longrightarrow> True"
apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
txt{* producing the goal state
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage} *}
+ \end{isabelle} *}
(*<*)oops(*>*)
text {*
- If you want to unfold definitions in all subgoals, then use the
- the tactic @{ML_ind rewrite_goals_tac}.
+ If you want to unfold definitions in \emph{all} subgoals not just one,
+ then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
*}
@@ -1947,10 +1935,9 @@
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
txt{*
where the simproc produces the goal state
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals[display]}
- \end{minipage}
+ \end{isabelle}
*}
(*<*)oops(*>*)
@@ -2053,11 +2040,9 @@
apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
txt {*
you obtain the more legible goal state
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage}
- *}
+ \end{isabelle}*}
(*<*)oops(*>*)
text {*
@@ -2389,10 +2374,9 @@
(if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
apply(tactic {* true1_tac @{context} 1 *})
txt {* where the tactic yields the goal state
-
- \begin{minipage}{\textwidth}
+ \begin{isabelle}
@{subgoals [display]}
- \end{minipage}*}
+ \end{isabelle}*}
(*<*)oops(*>*)
text {*
@@ -2543,8 +2527,20 @@
val this = Variable.export ctxt ctxt0 [this]
*}
+section {* Summary *}
+
text {*
- If a tactic should fail, return the empty sequence.
+
+ \begin{conventions}
+ \begin{itemize}
+ \item Reference theorems with the antiquotation @{text "@{thm \<dots>}"}.
+ \item If a tactic is supposed to fail, return the empty sequence.
+ \item If you apply a tactic to a sequence of subgoals, apply it
+ in reverse order (i.e.~start with the last subgoal).
+ \item Use simpsets that are as small as possible.
+ \end{itemize}
+ \end{conventions}
+
*}
end