# HG changeset patch # User Christian Urban # Date 1235274243 0 # Node ID e0d368a4553724ace6dc83a0c5f68a83b748e238 # Parent 693711a0c7026041a413c549e39e52464dcc13f0 started a section about simprocs diff -r 693711a0c702 -r e0d368a45537 CookBook/Appendix.thy --- a/CookBook/Appendix.thy Sat Feb 21 11:38:14 2009 +0000 +++ b/CookBook/Appendix.thy Sun Feb 22 03:44:03 2009 +0000 @@ -5,6 +5,12 @@ text {* \appendix *} +text {* + Possible topics: translations/print translations + +*} + + chapter {* Recipes *} end diff -r 693711a0c702 -r e0d368a45537 CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Sat Feb 21 11:38:14 2009 +0000 +++ b/CookBook/Package/Ind_Interface.thy Sun Feb 22 03:44:03 2009 +0000 @@ -1,15 +1,15 @@ theory Ind_Interface -imports "../Base" "../Parsing" Simple_Inductive_Package +imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package begin -section {* Parsing the Specification *} +section {* Parsing and Typing the Specification *} text {* To be able to write down the specification in Isabelle, we have to introduce - a new command (see Section~\ref{sec:newcommand}). As the keyword for the new - command we chose \simpleinductive{}. We want that the package can cope with + a new command (see Section~\ref{sec:newcommand}). As the keyword for the + new command we chose \simpleinductive{}. In the package we want to support + some ``advanced'' features: First, we want that the package can cope with specifications inside locales. For example it should be possible to declare - *} locale rel = @@ -20,35 +20,68 @@ *} -simple_inductive (in rel) trcl' +simple_inductive (in rel) + trcl' where base: "trcl' x x" | step: "trcl' x y \ R y z \ trcl' x z" -simple_inductive (in rel) accpart' +simple_inductive (in rel) + accpart' where accpartI: "(\y. R y x \ accpart' y) \ accpart' x" +text {* + Second, we want that the user can specify fixed parameters. + Remember in the previous section we stated that the user can give the + specification for the transitive closure of a relation @{text R} as +*} +simple_inductive + trcl\\ :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" +where + base: "trcl\\ R x x" +| step: "trcl\\ R x y \ R y z \ trcl\\ R x z" text {* - After the keyword we expect a constant (or constants) with possible typing - annotations and a - list of introduction rules. While these specifications are all - straightforward, there is a technicality we like to deal with to do with - fixed parameters and locales. Remember we pointed out that the parameter - @{text R} is fixed throughout the specifications of @{text trcl} and @{text - accpart}. The point is that they might be fixed in a locale and we like to - support this. Accordingly we treat some parameters of the inductive - definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive - closure and accessible part are defined with a fixed parameter @{text R} and - also inside a locale fixing @{text R}. + Note that there is no locale given in this specification---the parameter + @{text "R"} therefore needs to be included explicitly in @{term trcl\\}, but + stays fixed throughout the specification. The problem with this way of + stating the specification for the transitive closure is that it derives the + following induction principle. + + \begin{center}\small + \mprset{flushleft} + \mbox{\inferrule{ + @{thm_style prem1 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ + @{thm_style prem2 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ + @{thm_style prem3 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}} + {@{thm_style concl trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}}} + \end{center} + + But this does not correspond to the induction principle we derived by hand, which + was + + \begin{center}\small + \mprset{flushleft} + \mbox{\inferrule{ + @{thm_style prem1 trcl_induct[no_vars]}\\\\ + @{thm_style prem2 trcl_induct[no_vars]}\\\\ + @{thm_style prem3 trcl_induct[no_vars]}} + {@{thm_style concl trcl_induct[no_vars]}}} + \end{center} + + The difference is that in the one derived by hand the relation @{term R} is not + a parameter of the proposition @{term P} to be proved and it is also not universally + qunatified in the second and third premise. The point is that the parameter @{term R} + stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' + argument of the transitive closure, but one that can be freely instantiated. + In order to recognise such parameters, we have to extend the specification + to include a mechanism to state fixed parameters. The user should be able + to write + *} -text_raw {* - \begin{figure}[p] - \begin{isabelle} -*} simple_inductive trcl'' for R :: "'a \ 'a \ bool" where @@ -60,18 +93,8 @@ where accpartI: "(\y. R y x \ accpart'' R y) \ accpart'' R x" -text_raw {* - \end{isabelle} - \caption{The first definition is for the transitive closure where the - relation @{text R} is explicitly fixed. Simiraly the second definition - of the accessible part of the relation @{text R}. The last two definitions - specify the same inductive predicates, but this time defined inside - a locale.\label{fig:inddefsfixed}} - \end{figure} -*} - text {* - \begin{figure}[p] + \begin{figure}[t] \begin{isabelle} \railnontermfont{\rmfamily\itshape} \railterm{simpleinductive,where,for} @@ -95,11 +118,10 @@ *} text {* - For the first subtask, the syntax of the \simpleinductive{} command can be - described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram + This leads directly to the railroad diagram shown in + Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram more or less translates directly into the parser: - @{ML_chunk [display,gray] parser} which we described in Section~\ref{sec:parsingspecs}. If we feed into the diff -r 693711a0c702 -r e0d368a45537 CookBook/Package/Ind_Prelims.thy --- a/CookBook/Package/Ind_Prelims.thy Sat Feb 21 11:38:14 2009 +0000 +++ b/CookBook/Package/Ind_Prelims.thy Sun Feb 22 03:44:03 2009 +0000 @@ -5,11 +5,11 @@ section{* Preliminaries *} text {* - On the Isabelle level, the user will just give a specification of an - inductive predicate and expects from the package to produce a convenient - reasoning infrastructure. This infrastructure needs to be derived from the - definition that correspond to the specified predicate. This will roughly - mean that the package has three main parts, namely: + The user will just give a specification of an inductive predicate and + expects from the package to produce a convenient reasoning + infrastructure. This infrastructure needs to be derived from the definition + that correspond to the specified predicate. This will roughly mean that the + package has three main parts, namely: \begin{itemize} @@ -18,13 +18,14 @@ \item storing the results in the theory. \end{itemize} - Before we start with explaining all parts, - let us first give three examples showing how to define inductive predicates - by hand and then also how to prove by hand important properties about - them. From these examples, we will figure out a general method for defining - inductive predicates. The aim in this section is \emph{not} to write proofs - that are as beautiful as possible, but as close as possible to the ML-code - we will develop in later sections. + Before we start with explaining all parts, let us first give three examples + showing how to define inductive predicates by hand and then also how to + prove by hand important properties about them. From these examples, we will + figure out a general method for defining inductive predicates. The aim in + this section is \emph{not} to write proofs that are as beautiful as + possible, but as close as possible to the ML-code we will develop in later + sections. + We first consider the transitive closure of a relation @{text R}. It is an inductive predicate characterised by the two introduction rules: @@ -34,7 +35,7 @@ @{prop[mode=Rule] "R x y \ trcl R y z \ trcl R x z"} \end{center} - In Isabelle the user will state for @{term trcl\} the specification: + In Isabelle, the user will state for @{term trcl\} the specification: *} simple_inductive @@ -65,7 +66,7 @@ reasoning for the user. With this definition, the proof of the induction principle for @{term trcl} - closure is almost immediate. It suffices to convert all the meta-level + is almost immediate. It suffices to convert all the meta-level connectives in the lemma to object-level connectives using the proof method @{text atomize} (Line 4), expand the definition of @{term trcl} (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7), @@ -203,8 +204,8 @@ \begin{center}\small @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} - @{prop[mode=Rule] "odd m \ even (Suc m)"} \hspace{5mm} - @{prop[mode=Rule] "even m \ odd (Suc m)"} + @{prop[mode=Rule] "odd n \ even (Suc n)"} \hspace{5mm} + @{prop[mode=Rule] "even n \ odd (Suc n)"} \end{center} The user will state for this inductive definition the specification: @@ -339,13 +340,13 @@ text {* In Line 11, applying the assumption @{text "r1"} generates a goal state with the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the - proof above (Line 14). This local assumption will be used to solve - the goal @{term "P y"} using the assumption @{text "p1"}. + proof above (Line 14). This local assumption is used to solve + the goal @{term "P y"} with the help of assumption @{text "p1"}. The point of these examples is to get a feeling what the automatic proofs should do in order to solve all inductive definitions we throw at them. - This is usually the first step in writing a package. + This is usually the first step in writing a package. We next explain + the parsing and typing part of the package. *} - -end +(*<*)end(*>*) diff -r 693711a0c702 -r e0d368a45537 CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Sat Feb 21 11:38:14 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Sun Feb 22 03:44:03 2009 +0000 @@ -191,13 +191,13 @@ (* @end *) (* @chunk syntax *) -val ind_decl = +val specification = spec_parser >> (fn (((loc, preds), params), specs) => Toplevel.local_theory loc (add_inductive preds params specs)) val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" - OuterKeyword.thy_decl ind_decl + OuterKeyword.thy_decl specification (* @end *) end; diff -r 693711a0c702 -r e0d368a45537 CookBook/Tactical.thy --- 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 \ 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 diff -r 693711a0c702 -r e0d368a45537 cookbook.pdf Binary file cookbook.pdf has changed