theory FirstSteps+ −
imports Base+ −
begin+ −
+ −
chapter {* First Steps *}+ −
+ −
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 given in+ −
this chapter, we assume you are working inside the theory starting with+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}l}+ −
\isacommand{theory} FirstSteps\\+ −
\isacommand{imports} Main\\+ −
\isacommand{begin}\\+ −
\ldots+ −
\end{tabular}+ −
\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:+ −
+ −
\begin{isabelle}+ −
\begin{graybox}+ −
\isacommand{ML}~@{text "\<verbopen>"}\isanewline+ −
\hspace{5mm}@{ML "3 + 4"}\isanewline+ −
@{text "\<verbclose>"}\isanewline+ −
@{text "> 7"}\smallskip+ −
\end{graybox}+ −
\end{isabelle}+ −
+ −
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>"} scaffolding whenever we+ −
show code. The lines prefixed with @{text [quotes] ">"} are not part of the+ −
code, rather they indicate what the response is when the code is evaluated.+ −
+ −
Once a portion of code is relatively stable, you usually want to export it+ −
to a separate ML-file. Such files can then be included in a theory by using+ −
the \isacommand{uses}-command in the header of the theory, like:+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {}l}+ −
\isacommand{theory} FirstSteps\\+ −
\isacommand{imports} Main\\+ −
\isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\+ −
\isacommand{begin}\\+ −
\ldots+ −
\end{tabular}+ −
\end{center}+ −
+ −
*}+ −
+ −
section {* Debugging and Printing *}+ −
+ −
text {*+ −
+ −
During development you might find it necessary to inspect some data+ −
in your code. This can be done in a ``quick-and-dirty'' fashion using + −
the function @{ML "warning"}. For example + −
+ −
@{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}+ −
+ −
will print out @{text [quotes] "any string"} inside the response buffer+ −
of Isabelle. This function expects a string as argument. If you develop under PolyML,+ −
then there is a convenient, though again ``quick-and-dirty'', method for+ −
converting values into strings, namely the function @{ML makestring}:+ −
+ −
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} + −
+ −
However @{ML makestring} only works if the type of what is converted is monomorphic + −
and not a function.+ −
+ −
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} is more appropriate. This function writes all output into+ −
a separate tracing buffer. For example:+ −
+ −
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}+ −
+ −
It is also possible to redirect the ``channel'' where the string @{text "foo"} is + −
printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive + −
amounts of trace output. This redirection can be achieved with the code:+ −
*}+ −
+ −
ML{*val strip_specials =+ −
let+ −
fun strip ("\^A" :: _ :: cs) = strip cs+ −
| strip (c :: cs) = c :: strip cs+ −
| strip [] = [];+ −
in implode o strip o explode end;+ −
+ −
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\")"} + −
will cause that all tracing information is printed into the file @{text "foo.bar"}.+ −
+ −
You can print out error messages with the function @{ML error}; for example:+ −
+ −
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" + −
"Exception- ERROR \"foo\" raised+ −
At command \"ML\"."}+ −
+ −
Section~\ref{sec:printing} will give more information about printing + −
the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} + −
and @{ML_type thm}.+ −
*}+ −
+ −
+ −
section {* Antiquotations *}+ −
+ −
text {*+ −
The main advantage of embedding all code in a theory is that the code can+ −
contain references to entities defined on the logical level of Isabelle. By+ −
this we mean definitions, theorems, terms and so on. This kind of reference is+ −
realised with antiquotations. For example, one can print out the name of the current+ −
theory by typing+ −
+ −
+ −
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}+ −
+ −
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 using+ −
the function @{ML "Context.theory_name"}. + −
+ −
Note, however, that antiquotations are statically linked, that is their value is+ −
determined at ``compile-time'', not ``run-time''. For example the function+ −
*}+ −
+ −
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}+ −
+ −
text {*+ −
+ −
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 + −
\emph{not} replaced with code that will look up the current theory in + −
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 proved theorems:+ −
+ −
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}+ −
+ −
and current simpsets:+ −
+ −
@{ML_response_fake [display,gray] + −
"let+ −
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 stored in the+ −
simpset. You can 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+ −
stored in a \emph{discrimination net} (a data structure for fast+ −
indexing). From this net you can extract the entries using the function @{ML+ −
Net.entries}.+ −
+ −
+ −
\begin{readmore}+ −
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}+ −
and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented+ −
in @{ML_file "Pure/net.ML"}.+ −
\end{readmore}+ −
+ −
While antiquotations have many applications, they were originally introduced in order + −
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 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, you will learn more about these antiquotations:+ −
they can simplify Isabelle programming since one can directly access all+ −
kinds of logical elements from th ML-level.+ −
+ −
*}+ −
+ −
section {* Terms and Types *}+ −
+ −
text {*+ −
One way to construct terms of Isabelle is by using the antiquotation + −
\mbox{@{text "@{term \<dots>}"}}. For example:+ −
+ −
@{ML_response [display,gray] + −
"@{term \"(a::nat) + b = c\"}" + −
"Const (\"op =\", \<dots>) $ + −
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}+ −
+ −
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal+ −
representation of this term. This internal representation corresponds to the + −
datatype @{ML_type "term"}.+ −
+ −
The internal representation of terms uses the usual de Bruijn index mechanism where bound + −
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to+ −
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that+ −
binds the corresponding variable. However, in Isabelle the names of bound variables are + −
kept at abstractions for printing purposes, and so should be treated only as comments. + −
Application in Isabelle is realised with the term-constructor @{ML $}.+ −
+ −
\begin{readmore}+ −
Terms are described in detail in \isccite{sec:terms}. Their+ −
definition and many useful operations are implemented 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. + −
+ −
\begin{exercise}+ −
Look at the internal term representation of the following terms, and+ −
find out why they are represented like this:+ −
+ −
\begin{itemize}+ −
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"} + −
\item @{term "\<lambda>(x,y). P y x"} + −
\item @{term "{ [x::int] | x. x \<le> -2 }"} + −
\end{itemize}+ −
+ −
Hint: The third term is already quite big, and the pretty printer+ −
may omit parts of it by default. If you want to see all of it, you+ −
can use the following ML-function to set the printing depth to a higher + −
value:+ −
+ −
@{ML [display,gray] "print_depth 50"}+ −
\end{exercise}+ −
+ −
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, + −
inserting the invisible @{text "Trueprop"}-coercions whenever necessary. + −
Consider for example the pairs+ −
+ −
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),+ −
Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}+ −
+ −
where a coercion is inserted in the second component and + −
+ −
@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" + −
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}+ −
+ −
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:+ −
+ −
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}+ −
+ −
\begin{readmore}+ −
Types are described in detail in \isccite{sec:types}. Their+ −
definition and many useful operations are implemented + −
in @{ML_file "Pure/type.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Constructing Terms and Types Manually *} + −
+ −
text {*+ −
While antiquotations are very convenient for constructing terms, they can+ −
only construct fixed terms (remember they are ``linked'' at compile-time).+ −
However, you often need 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:+ −
+ −
*}+ −
+ −
ML{*fun make_imp P Q tau =+ −
let+ −
val x = Free ("x",tau)+ −
in + −
Logic.all x (Logic.mk_implies (P $ x, Q $ x))+ −
end *}+ −
+ −
text {*+ −
The reason is that you cannot pass the arguments @{term P}, @{term Q} and + −
@{term "tau"} into an antiquotation. For example the following does \emph{not} work.+ −
*}+ −
+ −
ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}+ −
+ −
text {*+ −
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} + −
to both functions. With @{ML make_imp} we obtain the intended term involving + −
the given arguments+ −
+ −
@{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" + −
"Const \<dots> $ + −
Abs (\"x\", Type (\"nat\",[]),+ −
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ + −
(Free (\"T\",\<dots>) $ \<dots>))"}+ −
+ −
whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} + −
and @{text "Q"} from the antiquotation.+ −
+ −
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" + −
"Const \<dots> $ + −
Abs (\"x\", \<dots>,+ −
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ + −
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}+ −
+ −
Although types of terms can often be inferred, there are many+ −
situations where you need to construct types manually, especially + −
when defining constants. For example the function returning a function + −
type is as follows:+ −
+ −
*} + −
+ −
ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}+ −
+ −
text {* This can be equally written as: *}+ −
+ −
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}+ −
+ −
text {*+ −
\begin{readmore}+ −
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and+ −
@{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms + −
and types easier.\end{readmore}+ −
+ −
Have a look at these files and try to solve the following two exercises:+ −
*}+ −
+ −
text {*+ −
+ −
\begin{exercise}\label{fun:revsum}+ −
Write a function @{text "rev_sum : term -> term"} that takes a+ −
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)+ −
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume+ −
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} + −
associates to the left. Try your function on some examples. + −
\end{exercise}+ −
+ −
\begin{exercise}\label{fun:makesum}+ −
Write a function which takes two terms representing natural numbers+ −
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the+ −
number representing their sum.+ −
\end{exercise}+ −
+ −
A handy function for manipulating terms is @{ML map_types}: it takes a + −
function and applies it to every type in the term. You can, for example,+ −
change every @{typ nat} in a term into an @{typ int} using the function:+ −
*}+ −
+ −
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 {*+ −
An example as follows:+ −
+ −
@{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\")"}+ −
+ −
+ −
There are a few subtle issues with constants. They usually crop up when+ −
pattern matching terms or constructing terms. While it is perfectly ok+ −
to write the function @{text is_true} as follows+ −
*}+ −
+ −
ML{*fun is_true @{term True} = true+ −
| is_true _ = false*}+ −
+ −
text {*+ −
this does not work for picking out @{text "\<forall>"}-quantified terms. Because+ −
the function + −
*}+ −
+ −
ML{*fun is_all (@{term All} $ _) = true+ −
| is_all _ = false*}+ −
+ −
text {* + −
will not correctly match the formula @{prop "\<forall>x::nat. P x"}: + −
+ −
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}+ −
+ −
The problem is that the @{text "@term"}-antiquotation in the pattern + −
fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for + −
an arbitrary, but fixed type @{typ "'a"}. A properly working alternative + −
for this function is+ −
*}+ −
+ −
ML{*fun is_all (Const ("All", _) $ _) = true+ −
| is_all _ = false*}+ −
+ −
text {* + −
because now+ −
+ −
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}+ −
+ −
matches correctly (the wildcard in the pattern matches any type).+ −
+ −
However there is still a problem: consider the similar function that+ −
attempts to pick out a @{text "Nil"}-term:+ −
*}+ −
+ −
ML{*fun is_nil (Const ("Nil", _)) = true+ −
| is_nil _ = false *}+ −
+ −
text {* + −
Unfortunately, also this function does \emph{not} work as expected, since+ −
+ −
@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}+ −
+ −
The problem is that on the ML-level the name of a constant is more+ −
subtle as you might expect. The function @{ML is_all} worked correctly,+ −
because @{term "All"} is such a fundamental constant, which can be referenced+ −
by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at+ −
+ −
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}+ −
+ −
the name of the constant depends on the theory in which the term constructor+ −
@{text "Nil"} is defined (@{text "List"}) and also in which datatype + −
(@{text "list"}). Even worse, some constants have a name involving + −
type-classes. Consider for example the constants for @{term "zero"} + −
and @{text "(op *)"}:+ −
+ −
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" + −
"(Const (\"HOL.zero_class.zero\", \<dots>), + −
Const (\"HOL.times_class.times\", \<dots>))"}+ −
+ −
While you could use the complete name, for example + −
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or+ −
matching against @{text "Nil"}, this would make the code rather brittle. + −
The reason is that the theory and the name of the datatype can easily change. + −
To make the code more robust, it is better to use the antiquotation + −
@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the + −
variable parts of the constant's name. Therefore a functions for + −
matching against constants that have a polymorphic type should + −
be written as follows.+ −
*}+ −
+ −
ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true+ −
| is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true+ −
| is_nil_or_all _ = false *}+ −
+ −
text {*+ −
Note that you occasional have to calculate what the ``base'' name of a given+ −
constant is. For this you can use the function @{ML Sign.extern_const} or+ −
@{ML Sign.base_name}. For example:+ −
+ −
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}+ −
+ −
The difference between both functions is that @{ML extern_const in Sign} returns+ −
the smallest name which is still unique, while @{ML base_name in Sign} always+ −
strips off all qualifiers.+ −
+ −
(FIXME authentic syntax on the ML-level)+ −
+ −
\begin{readmore}+ −
FIXME+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Type-Checking *}+ −
+ −
text {* + −
+ −
You can freely construct and manipulate @{ML_type "term"}s, since they are just+ −
arbitrary unchecked trees. However, you eventually want to see if a+ −
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+ −
"cterm"}s are abstract objects that are guaranteed to be+ −
type-correct, and they can only be constructed via ``official+ −
interfaces''.+ −
+ −
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 you can write:+ −
+ −
@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}+ −
+ −
This can also be written with an antiquotation:+ −
+ −
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}+ −
+ −
Attempting to obtain the certified term for+ −
+ −
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}+ −
+ −
yields an error (since the term is not typable). A slightly more elaborate+ −
example that type-checks is:+ −
+ −
@{ML_response_fake [display,gray] + −
"let+ −
val natT = @{typ \"nat\"}+ −
val zero = @{term \"0::nat\"}+ −
in+ −
cterm_of @{theory} + −
(Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)+ −
end" "0 + 0"}+ −
+ −
\begin{exercise}+ −
Check that the function defined in Exercise~\ref{fun:revsum} returns a+ −
result that type-checks.+ −
\end{exercise}+ −
+ −
Remember that in Isabelle a term contains enough typing information+ −
(constants, free variables and abstractions all have typing + −
information) so that it is always clear what the type of a term is. + −
Given a well-typed term, the function @{ML type_of} returns the + −
type of a term. Consider for example:+ −
+ −
@{ML_response [display,gray] + −
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}+ −
+ −
To calculate the type, this function traverses the whole term and will+ −
detect any inconsistency. For examle changing the type of the variable + −
from @{typ "nat"} to @{typ "int"} will result in the error message: + −
+ −
@{ML_response_fake [display,gray] + −
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" + −
"*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}+ −
+ −
Since the complete traversal might sometimes be too costly and+ −
not necessary, there is also the function @{ML fastype_of} which + −
returns a type.+ −
+ −
@{ML_response [display,gray] + −
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}+ −
+ −
However, efficiency is gained on the expense of skiping some tests. You + −
can see this in the following example+ −
+ −
@{ML_response [display,gray] + −
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}+ −
+ −
where no error is raised.+ −
+ −
Sometimes it is a bit inconvenient to construct a term with + −
complete typing annotations, especially in cases where the typing + −
information is redundant. A short-cut is to use the ``place-holder'' + −
type @{ML "dummyT"} and then let type-inference figure out the + −
complete type. An example is as follows:+ −
+ −
@{ML_response_fake [display,gray] + −
"let+ −
val term = + −
Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)+ −
in + −
Syntax.check_term @{context} term+ −
end"+ −
"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $+ −
Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}+ −
+ −
Instead of giving explicitly the type for the constant @{text "plus"} and the free + −
variable @{text "x"}, the type-inference will fill in the missing information.+ −
+ −
+ −
\begin{readmore}+ −
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,+ −
checking and pretty-printing of terms are defined.+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Theorems *}+ −
+ −
text {*+ −
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} + −
that can only be build by going through interfaces. As a consequence, every proof + −
in Isabelle is correct by construction. This follows the tradition of the LCF approach+ −
\cite{GordonMilnerWadsworth79}.+ −
+ −
+ −
To see theorems in ``action'', let us give a proof on the ML-level for the following + −
statement:+ −
*}+ −
+ −
lemma + −
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" + −
and assm\<^isub>2: "P t"+ −
shows "Q t" (*<*)oops(*>*) + −
+ −
text {*+ −
The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse+ −
application. See Section~\ref{sec:combinators}.}+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val thy = @{theory}+ −
+ −
val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}+ −
val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}+ −
+ −
val Pt_implies_Qt = + −
assume assm1+ −
|> forall_elim (cterm_of thy @{term \"t::nat\"});+ −
+ −
val Qt = implies_elim Pt_implies_Qt (assume assm2);+ −
in+ −
Qt + −
|> implies_intr assm2+ −
|> implies_intr assm1+ −
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}+ −
+ −
This code-snippet constructs the following proof:+ −
+ −
\[+ −
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}+ −
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}+ −
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}+ −
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}+ −
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}+ −
&+ −
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}+ −
}+ −
}+ −
}+ −
\]+ −
+ −
However, while we obtained a theorem as result, this theorem is not+ −
yet stored in Isabelle's theorem database. So it cannot be referenced later+ −
on. How to store theorems will be explained in the next section.+ −
+ −
\begin{readmore}+ −
For the functions @{text "assume"}, @{text "forall_elim"} etc + −
see \isccite{sec:thms}. The basic functions for theorems are defined in+ −
@{ML_file "Pure/thm.ML"}. + −
\end{readmore}+ −
+ −
(FIXME: how to add case-names to goal states)+ −
*}+ −
+ −
section {* Printing Terms and Theorems\label{sec:printing} *}+ −
+ −
text {* + −
During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} + −
or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, + −
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform + −
a term into a string is to use the function @{ML Syntax.string_of_term}.+ −
+ −
@{ML_response_fake [display,gray]+ −
"Syntax.string_of_term @{context} @{term \"1::nat\"}"+ −
"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}+ −
+ −
This produces a string with some printing directions encoded in it. The string+ −
can be properly printed by using the function @{ML warning}.+ −
+ −
@{ML_response_fake [display,gray]+ −
"warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"+ −
"\"1\""}+ −
+ −
A @{ML_type cterm} can be transformed into a string by the following function.+ −
*}+ −
+ −
ML{*fun str_of_cterm ctxt t = + −
Syntax.string_of_term ctxt (term_of t)*}+ −
+ −
text {*+ −
If there are more than one @{ML_type cterm}s to be printed, you can use the + −
function @{ML commas} to separate them.+ −
*} + −
+ −
ML{*fun str_of_cterms ctxt ts = + −
commas (map (str_of_cterm ctxt) ts)*}+ −
+ −
text {*+ −
The easiest way to get the string of a theorem is to transform it+ −
into a @{ML_type cterm} using the function @{ML crep_thm}.+ −
*}+ −
+ −
ML{*fun str_of_thm ctxt thm =+ −
let+ −
val {prop, ...} = crep_thm thm+ −
in + −
str_of_cterm ctxt prop+ −
end*}+ −
+ −
text {* + −
Again the function @{ML commas} helps with printing more than one theorem. + −
*}+ −
+ −
ML{*fun str_of_thms ctxt thms = + −
commas (map (str_of_thm ctxt) thms)*}+ −
+ −
section {* Theorem Attributes *}+ −
+ −
section {* Theories and Local Theories *}+ −
+ −
section {* Storing Theorems *}+ −
+ −
text {* @{ML PureThy.add_thms_dynamic} *}+ −
+ −
+ −
section {* Combinators\label{sec:combinators} *}+ −
+ −
text {*+ −
For beginners, perhaps the most puzzling parts in the existing code of Isabelle are+ −
the combinators. At first they seem to greatly obstruct the+ −
comprehension of the code, but after getting familiar with them, they+ −
actually ease the understanding and also the programming.+ −
+ −
\begin{readmore}+ −
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}+ −
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} + −
contains further information about combinators.+ −
\end{readmore}+ −
+ −
The simplest combinator is @{ML I}, which is just the identity function defined as+ −
*}+ −
+ −
ML{*fun I x = x*}+ −
+ −
text {* Another simple combinator is @{ML K}, defined as *}+ −
+ −
ML{*fun K x = fn _ => x*}+ −
+ −
text {*+ −
@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this + −
function ignores its argument. As a result, @{ML K} defines a constant function + −
always returning @{text x}.+ −
+ −
The next combinator is reverse application, @{ML "|>"}, defined as: + −
*}+ −
+ −
ML{*fun x |> f = f x*}+ −
+ −
text {* While just syntactic sugar for the usual function application,+ −
the purpose of this combinator is to implement functions in a + −
``waterfall fashion''. Consider for example the function *}+ −
+ −
ML %linenosgray{*fun inc_by_five x =+ −
x |> (fn x => x + 1)+ −
|> (fn x => (x, x))+ −
|> fst+ −
|> (fn x => x + 4)*}+ −
+ −
text {*+ −
which increments its argument @{text x} by 5. It does this by first incrementing + −
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking + −
the first component of the pair (Line 4) and finally incrementing the first + −
component by 4 (Line 5). This kind of cascading manipulations of values is quite+ −
common when dealing with theories (for example by adding a definition, followed by+ −
lemmas and so on). The reverse application allows you to read what happens in + −
a top-down manner. This kind of coding should also be familiar, + −
if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using + −
the reverse application is much clearer than writing+ −
*}+ −
+ −
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}+ −
+ −
text {* or *}+ −
+ −
ML{*fun inc_by_five x = + −
((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}+ −
+ −
text {* and typographically more economical than *}+ −
+ −
ML{*fun inc_by_five x =+ −
let val y1 = x + 1+ −
val y2 = (y1, y1)+ −
val y3 = fst y2+ −
val y4 = y3 + 4+ −
in y4 end*}+ −
+ −
text {* + −
Another reason why the let-bindings in the code above are better to be+ −
avoided: it is more than easy to get the intermediate values wrong, not to + −
mention the nightmares the maintenance of this code causes!+ −
+ −
+ −
(FIXME: give a real world example involving theories)+ −
+ −
Similarly, the combinator @{ML "#>"} is the reverse function + −
composition. It can be used to define the following function+ −
*}+ −
+ −
ML{*val inc_by_six = + −
(fn x => x + 1)+ −
#> (fn x => x + 2)+ −
#> (fn x => x + 3)*}+ −
+ −
text {* + −
which is the function composed of first the increment-by-one function and then+ −
increment-by-two, followed by increment-by-three. Again, the reverse function + −
composition allows you to read the code top-down.+ −
+ −
The remaining combinators described in this section add convenience for the+ −
``waterfall method'' of writing functions. The combinator @{ML tap} allows+ −
you to get hold of an intermediate result (to do some side-calculations for+ −
instance). The function+ −
+ −
*}+ −
+ −
ML %linenosgray{*fun inc_by_three x =+ −
x |> (fn x => x + 1)+ −
|> tap (fn x => tracing (makestring x))+ −
|> (fn x => x + 2)*}+ −
+ −
text {* + −
increments the argument first by @{text "1"} and then by @{text "2"}. In the+ −
middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''+ −
intermediate result inside the tracing buffer. The function @{ML tap} can+ −
only be used for side-calculations, because any value that is computed+ −
cannot be merged back into the ``main waterfall''. To do this, you can use+ −
the next combinator.+ −
+ −
The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value+ −
and returns the result together with the value (as a pair). For example+ −
the function + −
*}+ −
+ −
ML{*fun inc_as_pair x =+ −
x |> `(fn x => x + 1)+ −
|> (fn (x, y) => (x, y + 1))*}+ −
+ −
text {*+ −
takes @{text x} as argument, and then increments @{text x}, but also keeps+ −
@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"+ −
for x}. After that, the function increments the right-hand component of the+ −
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.+ −
+ −
The combinators @{ML "|>>"} and @{ML "||>"} are defined for + −
functions manipulating pairs. The first applies the function to+ −
the first component of the pair, defined as+ −
*}+ −
+ −
ML{*fun (x, y) |>> f = (f x, y)*}+ −
+ −
text {*+ −
and the second combinator to the second component, defined as+ −
*}+ −
+ −
ML{*fun (x, y) ||> f = (x, f y)*}+ −
+ −
text {*+ −
With the combinator @{ML "|->"} you can re-combine the elements from a pair.+ −
This combinator is defined as+ −
*}+ −
+ −
ML{*fun (x, y) |-> f = f x y*}+ −
+ −
text {* and can be used to write the following roundabout version + −
of the @{text double} function: + −
*}+ −
+ −
ML{*fun double x =+ −
x |> (fn x => (x, x))+ −
|-> (fn x => fn y => x + y)*}+ −
+ −
text {*+ −
Recall that @{ML "|>"} is the reverse function applications. Recall also that the related + −
reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},+ −
@{ML "|>>"} and @{ML "||>"} described above have related combinators for function+ −
composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, + −
for example, the function @{text double} can also be written as:+ −
*}+ −
+ −
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+ −
(*>*)+ −
+ −
section {* Misc *}+ −
+ −
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}+ −
+ −
end+ −