--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Advanced.thy Thu Nov 19 17:48:44 2009 +0100
@@ -0,0 +1,236 @@
+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