author | paulson |
Wed, 08 Aug 2001 14:52:10 +0200 | |
changeset 11483 | f4d10044a2cd |
parent 11451 | 8abfb4f7bd02 |
child 11701 | 3d51fbf81c17 |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Datatype_Universe.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 |
||
11483 | 12 |
Datatype_Universe = NatArith + Sum_Type + |
10213 | 13 |
|
14 |
||
15 |
(** lists, trees will be sets of nodes **) |
|
16 |
||
17 |
typedef (Node) |
|
11483 | 18 |
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
10213 | 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))})" |
|
10832 | 66 |
Scons_def "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr 2) ` N)" |
10213 | 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*) |
|
10832 | 77 |
Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" |
10213 | 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 }" |
|
10832 | 86 |
usum_def "usum A B == In0`A Un In1`B" |
10213 | 87 |
|
88 |
(*the corresponding eliminators*) |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
10832
diff
changeset
|
89 |
Split_def "Split c M == THE u. EX x y. M = Scons x y & u = c x y" |
10213 | 90 |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
10832
diff
changeset
|
91 |
Case_def "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
10832
diff
changeset
|
92 |
| (EX y . M = In1(y) & u = d(y))" |
10213 | 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 |