isabelle: src/HOL/GroupTheory/Sylow.thy@ae66c22ed52e (annotated)

11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	1	(* Title: HOL/GroupTheory/Sylow
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	2	ID: $Id$
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	3	Author: Florian Kammueller, with new proofs by L C Paulson
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	4	Copyright 1998-2001 University of Cambridge
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	5
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	6	Sylow's theorem using locales (combinatorial argument in Exponent.thy)
11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: 11394 diff changeset	7
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: 11394 diff changeset	8	See Florian Kamm\"uller and L. C. Paulson,
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: 11394 diff changeset	9	A Formal Proof of Sylow's theorem:
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: 11394 diff changeset	10	An Experiment in Abstract Algebra with Isabelle HOL
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: 11394 diff changeset	11	J. Automated Reasoning 23 (1999), 235-264
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	12	*)
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	13
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	14	Sylow = Coset +
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	15
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	16	locale sylow = coset +
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	17	fixes
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	18	p :: "nat"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	19	a :: "nat"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	20	m :: "nat"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	21	calM :: "'a set set"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	22	RelM :: "('a set * 'a set)set"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	23	assumes
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	24	prime_p "p\\<in>prime"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	25	order_G "order(G) = (p^a) * m"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	26	finite_G "finite (carrier G)"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	27	defines
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	28	calM_def "calM == {s. s <= carrier(G) & card(s) = p^a}"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	29	RelM_def "RelM == {(N1,N2). (N1,N2) \\<in> calM \\<times> calM &
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	30	(\\<exists>g \\<in> carrier(G). N1 = (N2 #> g) )}"
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	31
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	32	locale sylow_central = sylow +
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	33	fixes
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	34	H :: "'a set"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	35	M :: "'a set set"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	36	M1 :: "'a set"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	37	assumes
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	38	M_in_quot "M \\<in> calM // RelM"
11468 02cd5d5bc497 Tweaks for 1 -> 1' paulson parents: 11443 diff changeset	39	not_dvd_M "~(p ^ Suc(exponent p m) dvd card(M))"
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	40	M1_in_M "M1 \\<in> M"
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	41	defines
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	42	H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	43
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	44	end

author	paulson
	Wed, 26 Jun 2002 10:26:46 +0200
changeset 13248	ae66c22ed52e
parent 11468	02cd5d5bc497
child 13583	5fcc8bf538ee
permissions	-rw-r--r--