isabelle: src/ZF/AC/recfunAC16.thy@b50b8c0eec01 (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
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	8	recfunAC16 = Cardinal + Epsilon +
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	9
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	10	constdefs
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	11	recfunAC16 :: [i, i, i, i] => i
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	12
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	13	"recfunAC16(f,fa,i,a) ==
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	14	transrec2(i, 0,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	15	%g r. if(EX y:r. fa`g <= y, r,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	16	r Un {f`(LEAST i. fa`g <= f`i &
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	17	(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	18
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	19	end

author	paulson
	Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469	b50b8c0eec01
parent 1478	2b8c2a7547ab
child 11317	7f9e4c389318
permissions	-rw-r--r--