isabelle: src/HOLCF/Fix.thy@ca23ee574faa (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
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	21	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	23	iterate_def "iterate n F c == nat_rec c (%n x. F`x) n"
b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	24	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	25	fix_def "fix == (LAM f. Ifix f)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	27	adm_def "adm P == !Y. is_chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	28	(!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	29
3842 b55686a7b22c fixed dots; wenzelm parents: 3326 diff changeset	30	admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
1479 21eb5e156d91 expanded tabs clasohm parents: 1410 diff changeset	31	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	32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34

author	wenzelm
	Fri, 17 Oct 1997 17:39:04 +0200
changeset 3922	ca23ee574faa
parent 3842	b55686a7b22c
child 4721	c8a8482a8124
permissions	-rw-r--r--