isabelle: src/HOLCF/One.thy@8b24773de6db (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/one.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: 1274 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
625 119391dd1d59 New version nipkow parents: 243 diff changeset	6	Introduce atomic type one = (void)u
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
625 119391dd1d59 New version nipkow parents: 243 diff changeset	8	The type is axiomatized as the least solution of a domain equation.
119391dd1d59 New version nipkow parents: 243 diff changeset	9	The functor term that specifies the domain equation is:
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
625 119391dd1d59 New version nipkow parents: 243 diff changeset	11	FT = <U,K_{void}>
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
625 119391dd1d59 New version nipkow parents: 243 diff changeset	13	For details see chapter 5 of:
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
625 119391dd1d59 New version nipkow parents: 243 diff changeset	15	[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
119391dd1d59 New version nipkow parents: 243 diff changeset	16	Dissertation, Technische Universit"at M"unchen, 1994
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20	One = ccc1+
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22	types one 0
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23	arities one :: pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25	consts
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	26	abs_one :: "(void)u -> one"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	27	rep_one :: "one -> (void)u"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	28	one :: "one"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	29	one_when :: "'c -> one -> 'c"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	rules
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	32	abs_one_iso "abs_one`(rep_one`u) = u"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	33	rep_one_iso "rep_one`(abs_one`x) = x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 625 diff changeset	35	defs
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	36	one_def "one == abs_one`(up`UU)"
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 625 diff changeset	37	one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	38
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	39	translations
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	40	"case l of one => t1" == "one_when`t1`l"
ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	41
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	44
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	46
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47

author	paulson
	Wed, 21 Aug 1996 13:22:23 +0200
changeset 1933	8b24773de6db
parent 1479	21eb5e156d91
child 2275	dbce3dce821a
permissions	-rw-r--r--