isabelle: src/HOLCF/Fix.thy@663e0e435866 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	1	(* Title: HOLCF/Fix.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1410 diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 10834 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	definitions for fixed point operator and admissibility
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	Fix = Cfun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	consts
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
1990 9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	13	iterate :: "nat=>('a->'a)=>'a=>'a"
9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	14	Ifix :: "('a->'a)=>'a"
9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	15	fix :: "('a->'a)->'a"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2640 diff changeset	16	adm :: "('a::cpo=>bool)=>bool"
1990 9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	17	admw :: "('a=>bool)=>bool"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	19	primrec
704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	20	iterate_0 "iterate 0 F x = x"
10834 a7897aebbffc * empty log message * nipkow parents: 5192 diff changeset	21	iterate_Suc "iterate (Suc n) F x = F$(iterate n F x)"
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	22
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	23	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	24
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	25	Ifix_def "Ifix F == lub(range(%i. iterate i F UU))"
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	26	fix_def "fix == (LAM f. Ifix f)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 3842 diff changeset	28	adm_def "adm P == !Y. chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	29	(!i. P(Y i)) --> P(lub(range Y))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	31	admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
1479 21eb5e156d91 expanded tabs clasohm parents: 1410 diff changeset	32	P (lub(range (%i. iterate i F UU)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35

author	wenzelm
	Fri, 16 Apr 2004 21:03:40 +0200
changeset 14609	663e0e435866
parent 12030	46d57d0290a2
child 14981	e73f8140af78
permissions	-rw-r--r--