--- a/src/HOL/Isar_examples/ROOT.ML Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/Isar_examples/ROOT.ML Thu Nov 08 23:50:08 2001 +0100
@@ -13,7 +13,9 @@
time_use_thy "Summation";
time_use_thy "KnasterTarski";
time_use_thy "MutilatedCheckerboard";
-with_path "../W0" time_use_thy "W_correct";
+with_path "../W0" (no_document time_use_thy) "Type";
+with_path "../W0" time_use_thy "W_correct";
+with_path "../NumberTheory" (no_document time_use_thy) "Primes";
with_path "../NumberTheory" time_use_thy "Fibonacci";
time_use_thy "Puzzle";
time_use_thy "NestedDatatype";
--- a/src/HOL/Isar_examples/document/root.tex Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/Isar_examples/document/root.tex Thu Nov 08 23:50:08 2001 +0100
@@ -13,36 +13,21 @@
\maketitle
\begin{abstract}
- Isar offers a high-level proof (and theory) language for Isabelle.
- We give various examples of Isabelle/Isar proof developments,
- ranging from simple demonstrations of certain language features to
- more advanced applications.
+ Isar offers a high-level proof (and theory) language for Isabelle. We give
+ various examples of Isabelle/Isar proof developments, ranging from simple
+ demonstrations of certain language features to a bit more advanced
+ applications. Note that the ``real'' applications of Isar are found
+ elsewhere.
\end{abstract}
\tableofcontents
\parindent 0pt \parskip 0.5ex
-\input{BasicLogic.tex}
-\input{Cantor.tex}
-\input{Peirce.tex}
-\input{ExprCompiler.tex}
-\input{Group.tex}
-\input{Summation.tex}
-\input{KnasterTarski.tex}
-\input{MutilatedCheckerboard.tex}
-%\input{Maybe.tex}
-%\input{Type.tex}
-\input{W_correct.tex}
-%\input{Primes.tex}
-\input{Fibonacci.tex}
-\input{Puzzle.tex}
-\input{NestedDatatype.tex}
-\input{Hoare.tex}
-\input{HoareEx.tex}
+\input{session}
\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
-\bibliographystyle{plain}
+\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
--- a/src/HOL/ex/Locales.thy Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/ex/Locales.thy Thu Nov 08 23:50:08 2001 +0100
@@ -9,12 +9,18 @@
theory Locales = Main:
text {*
- Locales provide a mechanism for encapsulating local contexts. While
- the original version by Florian Kamm\"uller refers to the raw
- meta-logic, the present one of Isabelle/Isar builds on top of the
- rich infrastructure of Isar proof contexts. Subsequently, we
- demonstrate basic use of locales to model mathematical structures
- (by the inevitable group theory example).
+ Locales provide a mechanism for encapsulating local contexts. The
+ original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
+ refers directly to the raw meta-logic of Isabelle. The present
+ version for Isabelle/Isar
+ \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on
+ top of the rich infrastructure of proof contexts instead; this also
+ covers essential extra-logical concepts like term abbreviations or
+ local theorem attributes (e.g.\ declarations of simplification
+ rules).
+
+ Subsequently, we demonstrate basic use of locales to model
+ mathematical structures (by the inevitable group theory example).
*}
text_raw {*
@@ -28,7 +34,7 @@
text {*
The following definitions of @{text group} and @{text abelian_group}
- simply encapsulate local parameters (with private syntax) and
+ merely encapsulate local parameters (with private syntax) and
assumptions; local definitions may be given as well, but are not
shown here.
*}
@@ -76,9 +82,9 @@
qed
text {*
- \medskip Apart from the named locale context we may also refer to
- further ad-hoc elements (parameters, assumptions, etc.); these are
- discharged when the proof is finished.
+ \medskip Apart from the named context we may also refer to further
+ context elements (parameters, assumptions, etc.) in a casual manner;
+ these are discharged when the proof is finished.
*}
theorem (in group)
@@ -119,10 +125,10 @@
qed
text {*
- \medskip Results are automatically propagated through the hierarchy
- of locales. Below we establish a trivial fact of commutative
- groups, while referring both to theorems of @{text group} and the
- characteristic assumption of @{text abelian_group}.
+ \medskip Established results are automatically propagated through
+ the hierarchy of locales. Below we establish a trivial fact in
+ commutative groups, while referring both to theorems of @{text
+ group} and the additional assumption of @{text abelian_group}.
*}
theorem (in abelian_group)
@@ -134,7 +140,8 @@
qed
text {*
- \medskip Some further facts of general group theory follow.
+ \medskip Some further properties of inversion in general group
+ theory follow.
*}
theorem (in group)
@@ -175,12 +182,14 @@
*}
-subsection {* Referencing explicit structures implicitly *}
+subsection {* Explicit structures referenced implicitly *}
text {*
The issue of multiple parameters raised above may be easily
addressed by stating properties over a record of group operations,
- instead of the individual constituents.
+ instead of the individual constituents. See
+ \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
+ (extensible) record types in Isabelle/HOL.
*}
record 'a group =
@@ -197,8 +206,8 @@
further by using \emph{implicit} references to the underlying
abstract entity. To this end we define global syntax, which is
translated to refer to the ``current'' structure at hand, denoted by
- the dummy item ``@{text \<struct>}'' according to the builtin syntax
- mechanism for locales.
+ the dummy item ``@{text \<struct>}'' (according to the builtin syntax
+ mechanism for locales).
*}
syntax
@@ -212,7 +221,9 @@
text {*
The following locale definition introduces a single parameter, which
- is declared as ``\isakeyword{structure}''.
+ is declared as a ``\isakeyword{structure}''. In its context the
+ dummy ``@{text \<struct>}'' refers to this very parameter, independently of
+ the present naming.
*}
locale group_struct =
@@ -222,12 +233,10 @@
and left_one: "\<one> \<cdot> x = x"
text {*
- In its context the dummy ``@{text \<struct>}'' refers to this very
- parameter, independently of the present naming. We may now proceed
- to prove results within @{text group_struct} just as before for
- @{text group}. Proper treatment of ``@{text \<struct>}'' is hidden in
- concrete syntax, so the proof text is exactly the same as for @{text
- group} given before.
+ We may now proceed to prove results within @{text group_struct} just
+ as before for @{text group}. Proper treatment of ``@{text \<struct>}'' is
+ hidden in concrete syntax, so the proof text is exactly the same as
+ before.
*}
theorem (in group_struct)
@@ -278,7 +287,7 @@
text {*
\medskip The following synthetic example demonstrates how to refer
to several structures of type @{text group} succinctly; one might
- also think of working with renamed versions of the @{text
+ also think of working with several renamed versions of the @{text
group_struct} locale above.
*}
--- a/src/HOL/ex/ROOT.ML Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Nov 08 23:50:08 2001 +0100
@@ -1,42 +1,2 @@
-(* Title: HOL/ex/ROOT.ML
- ID: $Id$
-
-Miscellaneous examples for Higher-Order Logic.
-*)
-
-(*some examples of recursive function definitions: the TFL package*)
-time_use_thy "Recdefs";
-time_use_thy "Primrec";
-
-setmp proofs 2 time_use_thy "Hilbert_Classical";
-
-(*advanced concrete syntax*)
-time_use_thy "Tuple";
-time_use_thy "Antiquote";
-time_use_thy "Multiquote";
-
-(*basic use of extensible records*)
-time_use_thy "MonoidGroup";
-time_use_thy "Records";
time_use_thy "Locales";
-time_use_thy "StringEx";
-time_use_thy "BinEx";
-
-time_use_thy "NatSum";
-time_use "cla.ML";
-time_use "mesontest.ML";
-time_use_thy "mesontest2";
-time_use_thy "BT";
-time_use_thy "AVL";
-time_use_thy "InSort";
-time_use_thy "Qsort";
-time_use_thy "Puzzle";
-
-time_use_thy "IntRing";
-
-time_use_thy "set";
-time_use_thy "MT";
-time_use_thy "Tarski";
-
-if_svc_enabled time_use_thy "svc_test";
--- a/src/HOL/ex/document/root.tex Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/ex/document/root.tex Thu Nov 08 23:50:08 2001 +0100
@@ -19,4 +19,7 @@
\parindent 0pt\parskip 0.5ex
\input{session}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}