theory Advanced

imports Base FirstSteps

begin

(*<*)

setup{*

open_file_with_prelude 

  "Advanced_Code.thy"

  ["theory General", "imports Base FirstSteps", "begin"]

*}

(*>*)

chapter {* Advanced Isabelle *}

text {*

*}

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

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}

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

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