--- a/ProgTutorial/Advanced.thy Sat Nov 21 00:29:43 2009 +0100
+++ b/ProgTutorial/Advanced.thy Sun Nov 22 03:13:29 2009 +0100
@@ -14,18 +14,27 @@
chapter {* Advanced Isabelle *}
text {*
- TBD
+ While terms, types and theorems are the most basic data structures in
+ Isabelle, there are a number of layers built on top of them. Most of these
+ layers are concerned with storing and manipulating data. Handling
+ them properly is an essential skill for Isabelle programming. The most basic
+ layer are theories. They contain global data and can be seen as the
+ ``long-term memory'' of Isabelle. There is usually only one theory
+ active at each moment. Proof contexts and local theories, on the
+ other hand, store local data for a task at hand. They act like the
+ ``short-term memory'' and there can be many of them that are active
+ in parallel.
*}
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.
+ As said above, theories 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.
\begin{isabelle}
\isacommand{print\_theory}\\
@@ -43,23 +52,14 @@
@{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.}
*}
@@ -124,6 +124,15 @@
section {* Local Theories (TBD) *}
text {*
+ 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"}
@{ML_ind "Local_Theory.declaration"}
*}
--- a/ProgTutorial/Essential.thy Sat Nov 21 00:29:43 2009 +0100
+++ b/ProgTutorial/Essential.thy Sun Nov 22 03:13:29 2009 +0100
@@ -1169,7 +1169,8 @@
complete typing annotations, especially in cases where the typing
information is redundant. A short-cut is to use the ``place-holder''
type @{ML_ind dummyT in Term} and then let type-inference figure out the
- complete type. An example is as follows:
+ complete type. The type inference can be invoked with the function
+ @{ML_ind check_term in Syntax}. An example is as follows:
@{ML_response_fake [display,gray]
"let
@@ -1325,7 +1326,7 @@
|> implies_intr assm1
end*}
-text {*
+text {*
If we print out the value of @{ML my_thm} then we see only the
final statement of the theorem.
@@ -1424,8 +1425,6 @@
fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
text {*
- \footnote{\bf explain @{ML_ind add_thm in Thm} and @{ML_ind eq_thm_prop in Thm}.}
-
The function @{ML update} allows us to update the theorem list, for example
by adding the theorem @{thm [source] TrueI}.
*}
@@ -1466,10 +1465,18 @@
@{text "> True"}
\end{isabelle}
- There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule}
- for managing or manipulating theorems. For example
- we can test theorems for alpha equality. Suppose you proved the following three
- theorems.
+ Note that if we add the theorem @{thm [source] FalseE} again to the list
+*}
+
+setup %gray {* update @{thm FalseE} *}
+
+text {*
+ we still obtain the same list. The reason is that we used the function @{ML_ind
+ add_thm in Thm} in our update function. This is a dedicated function which
+ tests whether the theorem is already in the list. This test is done
+ according to alpha-equivalence of the proposition behind the theorem. The
+ corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
+ Suppose you proved the following three theorems.
*}
lemma
@@ -1478,11 +1485,11 @@
and thm3: "\<forall>y. Q y" sorry
text {*
- Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces:
+ Testing them for alpha equality produces:
@{ML_response [display,gray]
-"(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
- Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
+"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
+ Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
"(true, false)"}
Many functions destruct theorems into @{ML_type cterm}s. For example
@@ -1746,7 +1753,7 @@
install this function as the theorem style named @{text "my_strip_allq"}.
*}
-setup %gray {*
+setup %gray{*
Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq))
*}
@@ -1771,7 +1778,7 @@
\begin{isabelle}
@{text "@{thm (my_strip_allq) style_test}"}\\
- @{text ">"}~@{thm (my_strip_allq) style_test}\\
+ @{text ">"}~@{thm (my_strip_allq) style_test}
\end{isabelle}
without the leading quantifiers. We can improve this theorem style by explicitly
--- a/ProgTutorial/FirstSteps.thy Sat Nov 21 00:29:43 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Sun Nov 22 03:13:29 2009 +0100
@@ -838,7 +838,7 @@
theorem lists; see Section \ref{sec:storing}).
It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
- whose first argument is a statement (possibly many of them separated by @{text "and"},
+ whose first argument is a statement (possibly many of them separated by @{text "and"})
and the second is a proof. For example
*}
Binary file progtutorial.pdf has changed