# HG changeset patch # User wenzelm # Date 1083845658 -7200 # Node ID 71590b7733b70a5d05e930ad0b672b2e02738957 # Parent 14b2c22a7e402f9e19629d89b826a4fc1b7da20c tuned document; diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Bij.thy --- 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 *) diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Coset.thy --- 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 *) diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Exponent.thy --- 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 diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/FiniteProduct.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Group.thy --- 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 *} diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Lattice.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Module.thy --- 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 diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/Sylow.thy --- 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 diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/UnivPoly.thy --- 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. *} diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/document/root.bib --- /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} +} diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/document/root.tex --- 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} diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Accessible_Part.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Continuity.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/FuncSet.thy --- 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. \x. x \ A --> f(x) \ B(x)}" + Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" + "Pi A B == {f. \x. x \ A --> f x \ B x}" extensional :: "'a set => ('a => 'b) set" - "extensional A == {f. \x. x~:A --> f(x) = arbitrary}" + "extensional A == {f. \x. x~:A --> f x = arbitrary}" - restrict :: "['a => 'b, 'a set] => ('a => 'b)" - "restrict f A == (%x. if x \ A then f x else arbitrary)" + "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" + "restrict f A == (%x. if x \ 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\ _\_./ _)" 10) - funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\" 60) + funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\" 60) "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\_\_./ _)" [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 == \x\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 \ A ==> f x \ B x) ==> f \ Pi A B" -by (simp add: Pi_def) + by (simp add: Pi_def) lemma funcsetI: "(!!x. x \ A ==> f x \ B) ==> f \ A -> B" -by (simp add: Pi_def) + by (simp add: Pi_def) lemma Pi_mem: "[|f: Pi A B; x \ A|] ==> f x \ B x" -by (simp add: Pi_def) + by (simp add: Pi_def) lemma funcset_mem: "[|f \ A -> B; x \ A|] ==> f x \ B" -by (simp add: Pi_def) + by (simp add: Pi_def) lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\x\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 \ B u" in spec, auto) -apply (cut_tac P= "%y. y \ B x" in some_eq_ex, auto) +apply (cut_tac P= "%y. y \ 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 \ 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 \ A -> B; g \ B -> C |]==> compose A g f \ A -> C" -by (simp add: Pi_def compose_def restrict_def) +lemma funcset_compose: + "[| f \ A -> B; g \ B -> C |]==> compose A g f \ A -> C" + by (simp add: Pi_def compose_def restrict_def) lemma compose_assoc: - "[| f \ A -> B; g \ B -> C; h \ C -> D |] + "[| f \ A -> B; g \ B -> C; h \ 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 \ 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 \ A ==> f x \ B) ==> (\x\A. f x) \ A -> B" -by (simp add: Pi_def restrict_def) + by (simp add: Pi_def restrict_def) lemma restrictI: "(!!x. x \ A ==> f x \ B x) ==> (\x\A. f x) \ Pi A B" -by (simp add: Pi_def restrict_def) + by (simp add: Pi_def restrict_def) lemma restrict_apply [simp]: - "(\y\A. f y) x = (if x \ A then f x else arbitrary)" -by (simp add: restrict_def) + "(\y\A. f y) x = (if x \ A then f x else arbitrary)" + by (simp add: restrict_def) -lemma restrict_ext: +lemma restrict_ext: "(!!x. x \ A ==> f x = g x) ==> (\x\A. f x) = (\x\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 \ A -> B; f \ extensional A|] ==> compose A (\y\B. y) f = f" -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) + "[|f \ A -> B; f \ extensional A|] ==> compose A (\y\B. y) f = f" + by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) lemma compose_Id: - "[|g \ A -> B; g \ extensional A|] ==> compose A g (\x\A. x) = g" -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) + "[|g \ A -> B; g \ extensional A|] ==> compose A g (\x\A. x) = g" + by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) subsection{*Extensionality*} lemma extensional_arb: "[|f \ extensional A; x\ A|] ==> f x = arbitrary" -by (simp add: extensional_def) + by (simp add: extensional_def) lemma restrict_extensional [simp]: "restrict f A \ extensional A" -by (simp add: restrict_def extensional_def) + by (simp add: restrict_def extensional_def) lemma compose_extensional [simp]: "compose A f g \ extensional A" -by (simp add: compose_def) + by (simp add: compose_def) lemma extensionalityI: - "[| f \ extensional A; g \ extensional A; - !!x. x\A ==> f x = g x |] ==> f = g" -by (force simp add: expand_fun_eq extensional_def) + "[| f \ extensional A; g \ extensional A; + !!x. x\A ==> f x = g x |] ==> f = g" + by (force simp add: expand_fun_eq extensional_def) lemma Inv_funcset: "f ` A = B ==> (\x\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 (\y\B. Inv A f y) f = (\x\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 (\y\B. Inv A f y) = (\x\B. x)" -apply (simp add: compose_def) -apply (rule restrict_ext) -apply (simp add: f_Inv_f) -done + "f ` A = B ==> compose B f (\y\B. Inv A f y) = (\x\B. x)" + apply (simp add: compose_def) + apply (rule restrict_ext) + apply (simp add: f_Inv_f) + done end diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Library.thy --- 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 (*>*) diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Library/document/root.bib --- 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}, diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Library/document/root.tex --- 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} diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/List_Prefix.thy --- 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 == \zs. xs = zs @ ys" -lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def) -lemma postfix_trans: "\xs >= ys; ys >= zs\ \ xs >= zs" - by (auto simp add: postfix_def) -lemma postfix_antisym: "\xs >= ys; ys >= xs\ \ xs = ys" - by (auto simp add: postfix_def) +lemma postfix_refl [simp, intro!]: "xs >= xs" + by (auto simp add: postfix_def) +lemma postfix_trans: "\xs >= ys; ys >= zs\ \ xs >= zs" + by (auto simp add: postfix_def) +lemma postfix_antisym: "\xs >= ys; ys >= xs\ \ 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 \ x#xs >= ys" by (auto simp add: postfix_def) -lemma postfix_ConsD: "xs >= y#ys \ xs >= ys" by (auto simp add: postfix_def) +lemma postfix_ConsI: "xs >= ys \ x#xs >= ys" + by (auto simp add: postfix_def) +lemma postfix_ConsD: "xs >= y#ys \ xs >= ys" + by (auto simp add: postfix_def) -lemma postfix_appendI: "xs >= ys \ zs@xs >= ys" by(auto simp add: postfix_def) -lemma postfix_appendD: "xs >= zs@ys \ xs >= ys" by(auto simp add: postfix_def) +lemma postfix_appendI: "xs >= ys \ zs @ xs >= ys" + by (auto simp add: postfix_def) +lemma postfix_appendD: "xs >= zs @ ys \ xs >= ys" + by(auto simp add: postfix_def) lemma postfix_is_subset_lemma: "xs = zs @ ys \ set ys \ set xs" -by (induct zs, auto) + by (induct zs, auto) lemma postfix_is_subset: "xs >= ys \ set ys \ 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 \ 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 \ 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 diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Multiset.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/NatPair.thy --- 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 "\\"} to @{text + \}. Definition and proofs are from \cite[page + 85]{Oberschelp:1993}. +*} -constdefs +constdefs nat2_to_nat:: "(nat * nat) \ nat" "nat2_to_nat pair \ 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 \ x+y" proof (rule classical) assume "\ ?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 "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" - by (simp only: div_mult_self1_is_m) - also have "\ = (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 "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" + by (simp only: div_mult_self1_is_m) + also have "\ = (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 "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" - by (rule div_add1_eq[THEN sym]) - also have "\ = ((x+y+2)*Suc(x+y)) div 2" - by (simp only: add_mult_distrib[THEN sym]) - also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" - by (simp only: mult_le_mono div_le_mono) - also have "\ \ nat2_to_nat (u,v)" + qed + also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" + by (rule div_add1_eq [symmetric]) + also have "\ = ((x+y+2)*Suc(x+y)) div 2" + by (simp only: add_mult_distrib [symmetric]) + also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" + by (simp only: mult_le_mono div_le_mono) + also have "\ \ 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 \ x+y" by (rule nat2_to_nat_help) - also from prems[THEN sym] have "x+y \ u+v" + also from prems [symmetric] have "x+y \ 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 "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" + hence "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" by fast - thus ?thesis + thus ?thesis by (unfold inj_on_def) simp qed diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Nat_Infinity.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Nested_Environment.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Permutation.thy --- 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 = (\x. multiset xs x = multiset ys x) *) -header {* - \title{Permutations} - \author{Lawrence C Paulson and Thomas M Rasmussen} -*} +header {* Permutations *} theory Permutation = Main: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Primes.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Quotient.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/While_Combinator.thy --- 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: diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Word.thy --- 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": diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/Zorn.thy --- 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 \ S & (\x \ F. \y \ F. x \ y | y \ x)}" + "chain S == {F. F \ S & (\x \ F. \y \ F. x \ y | y \ x)}" super :: "['a set set,'a set set] => 'a set set set" - "super S c == {d. d \ chain(S) & c < d}" + "super S c == {d. d \ chain S & c \ d}" maxchain :: "'a set set => 'a set set set" - "maxchain S == {c. c \ chain S & super S c = {}}" + "maxchain S == {c. c \ chain S & super S c = {}}" succ :: "['a set set,'a set set] => 'a set set" - "succ S c == if (c \ chain S| c \ maxchain S) - then c else (@c'. c': (super S c))" + "succ S c == + if c \ chain S | c \ maxchain S + then c else SOME c'. c' \ 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 \ TFin S ==> succ S x \ TFin S" Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" - monos Pow_mono @@ -54,26 +55,26 @@ lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI] -lemma TFin_induct: - "[| n \ TFin S; - !!x. [| x \ TFin S; P(x) |] ==> P(succ S x); - !!Y. [| Y \ TFin S; Ball Y P |] ==> P(Union Y) |] +lemma TFin_induct: + "[| n \ TFin S; + !!x. [| x \ TFin S; P(x) |] ==> P(succ S x); + !!Y. [| Y \ TFin S; Ball Y P |] ==> P(Union Y) |] ==> P(n)" apply (erule TFin.induct, blast+) done lemma succ_trans: "x \ y ==> x \ 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 \ TFin S; m \ TFin S; - \x \ TFin S. x \ m --> x = m | succ S x \ m + "[| n \ TFin S; m \ TFin S; + \x \ TFin S. x \ m --> x = m | succ S x \ m |] ==> n \ m | succ S m \ 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 \ TFin S ==> \n \ TFin S. n \ m --> n=m | succ S n \ 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 \ TFin S; n \ TFin S|] ==> n \ m | m \ 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 "\"}, +text{*NB: We assume the partial ordering is @{text "\"}, the subset relation!*} lemma empty_set_mem_chain: "({} :: 'a set set) \ chain S" @@ -150,13 +151,13 @@ lemma mem_super_Ex: "c \ chain S - maxchain S ==> ? d. d \ super S c" by (unfold super_def maxchain_def, auto) -lemma select_super: "c \ chain S - maxchain S ==> +lemma select_super: "c \ 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 \ chain S - maxchain S ==> +lemma select_not_equals: "c \ chain S - maxchain S ==> (@c'. c': super S c) \ 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: "\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 \ chain S; z \ S; +lemma chain_extend: + "[| c \ chain S; z \ S; \x \ c. x<=(z:: 'a set) |] ==> {z} Un c \ chain S" by (unfold chain_def, blast) @@ -237,16 +238,16 @@ "\c \ chain S. \y \ S. \x \ c. x \ y ==> \y \ S. \x \ S. (y :: 'a set) \ 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 - diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/document/root.tex --- 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}