# HG changeset patch # User Christian Urban # Date 1236085255 0 # Node ID e8f11280c762cc99de437507073246589148bdc1 # Parent b6fca043a79655cf8a1323a2b50802df188516b3 polished diff -r b6fca043a796 -r e8f11280c762 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Mar 02 10:06:06 2009 +0000 +++ b/CookBook/FirstSteps.thy Tue Mar 03 13:00:55 2009 +0000 @@ -406,13 +406,16 @@ \emph{discrimination net} (a data structure for fast indexing). From this net you can extract the entries using the function @{ML Net.entries}. You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored - in the current simpset---this simpset can be referred to using the antiquotation + in the current simpset. This simpset can be referred to using the antiquotation @{text "@{simpset}"}. @{ML_response_fake [display,gray] "get_thm_names_from_ss @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} + Again, this way or referencing simpsets makes you independent from additions + of lemmas to the simpset by the user that potentially cause loops. + \begin{readmore} The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"} and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented @@ -427,7 +430,7 @@ text {* These bindings are difficult to maintain and also can be accidentally - overwritten by the user. This often breakes Isabelle + overwritten by the user. This often broke Isabelle packages. Antiquotations solve this problem, since they are ``linked'' statically at compile-time. However, this static linkage also limits their usefulness in cases where data needs to be build up dynamically. In the @@ -513,7 +516,7 @@ *} -section {* Constructing Terms and Types Manually *} +section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} text {* While antiquotations are very convenient for constructing terms, they can @@ -568,13 +571,13 @@ ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *} -text {* This can be equally written as: *} +text {* This can be equally written with the combinator @{ML "-->"} as: *} ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} text {* A handy function for manipulating terms is @{ML map_types}: it takes a - function and applies it to every type in the term. You can, for example, + function and applies it to every type in a term. You can, for example, change every @{typ nat} in a term into an @{typ int} using the function: *} @@ -918,7 +921,7 @@ context (which we ignore in the code above) and a theorem (@{text thm}), and returns another theorem (namely @{text thm} resolved with the lemma @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns - an attribute (of type @{ML_type "attribute"}). + an attribute. Before we can use the attribute, we need to set it up. This can be done using the function @{ML Attrib.add_attributes} as follows. @@ -974,7 +977,7 @@ text {* These functions take a theorem and a context and, for what we are explaining - here it is sufficient to just return the context unchanged. They change + here it is sufficient that they just return the context unchanged. They change however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm} adds a theorem if it is not already included in the list, and @{ML Thm.del_thm} deletes one. Both functions use the predicate @{ML @@ -982,7 +985,7 @@ propositions (modulo alpha-equivalence). - We can turn both functions into attributes using + You can turn both functions into attributes using *} ML{*val my_add = Thm.declaration_attribute my_thms_add @@ -1009,7 +1012,7 @@ @{ML_response_fake [display,gray] "!my_thms" "[\"True\"]"} - We can also add theorems using the command \isacommand{declare} + You can also add theorems using the command \isacommand{declare} *} declare test[my_thms] trueI_2[my_thms add] @@ -1030,7 +1033,7 @@ declare test[my_thms del] -text {* After this, the theorem list is: +text {* After this, the theorem list is again: @{ML_response_fake [display,gray] "!my_thms" @@ -1040,7 +1043,7 @@ but there can be any number of them. We just have to change the parser for reading the arguments accordingly. - However, as said at the beginning using references for storing theorems is + However, as said at the beginning of this example, using references for storing theorems is \emph{not} the received way of doing such things. The received way is to start a ``data slot'' in a context by using the functor @{text GenericDataFun}: *} @@ -1052,7 +1055,7 @@ fun merge _ = Thm.merge_thms) *} text {* - To use this data slot, we only have to change the functions @{ML my_thms_add} and + To use this data slot, you only have to change @{ML my_thms_add} and @{ML my_thms_del} to: *} @@ -1083,7 +1086,7 @@ modify the theorems. Furthermore, the facts are made available on the user level under the dynamic - fact name @{text foo}. For example we can declare three lemmas to be of the kind + fact name @{text foo}. For example you can declare three lemmas to be of the kind @{text foo} by: *} @@ -1103,7 +1106,7 @@ @{text "> ?B"} \end{isabelle} - On the ML-level the rules marked with @{text "foo"} an be retrieved + On the ML-level the rules marked with @{text "foo"} can be retrieved using the function @{ML FooRules.get}: @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} @@ -1114,10 +1117,7 @@ data. \end{readmore} - (FIXME What are: - - @{text "theory_attributes"} - @{text "proof_attributes"}) + (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?) \begin{readmore} diff -r b6fca043a796 -r e8f11280c762 CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Mar 02 10:06:06 2009 +0000 +++ b/CookBook/Intro.thy Tue Mar 03 13:00:55 2009 +0000 @@ -50,7 +50,7 @@ \item[The Isar Reference Manual] provides specification material (like grammars, examples and so on) about Isar and its implementation. It is currently in - the process of being updated. . + the process of being updated. \end{description} Then of course there is: @@ -60,7 +60,7 @@ things really work. Therefore you should not hesitate to look at the way things are actually implemented. More importantly, it is often good to look at code that does similar things as you want to do and - to learn from other people's code. + to learn from that code. \end{description} *} @@ -108,6 +108,10 @@ Further information or pointers to files. \end{readmore} + A few exercises a scattered around the text. Their solutions are given + in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try + to solve the exercises on your own. + *} section {* Acknowledgements *} @@ -115,7 +119,7 @@ text {* Financial support for this tutorial was provided by the German Research Council (DFG) under grant number URB 165/5-1. The following - people contributed: + people contributed to the text: \begin{itemize} \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the diff -r b6fca043a796 -r e8f11280c762 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Mar 02 10:06:06 2009 +0000 +++ b/CookBook/Parsing.thy Tue Mar 03 13:00:55 2009 +0000 @@ -11,7 +11,7 @@ Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so on, belong to the outer syntax, whereas items inside double quotation marks, such as terms, types and so on, belong to the inner syntax. For parsing inner syntax, - Isabelle uses a rather general and sophisticated algorithm due to Earley, which + Isabelle uses a rather general and sophisticated algorithm, which is driven by priority grammars. Parsers for outer syntax are built up by functional parsing combinators. These combinators are a well-established technique for parsing, which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}. @@ -348,7 +348,7 @@ text {* Most of the time, however, Isabelle developers have to deal with parsing - tokens, not strings. These token parsers will have the type: + tokens, not strings. These token parsers have the type: *} ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*} @@ -601,7 +601,7 @@ text {* There are a number of special purpose parsers that help with parsing - specifications of functions, inductive definitions and so on. In + specifications of function definitions, inductive predicates and so on. In Capter~\ref{chp:package}, for example, we will need to parse specifications for inductive predicates of the form: *} @@ -613,6 +613,8 @@ | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" +text {* and *} + simple_inductive trcl\ for R :: "'a \ 'a \ bool" where @@ -692,8 +694,8 @@ *} text {* - Whenever types are given, they are stored in the @{ML SOME}s. They types are - not yet given to the variable: this must be done by type inference later + Whenever types are given, they are stored in the @{ML SOME}s. The types are + not yet used to type the variables: this must be done by type-inference later on. Since types are part of the inner syntax they are strings with some encoded information (see previous section). If a syntax translation is present for a variable, then it is stored in the @{ML Mixfix} datastructure; @@ -853,7 +855,7 @@ @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} - on the Unix prompt. If you now also type @{text "ls $ISABELLE_LOGS"}, then the + on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the directory should include the files: @{text [display] diff -r b6fca043a796 -r e8f11280c762 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Mon Mar 02 10:06:06 2009 +0000 +++ b/CookBook/Solutions.thy Tue Mar 03 13:00:55 2009 +0000 @@ -3,7 +3,7 @@ uses "infix_conv.ML" begin -chapter {* Solutions to Most Exercises *} +chapter {* Solutions to Most Exercises\label{ch:solutions} *} text {* \solution{fun:revsum} *} diff -r b6fca043a796 -r e8f11280c762 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Mon Mar 02 10:06:06 2009 +0000 +++ b/CookBook/Tactical.thy Tue Mar 03 13:00:55 2009 +0000 @@ -289,8 +289,8 @@ printed by the Isabelle system and by @{ML my_print_tac}. The latter shows the goal state as represented internally (highlighted boxes). This illustrates that every goal state in Isabelle is represented by a theorem: - when we start the proof of \mbox{@{text "\A; B\ \ A \ B"}} the theorem is - @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"}; when we finish the proof the + when you start the proof of \mbox{@{text "\A; B\ \ A \ B"}} the theorem is + @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"}; when you finish the proof the theorem is @{text "\A; B\ \ A \ B"}.\label{fig:goalstates}} \end{figure} *} @@ -328,8 +328,9 @@ text {* Let us start with the tactic @{ML print_tac}, which is quite useful for low-level - debugging of tactics. It just prints out a message and the current goal state. - Processing the proof + debugging of tactics. It just prints out a message and the current goal state + (unlike @{ML my_print_tac} it prints the goal state as the user would see it). + For example, processing the proof *} lemma shows "False \ True" @@ -386,7 +387,7 @@ text {* Note the number in each tactic call. Also as mentioned in the previous section, most - basic tactics take such an argument; it addresses the subgoal they are analysing. + basic tactics take such a number as argument; it addresses the subgoal they are analysing. In the proof below, we first split up the conjunction in the second subgoal by focusing on this subgoal first. *} @@ -692,10 +693,12 @@ construct the patterns, the pattern in Line 8 cannot be constructed in this way. The reason is that an antiquotation would fix the type of the quantified variable. So you really have to construct the pattern using the - basic term-constructors. This is not necessary in other cases, because their type - is always fixed to function types involving only the type @{typ bool}. For the - final pattern, we chose to just return @{ML all_tac}. Consequently, - @{ML select_tac} never fails. + basic term-constructors. This is not necessary in other cases, because their + type is always fixed to function types involving only the type @{typ + bool}. (See Section \ref{sec:terms_types_manually} about constructing terms + manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. + Consequently, @{ML select_tac} never fails. + Let us now see how to apply this tactic. Consider the four goals: *} @@ -924,7 +927,7 @@ @{ML REPEAT1} is similar, but runs the tactic at least once (failing if this is not possible). - If you are after the ``primed'' version of @{ML repeat_xmp} then you + If you are after the ``primed'' version of @{ML repeat_xmp}, then you need to implement it as *} diff -r b6fca043a796 -r e8f11280c762 cookbook.pdf Binary file cookbook.pdf has changed