theory Advanced+ −
imports Base FirstSteps+ −
begin+ −
+ −
(*<*)+ −
setup{*+ −
open_file_with_prelude + −
"Advanced_Code.thy"+ −
["theory General", "imports Base FirstSteps", "begin"]+ −
*}+ −
(*>*)+ −
+ −
+ −
chapter {* Advanced Isabelle *}+ −
+ −
text {*+ −
TBD+ −
*}+ −
+ −
section {* Theories\label{sec:theories} (TBD) *}+ −
+ −
text {*+ −
Theories are the most fundamental building blocks in Isabelle. They + −
contain definitions, syntax declarations, axioms, proofs etc. If a definition+ −
is stated, it must be stored in a theory in order to be usable later+ −
on. Similar with proofs: once a proof is finished, the proved theorem+ −
needs to be stored in the theorem database of the theory in order to+ −
be usable. All relevant data of a theort can be querried as follows.+ −
+ −
\begin{isabelle}+ −
\isacommand{print\_theory}\\+ −
@{text "> names: Pure Code_Generator HOL \<dots>"}\\+ −
@{text "> classes: Inf < type \<dots>"}\\+ −
@{text "> default sort: type"}\\+ −
@{text "> syntactic types: #prop \<dots>"}\\+ −
@{text "> logical types: 'a \<times> 'b \<dots>"}\\+ −
@{text "> type arities: * :: (random, random) random \<dots>"}\\+ −
@{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\+ −
@{text "> abbreviations: \<dots>"}\\+ −
@{text "> axioms: \<dots>"}\\+ −
@{text "> oracles: \<dots>"}\\+ −
@{text "> definitions: \<dots>"}\\+ −
@{text "> theorems: \<dots>"}+ −
\end{isabelle}+ −
+ −
\begin{center}+ −
\begin{tikzpicture}+ −
\node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
+ −
In contrast to an ordinary theory, which simply consists of a type+ −
signature, as well as tables for constants, axioms and theorems, a local+ −
theory contains additional context information, such as locally fixed+ −
variables and local assumptions that may be used by the package. The type+ −
@{ML_type local_theory} is identical to the type of \emph{proof contexts}+ −
@{ML_type "Proof.context"}, although not every proof context constitutes a+ −
valid local theory.+ −
+ −
@{ML "Context.>> o Context.map_theory"}+ −
+ −
\footnote{\bf FIXME: list append in merge operations can cause + −
exponential blowups.}+ −
*}+ −
+ −
section {* Setups (TBD) *}+ −
+ −
text {*+ −
@{ML Sign.declare_const}+ −
+ −
In the previous section we used \isacommand{setup} in order to make+ −
a theorem attribute known to Isabelle. What happens behind the scenes+ −
is that \isacommand{setup} expects a function of type + −
@{ML_type "theory -> theory"}: the input theory is the current theory and the + −
output the theory where the theory attribute has been stored.+ −
+ −
This is a fundamental principle in Isabelle. A similar situation occurs + −
for example with declaring constants. The function that declares a + −
constant on the ML-level is @{ML_ind add_consts_i in Sign}. + −
If you write\footnote{Recall that ML-code needs to be + −
enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} + −
*} + −
+ −
ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}+ −
+ −
text {*+ −
for declaring the constant @{text "BAR"} with type @{typ nat} and + −
run the code, then you indeed obtain a theory as result. But if you + −
query the constant on the Isabelle level using the command \isacommand{term}+ −
+ −
\begin{isabelle}+ −
\isacommand{term}~@{text [quotes] "BAR"}\\+ −
@{text "> \"BAR\" :: \"'a\""}+ −
\end{isabelle}+ −
+ −
you do not obtain a constant of type @{typ nat}, but a free variable (printed in + −
blue) of polymorphic type. The problem is that the ML-expression above did + −
not register the declaration with the current theory. This is what the command+ −
\isacommand{setup} is for. The constant is properly declared with+ −
*}+ −
+ −
setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}+ −
+ −
text {* + −
Now + −
+ −
\begin{isabelle}+ −
\isacommand{term}~@{text [quotes] "BAR"}\\+ −
@{text "> \"BAR\" :: \"nat\""}+ −
\end{isabelle}+ −
+ −
returns a (black) constant with the type @{typ nat}.+ −
+ −
A similar command is \isacommand{local\_setup}, which expects a function+ −
of type @{ML_type "local_theory -> local_theory"}. Later on we will also+ −
use the commands \isacommand{method\_setup} for installing methods in the+ −
current theory and \isacommand{simproc\_setup} for adding new simprocs to+ −
the current simpset.+ −
*}+ −
+ −
section {* Contexts (TBD) *}+ −
+ −
section {* Local Theories (TBD) *}+ −
+ −
text {*+ −
@{ML_ind "Local_Theory.declaration"}+ −
*}+ −
+ −
(*+ −
setup {*+ −
Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] + −
*}+ −
lemma "bar = (1::nat)"+ −
oops+ −
+ −
setup {* + −
Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] + −
#> PureThy.add_defs false [((@{binding "foo_def"}, + −
Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] + −
#> snd+ −
*}+ −
*)+ −
(*+ −
lemma "foo = (1::nat)"+ −
apply(simp add: foo_def)+ −
done+ −
+ −
thm foo_def+ −
*)+ −
+ −
section {* Morphisms (TBD) *}+ −
+ −
text {*+ −
Morphisms are arbitrary transformations over terms, types, theorems and bindings.+ −
They can be constructed using the function @{ML_ind morphism in Morphism},+ −
which expects a record with functions of type+ −
+ −
\begin{isabelle}+ −
\begin{tabular}{rl}+ −
@{text "binding:"} & @{text "binding -> binding"}\\+ −
@{text "typ:"} & @{text "typ -> typ"}\\+ −
@{text "term:"} & @{text "term -> term"}\\+ −
@{text "fact:"} & @{text "thm list -> thm list"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as+ −
*}+ −
+ −
ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}+ −
+ −
text {*+ −
Morphisms can be composed with the function @{ML_ind "$>" in Morphism}+ −
*}+ −
+ −
ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) + −
| trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)+ −
| trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)+ −
| trm_phi t = t*}+ −
+ −
ML{*val phi = Morphism.term_morphism trm_phi*}+ −
+ −
ML{*Morphism.term phi @{term "P x y"}*}+ −
+ −
text {*+ −
@{ML_ind term_morphism in Morphism}+ −
+ −
@{ML_ind term in Morphism},+ −
@{ML_ind thm in Morphism}+ −
+ −
\begin{readmore}+ −
Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Misc (TBD) *}+ −
+ −
ML {*Datatype.get_info @{theory} "List.list"*}+ −
+ −
text {* + −
FIXME: association lists:+ −
@{ML_file "Pure/General/alist.ML"}+ −
+ −
FIXME: calling the ML-compiler+ −
+ −
*}+ −
+ −
section {* Managing Name Spaces (TBD) *}+ −
+ −
ML {* Sign.intern_type @{theory} "list" *}+ −
ML {* Sign.intern_const @{theory} "prod_fun" *}+ −
+ −
+ −
text {* + −
@{ML_ind "Binding.str_of"} returns the string with markup;+ −
@{ML_ind "Binding.name_of"} returns the string without markup+ −
+ −
@{ML_ind "Binding.conceal"} + −
*}+ −
+ −
section {* Concurrency (TBD) *}+ −
+ −
text {*+ −
@{ML_ind prove_future in Goal}+ −
@{ML_ind future_result in Goal}+ −
@{ML_ind fork_pri in Future}+ −
*}+ −
+ −
section {* Parse and Print Translations (TBD) *}+ −
+ −
section {* Summary *}+ −
+ −
text {*+ −
TBD+ −
*}+ −
+ −
end+ −