--- a/CookBook/Tactical.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Tactical.thy Sun Feb 22 03:44:03 2009 +0000
@@ -68,6 +68,8 @@
Isabelle Reference Manual.
\end{readmore}
+ (FIXME: what is @{ML Goal.prove_global}?)
+
Note that in the code above we use antiquotations for referencing the theorems. Many theorems
also have ML-bindings with the same name. Therefore, we could also just have
written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
@@ -1018,13 +1020,211 @@
@{ML ObjectLogic.rulify_tac}
- Something about simprocs.
+*}
+
+section {* Simprocs *}
+
+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
+ a rewriting rule must be produced on ``demand'' or when rewriting by
+ simplification is too unpredictable and potentially loops.
+
+ To see how simprocs work, let us first write a simproc that just prints out
+ the pattern that triggers it and otherwise does nothing. For this
+ you can use the function:
+*}
+
+ML %linenosgray{*fun fail_sp_aux simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+in
+ NONE
+end*}
+
+text {*
+ This function takes a simpset and a redex (a @{ML_type cterm}) as
+ argument. In Lines 3 and~4, we first extract the context from the given
+ 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
+*}
+
+simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+
+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
+*}
+lemma shows "Suc 0 = 1"
+apply(simp)
+(*<*)oops(*>*)
+
+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
+ 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:
+*}
+
+declare [[simproc del: fail_sp]]
+
+text {*
+ If you want to see what happens with just \emph{this} simproc, without any
+ interference from other rewrite rules, you can call @{text fail_sp}
+ as follows:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+(*<*)oops(*>*)
+
+text {*
+ (FIXME: should one use HOL-basic-ss or HOL-ss?)
+
+ Now the message shows up only once.
+
+ Setting up a simproc using the command \isacommand{setup\_simproc} will
+ always add automatically the simproc to the current simpset. If you do not
+ want this, then you have to use a slightly different method for setting
+ up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+ to
+*}
+
+ML{*fun fail_sp_aux' simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+in
+ NONE
+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
*}
+ML{*val fail_sp' =
+ Simplifier.simproc_i @{theory} "fail_sp'" [@{term "Suc n"}]
+ (K fail_sp_aux')*}
+
+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
+*}
+
+lemma shows "Suc (Suc 0) = (Suc 1)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+(*<*)oops(*>*)
+
+text {*
+ since it prints out the sequence @{term "Suc 0"}, @{term "Suc (Suc 0)"} and
+ @{term "Suc 1"}.
+
+ To see how a simproc applies a theorem let us rewrite 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
+ @{term "Suc 0"}. For this we can write
+*}
+
+ML{*fun plus_one_sp_aux thy ss redex =
+ case redex of
+ @{term "Suc 0"} => NONE
+ | _ => SOME @{thm plus_one}*}
+
+text {*
+ 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*}
+
+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
+*}
+
+lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sproc]) 1*})
+txt{*
+ the simproc produces the goal state
+
+ @{subgoals[display]}
+*}
+(*<*)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.
+*}
+
+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}. *}
+
+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)))
+ handle TERM _ => NONE
+end*}
+
+text {*
+ (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following loops.)
+*}
+
+ML{*val nat_number_sp =
+ Simplifier.simproc_i @{theory} "nat_number" [@{term "Suc n"}]
+ (K nat_number_sp_aux) *}
+
+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 {*
+ @{subgoals [display]}
+ *}
+(*<*)oops(*>*)
+
+
section {* Structured Proofs *}
+text {* TBD *}
+
lemma True
proof