# HG changeset patch # User Christian Urban # Date 1229132002 0 # Node ID 1783211b34947a2cbb99b21f76bce8a52f0858c5 # Parent 0c3580c831a4b5bbc751a32bbd94e852d0159950 tuned; added document antiquotation ML_response_fake_both diff -r 0c3580c831a4 -r 1783211b3494 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Sat Nov 29 21:20:18 2008 +0000 +++ b/CookBook/FirstSteps.thy Sat Dec 13 01:33:22 2008 +0000 @@ -7,9 +7,9 @@ text {* - Isabelle programming is done in SML. Just like lemmas and proofs, SML-code + 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 - this chapter, we assume you are working inside the theory defined by + this chapter, we assume you are working inside the theory starting with \begin{center} \begin{tabular}{@ {}l} @@ -49,7 +49,7 @@ \begin{center} \begin{tabular}{@ {}l} - \isacommand{theory} CookBook\\ + \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\"}\\ \isacommand{begin}\\ @@ -82,12 +82,12 @@ The function @{ML "warning"} should only be used for testing purposes, because any 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} should be used. This function writes all output into + function @{ML tracing} is more appropriate. This function writes all output into a separate tracing buffer. For example @{ML [display] "tracing \"foo\""} - It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is + It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is printed to a separate file, e.g. to prevent Proof General from choking on massive amounts of trace output. This redirection can be achieved using the code *} @@ -152,8 +152,11 @@ In a similar way you can use antiquotations to refer to theorems or simpsets: - @{ML [display] "@{thm allI}"} - @{ML [display] "@{simpset}"} + @{ML_response_fake [display] "@{thm allI}" "(\x. ?P x) \ \x. ?P x"} + @{ML_response_fake [display] "@{simpset}" "\"} + + (FIXME: what does a simpset look like? It seems to be the same problem + like tokens.) While antiquotations have many applications, they were originally introduced to avoid explicit bindings for theorems such as @@ -241,7 +244,7 @@ \begin{readmore} Types are described in detail in \isccite{sec:types}. Their - definition and many useful operations can be found in @{ML_file "Pure/type.ML"}. + definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}. \end{readmore} *} @@ -350,7 +353,7 @@ We can freely construct and manipulate terms, since they are just arbitrary unchecked trees. However, we eventually want to see if a - term is well-formed, 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 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. Unlike @{ML_type term}s, which are just trees, @{ML_type @@ -358,7 +361,7 @@ type-correct, and that can only be constructed via the ``official interfaces''. - Type checking is always relative to a theory context. For now we use + Type-checking is always relative to a theory context. For now we use the @{ML "@{theory}"} antiquotation to get hold of the current theory. For example we can write @@ -368,7 +371,11 @@ @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} - A slightly more elaborate example is + Attempting + + @{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \"} + + yields an error. A slightly more elaborate example is @{ML_response_fake [display] "let @@ -391,8 +398,8 @@ text {* Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} - that can only be built by going through interfaces, which means that all your proofs - will be checked. + that can only be built by going through interfaces. In effect all proofs + are checked. To see theorems in ``action'', let us give a proof for the following statement *} @@ -472,7 +479,8 @@ prop"} is just the identity function and used as a syntactic marker. \begin{readmore} - For more on goals see \isccite{sec:tactical-goals}. + For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which + file is most code for dealing with goals?) \end{readmore} Tactics are functions that map a goal state to a (lazy) @@ -525,7 +533,8 @@ end" "?P \ ?Q \ ?Q \ ?P"} \begin{readmore} - To learn more about the function @{ML Goal.prove} see \isccite{sec:results}. + To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and + the file @{ML_file "Pure/goal.ML"}. \end{readmore} diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Intro.thy --- a/CookBook/Intro.thy Sat Nov 29 21:20:18 2008 +0000 +++ b/CookBook/Intro.thy Sat Dec 13 01:33:22 2008 +0000 @@ -6,9 +6,10 @@ chapter {* Introduction *} text {* - The purpose of this cookbook is to guide the reader through the + The purpose of this Cookbook is to guide the reader through the first steps of Isabelle programming, and to provide recipes for - solving common problems. + solving common problems. The code provided in the Cookbook is + checked against recent versions of Isabelle. *} section {* Intended Audience and Prior Knowledge *} @@ -16,10 +17,10 @@ text {* This cookbook targets an audience who already knows how to use Isabelle for writing theories and proofs. We also assume that readers are - familiar with Standard ML (SML), the programming language in which - most of Isabelle is implemented. If you are unfamiliar with either of + familiar with the functional programming language ML, the language in + which most of Isabelle is implemented. If you are unfamiliar with either of these two subjects, you should first work through the Isabelle/HOL - tutorial \cite{isa-tutorial} or Paulson's book on SML + tutorial \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. *} @@ -57,9 +58,6 @@ learn from other people's code. \end{description} - The Cookbook is written in such a way that the code examples in it are - checked against recent versions of the code. - *} diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Sat Nov 29 21:20:18 2008 +0000 +++ b/CookBook/Parsing.thy Sat Dec 13 01:33:22 2008 +0000 @@ -399,7 +399,7 @@ end" "([\"in\",\"in\",\"in\"],[])"} - The following function will help us to run examples + The following function will help us later to run examples *} @@ -427,8 +427,8 @@ \begin{exercise} A type-identifier, for example @{typ "'a"}, is a token of - kind @{ML "Keyword" in OuterLex} can be parsed - + kind @{ML "Keyword" in OuterLex}. It can be parsed using + the function @{ML OuterParse.type_ident}. \end{exercise} diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Readme.thy --- a/CookBook/Readme.thy Sat Nov 29 21:20:18 2008 +0000 +++ b/CookBook/Readme.thy Sat Dec 13 01:33:22 2008 +0000 @@ -15,7 +15,7 @@ \item You can include references to other Isabelle manuals using the reference names from those manuals. To do this the following - four latex commands are defined: + four \LaTeX{} commands are defined: \begin{center} \begin{tabular}{l|c|c} @@ -44,7 +44,7 @@ free variables. The latter is used to indicate in which structure or structures the ML-expression should be evaluated. Examples are: - \begin{center} + \begin{center}\small \begin{tabular}{l} @{text "@{ML \"1 + 3\"}"}\\ @{text "@{ML \"a + b\" for a b}"}\\ @@ -67,6 +67,10 @@ the @{ML_text ML_response}-anti\-quotation, except that the result-specification is not checked. Use this antiquotation if the result cannot be constructed or the code generates an exception. + + \item[$\bullet$] @{text "@{ML_response_fake_both \"\\" \"\\"}"} can be + used to show erroneous code. Neither the code nor the response will be + chacked. \item[$\bullet$] @{text "@{ML_file \"\\"}"} Should be used when referring to a file. It checks whether the file exists. diff -r 0c3580c831a4 -r 1783211b3494 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Sat Nov 29 21:20:18 2008 +0000 +++ b/CookBook/antiquote_setup.ML Sat Dec 13 01:33:22 2008 +0000 @@ -43,6 +43,10 @@ let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) +fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = + let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) + in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end + fun check_file_exists ctxt txt = if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () else error ("Source file " ^ quote txt ^ " does not exist.") @@ -60,6 +64,8 @@ (output_ml_response ml_pat)), ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) (output_ml_response_fake ml_val)), + ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) + (output_ml_response_fake_both ml_val)), ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; diff -r 0c3580c831a4 -r 1783211b3494 cookbook.pdf Binary file cookbook.pdf has changed