--- a/CookBook/Tactical.thy Tue Mar 03 13:00:55 2009 +0000
+++ b/CookBook/Tactical.thy Wed Mar 04 13:15:29 2009 +0000
@@ -11,7 +11,7 @@
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
+ reasoning at the user-level, where goals are modified in a sequence of proof
steps until all of them are solved. However, there are also more structured
operations available on the ML-level that help with the handling of
variables and assumptions.
@@ -101,7 +101,7 @@
text {*
By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
- user level of Isabelle the tactic @{ML foo_tac} or
+ user-level of Isabelle the tactic @{ML foo_tac} or
any other function that returns a tactic.
The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
@@ -329,7 +329,7 @@
text {*
Let us start with the tactic @{ML print_tac}, 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} it prints the goal state as the user would see it).
+ (unlike @{ML my_print_tac}, it prints the goal state as the user would see it).
For example, processing the proof
*}
@@ -1022,10 +1022,17 @@
text {*
A lot of convenience in the reasoning with Isabelle derives from its
- powerful simplifier. There are the following five main tactics behind
- the simplifier (in parentheses is their userlevel counterpart)
+ powerful simplifier. The power of simplifier is at the same time a
+ strength and a weakness, because you can easily make the simplifier to
+ loop and its behaviour can sometimes be difficult to predict. There is also
+ a multitude of options that configurate 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 counterparts):
\begin{isabelle}
+ \begin{center}
\begin{tabular}{l@ {\hspace{2cm}}l}
@{ML simp_tac} & @{text "(simp (no_asm))"} \\
@{ML asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
@@ -1033,6 +1040,7 @@
@{ML asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
@{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
@@ -1044,120 +1052,349 @@
done
text {*
- corrsponds on the ML-level to the tactic
+ corresponds on the ML-level to the tactic
*}
lemma "Suc (1 + 2) < 3 + 2"
apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
done
-thm imp_cong simp_implies_cong
-
text {*
- The crucial information the developer has to control is the simpset
- to be used by the simplifier. If not handled with care, then the
- simplifier can easily run forever.
+ 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
+ for a constant and this constant is not present in a goal state, you can still
+ safely apply the simplifier.
- It might be surprising that a simpset is quite more complex than just
- a simple list 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 rules that have precoditions. The rewriting
- inside terms requires congruence rules which are meta-equalities
- typical of the form
+ When using the simplifier, the crucial information you have to control is
+ the simpset. If not handled with care, then the simplifier can easily run
+ into a loop. 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
+ 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"}}
- {@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>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. However there are also more complicated
- congruence rules. The user can declare lemmas to be congruence rules using the
- attribute @{text "[cong]"} (theses lemmas are usually equations that are internally
- transformed into meta-equations (FIXME: check that).
-
- The rewriting with rules involving preconditions requires solvers. However
- there are also 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. (FIXME: loopers and subgoalers?)
+ with @{text "constr"} being a term-constructor. 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
+ 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
+ @{ML_file "Provers/splitter.ML"}.
+ \end{readmore}
The most common combinators to modify simpsets are
\begin{isabelle}
\begin{tabular}{ll}
- @{ML addsimps} & @{ML delsimps}\\
- @{ML addcongs} & @{ML delcongs}\\
+ @{ML addsimps} & @{ML delsimps}\\
+ @{ML addcongs} & @{ML delcongs}\\
+ @{ML addsimprocs} & @{ML delsimprocs}\\
\end{tabular}
\end{isabelle}
- The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}.
+ (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+*}
+
+text_raw {*
+\begin{figure}[tp]
+\begin{isabelle}*}
+ML{*fun get_parts ss =
+let
+ val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss
+
+ val rules_list = Net.entries rules
+ val rnames = map #name rules_list
+ val rthms = map #thm rules_list
+
+ val congs_list = fst congs
+ val cnames = map fst congs_list
+ val cthms = map (#thm o snd) congs_list
+
+ val proc_list = Net.entries procs
+in
+ (rnames ~~ rthms, cnames ~~ cthms)
+end
+
+fun print_parts ctxt ss =
+let
+ val (simps, congs) = get_parts ss
+
+ fun name_thm (nm, thm) =
+ " " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+
+ val s1 = ["Simplification rules:"]
+ val s2 = map name_thm simps
+ val s3 = ["Congruences rules:"]
+ val s4 = map name_thm congs
+in
+ (s1 @ s2 @ s3 @ s4)
+ |> separate "\n"
+ |> implode
+ |> warning
+end*}
+text_raw {*
+\end{isabelle}
+\caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing
+ a simpset. We are here only interested in the simplifcation rules, congruence rules and
+ simprocs. The first and third are discrimination nets, which from which we extract
+ lists using @{ML Net.entries}. The congruence rules are stored in
+ an association list, associating a constant with a rule.\label{fig:prettyss}}
+\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
+
+ @{ML_response_fake [display,gray]
+ "print_parts @{context} empty_ss"
+"Simplification rules:
+Congruences rules:"}
+
+ you can see it contains nothing. This simpset is usually not useful, except as a
+ building block to build bigger simpsets. For example you can add to @{ML empty_ss}
+ the simplification rule @{thm [source] Diff_Int} as follows:
*}
-ML {* warning (Pretty.string_of (MetaSimplifier.pretty_ss HOL_ss)) *}
+ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+
+text {*
+ Printing out the components of this simpset gives:
-ML {*
-fun get_parts ss =
-let
- val ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = MetaSimplifier.rep_ss ss
-in
- (rules, congs, procs, loop_tacs, solvers)
-end
+ @{ML_response_fake [display,gray]
+ "print_parts @{context} ss1"
+"Simplification rules:
+ ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+Congruences rules:"}
+
+ Adding the congruence rule @{thm [source] UN_cong}
*}
-ML {*
- Pretty.big_list
+ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+
+text {*
+ gives
+
+ @{ML_response_fake [display,gray]
+ "print_parts @{context} ss2"
+"Simplification rules:
+ ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+Congruences rules:
+ UNION: \<lbrakk>?A1 = ?B1; \<And>x. x \<in> ?B1 \<Longrightarrow> ?C1 x = ?D1 x\<rbrakk> \<Longrightarrow>
+ \<Union>x\<in>?A1. ?C1 x \<equiv> \<Union>x\<in>?B1. ?D1 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.
+
+ In the context of HOL the first 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
+ form @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]},
+ and resolve with assumptions.
+*}
+
+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
+ up.
+
+ The simpset @{ML HOL_ss}, which is an extention of @{ML HOL_basic_ss}, contains
+ already many useful simplification 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.the_eq_trivial: THE x. x = ?y \<equiv> ?y
+ HOL.the_sym_eq_trivial: THE y. ?y = y \<equiv> ?y
+ \<dots>
+Congruences rules:
+ 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
+ not cause any loops with most of the simplification rules that
+ you might like to add.
*}
-ML {*
-fun print_ss ss =
- let
- val pretty_thms = map (enclose " " "\n" o Display.string_of_thm)
+text_raw {*
+\begin{figure}[tp]
+\begin{isabelle} *}
+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
+ then snd ab
+ else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
- fun pretty_cong (name, {thm, lhs}) =
- name ^ ":" ^ (Display.string_of_thm thm);
+primrec (perm_prod)
+ "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
+
+primrec (perm_list)
+ "pi\<bullet>[] = []"
+ "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma perm_append[simp]:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
+by (induct pi\<^isub>1) (auto)
+
+lemma perm_eq[simp]:
+ fixes c::"nat" and pi::"prm"
+ shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)"
+by (induct pi) (auto)
- val (rules, congs, procs, loop_tacs, solvers) = get_parts ss;
- val smps = map #thm (Net.entries rules);
-
- in
- "simplification rules:\n" ^
- (implode (pretty_thms smps)) ^
- "congruences:" ^ (commas (map pretty_cong (fst congs))) ^ "\n" ^
- "loopers:" ^ (commas (map (quote o fst) loop_tacs))
- end;
+lemma perm_rev[simp]:
+ fixes c::"nat" and pi::"prm"
+ shows "pi\<bullet>((rev pi)\<bullet>c) = c"
+by (induct pi arbitrary: c) (auto)
+
+lemma perm_compose:
+ 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>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
+by (induct pi\<^isub>2) (auto)
+text_raw {*
+\end{isabelle}\medskip
+\caption{A simple theory about permutations over @{typ nat}. The point is that the
+ lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
+ it would cause the simplifier to loop. It can still be used as a simplification
+ rule if the permutation is sufficiently protected.\label{fig:perms}
+ (FIXME: Uses old primrec.)}
+\end{figure} *}
+
+
+text {*
+ Often the situation arises that simplification rules will cause the
+ simplifier to run into an infinite loop. Consider for example the simple
+ theory about permutations shown in Figure~\ref{fig:perms}. The purpose of
+ the lemmas is to pus permutations as far inside a term where they might
+ disappear using the lemma @{thm [source] perm_rev}. However, to fully
+ simplifiy all instances, it would be desirable to add also the lemma @{thm
+ [source] perm_compose} to the simplifier in order to push 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. On the user-level it is difficult to work around such situations
+ and we end up with clunky proofs such as:
*}
-thm FalseE
-
-thm simp_impliesI
-lemma "P (Suc 0) \<Longrightarrow> P ?x"
-apply(tactic {* CHANGED (simp_tac HOL_basic_ss 1) *})
-oops
-
-ML {* warning (print_ss HOL_ss) *}
+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(simp)
+apply(rule trans)
+apply(rule perm_compose)
+apply(simp)
+done
text {*
- @{ML HOL_basic_ss} can deal essentially only with goals of the form:
- @{thm TrueI}, @{thm refl[no_vars]} @{term "x \<equiv> x"} and @{thm FalseE},
- and resolve with assumptions.
+ On the ML-level, we can however generate 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
+*}
+
+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 *}
+
+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)
+
+lemma perm_compose_aux:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)"
+unfolding perm_aux_def by (rule perm_compose)
+
+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
*}
-ML {* setsubgoaler *}
+ML %linenosgray{*val perm_simp_tac =
+let
+ val thms1 = [@{thm perm_aux_expand}]
+ val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev},
+ @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @
+ @{thms perm_list.simps} @ @{thms perm_nat.simps}
+ val thms3 = [@{thm perm_aux_def}]
+in
+ simp_tac (HOL_basic_ss addsimps thms1)
+ THEN' simp_tac (HOL_basic_ss addsimps thms2)
+ THEN' simp_tac (HOL_basic_ss addsimps thms3)
+end*}
text {*
- (FIXME: what do the simplifier tactics do when nothing can be rewritten)
+ This trick is not noticable for the user.
+*}
+
+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 {*
+ (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},
@{ML ObjectLogic.rulify_tac})
-
- \begin{readmore}
- For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
- and @{ML_file "Pure/simplifier.ML"}.
- \end{readmore}
-
*}
section {* Simprocs *}