# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1235408895 0 # Node ID 2d9198bcb850a5cba4bfa2259dc71297f74ff8a8 # Parent 8db9195bb3e995ac1b7af596e4f5d3834d58612c polished diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Feb 23 00:27:27 2009 +0000 +++ b/CookBook/FirstSteps.thy Mon Feb 23 17:08:15 2009 +0000 @@ -376,12 +376,20 @@ some data structure and return it. Instead, it is literally replaced with the value representing the theory name. - In a similar way you can use antiquotations to refer to proved theorems: + In a similar way you can use antiquotations to refer to proved theorems: + for a single theorem @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} - and current simpsets. For this we use the function that extracts the - theorem names stored in the simpset. + and for more than one + +@{ML_response_fake [display,gray] "@{thms conj_ac}" +"(?P \<and> ?Q) = (?Q \<and> ?P) +(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R) +((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} + + You can also refer to the current simpsets. To illustrate this we use the + function that extracts the theorem names stored in a simpset. *} ML{*fun get_thm_names simpset = diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Feb 23 00:27:27 2009 +0000 +++ b/CookBook/Parsing.thy Mon Feb 23 17:08:15 2009 +0000 @@ -429,7 +429,7 @@ in (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) end" -"([\"}\", \"{\", \<dots>],[\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} +"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} The parser @{ML "OuterParse.$$$"} parses a single keyword. For example: diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Mon Feb 23 00:27:27 2009 +0000 +++ b/CookBook/Solutions.thy Mon Feb 23 17:08:15 2009 +0000 @@ -63,9 +63,9 @@ 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)) + val goal = Logic.mk_equals (t, sum) in - mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))) + Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1)) end fun add_sp_aux ss t = diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/Tactical.thy --- 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 *} diff -r 8db9195bb3e9 -r 2d9198bcb850 cookbook.pdf Binary file cookbook.pdf has changed