1 (* Title: HOL/Univ.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat) |
|
7 |
|
8 Defines "Cartesian Product" and "Disjoint Sum" as set operations. |
|
9 Could <*> be generalized to a general summation (Sigma)? |
|
10 *) |
|
11 |
|
12 Univ = Arith + Sum + |
|
13 |
|
14 |
|
15 (** lists, trees will be sets of nodes **) |
|
16 |
|
17 typedef (Node) |
|
18 ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
|
19 |
|
20 types |
|
21 'a item = ('a, unit) node set |
|
22 ('a, 'b) dtree = ('a, 'b) node set |
|
23 |
|
24 consts |
|
25 apfst :: "['a=>'c, 'a*'b] => 'c*'b" |
|
26 Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" |
|
27 |
|
28 Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" |
|
29 ndepth :: ('a, 'b) node => nat |
|
30 |
|
31 Atom :: "('a + nat) => ('a, 'b) dtree" |
|
32 Leaf :: 'a => ('a, 'b) dtree |
|
33 Numb :: nat => ('a, 'b) dtree |
|
34 Scons :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree |
|
35 In0,In1 :: ('a, 'b) dtree => ('a, 'b) dtree |
|
36 |
|
37 Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree |
|
38 Funs :: "'u set => ('t => 'u) set" |
|
39 |
|
40 ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree |
|
41 |
|
42 uprod :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set |
|
43 usum :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set |
|
44 |
|
45 Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
|
46 Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
|
47 |
|
48 dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
49 => (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
50 dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
|
51 => (('a, 'b) dtree * ('a, 'b) dtree)set" |
|
52 |
|
53 |
|
54 defs |
|
55 |
|
56 Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" |
|
57 |
|
58 (*crude "lists" of nats -- needed for the constructions*) |
|
59 apfst_def "apfst == (%f (x,y). (f(x),y))" |
|
60 Push_def "Push == (%b h. nat_case b h)" |
|
61 |
|
62 (** operations on S-expressions -- sets of nodes **) |
|
63 |
|
64 (*S-expression constructors*) |
|
65 Atom_def "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" |
|
66 Scons_def "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)" |
|
67 |
|
68 (*Leaf nodes, with arbitrary or nat labels*) |
|
69 Leaf_def "Leaf == Atom o Inl" |
|
70 Numb_def "Numb == Atom o Inr" |
|
71 |
|
72 (*Injections of the "disjoint sum"*) |
|
73 In0_def "In0(M) == Scons (Numb 0) M" |
|
74 In1_def "In1(M) == Scons (Numb 1) M" |
|
75 |
|
76 (*Function spaces*) |
|
77 Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}" |
|
78 Funs_def "Funs S == {f. range f <= S}" |
|
79 |
|
80 (*the set of nodes with depth less than k*) |
|
81 ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
|
82 ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}" |
|
83 |
|
84 (*products and sums for the "universe"*) |
|
85 uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }" |
|
86 usum_def "usum A B == In0``A Un In1``B" |
|
87 |
|
88 (*the corresponding eliminators*) |
|
89 Split_def "Split c M == @u. ? x y. M = Scons x y & u = c x y" |
|
90 |
|
91 Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) |
|
92 | (? y . M = In1(y) & u = d(y))" |
|
93 |
|
94 |
|
95 (** equality for the "universe" **) |
|
96 |
|
97 dprod_def "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" |
|
98 |
|
99 dsum_def "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un |
|
100 (UN (y,y'):s. {(In1(y),In1(y'))})" |
|
101 |
|
102 end |
|