--- a/CookBook/Tactical.thy Mon Feb 23 00:27:27 2009 +0000
+++ b/CookBook/Tactical.thy Mon Feb 23 17:08:15 2009 +0000
@@ -68,8 +68,6 @@
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
@@ -210,11 +208,11 @@
*}
ML{*fun my_print_tac ctxt thm =
- let
- val _ = warning (str_of_thm ctxt thm)
- in
- Seq.single thm
- end*}
+let
+ val _ = warning (str_of_thm ctxt thm)
+in
+ Seq.single thm
+end*}
text_raw {*
\begin{figure}[p]
@@ -537,21 +535,21 @@
\begin{isabelle}
*}
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
- let
- val str_of_params = str_of_cterms context params
- val str_of_asms = str_of_cterms context asms
- val str_of_concl = str_of_cterm context concl
- val str_of_prems = str_of_thms context prems
- val str_of_schms = str_of_cterms context (snd schematics)
+let
+ val str_of_params = str_of_cterms context params
+ val str_of_asms = str_of_cterms context asms
+ val str_of_concl = str_of_cterm context concl
+ val str_of_prems = str_of_thms context prems
+ val str_of_schms = str_of_cterms context (snd schematics)
- val _ = (warning ("params: " ^ str_of_params);
- warning ("schematics: " ^ str_of_schms);
- warning ("assumptions: " ^ str_of_asms);
- warning ("conclusion: " ^ str_of_concl);
- warning ("premises: " ^ str_of_prems))
- in
- no_tac
- end*}
+ val _ = (warning ("params: " ^ str_of_params);
+ warning ("schematics: " ^ str_of_schms);
+ warning ("assumptions: " ^ str_of_asms);
+ warning ("conclusion: " ^ str_of_concl);
+ warning ("premises: " ^ str_of_prems))
+in
+ no_tac
+end*}
text_raw{*
\end{isabelle}
\caption{A function that prints out the various parameters provided by the tactic
@@ -1032,7 +1030,7 @@
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
+ the pattern which triggers it and otherwise does nothing. For this
you can use the function:
*}
@@ -1046,7 +1044,7 @@
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
+ arguments. 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
@@ -1075,8 +1073,8 @@
0"}, and then the simproc ``fires'' also on that term.
We can add or delete the simproc from the current simpset by the usual
- \isacommand{declare}-statement. For example the simproc will be deleted
- if you type:
+ \isacommand{declare}-statement. For example the simproc will be deleted
+ with the declaration
*}
declare [[simproc del: fail_sp]]
@@ -1088,12 +1086,10 @@
*}
lemma shows "Suc 0 = 1"
- apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+ apply(tactic {* simp_tac (HOL_basic_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 since the term @{term "1::nat"} is
left unchanged.
@@ -1130,8 +1126,12 @@
text {*
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
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
+ Now the simproc is set up and can be explicitly added using
+ {ML addsimprocs} to a simpset whenerver
+ needed.
+
+ 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)"
@@ -1139,7 +1139,7 @@
(*<*)oops(*>*)
text {*
- since @{ML fail_sp'} prints out the sequence
+ The simproc @{ML fail_sp'} prints out the sequence
@{text [display]
"> Suc 0
@@ -1156,7 +1156,7 @@
text {*
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 one has relatively precise control over
+ preconditions can be solved). To see that one has relatively precise control over
the rewriting with simprocs, let us further assume we want that the simproc
only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write
*}
@@ -1180,7 +1180,7 @@
end*}
text {*
- Now the simproc is set up xso that it is triggered by terms
+ Now the simproc is set up 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
@@ -1196,14 +1196,15 @@
(*<*)oops(*>*)
text {*
- As usual with simplification you have to be careful with looping: 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}).
+ As usual with simplification you have to worry about looping: you already have
+ a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
+ the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+ namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful
+ in choosing the right simpset to which you add a simproc.
- Let us next implement a simproc that replaces terms of the form @{term "Suc n"}
+ Next let us 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.
+ takes a term and produces the corresponding integer value.
*}
@@ -1221,21 +1222,45 @@
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))
+ val goal = Logic.mk_equals (t, num)
in
- mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+ Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
end*}
text {*
- (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
+ From the integer value it generates the corresponding number term, called
+ @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"}
+ (Line 4), which it proves by the arithmetic tactic in Line 6.
+
+ For our purpose at the moment, using in the code above @{ML arith_tac} is
+ fine, but there is also an alternative employing the simplifier with a very
+ restricted simpset. For the kind of lemmas we want to prove, the simpset
+ @{text "num_ss"} in the code will suffice.
+*}
- From the integer value it generates the corresponding number 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 into a meta-equality.
+ML{*fun get_thm_alt ctxt (t, n) =
+let
+ val num = HOLogic.mk_number @{typ "nat"} n
+ val goal = Logic.mk_equals (t, num)
+ val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @
+ @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+in
+ Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end*}
- Both functions can be stringed together in the function that produces the
- actual theorem for the simproc.
+text {*
+ The advantage of @{ML get_thm_alt} is that it leaves very little room for
+ something to go wrong; in contrast it is much more difficult to predict
+ what happens with @{ML arith_tac}, especially in more complicated
+ circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+ that is sufficiently powerful to solve every instance of the lemmas
+ we like to prove. This requires careful tuning, but is often necessary in
+ ``production code''.\footnote{It would be of great help if there is another
+ way than tracing the simplifier to obtain the lemmas that are successfully
+ applied during simplification. Alas, there is none.}
+
+ Anyway, either version can be used in the function that produces the actual
+ theorem for the simproc.
*}
ML{*fun nat_number_sp_aux ss t =
@@ -1254,12 +1279,12 @@
*}
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*}
+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
@@ -1275,7 +1300,7 @@
(*<*)oops(*>*)
text {*
- where the simproc rewrites all @{term "Suc"}s except in the last arguments. There it cannot
+ where the simproc rewrites all @{term "Suc"}s except in the last argument. 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.
@@ -1289,6 +1314,9 @@
one can say about them?)
*}
+section {* Conversions *}
+
+
section {* Structured Proofs *}
text {* TBD *}