--- a/ProgTutorial/Advanced.thy Sat Nov 05 18:44:28 2011 +0000
+++ b/ProgTutorial/Advanced.thy Sun Nov 06 15:15:59 2011 +0000
@@ -32,15 +32,15 @@
parallel.
*}
-section {* Theories\label{sec:theories} (TBD) *}
+section {* Theories and Setups\label{sec:theories} *}
text {*
- Theories, as said above, are the most basic layer 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 theory can be queried as follows.
+ Theories, as said above, are the most basic layer of abstraction in
+ Isabelle. They contain definitions, syntax declarations, axioms, proofs
+ and much more. If a definition is made, 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 theory can be queried as follows.
\begin{isabelle}
\isacommand{print\_theory}\\
@@ -58,33 +58,17 @@
@{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}
-
- \footnote{\bf FIXME: list append in merge operations can cause
- exponential blowups.}
-*}
-
-section {* Setups (TBD) *}
-
-text {*
- In the previous section we used \isacommand{setup} in order, for example,
- to make a theorem attribute known to Isabelle or register a theorem under
- a name. 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 or theorem has been
- stored.
-
- This is a fundamental principle in Isabelle. A similar situation arises
- with declaring constants. The function that declares a
- constant on the ML-level is @{ML_ind declare_const in Sign}.
- However, note that if you simply write\footnote{Recall that ML-code needs to be
- enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
+ In the context ML-programming, the most important command with theories
+ is \isacommand{setup}. In the previous chapters we used it, for
+ example, to make a theorem attribute known to Isabelle or to register a theorem
+ under a name. 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 attribute has been
+ registered or the theorem has been stored. This is a fundamental principle
+ in Isabelle. A similar situation arises with declaring constants. The
+ function that declares a constant on the ML-level is @{ML_ind declare_const
+ in Sign} in the structure @{ML_struct Sign}. To see how \isacommand{setup}
+ works, consider the following code:
*}
ML{*let
@@ -95,9 +79,11 @@
end*}
text {*
- with the intention of declaring the constant @{text "BAR"} with type @{typ nat}
- and run the code, then indeed you obtain a theory as result. But if you
- query the constant on the Isabelle level using the command \isacommand{term}
+ If you simply write this code\footnote{Recall that ML-code needs to be enclosed in
+ \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the
+ intention of declaring a constant @{text "BAR"} with type @{typ nat} and run
+ the code, then indeed you 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 BAR}\\
@@ -111,39 +97,131 @@
declared with
*}
-setup %gray {* let
+setup %gray {* fn thy =>
+let
val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
+ val (_, thy') = Sign.declare_const @{context} bar_const thy
in
- Sign.declare_const @{context} bar_const #> snd
+ thy'
end *}
text {*
- where the declaration is actually applied to the theory and
+ where the declaration is actually applied to the current theory and
\begin{isabelle}
\isacommand{term}~@{text [quotes] "BAR"}\\
@{text "> \"BAR\" :: \"nat\""}
\end{isabelle}
- returns a (black) constant with the type @{typ nat}, as expected.
+ returns now a (black) constant with the type @{typ nat}, as expected.
In a sense, \isacommand{setup} can be seen as a transaction that takes the
current theory, applies an operation, and produces a new current theory. This
- means that we have to be careful to apply operations always to the current
- theory, not to a \emph{stale} one. The code below produces
+ means that we have to be careful to apply operations always to the most current
+ theory, not to a \emph{stale} one. Consider again the function inside the
+ \isacommand{setup}-command:
+ \begin{isabelle}
+ \begin{graybox}
+ \isacommand{setup}~@{text "\<verbopen>"} @{ML
+"fn thy =>
+let
+ val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
+ val (_, thy') = Sign.declare_const @{context} bar_const thy
+in
+ thy
+end"}~@{text "\<verbclose>"}\isanewline
+ @{text "> ERROR \"Stale theory encountered\""}
+ \end{graybox}
+ \end{isabelle}
+
+ This time we erroneously return the original theory @{text thy}, instead of
+ the modified one @{text thy'}. Such programming errors with handling the
+ most current theory will always result into stale theory error messages.
+
+ However, sometimes it does make sense to work with two theories at the same
+ time, especially in the context of parsing and typing. In the code below we
+ use in Line 3 the function @{ML_ind copy in Theory} from the structure
+ @{ML_struct Theory} for obtaining a new theory that contains the same
+ data, but is unrelated to the existing theory.
+*}
- 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.
+setup %graylinenos {* fn thy =>
+let
+ val tmp_thy = Theory.copy thy
+ val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)
+ val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
+ val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
+ val trm2 = Syntax.read_term_global thy "FOO baz"
+ val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
+in
+ thy
+end *}
+
+text {*
+ That means we can make changes to the theory @{text tmp_thy} without
+ affecting the current theory @{text thy}. In this case we declare in @{text
+ "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code
+ is that we next, in Lines 6 and 7, parse a string to become a term (both
+ times the string is @{text [quotes] "FOO baz"}). But since we parse the string
+ once in the context of the theory @{text tmp_thy'} in which @{text FOO} is
+ declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context
+ of @{text thy}, we obtain two different terms, namely
+
+ \begin{isabelle}
+ \begin{graybox}
+ @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline
+ @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}
+ \end{graybox}
+ \end{isabelle}
+
+ There are two reasons for parsing a term in a temporary theory. One is to
+ obtain fully qualified names and the other is appropriate type inference.
+ This is relevant in situations where definitions are made later, but parsing
+ and type inference has to take already proceed as if the definitions were
+ already made.
*}
section {* Contexts (TBD) *}
-ML{*Proof_Context.debug*}
-ML{*Proof_Context.verbose*}
+text {*
+ Contexts are arguably more important than theories, even though they only
+ contain ``short-term memory data''. The reason is that a vast number of
+ functions in Isabelle depend one way or the other on contexts. Even such
+ mundane operation like printing out a term make essential use of contexts.
+*}
+
+(*
+ML{*Proof_Context.debug := true*}
+ML{*Proof_Context.verbose := true*}
+*)
+
+lemma "True"
+proof -
+ { -- "\<And>x. _"
+ fix x
+ have "B x" sorry
+ thm this
+ }
+
+ thm this
+
+ { -- "A \<Longrightarrow> _"
+ assume A
+ have B sorry
+ thm this
+ }
+
+ thm this
+
+ { -- "\<And>x. x = _ \<Longrightarrow> _"
+ def x \<equiv> a
+ have "B x" sorry
+ }
+
+ thm this
+
+oops
section {* Local Theories (TBD) *}
@@ -159,29 +237,14 @@
@{ML "Context.>> o Context.map_theory"}
@{ML_ind "Local_Theory.declaration"}
+
+ 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.
*}
-(*
-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) *}