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}+ −
+ −
We also generally assume you are working with HOL. The given examples might+ −
need to be adapted slightly if you work in a different logic.+ −
*}+ −
+ −
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 in the Introduction, 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\label{sec: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\"."}+ −
+ −
Most often you want to inspect data 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 additional information 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 {*+ −
In this example the function @{ML term_of} extracts the @{ML_type term} from+ −
a @{ML_type cterm}. 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}. Theorems+ −
also include schematic variables, such as @{text "?P"}, @{text "?Q"}+ −
and so on. In order to improve the readability of theorems we convert+ −
these schematic variables into free variables using the + −
function @{ML Variable.import_thms}.+ −
*}+ −
+ −
ML{*fun no_vars ctxt thm =+ −
let + −
val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt+ −
in+ −
thm'+ −
end+ −
+ −
fun str_of_thm ctxt thm =+ −
str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}+ −
+ −
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 {* 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.+ −
+ −
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 have been exposed to 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!+ −
+ −
In the context of Isabelle, a ``real world'' example for a function written in + −
the waterfall fashion might be the following code:+ −
*}+ −
+ −
ML %linenosgray{*fun apply_fresh_args pred ctxt =+ −
pred |> fastype_of+ −
|> binder_types + −
|> map (pair "z")+ −
|> Variable.variant_frees ctxt [pred]+ −
|> map Free + −
|> (curry list_comb) pred *}+ −
+ −
text {*+ −
This code extracts the argument types of the given+ −
predicate and then generate for each type a distinct variable; finally it+ −
applies the generated variables to the predicate. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} + −
|> Syntax.string_of_term @{context}+ −
|> warning"+ −
"P z za zb"}+ −
+ −
You can read this off this behaviour from how @{ML apply_fresh_args} is+ −
coded: in Line 2, the function @{ML fastype_of} calculates the type of the+ −
predicate; in Line 3, @{ML binder_types} produces the list of argument+ −
types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each + −
type with the string @{text "z"}; the+ −
function @{ML variant_frees in Variable} generates for each @{text "z"} a+ −
unique name avoiding @{text pred}; the list of name-type pairs is turned+ −
into a list of variable terms in Line 6, which in the last line are applied+ −
by the function @{ML list_comb} to the predicate. We have to use the+ −
function @{ML curry}, because @{ML list_comb} expects the predicate and the+ −
argument list as a pair.+ −
+ −
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)+ −
+ −
\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}+ −
+ −
*}+ −
+ −
+ −
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: + −
@{text "@{thm \<dots>}"} for a single theorem+ −
+ −
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}+ −
+ −
and @{text "@{thms \<dots>}"} for more than one+ −
+ −
@{ML_response_fake [display,gray] "@{thms conj_ac}" + −
"(?P \<and> ?Q) = (?Q \<and> ?P)+ −
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)+ −
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} + −
+ −
You can also refer to the current simpset. To illustrate this we implement the+ −
function that extracts the theorem names stored in a simpset.+ −
*}+ −
+ −
ML{*fun get_thm_names_from_ss simpset =+ −
let+ −
val {simps,...} = MetaSimplifier.dest_ss simpset+ −
in+ −
map #1 simps+ −
end*}+ −
+ −
text {*+ −
The function @{ML dest_ss in MetaSimplifier} returns a record containing all+ −
information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored+ −
in the current simpset. This simpset can be referred to using the antiquotation+ −
@{text "@{simpset}"}.+ −
+ −
@{ML_response_fake [display,gray] + −
"get_thm_names_from_ss @{simpset}" + −
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}+ −
+ −
Again, this way or referencing simpsets makes you independent from additions+ −
of lemmas to the simpset by the user that potentially cause loops.+ −
+ −
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 broke 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 chapter 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.+ −
*}+ −
+ −
text {*+ −
(FIXME: say something about @{text "@{binding \<dots>}"}+ −
*}+ −
+ −
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\label{sec:terms_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>)))"}+ −
+ −
(FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda})+ −
+ −
+ −
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 with the combinator @{ML "-->"} as: *}+ −
+ −
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}+ −
+ −
text {*+ −
A handy function for manipulating terms is @{ML map_types}: it takes a + −
function and applies it to every type in a 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\")"}+ −
+ −
\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}+ −
+ −
There are a few subtle issues with constants. They usually crop up when+ −
pattern matching terms or types, or when constructing them. 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 first wildcard in the pattern matches any type and the+ −
second any term).+ −
+ −
However there is still a problem: consider the similar function that+ −
attempts to pick out @{text "Nil"}-terms:+ −
*}+ −
+ −
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 than 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 @{text "Nil"} depends on the theory in which the+ −
term constructor 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+ −
\mbox{@{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 {*+ −
Occasional you 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 Long_Name.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 that is still unique, whereas @{ML base_name in Long_Name} always+ −
strips off all qualifiers.+ −
+ −
\begin{readmore}+ −
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};+ −
functions about signatures in @{ML_file "Pure/sign.ML"}.+ −
+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Type-Checking *}+ −
+ −
text {* + −
+ −
You can freely construct and manipulate @{ML_type "term"}s and @{ML_type+ −
typ}es, 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::nat) + 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"}+ −
+ −
In Isabelle not just types need to be certified, but also types. For example, + −
you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on + −
the ML-level as follows:+ −
+ −
@{ML_response_fake [display,gray]+ −
"ctyp_of @{theory} (@{typ nat} --> @{typ bool})"+ −
"nat \<Rightarrow> bool"}+ −
+ −
\begin{readmore}+ −
For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see + −
the file @{ML_file "Pure/thm.ML"}.+ −
\end{readmore}+ −
+ −
\begin{exercise}+ −
Check that the function defined in Exercise~\ref{fun:revsum} returns a+ −
result that type-checks.+ −
\end{exercise}+ −
+ −
Remember Isabelle foolows the Church-style typing for terms, i.e.~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 typing inconsistency. For examle changing the type of the variable + −
@{term "x"} 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 the function @{ML fastype_of}, which + −
also returns the type of a term.+ −
+ −
@{ML_response [display,gray] + −
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}+ −
+ −
However, efficiency is gained on the expense of skipping 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 detected.+ −
+ −
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 c = Const (@{const_name \"plus\"}, dummyT) + −
val o = @{term \"1::nat\"} + −
val v = Free (\"x\", dummyT)+ −
in + −
Syntax.check_term @{context} (c $ o $ v)+ −
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 filles 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. Fuctions related to the+ −
type inference are implemented in @{ML_file "Pure/type.ML"} and + −
@{ML_file "Pure/type_infer.ML"}. + −
\end{readmore}+ −
+ −
(FIXME: say something about sorts)+ −
*}+ −
+ −
+ −
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 assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}+ −
val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}+ −
+ −
val Pt_implies_Qt = + −
assume assm1+ −
|> forall_elim @{cterm \"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 Section~\ref{sec:storing}.+ −
+ −
\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 - maybe in the next section)+ −
*}+ −
+ −
section {* Theorem Attributes *}+ −
+ −
text {*+ −
Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text+ −
"[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags+ −
annotated to theorems, but functions that do further processing once a+ −
theorem is proven. In particular, it is not possible to find out+ −
what are all theorems that have a given attribute in common, unless of course+ −
the function behind the attribute stores the theorems in a retrivable + −
datastructure. + −
+ −
If you want to print out all currently known attributes a theorem + −
can have, you can use the function:+ −
+ −
@{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" + −
"COMP: direct composition with rules (no lifting)+ −
HOL.dest: declaration of Classical destruction rule+ −
HOL.elim: declaration of Classical elimination rule + −
\<dots>"}+ −
+ −
To explain how to write your own attribute, let us start with an extremely simple + −
version of the attribute @{text "[symmetric]"}. The purpose of this attribute is+ −
to produce the ``symmetric'' version of an equation. The main function behind + −
this attribute is+ −
*}+ −
+ −
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}+ −
+ −
text {* + −
where the function @{ML "Thm.rule_attribute"} expects a function taking a + −
context (which we ignore in the code above) and a theorem (@{text thm}), and + −
returns another theorem (namely @{text thm} resolved with the lemma + −
@{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns + −
an attribute.+ −
+ −
Before we can use the attribute, we need to set it up. This can be done+ −
using the function @{ML Attrib.setup} as follows.+ −
*}+ −
+ −
setup %gray {* Attrib.setup @{binding "my_sym"} + −
(Scan.succeed my_symmetric) "applying the sym rule"*}+ −
+ −
text {*+ −
The attribute does not expect any further arguments (unlike @{text "[OF+ −
\<dots>]"}, for example, which can take a list of theorems as argument). Therefore+ −
we use the parser @{ML Scan.succeed}. Later on we will also consider+ −
attributes taking further arguments. An example for the attribute @{text+ −
"[my_sym]"} is the proof+ −
*} + −
+ −
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp+ −
+ −
text {*+ −
which stores the theorem @{thm test} under the name @{thm [source] test}. We + −
can also use the attribute when referring to this theorem.+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test[my_sym]"}\\+ −
@{text "> "}~@{thm test[my_sym]}+ −
\end{isabelle}+ −
+ −
The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.+ −
Another usage of attributes is to add and delete theorems from stored data.+ −
For example the attribute @{text "[simp]"} adds or deletes a theorem from the+ −
current simpset. For these applications, you can use @{ML Thm.declaration_attribute}. + −
To illustrate this function, let us introduce a reference containing a list+ −
of theorems.+ −
*}+ −
+ −
ML{*val my_thms = ref ([]:thm list)*}+ −
+ −
text {* + −
A word of warning: such references must not be used in any code that+ −
is meant to be more than just for testing purposes! Here it is only used + −
to illustrate matters. We will show later how to store data properly without + −
using references. The function @{ML Thm.declaration_attribute} expects us to + −
provide two functions that add and delete theorems from this list. + −
For this we use the two functions:+ −
*}+ −
+ −
ML{*fun my_thms_add thm ctxt =+ −
(my_thms := Thm.add_thm thm (!my_thms); ctxt)+ −
+ −
fun my_thms_del thm ctxt =+ −
(my_thms := Thm.del_thm thm (!my_thms); ctxt)*}+ −
+ −
text {*+ −
These functions take a theorem and a context and, for what we are explaining+ −
here it is sufficient that they just return the context unchanged. They change+ −
however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}+ −
adds a theorem if it is not already included in the list, and @{ML+ −
Thm.del_thm} deletes one. Both functions use the predicate @{ML+ −
Thm.eq_thm_prop} which compares theorems according to their proved+ −
propositions (modulo alpha-equivalence).+ −
+ −
+ −
You can turn both functions into attributes using+ −
*}+ −
+ −
ML{*val my_add = Thm.declaration_attribute my_thms_add+ −
val my_del = Thm.declaration_attribute my_thms_del *}+ −
+ −
text {* + −
and set up the attributes as follows+ −
*}+ −
+ −
setup %gray {* Attrib.setup @{binding "my_thms"}+ −
(Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}+ −
+ −
text {*+ −
Now if you prove the lemma attaching the attribute @{text "[my_thms]"}+ −
*}+ −
+ −
lemma trueI_2[my_thms]: "True" by simp+ −
+ −
text {*+ −
then you can see the lemma is added to the initially empty list.+ −
+ −
@{ML_response_fake [display,gray]+ −
"!my_thms" "[\"True\"]"}+ −
+ −
You can also add theorems using the command \isacommand{declare}.+ −
*}+ −
+ −
declare test[my_thms] trueI_2[my_thms add]+ −
+ −
text {*+ −
The @{text "add"} is the default operation and does not need+ −
to be given. This declaration will cause the theorem list to be + −
updated as follows.+ −
+ −
@{ML_response_fake [display,gray]+ −
"!my_thms"+ −
"[\"True\", \"Suc (Suc 0) = 2\"]"}+ −
+ −
The theorem @{thm [source] trueI_2} only appears once, since the + −
function @{ML Thm.add_thm} tests for duplicates, before extending+ −
the list. Deletion from the list works as follows:+ −
*}+ −
+ −
declare test[my_thms del]+ −
+ −
text {* After this, the theorem list is again: + −
+ −
@{ML_response_fake [display,gray]+ −
"!my_thms"+ −
"[\"True\"]"}+ −
+ −
We used in this example two functions declared as @{ML Thm.declaration_attribute}, + −
but there can be any number of them. We just have to change the parser for reading+ −
the arguments accordingly. + −
+ −
However, as said at the beginning of this example, using references for storing theorems is+ −
\emph{not} the received way of doing such things. The received way is to + −
start a ``data slot'' in a context by using the functor @{text GenericDataFun}:+ −
*}+ −
+ −
ML {*structure Data = GenericDataFun+ −
(type T = thm list+ −
val empty = []+ −
val extend = I+ −
fun merge _ = Thm.merge_thms) *}+ −
+ −
text {*+ −
To use this data slot, you only have to change @{ML my_thms_add} and+ −
@{ML my_thms_del} to:+ −
*}+ −
+ −
ML{*val thm_add = Data.map o Thm.add_thm+ −
val thm_del = Data.map o Thm.del_thm*}+ −
+ −
text {*+ −
where @{ML Data.map} updates the data appropriately in the context. Since storing+ −
theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},+ −
which does most of the work for you. To obtain such a named theorem lists, you just+ −
declare + −
*}+ −
+ −
ML{*structure FooRules = NamedThmsFun + −
(val name = "foo" + −
val description = "Rules for foo"); *}+ −
+ −
text {*+ −
and set up the @{ML_struct FooRules} with the command+ −
*}+ −
+ −
setup %gray {* FooRules.setup *}+ −
+ −
text {*+ −
This code declares a data slot where the theorems are stored,+ −
an attribute @{text foo} (with the @{text add} and @{text del} options+ −
for adding and deleting theorems) and an internal ML interface to retrieve and + −
modify the theorems.+ −
+ −
Furthermore, the facts are made available on the user-level under the dynamic + −
fact name @{text foo}. For example you can declare three lemmas to be of the kind+ −
@{text foo} by:+ −
*}+ −
+ −
lemma rule1[foo]: "A" sorry+ −
lemma rule2[foo]: "B" sorry+ −
lemma rule3[foo]: "C" sorry+ −
+ −
text {* and undeclare the first one by: *}+ −
+ −
declare rule1[foo del]+ −
+ −
text {* and query the remaining ones with:+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "foo"}\\+ −
@{text "> ?C"}\\+ −
@{text "> ?B"}+ −
\end{isabelle}+ −
+ −
On the ML-level the rules marked with @{text "foo"} can be retrieved+ −
using the function @{ML FooRules.get}:+ −
+ −
@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}+ −
+ −
\begin{readmore}+ −
For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also+ −
the recipe in Section~\ref{recipe:storingdata} about storing arbitrary+ −
data.+ −
\end{readmore}+ −
+ −
(FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)+ −
+ −
+ −
\begin{readmore}+ −
FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Setups (TBD) *}+ −
+ −
text {*+ −
In the previous section we used \isacommand{setup} in order to make+ −
a theorem attribute known to Isabelle. What happens behind the scenes+ −
is that \isacommand{setup} expects a functions from @{ML_type theory}+ −
to @{ML_type theory}: the input theory is the current theory and the + −
output the theory where the theory attribute has been stored.+ −
+ −
This is a fundamental principle in Isabelle. A similar situation occurs + −
for example with declaring constants. The function that declares a + −
constant on the ML-level is @{ML Sign.add_consts_i}. Recall that ML-code + −
needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.+ −
If you write + −
*} + −
+ −
ML{*Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] @{theory} *}+ −
+ −
text {*+ −
for declaring the constant @{text "BAR"} with type @{typ nat} and + −
run the code, then you indeed obtain a theory as result. But if you + −
query the constant with \isacommand{term}+ −
+ −
\begin{isabelle}+ −
\isacommand{term}~@{text [quotes] "BAR"}\\+ −
@{text "> \"BAR\" :: \"'a\""}+ −
\end{isabelle}+ −
+ −
you do not obtain a constant of type @{typ nat}, but a free variable (printed in + −
blue) of polymorphic type. The problem is that the ML-expression above did + −
not register the declaration with the current theory. This is what the command+ −
\isacommand{setup} is for. The constant is properly declared with+ −
*}+ −
+ −
setup %gray {* Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] *}+ −
+ −
text {* + −
Now + −
+ −
\begin{isabelle}+ −
\isacommand{term}~@{text [quotes] "BAR"}\\+ −
@{text "> \"BAR\" :: \"nat\""}+ −
\end{isabelle}+ −
+ −
returns a (black) constant with the type @{typ nat}.+ −
+ −
A similar command is \isacommand{local\_setup}, which expects a function+ −
of type @{ML_type "local_theory -> local_theory"}. Later on we will also+ −
use the commands \isacommand{method\_setup} for installing methods in the+ −
current theory and \isacommand{simproc\_setup} for adding new simprocs to+ −
the current simpset.+ −
*}+ −
+ −
section {* Theories, Contexts and Local Theories (TBD) *}+ −
+ −
text {*+ −
There are theories, proof contexts and local theories (in this order, if you+ −
want to order them). + −
+ −
In contrast to an ordinary theory, which simply consists of a type+ −
signature, as well as tables for constants, axioms and theorems, a local+ −
theory also contains additional context information, such as locally fixed+ −
variables and local assumptions that may be used by the package. The type+ −
@{ML_type local_theory} is identical to the type of \emph{proof contexts}+ −
@{ML_type "Proof.context"}, although not every proof context constitutes a+ −
valid local theory.+ −
*}+ −
+ −
section {* Storing Theorems\label{sec:storing} (TBD) *}+ −
+ −
text {* @{ML PureThy.add_thms_dynamic} *}+ −
+ −
+ −
+ −
(* FIXME: some code below *)+ −
+ −
(*<*)+ −
(*+ −
setup {*+ −
Sign.add_consts_i [(Binding"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 {* Pretty-Printing (TBD) *}+ −
+ −
text {*+ −
@{ML Pretty.big_list},+ −
@{ML Pretty.brk},+ −
@{ML Pretty.block},+ −
@{ML Pretty.chunks}+ −
*}+ −
+ −
section {* Misc (TBD) *}+ −
+ −
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}+ −
+ −
end+ −