theory Advancedimports Base FirstStepsbegin(*<*)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)" oopssetup {* 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) donethm 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