tuned document;
authorwenzelm
Thu May 06 14:14:18 2004 +0200 (2004-05-06)
changeset 1470671590b7733b7
parent 14705 14b2c22a7e40
child 14707 2d6350d7b9b7
tuned document;
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/document/root.bib
src/HOL/Algebra/document/root.tex
src/HOL/Library/Accessible_Part.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Library.thy
src/HOL/Library/Library/document/root.bib
src/HOL/Library/Library/document/root.tex
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
src/HOL/Library/Zorn.thy
src/HOL/document/root.tex
     1.1 --- a/src/HOL/Algebra/Bij.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Algebra/Bij
     1.5 +(*  Title:      HOL/Algebra/Bij.thy
     1.6      ID:         $Id$
     1.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     1.8  *)
     2.1 --- a/src/HOL/Algebra/Coset.thy	Thu May 06 12:43:00 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Thu May 06 14:14:18 2004 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/GroupTheory/Coset
     2.5 +(*  Title:      HOL/Algebra/Coset.thy
     2.6      ID:         $Id$
     2.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     2.8  *)
     3.1 --- a/src/HOL/Algebra/Exponent.thy	Thu May 06 12:43:00 2004 +0200
     3.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu May 06 14:14:18 2004 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/GroupTheory/Exponent
     3.5 +(*  Title:      HOL/Algebra/Exponent.thy
     3.6      ID:         $Id$
     3.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     3.8  
     4.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu May 06 12:43:00 2004 +0200
     4.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu May 06 14:14:18 2004 +0200
     4.3 @@ -1,11 +1,11 @@
     4.4 -(*  Title:      Product Operator for Commutative Monoids
     4.5 +(*  Title:      HOL/Algebra/FiniteProduct.thy
     4.6      ID:         $Id$
     4.7      Author:     Clemens Ballarin, started 19 November 2002
     4.8  
     4.9  This file is largely based on HOL/Finite_Set.thy.
    4.10  *)
    4.11  
    4.12 -header {* Product Operator *}
    4.13 +header {* Product Operator for Commutative Monoids *}
    4.14  
    4.15  theory FiniteProduct = Group:
    4.16  
     5.1 --- a/src/HOL/Algebra/Group.thy	Thu May 06 12:43:00 2004 +0200
     5.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 06 14:14:18 2004 +0200
     5.3 @@ -13,9 +13,9 @@
     5.4  section {* From Magmas to Groups *}
     5.5  
     5.6  text {*
     5.7 -  Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
     5.8 -  the exception of \emph{magma} which, following Bourbaki, is a set
     5.9 -  together with a binary, closed operation.
    5.10 +  Definitions follow \cite{Jacobson:1985}; with the exception of
    5.11 +  \emph{magma} which, following Bourbaki, is a set together with a
    5.12 +  binary, closed operation.
    5.13  *}
    5.14  
    5.15  subsection {* Definitions *}
     6.1 --- a/src/HOL/Algebra/Lattice.thy	Thu May 06 12:43:00 2004 +0200
     6.2 +++ b/src/HOL/Algebra/Lattice.thy	Thu May 06 14:14:18 2004 +0200
     6.3 @@ -1,11 +1,11 @@
     6.4  (*
     6.5 -  Title:     Orders and Lattices
     6.6 +  Title:     HOL/Algebra/Lattice.thy
     6.7    Id:        $Id$
     6.8    Author:    Clemens Ballarin, started 7 November 2003
     6.9    Copyright: Clemens Ballarin
    6.10  *)
    6.11  
    6.12 -header {* Order and Lattices *}
    6.13 +header {* Orders and Lattices *}
    6.14  
    6.15  theory Lattice = Group:
    6.16  
     7.1 --- a/src/HOL/Algebra/Module.thy	Thu May 06 12:43:00 2004 +0200
     7.2 +++ b/src/HOL/Algebra/Module.thy	Thu May 06 14:14:18 2004 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Algebra/Module
     7.5 +(*  Title:      HOL/Algebra/Module.thy
     7.6      ID:         $Id$
     7.7      Author:     Clemens Ballarin, started 15 April 2003
     7.8      Copyright:  Clemens Ballarin
     8.1 --- a/src/HOL/Algebra/Sylow.thy	Thu May 06 12:43:00 2004 +0200
     8.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu May 06 14:14:18 2004 +0200
     8.3 @@ -1,17 +1,16 @@
     8.4 -(*  Title:      HOL/GroupTheory/Sylow
     8.5 +(*  Title:      HOL/Algebra/Sylow.thy
     8.6      ID:         $Id$
     8.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     8.8 -
     8.9 -See Florian Kamm\"uller and L. C. Paulson,
    8.10 -    A Formal Proof of Sylow's theorem:
    8.11 -        An Experiment in Abstract Algebra with Isabelle HOL
    8.12 -    J. Automated Reasoning 23 (1999), 235-264
    8.13  *)
    8.14  
    8.15 -header{*Sylow's theorem using locales*}
    8.16 +header {* Sylow's theorem *}
    8.17  
    8.18  theory Sylow = Coset:
    8.19  
    8.20 +text {*
    8.21 +  See also \cite{Kammueller-Paulson:1999}.
    8.22 +*}
    8.23 +
    8.24  subsection {*Order of a Group and Lagrange's Theorem*}
    8.25  
    8.26  constdefs
     9.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu May 06 12:43:00 2004 +0200
     9.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu May 06 14:14:18 2004 +0200
     9.3 @@ -1,5 +1,5 @@
     9.4  (*
     9.5 -  Title:     Univariate Polynomials
     9.6 +  Title:     HOL/Algebra/UnivPoly.thy
     9.7    Id:        $Id$
     9.8    Author:    Clemens Ballarin, started 9 December 1996
     9.9    Copyright: Clemens Ballarin
    9.10 @@ -16,10 +16,9 @@
    9.11    carrier set is a set of bounded functions from Nat to the
    9.12    coefficient domain.  Bounded means that these functions return zero
    9.13    above a certain bound (the degree).  There is a chapter on the
    9.14 -  formalisation of polynomials in my PhD thesis
    9.15 -  (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
    9.16 -  implemented with axiomatic type classes.  This was later ported to
    9.17 -  Locales.
    9.18 +  formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
    9.19 +  which was implemented with axiomatic type classes.  This was later
    9.20 +  ported to Locales.
    9.21  *}
    9.22  
    9.23  
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Algebra/document/root.bib	Thu May 06 14:14:18 2004 +0200
    10.3 @@ -0,0 +1,25 @@
    10.4 +
    10.5 +@PhdThesis{Ballarin:1999,
    10.6 +  author = 	 {Clemens Ballarin},
    10.7 +  title = 	 {Computer Algebra and Theorem Proving},
    10.8 +  school = 	 {University of Cambridge},
    10.9 +  year = 	 1999,
   10.10 +  note =	 {\url{http://www4.in.tum.de/~ballarin/publications.html}}
   10.11 +}
   10.12 +
   10.13 +@Book{Jacobson:1985,
   10.14 +  author =	 {Nathan Jacobson},
   10.15 +  title = 	 {Basic Algebra I},
   10.16 +  publisher = 	 {Freeman},
   10.17 +  year = 	 1985
   10.18 +}
   10.19 +
   10.20 +@Article{Kammueller-Paulson:1999,
   10.21 +  author = 	 {Florian Kamm\"uller and L. C. Paulson},
   10.22 +  title =        {A Formal Proof of Sylow's theorem: An Experiment in
   10.23 +                  Abstract Algebra with {Isabelle HOL}},
   10.24 +  journal = 	 {J. Automated Reasoning},
   10.25 +  year = 	 1999,
   10.26 +  number =	 23,
   10.27 +  pages =	 {235--264}
   10.28 +}
    11.1 --- a/src/HOL/Algebra/document/root.tex	Thu May 06 12:43:00 2004 +0200
    11.2 +++ b/src/HOL/Algebra/document/root.tex	Thu May 06 14:14:18 2004 +0200
    11.3 @@ -1,3 +1,5 @@
    11.4 +
    11.5 +% $Id$
    11.6  
    11.7  \documentclass[11pt,a4paper]{article}
    11.8  \usepackage{graphicx}
    11.9 @@ -10,21 +12,18 @@
   11.10  % this should be the last package used
   11.11  \usepackage{pdfsetup}
   11.12  
   11.13 -% proper setup for best-style documents
   11.14  \urlstyle{rm}
   11.15  \isabellestyle{it}
   11.16 -
   11.17 -%\usepackage{substr}
   11.18 -
   11.19 -%\renewcommand{\isamarkupheader}[1]{%
   11.20 -%  \IfSubStringInString{Chapter: }{#1}{%
   11.21 -%    \chapter{\BehindSubString{Chapter: }{#1}}}{%
   11.22 -%  \section{#1}}}
   11.23 -
   11.24 +\pagestyle{myheadings}
   11.25  
   11.26  \begin{document}
   11.27  
   11.28 -\title{The Isabelle Algebra Library}
   11.29 +\title{The Isabelle/HOL Algebra Library}
   11.30 +\author{
   11.31 +  Clemens Ballarin \\
   11.32 +  Florian Kammu\"uller \\
   11.33 +  Lawrence C Paulson \\
   11.34 +}
   11.35  \maketitle
   11.36  
   11.37  \tableofcontents
   11.38 @@ -35,8 +34,14 @@
   11.39  
   11.40  \clearpage
   11.41  
   11.42 +\renewcommand{\isamarkupheader}[1]%
   11.43 +{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
   11.44 +
   11.45  \parindent 0pt\parskip 0.5ex
   11.46 -
   11.47  \input{session}
   11.48  
   11.49 +\pagestyle{headings}
   11.50 +\bibliographystyle{abbrv}
   11.51 +\bibliography{root}
   11.52 +
   11.53  \end{document}
    12.1 --- a/src/HOL/Library/Accessible_Part.thy	Thu May 06 12:43:00 2004 +0200
    12.2 +++ b/src/HOL/Library/Accessible_Part.thy	Thu May 06 14:14:18 2004 +0200
    12.3 @@ -4,10 +4,7 @@
    12.4      Copyright   1994  University of Cambridge
    12.5  *)
    12.6  
    12.7 -header {*
    12.8 - \title{The accessible part of a relation}
    12.9 - \author{Lawrence C Paulson}
   12.10 -*}
   12.11 +header {* The accessible part of a relation *}
   12.12  
   12.13  theory Accessible_Part = Main:
   12.14  
    13.1 --- a/src/HOL/Library/Continuity.thy	Thu May 06 12:43:00 2004 +0200
    13.2 +++ b/src/HOL/Library/Continuity.thy	Thu May 06 14:14:18 2004 +0200
    13.3 @@ -4,10 +4,7 @@
    13.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.5  *)
    13.6  
    13.7 -header {*
    13.8 -  \title{Continuity and iterations (of set transformers)}
    13.9 -  \author{David von Oheimb}
   13.10 -*}
   13.11 +header {* Continuity and iterations (of set transformers) *}
   13.12  
   13.13  theory Continuity = Main:
   13.14  
    14.1 --- a/src/HOL/Library/FuncSet.thy	Thu May 06 12:43:00 2004 +0200
    14.2 +++ b/src/HOL/Library/FuncSet.thy	Thu May 06 14:14:18 2004 +0200
    14.3 @@ -3,22 +3,19 @@
    14.4      Author:     Florian Kammueller and Lawrence C Paulson
    14.5  *)
    14.6  
    14.7 -header {*
    14.8 -  \title{Pi and Function Sets}
    14.9 -  \author{Florian Kammueller and Lawrence C Paulson}
   14.10 -*}
   14.11 +header {* Pi and Function Sets *}
   14.12  
   14.13  theory FuncSet = Main:
   14.14  
   14.15  constdefs
   14.16 -  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
   14.17 -    "Pi A B == {f. \<forall>x. x \<in> A --> f(x) \<in> B(x)}"
   14.18 +  Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
   14.19 +  "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
   14.20  
   14.21    extensional :: "'a set => ('a => 'b) set"
   14.22 -    "extensional A == {f. \<forall>x. x~:A --> f(x) = arbitrary}"
   14.23 +  "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
   14.24  
   14.25 -  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
   14.26 -    "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
   14.27 +  "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
   14.28 +  "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
   14.29  
   14.30  syntax
   14.31    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
   14.32 @@ -27,7 +24,7 @@
   14.33  
   14.34  syntax (xsymbols)
   14.35    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
   14.36 -  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60) 
   14.37 +  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
   14.38    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
   14.39  
   14.40  syntax (HTML output)
   14.41 @@ -36,11 +33,11 @@
   14.42  
   14.43  translations
   14.44    "PI x:A. B" => "Pi A (%x. B)"
   14.45 -  "A -> B"    => "Pi A (_K B)"
   14.46 -  "%x:A. f"  == "restrict (%x. f) A"
   14.47 +  "A -> B" => "Pi A (_K B)"
   14.48 +  "%x:A. f" == "restrict (%x. f) A"
   14.49  
   14.50  constdefs
   14.51 -  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
   14.52 +  "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
   14.53    "compose A g f == \<lambda>x\<in>A. g (f x)"
   14.54  
   14.55  print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
   14.56 @@ -49,126 +46,123 @@
   14.57  subsection{*Basic Properties of @{term Pi}*}
   14.58  
   14.59  lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
   14.60 -by (simp add: Pi_def)
   14.61 +  by (simp add: Pi_def)
   14.62  
   14.63  lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
   14.64 -by (simp add: Pi_def)
   14.65 +  by (simp add: Pi_def)
   14.66  
   14.67  lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
   14.68 -by (simp add: Pi_def)
   14.69 +  by (simp add: Pi_def)
   14.70  
   14.71  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
   14.72 -by (simp add: Pi_def)
   14.73 +  by (simp add: Pi_def)
   14.74  
   14.75  lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
   14.76  apply (simp add: Pi_def, auto)
   14.77  txt{*Converse direction requires Axiom of Choice to exhibit a function
   14.78  picking an element from each non-empty @{term "B x"}*}
   14.79  apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
   14.80 -apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto) 
   14.81 +apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
   14.82  done
   14.83  
   14.84  lemma Pi_empty [simp]: "Pi {} B = UNIV"
   14.85 -by (simp add: Pi_def)
   14.86 +  by (simp add: Pi_def)
   14.87  
   14.88  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
   14.89 -by (simp add: Pi_def)
   14.90 +  by (simp add: Pi_def)
   14.91  
   14.92  text{*Covariance of Pi-sets in their second argument*}
   14.93  lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
   14.94 -by (simp add: Pi_def, blast)
   14.95 +  by (simp add: Pi_def, blast)
   14.96  
   14.97  text{*Contravariance of Pi-sets in their first argument*}
   14.98  lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
   14.99 -by (simp add: Pi_def, blast)
  14.100 +  by (simp add: Pi_def, blast)
  14.101  
  14.102  
  14.103  subsection{*Composition With a Restricted Domain: @{term compose}*}
  14.104  
  14.105 -lemma funcset_compose: 
  14.106 -     "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
  14.107 -by (simp add: Pi_def compose_def restrict_def)
  14.108 +lemma funcset_compose:
  14.109 +    "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
  14.110 +  by (simp add: Pi_def compose_def restrict_def)
  14.111  
  14.112  lemma compose_assoc:
  14.113 -     "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |] 
  14.114 +    "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
  14.115        ==> compose A h (compose A g f) = compose A (compose B h g) f"
  14.116 -by (simp add: expand_fun_eq Pi_def compose_def restrict_def) 
  14.117 +  by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
  14.118  
  14.119  lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
  14.120 -by (simp add: compose_def restrict_def)
  14.121 +  by (simp add: compose_def restrict_def)
  14.122  
  14.123  lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
  14.124 -by (auto simp add: image_def compose_eq)
  14.125 +  by (auto simp add: image_def compose_eq)
  14.126  
  14.127  lemma inj_on_compose:
  14.128 -     "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
  14.129 -by (auto simp add: inj_on_def compose_eq)
  14.130 +    "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
  14.131 +  by (auto simp add: inj_on_def compose_eq)
  14.132  
  14.133  
  14.134  subsection{*Bounded Abstraction: @{term restrict}*}
  14.135  
  14.136  lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
  14.137 -by (simp add: Pi_def restrict_def)
  14.138 +  by (simp add: Pi_def restrict_def)
  14.139  
  14.140  lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
  14.141 -by (simp add: Pi_def restrict_def)
  14.142 +  by (simp add: Pi_def restrict_def)
  14.143  
  14.144  lemma restrict_apply [simp]:
  14.145 -     "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
  14.146 -by (simp add: restrict_def)
  14.147 +    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
  14.148 +  by (simp add: restrict_def)
  14.149  
  14.150 -lemma restrict_ext: 
  14.151 +lemma restrict_ext:
  14.152      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
  14.153 -by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
  14.154 +  by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
  14.155  
  14.156  lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
  14.157 -by (simp add: inj_on_def restrict_def)
  14.158 -
  14.159 +  by (simp add: inj_on_def restrict_def)
  14.160  
  14.161  lemma Id_compose:
  14.162 -     "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
  14.163 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
  14.164 +    "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
  14.165 +  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
  14.166  
  14.167  lemma compose_Id:
  14.168 -     "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
  14.169 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
  14.170 +    "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
  14.171 +  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
  14.172  
  14.173  
  14.174  subsection{*Extensionality*}
  14.175  
  14.176  lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
  14.177 -by (simp add: extensional_def)
  14.178 +  by (simp add: extensional_def)
  14.179  
  14.180  lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
  14.181 -by (simp add: restrict_def extensional_def)
  14.182 +  by (simp add: restrict_def extensional_def)
  14.183  
  14.184  lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
  14.185 -by (simp add: compose_def)
  14.186 +  by (simp add: compose_def)
  14.187  
  14.188  lemma extensionalityI:
  14.189 -     "[| f \<in> extensional A; g \<in> extensional A; 
  14.190 -         !!x. x\<in>A ==> f x = g x |] ==> f = g"
  14.191 -by (force simp add: expand_fun_eq extensional_def)
  14.192 +    "[| f \<in> extensional A; g \<in> extensional A;
  14.193 +      !!x. x\<in>A ==> f x = g x |] ==> f = g"
  14.194 +  by (force simp add: expand_fun_eq extensional_def)
  14.195  
  14.196  lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
  14.197 -apply (unfold Inv_def)
  14.198 -apply (fast intro: restrict_in_funcset someI2)
  14.199 -done
  14.200 +  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
  14.201  
  14.202  lemma compose_Inv_id:
  14.203 -     "[| inj_on f A;  f ` A = B |]  
  14.204 +    "[| inj_on f A;  f ` A = B |]
  14.205        ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
  14.206 -apply (simp add: compose_def)
  14.207 -apply (rule restrict_ext, auto)
  14.208 -apply (erule subst)
  14.209 -apply (simp add: Inv_f_f)
  14.210 -done
  14.211 +  apply (simp add: compose_def)
  14.212 +  apply (rule restrict_ext, auto)
  14.213 +  apply (erule subst)
  14.214 +  apply (simp add: Inv_f_f)
  14.215 +  done
  14.216  
  14.217  lemma compose_id_Inv:
  14.218 -     "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
  14.219 -apply (simp add: compose_def)
  14.220 -apply (rule restrict_ext)
  14.221 -apply (simp add: f_Inv_f)
  14.222 -done
  14.223 +    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
  14.224 +  apply (simp add: compose_def)
  14.225 +  apply (rule restrict_ext)
  14.226 +  apply (simp add: f_Inv_f)
  14.227 +  done
  14.228  
  14.229  end
    15.1 --- a/src/HOL/Library/Library.thy	Thu May 06 12:43:00 2004 +0200
    15.2 +++ b/src/HOL/Library/Library.thy	Thu May 06 14:14:18 2004 +0200
    15.3 @@ -1,16 +1,18 @@
    15.4  (*<*)
    15.5  theory Library =
    15.6 -  Quotient +
    15.7 -  Nat_Infinity +
    15.8 -  List_Prefix +
    15.9 -  Nested_Environment +
   15.10    Accessible_Part +
   15.11    Continuity +
   15.12 +  FuncSet +
   15.13 +  List_Prefix +
   15.14    Multiset +
   15.15 -  Permutation +
   15.16    NatPair +
   15.17 +  Nat_Infinity +
   15.18 +  Nested_Environment +
   15.19 +  Permutation +
   15.20    Primes +
   15.21 +  Quotient +
   15.22 +  While_Combinator +
   15.23    Word +
   15.24 -  While_Combinator:
   15.25 +  Zorn:
   15.26  end
   15.27  (*>*)
    16.1 --- a/src/HOL/Library/Library/document/root.bib	Thu May 06 12:43:00 2004 +0200
    16.2 +++ b/src/HOL/Library/Library/document/root.bib	Thu May 06 14:14:18 2004 +0200
    16.3 @@ -1,3 +1,17 @@
    16.4 +
    16.5 + @Unpublished{Abrial-Laffitte,
    16.6 +  author = 	 {Abrial and Laffitte},
    16.7 +  title = 	 {Towards the Mechanization of the Proofs of
    16.8 +                  Some Classical Theorems of Set Theory},
    16.9 +  note = 	 {Unpublished}
   16.10 +}
   16.11 +
   16.12 +@Book{Oberschelp:1993,
   16.13 +  author =	 {Arnold Oberschelp},
   16.14 +  title = 	 {Rekursionstheorie},
   16.15 +  publisher = 	 {BI-Wissenschafts-Verlag},
   16.16 +  year = 	 1993
   16.17 +}
   16.18  
   16.19  @Book{davenport92,
   16.20    author =	 {H. Davenport},
    17.1 --- a/src/HOL/Library/Library/document/root.tex	Thu May 06 12:43:00 2004 +0200
    17.2 +++ b/src/HOL/Library/Library/document/root.tex	Thu May 06 14:14:18 2004 +0200
    17.3 @@ -15,6 +15,7 @@
    17.4  \title{The Supplemental Isabelle/HOL Library}
    17.5  \author{
    17.6    Gertrud Bauer \\
    17.7 +  Jacques D Fleuriot \\
    17.8    Tobias Nipkow \\
    17.9    David von Oheimb \\
   17.10    Lawrence C Paulson \\
   17.11 @@ -28,16 +29,8 @@
   17.12  \tableofcontents
   17.13  \newpage
   17.14  
   17.15 -%now hack the "header" markup to support \title and \author
   17.16 -\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
   17.17 -\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
   17.18  \renewcommand{\isamarkupheader}[1]%
   17.19 -{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
   17.20 -#1%
   17.21 -\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
   17.22 -\markright{THEORY~``\isabellecontext''}%
   17.23 -\ifthenelse{\equal{}{\isabelleauthor}}{}%
   17.24 -{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
   17.25 +{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
   17.26  
   17.27  \parindent 0pt \parskip 0.5ex
   17.28  \input{session}
    18.1 --- a/src/HOL/Library/List_Prefix.thy	Thu May 06 12:43:00 2004 +0200
    18.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu May 06 14:14:18 2004 +0200
    18.3 @@ -4,10 +4,7 @@
    18.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    18.5  *)
    18.6  
    18.7 -header {*
    18.8 -  \title{List prefixes and postfixes}
    18.9 -  \author{Tobias Nipkow and Markus Wenzel}
   18.10 -*}
   18.11 +header {* List prefixes and postfixes *}
   18.12  
   18.13  theory List_Prefix = Main:
   18.14  
   18.15 @@ -222,36 +219,43 @@
   18.16    postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
   18.17    "xs >= ys == \<exists>zs. xs = zs @ ys"
   18.18  
   18.19 -lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def)
   18.20 -lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" 
   18.21 -         by (auto simp add: postfix_def)
   18.22 -lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" 
   18.23 -         by (auto simp add: postfix_def)
   18.24 +lemma postfix_refl [simp, intro!]: "xs >= xs"
   18.25 +  by (auto simp add: postfix_def)
   18.26 +lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs"
   18.27 +  by (auto simp add: postfix_def)
   18.28 +lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys"
   18.29 +  by (auto simp add: postfix_def)
   18.30  
   18.31 -lemma Nil_postfix [iff]: "xs >= []" by (simp add: postfix_def)
   18.32 -lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"by (auto simp add:postfix_def)
   18.33 +lemma Nil_postfix [iff]: "xs >= []"
   18.34 +  by (simp add: postfix_def)
   18.35 +lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"
   18.36 +  by (auto simp add:postfix_def)
   18.37  
   18.38 -lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" by (auto simp add: postfix_def)
   18.39 -lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" by (auto simp add: postfix_def)
   18.40 +lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys"
   18.41 +  by (auto simp add: postfix_def)
   18.42 +lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys"
   18.43 +  by (auto simp add: postfix_def)
   18.44  
   18.45 -lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs@xs >= ys" by(auto simp add: postfix_def)
   18.46 -lemma postfix_appendD: "xs >= zs@ys \<Longrightarrow> xs >= ys" by(auto simp add: postfix_def)
   18.47 +lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys"
   18.48 +  by (auto simp add: postfix_def)
   18.49 +lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys"
   18.50 +  by(auto simp add: postfix_def)
   18.51  
   18.52  lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
   18.53 -by (induct zs, auto)
   18.54 +  by (induct zs, auto)
   18.55  lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
   18.56 -by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
   18.57 +  by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
   18.58  
   18.59  lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
   18.60 -by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
   18.61 +  by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
   18.62  lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
   18.63 -by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
   18.64 +  by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
   18.65  
   18.66  lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
   18.67 -apply (unfold prefix_def postfix_def, safe)
   18.68 -apply (rule_tac x = "rev zs" in exI, simp)
   18.69 -apply (rule_tac x = "rev zs" in exI)
   18.70 -apply (rule rev_is_rev_conv [THEN iffD1], simp)
   18.71 -done
   18.72 +  apply (unfold prefix_def postfix_def, safe)
   18.73 +  apply (rule_tac x = "rev zs" in exI, simp)
   18.74 +  apply (rule_tac x = "rev zs" in exI)
   18.75 +  apply (rule rev_is_rev_conv [THEN iffD1], simp)
   18.76 +  done
   18.77  
   18.78  end
    19.1 --- a/src/HOL/Library/Multiset.thy	Thu May 06 12:43:00 2004 +0200
    19.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 06 14:14:18 2004 +0200
    19.3 @@ -4,10 +4,7 @@
    19.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    19.5  *)
    19.6  
    19.7 -header {*
    19.8 - \title{Multisets}
    19.9 - \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson}
   19.10 -*}
   19.11 +header {* Multisets *}
   19.12  
   19.13  theory Multiset = Accessible_Part:
   19.14  
    20.1 --- a/src/HOL/Library/NatPair.thy	Thu May 06 12:43:00 2004 +0200
    20.2 +++ b/src/HOL/Library/NatPair.thy	Thu May 06 14:14:18 2004 +0200
    20.3 @@ -4,89 +4,89 @@
    20.4      Copyright   2003 Technische Universitaet Muenchen
    20.5  *)
    20.6  
    20.7 -header {*
    20.8 -  \title{Pairs of Natural Numbers}
    20.9 -  \author{Stefan Richter}
   20.10 -*}
   20.11 +header {* Pairs of Natural Numbers *}
   20.12  
   20.13  theory NatPair = Main:
   20.14  
   20.15 -text{*An injective function from $\mathbf{N}^2$ to
   20.16 -  $\mathbf{N}$.  Definition and proofs are from 
   20.17 -  Arnold Oberschelp.  Rekursionstheorie.  BI-Wissenschafts-Verlag, 1993
   20.18 -  (page 85).  *}
   20.19 +text{*
   20.20 +  An injective function from @{text "\<nat>\<twosuperior>"} to @{text
   20.21 +  \<nat>}.  Definition and proofs are from \cite[page
   20.22 +  85]{Oberschelp:1993}.
   20.23 +*}
   20.24  
   20.25 -constdefs 
   20.26 +constdefs
   20.27    nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
   20.28    "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
   20.29  
   20.30 -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" 
   20.31 -proof (cases "2 dvd a") 
   20.32 +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
   20.33 +proof (cases "2 dvd a")
   20.34    case True
   20.35    thus ?thesis by (rule dvd_mult2)
   20.36  next
   20.37 -  case False 
   20.38 +  case False
   20.39    hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
   20.40 -  hence "Suc a mod 2 = 0" by (simp add: mod_Suc) 
   20.41 -  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) 
   20.42 +  hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
   20.43 +  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
   20.44    thus ?thesis by (rule dvd_mult)
   20.45  qed
   20.46  
   20.47 -lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" 
   20.48 +lemma
   20.49 +  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
   20.50    shows nat2_to_nat_help: "u+v \<le> x+y"
   20.51  proof (rule classical)
   20.52    assume "\<not> ?thesis"
   20.53 -  hence contrapos: "x+y < u+v" 
   20.54 +  hence contrapos: "x+y < u+v"
   20.55      by simp
   20.56 -  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" 
   20.57 +  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
   20.58      by (unfold nat2_to_nat_def) (simp add: Let_def)
   20.59 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" 
   20.60 -    by (simp only: div_mult_self1_is_m) 
   20.61 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 
   20.62 -    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" 
   20.63 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
   20.64 +    by (simp only: div_mult_self1_is_m)
   20.65 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
   20.66 +    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
   20.67    proof -
   20.68 -    have "2 dvd (x+y)*Suc(x+y)" 
   20.69 +    have "2 dvd (x+y)*Suc(x+y)"
   20.70        by (rule dvd2_a_x_suc_a)
   20.71 -    hence "(x+y)*Suc(x+y) mod 2 = 0" 
   20.72 +    hence "(x+y)*Suc(x+y) mod 2 = 0"
   20.73        by (simp only: dvd_eq_mod_eq_0)
   20.74      also
   20.75 -    have "2 * Suc(x+y) mod 2 = 0" 
   20.76 +    have "2 * Suc(x+y) mod 2 = 0"
   20.77        by (rule mod_mult_self1_is_0)
   20.78 -    ultimately have 
   20.79 -      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" 
   20.80 -      by simp 
   20.81 -    thus ?thesis 
   20.82 +    ultimately have
   20.83 +      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
   20.84 +      by simp
   20.85 +    thus ?thesis
   20.86        by simp
   20.87 -  qed 
   20.88 -  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" 
   20.89 -    by (rule div_add1_eq[THEN sym])
   20.90 -  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" 
   20.91 -    by (simp only: add_mult_distrib[THEN sym])
   20.92 -  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" 
   20.93 -    by (simp only: mult_le_mono div_le_mono) 
   20.94 -  also have "\<dots> \<le> nat2_to_nat (u,v)" 
   20.95 +  qed
   20.96 +  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
   20.97 +    by (rule div_add1_eq [symmetric])
   20.98 +  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
   20.99 +    by (simp only: add_mult_distrib [symmetric])
  20.100 +  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
  20.101 +    by (simp only: mult_le_mono div_le_mono)
  20.102 +  also have "\<dots> \<le> nat2_to_nat (u,v)"
  20.103      by (unfold nat2_to_nat_def) (simp add: Let_def)
  20.104 -  finally show ?thesis 
  20.105 +  finally show ?thesis
  20.106      by (simp only: eq)
  20.107  qed
  20.108  
  20.109 -lemma nat2_to_nat_inj: "inj nat2_to_nat"
  20.110 +theorem nat2_to_nat_inj: "inj nat2_to_nat"
  20.111  proof -
  20.112 -  {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
  20.113 +  {
  20.114 +    fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
  20.115      hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
  20.116 -    also from prems[THEN sym] have "x+y \<le> u+v" 
  20.117 +    also from prems [symmetric] have "x+y \<le> u+v"
  20.118        by (rule nat2_to_nat_help)
  20.119      finally have eq: "u+v = x+y" .
  20.120 -    with prems have ux: "u=x" 
  20.121 +    with prems have ux: "u=x"
  20.122        by (simp add: nat2_to_nat_def Let_def)
  20.123 -    with eq have vy: "v=y" 
  20.124 +    with eq have vy: "v=y"
  20.125        by simp
  20.126 -    with ux have "(u,v) = (x,y)" 
  20.127 +    with ux have "(u,v) = (x,y)"
  20.128        by simp
  20.129    }
  20.130 -  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" 
  20.131 +  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
  20.132      by fast
  20.133 -  thus ?thesis 
  20.134 +  thus ?thesis
  20.135      by (unfold inj_on_def) simp
  20.136  qed
  20.137  
    21.1 --- a/src/HOL/Library/Nat_Infinity.thy	Thu May 06 12:43:00 2004 +0200
    21.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 06 14:14:18 2004 +0200
    21.3 @@ -4,10 +4,7 @@
    21.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    21.5  *)
    21.6  
    21.7 -header {*
    21.8 -  \title{Natural numbers with infinity}
    21.9 -  \author{David von Oheimb}
   21.10 -*}
   21.11 +header {* Natural numbers with infinity *}
   21.12  
   21.13  theory Nat_Infinity = Main:
   21.14  
    22.1 --- a/src/HOL/Library/Nested_Environment.thy	Thu May 06 12:43:00 2004 +0200
    22.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu May 06 14:14:18 2004 +0200
    22.3 @@ -4,10 +4,7 @@
    22.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    22.5  *)
    22.6  
    22.7 -header {*
    22.8 -  \title{Nested environments}
    22.9 -  \author{Markus Wenzel}
   22.10 -*}
   22.11 +header {* Nested environments *}
   22.12  
   22.13  theory Nested_Environment = Main:
   22.14  
    23.1 --- a/src/HOL/Library/Permutation.thy	Thu May 06 12:43:00 2004 +0200
    23.2 +++ b/src/HOL/Library/Permutation.thy	Thu May 06 14:14:18 2004 +0200
    23.3 @@ -1,16 +1,13 @@
    23.4  (*  Title:      HOL/Library/Permutation.thy
    23.5      ID:         $Id$
    23.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 +    Author:     Lawrence C Paulson and Thomas M Rasmussen
    23.8      Copyright   1995  University of Cambridge
    23.9  
   23.10  TODO: it would be nice to prove (for "multiset", defined on
   23.11  HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x)
   23.12  *)
   23.13  
   23.14 -header {*
   23.15 - \title{Permutations}
   23.16 - \author{Lawrence C Paulson and Thomas M Rasmussen}
   23.17 -*}
   23.18 +header {* Permutations *}
   23.19  
   23.20  theory Permutation = Main:
   23.21  
    24.1 --- a/src/HOL/Library/Primes.thy	Thu May 06 12:43:00 2004 +0200
    24.2 +++ b/src/HOL/Library/Primes.thy	Thu May 06 14:14:18 2004 +0200
    24.3 @@ -4,10 +4,7 @@
    24.4      Copyright   1996  University of Cambridge
    24.5  *)
    24.6  
    24.7 -header {*
    24.8 -  \title{The Greatest Common Divisor and Euclid's algorithm}
    24.9 -  \author{Christophe Tabacznyj and Lawrence C Paulson}
   24.10 -*}
   24.11 +header {* The Greatest Common Divisor and Euclid's algorithm *}
   24.12  
   24.13  theory Primes = Main:
   24.14  
    25.1 --- a/src/HOL/Library/Quotient.thy	Thu May 06 12:43:00 2004 +0200
    25.2 +++ b/src/HOL/Library/Quotient.thy	Thu May 06 14:14:18 2004 +0200
    25.3 @@ -4,10 +4,7 @@
    25.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    25.5  *)
    25.6  
    25.7 -header {*
    25.8 -  \title{Quotient types}
    25.9 -  \author{Markus Wenzel}
   25.10 -*}
   25.11 +header {* Quotient types *}
   25.12  
   25.13  theory Quotient = Main:
   25.14  
    26.1 --- a/src/HOL/Library/While_Combinator.thy	Thu May 06 12:43:00 2004 +0200
    26.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu May 06 14:14:18 2004 +0200
    26.3 @@ -4,10 +4,7 @@
    26.4      Copyright   2000 TU Muenchen
    26.5  *)
    26.6  
    26.7 -header {*
    26.8 - \title{A general ``while'' combinator}
    26.9 - \author{Tobias Nipkow}
   26.10 -*}
   26.11 +header {* A general ``while'' combinator *}
   26.12  
   26.13  theory While_Combinator = Main:
   26.14  
    27.1 --- a/src/HOL/Library/Word.thy	Thu May 06 12:43:00 2004 +0200
    27.2 +++ b/src/HOL/Library/Word.thy	Thu May 06 14:14:18 2004 +0200
    27.3 @@ -3,10 +3,7 @@
    27.4      Author:     Sebastian Skalberg (TU Muenchen)
    27.5  *)
    27.6  
    27.7 -header {*
    27.8 -  \title{Binary Words}
    27.9 -  \author{Sebastian Skalberg}
   27.10 -*}
   27.11 +header {* Binary Words *}
   27.12  
   27.13  theory Word = Main files "word_setup.ML":
   27.14  
    28.1 --- a/src/HOL/Library/Zorn.thy	Thu May 06 12:43:00 2004 +0200
    28.2 +++ b/src/HOL/Library/Zorn.thy	Thu May 06 14:14:18 2004 +0200
    28.3 @@ -1,39 +1,40 @@
    28.4 -(*  Title       : Zorn.thy
    28.5 +(*  Title       : HOL/Library/Zorn.thy
    28.6      ID          : $Id$
    28.7      Author      : Jacques D. Fleuriot
    28.8 -    Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
    28.9 -*) 
   28.10 +    Description : Zorn's Lemma -- see Larry Paulson's Zorn.thy in ZF
   28.11 +*)
   28.12  
   28.13 -header {*Zorn's Lemma*}
   28.14 +header {* Zorn's Lemma *}
   28.15  
   28.16  theory Zorn = Main:
   28.17  
   28.18 -text{*The lemma and section numbers refer to an unpublished article ``Towards
   28.19 -the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
   28.20 -Abrial and Laffitte.  *}
   28.21 +text{*
   28.22 +  The lemma and section numbers refer to an unpublished article
   28.23 +  \cite{Abrial-Laffitte}.
   28.24 +*}
   28.25  
   28.26  constdefs
   28.27    chain     ::  "'a set set => 'a set set set"
   28.28 -    "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
   28.29 +  "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
   28.30  
   28.31    super     ::  "['a set set,'a set set] => 'a set set set"
   28.32 -    "super S c == {d. d \<in> chain(S) & c < d}"
   28.33 +  "super S c == {d. d \<in> chain S & c \<subset> d}"
   28.34  
   28.35    maxchain  ::  "'a set set => 'a set set set"
   28.36 -    "maxchain S == {c. c \<in> chain S & super S c = {}}"
   28.37 +  "maxchain S == {c. c \<in> chain S & super S c = {}}"
   28.38  
   28.39    succ      ::  "['a set set,'a set set] => 'a set set"
   28.40 -    "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
   28.41 -                 then c else (@c'. c': (super S c))" 
   28.42 +  "succ S c ==
   28.43 +    if c \<notin> chain S | c \<in> maxchain S
   28.44 +    then c else SOME c'. c' \<in> super S c"
   28.45  
   28.46 -consts 
   28.47 -  "TFin" ::  "'a set set => 'a set set set"
   28.48 +consts
   28.49 +  TFin :: "'a set set => 'a set set set"
   28.50  
   28.51 -inductive "TFin(S)"
   28.52 +inductive "TFin S"
   28.53    intros
   28.54      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
   28.55      Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
   28.56 -           
   28.57    monos          Pow_mono
   28.58  
   28.59  
   28.60 @@ -54,26 +55,26 @@
   28.61  
   28.62  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
   28.63  
   28.64 -lemma TFin_induct: 
   28.65 -          "[| n \<in> TFin S;  
   28.66 -             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);  
   28.67 -             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]  
   28.68 +lemma TFin_induct:
   28.69 +          "[| n \<in> TFin S;
   28.70 +             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
   28.71 +             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
   28.72            ==> P(n)"
   28.73  apply (erule TFin.induct, blast+)
   28.74  done
   28.75  
   28.76  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
   28.77 -apply (erule subset_trans) 
   28.78 -apply (rule Abrial_axiom1) 
   28.79 +apply (erule subset_trans)
   28.80 +apply (rule Abrial_axiom1)
   28.81  done
   28.82  
   28.83  text{*Lemma 1 of section 3.1*}
   28.84  lemma TFin_linear_lemma1:
   28.85 -     "[| n \<in> TFin S;  m \<in> TFin S;   
   28.86 -         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m  
   28.87 +     "[| n \<in> TFin S;  m \<in> TFin S;
   28.88 +         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
   28.89        |] ==> n \<subseteq> m | succ S m \<subseteq> n"
   28.90  apply (erule TFin_induct)
   28.91 -apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*}
   28.92 +apply (erule_tac [2] Union_lemma0) (*or just blast*)
   28.93  apply (blast del: subsetI intro: succ_trans)
   28.94  done
   28.95  
   28.96 @@ -82,20 +83,20 @@
   28.97       "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
   28.98  apply (erule TFin_induct)
   28.99  apply (rule impI [THEN ballI])
  28.100 -txt{*case split using TFin_linear_lemma1*}
  28.101 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
  28.102 +txt{*case split using @{text TFin_linear_lemma1}*}
  28.103 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
  28.104         assumption+)
  28.105  apply (drule_tac x = n in bspec, assumption)
  28.106 -apply (blast del: subsetI intro: succ_trans, blast) 
  28.107 +apply (blast del: subsetI intro: succ_trans, blast)
  28.108  txt{*second induction step*}
  28.109  apply (rule impI [THEN ballI])
  28.110  apply (rule Union_lemma0 [THEN disjE])
  28.111  apply (rule_tac [3] disjI2)
  28.112 - prefer 2 apply blast 
  28.113 + prefer 2 apply blast
  28.114  apply (rule ballI)
  28.115 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
  28.116 -       assumption+, auto) 
  28.117 -apply (blast intro!: Abrial_axiom1 [THEN subsetD])  
  28.118 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
  28.119 +       assumption+, auto)
  28.120 +apply (blast intro!: Abrial_axiom1 [THEN subsetD])
  28.121  done
  28.122  
  28.123  text{*Re-ordering the premises of Lemma 2*}
  28.124 @@ -107,10 +108,10 @@
  28.125  
  28.126  text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
  28.127  lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
  28.128 -apply (rule disjE) 
  28.129 +apply (rule disjE)
  28.130  apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
  28.131  apply (assumption+, erule disjI2)
  28.132 -apply (blast del: subsetI 
  28.133 +apply (blast del: subsetI
  28.134               intro: subsetI Abrial_axiom1 [THEN subset_trans])
  28.135  done
  28.136  
  28.137 @@ -130,12 +131,12 @@
  28.138  apply (erule ssubst)
  28.139  apply (rule Abrial_axiom1 [THEN equalityI])
  28.140  apply (blast del: subsetI
  28.141 -	     intro: subsetI TFin_UnionI TFin.succI)
  28.142 +             intro: subsetI TFin_UnionI TFin.succI)
  28.143  done
  28.144  
  28.145  subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
  28.146  
  28.147 -text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, 
  28.148 +text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
  28.149   the subset relation!*}
  28.150  
  28.151  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
  28.152 @@ -150,13 +151,13 @@
  28.153  lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
  28.154  by (unfold super_def maxchain_def, auto)
  28.155  
  28.156 -lemma select_super: "c \<in> chain S - maxchain S ==>  
  28.157 +lemma select_super: "c \<in> chain S - maxchain S ==>
  28.158                            (@c'. c': super S c): super S c"
  28.159  apply (erule mem_super_Ex [THEN exE])
  28.160  apply (rule someI2, auto)
  28.161  done
  28.162  
  28.163 -lemma select_not_equals: "c \<in> chain S - maxchain S ==>  
  28.164 +lemma select_not_equals: "c \<in> chain S - maxchain S ==>
  28.165                            (@c'. c': super S c) \<noteq> c"
  28.166  apply (rule notI)
  28.167  apply (drule select_super)
  28.168 @@ -180,26 +181,26 @@
  28.169  apply (unfold chain_def)
  28.170  apply (rule CollectI, safe)
  28.171  apply (drule bspec, assumption)
  28.172 -apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE], 
  28.173 +apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
  28.174         blast+)
  28.175  done
  28.176 - 
  28.177 +
  28.178  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
  28.179  apply (rule_tac x = "Union (TFin S) " in exI)
  28.180  apply (rule classical)
  28.181  apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
  28.182   prefer 2
  28.183 - apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric]) 
  28.184 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
  28.185  apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
  28.186  apply (drule DiffI [THEN succ_not_equals], blast+)
  28.187  done
  28.188  
  28.189  
  28.190 -subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then 
  28.191 +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
  28.192                                 There Is  a Maximal Element*}
  28.193  
  28.194 -lemma chain_extend: 
  28.195 -    "[| c \<in> chain S; z \<in> S;  
  28.196 +lemma chain_extend:
  28.197 +    "[| c \<in> chain S; z \<in> S;
  28.198          \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
  28.199  by (unfold chain_def, blast)
  28.200  
  28.201 @@ -237,16 +238,16 @@
  28.202       "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
  28.203        ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
  28.204  apply (cut_tac Hausdorff maxchain_subset_chain)
  28.205 -apply (erule exE) 
  28.206 -apply (drule subsetD, assumption) 
  28.207 -apply (drule bspec, assumption, erule bexE) 
  28.208 +apply (erule exE)
  28.209 +apply (drule subsetD, assumption)
  28.210 +apply (drule bspec, assumption, erule bexE)
  28.211  apply (rule_tac x = y in bexI)
  28.212   prefer 2 apply assumption
  28.213 -apply clarify 
  28.214 -apply (rule ccontr) 
  28.215 +apply clarify
  28.216 +apply (rule ccontr)
  28.217  apply (frule_tac z = x in chain_extend)
  28.218  apply (assumption, blast)
  28.219 -apply (unfold maxchain_def super_def psubset_def) 
  28.220 +apply (unfold maxchain_def super_def psubset_def)
  28.221  apply (blast elim!: equalityCE)
  28.222  done
  28.223  
  28.224 @@ -259,4 +260,3 @@
  28.225  by (unfold chain_def, blast)
  28.226  
  28.227  end
  28.228 -
    29.1 --- a/src/HOL/document/root.tex	Thu May 06 12:43:00 2004 +0200
    29.2 +++ b/src/HOL/document/root.tex	Thu May 06 14:14:18 2004 +0200
    29.3 @@ -24,8 +24,7 @@
    29.4  \newpage
    29.5  
    29.6  \renewcommand{\isamarkupheader}[1]%
    29.7 -{\section{\isabellecontext: #1}%
    29.8 -\markright{THEORY~``\isabellecontext''}}
    29.9 +{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
   29.10  
   29.11  \parindent 0pt\parskip 0.5ex
   29.12  \input{session}