isabelle: src/HOLCF/Fix.thy@bc883b390d91 (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
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	definitions for fixed point operator and admissibility
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	*)
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	Fix = Cfun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	consts
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
1990 9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	15	iterate :: "nat=>('a->'a)=>'a=>'a"
9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	16	Ifix :: "('a->'a)=>'a"
9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	17	fix :: "('a->'a)->'a"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2640 diff changeset	18	adm :: "('a::cpo=>bool)=>bool"
1990 9e23119c0219 added comment on is_flat oheimb parents: 1825 diff changeset	19	admw :: "('a=>bool)=>bool"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	21	primrec
704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	22	iterate_0 "iterate 0 F x = x"
704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	23	iterate_Suc "iterate (Suc n) F x = F`(iterate n F x)"
704dd3a6d47d Adapted to new datatype package. berghofe parents: 4721 diff changeset	24
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	25	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	27	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	28	fix_def "fix == (LAM f. Ifix f)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
4721 c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin oheimb parents: 3842 diff changeset	30	adm_def "adm P == !Y. chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	31	(!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	32
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	33	admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
1479 21eb5e156d91 expanded tabs clasohm parents: 1410 diff changeset	34	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	35
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37

author	wenzelm
	Sat, 02 Sep 2000 21:49:51 +0200
changeset 9803	bc883b390d91
parent 5192	704dd3a6d47d
child 10834	a7897aebbffc
permissions	-rw-r--r--