isabelle: src/ZF/AC/recfunAC16.thy@00ac25b2791d (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/AC/recfunAC16.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
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	4
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	5	A recursive definition used in the proof of WO2 ==> AC16
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	recfunAC16 = Transrec2 + Cardinal +
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	9
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	10	consts
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	11
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1204 diff changeset	12	recfunAC16 :: [i, i, i, i] => i
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	13
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	14	defs
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	15
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	16	recfunAC16_def
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	17	"recfunAC16(f,fa,i,a) ==
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	18	transrec2(i, 0,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	19	%g r. if(EX y:r. fa`g <= y, r,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	r Un {f`(LEAST i. fa`g <= f`i &
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	21	(ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	22
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	23	end

author	paulson
	Thu, 05 Dec 1996 19:03:38 +0100
changeset 2327	00ac25b2791d
parent 1478	2b8c2a7547ab
child 2469	b50b8c0eec01
permissions	-rw-r--r--