41 Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree |
41 Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree |
42 Funs :: "'u set => ('t => 'u) set" |
42 Funs :: "'u set => ('t => 'u) set" |
43 |
43 |
44 ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree |
44 ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree |
45 |
45 |
46 "<*>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 80) |
46 uprod :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set |
47 "<+>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 70) |
47 usum :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set |
48 |
48 |
49 Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
49 Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
50 Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
50 Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c |
51 |
51 |
52 "<**>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
52 dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
53 => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 80) |
53 => (('a, 'b) dtree * ('a, 'b) dtree)set" |
54 "<++>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
54 dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] |
55 => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 70) |
55 => (('a, 'b) dtree * ('a, 'b) dtree)set" |
56 |
56 |
57 |
57 |
58 local |
58 local |
59 |
59 |
60 defs |
60 defs |
86 (*the set of nodes with depth less than k*) |
86 (*the set of nodes with depth less than k*) |
87 ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
87 ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" |
88 ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}" |
88 ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}" |
89 |
89 |
90 (*products and sums for the "universe"*) |
90 (*products and sums for the "universe"*) |
91 uprod_def "A<*>B == UN x:A. UN y:B. { Scons x y }" |
91 uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }" |
92 usum_def "A<+>B == In0``A Un In1``B" |
92 usum_def "usum A B == In0``A Un In1``B" |
93 |
93 |
94 (*the corresponding eliminators*) |
94 (*the corresponding eliminators*) |
95 Split_def "Split c M == @u. ? x y. M = Scons x y & u = c x y" |
95 Split_def "Split c M == @u. ? x y. M = Scons x y & u = c x y" |
96 |
96 |
97 Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) |
97 Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) |
98 | (? y . M = In1(y) & u = d(y))" |
98 | (? y . M = In1(y) & u = d(y))" |
99 |
99 |
100 |
100 |
101 (** equality for the "universe" **) |
101 (** equality for the "universe" **) |
102 |
102 |
103 dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" |
103 dprod_def "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" |
104 |
104 |
105 dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un |
105 dsum_def "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un |
106 (UN (y,y'):s. {(In1(y),In1(y'))})" |
106 (UN (y,y'):s. {(In1(y),In1(y'))})" |
107 |
107 |
108 end |
108 end |