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

    35 section {* Theories and Setups\label{sec:theories} *}

    36 

    36 

    37 text {*

    37 text {*

    38   Theories, as said above, are the most basic layer in Isabelle. They contain

    38   Theories, as said above, are the most basic layer of abstraction in

    39   definitions, syntax declarations, axioms, proofs etc. If a definition is

    39   Isabelle. They contain definitions, syntax declarations, axioms, proofs

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

    40   and much more. If a definition is made, it must be stored in a theory in order to be

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

    41   usable later on. Similar with proofs: once a proof is finished, the proved

    42   to be stored in the theorem database of the theory in order to be

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

    43   usable. All relevant data of a theory can be queried as follows.

    43   be usable. All relevant data of a theory can be queried as follows.

    61 

    61   In the context ML-programming, the most important command with theories

    62 

    62   is \isacommand{setup}. In the previous chapters we used it, for

    63   \begin{center}

    63   example, to make a theorem attribute known to Isabelle or to register a theorem

    64   \begin{tikzpicture}

    64   under a name. What happens behind the scenes is that \isacommand{setup}

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

    65   expects a function of type @{ML_type "theory -> theory"}: the input theory

    66   \end{tikzpicture}

    66   is the current theory and the output the theory where the attribute has been

    67   \end{center}

    67   registered or the theorem has been stored.  This is a fundamental principle

    68 

    68   in Isabelle. A similar situation arises with declaring constants. The

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

    69   function that declares a constant on the ML-level is @{ML_ind declare_const

    70   exponential blowups.}

    70   in Sign} in the structure @{ML_struct Sign}. To see how \isacommand{setup}

    71 *}

    71   works, consider the following code: 

    72 

    73 section {* Setups (TBD) *}

    74 

    75 text {*

    76   In the previous section we used \isacommand{setup} in order, for example, 

    77   to make a theorem attribute known to Isabelle or register a theorem under

    78   a name. What happens behind the scenes is that \isacommand{setup} expects a 

    79   function of type @{ML_type "theory -> theory"}: the input theory is the current

    80   theory and the output the theory where the theory attribute or theorem has been

    81   stored.

    82 

    83   This is a fundamental principle in Isabelle. A similar situation arises

    84   with declaring constants. The function that declares a 

    85   constant on the ML-level is @{ML_ind  declare_const in Sign}. 

    86   However, note that if you simply write\footnote{Recall that ML-code  needs to be 

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

    98   with the intention of declaring the constant @{text "BAR"} with type @{typ nat} 

    82   If you simply write this code\footnote{Recall that ML-code needs to be enclosed in

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

    83   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the

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

    84   intention of declaring a constant @{text "BAR"} with type @{typ nat} and run

    85   the code, then indeed you obtain a theory as result. But if you query the

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

   114 setup %gray {* let

   100 setup %gray {* fn thy => 

   101 let

   117   Sign.declare_const @{context} bar_const #> snd 

   105   thy'

   121   where the declaration is actually applied to the theory and

   109   where the declaration is actually applied to the current theory and

   128   returns a (black) constant with the type @{typ nat}, as expected.

   116   returns now a (black) constant with the type @{typ nat}, as expected.

   132   means that we have to be careful to apply operations always to the current

   120   means that we have to be careful to apply operations always to the most current

   133   theory, not to a \emph{stale} one. The code below produces

   121   theory, not to a \emph{stale} one. Consider again the function inside the

   134 

   122   \isacommand{setup}-command:

   135 

   123 

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

   124   \begin{isabelle}

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

   125   \begin{graybox}

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

   126   \isacommand{setup}~@{text "\<verbopen>"} @{ML

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

   127 "fn thy => 

   140   the current simpset.

   128 let

   129   val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)

   130   val (_, thy') = Sign.declare_const @{context} bar_const thy

   131 in

   132   thy

   133 end"}~@{text "\<verbclose>"}\isanewline

   134   @{text "> ERROR \"Stale theory encountered\""}

   135   \end{graybox}

   136   \end{isabelle}

   137 

   138   This time we erroneously return the original theory @{text thy}, instead of

   139   the modified one @{text thy'}. Such programming errors with handling the

   140   most current theory will always result into stale theory error messages.

   141 

   142   However, sometimes it does make sense to work with two theories at the same

   143   time, especially in the context of parsing and typing. In the code below we

   144   use in Line 3 the function @{ML_ind copy in Theory} from the structure

   145   @{ML_struct Theory} for obtaining a new theory that contains the same

   146   data, but is unrelated to the existing theory.

   147 *}

   148 

   149 setup %graylinenos {* fn thy => 

   150 let

   151   val tmp_thy = Theory.copy thy

   152   val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)

   153   val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy

   154   val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"

   155   val trm2 = Syntax.read_term_global thy "FOO baz"

   156   val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)

   157 in

   158   thy

   159 end *}

   160 

   161 text {*

   162   That means we can make changes to the theory @{text tmp_thy} without

   163   affecting the current theory @{text thy}. In this case we declare in @{text

   164   "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code

   165   is that we next, in Lines 6 and 7, parse a string to become a term (both

   166   times the string is @{text [quotes] "FOO baz"}). But since we parse the string

   167   once in the context of the theory @{text tmp_thy'} in which @{text FOO} is

   168   declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context 

   169   of @{text thy}, we obtain two different terms, namely 

   170 

   171   \begin{isabelle}

   172   \begin{graybox}

   173   @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline

   174   @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}

   175   \end{graybox}

   176   \end{isabelle}

   177 

   178   There are two reasons for parsing a term in a temporary theory. One is to

   179   obtain fully qualified names and the other is appropriate type inference.

   180   This is relevant in situations where definitions are made later, but parsing

   181   and type inference has to take already proceed as if the definitions were

   182   already made.

   145 ML{*Proof_Context.debug*}

   187 text {*

   146 ML{*Proof_Context.verbose*}

   188   Contexts are arguably more important than theories, even though they only 

   189   contain ``short-term memory data''. The reason is that a vast number of

   190   functions in Isabelle depend one way or the other on contexts. Even such

   191   mundane operation like printing out a term make essential use of contexts.

   192 *}

   193 

   194 (*

   195 ML{*Proof_Context.debug := true*}

   196 ML{*Proof_Context.verbose := true*}

   197 *)

   198 

   199 lemma "True"

   200 proof -

   201   { -- "\<And>x. _"

   202     fix x

   203     have "B x" sorry

   204     thm this

   205   }

   206 

   207   thm this

   208 

   209   { -- "A \<Longrightarrow> _"

   210     assume A

   211     have B sorry

   212     thm this

   213   }

   214    

   215   thm this

   216 

   217   { -- "\<And>x. x = _ \<Longrightarrow> _"

   218     def x \<equiv> a

   219     have "B x" sorry

   220   }

   221 

   222   thm this

   223 

   224 oops

   162 *}

   240 

   163 

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

   164 (*

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

   165 setup {*

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

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

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

   167 *}

   245   the current simpset.

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

   246 *}

   169   oops

   247 

   170 

   171 setup {*   

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

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

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

   175  #> snd

   176 *}

   177 *)

   178 (*

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

   180   apply(simp add: foo_def)

   181   done

   182 

   183 thm foo_def

   184 *)