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.
*}

section {* Theories\label{sec:theories} (TBD) *}

text {*
  Theories, as said above, are the most basic layer 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 theory can be queried 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}

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

ML_command "ProofContext.debug := true"
ML_command "ProofContext.verbose := true"


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

(*
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 {* 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 "ProofContext.extern_const"} or
  @{ML_ind  Long_Name.base_name}. For example:

  @{ML_response [display,gray] "ProofContext.extern_const @{context} \"List.list.Nil\"" "\"Nil\""}

  The difference between both functions is that @{ML extern_const in ProofContext} returns
  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
  strips off all qualifiers.

  \begin{readmore}
  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
  functions about signatures in @{ML_file "Pure/sign.ML"}.
  \end{readmore}
*}

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