diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/FirstSteps.thy Thu Oct 30 13:36:51 2008 +0100 @@ -24,6 +24,8 @@ section {* Including ML-Code *} + + text {* The easiest and quickest way to include code in a theory is by using the \isacommand{ML} command. For example\smallskip @@ -37,18 +39,8 @@ Expressions inside \isacommand{ML} commands are immediately evaluated, like ``normal'' Isabelle proof scripts, 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. However on such \isacommand{ML} - commands the undo operation behaves slightly counter-intuitive, because - if you define\smallskip - -\isa{\isacommand{ML} -\isacharverbatimopen\isanewline -\hspace{5mm}@{ML_text "val foo = true"}\isanewline -\isacharverbatimclose\isanewline -@{ML_text "> true"}\smallskip} - - then Isabelle's undo operation has no effect on the definition of - @{ML_text "foo"}. Note that from now on we will drop the + can also contain value and function bindings, and even those can be + undone when the proof script is retracted. From now on we will drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever we show code and its response. @@ -78,7 +70,7 @@ @{ML [display] "warning \"any string\""} - will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle. + will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, for example: @@ -101,7 +93,7 @@ amounts of trace output. This rediretion can be achieved using the code *} -ML {* +ML{* val strip_specials = let fun strip ("\^A" :: _ :: cs) = strip cs @@ -113,7 +105,7 @@ Output.tracing_fn := (fn s => (TextIO.output (stream, (strip_specials s)); TextIO.output (stream, "\n"); - TextIO.flushOut stream)); + TextIO.flushOut stream)); *} text {* @@ -163,8 +155,8 @@ @{ML [display] "@{thm allI}"} @{ML [display] "@{simpset}"} - While antiquotations have many uses, they were introduced to avoid explicit - bindings for theorems such as + While antiquotations have many applications, they were originally introduced to + avoid explicit bindings for theorems such as *} ML {* @@ -172,14 +164,12 @@ *} text {* - These bindings were difficult to maintain and also could be overwritten - by bindings introduced by the user. This had the potential to break - definitional packages. This additional layer of maintenance complexity - can be avoided by using antiquotations, since they are ``linked'' statically - at compile time. 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. - + These bindings were difficult to maintain and also could be accidentally overwritten + by the user. This usually broke definitional packages. Antiquotations solve this + problem, since they are ``linked'' statically at compile time. 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. *} section {* Terms and Types *} @@ -208,10 +198,8 @@ 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. -*} + 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. @@ -246,24 +234,14 @@ which does not. Types can be constructed using the antiquotation @{text "@{typ \}"}. For example - - *} - - -text {* @{ML_response_fake [display] "@{typ \"bool \ nat\"}" "bool \ nat"} - (FIXME: Unlike the term antiquotation, @{text "@{typ \}"} does not print the - internal representation. Is there a reason for this, that needs to be explained - here?) - \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"}. \end{readmore} - - *} +*} section {* Constructing Terms and Types Manually *} @@ -271,7 +249,7 @@ text {* While antiquotations are very convenient for constructing terms and types, - they can only construct fixed terms. Unfortunately, one often needs to construct them + they can only construct fixed terms. Unfortunately, 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 typ @{term "\"} as arguments can only be written as @@ -289,7 +267,8 @@ 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 not work. + @{term "tau"} into an antiquotation. For example the following does not work as + expected. *} ML {* @@ -350,6 +329,8 @@ section {* Type Checking *} +ML {* cterm_of @{theory} @{term "a + b = c"} *} + text {* We can freely construct and manipulate terms, since they are just @@ -364,11 +345,15 @@ Type checking is always relative to a theory context. For now we can use the @{ML "@{theory}"} antiquotation to get hold of the current theory. - For example we can write: + For example we can write + + @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"} + + or use the antiquotation @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} - and + A slightly more elaborate example is @{ML_response_fake [display] "let