isabelle: src/ZF/AC/AC16_WO4.thy@a196b944569b (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/AC/AC16_WO4.thy
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Krzysztof Grabczewski
5284 c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	4
5314 c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	5	Tidied using locales by LCP
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	6	*)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	7
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	8	AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	9
5284 c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	10	locale AC16 =
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	11	fixes
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	12	x :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	13	y :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	14	k :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	15	l :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	16	m :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	17	t_n :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	18	R :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	19	MM :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	20	LL :: i
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	21	GG :: i
5314 c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	22	s :: i=>i
5284 c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	23	assumes
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	24	all_ex "ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}.
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	25	EX! w. w:t_n & z <= w "
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	26	disjoint "x Int y = 0"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	27	includes "t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	28	WO_R "well_ord(y,R)"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	29	lnat "l:nat"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	30	mnat "m:nat"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	31	mpos "0<m"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	32	Infinite "~ Finite(y)"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	33	noLepoll "~ y lepoll {v:Pow(x). v eqpoll m}"
c77e9dd9bafc Tidying of AC, especially of AC16_WO4 using a locale paulson parents: 1478 diff changeset	34	defines
5314 c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	35	k_def "k == succ(l)"
c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	36	MM_def "MM == {v:t_n. succ(k) lepoll v Int y}"
c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	37	LL_def "LL == {v Int y. v:MM}"
c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	38	GG_def "GG == lam v:LL. (THE w. w:MM & v <= w) - v"
c061e6f9d546 Moved the definition of s_u (as s) into the locale paulson parents: 5284 diff changeset	39	s_def "s(u) == {v:t_n. u:v & k lepoll v Int y}"
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	40
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	41	end

author	paulson
	Wed, 13 Dec 2000 10:34:45 +0100
changeset 10660	a196b944569b
parent 5314	c061e6f9d546
child 11317	7f9e4c389318
permissions	-rw-r--r--