equal
deleted
inserted
replaced
1 (* Title: HOLCF/one.thy |
1 (* Title: HOLCF/One.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Oscar Slotosch |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
|
6 Introduce atomic type one = (void)u |
|
7 |
|
8 The type is axiomatized as the least solution of a domain equation. |
|
9 The functor term that specifies the domain equation is: |
|
10 |
|
11 FT = <U,K_{void}> |
|
12 |
|
13 For details see chapter 5 of: |
|
14 |
|
15 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, |
|
16 Dissertation, Technische Universit"at M"unchen, 1994 |
|
17 |
|
18 *) |
5 *) |
19 |
6 |
20 One = ccc1+ |
7 One = Lift + |
21 |
8 |
22 types one 0 |
9 types one = "unit lift" |
23 arities one :: pcpo |
|
24 |
10 |
25 consts |
11 consts |
26 abs_one :: "(void)u -> one" |
12 ONE :: "one" |
27 rep_one :: "one -> (void)u" |
13 |
28 one :: "one" |
14 translations |
29 one_when :: "'c -> one -> 'c" |
15 "one" == (type) "unit lift" |
30 |
16 |
31 rules |
17 rules |
32 abs_one_iso "abs_one`(rep_one`u) = u" |
18 ONE_def "ONE == Def()" |
33 rep_one_iso "rep_one`(abs_one`x) = x" |
|
34 |
|
35 defs |
|
36 one_def "one == abs_one`(up`UU)" |
|
37 one_when_def "one_when == (LAM c u.fup`(LAM x.c)`(rep_one`u))" |
|
38 |
|
39 translations |
|
40 "case l of one => t1" == "one_when`t1`l" |
|
41 |
|
42 end |
19 end |
43 |
20 |
44 |
21 |
45 |
|
46 |
|
47 |
|