summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 08 Nov 2001 23:50:08 +0100 | |

changeset 12105 | 1e4451999200 |

parent 12104 | c058fd42b5fc |

child 12106 | 4a8558dbb6a0 |

tuned;

--- 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";