theory Advanced

imports Base First_Steps

begin

(*<*)

setup{*

open_file_with_prelude 

  "Advanced_Code.thy"

  ["theory Advanced", "imports Base First_Steps", "begin"]

*}

(*>*)

chapter {* Advanced Isabelle\label{chp:advanced} *}

text {*

   \begin{flushright}

  {\em All things are difficult before they are easy.} \\[1ex]

  proverb

  \end{flushright}

  \medskip

  While terms, types and theorems are the most basic data structures in

  Isabelle, there are a number of layers built on top of them. Most of these

  layers are concerned with storing and manipulating data. Handling them

  properly is an essential skill for programming on the ML-level of Isabelle. 

  The most basic layer are theories. They contain global data and

  can be seen as the ``long-term memory'' of Isabelle. There is usually only

  one theory active at each moment. Proof contexts and local theories, on the

  other hand, store local data for a task at hand. They act like the

  ``short-term memory'' and there can be many of them that are active in

  parallel.

*}

section {* Theories and Setups\label{sec:theories} *}

text {*

  Theories, as said above, are the most basic layer of abstraction in

  Isabelle. They record information about definitions, syntax declarations, axioms,

  theorems and much more.  For example, if a definition is made, 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 theory can be queried with the

  Isabelle command \isacommand{print\_theory}.

  \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}

  Functions acting on theories often end with the suffix @{text "_global"},

  for example the function @{ML read_term_global in Syntax} in the structure

  @{ML_struct Syntax}. The reason is to set them syntactically apart from

  functions acting on contexts or local theories, which will be discussed in

  the next sections. There is a tendency amongst Isabelle developers to prefer

  ``non-global'' operations, because they have some advantages, as we will also

  discuss later. However, some basic understanding of theories is still necessary

  for effective Isabelle programming.

  An important Isabelle command with theories is \isacommand{setup}. In the

  previous chapters we used it already to make a theorem attribute known

  to Isabelle and to register a theorem under a name. 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 attribute has been registered or the theorem has been

  stored.  This is a fundamental principle in Isabelle. A similar situation

  arises with declaring a constant, which can be done on the ML-level with 

  function @{ML_ind declare_const in Sign} from the structure @{ML_struct

  Sign}. To see how \isacommand{setup} works, consider the following code:

*}  

ML{*let

  val thy = @{theory}

  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)

in 

  Sign.declare_const @{context} bar_const thy  

end*}

text {*

  If you simply run this code\footnote{Recall that ML-code needs to be enclosed in

  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the

  intention of declaring a constant @{text "BAR"} having type @{typ nat}, then 

  indeed you 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 BAR}\\

  @{text "> \"BAR\" :: \"'a\""}

  \end{isabelle}

  you can see that you do \emph{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 {* fn thy => 

let

  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)

  val (_, thy') = Sign.declare_const @{context} bar_const thy

in 

  thy'

end *}

text {* 

  where the declaration is actually applied to the current theory and

  \begin{isabelle}

  \isacommand{term}~@{text [quotes] "BAR"}\\

  @{text "> \"BAR\" :: \"nat\""}

  \end{isabelle}

  now returns a (black) constant with the type @{typ nat}, as expected.

  In a sense, \isacommand{setup} can be seen as a transaction that

  takes the current theory @{text thy}, applies an operation, and

  produces a new current theory @{text thy'}. This means that we have

  to be careful to apply operations always to the most current theory,

  not to a \emph{stale} one. Consider again the function inside the

  \isacommand{setup}-command:

  \begin{isabelle}

  \begin{graybox}

  \isacommand{setup}~@{text "\<verbopen>"} @{ML

"fn thy => 

let

  val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)

  val (_, thy') = Sign.declare_const @{context} bar_const thy

in

  thy

end"}~@{text "\<verbclose>"}\isanewline

  @{text "> ERROR \"Stale theory encountered\""}

  \end{graybox}

  \end{isabelle}

  This time we erroneously return the original theory @{text thy}, instead of

  the modified one @{text thy'}. Such buggy code will always result into 

  a runtime error message about stale theories.

  However, sometimes it does make sense to work with two theories at the same

  time, especially in the context of parsing and typing. In the code below we

  use in Line 3 the function @{ML_ind copy in Theory} from the structure

  @{ML_struct Theory} for obtaining a new theory that contains the same

  data, but is unrelated to the existing theory.

*}

setup %graylinenos {* fn thy => 

let

  val tmp_thy = Theory.copy thy

  val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)

  val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy

  val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"

  val trm2 = Syntax.read_term_global thy "FOO baz"

  val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)

in

  thy

end *}

text {*

  That means we can make changes to the theory @{text tmp_thy} without

  affecting the current theory @{text thy}. In this case we declare in @{text

  "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code

  is that we next, in Lines 6 and 7, parse a string to become a term (both

  times the string is @{text [quotes] "FOO baz"}). But since we parse the string

  once in the context of the theory @{text tmp_thy'} in which @{text FOO} is

  declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context 

  of @{text thy} where it is not, we obtain two different terms, namely 

  \begin{isabelle}

  \begin{graybox}

  @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline

  @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}

  \end{graybox}

  \end{isabelle}

  There are two reasons for parsing a term in a temporary theory. One is to

  obtain fully qualified names for constants and the other is appropriate type 

  inference. This is relevant in situations where definitions are made later, 

  but parsing and type inference has to take already proceed as if the definitions 

  were already made.

*}

section {* Contexts (TBD) *}

text {*

  Contexts are arguably more important than theories, even though they only 

  contain ``short-term memory data''. The reason is that a vast number of

  functions in Isabelle depend in one way or another on contexts. Even such

  mundane operations like printing out a term make essential use of contexts.

  For this consider the following contrived proof-snippet whose only purpose is to 

  fix two variables:

*}

lemma "True"

proof -

  txt_raw {*\mbox{}\\[-7mm]*} 

  ML_prf {* Variable.dest_fixes @{context} *} 

  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}

 fix x y  

  txt_raw {*\mbox{}\\[-7mm]*}

  ML_prf {* Variable.dest_fixes @{context} *} 

  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)

text {*

  The interesting point in this proof is that we injected ML-code before and after

  the variables are fixed. For this remember that ML-code inside a proof

  needs to be enclosed in \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},

  not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function 

  @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes 

  a context and returns all its currently fixed variable (names). That 

  means a context has a dataslot containing information about fixed variables.

  The ML-antiquotation @{text "@{context}"} points to the context that is

  active at that point of the theory. Consequently, in the first call to 

  @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 

  filled with @{text x} and @{text y}. What is interesting is that contexts

  can be stacked. For this consider the following proof fragment

*}

lemma "True"

proof -

  fix x y

  { fix z w

  txt_raw {*\mbox{}\\[-7mm]*}

  ML_prf {* Variable.dest_fixes @{context} *} 

  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}

 }

  txt_raw {*\mbox{}\\[-7mm]*}

  ML_prf {* Variable.dest_fixes @{context} *} 

  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)

text {*

  The first time we call @{ML dest_fixes in Variable} we have four fixes variables;

  the second time we get only the fixes variables @{text x} and @{text y} as answer. 

  This means the curly-braces act as opening and closing statements for a context.

  The above proof corresoponds roughly to the following ML-code.

*}

ML{*val ctxt0 = @{context};

val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;

val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}

text {*

  Now let us come back to the point about printing terms.

*}

(*

ML{*Proof_Context.debug := true*}

ML{*Proof_Context.verbose := true*}

*)

(*

lemma "True"

proof -

  { -- "\<And>x. _"

    fix x

    have "B x" sorry

    thm this

  }

  thm this

  { -- "A \<Longrightarrow> _"

    assume A

    have B sorry

    thm this

  }

  thm this

  { -- "\<And>x. x = _ \<Longrightarrow> _"

    def x \<equiv> a

    have "B x" sorry

  }

  thm this

oops

*)

section {* Local Theories (TBD) *}

text {*

  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"}

  @{ML_ind "Local_Theory.declaration"}

   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 {* 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 = [], typ = [], term = [], fact = []}*}

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 {* What Is In an Isabelle Name? (TBD) *}

text {*

  On the ML-level of Isabelle, you often have to work with qualified names.

  These are strings with some additional information, such as positional

  information and qualifiers. Such qualified names can be generated with the

  antiquotation @{text "@{binding \<dots>}"}. For example

  @{ML_response [display,gray]

  "@{binding \"name\"}"

  "name"}

  An example where a qualified name is needed is the function 

  @{ML_ind define in Local_Theory}.  This function is used below to define 

  the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.

*}

local_setup %gray {* 

  Local_Theory.define ((@{binding "TrueConj"}, NoSyn), 

      (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}

text {* 

  Now querying the definition you obtain:

  \begin{isabelle}

  \isacommand{thm}~@{text "TrueConj_def"}\\

  @{text "> "}~@{thm TrueConj_def}

  \end{isabelle}

  \begin{readmore}

  The basic operations on bindings are implemented in 

  @{ML_file "Pure/General/binding.ML"}.

  \end{readmore}

  \footnote{\bf FIXME give a better example why bindings are important}

  \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain

  why @{ML snd} is needed.}

  \footnote{\bf FIXME: There should probably a separate section on binding, long-names

  and sign.}

*}

ML {* Sign.intern_type @{theory} "list" *}

ML {* Sign.intern_const @{theory} "prod_fun" *}

text {*

  \footnote{\bf FIXME: Explain the following better; maybe put in a separate

  section and link with the comment in the antiquotation section.}

  Occasionally you have to calculate what the ``base'' name of a given

  constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:

  @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}

  \begin{readmore}

  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

  functions about signatures in @{ML_file "Pure/sign.ML"}.

  \end{readmore}

*}

text {* 

  @{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