# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1235309867 0
# Node ID a21d7b300616e5473e8ef7c3573a36aa1b07a863
# Parent  e0d368a4553724ace6dc83a0c5f68a83b748e238
polished the section about simprocs and added an exercise

diff -r e0d368a45537 -r a21d7b300616 CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Sun Feb 22 03:44:03 2009 +0000
+++ b/CookBook/Solutions.thy	Sun Feb 22 13:37:47 2009 +0000
@@ -8,20 +8,20 @@
 
 ML{*fun rev_sum t =
 let
- fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
-   | dest_sum u = [u]
- in
+  fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
+    | dest_sum u = [u]
+in
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
- end *}
+end *}
 
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =
-    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
+      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 text {* \solution{ex:scancmts} *}
 
-ML{*val any = Scan.one (Symbol.not_eof);
+ML{*val any = Scan.one (Symbol.not_eof)
 
 val scan_cmt =
   let
@@ -32,9 +32,10 @@
     >> (enclose "(**" "**)" o implode)
   end
 
+val parser = Scan.repeat (scan_cmt || any)
+
 val scan_all =
-  Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) 
-    >> implode #> fst *}
+  Scan.finite Symbol.stopper parser >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function 
@@ -43,12 +44,55 @@
 
   @{ML_response [display,gray]
 "let
-   val input1 = (explode \"foo bar\")
-   val input2 = (explode \"foo (*test*) bar (*test*)\")
- in
-   (scan_all input1, scan_all input2)
- end"
-"(\"foo bar\",\"foo (**test**) bar (**test**)\")"}
+  val input1 = (explode \"foo bar\")
+  val input2 = (explode \"foo (*test*) bar (*test*)\")
+in
+  (scan_all input1, scan_all input2)
+end"
+"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 *}
 
+text {* \solution{ex:addsimproc} *}
+
+ML{*fun dest_sum term =
+  case term of 
+    (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+        (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
+  | _ => raise TERM ("dest_sum", [term])
+
+fun get_sum_thm ctxt t (n1, n2) =  
+let 
+  val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
+  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, sum))
+in
+  mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+end
+
+fun add_sp_aux ss t =
+let 
+  val ctxt = Simplifier.the_context ss
+  val t' = term_of t
+in
+  SOME (get_sum_thm ctxt t' (dest_sum t'))
+  handle TERM _ => NONE
+end*}
+
+text {* The setup for the simproc is *}
+
+simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}
+ 
+text {* and a test case is the lemma *}
+
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})
+txt {* 
+  where the simproc produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}
+*}(*<*)oops(*>*)
+
+
+
 end
\ No newline at end of file
diff -r e0d368a45537 -r a21d7b300616 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Sun Feb 22 03:44:03 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Feb 22 13:37:47 2009 +0000
@@ -1027,7 +1027,7 @@
 text {*
   In Isabelle you can also implement custom simplification procedures, called
   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
-  rewrite a term according to a given theorem. They are useful in cases where
+  rewrite a term according to theorem. They are useful in cases where
   a rewriting rule must be produced on ``demand'' or when rewriting by
   simplification is too unpredictable and potentially loops.
 
@@ -1050,8 +1050,8 @@
   simpset and then print out a message containing the redex.  The function
   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
   moment we are \emph{not} interested in actually rewriting anything. We want
-  that the simproc is triggered by the pattern @{term "Suc n"}. For this we
-  can add the simproc with this pattern to the current simpset as follows
+  that the simproc is triggered by the pattern @{term "Suc n"}. This can be
+  done by adding the simproc to the current simproc as follows
 *}
 
 simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
@@ -1059,8 +1059,9 @@
 text {*
   where the second argument specifies the pattern and the right-hand side
   contains the code of the simproc (we have to use @{ML K} since we ignoring
-  an argument). After this setup, the simplifier is aware of
-  this simproc and you can test whether it fires with the lemma
+  an argument about a morphism\footnote{FIXME: what does the morphism do?}). 
+  After this, the simplifier is aware of the simproc and you can test whether 
+  it fires on the lemma
 *}
 
 lemma shows "Suc 0 = 1"
@@ -1069,12 +1070,12 @@
 
 text {*
   This will print out the message twice: once for the left-hand side and
-  once for the right-hand side. This is because during simplification the
-  simplifier will by default reduce the term @{term "1::nat"} to @{term "Suc
+  once for the right-hand side. The reason is that during simplification the
+  simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
   0"}, and then the simproc ``fires'' also on that term. 
 
-  We can add or delete the simproc by the usual methods. For example
-  the simproc will be deleted by the declaration:
+  We can add or delete the simproc by the usual \isacommand{declare}-statement. 
+  For example the simproc will be deleted if you type:
 *}
 
 declare [[simproc del: fail_sp]]
@@ -1092,7 +1093,7 @@
 text {*
   (FIXME: should one use HOL-basic-ss or HOL-ss?)
 
-  Now the message shows up only once. 
+  Now the message shows up only once since @{term "1::nat"} is left unchanged. 
 
   Setting up a simproc using the command \isacommand{setup\_simproc} will
   always add automatically the simproc to the current simpset. If you do not
@@ -1110,20 +1111,25 @@
 end*}
 
 text {*
-  Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}.
-  We can turn this function into a simproc using
+  Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
+  (therefore we printing it out using the function @{ML string_of_term in Syntax}).
+  We can turn this function into a proper simproc using
 *}
 
 
 ML{*val fail_sp' = 
-      Simplifier.simproc_i @{theory} "fail_sp'" [@{term "Suc n"}] 
-        (K fail_sp_aux')*}
+  let 
+    val thy = @{theory}
+    val pat = [@{term "Suc n"}]
+  in
+    Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+  end*}
 
 text {*
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
-
-  Simprocs are applied from inside to outside, from left to right. You can see
-  this in the proof
+  The function also takes a list of patterns that can trigger the simproc.
+  It might be interesting to notice that simprocs are applied from inside 
+  to outside and from left to right. You can see this in the proof
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
@@ -1131,24 +1137,29 @@
 (*<*)oops(*>*)
 
 text {*
-  since it prints out the sequence @{term "Suc 0"}, @{term "Suc (Suc 0)"} and 
-  @{term "Suc 1"}.
+  since the @{ML fail_sp'}-simproc prints out the sequence 
 
-  To see how a simproc applies a theorem  let us rewrite terms according to the 
-  equation:
+@{text [display]
+"> Suc 0
+> Suc (Suc 0) 
+> Suc 1"}
+
+  To see how a simproc applies a theorem  let us implement a simproc that
+  rewrites terms according to the equation:
 *}
 
 lemma plus_one: 
   shows "Suc n \<equiv> n + 1" by simp
 
 text {*
-  The simproc expects the equation to be a meta-equation, however it can contain 
-  possible preconditions (the simproc then only fires if the preconditions can be 
-  solved). Let us further assume we want to only rewrite terms greater than 
+  Simprocs expect that the given equation is a meta-equation, however the
+  equation can contain preconditions (the simproc then will only fire if the 
+  preconditions can be solved). To see how rewriting can be tuned precisely, let us 
+  further assume we want that the simproc only rewrites terms greater than 
   @{term "Suc 0"}. For this we can write
 *}
 
-ML{*fun plus_one_sp_aux thy ss redex =
+ML{*fun plus_one_sp_aux ss redex =
   case redex of
     @{term "Suc 0"} => NONE
   | _ => SOME @{thm plus_one}*}
@@ -1157,18 +1168,23 @@
   and set up the simproc as follows.
 *}
 
-ML{*val plus_one_sproc = 
-       Simplifier.simproc_i @{theory} "sproc +1" [@{term "Suc n"}] 
-         plus_one_sp_aux*}
+ML{*val plus_one_sp =
+  let
+    val thy = @{theory}
+    val pat = [@{term "Suc n"}] 
+  in
+    Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+  end*}
 
 text {*
-  Now the simproc fires one every term of the for @{term "Suc n"}, but
-  the lemma is only applied whenever the term is not @{term "Suc 0"}. So
-  in 
+  Now the have set up the simproc so that it is triggered by terms
+  of the form @{term "Suc n"}, but inside the simproc we only produce
+  a theorem if the term is not @{term "Suc 0"}. The result you can see
+  in the following proof.
 *}
 
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sproc]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
   the simproc produces the goal state
 
@@ -1177,49 +1193,98 @@
 (*<*)oops(*>*)
 
 text {*
-  where the first argument is rewritten, but not the second. With @{ML
-  plus_one_sproc} you already have to be careful to not cause the simplifier
-  to loop. If we call this simproc together with the default simpset, we
-  already have a loop as it contains a rule which just undoes the rewriting of
-  the simproc.
+  As usual with simplification you have to be careful with loops: you already have
+  one @{ML plus_one_sp}, if you apply if with the default simpset (because
+  the default simpset contains a rule which just undoes the rewriting 
+  @{ML plus_one_sp}).
+
+  Let us next implement a simproc that replaces terms of the form @{term "Suc n"}
+  with the number @{text n} increase by one. First we implement a function that
+  takes a term and produces the corresponding integer value, if it can.
+
 *}
 
 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
   | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 
-text {* This function might raise @{ML TERM}. *}
+text {* 
+  It uses the library function @{ML dest_number in HOLogic} that transforms
+  (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
+  on, into integer values. This function raises the exception @{ML TERM} if
+  the term is not a number. The next function expects a pair consisting of a term
+  @{text t} and the corresponding integer value @{text n}. 
+*}
+
+ML %linenosgray{*fun get_thm ctxt (t, n) =
+let
+  val num = HOLogic.mk_number @{typ "nat"} n
+  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
+in
+  mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+end*}
+
+text {*
+  From the integer value it generates the corresponding Isabelle term, called 
+  @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4)
+  which it proves by simplification in Line 6. The function @{ML mk_meta_eq} 
+  at the outside of the proof just transforms the equality to a meta-equality.
+
+  Both functions can be stringed together in the function that produces the 
+  actual theorem for the simproc.
+*}
 
 ML{*fun nat_number_sp_aux ss t =
 let 
   val ctxt = Simplifier.the_context ss
-
-  fun get_thm (t, n) =
-  let
-    val num = HOLogic.mk_number @{typ "nat"} n
-    val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
-  in
-    Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))
-  end
 in
-  SOME (mk_meta_eq (get_thm (t,dest_suc_trm t)))
+  SOME (get_thm ctxt (t, dest_suc_trm t))
   handle TERM _ => NONE
 end*}
 
 text {*
-  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following loops.)
+  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
+
+  This function uses the fact that @{ML dest_suc_trm} might throw an exception 
+  @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
+  theorem is produced. To try out the simproc on an example, you can set it up as 
+  follows:
 *}
 
-ML{*val nat_number_sp = 
-       Simplifier.simproc_i @{theory} "nat_number" [@{term "Suc n"}] 
-         (K nat_number_sp_aux) *}
+ML{*val nat_number_sp =
+  let
+    val thy = @{theory}
+    val pat = [@{term "Suc n"}]
+  in 
+    Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 
+  end*}
+
+text {* 
+  Now in the lemma
+  *}
 
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
   apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
 txt {* 
+  you obtain the more legible goal state
+  
   @{subgoals [display]}
   *}
 (*<*)oops(*>*)
 
+text {*
+  where the simproc rewrites all @{term "Suc"}s except in the last arguments. There it cannot 
+  rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
+  into a number. To solve this problem have a look at the next exercise. 
+
+  \begin{exercise}\label{ex:addsimproc}
+  Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their 
+  result. You can assume the terms are ``proper'' numbers, that is of the form
+  @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
+  \end{exercise}
+
+  (FIXME: We did not do anything with morphisms. Anything interesting
+  one can say about them?)
+*}
 
 section {* Structured Proofs *}
 
diff -r e0d368a45537 -r a21d7b300616 cookbook.pdf
Binary file cookbook.pdf has changed