--- a/CookBook/FirstSteps.thy Thu Oct 02 05:30:46 2008 -0400
+++ b/CookBook/FirstSteps.thy Sun Oct 05 14:29:13 2008 -0400
@@ -36,7 +36,7 @@
*}
text {*
- The expression inside \isacommand{ML} commands is immediately evaluated,
+ 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}
@@ -80,22 +80,24 @@
text {*
will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
- PolyML provides a convenient, though again ``quick-and-dirty'', method for
- converting arbitrary values into strings, for example:
+ If you develop under PolyML, then there is a convenient, though again
+ ``quick-and-dirty'', method for converting values into strings,
+ for example:
*}
ML {* warning (makestring 1) *}
text {*
- However this only works if the type of what is printed is monomorphic and not
+ However this only works if the type of what is converted is monomorphic and not
a function.
*}
text {*
The funtion warning should only be used for testing purposes, because
- any output this funtion generated will be overwritten, if an error is raised.
- For printing anything more serious and elaborate, the function @{ML tracing}
- should be used. This function writes all output in a separate buffer.
+ any output this funtion generates will be overwritten, as soon as an error
+ is raised.
+ Therefore for printing anything more serious and elaborate, the function @{ML tracing}
+ should be used. This function writes all output into a separate buffer.
*}
ML {* tracing "foo" *}
@@ -124,7 +126,7 @@
*}
text {*
- Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"}
+ Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
*}
@@ -154,7 +156,7 @@
*}
ML {*
- fun current_thyname () = Context.theory_name @{theory}
+ fun not_current_thyname () = Context.theory_name @{theory}
*}
text {*
@@ -166,10 +168,9 @@
some data structure and return it. Instead, it is literally
replaced with the value representing the theory name.
- In a similar way you can use antiquotations to refer to types and theorems:
+ In a similar way you can use antiquotations to refer to theorems:
*}
-ML {* @{typ "(int * nat) list"} *}
ML {* @{thm allI} *}
text {*
@@ -238,31 +239,51 @@
ML {* @{term "P x"} ; @{prop "P x"} *}
-text {* which inserts the coercion in the latter ase and *}
+text {* which inserts the coercion in the latter case and *}
ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
-text {* which does not. *}
+text {*
+ which does not.
+
+ Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
+
+ *}
+
+ML {* @{typ "bool \<Rightarrow> nat"} *}
-text {* (FIXME: add something about @{text "@{typ \<dots>}"}) *}
+text {*
+ (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 (similarly types),
+ While antiquotations are very convenient for constructing terms and types,
they can only construct fixed terms. Unfortunately, one often needs to construct them
dynamically. For example, a function that returns the implication
- @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments
- can only be written as
+ @{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
*}
ML {*
- fun make_imp P Q =
+ fun make_imp P Q tau =
let
- val x = @{term "x::nat"}
+ val x = Free ("x",tau)
in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
HOLogic.mk_Trueprop (Q $ x)))
end
@@ -270,21 +291,22 @@
text {*
- The reason is that one cannot pass the arguments @{term P} and @{term Q} into
- an antiquotation. For example this following does not work.
+ The reason is that one cannot pass the arguments @{term P}, @{term Q} and
+ @{term "tau"} into an antiquotation. For example this following does not work.
*}
ML {*
- fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
+ fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
*}
text {*
- To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions.
-
- One tricky point in constructing terms by hand is to obtain the fully qualified
- name for constants. For example the names for @{text "zero"} or @{text "+"} are
- more complex than one first expects, namely
+ To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
+ to both functions.
+
+ One tricky point in constructing terms by hand is to obtain the
+ fully qualified name for constants. For example the names for @{text "zero"} or
+ @{text "+"} are more complex than one first expects, namely
\begin{center}
@{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}.
@@ -295,12 +317,11 @@
which theory they are defined. Guessing such internal names can sometimes be quite hard.
Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the
expansion automatically, for example:
-
*}
+
+text {*
-ML {* @{const_name HOL.zero}; @{const_name plus} *}
-
-text {*
+ (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
\begin{readmore}
There are many functions in @{ML_file "Pure/logic.ML"} and