summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOLCF/One.thy

author | nipkow |

Wed Jan 19 17:35:01 1994 +0100 (1994-01-19) | |

changeset 243 | c22b85994e17 |

child 625 | 119391dd1d59 |

permissions | -rw-r--r-- |

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF

in HOL.

in HOL.

1 (* Title: HOLCF/one.thy

2 ID: $Id$

3 Author: Franz Regensburger

4 Copyright 1993 Technische Universitaet Muenchen

6 Introduve atomic type one = (void)u

8 This is the first type that is introduced using a domain isomorphism.

9 The type axiom

11 arities one :: pcpo

13 and the continuity of the Isomorphisms are taken for granted. Since the

14 type is not recursive, it could be easily introduced in a purely conservative

15 style as it was used for the types sprod, ssum, lift. The definition of the

16 ordering is canonical using abstraction and representation, but this would take

17 again a lot of internal constants. It can easily be seen that the axioms below

18 are consistent.

20 The partial ordering on type one is implicitly defined via the

21 isomorphism axioms and the continuity of abs_one and rep_one.

23 We could also introduce the function less_one with definition

25 less_one(x,y) = rep_one[x] << rep_one[y]

28 *)

30 One = ccc1+

32 types one 0

33 arities one :: pcpo

35 consts

36 abs_one :: "(void)u -> one"

37 rep_one :: "one -> (void)u"

38 one :: "one"

39 one_when :: "'c -> one -> 'c"

41 rules

42 abs_one_iso "abs_one[rep_one[u]] = u"

43 rep_one_iso "rep_one[abs_one[x]] = x"

45 one_def "one == abs_one[up[UU]]"

46 one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"

48 end