--- a/src/HOL/Algebra/Bij.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Bij.thy Thu May 06 14:14:18 2004 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Algebra/Bij
+(* Title: HOL/Algebra/Bij.thy
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
*)
--- a/src/HOL/Algebra/Coset.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy Thu May 06 14:14:18 2004 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/GroupTheory/Coset
+(* Title: HOL/Algebra/Coset.thy
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
*)
--- a/src/HOL/Algebra/Exponent.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Exponent.thy Thu May 06 14:14:18 2004 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/GroupTheory/Exponent
+(* Title: HOL/Algebra/Exponent.thy
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
--- a/src/HOL/Algebra/FiniteProduct.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Thu May 06 14:14:18 2004 +0200
@@ -1,11 +1,11 @@
-(* Title: Product Operator for Commutative Monoids
+(* Title: HOL/Algebra/FiniteProduct.thy
ID: $Id$
Author: Clemens Ballarin, started 19 November 2002
This file is largely based on HOL/Finite_Set.thy.
*)
-header {* Product Operator *}
+header {* Product Operator for Commutative Monoids *}
theory FiniteProduct = Group:
--- a/src/HOL/Algebra/Group.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Group.thy Thu May 06 14:14:18 2004 +0200
@@ -13,9 +13,9 @@
section {* From Magmas to Groups *}
text {*
- Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
- the exception of \emph{magma} which, following Bourbaki, is a set
- together with a binary, closed operation.
+ Definitions follow \cite{Jacobson:1985}; with the exception of
+ \emph{magma} which, following Bourbaki, is a set together with a
+ binary, closed operation.
*}
subsection {* Definitions *}
--- a/src/HOL/Algebra/Lattice.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy Thu May 06 14:14:18 2004 +0200
@@ -1,11 +1,11 @@
(*
- Title: Orders and Lattices
+ Title: HOL/Algebra/Lattice.thy
Id: $Id$
Author: Clemens Ballarin, started 7 November 2003
Copyright: Clemens Ballarin
*)
-header {* Order and Lattices *}
+header {* Orders and Lattices *}
theory Lattice = Group:
--- a/src/HOL/Algebra/Module.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Module.thy Thu May 06 14:14:18 2004 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Algebra/Module
+(* Title: HOL/Algebra/Module.thy
ID: $Id$
Author: Clemens Ballarin, started 15 April 2003
Copyright: Clemens Ballarin
--- a/src/HOL/Algebra/Sylow.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy Thu May 06 14:14:18 2004 +0200
@@ -1,17 +1,16 @@
-(* Title: HOL/GroupTheory/Sylow
+(* Title: HOL/Algebra/Sylow.thy
ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
-
-See Florian Kamm\"uller and L. C. Paulson,
- A Formal Proof of Sylow's theorem:
- An Experiment in Abstract Algebra with Isabelle HOL
- J. Automated Reasoning 23 (1999), 235-264
*)
-header{*Sylow's theorem using locales*}
+header {* Sylow's theorem *}
theory Sylow = Coset:
+text {*
+ See also \cite{Kammueller-Paulson:1999}.
+*}
+
subsection {*Order of a Group and Lagrange's Theorem*}
constdefs
--- a/src/HOL/Algebra/UnivPoly.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Thu May 06 14:14:18 2004 +0200
@@ -1,5 +1,5 @@
(*
- Title: Univariate Polynomials
+ Title: HOL/Algebra/UnivPoly.thy
Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
@@ -16,10 +16,9 @@
carrier set is a set of bounded functions from Nat to the
coefficient domain. Bounded means that these functions return zero
above a certain bound (the degree). There is a chapter on the
- formalisation of polynomials in my PhD thesis
- (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
- implemented with axiomatic type classes. This was later ported to
- Locales.
+ formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
+ which was implemented with axiomatic type classes. This was later
+ ported to Locales.
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/document/root.bib Thu May 06 14:14:18 2004 +0200
@@ -0,0 +1,25 @@
+
+@PhdThesis{Ballarin:1999,
+ author = {Clemens Ballarin},
+ title = {Computer Algebra and Theorem Proving},
+ school = {University of Cambridge},
+ year = 1999,
+ note = {\url{http://www4.in.tum.de/~ballarin/publications.html}}
+}
+
+@Book{Jacobson:1985,
+ author = {Nathan Jacobson},
+ title = {Basic Algebra I},
+ publisher = {Freeman},
+ year = 1985
+}
+
+@Article{Kammueller-Paulson:1999,
+ author = {Florian Kamm\"uller and L. C. Paulson},
+ title = {A Formal Proof of Sylow's theorem: An Experiment in
+ Abstract Algebra with {Isabelle HOL}},
+ journal = {J. Automated Reasoning},
+ year = 1999,
+ number = 23,
+ pages = {235--264}
+}
--- a/src/HOL/Algebra/document/root.tex Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Algebra/document/root.tex Thu May 06 14:14:18 2004 +0200
@@ -1,3 +1,5 @@
+
+% $Id$
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
@@ -10,21 +12,18 @@
% this should be the last package used
\usepackage{pdfsetup}
-% proper setup for best-style documents
\urlstyle{rm}
\isabellestyle{it}
-
-%\usepackage{substr}
-
-%\renewcommand{\isamarkupheader}[1]{%
-% \IfSubStringInString{Chapter: }{#1}{%
-% \chapter{\BehindSubString{Chapter: }{#1}}}{%
-% \section{#1}}}
-
+\pagestyle{myheadings}
\begin{document}
-\title{The Isabelle Algebra Library}
+\title{The Isabelle/HOL Algebra Library}
+\author{
+ Clemens Ballarin \\
+ Florian Kammu\"uller \\
+ Lawrence C Paulson \\
+}
\maketitle
\tableofcontents
@@ -35,8 +34,14 @@
\clearpage
+\renewcommand{\isamarkupheader}[1]%
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
\parindent 0pt\parskip 0.5ex
-
\input{session}
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}
--- a/src/HOL/Library/Accessible_Part.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Accessible_Part.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
Copyright 1994 University of Cambridge
*)
-header {*
- \title{The accessible part of a relation}
- \author{Lawrence C Paulson}
-*}
+header {* The accessible part of a relation *}
theory Accessible_Part = Main:
--- a/src/HOL/Library/Continuity.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Continuity.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Continuity and iterations (of set transformers)}
- \author{David von Oheimb}
-*}
+header {* Continuity and iterations (of set transformers) *}
theory Continuity = Main:
--- a/src/HOL/Library/FuncSet.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy Thu May 06 14:14:18 2004 +0200
@@ -3,22 +3,19 @@
Author: Florian Kammueller and Lawrence C Paulson
*)
-header {*
- \title{Pi and Function Sets}
- \author{Florian Kammueller and Lawrence C Paulson}
-*}
+header {* Pi and Function Sets *}
theory FuncSet = Main:
constdefs
- Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
- "Pi A B == {f. \<forall>x. x \<in> A --> f(x) \<in> B(x)}"
+ Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
+ "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
extensional :: "'a set => ('a => 'b) set"
- "extensional A == {f. \<forall>x. x~:A --> f(x) = arbitrary}"
+ "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
- restrict :: "['a => 'b, 'a set] => ('a => 'b)"
- "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
+ "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
+ "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
syntax
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
@@ -27,7 +24,7 @@
syntax (xsymbols)
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
- funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
+ funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
"@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
syntax (HTML output)
@@ -36,11 +33,11 @@
translations
"PI x:A. B" => "Pi A (%x. B)"
- "A -> B" => "Pi A (_K B)"
- "%x:A. f" == "restrict (%x. f) A"
+ "A -> B" => "Pi A (_K B)"
+ "%x:A. f" == "restrict (%x. f) A"
constdefs
- compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
+ "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
"compose A g f == \<lambda>x\<in>A. g (f x)"
print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
@@ -49,126 +46,123 @@
subsection{*Basic Properties of @{term Pi}*}
lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
apply (simp add: Pi_def, auto)
txt{*Converse direction requires Axiom of Choice to exhibit a function
picking an element from each non-empty @{term "B x"}*}
apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
-apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
+apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
done
lemma Pi_empty [simp]: "Pi {} B = UNIV"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
-by (simp add: Pi_def)
+ by (simp add: Pi_def)
text{*Covariance of Pi-sets in their second argument*}
lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
-by (simp add: Pi_def, blast)
+ by (simp add: Pi_def, blast)
text{*Contravariance of Pi-sets in their first argument*}
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
-by (simp add: Pi_def, blast)
+ by (simp add: Pi_def, blast)
subsection{*Composition With a Restricted Domain: @{term compose}*}
-lemma funcset_compose:
- "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
-by (simp add: Pi_def compose_def restrict_def)
+lemma funcset_compose:
+ "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
+ by (simp add: Pi_def compose_def restrict_def)
lemma compose_assoc:
- "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
+ "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
==> compose A h (compose A g f) = compose A (compose B h g) f"
-by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
+ by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
-by (simp add: compose_def restrict_def)
+ by (simp add: compose_def restrict_def)
lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
-by (auto simp add: image_def compose_eq)
+ by (auto simp add: image_def compose_eq)
lemma inj_on_compose:
- "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
-by (auto simp add: inj_on_def compose_eq)
+ "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
+ by (auto simp add: inj_on_def compose_eq)
subsection{*Bounded Abstraction: @{term restrict}*}
lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
-by (simp add: Pi_def restrict_def)
+ by (simp add: Pi_def restrict_def)
lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
-by (simp add: Pi_def restrict_def)
+ by (simp add: Pi_def restrict_def)
lemma restrict_apply [simp]:
- "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
-by (simp add: restrict_def)
+ "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
+ by (simp add: restrict_def)
-lemma restrict_ext:
+lemma restrict_ext:
"(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
-by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
+ by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
-by (simp add: inj_on_def restrict_def)
-
+ by (simp add: inj_on_def restrict_def)
lemma Id_compose:
- "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
-by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
+ "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
+ by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
lemma compose_Id:
- "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
-by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
+ "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
+ by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
subsection{*Extensionality*}
lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
-by (simp add: extensional_def)
+ by (simp add: extensional_def)
lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
-by (simp add: restrict_def extensional_def)
+ by (simp add: restrict_def extensional_def)
lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
-by (simp add: compose_def)
+ by (simp add: compose_def)
lemma extensionalityI:
- "[| f \<in> extensional A; g \<in> extensional A;
- !!x. x\<in>A ==> f x = g x |] ==> f = g"
-by (force simp add: expand_fun_eq extensional_def)
+ "[| f \<in> extensional A; g \<in> extensional A;
+ !!x. x\<in>A ==> f x = g x |] ==> f = g"
+ by (force simp add: expand_fun_eq extensional_def)
lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
-apply (unfold Inv_def)
-apply (fast intro: restrict_in_funcset someI2)
-done
+ by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
lemma compose_Inv_id:
- "[| inj_on f A; f ` A = B |]
+ "[| inj_on f A; f ` A = B |]
==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
-apply (simp add: compose_def)
-apply (rule restrict_ext, auto)
-apply (erule subst)
-apply (simp add: Inv_f_f)
-done
+ apply (simp add: compose_def)
+ apply (rule restrict_ext, auto)
+ apply (erule subst)
+ apply (simp add: Inv_f_f)
+ done
lemma compose_id_Inv:
- "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
-apply (simp add: compose_def)
-apply (rule restrict_ext)
-apply (simp add: f_Inv_f)
-done
+ "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
+ apply (simp add: compose_def)
+ apply (rule restrict_ext)
+ apply (simp add: f_Inv_f)
+ done
end
--- a/src/HOL/Library/Library.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Library.thy Thu May 06 14:14:18 2004 +0200
@@ -1,16 +1,18 @@
(*<*)
theory Library =
- Quotient +
- Nat_Infinity +
- List_Prefix +
- Nested_Environment +
Accessible_Part +
Continuity +
+ FuncSet +
+ List_Prefix +
Multiset +
- Permutation +
NatPair +
+ Nat_Infinity +
+ Nested_Environment +
+ Permutation +
Primes +
+ Quotient +
+ While_Combinator +
Word +
- While_Combinator:
+ Zorn:
end
(*>*)
--- a/src/HOL/Library/Library/document/root.bib Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Library/document/root.bib Thu May 06 14:14:18 2004 +0200
@@ -1,3 +1,17 @@
+
+ @Unpublished{Abrial-Laffitte,
+ author = {Abrial and Laffitte},
+ title = {Towards the Mechanization of the Proofs of
+ Some Classical Theorems of Set Theory},
+ note = {Unpublished}
+}
+
+@Book{Oberschelp:1993,
+ author = {Arnold Oberschelp},
+ title = {Rekursionstheorie},
+ publisher = {BI-Wissenschafts-Verlag},
+ year = 1993
+}
@Book{davenport92,
author = {H. Davenport},
--- a/src/HOL/Library/Library/document/root.tex Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Library/document/root.tex Thu May 06 14:14:18 2004 +0200
@@ -15,6 +15,7 @@
\title{The Supplemental Isabelle/HOL Library}
\author{
Gertrud Bauer \\
+ Jacques D Fleuriot \\
Tobias Nipkow \\
David von Oheimb \\
Lawrence C Paulson \\
@@ -28,16 +29,8 @@
\tableofcontents
\newpage
-%now hack the "header" markup to support \title and \author
-\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
-\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
\renewcommand{\isamarkupheader}[1]%
-{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
-#1%
-\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
-\markright{THEORY~``\isabellecontext''}%
-\ifthenelse{\equal{}{\isabelleauthor}}{}%
-{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
\parindent 0pt \parskip 0.5ex
\input{session}
--- a/src/HOL/Library/List_Prefix.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/List_Prefix.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{List prefixes and postfixes}
- \author{Tobias Nipkow and Markus Wenzel}
-*}
+header {* List prefixes and postfixes *}
theory List_Prefix = Main:
@@ -222,36 +219,43 @@
postfix :: "'a list => 'a list => bool" ("(_/ >= _)" [51, 50] 50)
"xs >= ys == \<exists>zs. xs = zs @ ys"
-lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def)
-lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs"
- by (auto simp add: postfix_def)
-lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys"
- by (auto simp add: postfix_def)
+lemma postfix_refl [simp, intro!]: "xs >= xs"
+ by (auto simp add: postfix_def)
+lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs"
+ by (auto simp add: postfix_def)
+lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys"
+ by (auto simp add: postfix_def)
-lemma Nil_postfix [iff]: "xs >= []" by (simp add: postfix_def)
-lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"by (auto simp add:postfix_def)
+lemma Nil_postfix [iff]: "xs >= []"
+ by (simp add: postfix_def)
+lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"
+ by (auto simp add:postfix_def)
-lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" by (auto simp add: postfix_def)
-lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" by (auto simp add: postfix_def)
+lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys"
+ by (auto simp add: postfix_def)
+lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys"
+ by (auto simp add: postfix_def)
-lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs@xs >= ys" by(auto simp add: postfix_def)
-lemma postfix_appendD: "xs >= zs@ys \<Longrightarrow> xs >= ys" by(auto simp add: postfix_def)
+lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys"
+ by (auto simp add: postfix_def)
+lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys"
+ by(auto simp add: postfix_def)
lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
-by (induct zs, auto)
+ by (induct zs, auto)
lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
-by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
+ by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
-by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
+ by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
-by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
+ by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
-apply (unfold prefix_def postfix_def, safe)
-apply (rule_tac x = "rev zs" in exI, simp)
-apply (rule_tac x = "rev zs" in exI)
-apply (rule rev_is_rev_conv [THEN iffD1], simp)
-done
+ apply (unfold prefix_def postfix_def, safe)
+ apply (rule_tac x = "rev zs" in exI, simp)
+ apply (rule_tac x = "rev zs" in exI)
+ apply (rule rev_is_rev_conv [THEN iffD1], simp)
+ done
end
--- a/src/HOL/Library/Multiset.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Multiset.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Multisets}
- \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson}
-*}
+header {* Multisets *}
theory Multiset = Accessible_Part:
--- a/src/HOL/Library/NatPair.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/NatPair.thy Thu May 06 14:14:18 2004 +0200
@@ -4,89 +4,89 @@
Copyright 2003 Technische Universitaet Muenchen
*)
-header {*
- \title{Pairs of Natural Numbers}
- \author{Stefan Richter}
-*}
+header {* Pairs of Natural Numbers *}
theory NatPair = Main:
-text{*An injective function from $\mathbf{N}^2$ to
- $\mathbf{N}$. Definition and proofs are from
- Arnold Oberschelp. Rekursionstheorie. BI-Wissenschafts-Verlag, 1993
- (page 85). *}
+text{*
+ An injective function from @{text "\<nat>\<twosuperior>"} to @{text
+ \<nat>}. Definition and proofs are from \cite[page
+ 85]{Oberschelp:1993}.
+*}
-constdefs
+constdefs
nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
"nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
-lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
-proof (cases "2 dvd a")
+lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
+proof (cases "2 dvd a")
case True
thus ?thesis by (rule dvd_mult2)
next
- case False
+ case False
hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
- hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
- hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
+ hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
+ hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
thus ?thesis by (rule dvd_mult)
qed
-lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
+lemma
+ assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
shows nat2_to_nat_help: "u+v \<le> x+y"
proof (rule classical)
assume "\<not> ?thesis"
- hence contrapos: "x+y < u+v"
+ hence contrapos: "x+y < u+v"
by simp
- have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
+ have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
by (unfold nat2_to_nat_def) (simp add: Let_def)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
- by (simp only: div_mult_self1_is_m)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
- + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
+ also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
+ by (simp only: div_mult_self1_is_m)
+ also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
+ + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
proof -
- have "2 dvd (x+y)*Suc(x+y)"
+ have "2 dvd (x+y)*Suc(x+y)"
by (rule dvd2_a_x_suc_a)
- hence "(x+y)*Suc(x+y) mod 2 = 0"
+ hence "(x+y)*Suc(x+y) mod 2 = 0"
by (simp only: dvd_eq_mod_eq_0)
also
- have "2 * Suc(x+y) mod 2 = 0"
+ have "2 * Suc(x+y) mod 2 = 0"
by (rule mod_mult_self1_is_0)
- ultimately have
- "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
- by simp
- thus ?thesis
+ ultimately have
+ "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
+ by simp
+ thus ?thesis
by simp
- qed
- also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
- by (rule div_add1_eq[THEN sym])
- also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
- by (simp only: add_mult_distrib[THEN sym])
- also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
- by (simp only: mult_le_mono div_le_mono)
- also have "\<dots> \<le> nat2_to_nat (u,v)"
+ qed
+ also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
+ by (rule div_add1_eq [symmetric])
+ also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
+ by (simp only: add_mult_distrib [symmetric])
+ also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
+ by (simp only: mult_le_mono div_le_mono)
+ also have "\<dots> \<le> nat2_to_nat (u,v)"
by (unfold nat2_to_nat_def) (simp add: Let_def)
- finally show ?thesis
+ finally show ?thesis
by (simp only: eq)
qed
-lemma nat2_to_nat_inj: "inj nat2_to_nat"
+theorem nat2_to_nat_inj: "inj nat2_to_nat"
proof -
- {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
+ {
+ fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
- also from prems[THEN sym] have "x+y \<le> u+v"
+ also from prems [symmetric] have "x+y \<le> u+v"
by (rule nat2_to_nat_help)
finally have eq: "u+v = x+y" .
- with prems have ux: "u=x"
+ with prems have ux: "u=x"
by (simp add: nat2_to_nat_def Let_def)
- with eq have vy: "v=y"
+ with eq have vy: "v=y"
by simp
- with ux have "(u,v) = (x,y)"
+ with ux have "(u,v) = (x,y)"
by simp
}
- hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
+ hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
by fast
- thus ?thesis
+ thus ?thesis
by (unfold inj_on_def) simp
qed
--- a/src/HOL/Library/Nat_Infinity.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Natural numbers with infinity}
- \author{David von Oheimb}
-*}
+header {* Natural numbers with infinity *}
theory Nat_Infinity = Main:
--- a/src/HOL/Library/Nested_Environment.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Nested environments}
- \author{Markus Wenzel}
-*}
+header {* Nested environments *}
theory Nested_Environment = Main:
--- a/src/HOL/Library/Permutation.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Permutation.thy Thu May 06 14:14:18 2004 +0200
@@ -1,16 +1,13 @@
(* Title: HOL/Library/Permutation.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson and Thomas M Rasmussen
Copyright 1995 University of Cambridge
TODO: it would be nice to prove (for "multiset", defined on
HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x)
*)
-header {*
- \title{Permutations}
- \author{Lawrence C Paulson and Thomas M Rasmussen}
-*}
+header {* Permutations *}
theory Permutation = Main:
--- a/src/HOL/Library/Primes.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Primes.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
Copyright 1996 University of Cambridge
*)
-header {*
- \title{The Greatest Common Divisor and Euclid's algorithm}
- \author{Christophe Tabacznyj and Lawrence C Paulson}
-*}
+header {* The Greatest Common Divisor and Euclid's algorithm *}
theory Primes = Main:
--- a/src/HOL/Library/Quotient.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Quotient.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Quotient types}
- \author{Markus Wenzel}
-*}
+header {* Quotient types *}
theory Quotient = Main:
--- a/src/HOL/Library/While_Combinator.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy Thu May 06 14:14:18 2004 +0200
@@ -4,10 +4,7 @@
Copyright 2000 TU Muenchen
*)
-header {*
- \title{A general ``while'' combinator}
- \author{Tobias Nipkow}
-*}
+header {* A general ``while'' combinator *}
theory While_Combinator = Main:
--- a/src/HOL/Library/Word.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Word.thy Thu May 06 14:14:18 2004 +0200
@@ -3,10 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-header {*
- \title{Binary Words}
- \author{Sebastian Skalberg}
-*}
+header {* Binary Words *}
theory Word = Main files "word_setup.ML":
--- a/src/HOL/Library/Zorn.thy Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/Library/Zorn.thy Thu May 06 14:14:18 2004 +0200
@@ -1,39 +1,40 @@
-(* Title : Zorn.thy
+(* Title : HOL/Library/Zorn.thy
ID : $Id$
Author : Jacques D. Fleuriot
- Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
-*)
+ Description : Zorn's Lemma -- see Larry Paulson's Zorn.thy in ZF
+*)
-header {*Zorn's Lemma*}
+header {* Zorn's Lemma *}
theory Zorn = Main:
-text{*The lemma and section numbers refer to an unpublished article ``Towards
-the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
-Abrial and Laffitte. *}
+text{*
+ The lemma and section numbers refer to an unpublished article
+ \cite{Abrial-Laffitte}.
+*}
constdefs
chain :: "'a set set => 'a set set set"
- "chain S == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
+ "chain S == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
super :: "['a set set,'a set set] => 'a set set set"
- "super S c == {d. d \<in> chain(S) & c < d}"
+ "super S c == {d. d \<in> chain S & c \<subset> d}"
maxchain :: "'a set set => 'a set set set"
- "maxchain S == {c. c \<in> chain S & super S c = {}}"
+ "maxchain S == {c. c \<in> chain S & super S c = {}}"
succ :: "['a set set,'a set set] => 'a set set"
- "succ S c == if (c \<notin> chain S| c \<in> maxchain S)
- then c else (@c'. c': (super S c))"
+ "succ S c ==
+ if c \<notin> chain S | c \<in> maxchain S
+ then c else SOME c'. c' \<in> super S c"
-consts
- "TFin" :: "'a set set => 'a set set set"
+consts
+ TFin :: "'a set set => 'a set set set"
-inductive "TFin(S)"
+inductive "TFin S"
intros
succI: "x \<in> TFin S ==> succ S x \<in> TFin S"
Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
-
monos Pow_mono
@@ -54,26 +55,26 @@
lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
-lemma TFin_induct:
- "[| n \<in> TFin S;
- !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
- !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
+lemma TFin_induct:
+ "[| n \<in> TFin S;
+ !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
+ !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
==> P(n)"
apply (erule TFin.induct, blast+)
done
lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
-apply (erule subset_trans)
-apply (rule Abrial_axiom1)
+apply (erule subset_trans)
+apply (rule Abrial_axiom1)
done
text{*Lemma 1 of section 3.1*}
lemma TFin_linear_lemma1:
- "[| n \<in> TFin S; m \<in> TFin S;
- \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
+ "[| n \<in> TFin S; m \<in> TFin S;
+ \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
|] ==> n \<subseteq> m | succ S m \<subseteq> n"
apply (erule TFin_induct)
-apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*}
+apply (erule_tac [2] Union_lemma0) (*or just blast*)
apply (blast del: subsetI intro: succ_trans)
done
@@ -82,20 +83,20 @@
"m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
apply (erule TFin_induct)
apply (rule impI [THEN ballI])
-txt{*case split using TFin_linear_lemma1*}
-apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
+txt{*case split using @{text TFin_linear_lemma1}*}
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
assumption+)
apply (drule_tac x = n in bspec, assumption)
-apply (blast del: subsetI intro: succ_trans, blast)
+apply (blast del: subsetI intro: succ_trans, blast)
txt{*second induction step*}
apply (rule impI [THEN ballI])
apply (rule Union_lemma0 [THEN disjE])
apply (rule_tac [3] disjI2)
- prefer 2 apply blast
+ prefer 2 apply blast
apply (rule ballI)
-apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
- assumption+, auto)
-apply (blast intro!: Abrial_axiom1 [THEN subsetD])
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
+ assumption+, auto)
+apply (blast intro!: Abrial_axiom1 [THEN subsetD])
done
text{*Re-ordering the premises of Lemma 2*}
@@ -107,10 +108,10 @@
text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
lemma TFin_subset_linear: "[| m \<in> TFin S; n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
-apply (rule disjE)
+apply (rule disjE)
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
apply (assumption+, erule disjI2)
-apply (blast del: subsetI
+apply (blast del: subsetI
intro: subsetI Abrial_axiom1 [THEN subset_trans])
done
@@ -130,12 +131,12 @@
apply (erule ssubst)
apply (rule Abrial_axiom1 [THEN equalityI])
apply (blast del: subsetI
- intro: subsetI TFin_UnionI TFin.succI)
+ intro: subsetI TFin_UnionI TFin.succI)
done
subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
-text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
+text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
the subset relation!*}
lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
@@ -150,13 +151,13 @@
lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
by (unfold super_def maxchain_def, auto)
-lemma select_super: "c \<in> chain S - maxchain S ==>
+lemma select_super: "c \<in> chain S - maxchain S ==>
(@c'. c': super S c): super S c"
apply (erule mem_super_Ex [THEN exE])
apply (rule someI2, auto)
done
-lemma select_not_equals: "c \<in> chain S - maxchain S ==>
+lemma select_not_equals: "c \<in> chain S - maxchain S ==>
(@c'. c': super S c) \<noteq> c"
apply (rule notI)
apply (drule select_super)
@@ -180,26 +181,26 @@
apply (unfold chain_def)
apply (rule CollectI, safe)
apply (drule bspec, assumption)
-apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
+apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
blast+)
done
-
+
theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
apply (rule_tac x = "Union (TFin S) " in exI)
apply (rule classical)
apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
prefer 2
- apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
+ apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
apply (drule DiffI [THEN succ_not_equals], blast+)
done
-subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
+subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
There Is a Maximal Element*}
-lemma chain_extend:
- "[| c \<in> chain S; z \<in> S;
+lemma chain_extend:
+ "[| c \<in> chain S; z \<in> S;
\<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
by (unfold chain_def, blast)
@@ -237,16 +238,16 @@
"\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
apply (cut_tac Hausdorff maxchain_subset_chain)
-apply (erule exE)
-apply (drule subsetD, assumption)
-apply (drule bspec, assumption, erule bexE)
+apply (erule exE)
+apply (drule subsetD, assumption)
+apply (drule bspec, assumption, erule bexE)
apply (rule_tac x = y in bexI)
prefer 2 apply assumption
-apply clarify
-apply (rule ccontr)
+apply clarify
+apply (rule ccontr)
apply (frule_tac z = x in chain_extend)
apply (assumption, blast)
-apply (unfold maxchain_def super_def psubset_def)
+apply (unfold maxchain_def super_def psubset_def)
apply (blast elim!: equalityCE)
done
@@ -259,4 +260,3 @@
by (unfold chain_def, blast)
end
-
--- a/src/HOL/document/root.tex Thu May 06 12:43:00 2004 +0200
+++ b/src/HOL/document/root.tex Thu May 06 14:14:18 2004 +0200
@@ -24,8 +24,7 @@
\newpage
\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}%
-\markright{THEORY~``\isabellecontext''}}
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
\parindent 0pt\parskip 0.5ex
\input{session}