27 ndepth :: "'a node => nat" |
27 ndepth :: "'a node => nat" |
28 |
28 |
29 Atom :: "('a+nat) => 'a node set" |
29 Atom :: "('a+nat) => 'a node set" |
30 Leaf :: "'a => 'a node set" |
30 Leaf :: "'a => 'a node set" |
31 Numb :: "nat => 'a node set" |
31 Numb :: "nat => 'a node set" |
32 "." :: "['a node set, 'a node set]=> 'a node set" (infixr 60) |
32 "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60) |
33 In0,In1 :: "'a node set => 'a node set" |
33 In0,In1 :: "'a node set => 'a node set" |
34 |
34 |
35 ntrunc :: "[nat, 'a node set] => 'a node set" |
35 ntrunc :: "[nat, 'a node set] => 'a node set" |
36 |
36 |
37 "<*>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80) |
37 "<*>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80) |
65 |
65 |
66 (** operations on S-expressions -- sets of nodes **) |
66 (** operations on S-expressions -- sets of nodes **) |
67 |
67 |
68 (*S-expression constructors*) |
68 (*S-expression constructors*) |
69 Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})" |
69 Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})" |
70 Scons_def "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" |
70 Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" |
71 |
71 |
72 (*Leaf nodes, with arbitrary or nat labels*) |
72 (*Leaf nodes, with arbitrary or nat labels*) |
73 Leaf_def "Leaf == Atom o Inl" |
73 Leaf_def "Leaf == Atom o Inl" |
74 Numb_def "Numb == Atom o Inr" |
74 Numb_def "Numb == Atom o Inr" |
75 |
75 |
76 (*Injections of the "disjoint sum"*) |
76 (*Injections of the "disjoint sum"*) |
77 In0_def "In0(M) == Numb(0) . M" |
77 In0_def "In0(M) == Numb(0) $ M" |
78 In1_def "In1(M) == Numb(Suc(0)) . M" |
78 In1_def "In1(M) == Numb(Suc(0)) $ M" |
79 |
79 |
80 (*the set of nodes with depth less than k*) |
80 (*the set of nodes with depth less than k*) |
81 ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)" |
81 ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)" |
82 ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}" |
82 ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}" |
83 |
83 |
84 (*products and sums for the "universe"*) |
84 (*products and sums for the "universe"*) |
85 uprod_def "A<*>B == UN x:A. UN y:B. { (x.y) }" |
85 uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }" |
86 usum_def "A<+>B == In0``A Un In1``B" |
86 usum_def "A<+>B == In0``A Un In1``B" |
87 |
87 |
88 (*the corresponding eliminators*) |
88 (*the corresponding eliminators*) |
89 Split_def "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)" |
89 Split_def "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)" |
90 |
90 |
91 Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \ |
91 Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \ |
92 \ | (? y . M = In1(y) & u = d(y))" |
92 \ | (? y . M = In1(y) & u = d(y))" |
93 |
93 |
94 |
94 |
95 (** diagonal sets and equality for the "universe" **) |
95 (** diagonal sets and equality for the "universe" **) |
96 |
96 |
97 diag_def "diag(A) == UN x:A. {<x,x>}" |
97 diag_def "diag(A) == UN x:A. {<x,x>}" |
98 |
98 |
99 dprod_def "r<**>s == UN u:r. UN v:s. \ |
99 dprod_def "r<**>s == UN u:r. UN v:s. \ |
100 \ split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))" |
100 \ split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))" |
101 |
101 |
102 dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \ |
102 dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \ |
103 \ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))" |
103 \ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))" |
104 |
104 |
105 end |
105 end |