# HG changeset patch # User Christian Urban # Date 1233222396 0 # Node ID fee4942c4770d8765d8f33e826592c158d5898ba # Parent ebbd0dd008c880d8ed70b791cca4d4e265996d58 polishing diff -r ebbd0dd008c8 -r fee4942c4770 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Jan 29 09:46:17 2009 +0000 +++ b/CookBook/FirstSteps.thy Thu Jan 29 09:46:36 2009 +0000 @@ -7,7 +7,7 @@ text {* Isabelle programming is done in ML. Just like lemmas and proofs, ML-code - in Isabelle is part of a theory. If you want to follow the code written in + in Isabelle is part of a theory. If you want to follow the code given in this chapter, we assume you are working inside the theory starting with \begin{center} @@ -26,7 +26,7 @@ text {* The easiest and quickest way to include code in a theory is - by using the \isacommand{ML}-command. For example\smallskip + by using the \isacommand{ML}-command. For example: \begin{isabelle} \begin{graybox} @@ -37,17 +37,17 @@ \end{graybox} \end{isabelle} - Like ``normal'' Isabelle proof scripts, + Like normal Isabelle proof scripts, \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of your Isabelle environment. The code inside the \isacommand{ML}-command can also contain value and function bindings, and even those can be undone when the proof script is retracted. As mentioned earlier, we will drop the \isacommand{ML}~@{text "\ \ \"} - whenever we show code. + scaffolding whenever we show code. Once a portion of code is relatively stable, one usually wants to export it to a separate ML-file. Such files can then be included in a - theory by using \isacommand{uses} in the header of the theory, like + theory by using the \isacommand{uses}-command in the header of the theory, like: \begin{center} \begin{tabular}{@ {}l} @@ -85,7 +85,7 @@ output this function generates will be overwritten as soon as an error is raised. For printing anything more serious and elaborate, the function @{ML tracing} is more appropriate. This function writes all output into - a separate tracing buffer. For example + a separate tracing buffer. For example: @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} @@ -111,7 +111,7 @@ Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{text "foo.bar"}. - Error messages can be printed using the function @{ML error}, as in + You can print out error messages with the function @{ML error}, as in: @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""} @@ -134,10 +134,10 @@ where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory - @{text FirstSteps}). The name of this theory can be extracted with + @{text FirstSteps}). The name of this theory can be extracted using the function @{ML "Context.theory_name"}. - Note, however, that antiquotations are statically scoped, that is their value is + Note, however, that antiquotations are statically linked, that is their value is determined at ``compile-time'', not ``run-time''. For example the function *} @@ -145,7 +145,7 @@ text {* - does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a + does \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function that always returns the string @{text [quotes] "FirstSteps"}, no matter where the function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is @@ -161,12 +161,12 @@ @{ML_response_fake [display,gray] "let - val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset} + val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset} in map #name (Net.entries rules) end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} - The code about simpsets extracts the theorem names that are stored in the + The code about simpsets extracts the theorem names stored in the current simpset. We get hold of the current simpset with the antiquotation @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record containing all information about the simpset. The rules of a simpset are @@ -182,20 +182,20 @@ \end{readmore} While antiquotations have many applications, they were originally introduced in order - to avoid explicit bindings for theorems such as + to avoid explicit bindings for theorems such as: *} ML{*val allI = thm "allI" *} text {* These bindings are difficult to maintain and also can be accidentally - overwritten by the user. This often breakes definitional + overwritten by the user. This often breakes 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 course of - this introduction, we will learn more about - these antiquotations: they greatly simplify Isabelle programming since one - can directly access all kinds of logical elements from ML. + statically at compile-time. However, this static linkage also limits their + usefulness in cases where data needs to be build up dynamically. In the + course of this introduction, we will learn more about these antiquotations: + they greatly simplify Isabelle programming since one can directly access all + kinds of logical elements from th ML-level. *} @@ -203,7 +203,7 @@ text {* One way to construct terms of Isabelle on the ML-level is by using the antiquotation - \mbox{@{text "@{term \}"}}. For example + \mbox{@{text "@{term \}"}}. For example: @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" @@ -231,7 +231,7 @@ \begin{exercise} Look at the internal term representation of the following terms, and - find out why they are represented like this. + find out why they are represented like this: \begin{itemize} \item @{term "case x of 0 \ 0 | Suc y \ y"} @@ -261,7 +261,7 @@ where it is not (since it is already constructed by a meta-implication). - Types can be constructed using the antiquotation @{text "@{typ \}"}. For example + Types can be constructed using the antiquotation @{text "@{typ \}"}. For example: @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ nat"} @@ -279,11 +279,11 @@ While antiquotations are very convenient for constructing terms, they can only construct fixed terms (remember they are ``linked'' at compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external} - for a function that pattern-matches over terms and where the pattern are - constructed from antiquotations. However, one often needs to construct + for a function that pattern-matches over terms and where the patterns are + constructed using antiquotations. However, one often needs to construct terms dynamically. For example, a function that returns the implication @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the type @{term - "\"} as arguments can only be written as + "\"} as arguments can only be written as: *} ML{*fun make_imp P Q tau = @@ -294,7 +294,6 @@ end *} text {* - The reason is that one cannot pass the arguments @{term P}, @{term Q} and @{term "tau"} into an antiquotation. For example the following does \emph{not} work: *} @@ -357,7 +356,7 @@ text {* \begin{readmore} - There are many functions in @{ML_file "Pure/logic.ML"} and + There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms and types easier.\end{readmore} @@ -381,8 +380,23 @@ number representing their sum. \end{exercise} + (FIXME: maybe should go) - (FIXME: operation from page 19 of the implementation manual) +*} + +ML{*fun nat_to_int t = + (case t of + @{typ nat} => @{typ int} + | Type (s, ts) => Type (s, map nat_to_int ts) + | _ => t)*} + +text {* + +@{ML_response_fake [display,gray] +"map_types nat_to_int @{term \"a = (1::nat)\"}" +"Const (\"op =\", \"int \ int \ bool\") + $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} + *} section {* Type-Checking *} @@ -431,7 +445,7 @@ result that type-checks. \end{exercise} - (FIXME: @{text "ctyp_of"}) + (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT}) *} @@ -676,13 +690,33 @@ ML{*val double = (fn x => (x, x)) #-> (fn x => fn y => x + y)*} - text {* - - (FIXME: find a good exercise for combinators) *} + +(*<*) +setup {* + Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] +*} + +lemma "bar = (1::nat)" + oops + +setup {* + Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] + #> PureThy.add_defs false [((Binding.name "foo_def", + Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] + #> snd +*} + +lemma "foo = (1::nat)" + apply(simp add: foo_def) + done + +thm foo_def +(*>*) + end \ No newline at end of file diff -r ebbd0dd008c8 -r fee4942c4770 CookBook/Intro.thy --- a/CookBook/Intro.thy Thu Jan 29 09:46:17 2009 +0000 +++ b/CookBook/Intro.thy Thu Jan 29 09:46:36 2009 +0000 @@ -7,12 +7,14 @@ chapter {* Introduction *} text {* - The purpose of this Cookbook is to guide the reader through the first steps - of Isabelle programming, and to explain tricks of the trade. The code - provided in the Cookbook is as far as possible checked against recent - versions of Isabelle. If something does not work, then please let us - know. If you have comments, criticism or like to add to the Cookbook, - feel free---you are most welcome! + If your next project requires you to program on the ML-level of Isabelle, + then this Cookbook is for you. It will guide you through the first steps of + Isabelle programming, and also explain tricks of the trade. The best way to + get to know the ML-level of Isabelle is by experimenting with the many code + examples included in the Cookbook. The code is as far as possible checked + against recent versions of Isabelle. If something does not work, then + please let us know. If you have comments, criticism or like to add to the + Cookbook, feel free---you are most welcome! *} section {* Intended Audience and Prior Knowledge *} @@ -41,7 +43,7 @@ \item[The Isabelle Reference Manual] is an older document that used to be the main reference of Isabelle at a time when all proof scripts - were written on the ML level. Many parts of this manual are outdated + were written on the ML-level. Many parts of this manual are outdated now, but some parts, particularly the chapters on tactics, are still useful. @@ -56,8 +58,8 @@ \item[The code] is of course the ultimate reference for how 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, to - learn from other people's code. + good to look at code that does similar things as you want to do and + to learn from other people's code. \end{description} *} @@ -66,8 +68,8 @@ text {* - All ML-code in this Cookbook is typeset in highlighed boxes, like the following - ML-expression. + All ML-code in this Cookbook is typeset in highlighted boxes, like the following + ML-expression: \begin{isabelle} \begin{graybox} @@ -77,28 +79,28 @@ \end{graybox} \end{isabelle} - This corresponds to how code can be processed inside the interactive - environment of Isabelle. It is therefore easy to experiment with the code - (which by the way is highly recommended). However, for better readability we - will drop the enclosing \isacommand{ML}~@{text "\ \ \"} and just write + These boxes corresponds to how code can be processed inside the interactive + environment of Isabelle. It is therefore easy to experiment with what is + displayed. However, for better readability we will drop the enclosing + \isacommand{ML}~@{text "\ \ \"} and just write: @{ML [display,gray] "3 + 4"} - for the code above. Whenever appropriate we also show the response the code + Whenever appropriate we also show the response the code generates when evaluated. This response is prefixed with a - @{text [quotes] ">"} like + @{text [quotes] ">"} like: @{ML_response [display,gray] "3 + 4" "7"} The usual Isabelle commands are written in bold, for example \isacommand{lemma}, \isacommand{foobar} and so on. We use @{text "$"} to indicate that - a command needs to be run on the Unix-command line, for example + a command needs to be run in the Unix-shell, for example @{text [display] "$ ls -la"} - Pointers to further information and Isabelle files are given - as follows: + Pointers to further information and Isabelle files are typeset in + italic and highlighted as follows: \begin{readmore} Further information or pointer to file. diff -r ebbd0dd008c8 -r fee4942c4770 CookBook/document/root.tex --- a/CookBook/document/root.tex Thu Jan 29 09:46:17 2009 +0000 +++ b/CookBook/document/root.tex Thu Jan 29 09:46:36 2009 +0000 @@ -12,6 +12,7 @@ \usepackage{lineno} \usepackage{xcolor} \usepackage{framed} +\usepackage{mathpartir} \usepackage{pdfsetup} \urlstyle{rm} diff -r ebbd0dd008c8 -r fee4942c4770 cookbook.pdf Binary file cookbook.pdf has changed