isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:81e2d73f7191
+:4daf913fdbe1
 \end{center}
 *}
 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
 \isa{\isacommand{ML}
 @{ML_text "> 7"}\smallskip}
 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}
+can also contain value and function bindings, and even those can be
-commands the undo operation behaves slightly counter-intuitive, because
+undone when the proof script is retracted. From now on we will drop the
-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
 \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
 we show code and its response.
 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
 in your code. This can be done in a ``quick-and-dirty'' fashion using
 the function @{ML "warning"}. For example
 @{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:
 @{ML [display] "warning (makestring 1)"}
 It is also possible to redirect the channel where the @{ML_text "foo"} is
 printed to a separate file, e.g. to prevent Proof General from choking on massive
 amounts of trace output. This rediretion can be achieved using the code
 *}
-ML {*
+ML{*
 val strip_specials =
 let
 fun strip ("\^A" :: _ :: cs) = strip cs
 | strip (c :: cs) = c :: strip cs
 | strip [] = [];
 fun redirect_tracing stream =
 Output.tracing_fn := (fn s =>
 (TextIO.output (stream, (strip_specials s));
 TextIO.output (stream, "\n");
 TextIO.flushOut stream));
 *}
 text {*
 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
 In a similar way you can use antiquotations to refer to theorems or simpsets:
 @{ML [display] "@{thm allI}"}
 @{ML [display] "@{simpset}"}
-While antiquotations have many uses, they were introduced to avoid explicit
+While antiquotations have many applications, they were originally introduced to
-bindings for theorems such as
+avoid explicit bindings for theorems such as
 *}
 ML {*
 val allI = thm "allI"
 *}
 text {*
-These bindings were difficult to maintain and also could be overwritten
+These bindings were difficult to maintain and also could be accidentally overwritten
-by bindings introduced by the user. This had the potential to break
+by the user. This usually broke definitional packages. Antiquotations solve this
-definitional packages. This additional layer of maintenance complexity
+problem, since they are ``linked'' statically at compile time.  In the course of this
-can be avoided by using antiquotations, since they are ``linked'' statically
+introduction, we will learn more about these antiquotations: they greatly simplify
-at compile time.  In the course of this introduction, we will learn more about
+Isabelle programming since one can directly access all kinds of logical elements
-these antiquotations: they greatly simplify Isabelle programming since one
+from ML.
-can directly access all kinds of logical elements from ML.
 *}
 section {* Terms and Types *}
 text {*
 definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
 \end{readmore}
 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.
 \begin{itemize}
 @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
 which does not.
 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
-*}
-text {*
 @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
-(FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} 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 *}
 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 "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
 as arguments can only be written as
 *}
 *}
 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 {*
 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
 *}
 \end{exercise}
 *}
 section {* Type Checking *}
+ML {* cterm_of @{theory} @{term "a + b = c"} *}
 text {*
 We can freely construct and manipulate terms, since they are just
 arbitrary unchecked trees. However, we eventually want to see if a
 type-correct, and that can only be constructed via the official
 interfaces.
 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
 val natT = @{typ \"nat\"}
 val zero = @{term \"0::nat\"}

changeset 47	4daf913fdbe1
parent 43	02f76f1b6e7b
child 48	609f9ef73494