1 theory Advanced

     2 imports Base FirstSteps

     3 begin

     4 

     5 (*<*)

     6 setup{*

     7 open_file_with_prelude 

     8   "Advanced_Code.thy"

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

    10 *}

    11 (*>*)

    12 

    13 

    14 chapter {* Advanced Isabelle *}

    15 

    16 text {*

    17   TBD

    18 *}

    19 

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

    21 

    22 text {*

    23   Theories are the most fundamental building blocks in Isabelle. They 

    24   contain definitions, syntax declarations, axioms, proofs etc. If a definition

    25   is stated, it must be stored in a theory in order to be usable later

    26   on. Similar with proofs: once a proof is finished, the proved theorem

    27   needs to be stored in the theorem database of the theory in order to

    28   be usable. All relevant data of a theort can be querried as follows.

    29 

    30   \begin{isabelle}

    31   \isacommand{print\_theory}\\

    32   @{text "> names: Pure Code_Generator HOL \<dots>"}\\

    33   @{text "> classes: Inf < type \<dots>"}\\

    34   @{text "> default sort: type"}\\

    35   @{text "> syntactic types: #prop \<dots>"}\\

    36   @{text "> logical types: 'a \<times> 'b \<dots>"}\\

    37   @{text "> type arities: * :: (random, random) random \<dots>"}\\

    38   @{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\

    39   @{text "> abbreviations: \<dots>"}\\

    40   @{text "> axioms: \<dots>"}\\

    41   @{text "> oracles: \<dots>"}\\

    42   @{text "> definitions: \<dots>"}\\

    43   @{text "> theorems: \<dots>"}

    44   \end{isabelle}

    45 

    46   \begin{center}

    47   \begin{tikzpicture}

    48   \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};

    49   \end{tikzpicture}

    50   \end{center}

    51 

    52 

    53   In contrast to an ordinary theory, which simply consists of a type

    54   signature, as well as tables for constants, axioms and theorems, a local

    55   theory contains additional context information, such as locally fixed

    56   variables and local assumptions that may be used by the package. The type

    57   @{ML_type local_theory} is identical to the type of \emph{proof contexts}

    58   @{ML_type "Proof.context"}, although not every proof context constitutes a

    59   valid local theory.

    60 

    61   @{ML "Context.>> o Context.map_theory"}

    62 

    63   \footnote{\bf FIXME: list append in merge operations can cause 

    64   exponential blowups.}

    65 *}

    66 

    67 section {* Setups (TBD) *}

    68 

    69 text {*

    70   @{ML Sign.declare_const}

    71 

    72   In the previous section we used \isacommand{setup} in order to make

    73   a theorem attribute known to Isabelle. What happens behind the scenes

    74   is that \isacommand{setup} expects a function of type 

    75   @{ML_type "theory -> theory"}: the input theory is the current theory and the 

    76   output the theory where the theory attribute has been stored.

    77   

    78   This is a fundamental principle in Isabelle. A similar situation occurs 

    79   for example with declaring constants. The function that declares a 

    80   constant on the ML-level is @{ML_ind  add_consts_i in Sign}. 

    81   If you write\footnote{Recall that ML-code  needs to be 

    82   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 

    83 *}  

    84 

    85 ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}

    86 

    87 text {*

    88   for declaring the constant @{text "BAR"} with type @{typ nat} and 

    89   run the code, then you indeed obtain a theory as result. But if you 

    90   query the constant on the Isabelle level using the command \isacommand{term}

    91 

    92   \begin{isabelle}

    93   \isacommand{term}~@{text [quotes] "BAR"}\\

    94   @{text "> \"BAR\" :: \"'a\""}

    95   \end{isabelle}

    96 

    97   you do not obtain a constant of type @{typ nat}, but a free variable (printed in 

    98   blue) of polymorphic type. The problem is that the ML-expression above did 

    99   not register the declaration with the current theory. This is what the command

   100   \isacommand{setup} is for. The constant is properly declared with

   101 *}

   102 

   103 setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}

   104 

   105 text {* 

   106   Now 

   107   

   108   \begin{isabelle}

   109   \isacommand{term}~@{text [quotes] "BAR"}\\

   110   @{text "> \"BAR\" :: \"nat\""}

   111   \end{isabelle}

   112 

   113   returns a (black) constant with the type @{typ nat}.

   114 

   115   A similar command is \isacommand{local\_setup}, which expects a function

   116   of type @{ML_type "local_theory -> local_theory"}. Later on we will also

   117   use the commands \isacommand{method\_setup} for installing methods in the

   118   current theory and \isacommand{simproc\_setup} for adding new simprocs to

   119   the current simpset.

   120 *}

   121 

   122 section {* Contexts (TBD) *}

   123 

   124 section {* Local Theories (TBD) *}

   125 

   126 text {*

   127   @{ML_ind "Local_Theory.declaration"}

   128 *}

   129 

   130 (*

   131 setup {*

   132  Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 

   133 *}

   134 lemma "bar = (1::nat)"

   135   oops

   136 

   137 setup {*   

   138   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 

   139  #> PureThy.add_defs false [((@{binding "foo_def"}, 

   140        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 

   141  #> snd

   142 *}

   143 *)

   144 (*

   145 lemma "foo = (1::nat)"

   146   apply(simp add: foo_def)

   147   done

   148 

   149 thm foo_def

   150 *)

   151 

   152 section {* Morphisms (TBD) *}

   153 

   154 text {*

   155   Morphisms are arbitrary transformations over terms, types, theorems and bindings.

   156   They can be constructed using the function @{ML_ind morphism in Morphism},

   157   which expects a record with functions of type

   158 

   159   \begin{isabelle}

   160   \begin{tabular}{rl}

   161   @{text "binding:"} & @{text "binding -> binding"}\\

   162   @{text "typ:"}     & @{text "typ -> typ"}\\

   163   @{text "term:"}    & @{text "term -> term"}\\

   164   @{text "fact:"}    & @{text "thm list -> thm list"}

   165   \end{tabular}

   166   \end{isabelle}

   167 

   168   The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as

   169 *}

   170 

   171 ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}

   172   

   173 text {*

   174   Morphisms can be composed with the function @{ML_ind "$>" in Morphism}

   175 *}

   176 

   177 ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) 

   178   | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)

   179   | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)

   180   | trm_phi t = t*}

   181 

   182 ML{*val phi = Morphism.term_morphism trm_phi*}

   183 

   184 ML{*Morphism.term phi @{term "P x y"}*}

   185 

   186 text {*

   187   @{ML_ind term_morphism in Morphism}

   188 

   189   @{ML_ind term in Morphism},

   190   @{ML_ind thm in Morphism}

   191 

   192   \begin{readmore}

   193   Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.

   194   \end{readmore}

   195 *}

   196 

   197 section {* Misc (TBD) *}

   198 

   199 ML {*Datatype.get_info @{theory} "List.list"*}

   200 

   201 text {* 

   202 FIXME: association lists:

   203 @{ML_file "Pure/General/alist.ML"}

   204 

   205 FIXME: calling the ML-compiler

   206 

   207 *}

   208 

   209 section {* Managing Name Spaces (TBD) *}

   210 

   211 ML {* Sign.intern_type @{theory} "list" *}

   212 ML {* Sign.intern_const @{theory} "prod_fun" *}

   213 

   214 

   215 text {* 

   216   @{ML_ind "Binding.str_of"} returns the string with markup;

   217   @{ML_ind "Binding.name_of"} returns the string without markup

   218 

   219   @{ML_ind "Binding.conceal"} 

   220 *}

   221 

   222 section {* Concurrency (TBD) *}

   223 

   224 text {*

   225   @{ML_ind prove_future in Goal}

   226   @{ML_ind future_result in Goal}

   227   @{ML_ind fork_pri in Future}

   228 *}

   229 

   230 section {* Summary *}

   231 

   232 text {*

   233   TBD

   234 *}

   235 

   236 end