some blabla about type classes, sorts, overloading, high level view on type classes
theory Essential+ −
imports Base FirstSteps+ −
begin+ −
+ −
(*<*)+ −
setup{*+ −
open_file_with_prelude + −
"Essential_Code.thy"+ −
["theory Essential", "imports Base FirstSteps", "begin"]+ −
*}+ −
(*>*)+ −
+ −
+ −
chapter {* Isabelle Essentials *}+ −
+ −
text {*+ −
\begin{flushright}+ −
{\em One man's obfuscation is another man's abstraction.} \\[1ex]+ −
Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ + −
24~Nov.~2009+ −
\end{flushright}+ −
+ −
\medskip+ −
Isabelle is build around a few central ideas. One central idea is the+ −
LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there+ −
is a small trusted core and everything else is built on top of this trusted+ −
core. The fundamental data structures involved in this core are certified+ −
terms and certified types, as well as theorems.+ −
*}+ −
+ −
+ −
section {* Terms and Types *}+ −
+ −
text {*+ −
In Isabelle, there are certified terms and uncertified terms (respectively types). + −
Uncertified terms are often just called terms. One way to construct them is by + −
using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example+ −
+ −
@{ML_response [display,gray] + −
"@{term \"(a::nat) + b = c\"}" + −
"Const (\"op =\", \<dots>) $ + −
(Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}+ −
+ −
constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using + −
the internal representation corresponding to the datatype @{ML_type_ind "term"}, + −
which is defined as follows: + −
*} + −
+ −
ML_val %linenosgray{*datatype term =+ −
Const of string * typ + −
| Free of string * typ + −
| Var of indexname * typ + −
| Bound of int + −
| Abs of string * typ * term + −
| $ of term * term *}+ −
+ −
text {*+ −
This datatype implements Church-style lambda-terms, where types are+ −
explicitly recorded in variables, constants and abstractions. As can be+ −
seen in Line 5, terms use the usual de Bruijn index mechanism for+ −
representing bound variables. For example in+ −
+ −
@{ML_response_fake [display, gray]+ −
"@{term \"\<lambda>x y. x y\"}"+ −
"Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}+ −
+ −
the indices refer to the number of Abstractions (@{ML Abs}) that we need to+ −
skip until we hit the @{ML Abs} that binds the corresponding+ −
variable. Constructing a term with dangling de Bruijn indices is possible,+ −
but will be flagged as ill-formed when you try to typecheck or certify it+ −
(see Section~\ref{sec:typechecking}). Note that 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 $}.+ −
+ −
Isabelle makes a distinction between \emph{free} variables (term-constructor+ −
@{ML Free} and written on the user level in blue colour) and+ −
\emph{schematic} variables (term-constructor @{ML Var} and written with a+ −
leading question mark). Consider the following two examples+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val v1 = Var ((\"x\", 3), @{typ bool})+ −
val v2 = Var ((\"x1\", 3), @{typ bool})+ −
val v3 = Free (\"x\", @{typ bool})+ −
in+ −
string_of_terms @{context} [v1, v2, v3]+ −
|> tracing+ −
end"+ −
"?x3, ?x1.3, x"}+ −
+ −
When constructing terms, you are usually concerned with free variables (as+ −
mentioned earlier, you cannot construct schematic variables using the+ −
antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,+ −
however, observe the distinction. The reason is that only schematic+ −
variables can be instantiated with terms when a theorem is applied. A+ −
similar distinction between free and schematic variables holds for types+ −
(see below).+ −
+ −
\begin{readmore}+ −
Terms and types are described in detail in \isccite{sec:terms}. Their+ −
definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.+ −
For constructing terms involving HOL constants, many helper functions are defined+ −
in @{ML_file "HOL/Tools/hologic.ML"}.+ −
\end{readmore}+ −
+ −
Constructing terms via antiquotations has the advantage that only typable+ −
terms can be constructed. For example+ −
+ −
@{ML_response_fake_both [display,gray]+ −
"@{term \"x x\"}"+ −
"Type unification failed: Occurs check!"}+ −
+ −
raises a typing error, while it perfectly ok to construct the term+ −
with the raw ML-constructors:+ −
+ −
@{ML_response_fake [display,gray] + −
"let+ −
val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})+ −
in + −
tracing (string_of_term @{context} omega)+ −
end"+ −
"x x"}+ −
+ −
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 by inserting the + −
usually 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). + −
The purpose of the @{text "Trueprop"}-coercion is to embed formulae of+ −
an object logic, for example HOL, into the meta-logic of Isabelle. The coercion+ −
is needed whenever a term is constructed that will be proved as a theorem. + −
+ −
As already seen above, types can be constructed using the antiquotation + −
@{text "@{typ \<dots>}"}. For example:+ −
+ −
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}+ −
+ −
The corresponding datatype is+ −
*}+ −
+ −
ML_val{*datatype typ =+ −
Type of string * typ list + −
| TFree of string * sort + −
| TVar of indexname * sort *}+ −
+ −
text {*+ −
Like with terms, there is the distinction between free type+ −
variables (term-constructor @{ML "TFree"}) and schematic+ −
type variables (term-constructor @{ML "TVar"} and printed with+ −
a leading question mark). A type constant,+ −
like @{typ "int"} or @{typ bool}, are types with an empty list+ −
of argument types. However, it needs a bit of effort to show an+ −
example, because Isabelle always pretty prints types (unlike terms).+ −
Using just the antiquotation @{text "@{typ \"bool\"}"} we only see+ −
+ −
@{ML_response [display, gray]+ −
"@{typ \"bool\"}"+ −
"bool"}+ −
+ −
which is the pretty printed version of @{text "bool"}. However, in PolyML+ −
(version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the+ −
function below we mimic the behaviour of the usual pretty printer for+ −
datatypes (it uses pretty-printing functions which will be explained in more+ −
detail in Section~\ref{sec:pretty}).+ −
*}+ −
+ −
ML{*local+ −
fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]+ −
fun pp_list xs = Pretty.list "[" "]" xs+ −
fun pp_str s = Pretty.str s+ −
fun pp_qstr s = Pretty.quote (pp_str s)+ −
fun pp_int i = pp_str (string_of_int i)+ −
fun pp_sort S = pp_list (map pp_qstr S)+ −
fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]+ −
in+ −
fun raw_pp_typ (TVar ((a, i), S)) = + −
pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))+ −
| raw_pp_typ (TFree (a, S)) = + −
pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))+ −
| raw_pp_typ (Type (a, tys)) = + −
pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))+ −
end*}+ −
+ −
text {*+ −
We can install this pretty printer with the function + −
@{ML_ind addPrettyPrinter in PolyML} as follows.+ −
*}+ −
+ −
ML{*PolyML.addPrettyPrinter + −
(fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}+ −
+ −
text {*+ −
Now the type bool is printed out in full detail.+ −
+ −
@{ML_response [display,gray]+ −
"@{typ \"bool\"}"+ −
"Type (\"bool\", [])"}+ −
+ −
When printing out a list-type+ −
+ −
@{ML_response [display,gray]+ −
"@{typ \"'a list\"}"+ −
"Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}+ −
+ −
we can see the full name of the type is actually @{text "List.list"}, indicating+ −
that it is defined in the theory @{text "List"}. However, one has to be + −
careful with names of types, because even if+ −
@{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the + −
theories @{text "HOL"} and @{text "Nat"}, respectively, they are + −
still represented by their simple name.+ −
+ −
@{ML_response [display,gray]+ −
"@{typ \"bool \<Rightarrow> nat\"}"+ −
"Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"}+ −
+ −
We can restore the usual behaviour of Isabelle's pretty printer+ −
with the code+ −
*}+ −
+ −
ML{*PolyML.addPrettyPrinter + −
(fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}+ −
+ −
text {*+ −
After that the types for booleans, lists and so on are printed out again + −
the standard Isabelle way.+ −
+ −
@{ML_response_fake [display, gray]+ −
"@{typ \"bool\"};+ −
@{typ \"'a list\"}"+ −
"\"bool\"+ −
\"'a List.list\""}+ −
+ −
\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 manually. For example, a+ −
function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking+ −
@{term P} and @{term Q} as arguments can only be written as:+ −
+ −
*}+ −
+ −
ML{*fun make_imp P Q =+ −
let+ −
val x = Free ("x", @{typ nat})+ −
in + −
Logic.all x (Logic.mk_implies (P $ x, Q $ x))+ −
end *}+ −
+ −
text {*+ −
The reason is that you cannot pass the arguments @{term P} and @{term Q} + −
into an antiquotation.\footnote{At least not at the moment.} For example + −
the following does \emph{not} work.+ −
*}+ −
+ −
ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}+ −
+ −
text {*+ −
To see this, apply @{text "@{term S}"} and @{text "@{term T}"} + −
to both functions. With @{ML make_imp} you obtain the intended term involving + −
the given arguments+ −
+ −
@{ML_response [display,gray] "make_imp @{term S} @{term T}" + −
"Const \<dots> $ + −
Abs (\"x\", Type (\"nat\",[]),+ −
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}+ −
+ −
whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} + −
and @{text "Q"} from the antiquotation.+ −
+ −
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" + −
"Const \<dots> $ + −
Abs (\"x\", \<dots>,+ −
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ + −
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}+ −
+ −
There are a number of handy functions that are frequently used for+ −
constructing terms. One is the function @{ML_ind list_comb in Term}, which+ −
takes as argument a term and a list of terms, and produces as output the+ −
term list applied to the term. For example+ −
+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}+ −
val args = [@{term \"True\"}, @{term \"False\"}]+ −
in+ −
list_comb (trm, args)+ −
end"+ −
"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\") + −
$ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}+ −
+ −
Another handy function is @{ML_ind lambda in Term}, which abstracts a variable + −
in a term. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val x_nat = @{term \"x::nat\"}+ −
val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}+ −
in+ −
lambda x_nat trm+ −
end"+ −
"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}+ −
+ −
In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), + −
and an abstraction, where it also records the type of the abstracted+ −
variable and for printing purposes also its name. Note that because of the+ −
typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}+ −
is of the same type as the abstracted variable. If it is of different type,+ −
as in+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val x_int = @{term \"x::int\"}+ −
val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}+ −
in+ −
lambda x_int trm+ −
end"+ −
"Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}+ −
+ −
then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. + −
This is a fundamental principle+ −
of Church-style typing, where variables with the same name still differ, if they + −
have different type.+ −
+ −
There is also the function @{ML_ind subst_free in Term} with which terms can be+ −
replaced by other terms. For example below, we will replace in @{term+ −
"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by+ −
@{term y}, and @{term x} by @{term True}.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})+ −
val sub2 = (@{term \"x::nat\"}, @{term \"True\"})+ −
val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}+ −
in+ −
subst_free [sub1, sub2] trm+ −
end"+ −
"Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}+ −
+ −
As can be seen, @{ML subst_free} does not take typability into account.+ −
However it takes alpha-equivalence into account:+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})+ −
val trm = @{term \"(\<lambda>x::nat. x)\"}+ −
in+ −
subst_free [sub] trm+ −
end"+ −
"Free (\"x\", \"nat\")"}+ −
+ −
Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound + −
variables with terms. To see how this function works, let us implement a+ −
function that strips off the outermost quantifiers in a term.+ −
*}+ −
+ −
ML{*fun strip_alls t =+ −
let + −
fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))+ −
in+ −
case t of+ −
Const ("All", _) $ Abs body => aux body+ −
| _ => ([], t)+ −
end*}+ −
+ −
text {*+ −
The function returns a pair consisting of the stripped off variables and+ −
the body of the universal quantification. For example+ −
+ −
@{ML_response_fake [display, gray]+ −
"strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"+ −
"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],+ −
Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}+ −
+ −
After calling @{ML strip_alls}, you obtain a term with lose bound variables. With+ −
the function @{ML subst_bounds}, you can replace these lose @{ML_ind + −
Bound in Term}s with the stripped off variables.+ −
+ −
@{ML_response_fake [display, gray, linenos]+ −
"let+ −
val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}+ −
in + −
subst_bounds (rev vrs, trm) + −
|> string_of_term @{context}+ −
|> tracing+ −
end"+ −
"x = y"}+ −
+ −
Note that in Line 4 we had to reverse the list of variables that @{ML+ −
strip_alls} returned. The reason is that the head of the list the function+ −
@{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next+ −
element for @{ML "Bound 1"} and so on. + −
+ −
Notice also that this function might introduce name clashes, since we+ −
substitute just a variable with the name recorded in an abstraction. This+ −
name is by no means unique. If clashes need to be avoided, then we should+ −
use the function @{ML_ind dest_abs in Term}, which returns the body where+ −
the lose de Bruijn index is replaced by a unique free variable. For example+ −
+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val body = Bound 0 $ Free (\"x\", @{typ nat})+ −
in+ −
Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)+ −
end"+ −
"(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}+ −
+ −
There are also many convenient functions that construct specific HOL-terms+ −
in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in+ −
HOLogic} constructs an equality out of two terms. The types needed in this+ −
equality are calculated from the type of the arguments. For example+ −
+ −
@{ML_response_fake [gray,display]+ −
"let+ −
val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})+ −
in+ −
string_of_term @{context} eq+ −
|> tracing+ −
end"+ −
"True = False"}+ −
+ −
\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 manual+ −
constructions of terms and types easier.+ −
\end{readmore}+ −
+ −
When constructing terms manually, 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[source] "\<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 (\"Groups.zero_class.zero\", \<dots>), + −
Const (\"Groups.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 function 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 {*+ −
The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.+ −
For example+ −
+ −
@{ML_response [display,gray]+ −
"@{type_name \"list\"}" "\"List.list\""}+ −
+ −
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 ty1 ty2 = Type ("fun", [ty1, ty2]) *}+ −
+ −
text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}+ −
+ −
ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}+ −
+ −
text {*+ −
If you want to construct a function type with more than one argument+ −
type, then you can use @{ML_ind "--->" in Term}.+ −
*}+ −
+ −
ML{*fun make_fun_types tys ty = tys ---> ty *}+ −
+ −
text {*+ −
A handy function for manipulating terms is @{ML_ind map_types in Term}: 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 ty =+ −
(case ty of+ −
@{typ nat} => @{typ int}+ −
| Type (s, tys) => Type (s, map nat_to_int tys)+ −
| _ => ty)*}+ −
+ −
text {*+ −
Here is an example:+ −
+ −
@{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\")"}+ −
+ −
If you want to obtain the list of free type-variables of a term, you+ −
can use the function @{ML_ind add_tfrees in Term} + −
(similarly @{ML_ind add_tvars in Term} for the schematic type-variables). + −
One would expect that such functions+ −
take a term as input and return a list of types. But their type is actually + −
+ −
@{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}+ −
+ −
that is they take, besides a term, also a list of type-variables as input. + −
So in order to obtain the list of type-variables of a term you have to + −
call them as follows+ −
+ −
@{ML_response [gray,display]+ −
"Term.add_tfrees @{term \"(a, b)\"} []"+ −
"[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}+ −
+ −
The reason for this definition is that @{ML add_tfrees in Term} can+ −
be easily folded over a list of terms. Similarly for all functions+ −
named @{text "add_*"} in @{ML_file "Pure/term.ML"}.+ −
+ −
\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 one)+ −
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 that takes two terms representing natural numbers+ −
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the+ −
number representing their sum.+ −
\end{exercise}+ −
+ −
\begin{exercise}\label{ex:debruijn}+ −
Implement the function, which we below name deBruijn, that depends on a natural+ −
number n$>$0 and constructs terms of the form:+ −
+ −
\begin{center}+ −
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+ −
{\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i}\\+ −
{\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}+ −
$\longrightarrow$ {\it rhs n}\\+ −
{\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
This function returns for n=3 the term+ −
+ −
\begin{center}+ −
\begin{tabular}{l}+ −
(P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\+ −
(P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\ + −
(P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3+ −
\end{tabular}+ −
\end{center}+ −
+ −
Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}+ −
for constructing the terms for the logical connectives.\footnote{Thanks to Roy+ −
Dyckhoff for suggesting this exercise and working out the details.} + −
\end{exercise}+ −
*}+ −
+ −
section {* Unification and Matching\label{sec:univ} *}+ −
+ −
text {* + −
As seen earlier, Isabelle's terms and types may contain schematic term variables+ −
(term-constructor @{ML Var}) and schematic type variables (term-constructor+ −
@{ML TVar}). These variables stand for unknown entities, which can be made+ −
more concrete by instantiations. Such instantiations might be a result of+ −
unification or matching. While in case of types, unification and matching is+ −
relatively straightforward, in case of terms the algorithms are+ −
substantially more complicated, because terms need higher-order versions of+ −
the unification and matching algorithms. Below we shall use the+ −
antiquotations @{text "@{typ_pat \<dots>}"} and @{text "@{term_pat \<dots>}"} from+ −
Section~\ref{sec:antiquote} in order to construct examples involving+ −
schematic variables.+ −
+ −
Let us begin with describing the unification and matching functions for+ −
types. Both return type environments (ML-type @{ML_type "Type.tyenv"})+ −
which map schematic type variables to types and sorts. Below we use the+ −
function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}+ −
for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *+ −
nat"}. This will produce the mapping, or type environment, @{text "[?'a :=+ −
?'b list, ?'b := nat]"}.+ −
*}+ −
+ −
ML %linenosgray{*val (tyenv_unif, _) = let+ −
val ty1 = @{typ_pat "?'a * ?'b"}+ −
val ty2 = @{typ_pat "?'b list * nat"}+ −
in+ −
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) + −
end*}+ −
+ −
text {* + −
The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type+ −
environment, which is needed for starting the unification without any+ −
(pre)instantiations. The @{text 0} is an integer index that will be explained+ −
below. In case of failure, @{ML typ_unify in Sign} will throw the exception+ −
@{text TUNIFY}. We can print out the resulting type environment bound to + −
@{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the+ −
structure @{ML_struct Vartab}.+ −
+ −
@{ML_response_fake [display,gray]+ −
"Vartab.dest tyenv_unif"+ −
"[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), + −
((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} + −
*}+ −
+ −
text_raw {*+ −
\begin{figure}[t]+ −
\begin{minipage}{\textwidth}+ −
\begin{isabelle}*}+ −
ML{*fun pretty_helper aux env =+ −
env |> Vartab.dest + −
|> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) + −
|> commas + −
|> enclose "[" "]" + −
|> tracing+ −
+ −
fun pretty_tyenv ctxt tyenv =+ −
let+ −
fun get_typs (v, (s, T)) = (TVar (v, s), T)+ −
val print = pairself (Syntax.string_of_typ ctxt)+ −
in + −
pretty_helper (print o get_typs) tyenv+ −
end*}+ −
text_raw {*+ −
\end{isabelle}+ −
\end{minipage}+ −
\caption{A pretty printing function for type environments, which are + −
produced by unification and matching.\label{fig:prettyenv}}+ −
\end{figure}+ −
*}+ −
+ −
text {*+ −
The first components in this list stand for the schematic type variables and+ −
the second are the associated sorts and types. In this example the sort is+ −
the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will+ −
use in what follows our own pretty-printing function from+ −
Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type+ −
environment in the example this function prints out the more legible:+ −
+ −
+ −
@{ML_response_fake [display, gray]+ −
"pretty_tyenv @{context} tyenv_unif"+ −
"[?'a := ?'b list, ?'b := nat]"}+ −
+ −
The way the unification function @{ML typ_unify in Sign} is implemented + −
using an initial type environment and initial index makes it easy to+ −
unify more than two terms. For example + −
*}+ −
+ −
ML %linenosgray{*val (tyenvs, _) = let+ −
val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})+ −
val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})+ −
in+ −
fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) + −
end*}+ −
+ −
text {*+ −
The index @{text 0} in Line 5 is the maximal index of the schematic type+ −
variables occurring in @{text tys1} and @{text tys2}. This index will be+ −
increased whenever a new schematic type variable is introduced during+ −
unification. This is for example the case when two schematic type variables+ −
have different, incomparable sorts. Then a new schematic type variable is+ −
introduced with the combined sorts. To show this let us assume two sorts,+ −
say @{text "s1"} and @{text "s2"}, which we attach to the schematic type+ −
variables @{text "?'a"} and @{text "?'b"}. Since we do not make any+ −
assumption about the sorts, they are incomparable.+ −
*}+ −
+ −
class s1+ −
class s2 + −
+ −
ML{*val (tyenv, index) = let+ −
val ty1 = @{typ_pat "?'a::s1"}+ −
val ty2 = @{typ_pat "?'b::s2"}+ −
in+ −
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) + −
end*}+ −
+ −
text {*+ −
To print out the result type environment we switch on the printing + −
of sort information by setting @{ML_ind show_sorts in Syntax} to + −
true. This allows us to inspect the typing environment.+ −
+ −
@{ML_response_fake [display,gray]+ −
"pretty_tyenv @{context} tyenv"+ −
"[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}+ −
+ −
As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated+ −
with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new+ −
type variable has been introduced the @{ML index}, originally being @{text 0}, + −
has been increased to @{text 1}.+ −
+ −
@{ML_response [display,gray]+ −
"index"+ −
"1"}+ −
+ −
Let us now return to the unification problem @{text "?'a * ?'b"} and + −
@{text "?'b list * nat"} from the beginning of this section, and the + −
calculated type environment @{ML tyenv_unif}:+ −
+ −
@{ML_response_fake [display, gray]+ −
"pretty_tyenv @{context} tyenv_unif"+ −
"[?'a := ?'b list, ?'b := nat]"}+ −
+ −
Observe that the type environment which the function @{ML typ_unify in+ −
Sign} returns is \emph{not} an instantiation in fully solved form: while @{text+ −
"?'b"} is instantiated to @{typ nat}, this is not propagated to the+ −
instantiation for @{text "?'a"}. In unification theory, this is often+ −
called an instantiation in \emph{triangular form}. These triangular + −
instantiations, or triangular type environments, are used because of + −
performance reasons. To apply such a type environment to a type, say @{text "?'a *+ −
?'b"}, you should use the function @{ML_ind norm_type in Envir}:+ −
+ −
@{ML_response_fake [display, gray]+ −
"Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"+ −
"nat list * nat"}+ −
+ −
Matching of types can be done with the function @{ML_ind typ_match in Sign}+ −
also from the structure @{ML_struct Sign}. This function returns a @{ML_type+ −
Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case+ −
of failure. For example+ −
*}+ −
+ −
ML{*val tyenv_match = let+ −
val pat = @{typ_pat "?'a * ?'b"}+ −
and ty = @{typ_pat "bool list * nat"}+ −
in+ −
Sign.typ_match @{theory} (pat, ty) Vartab.empty + −
end*}+ −
+ −
text {*+ −
Printing out the calculated matcher gives+ −
+ −
@{ML_response_fake [display,gray]+ −
"pretty_tyenv @{context} tyenv_match"+ −
"[?'a := bool list, ?'b := nat]"}+ −
+ −
Unlike unification, which uses the function @{ML norm_type in Envir}, + −
applying the matcher to a type needs to be done with the function+ −
@{ML_ind subst_type in Envir}. For example+ −
+ −
@{ML_response_fake [display, gray]+ −
"Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"+ −
"bool list * nat"}+ −
+ −
Be careful to observe the difference: always use+ −
@{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} + −
for unifiers. To show the difference, let us calculate the + −
following matcher:+ −
*}+ −
+ −
ML{*val tyenv_match' = let+ −
val pat = @{typ_pat "?'a * ?'b"}+ −
and ty = @{typ_pat "?'b list * nat"}+ −
in+ −
Sign.typ_match @{theory} (pat, ty) Vartab.empty + −
end*}+ −
+ −
text {*+ −
Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply + −
@{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain+ −
+ −
@{ML_response_fake [display, gray]+ −
"Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"+ −
"nat list * nat"}+ −
+ −
which does not solve the matching problem, and if+ −
we apply @{ML subst_type in Envir} to the same type we obtain+ −
+ −
@{ML_response_fake [display, gray]+ −
"Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"+ −
"?'b list * nat"}+ −
+ −
which does not solve the unification problem.+ −
+ −
\begin{readmore}+ −
Unification and matching for types is implemented+ −
in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them+ −
are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments+ −
as results. These are implemented in @{ML_file "Pure/envir.ML"}.+ −
This file also includes the substitution and normalisation functions,+ −
which apply a type environment to a type. Type environments are lookup + −
tables which are implemented in @{ML_file "Pure/term_ord.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
text {*+ −
Unification and matching of terms is substantially more complicated than the+ −
type-case. The reason is that terms have abstractions and, in this context, + −
unification or matching modulo plain equality is often not meaningful. + −
Nevertheless, Isabelle implements the function @{ML_ind+ −
first_order_match in Pattern} for terms. This matching function returns a+ −
type environment and a term environment. To pretty print the latter we use+ −
the function @{text "pretty_env"}:+ −
*}+ −
+ −
ML{*fun pretty_env ctxt env =+ −
let+ −
fun get_trms (v, (T, t)) = (Var (v, T), t) + −
val print = pairself (string_of_term ctxt)+ −
in+ −
pretty_helper (print o get_trms) env + −
end*}+ −
+ −
text {*+ −
As can be seen from the @{text "get_trms"}-function, a term environment associates + −
a schematic term variable with a type and a term. An example of a first-order + −
matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern + −
@{text "?X ?Y"}.+ −
*}+ −
+ −
ML{*val (_, fo_env) = let+ −
val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}+ −
val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} + −
val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}+ −
val init = (Vartab.empty, Vartab.empty) + −
in+ −
Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init+ −
end *}+ −
+ −
text {*+ −
In this example we annotated types explicitly because then + −
the type environment is empty and can be ignored. The + −
resulting term environment is+ −
+ −
@{ML_response_fake [display, gray]+ −
"pretty_env @{context} fo_env"+ −
"[?X := P, ?Y := \<lambda>a b. Q b a]"}+ −
+ −
The matcher can be applied to a term using the function @{ML_ind subst_term+ −
in Envir} (remember the same convention for types applies to terms: @{ML+ −
subst_term in Envir} is for matchers and @{ML norm_term in Envir} for+ −
unifiers). The function @{ML subst_term in Envir} expects a type environment,+ −
which is set to empty in the example below, and a term environment.+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}+ −
in+ −
Envir.subst_term (Vartab.empty, fo_env) trm+ −
|> string_of_term @{context}+ −
|> tracing+ −
end"+ −
"P (\<lambda>a b. Q b a)"}+ −
+ −
First-order matching is useful for matching against applications and+ −
variables. It can also deal with abstractions and a limited form of+ −
alpha-equivalence, but this kind of matching should be used with care, since+ −
it is not clear whether the result is meaningful. A meaningful example is+ −
matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this+ −
case, first-order matching produces @{text "[?X := P]"}.+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}+ −
val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"} + −
val init = (Vartab.empty, Vartab.empty) + −
in+ −
Pattern.first_order_match @{theory} (fo_pat, trm) init+ −
|> snd + −
|> pretty_env @{context} + −
end"+ −
"[?X := P]"}+ −
*}+ −
+ −
text {*+ −
Unification of abstractions is more thoroughly studied in the context of+ −
higher-order pattern unification and higher-order pattern matching. A+ −
\emph{\index*{pattern}} is a well-formed beta-normal term in which the arguments to+ −
every schematic variable are distinct bounds.+ −
In particular this excludes terms where a+ −
schematic variable is an argument of another one and where a schematic+ −
variable is applied twice with the same bound variable. The function+ −
@{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests+ −
whether a term satisfies these restrictions under the assumptions+ −
that it is beta-normal, well-typed and has no loose bound variables.+ −
+ −
@{ML_response [display, gray]+ −
"let+ −
val trm_list = + −
[@{term_pat \"?X\"}, @{term_pat \"a\"},+ −
@{term_pat \"f (\<lambda>a b. ?X a b) c\"},+ −
@{term_pat \"\<lambda>a b. (op +) a b\"},+ −
@{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},+ −
@{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},+ −
@{term_pat \"?X a\"}] + −
in+ −
map Pattern.pattern trm_list+ −
end"+ −
"[true, true, true, true, true, false, false, false, false]"}+ −
+ −
The point of the restriction to patterns is that unification and matching + −
are decidable and produce most general unifiers, respectively matchers. + −
Note that \emph{both} terms to be unified have to be higher-order patterns+ −
for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure+ −
in this regard.+ −
In this way, matching and unification can be implemented as functions that + −
produce a type and term environment (unification actually returns a + −
record of type @{ML_type Envir.env} containing a max-index, a type environment + −
and a term environment). The corresponding functions are @{ML_ind match in Pattern}+ −
and @{ML_ind unify in Pattern}, both implemented in the structure+ −
@{ML_struct Pattern}. An example for higher-order pattern unification is+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}+ −
val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}+ −
val init = Envir.empty 0+ −
val env = Pattern.unify @{theory} (trm1, trm2) init+ −
in+ −
pretty_env @{context} (Envir.term_env env)+ −
end"+ −
"[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}+ −
+ −
The function @{ML_ind "Envir.empty"} generates a record with a specified+ −
max-index for the schematic variables (in the example the index is @{text+ −
0}) and empty type and term environments. The function @{ML_ind+ −
"Envir.term_env"} pulls out the term environment from the result record. The+ −
corresponding function for type environment is @{ML_ind+ −
"Envir.type_env"}. An assumption of this function is that the terms to be+ −
unified have already the same type. In case of failure, the exceptions that+ −
are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.+ −
*}+ −
+ −
(*+ −
ML {*+ −
fun patunif_in_emptyenv (t, u) =+ −
let+ −
val init = Envir.empty 0;+ −
val env = Pattern.unify @{theory} (t, u) init;+ −
in+ −
(env |> Envir.term_env |> Vartab.dest,+ −
env |> Envir.type_env |> Vartab.dest)+ −
end+ −
*}+ −
+ −
text {*+ −
@{ML_response [display, gray]+ −
"val t1 = @{term_pat \"(% x y. ?f y x)\"};+ −
val u1 = @{term_pat \"z::bool\"};+ −
(* type conflict isnt noticed *)+ −
patunif_in_emptyenv (t1, u1);"+ −
"check missing"+ −
*}+ −
@{ML_response [display, gray] + −
"val t2 = @{term_pat \"(% y. ?f y)\"} |> Term.strip_abs_body;+ −
val u2 = @{term_pat \"z::bool\"};+ −
(* fails because of loose bounds *)+ −
(* patunif_in_emptyenv (t2, u2) *)"+ −
"check missing"+ −
*}+ −
@{ML_response [display, gray]+ −
"val t3 = @{term_pat \"(% y. plu (?f y) (% x. g x))\"};+ −
val u3 = @{term_pat \"(% y. plu y (% x. g x))\"};+ −
(* eta redexe im term egal, hidden polym wird inst *)+ −
patunif_in_emptyenv (t3, u3)"+ −
"check missing"+ −
*}+ −
@{ML_response [display, gray] + −
"val t4 = @{term_pat \"(% y. plu (?f y) ((% x. g x) k))\"};+ −
val u4 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};+ −
(* beta redexe are largely ignored, hidden polymorphism is instantiated *)+ −
patunif_in_emptyenv (t4, u4)"+ −
"check missing"+ −
*}+ −
@{ML_response [display, gray]+ −
"val t5 = @{term_pat \"(% y. plu ((% x. ?f) y) ((% x. g x) k))\"};+ −
val u5 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};+ −
(* fails: can't have beta redexes which seperate a var from its arguments *)+ −
(* patunif_in_emptyenv (t5, u5) *)"+ −
*}+ −
+ −
@{ML_response [display, gray] + −
"val t6 = @{term_pat \"(% x y. ?f x y) a b\"};+ −
val u6 = @{term_pat \"c\"};+ −
(* Pattern.pattern assumes argument is beta-normal *)+ −
Pattern.pattern t6; + −
(* fails: can't have beta redexes which seperate a var from its arguments,+ −
otherwise this would be general unification for general a,b,c *)+ −
(* patunif_in_emptyenv (t6, u6) *)"+ −
*}+ −
@{ML_response [display, gray]+ −
"val t7 = @{term_pat \"(% y. plu ((% x. ?f x) y) ((% x. g x) k))\"};+ −
val u7 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};+ −
(* eta redexe die Pattern trennen brauchen nicht normalisiert sein *)+ −
patunif_in_emptyenv (t7, u7)"+ −
*}+ −
@{ML_response [display, gray] + −
"val t8 = @{term_pat \"(% y. ?f y)\"};+ −
val u8 = @{term_pat \"(% y. y ?f)\"};+ −
(* variables of the same name are identified *)+ −
(* patunif_in_emptyenv (t8, u8) *)"+ −
*}+ −
+ −
@{ML_response [display, gray]+ −
"val t9 = @{term_pat \"(% y. ?f y)\"};+ −
val u9 = @{term_pat \"(% y. ?f y)\"};+ −
(* trivial solutions are empty and don't contain ?f = ?f etc *)+ −
patunif_in_emptyenv (t9, u9)"+ −
*}+ −
@{ML_response [display, gray] + −
"val t10 = @{term_pat \"(% y. (% x. ?f x) y)\"};+ −
val u10 = @{term_pat \"(% y. ?f y)\"};+ −
(* trivial solutions are empty and don't contain ?f = ?f etc *)+ −
patunif_in_emptyenv (t10, u10)"+ −
*}+ −
@{ML_response [display, gray]+ −
"val t11 = @{term_pat \"(% z. ?f z)\"};+ −
val u11 = @{term_pat \"(% z. k (?f z))\"};+ −
(* fails: occurs check *)+ −
(* patunif_in_emptyenv (t11, u11) *)"+ −
*}+ −
@{ML_response [display, gray]+ −
"val t12 = @{term_pat \"(% z. ?f z)\"};+ −
val u12 = @{term_pat \"?g a\"};+ −
(* fails: *both* terme have to be higher-order patterns *)+ −
(* patunif_in_emptyenv (t12, u12) *)"+ −
*}+ −
*}+ −
*)+ −
+ −
text {*+ −
+ −
As mentioned before, unrestricted higher-order unification, respectively+ −
unrestricted higher-order matching, is in general undecidable and might also+ −
not posses a single most general solution. Therefore Isabelle implements the+ −
unification function @{ML_ind unifiers in Unify} so that it returns a lazy+ −
list of potentially infinite unifiers. An example is as follows+ −
*}+ −
+ −
ML{*val uni_seq =+ −
let + −
val trm1 = @{term_pat "?X ?Y"}+ −
val trm2 = @{term "f a"}+ −
val init = Envir.empty 0+ −
in+ −
Unify.unifiers (@{theory}, init, [(trm1, trm2)])+ −
end *}+ −
+ −
text {*+ −
The unifiers can be extracted from the lazy sequence using the + −
function @{ML_ind "Seq.pull"}. In the example we obtain three + −
unifiers @{text "un1\<dots>un3"}.+ −
*}+ −
+ −
ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;+ −
val SOME ((un2, _), next2) = Seq.pull next1;+ −
val SOME ((un3, _), next3) = Seq.pull next2;+ −
val NONE = Seq.pull next3 *}+ −
+ −
text {*+ −
\footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}+ −
+ −
We can print them out as follows.+ −
+ −
@{ML_response_fake [display, gray]+ −
"pretty_env @{context} (Envir.term_env un1);+ −
pretty_env @{context} (Envir.term_env un2);+ −
pretty_env @{context} (Envir.term_env un3)"+ −
"[?X := \<lambda>a. a, ?Y := f a]+ −
[?X := f, ?Y := a]+ −
[?X := \<lambda>b. f a]"}+ −
+ −
+ −
In case of failure the function @{ML_ind unifiers in Unify} does not raise+ −
an exception, rather returns the empty sequence. For example+ −
+ −
@{ML_response [display, gray]+ −
"let + −
val trm1 = @{term \"a\"}+ −
val trm2 = @{term \"b\"}+ −
val init = Envir.empty 0+ −
in+ −
Unify.unifiers (@{theory}, init, [(trm1, trm2)])+ −
|> Seq.pull+ −
end"+ −
"NONE"}+ −
+ −
In order to find a reasonable solution for a unification problem, Isabelle+ −
also tries first to solve the problem by higher-order pattern+ −
unification. Only in case of failure full higher-order unification is+ −
called. This function has a built-in bound, which can be accessed and+ −
manipulated as a configuration value:+ −
+ −
@{ML_response_fake [display,gray]+ −
"Config.get_global @{theory} (Unify.search_bound_value)"+ −
"Int 60"}+ −
+ −
If this bound is reached during unification, Isabelle prints out the+ −
warning message @{text [quotes] "Unification bound exceeded"} and+ −
plenty of diagnostic information (sometimes annoyingly plenty of + −
information). + −
+ −
+ −
For higher-order matching the function is called @{ML_ind matchers in Unify}+ −
implemented in the structure @{ML_struct Unify}. Also this function returns+ −
sequences with possibly more than one matcher. Like @{ML unifiers in+ −
Unify}, this function does not raise an exception in case of failure, but+ −
returns an empty sequence. It also first tries out whether the matching+ −
problem can be solved by first-order matching.+ −
+ −
Higher-order matching might be necessary for instantiating a theorem+ −
appropriately. More on this will be given in Sections~\ref{sec:theorems}. + −
Here we only have a look at a simple case, namely the theorem + −
@{thm [source] spec}:+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{thm [source] spec}\\+ −
@{text "> "}~@{thm spec}+ −
\end{isabelle}+ −
+ −
as an introduction rule. Applying it directly can lead to unexpected+ −
behaviour since the unification has more than one solution. One way round+ −
this problem is to instantiate the schematic variables @{text "?P"} and+ −
@{text "?x"}. instantiation function for theorems is @{ML_ind instantiate+ −
in Drule} from the structure @{ML_struct Drule}. One problem, however, is+ −
that this function expects the instantiations as lists of @{ML_type ctyp}+ −
and @{ML_type cterm} pairs:+ −
+ −
\begin{isabelle}+ −
@{ML instantiate in Drule}@{text ":"}+ −
@{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}+ −
\end{isabelle}+ −
+ −
This means we have to transform the environment the higher-order matching + −
function returns into such an instantiation. For this we use the functions+ −
@{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract+ −
from an environment the corresponding variable mappings for schematic type + −
and term variables. These mappings can be turned into proper + −
@{ML_type ctyp}-pairs with the function+ −
*}+ −
+ −
ML{*fun prep_trm thy (x, (T, t)) = + −
(cterm_of thy (Var (x, T)), cterm_of thy t)*} + −
+ −
text {*+ −
and into proper @{ML_type cterm}-pairs with+ −
*}+ −
+ −
ML{*fun prep_ty thy (x, (S, ty)) = + −
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}+ −
+ −
text {*+ −
We can now calculate the instantiations from the matching function. + −
*}+ −
+ −
ML %linenosgray{*fun matcher_inst thy pat trm i = + −
let+ −
val univ = Unify.matchers thy [(pat, trm)] + −
val env = nth (Seq.list_of univ) i+ −
val tenv = Vartab.dest (Envir.term_env env)+ −
val tyenv = Vartab.dest (Envir.type_env env)+ −
in+ −
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)+ −
end*}+ −
+ −
text {*+ −
In Line 3 we obtain the higher-order matcher. We assume there is a finite+ −
number of them and select the one we are interested in via the parameter + −
@{text i} in the next line. In Lines 5 and 6 we destruct the resulting + −
environments using the function @{ML_ind dest in Vartab}. Finally, we need + −
to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective + −
environments (Line 8). As a simple example we instantiate the+ −
@{thm [source] spec} rule so that its conclusion is of the form + −
@{term "Q True"}. + −
+ −
+ −
@{ML_response_fake [gray,display,linenos] + −
"let + −
val pat = Logic.strip_imp_concl (prop_of @{thm spec})+ −
val trm = @{term \"Trueprop (Q True)\"}+ −
val inst = matcher_inst @{theory} pat trm 1+ −
in+ −
Drule.instantiate inst @{thm spec}+ −
end"+ −
"\<forall>x. Q x \<Longrightarrow> Q True"}+ −
+ −
Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the + −
conclusion of @{thm [source] spec} contains one.+ −
+ −
\begin{readmore}+ −
Unification and matching of higher-order patterns is implemented in + −
@{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher+ −
for terms. Full higher-order unification is implemented+ −
in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented+ −
in @{ML_file "Pure/General/seq.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Sorts (TBD) *}+ −
+ −
text {*+ −
Type classes are formal names in the type system which are linked to+ −
predicates on of one type variable (via the axclass mechanism) and thereby+ −
express extra properties on types to be propagated by the type system.+ −
The type-in-class judgement is defined+ −
over a simple logic based on implication and schematic quantification.+ −
The signature of this logic is called an order-sorted algebra (see Schmidt-Schauss)+ −
and consists of an acyclic subclass relation and a set of image+ −
declarations for type constructors, called arities.+ −
+ −
A well-behaved high-level view on type classes has long been established+ −
(cite Haftmann-Wenzel): the predicate behind a type class is the basis for a locale+ −
(for context-management reasons)+ −
and may use so-called type class parameters which are implemented as overloaded+ −
constants. Overloading a constant means specifying its type-indexed value based on+ −
a well-founded reduction towards other constants. When instantiating type classes+ −
(i.e. proving arities) you are specifying overloading via primitive recursion.+ −
+ −
Sorts are finite intersections of type classes and are implemented as lists+ −
of type class names. The empty intersection, i.e. the empty list, is therefore+ −
inhabited by all types and is called the topsort.+ −
+ −
Free and schematic type variables may be annotated with sorts, thereby restricting+ −
the domain of types they quantify over and corresponding to an implicit hypothesis+ −
about the type variable.+ −
*}+ −
+ −
+ −
ML {* Sign.classes_of @{theory} *}+ −
+ −
text {*+ −
\begin{readmore}+ −
Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.+ −
+ −
@{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,+ −
manages the order sorted algebra and offers an interface for reinterpreting+ −
derivations of type in class judgements+ −
@{ML_file "Pure/defs.ML"} manages the constant definition dependency graph and keeps it well-founded+ −
(its define function doesn't terminate for complex non-well-founded dependencies)+ −
@{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations+ −
and provides basic infrastructure for establishing the high-level view on type classes+ −
@{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations+ −
(especially names, constants, paths, type classes) a+ −
theory acquires by theory extension mechanisms and manages associated certification+ −
functionality.+ −
It also provides the most needed functionality from individual underlying modules.+ −
\end{readmore}+ −
*}+ −
+ −
+ −
section {* Type-Checking\label{sec:typechecking} *}+ −
+ −
text {* + −
Remember Isabelle follows 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_ind type_of in Term} 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 example 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_ind fastype_of in Term}, 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_ind dummyT in Term} and then let type-inference figure out the + −
complete type. The type inference can be invoked with the function+ −
@{ML_ind check_term in Syntax}. 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"}, type-inference fills 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. Functions related to+ −
type-inference are implemented in @{ML_file "Pure/type.ML"} and + −
@{ML_file "Pure/type_infer.ML"}. + −
\end{readmore}+ −
+ −
+ −
\begin{exercise}+ −
Check that the function defined in Exercise~\ref{fun:revsum} returns a+ −
result that type-checks. See what happens to the solutions of this + −
exercise given in Appendix \ref{ch:solutions} when they receive an + −
ill-typed term as input.+ −
\end{exercise}+ −
*}+ −
+ −
section {* Certified Terms and Certified Types *}+ −
+ −
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_ind cterm_of in Thm}, 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''.+ −
+ −
Certification is always relative to a theory context. 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\"}+ −
val plus = Const (@{const_name plus}, [natT, natT] ---> natT)+ −
in+ −
cterm_of @{theory} (plus $ zero $ zero)+ −
end" + −
"0 + 0"}+ −
+ −
In Isabelle not just terms need to be certified, but also types. For example, + −
you obtain the certified type for the Isabelle 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"}+ −
+ −
or with the antiquotation:+ −
+ −
@{ML_response_fake [display,gray]+ −
"@{ctyp \"nat \<Rightarrow> bool\"}"+ −
"nat \<Rightarrow> bool"}+ −
+ −
Since certified terms are, unlike terms, abstract objects, we cannot+ −
pattern-match against them. However, we can construct them. For example+ −
the function @{ML_ind capply in Thm} produces a certified application.+ −
+ −
@{ML_response_fake [display,gray]+ −
"Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"+ −
"P 3"}+ −
+ −
Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}+ −
applies a list of @{ML_type cterm}s.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}+ −
val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]+ −
in+ −
Drule.list_comb (chead, cargs)+ −
end"+ −
"P () 3"}+ −
+ −
\begin{readmore}+ −
For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see + −
the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and+ −
@{ML_file "Pure/drule.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Theorems\label{sec:theorems} *}+ −
+ −
text {*+ −
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} + −
that can only be built by going through interfaces. As a consequence, every proof + −
in Isabelle is correct by construction. This follows the tradition of the LCF-approach.+ −
+ −
+ −
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:+ −
*}+ −
+ −
ML %linenosgray{*val my_thm = + −
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*}+ −
+ −
text {*+ −
Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which+ −
inserts necessary @{text "Trueprop"}s.+ −
+ −
If we print out the value of @{ML my_thm} then we see only the + −
final statement of the theorem.+ −
+ −
@{ML_response_fake [display, gray]+ −
"tracing (string_of_thm @{context} my_thm)"+ −
"\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}+ −
+ −
However, internally the 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"}}{}+ −
}+ −
}+ −
}+ −
\]+ −
+ −
While we obtained a theorem as result, this theorem is not+ −
yet stored in Isabelle's theorem database. Consequently, it cannot be + −
referenced on the user level. One way to store it in the theorem database is+ −
by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer+ −
to the section about local-setup is given here.}+ −
*}+ −
+ −
local_setup %gray {*+ −
Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}+ −
+ −
text {*+ −
The third argument of @{ML note in Local_Theory} is the list of theorems we+ −
want to store under a name. We can store more than one under a single name. + −
The first argument of @{ML note in Local_Theory} is the name under+ −
which we store the theorem or theorems. The second argument can contain a+ −
list of theorem attributes, which we will explain in detail in+ −
Section~\ref{sec:attributes}. Below we just use one such attribute for+ −
adding the theorem to the simpset:+ −
*}+ −
+ −
local_setup %gray {*+ −
Local_Theory.note ((@{binding "my_thm_simp"}, + −
[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}+ −
+ −
text {*+ −
Note that we have to use another name under which the theorem is stored,+ −
since Isabelle does not allow us to call @{ML_ind note in Local_Theory} twice+ −
with the same name. The attribute needs to be wrapped inside the function @{ML_ind+ −
internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function + −
@{ML get_thm_names_from_ss} from+ −
the previous chapter, we can check whether the theorem has actually been+ −
added.+ −
+ −
+ −
@{ML_response [display,gray]+ −
"let+ −
fun pred s = match_string \"my_thm_simp\" s+ −
in+ −
exists pred (get_thm_names_from_ss @{simpset})+ −
end"+ −
"true"}+ −
+ −
The main point of storing the theorems @{thm [source] my_thm} and @{thm+ −
[source] my_thm_simp} is that they can now also be referenced with the+ −
\isacommand{thm}-command on the user-level of Isabelle+ −
+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline+ −
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline+ −
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}+ −
\end{isabelle}+ −
+ −
or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the + −
user has no access to these theorems. + −
+ −
Recall that Isabelle does not let you call @{ML note in Local_Theory} twice+ −
with the same theorem name. In effect, once a theorem is stored under a name, + −
this association is fixed. While this is a ``safety-net'' to make sure a+ −
theorem name refers to a particular theorem or collection of theorems, it is + −
also a bit too restrictive in cases where a theorem name should refer to a + −
dynamically expanding list of theorems (like a simpset). Therefore Isabelle + −
also implements a mechanism where a theorem name can refer to a custom theorem + −
list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. + −
To see how it works let us assume we defined our own theorem list @{text MyThmList}.+ −
*}+ −
+ −
ML{*structure MyThmList = Generic_Data+ −
(type T = thm list+ −
val empty = []+ −
val extend = I+ −
val merge = merge Thm.eq_thm_prop)+ −
+ −
fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}+ −
+ −
text {*+ −
The function @{ML update} allows us to update the theorem list, for example+ −
by adding the theorem @{thm [source] TrueI}.+ −
*}+ −
+ −
setup %gray {* update @{thm TrueI} *}+ −
+ −
text {*+ −
We can now install the theorem list so that it is visible to the user and + −
can be refered to by a theorem name. For this need to call + −
@{ML_ind add_thms_dynamic in PureThy}+ −
*}+ −
+ −
setup %gray {* + −
PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) + −
*}+ −
+ −
text {*+ −
with a name and a function that accesses the theorem list. Now if the+ −
user issues the command+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "mythmlist"}\\+ −
@{text "> True"}+ −
\end{isabelle}+ −
+ −
the current content of the theorem list is displayed. If more theorems are stored in + −
the list, say+ −
*}+ −
+ −
setup %gray {* update @{thm FalseE} *}+ −
+ −
text {*+ −
then the same command produces+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "mythmlist"}\\+ −
@{text "> False \<Longrightarrow> ?P"}\\+ −
@{text "> True"}+ −
\end{isabelle}+ −
+ −
Note that if we add the theorem @{thm [source] FalseE} again to the list+ −
*}+ −
+ −
setup %gray {* update @{thm FalseE} *}+ −
+ −
text {*+ −
we still obtain the same list. The reason is that we used the function @{ML_ind+ −
add_thm in Thm} in our update function. This is a dedicated function which+ −
tests whether the theorem is already in the list. This test is done+ −
according to alpha-equivalence of the proposition of the theorem. The+ −
corresponding testing function is @{ML_ind eq_thm_prop in Thm}.+ −
Suppose you proved the following three theorems.+ −
*}+ −
+ −
lemma+ −
shows thm1: "\<forall>x. P x" + −
and thm2: "\<forall>y. P y" + −
and thm3: "\<forall>y. Q y" sorry+ −
+ −
text {*+ −
Testing them for alpha equality produces:+ −
+ −
@{ML_response [display,gray]+ −
"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),+ −
Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"+ −
"(true, false)"}+ −
+ −
Many functions destruct theorems into @{ML_type cterm}s. For example+ −
the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return + −
the left and right-hand side, respectively, of a meta-equality.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val eq = @{thm True_def}+ −
in+ −
(Thm.lhs_of eq, Thm.rhs_of eq) + −
|> pairself (string_of_cterm @{context})+ −
end"+ −
"(True, (\<lambda>x. x) = (\<lambda>x. x))"}+ −
+ −
Other function produce terms that can be pattern-matched. + −
Suppose the following two theorems.+ −
*}+ −
+ −
lemma + −
shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C" + −
and foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry+ −
+ −
text {*+ −
We can destruct them into premises and conclusions as follows. + −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ctxt = @{context}+ −
fun prems_and_concl thm =+ −
[\"Premises: \" ^ (string_of_terms ctxt (Thm.prems_of thm))] @ + −
[\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]+ −
|> cat_lines+ −
|> tracing+ −
in+ −
prems_and_concl @{thm foo_test1};+ −
prems_and_concl @{thm foo_test2}+ −
end"+ −
"Premises: ?A, ?B+ −
Conclusion: ?C+ −
Premises: + −
Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}+ −
+ −
Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}+ −
separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication+ −
from HOL, which just constructs a formula.+ −
+ −
\begin{readmore}+ −
The basic functions for theorems are defined in+ −
@{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. + −
\end{readmore}+ −
+ −
Although we will explain the simplifier in more detail as tactic in + −
Section~\ref{sec:simplifier}, the simplifier + −
can be used to work directly over theorems, for example to unfold definitions. To show+ −
this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then + −
unfold the constant @{term "True"} according to its definition (Line 2).+ −
+ −
@{ML_response_fake [display,gray,linenos]+ −
"Thm.reflexive @{cterm \"True\"}+ −
|> Simplifier.rewrite_rule [@{thm True_def}]+ −
|> string_of_thm @{context}+ −
|> tracing"+ −
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}+ −
+ −
Often it is necessary to transform theorems to and from the object + −
logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} + −
and @{text "\<And>"}, or the other way around. A reason for such a transformation + −
might be stating a definition. The reason is that definitions can only be + −
stated using object logic connectives, while theorems using the connectives + −
from the meta logic are more convenient for reasoning. Therefore there are+ −
some build in functions which help with these transformations. The function + −
@{ML_ind rulify in Object_Logic} + −
replaces all object connectives by equivalents in the meta logic. For example+ −
+ −
@{ML_response_fake [display, gray]+ −
"Object_Logic.rulify @{thm foo_test2}"+ −
"\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}+ −
+ −
The transformation in the other direction can be achieved with function+ −
@{ML_ind atomize in Object_Logic} and the following code.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val thm = @{thm foo_test1}+ −
val meta_eq = Object_Logic.atomize (cprop_of thm)+ −
in+ −
MetaSimplifier.rewrite_rule [meta_eq] thm+ −
end"+ −
"?A \<longrightarrow> ?B \<longrightarrow> ?C"}+ −
+ −
In this code the function @{ML atomize in Object_Logic} produces + −
a meta-equation between the given theorem and the theorem transformed+ −
into the object logic. The result is the theorem with object logic + −
connectives. However, in order to completely transform a theorem+ −
involving meta variables, such as @{thm [source] list.induct}, which + −
is of the form + −
+ −
@{thm [display] list.induct}+ −
+ −
we have to first abstract over the meta variables @{text "?P"} and + −
@{text "?list"}. For this we can use the function + −
@{ML_ind forall_intr_vars in Drule}. This allows us to implement the+ −
following function for atomizing a theorem.+ −
*}+ −
+ −
ML{*fun atomize_thm thm =+ −
let+ −
val thm' = forall_intr_vars thm+ −
val thm'' = Object_Logic.atomize (cprop_of thm')+ −
in+ −
MetaSimplifier.rewrite_rule [thm''] thm'+ −
end*}+ −
+ −
text {*+ −
This function produces for the theorem @{thm [source] list.induct}+ −
+ −
@{ML_response_fake [display, gray]+ −
"atomize_thm @{thm list.induct}"+ −
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}+ −
+ −
Theorems can also be produced from terms by giving an explicit proof. + −
One way to achieve this is by using the function @{ML_ind prove in Goal}+ −
in the structure @{ML_struct Goal}. For example below we use this function+ −
to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?}+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val trm = @{term \"P \<Longrightarrow> P::bool\"}+ −
val tac = K (atac 1)+ −
in+ −
Goal.prove @{context} [\"P\"] [] trm tac+ −
end"+ −
"?P \<Longrightarrow> ?P"}+ −
+ −
This function takes first a context and second a list of strings. This list+ −
specifies which variables should be turned into schematic variables once the term+ −
is proved. The fourth argument is the term to be proved. The fifth is a+ −
corresponding proof given in form of a tactic (we explain tactics in+ −
Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem+ −
by assumption. As before this code will produce a theorem, but the theorem+ −
is not yet stored in the theorem database. + −
+ −
While the LCF-approach of going through interfaces ensures soundness in Isabelle, there+ −
is the function @{ML_ind make_thm in Skip_Proof} in the structure + −
@{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.+ −
Potentially making the system unsound. This is sometimes useful for developing + −
purposes, or when explicit proof construction should be omitted due to performace + −
reasons. An example of this function is as follows:+ −
+ −
@{ML_response_fake [display, gray]+ −
"Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"+ −
"True = False"}+ −
+ −
\begin{readmore}+ −
Functions that setup goal states and prove theorems are implemented in + −
@{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to+ −
skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.+ −
\end{readmore}+ −
+ −
Theorems also contain auxiliary data, such as the name of the theorem, its+ −
kind, the names for cases and so on. This data is stored in a string-string+ −
list and can be retrieved with the function @{ML_ind get_tags in+ −
Thm}. Assume you prove the following lemma.+ −
*}+ −
+ −
lemma foo_data: + −
shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption+ −
+ −
text {*+ −
The auxiliary data of this lemma can be retrieved using the function + −
@{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is + −
+ −
@{ML_response_fake [display,gray]+ −
"Thm.get_tags @{thm foo_data}"+ −
"[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}+ −
+ −
consisting of a name and a kind. When we store lemmas in the theorem database, + −
we might want to explicitly extend this data by attaching case names to the + −
two premises of the lemma. This can be done with the function @{ML_ind name in Rule_Cases}+ −
from the structure @{ML_struct Rule_Cases}.+ −
*}+ −
+ −
local_setup %gray {*+ −
Local_Theory.note ((@{binding "foo_data'"}, []), + −
[(Rule_Cases.name ["foo_case_one", "foo_case_two"] + −
@{thm foo_data})]) #> snd *}+ −
+ −
text {*+ −
The data of the theorem @{thm [source] foo_data'} is then as follows:+ −
+ −
@{ML_response_fake [display,gray]+ −
"Thm.get_tags @{thm foo_data'}"+ −
"[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), + −
(\"case_names\", \"foo_case_one;foo_case_two\")]"}+ −
+ −
You can observe the case names of this lemma on the user level when using + −
the proof methods @{text cases} and @{text induct}. In the proof below+ −
*}+ −
+ −
lemma+ −
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"+ −
proof (cases rule: foo_data')+ −
+ −
(*<*)oops(*>*)+ −
text_raw{*+ −
\begin{tabular}{@ {}l}+ −
\isacommand{print\_cases}\\+ −
@{text "> cases:"}\\+ −
@{text "> foo_case_one:"}\\+ −
@{text "> let \"?case\" = \"?P\""}\\+ −
@{text "> foo_case_two:"}\\+ −
@{text "> let \"?case\" = \"?P\""}+ −
\end{tabular}*}+ −
+ −
text {*+ −
we can proceed by analysing the cases @{text "foo_case_one"} and + −
@{text "foo_case_two"}. While if the theorem has no names, then+ −
the cases have standard names @{text 1}, @{text 2} and so + −
on. This can be seen in the proof below.+ −
*}+ −
+ −
lemma+ −
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"+ −
proof (cases rule: foo_data)+ −
+ −
(*<*)oops(*>*)+ −
text_raw{*+ −
\begin{tabular}{@ {}l}+ −
\isacommand{print\_cases}\\+ −
@{text "> cases:"}\\+ −
@{text "> 1:"}\\+ −
@{text "> let \"?case\" = \"?P\""}\\+ −
@{text "> 2:"}\\+ −
@{text "> let \"?case\" = \"?P\""}+ −
\end{tabular}*}+ −
+ −
+ −
text {*+ −
One great feature of Isabelle is its document preparation system, where+ −
proved theorems can be quoted in documents referencing directly their+ −
formalisation. This helps tremendously to minimise cut-and-paste errors. However,+ −
sometimes the verbatim quoting is not what is wanted or what can be shown to+ −
readers. For such situations Isabelle allows the installation of \emph{\index*{theorem + −
styles}}. These are, roughly speaking, functions from terms to terms. The input + −
term stands for the theorem to be presented; the output can be constructed to+ −
ones wishes. Let us, for example, assume we want to quote theorems without+ −
leading @{text \<forall>}-quantifiers. For this we can implement the following function + −
that strips off @{text "\<forall>"}s.+ −
*}+ −
+ −
ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = + −
Term.dest_abs body |> snd |> strip_allq+ −
| strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = + −
strip_allq t+ −
| strip_allq t = t*}+ −
+ −
text {*+ −
We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,+ −
since this function deals correctly with potential name clashes. This function produces+ −
a pair consisting of the variable and the body of the abstraction. We are only interested+ −
in the body, which we feed into the recursive call. In Line 3 and 4, we also+ −
have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can + −
install this function as the theorem style named @{text "my_strip_allq"}. + −
*}+ −
+ −
setup %gray{* + −
Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) + −
*}+ −
+ −
text {*+ −
We can test this theorem style with the following theorem+ −
*}+ −
+ −
theorem style_test:+ −
shows "\<forall>x y z. (x, x) = (y, z)" sorry+ −
+ −
text {*+ −
Now printing out in a document the theorem @{thm [source] style_test} normally+ −
using @{text "@{thm \<dots>}"} produces+ −
+ −
\begin{isabelle}+ −
@{text "@{thm style_test}"}\\+ −
@{text ">"}~@{thm style_test}+ −
\end{isabelle}+ −
+ −
as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} + −
we obtain+ −
+ −
\begin{isabelle}+ −
@{text "@{thm (my_strip_allq) style_test}"}\\+ −
@{text ">"}~@{thm (my_strip_allq) style_test}+ −
\end{isabelle}+ −
+ −
without the leading quantifiers. We can improve this theorem style by explicitly + −
giving a list of strings that should be used for the replacement of the+ −
variables. For this we implement the function which takes a list of strings+ −
and uses them as name in the outermost abstractions.+ −
*}+ −
+ −
ML{*fun rename_allq [] t = t+ −
| rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = + −
Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)+ −
| rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =+ −
rename_allq xs t+ −
| rename_allq _ t = t*}+ −
+ −
text {*+ −
We can now install a the modified theorem style as follows+ −
*}+ −
+ −
setup %gray {* let+ −
val parser = Scan.repeat Args.name+ −
fun action xs = K (rename_allq xs #> strip_allq)+ −
in+ −
Term_Style.setup "my_strip_allq2" (parser >> action)+ −
end *}+ −
+ −
text {*+ −
The parser reads a list of names. In the function @{text action} we first+ −
call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}+ −
on the resulting term. We can now suggest, for example, two variables for+ −
stripping off the first two @{text \<forall>}-quantifiers.+ −
+ −
+ −
\begin{isabelle}+ −
@{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\+ −
@{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}+ −
\end{isabelle}+ −
+ −
Such styles allow one to print out theorems in documents formatted to + −
ones heart content. The styles can also be used in the document + −
antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"}+ −
and @{text "@{typeof ...}"}.+ −
+ −
Next we explain theorem attributes, which is another+ −
mechanism for dealing with theorems.+ −
+ −
\begin{readmore}+ −
Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Theorem Attributes\label{sec:attributes} *}+ −
+ −
text {*+ −
Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text+ −
"[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags+ −
annotated to theorems, but functions that do further processing of + −
theorems. 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 retrievable + −
data structure. + −
+ −
If you want to print out all currently known attributes a theorem can have, + −
you can use the Isabelle command+ −
+ −
\begin{isabelle}+ −
\isacommand{print\_attributes}\\+ −
@{text "> COMP: direct composition with rules (no lifting)"}\\+ −
@{text "> HOL.dest: declaration of Classical destruction rule"}\\+ −
@{text "> HOL.elim: declaration of Classical elimination rule"}\\+ −
@{text "> \<dots>"}+ −
\end{isabelle}+ −
+ −
The theorem attributes fall roughly into two categories: the first category manipulates+ −
theorems (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second+ −
stores theorems somewhere as data (for example @{text "[simp]"}, which adds+ −
theorems to the current simpset).+ −
+ −
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_ind rule_attribute in Thm} 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 theorem + −
@{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule} + −
is explained in Section~\ref{sec:simpletacs}). The function + −
@{ML rule_attribute in Thm} then returns an attribute.+ −
+ −
Before we can use the attribute, we need to set it up. This can be done+ −
using the Isabelle command \isacommand{attribute\_setup} as follows:+ −
*}+ −
+ −
attribute_setup %gray my_sym = + −
{* Scan.succeed my_symmetric *} "applying the sym rule"+ −
+ −
text {*+ −
Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser+ −
for the theorem attribute. Since the attribute does not expect any further + −
arguments (unlike @{text "[THEN \<dots>]"}, for instance), we use the parser @{ML+ −
Scan.succeed}. 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}. You+ −
can see this, if you query the lemma: + −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test"}\\+ −
@{text "> "}~@{thm test}+ −
\end{isabelle}+ −
+ −
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}+ −
+ −
An alternative for setting up an attribute is the function @{ML_ind setup in Attrib}.+ −
So instead of using \isacommand{attribute\_setup}, you can also set up the+ −
attribute as follows:+ −
*}+ −
+ −
ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)+ −
"applying the sym rule" *}+ −
+ −
text {*+ −
This gives a function from @{ML_type "theory -> theory"}, which+ −
can be used for example with \isacommand{setup} or with+ −
@{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.}+ −
+ −
As an example of a slightly more complicated theorem attribute, we implement + −
our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems+ −
as argument and resolve the theorem with this list (one theorem + −
after another). The code for this attribute is+ −
*}+ −
+ −
ML{*fun MY_THEN thms = + −
let+ −
fun RS_rev thm1 thm2 = thm2 RS thm1+ −
in+ −
Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)+ −
end*}+ −
+ −
text {* + −
where for convenience we define the reverse and curried version of @{ML RS}. + −
The setup of this theorem attribute uses the parser @{ML thms in Attrib}, + −
which parses a list of theorems. + −
*}+ −
+ −
attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} + −
"resolving the list of theorems with the theorem"+ −
+ −
text {* + −
You can, for example, use this theorem attribute to turn an equation into a + −
meta-equation:+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\+ −
@{text "> "}~@{thm test[MY_THEN eq_reflection]}+ −
\end{isabelle}+ −
+ −
If you need the symmetric version as a meta-equation, you can write+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\+ −
@{text "> "}~@{thm test[MY_THEN sym eq_reflection]}+ −
\end{isabelle}+ −
+ −
It is also possible to combine different theorem attributes, as in:+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\+ −
@{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}+ −
\end{isabelle}+ −
+ −
However, here also a weakness of the concept+ −
of theorem attributes shows through: since theorem attributes can be+ −
arbitrary functions, they do not commute in general. If you try+ −
+ −
\begin{isabelle}+ −
\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\+ −
@{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}+ −
\end{isabelle}+ −
+ −
you get an exception indicating that the theorem @{thm [source] sym}+ −
does not resolve with meta-equations. + −
+ −
The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate+ −
theorems. Another usage of theorem attributes is to add and delete theorems+ −
from stored data. For example the theorem attribute @{text "[simp]"} adds+ −
or deletes a theorem from the current simpset. For these applications, you+ −
can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,+ −
let us introduce a theorem list.+ −
*}+ −
+ −
ML{*structure MyThms = Named_Thms+ −
(val name = "attr_thms" + −
val description = "Theorems for an Attribute") *}+ −
+ −
text {* + −
We are going to modify this list by adding and deleting theorems.+ −
For this we use the two functions @{ML MyThms.add_thm} and+ −
@{ML MyThms.del_thm}. You can turn them into attributes + −
with the code+ −
*}+ −
+ −
ML{*val my_add = Thm.declaration_attribute MyThms.add_thm+ −
val my_del = Thm.declaration_attribute MyThms.del_thm *}+ −
+ −
text {* + −
and set up the attributes as follows+ −
*}+ −
+ −
attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} + −
"maintaining a list of my_thms" + −
+ −
text {*+ −
The parser @{ML_ind add_del in Attrib} is a predefined parser for + −
adding and deleting lemmas. Now if you prove the next lemma + −
and attach to it the attribute @{text "[my_thms]"}+ −
*}+ −
+ −
lemma trueI_2[my_thms]: "True" by simp+ −
+ −
text {*+ −
then you can see it is added to the initially empty list.+ −
+ −
@{ML_response_fake [display,gray]+ −
"MyThms.get @{context}" + −
"[\"True\"]"}+ −
+ −
You can also add theorems using the command \isacommand{declare}.+ −
*}+ −
+ −
declare test[my_thms] trueI_2[my_thms add]+ −
+ −
text {*+ −
With this attribute, the @{text "add"} operation is the default and does + −
not need to be explicitly given. These three declarations will cause the + −
theorem list to be updated as:+ −
+ −
@{ML_response_fake [display,gray]+ −
"MyThms.get @{context}"+ −
"[\"True\", \"Suc (Suc 0) = 2\"]"}+ −
+ −
The theorem @{thm [source] trueI_2} only appears once, since the + −
function @{ML_ind add_thm in 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]+ −
"MyThms.get @{context}"+ −
"[\"True\"]"}+ −
+ −
We used in this example two functions declared as @{ML_ind+ −
declaration_attribute in Thm}, but there can be any number of them. We just+ −
have to change the parser for reading the arguments accordingly.+ −
+ −
\footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}+ −
\footnote{\bf FIXME readmore}+ −
+ −
\begin{readmore}+ −
FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in + −
@{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about+ −
parsing.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Pretty-Printing\label{sec:pretty} *}+ −
+ −
text {*+ −
So far we printed out only plain strings without any formatting except for+ −
occasional explicit line breaks using @{text [quotes] "\\n"}. This is+ −
sufficient for ``quick-and-dirty'' printouts. For something more+ −
sophisticated, Isabelle includes an infrastructure for properly formatting+ −
text. Most of its functions do not operate on @{ML_type string}s, but on+ −
instances of the pretty type:+ −
+ −
@{ML_type_ind [display, gray] "Pretty.T"}+ −
+ −
The function @{ML str in Pretty} transforms a (plain) string into such a pretty + −
type. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"Pretty.str \"test\"" "String (\"test\", 4)"}+ −
+ −
where the result indicates that we transformed a string with length 4. Once+ −
you have a pretty type, you can, for example, control where linebreaks may+ −
occur in case the text wraps over a line, or with how much indentation a+ −
text should be printed. However, if you want to actually output the+ −
formatted text, you have to transform the pretty type back into a @{ML_type+ −
string}. This can be done with the function @{ML_ind string_of in Pretty}. In what+ −
follows we will use the following wrapper function for printing a pretty+ −
type:+ −
*}+ −
+ −
ML{*fun pprint prt = tracing (Pretty.string_of prt)*}+ −
+ −
text {*+ −
The point of the pretty-printing infrastructure is to give hints about how to+ −
layout text and let Isabelle do the actual layout. Let us first explain+ −
how you can insert places where a line break can occur. For this assume the+ −
following function that replicates a string n times:+ −
*}+ −
+ −
ML{*fun rep n str = implode (replicate n str) *}+ −
+ −
text {*+ −
and suppose we want to print out the string:+ −
*}+ −
+ −
ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}+ −
+ −
text {*+ −
We deliberately chose a large string so that it spans over more than one line. + −
If we print out the string using the usual ``quick-and-dirty'' method, then+ −
we obtain the ugly output:+ −
+ −
@{ML_response_fake [display,gray]+ −
"tracing test_str"+ −
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo+ −
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa+ −
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo+ −
oooooooooooooobaaaaaaaaaaaar"}+ −
+ −
We obtain the same if we just use the function @{ML pprint}.+ −
+ −
@{ML_response_fake [display,gray]+ −
"pprint (Pretty.str test_str)"+ −
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo+ −
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa+ −
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo+ −
oooooooooooooobaaaaaaaaaaaar"}+ −
+ −
However by using pretty types you have the ability to indicate possible+ −
linebreaks for example at each whitespace. You can achieve this with the+ −
function @{ML_ind breaks in Pretty}, which expects a list of pretty types+ −
and inserts a possible line break in between every two elements in this+ −
list. To print this list of pretty types as a single string, we concatenate+ −
them with the function @{ML_ind blk in Pretty} as follows:+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs = map Pretty.str (space_explode \" \" test_str)+ −
in+ −
pprint (Pretty.blk (0, Pretty.breaks ptrs))+ −
end"+ −
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar+ −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}+ −
+ −
Here the layout of @{ML test_str} is much more pleasing to the + −
eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no hanging + −
indentation of the printed string. You can increase the indentation + −
and obtain+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs = map Pretty.str (space_explode \" \" test_str)+ −
in+ −
pprint (Pretty.blk (3, Pretty.breaks ptrs))+ −
end"+ −
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar+ −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}+ −
+ −
where starting from the second line the indent is 3. If you want+ −
that every line starts with the same indent, you can use the+ −
function @{ML_ind indent in Pretty} as follows:+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs = map Pretty.str (space_explode \" \" test_str)+ −
in+ −
pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))+ −
end"+ −
" fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar+ −
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}+ −
+ −
If you want to print out a list of items separated by commas and + −
have the linebreaks handled properly, you can use the function + −
@{ML_ind commas in Pretty}. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)+ −
in+ −
pprint (Pretty.blk (0, Pretty.commas ptrs))+ −
end"+ −
"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, + −
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, + −
100016, 100017, 100018, 100019, 100020"}+ −
+ −
where @{ML upto} generates a list of integers. You can print out this+ −
list as a ``set'', that means enclosed inside @{text [quotes] "{"} and+ −
@{text [quotes] "}"}, and separated by commas using the function+ −
@{ML_ind enum in Pretty}. For example+ −
*}+ −
+ −
text {*+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)+ −
in+ −
pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)+ −
end"+ −
"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, + −
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, + −
100016, 100017, 100018, 100019, 100020}"}+ −
+ −
As can be seen, this function prints out the ``set'' so that starting + −
from the second, each new line has an indentation of 2.+ −
+ −
If you print out something that goes beyond the capabilities of the+ −
standard functions, you can do relatively easily the formatting+ −
yourself. Assume you want to print out a list of items where like in ``English''+ −
the last two items are separated by @{text [quotes] "and"}. For this you can+ −
write the function+ −
+ −
*}+ −
+ −
ML %linenosgray{*fun and_list [] = []+ −
| and_list [x] = [x]+ −
| and_list xs = + −
let + −
val (front, last) = split_last xs+ −
in+ −
(Pretty.commas front) @ + −
[Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]+ −
end *}+ −
+ −
text {*+ −
where Line 7 prints the beginning of the list and Line+ −
8 the last item. We have to use @{ML "Pretty.brk 1"} in order+ −
to insert a space (of length 1) before the + −
@{text [quotes] "and"}. This space is also a place where a line break + −
can occur. We do the same after the @{text [quotes] "and"}. This gives you+ −
for example+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)+ −
val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)+ −
in+ −
pprint (Pretty.blk (0, and_list ptrs1));+ −
pprint (Pretty.blk (0, and_list ptrs2))+ −
end"+ −
"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 + −
and 22+ −
10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and+ −
28"}+ −
+ −
Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out + −
a list of items, but automatically inserts forced breaks between each item.+ −
Compare+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]+ −
in+ −
pprint (Pretty.blk (0, a_and_b));+ −
pprint (Pretty.chunks a_and_b)+ −
end"+ −
"ab+ −
a+ −
b"}+ −
+ −
The function @{ML_ind big_list in Pretty} helps with printing long lists.+ −
It is used for example in the command \isacommand{print\_theorems}. An+ −
example is as follows.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val pstrs = map (Pretty.str o string_of_int) (4 upto 10)+ −
in+ −
pprint (Pretty.big_list \"header\" pstrs)+ −
end"+ −
"header+ −
4+ −
5+ −
6+ −
7+ −
8+ −
9+ −
10"}+ −
+ −
The point of the pretty-printing functions is to conveninetly obtain + −
a lay-out of terms and types that is pleasing to the eye. If we print+ −
out the the terms produced by the the function @{ML de_bruijn} from + −
exercise~\ref{ex:debruijn} we obtain the following: + −
+ −
@{ML_response_fake [display,gray]+ −
"pprint (Syntax.pretty_term @{context} (de_bruijn 4))"+ −
"(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>+ −
(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>+ −
(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and> + −
(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>+ −
P 4 \<and> P 3 \<and> P 2 \<and> P 1"}+ −
+ −
We use the function @{ML_ind pretty_term in Syntax} for pretty-printing+ −
terms. Next we like to pretty-print a term and its type. For this we use the+ −
function @{text "tell_type"}.+ −
*}+ −
+ −
ML %linenosgray{*fun tell_type ctxt trm = + −
let+ −
fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))+ −
val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm)+ −
val pty = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm))+ −
in+ −
pprint (Pretty.blk (0, + −
(pstr "The term " @ [ptrm] @ pstr " has type " + −
@ [pty, Pretty.str "."])))+ −
end*}+ −
+ −
text {*+ −
In Line 3 we define a function that inserts possible linebreaks in places+ −
where a space is. In Lines 4 and 5 we pretty-print the term and its type+ −
using the functions @{ML pretty_term in Syntax} and @{ML_ind + −
pretty_typ in Syntax}. We also use the function @{ML_ind quote in+ −
Pretty} in order to enclose the term and type inside quotation marks. In+ −
Line 9 we add a period right after the type without the possibility of a+ −
line break, because we do not want that a line break occurs there.+ −
Now you can write+ −
+ −
@{ML_response_fake [display,gray]+ −
"tell_type @{context} @{term \"min (Suc 0)\"}"+ −
"The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}+ −
+ −
To see the proper line breaking, you can try out the function on a bigger term + −
and type. For example:+ −
+ −
@{ML_response_fake [display,gray]+ −
"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"+ −
"The term \"op = (op = (op = (op = (op = op =))))\" has type + −
\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}+ −
+ −
\begin{readmore}+ −
The general infrastructure for pretty-printing is implemented in the file+ −
@{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}+ −
contains pretty-printing functions for terms, types, theorems and so on.+ −
+ −
@{ML_file "Pure/General/markup.ML"}+ −
\end{readmore}+ −
*}+ −
+ −
section {* Summary *}+ −
+ −
text {*+ −
\begin{conventions}+ −
\begin{itemize}+ −
\item Start with a proper context and then pass it around + −
through all your functions.+ −
\end{itemize}+ −
\end{conventions}+ −
*}+ −
+ −
end+ −