# HG changeset patch # User Christian Urban # Date 1222906185 14400 # Node ID 2b07da8b310d27527ca1b5e17a7a877f73e15c78 # Parent 2f1736cb8f2653162a7ca302bcc5b92c11da309e polished and added a subdirectory for the recipes diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/Appendix.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Appendix.thy Wed Oct 01 20:09:45 2008 -0400 @@ -0,0 +1,15 @@ + +theory Appendix +imports Main +begin + +text {* \appendix *} + +chapter {* Recipes *} + + +end + + + + diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Oct 01 15:40:20 2008 -0400 +++ b/CookBook/FirstSteps.thy Wed Oct 01 20:09:45 2008 -0400 @@ -64,6 +64,8 @@ then Isabelle's undo operation has no effect on the definition of @{ML "foo"}. + (FIXME: add comment about including whole ML-files) + During developments you might find it necessary to quickly inspect some data in your code. This can be done in a ``quick-and-dirty'' fashion using the function @{ML "warning"}. For example @@ -75,8 +77,8 @@ text {* will print out @{ML "\"any string\""} inside the response buffer of Isabelle. - PolyML provides a convenient, though quick-and-dirty, method for converting - arbitrary values into strings, for example: + PolyML provides a convenient, though again ``quick-and-dirty'', method for + converting arbitrary values into strings, for example: *} ML {* @@ -88,8 +90,8 @@ a function. *} -text {* (FIXME: add comment about including ML-files) *} - +text {* (FIXME: add here or in the appendix a comment about tracing) *} +text {* (FIXME: maybe a comment about redirecting the trace information) *} section {* Antiquotations *} @@ -106,7 +108,7 @@ text {* where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory CookBook). - The name of this theory can be extrated using the function @{ML "Context.theory_name"}. + The name of this theory can be extracted using the function @{ML "Context.theory_name"}. So the code above returns the string @{ML "\"CookBook\""}. Note, however, that antiquotations are statically scoped, that is the value is @@ -135,7 +137,7 @@ text {* In the course of this introduction, we will learn more about - these antoquotations: they greatly simplify Isabelle programming since one + these antiquotations: they greatly simplify Isabelle programming since one can directly access all kinds of logical elements from ML. *} @@ -151,8 +153,8 @@ text {* This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal - representation of this term. This internal represenation corresponds to the - datatype defined in @{ML_file "Pure/term.ML"}. + representation of this term. This internal representation corresponds to the + datatype @{ML_text "term"}. The internal representation of terms uses the usual de-Bruijn index mechanism where bound variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to @@ -161,14 +163,16 @@ kept at abstractions for printing purposes, and so should be treated only as comments. \begin{readmore} - Terms are described in detail in \ichcite{ch:logic}. Their + Terms are described in detail in \isccite{sec:terms}. Their definition and many useful operations can be found in @{ML_file "Pure/term.ML"}. \end{readmore} - Sometimes the internal representation can be surprisingly different + Sometimes the internal representation of terms can be surprisingly different from what you see at the user level, because the layers of parsing/type checking/pretty printing can be quite elaborate. +*} +text {* \begin{exercise} Look at the internal term representation of the following terms, and find out why they are represented like this. @@ -181,43 +185,45 @@ Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you - can use @{ML "print_depth 50"} to set the limit to a value high enough. + can use the following ML funtion to set the limit to a value high + enough: \end{exercise} +*} +ML {* print_depth 50 *} - The anti-quotation @{text "@prop"} constructs terms of proposition type, - inserting the invisible @{text "Trueprop"} coercion when necessary. +text {* + + The antiquotation @{text "@{prop \}"} constructs terms of propositional type, + inserting the invisible @{text "Trueprop"} coercions whenever necessary. Consider for example *} -ML {* @{term "P x"} *} +ML {* @{term "P x"} ; @{prop "P x"} *} -ML {* @{prop "P x"} *} - -text {* and *} +text {* which needs the coercion and *} -ML {* @{term "P x \ Q x"} *} +ML {* @{term "P x \ Q x"} ; @{prop "P x \ Q x"} *} -ML {* @{prop "P x \ Q x"} *} +text {* which does not. *} -section {* Construting Terms Manually *} +section {* Constructing Terms Manually *} text {* While antiquotations are very convenient for constructing terms, they can - only construct fixed terms. However, one often needs to construct terms dynamially. - For example in order to write the function that returns the implication - @{term "\x. P x \ Q x"} taking @{term P} and @{term Q} as arguments, one can - only write + only construct fixed terms. Unfortunately, one often needs to construct terms + dynamically. For example, a function that returns the implication + @{text "\(x::nat). P x \ Q x"} taking @{term P} and @{term Q} as input terms + can only be written as *} ML {* - fun make_PQ_imp P Q = + fun make_imp P Q = let - val nat = HOLogic.natT - val x = Free ("x", nat) + val x = @{term "x::nat"} in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), HOLogic.mk_Trueprop (Q $ x))) end @@ -226,45 +232,52 @@ text {* The reason is that one cannot pass the arguments @{term P} and @{term Q} into - an antiquotation. + an antiquotation, like +*} + +ML {* + fun make_imp_wrong P Q = @{prop "\x. P x \ Q x"} *} text {* - The internal names of constants like @{term "zero"} or @{text "+"} are - often more complex than one first expects. Here, the extra prefixes - @{text zero_class} and @{text plus_class} are present because the - constants are defined within a type class. Guessing such internal - names can be extremely hard, which is why the system provides - another antiquotation: @{ML "@{const_name plus}"} gives just this - name. For example + To see the difference apply @{text "@{term S}"} and + @{text "@{term T}"} to the functions. + + + One tricky point in constructing terms by hand is to obtain the fully qualified + names for constants. For example the names for @{text "zero"} or @{text "+"} are + more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} + and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} + and @{ML_text plus_class} are present because these constants are defined + within type classes; the prefix @{text "HOL"} indicates in which theory they are + defined. Guessing such internal names can sometimes be quite hard. Therefore + Isabellle provides the antiquotation @{text "@{const_name \}"} does the expansion + automatically, for example: *} -ML {* @{const_name plus} *} - -text {* produes the fully qualyfied name of the constant plus. *} - - - +ML {* @{const_name HOL.zero}; @{const_name plus} *} text {* - There are many funtions in @{ML_file "Pure/logic.ML"} and + \begin{readmore} + There are many functions in @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms - easier. Have a look ther and try to solve the following exercises: + easier.\end{readmore} + + Have a look at these files and try to solve the following two exercises: *} text {* - \begin{exercise} + \begin{exercise}\label{fun:revsum} Write a function @{ML_text "rev_sum : term -> term"} that takes a term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "i"} might be zero) and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. Assume the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} - associates to the left. Try your function on some examples, and see if - the result typechecks. + associates to the left. Try your function on some examples. \end{exercise} *} @@ -298,10 +311,12 @@ section {* Type checking *} text {* + + (FIXME: Should we say something about types?) + We can freely construct and manipulate terms, since they are just arbitrary unchecked trees. However, we eventually want to see if a - term is wellformed, or type checks, relative to a theory. - + term is well-formed, or type checks, relative to a theory. Type checking is done via the function @{ML cterm_of}, which turns a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. Unlike @{ML_type term}s, which are just trees, @{ML_type @@ -327,37 +342,38 @@ end *} +text {* + + \begin{exercise} + Check that the function defined in Exercise~\ref{fun:revsum} returns a + result that type checks. + \end{exercise} + +*} + section {* Theorems *} text {* Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are abstract objects that can only be built by going through the kernel - interfaces, which means that all your proofs will be checked. The - basic rules of the Isabelle/Pure logical framework are defined in - @{ML_file "Pure/thm.ML"}. + interfaces, which means that all your proofs will be checked. - Using these rules, which are just ML functions, you can do simple - natural deduction proofs on the ML level. For example, the statement + To see theorems in ``action'', let us give a proof for the following statement *} lemma assumes assm\<^isub>1: "\(x::nat). P x \ Q x" and assm\<^isub>2: "P t" - shows "Q t" - (*<*)oops(*>*) + shows "Q t" (*<*)oops(*>*) text {* - can be proved in ML like - this\footnote{Note that @{text "|>"} is just reverse + on the ML level:\footnote{Note that @{text "|>"} is just reverse application. This combinator, and several variants are defined in - @{ML_file "Pure/General/basics.ML"}}: + @{ML_file "Pure/General/basics.ML"}.} *} - - ML {* - let val thy = @{theory} @@ -375,13 +391,15 @@ |> implies_intr assm2 |> implies_intr assm1 end - *} text {* - For how the functions @{text "assume"}, @{text "forall_elim"} and so on work - see \ichcite{sec:thms}. (FIXME correct name) + \begin{readmore} + For how the functions @{text "assume"}, @{text "forall_elim"} etc work + see \isccite{sec:thms}. The basic functions for theorems are defined in + @{ML_file "Pure/thm.ML"}. + \end{readmore} *} @@ -389,20 +407,26 @@ section {* Tactical Reasoning *} text {* - The goal-oriented tactical style is similar to the @{text apply} - style at the user level. Reasoning is centered around a \emph{goal}, - which is modified in a sequence of proof steps until it is solved. + The goal-oriented tactical style reasoning of the ML level is similar + to the @{text apply}-style at the user level, i.e.~the reasoning is centred + around a \emph{goal}, which is modified in a sequence of proof steps + until it is solved. A goal (or goal state) is a special @{ML_type thm}, which by convention is an implication of the form: @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ #(C)"} - Since the formula @{term C} could potentially be an implication, there is a + where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. + + Since the goal @{term C} can potentially be an implication, there is a @{text "#"} wrapped around it, which prevents that premises are misinterpreted as open subgoals. The protection @{text "# :: prop \ prop"} is just the identity function and used as a syntactic marker. - For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name) + + \begin{readmore} + For more on goals see \isccite{sec:tactical-goals}. + \end{readmore} Tactics are functions that map a goal state to a (lazy) sequence of successor states, hence the type of a tactic is @@ -410,18 +434,18 @@ \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy - sequences. However one rarly onstructs sequences manually, but uses - the predefined tactic combinators (tacticals) instead - (see @{ML_file "Pure/tctical.ML"}). + sequences. However in day-to-day Isabelle programming, one rarely + constructs sequences explicitly, but uses the predefined tactic + combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). + (FIXME: Pointer to the old reference manual) \end{readmore} - Note, however, that tactics are expected to behave nicely and leave - the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"} - representing the subgoals to be proved) with the exception of possibly - instantiating schematic variables. + While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they + are expected to leave the conclusion @{term C} intact, with the + exception of possibly instantiating schematic variables. - To see how tactics work, let us transcribe a simple apply-style proof from the - tutorial \cite{isa-tutorial} into ML: + To see how tactics work, let us transcribe a simple @{text apply}-style + proof from the tutorial \cite{isa-tutorial} into ML: *} lemma disj_swap: "P \ Q \ Q \ P" @@ -437,9 +461,9 @@ To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"} sets up a goal state for proving @{text goal} under the assumptions @{text assms} with - additional variables @{text params} (the variables that are generalised once the - goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing - explanation in the imp-manual). + the variables @{text params} that will be generalised once the + goal is proved; @{text "tac"} is a function that returns a tactic having some funny + input parameters (FIXME by possibly having an explanation in the implementation-manual). *} diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/NamedThms.thy --- a/CookBook/NamedThms.thy Wed Oct 01 15:40:20 2008 -0400 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,65 +0,0 @@ - -theory NamedThms -imports Main -begin - - -chapter {* Recipes *} - -text_raw {* - -\section*{Accumulate a list of theorems under a name} -*} - -text {* - \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules. - - Users should be able to declare @{text foo}-rules in the theory, - which are then used by some method. - - \paragraph{Solution:} - - *} -ML {* - structure FooRules = NamedThmsFun( - val name = "foo" - val description = "Rules for foo" - ); -*} - -setup FooRules.setup - -text {* - This declares a context data slot where the theorems are stored, - an attribute @{attribute foo} (with the usual @{text add} and @{text del} options - to declare new rules, and the internal ML interface to retrieve and - modify the facts. - - Furthermore, the facts are made available under the dynamic fact name - @{text foo}: -*} - -lemma rule1[foo]: "A" sorry -lemma rule2[foo]: "B" sorry - -declare rule1[foo del] - -thm foo - -ML {* - FooRules.get @{context}; -*} - - -text {* - \begin{readmore} - For more information see @{ML_file "Pure/Tools/named_thms.ML"}. - \end{readmore} - *} - - -end - - - - diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/ROOT.ML --- a/CookBook/ROOT.ML Wed Oct 01 15:40:20 2008 -0400 +++ b/CookBook/ROOT.ML Wed Oct 01 20:09:45 2008 -0400 @@ -3,5 +3,7 @@ use_thy "Intro"; use_thy "FirstSteps"; use_thy "Parsing"; -use_thy "NamedThms"; -use_thy "Transformation"; \ No newline at end of file + +use_thy "Appendix"; +use_thy "Recipes/NamedThms"; +use_thy "Recipes/Transformation"; \ No newline at end of file diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/Recipes/NamedThms.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Recipes/NamedThms.thy Wed Oct 01 20:09:45 2008 -0400 @@ -0,0 +1,61 @@ + +theory NamedThms +imports Main +begin + + +section {* Accumulate a List of Theorems under a Name *} + + +text {* + \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules. + + Users should be able to declare @{text foo}-rules in the theory, + which are then used by some method. + + \paragraph{Solution:} + + *} +ML {* + structure FooRules = NamedThmsFun( + val name = "foo" + val description = "Rules for foo" + ); +*} + +setup FooRules.setup + +text {* + This declares a context data slot where the theorems are stored, + an attribute @{attribute foo} (with the usual @{text add} and @{text del} options + to declare new rules, and the internal ML interface to retrieve and + modify the facts. + + Furthermore, the facts are made available under the dynamic fact name + @{text foo}: +*} + +lemma rule1[foo]: "A" sorry +lemma rule2[foo]: "B" sorry + +declare rule1[foo del] + +thm foo + +ML {* + FooRules.get @{context}; +*} + + +text {* + \begin{readmore} + For more information see @{ML_file "Pure/Tools/named_thms.ML"}. + \end{readmore} + *} + + +end + + + + diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/Recipes/Transformation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Recipes/Transformation.thy Wed Oct 01 20:09:45 2008 -0400 @@ -0,0 +1,15 @@ + +theory Transformation +imports Main +begin + + +section {* Ad-hoc Transformations of Theorems *} + + + +end + + + + diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/Transformation.thy --- a/CookBook/Transformation.thy Wed Oct 01 15:40:20 2008 -0400 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ - -theory Transformation -imports Main -begin - - -text_raw {* - -\section*{Ad-hoc Transformation of Theorems} -*} - - - -end - - - - diff -r 2f1736cb8f26 -r 2b07da8b310d CookBook/document/root.tex --- a/CookBook/document/root.tex Wed Oct 01 15:40:20 2008 -0400 +++ b/CookBook/document/root.tex Wed Oct 01 20:09:45 2008 -0400 @@ -9,8 +9,8 @@ \usepackage{xr} \externaldocument[I-]{implementation} \newcommand{\impref}[1]{\ref{I-#1}} -\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]} -\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]} +\newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]} +\newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]} \usepackage{pdfsetup} diff -r 2f1736cb8f26 -r 2b07da8b310d cookbook.pdf Binary file cookbook.pdf has changed