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

  programming. 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.

*}

text {*

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

*}  

ML{*let

  val thy = @{theory}

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

in 

  Sign.declare_const @{context} bar_const thy  

end*}

text {*

  \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

*}

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

in 

end *}

text {* 

  \begin{isabelle}

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

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

  \end{isabelle}

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

  current theory, applies an operation, and produces a new current theory. This

*}

section {* Contexts (TBD) *}

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

*}

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