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 {* Summary *}+
−
+
−
text {*+
−
  TBD+
−
*}+
−
+
−
end+
−