--- 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 "\<verbopen> \<dots> \<verbclose>"}
- 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\", \<dots>]"}
- 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 \<dots>}"}}. For example
+ \mbox{@{text "@{term \<dots>}"}}. 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 \<Rightarrow> 0 | Suc y \<Rightarrow> 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 \<dots>}"}. For example
+ Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> 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 "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term
- "\<tau>"} as arguments can only be written as
+ "\<tau>"} 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 \<Rightarrow> int \<Rightarrow> 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