--- 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) *}
--- a/ProgTutorial/Intro.thy Sat Nov 05 18:44:28 2011 +0000
+++ b/ProgTutorial/Intro.thy Sun Nov 06 15:15:59 2011 +0000
@@ -221,36 +221,31 @@
of many developers. Therefore, disruptions that break the work of others
are generally frowned upon. ``Accidents'' however do happen and everybody knows
this. Still to keep them to a minimum, you can submit your changes first to a rather
- sophisticated \emph{testboard}, which will perform checks of your changes agains the
+ sophisticated \emph{testboard}, which will perform checks of your changes against the
Isabelle repository and against the AFP. The advantage of the testboard is
that the testing is performed by rather powerful machines, saving you lengthy
- tests on, for example, your laptop. You can see the results of the testboard
+ tests on, for example, your own laptop. You can see the results of the testboard
at
- \begin{isabelle}
- ??
- \end{isabelle}
+ \begin{center}
+ \url{http://isabelle.in.tum.de/testboard/Isabelle/}
+ \end{center}
which is organised like a Mercurial repository. A green point next to a change
indicates that the change passes the corresponding tests (for this of course you
- have to allow some time). To facilitate the use of the testboard you should add
+ have to allow some time). You can summit any changes to the testboard using the
+ command
- \begin{isabelle}
- \begin{tabular}{@ {}l}
- @{text "[path]"}\\
- @{text "testboard = "}
- \end{tabular}
- \end{isabelle}
+ @{text [display] "$ hg push -f ssh://...@macbroy21.informatik.tu-muenchen.de\\
+ //home/isabelle-repository/repos/testboard"}
- to your Mercurial settings file. Then you can test any changes using the command
-
- @{text [display] "$ hg push -f testboard"}
-
- Note that for pushing changes to the testboard you need to add the option @{text "-f"},
- which however should \emph{never} be used with the main Isabelle repository. While
- the testboard is a great system for supporting Isabelle developers, its
- disadvantage is that it needs login permissions for the computers in Munich. So in order
- to use it, you might have to ask other developers.
+ where the dots need to be replaced by your login name. Note that for
+ pushing changes to the testboard you need to add the option @{text "-f"},
+ which however should \emph{never} be used with the main Isabelle
+ repository. While the testboard is a great system for supporting Isabelle
+ developers, its disadvantage is that it needs login permissions for the
+ computers in Munich. So in order to use it, you might have to ask other
+ developers to obtain one.
*}