tuned;
authorwenzelm
Thu Nov 08 23:50:08 2001 +0100 (2001-11-08)
changeset 121051e4451999200
parent 12104 c058fd42b5fc
child 12106 4a8558dbb6a0
tuned;
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/document/root.tex
src/HOL/ex/Locales.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/document/root.tex
     1.1 --- a/src/HOL/Isar_examples/ROOT.ML	Thu Nov 08 17:54:58 2001 +0100
     1.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Thu Nov 08 23:50:08 2001 +0100
     1.3 @@ -13,7 +13,9 @@
     1.4  time_use_thy "Summation";
     1.5  time_use_thy "KnasterTarski";
     1.6  time_use_thy "MutilatedCheckerboard";
     1.7 -with_path "../W0"           time_use_thy "W_correct";
     1.8 +with_path "../W0" (no_document time_use_thy) "Type";
     1.9 +with_path "../W0" time_use_thy "W_correct";
    1.10 +with_path "../NumberTheory" (no_document time_use_thy) "Primes";
    1.11  with_path "../NumberTheory" time_use_thy "Fibonacci";
    1.12  time_use_thy "Puzzle";
    1.13  time_use_thy "NestedDatatype";
     2.1 --- a/src/HOL/Isar_examples/document/root.tex	Thu Nov 08 17:54:58 2001 +0100
     2.2 +++ b/src/HOL/Isar_examples/document/root.tex	Thu Nov 08 23:50:08 2001 +0100
     2.3 @@ -13,36 +13,21 @@
     2.4  \maketitle
     2.5  
     2.6  \begin{abstract}
     2.7 -  Isar offers a high-level proof (and theory) language for Isabelle.
     2.8 -  We give various examples of Isabelle/Isar proof developments,
     2.9 -  ranging from simple demonstrations of certain language features to
    2.10 -  more advanced applications.
    2.11 +  Isar offers a high-level proof (and theory) language for Isabelle.  We give
    2.12 +  various examples of Isabelle/Isar proof developments, ranging from simple
    2.13 +  demonstrations of certain language features to a bit more advanced
    2.14 +  applications.  Note that the ``real'' applications of Isar are found
    2.15 +  elsewhere.
    2.16  \end{abstract}
    2.17  
    2.18  \tableofcontents
    2.19  
    2.20  \parindent 0pt \parskip 0.5ex
    2.21  
    2.22 -\input{BasicLogic.tex}
    2.23 -\input{Cantor.tex}
    2.24 -\input{Peirce.tex}
    2.25 -\input{ExprCompiler.tex}
    2.26 -\input{Group.tex}
    2.27 -\input{Summation.tex}
    2.28 -\input{KnasterTarski.tex}
    2.29 -\input{MutilatedCheckerboard.tex}
    2.30 -%\input{Maybe.tex}
    2.31 -%\input{Type.tex}
    2.32 -\input{W_correct.tex}
    2.33 -%\input{Primes.tex}
    2.34 -\input{Fibonacci.tex}
    2.35 -\input{Puzzle.tex}
    2.36 -\input{NestedDatatype.tex}
    2.37 -\input{Hoare.tex}
    2.38 -\input{HoareEx.tex}
    2.39 +\input{session}
    2.40  
    2.41  \nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
    2.42 -\bibliographystyle{plain}
    2.43 +\bibliographystyle{abbrv}
    2.44  \bibliography{root}
    2.45  
    2.46  \end{document}
     3.1 --- a/src/HOL/ex/Locales.thy	Thu Nov 08 17:54:58 2001 +0100
     3.2 +++ b/src/HOL/ex/Locales.thy	Thu Nov 08 23:50:08 2001 +0100
     3.3 @@ -9,12 +9,18 @@
     3.4  theory Locales = Main:
     3.5  
     3.6  text {*
     3.7 -  Locales provide a mechanism for encapsulating local contexts.  While
     3.8 -  the original version by Florian Kamm\"uller refers to the raw
     3.9 -  meta-logic, the present one of Isabelle/Isar builds on top of the
    3.10 -  rich infrastructure of Isar proof contexts.  Subsequently, we
    3.11 -  demonstrate basic use of locales to model mathematical structures
    3.12 -  (by the inevitable group theory example).
    3.13 +  Locales provide a mechanism for encapsulating local contexts.  The
    3.14 +  original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
    3.15 +  refers directly to the raw meta-logic of Isabelle.  The present
    3.16 +  version for Isabelle/Isar
    3.17 +  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on
    3.18 +  top of the rich infrastructure of proof contexts instead; this also
    3.19 +  covers essential extra-logical concepts like term abbreviations or
    3.20 +  local theorem attributes (e.g.\ declarations of simplification
    3.21 +  rules).
    3.22 +
    3.23 +  Subsequently, we demonstrate basic use of locales to model
    3.24 +  mathematical structures (by the inevitable group theory example).
    3.25  *}
    3.26  
    3.27  text_raw {*
    3.28 @@ -28,7 +34,7 @@
    3.29  
    3.30  text {*
    3.31    The following definitions of @{text group} and @{text abelian_group}
    3.32 -  simply encapsulate local parameters (with private syntax) and
    3.33 +  merely encapsulate local parameters (with private syntax) and
    3.34    assumptions; local definitions may be given as well, but are not
    3.35    shown here.
    3.36  *}
    3.37 @@ -76,9 +82,9 @@
    3.38  qed
    3.39  
    3.40  text {*
    3.41 -  \medskip Apart from the named locale context we may also refer to
    3.42 -  further ad-hoc elements (parameters, assumptions, etc.); these are
    3.43 -  discharged when the proof is finished.
    3.44 +  \medskip Apart from the named context we may also refer to further
    3.45 +  context elements (parameters, assumptions, etc.) in a casual manner;
    3.46 +  these are discharged when the proof is finished.
    3.47  *}
    3.48  
    3.49  theorem (in group)
    3.50 @@ -119,10 +125,10 @@
    3.51  qed
    3.52  
    3.53  text {*
    3.54 -  \medskip Results are automatically propagated through the hierarchy
    3.55 -  of locales.  Below we establish a trivial fact of commutative
    3.56 -  groups, while referring both to theorems of @{text group} and the
    3.57 -  characteristic assumption of @{text abelian_group}.
    3.58 +  \medskip Established results are automatically propagated through
    3.59 +  the hierarchy of locales.  Below we establish a trivial fact in
    3.60 +  commutative groups, while referring both to theorems of @{text
    3.61 +  group} and the additional assumption of @{text abelian_group}.
    3.62  *}
    3.63  
    3.64  theorem (in abelian_group)
    3.65 @@ -134,7 +140,8 @@
    3.66  qed
    3.67  
    3.68  text {*
    3.69 -  \medskip Some further facts of general group theory follow.
    3.70 +  \medskip Some further properties of inversion in general group
    3.71 +  theory follow.
    3.72  *}
    3.73  
    3.74  theorem (in group)
    3.75 @@ -175,12 +182,14 @@
    3.76  *}
    3.77  
    3.78  
    3.79 -subsection {* Referencing explicit structures implicitly *}
    3.80 +subsection {* Explicit structures referenced implicitly *}
    3.81  
    3.82  text {*
    3.83    The issue of multiple parameters raised above may be easily
    3.84    addressed by stating properties over a record of group operations,
    3.85 -  instead of the individual constituents.
    3.86 +  instead of the individual constituents.  See
    3.87 +  \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
    3.88 +  (extensible) record types in Isabelle/HOL.
    3.89  *}
    3.90  
    3.91  record 'a group =
    3.92 @@ -197,8 +206,8 @@
    3.93    further by using \emph{implicit} references to the underlying
    3.94    abstract entity.  To this end we define global syntax, which is
    3.95    translated to refer to the ``current'' structure at hand, denoted by
    3.96 -  the dummy item ``@{text \<struct>}'' according to the builtin syntax
    3.97 -  mechanism for locales.
    3.98 +  the dummy item ``@{text \<struct>}'' (according to the builtin syntax
    3.99 +  mechanism for locales).
   3.100  *}
   3.101  
   3.102  syntax
   3.103 @@ -212,7 +221,9 @@
   3.104  
   3.105  text {*
   3.106    The following locale definition introduces a single parameter, which
   3.107 -  is declared as ``\isakeyword{structure}''.
   3.108 +  is declared as a ``\isakeyword{structure}''. In its context the
   3.109 +  dummy ``@{text \<struct>}'' refers to this very parameter, independently of
   3.110 +  the present naming.
   3.111  *}
   3.112  
   3.113  locale group_struct =
   3.114 @@ -222,12 +233,10 @@
   3.115      and left_one: "\<one> \<cdot> x = x"
   3.116  
   3.117  text {*
   3.118 -  In its context the dummy ``@{text \<struct>}'' refers to this very
   3.119 -  parameter, independently of the present naming.  We may now proceed
   3.120 -  to prove results within @{text group_struct} just as before for
   3.121 -  @{text group}.  Proper treatment of ``@{text \<struct>}'' is hidden in
   3.122 -  concrete syntax, so the proof text is exactly the same as for @{text
   3.123 -  group} given before.
   3.124 +  We may now proceed to prove results within @{text group_struct} just
   3.125 +  as before for @{text group}.  Proper treatment of ``@{text \<struct>}'' is
   3.126 +  hidden in concrete syntax, so the proof text is exactly the same as
   3.127 +  before.
   3.128  *}
   3.129  
   3.130  theorem (in group_struct)
   3.131 @@ -278,7 +287,7 @@
   3.132  text {*
   3.133    \medskip The following synthetic example demonstrates how to refer
   3.134    to several structures of type @{text group} succinctly; one might
   3.135 -  also think of working with renamed versions of the @{text
   3.136 +  also think of working with several renamed versions of the @{text
   3.137    group_struct} locale above.
   3.138  *}
   3.139  
     4.1 --- a/src/HOL/ex/ROOT.ML	Thu Nov 08 17:54:58 2001 +0100
     4.2 +++ b/src/HOL/ex/ROOT.ML	Thu Nov 08 23:50:08 2001 +0100
     4.3 @@ -1,42 +1,2 @@
     4.4 -(*  Title:      HOL/ex/ROOT.ML
     4.5 -    ID:         $Id$
     4.6 -
     4.7 -Miscellaneous examples for Higher-Order Logic.
     4.8 -*)
     4.9 -
    4.10 -(*some examples of recursive function definitions: the TFL package*)
    4.11 -time_use_thy "Recdefs";
    4.12 -time_use_thy "Primrec";
    4.13 -
    4.14 -setmp proofs 2 time_use_thy "Hilbert_Classical";
    4.15 -
    4.16 -(*advanced concrete syntax*)
    4.17 -time_use_thy "Tuple";
    4.18 -time_use_thy "Antiquote";
    4.19 -time_use_thy "Multiquote";
    4.20 -
    4.21 -(*basic use of extensible records*)
    4.22 -time_use_thy "MonoidGroup";
    4.23 -time_use_thy "Records";
    4.24  
    4.25  time_use_thy "Locales";
    4.26 -time_use_thy "StringEx";
    4.27 -time_use_thy "BinEx";
    4.28 -
    4.29 -time_use_thy "NatSum";
    4.30 -time_use     "cla.ML";
    4.31 -time_use     "mesontest.ML";
    4.32 -time_use_thy "mesontest2";
    4.33 -time_use_thy "BT";
    4.34 -time_use_thy "AVL";
    4.35 -time_use_thy "InSort";
    4.36 -time_use_thy "Qsort";
    4.37 -time_use_thy "Puzzle";
    4.38 -
    4.39 -time_use_thy "IntRing";
    4.40 -
    4.41 -time_use_thy "set";
    4.42 -time_use_thy "MT";
    4.43 -time_use_thy "Tarski";
    4.44 -
    4.45 -if_svc_enabled time_use_thy "svc_test";
     5.1 --- a/src/HOL/ex/document/root.tex	Thu Nov 08 17:54:58 2001 +0100
     5.2 +++ b/src/HOL/ex/document/root.tex	Thu Nov 08 23:50:08 2001 +0100
     5.3 @@ -19,4 +19,7 @@
     5.4  \parindent 0pt\parskip 0.5ex
     5.5  \input{session}
     5.6  
     5.7 +\bibliographystyle{abbrv}
     5.8 +\bibliography{root}
     5.9 +
    5.10  \end{document}