diff -r e8f11280c762 -r 76cdc8f562fc CookBook/Tactical.thy
--- 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 *}