--- a/Univ.thy Thu Aug 18 12:13:26 1994 +0200
+++ b/Univ.thy Thu Aug 18 12:23:52 1994 +0200
@@ -11,7 +11,7 @@
Could <*> be generalized to a general summation (Sigma)?
*)
-Univ = Arith +
+Univ = Arith + Sum +
types
'a node
@@ -42,8 +42,8 @@
"<*>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
"<+>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
- Split :: "['a node set, ['a node set, 'a node set]=>'b] => 'b"
- Case :: "['a node set, ['a node set]=>'b, ['a node set]=>'b] => 'b"
+ Split :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
+ Case :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
diag :: "'a set => ('a * 'a)set"
"<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
@@ -65,8 +65,8 @@
Push_Node_def "Push_Node == (%n x. Abs_Node (apfst(Push(n),Rep_Node(x))))"
(*crude "lists" of nats -- needed for the constructions*)
- apfst_def "apfst == (%f p.split(p, %x y. <f(x),y>))"
- Push_def "Push == (%b h n. nat_case(n,Suc(b),h))"
+ apfst_def "apfst == (%f. split(%x y. <f(x),y>))"
+ Push_def "Push == (%b h. nat_case(Suc(b),h))"
(** operations on S-expressions -- sets of nodes **)
@@ -83,7 +83,7 @@
In1_def "In1(M) == Numb(Suc(0)) $ M"
(*the set of nodes with depth less than k*)
- ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
+ ndepth_def "ndepth(n) == split(%f x. LEAST k. f(k)=0, Rep_Node(n))"
ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
(*products and sums for the "universe"*)
@@ -91,9 +91,9 @@
usum_def "A<+>B == In0``A Un In1``B"
(*the corresponding eliminators*)
- Split_def "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
+ Split_def "Split(c,M) == @u. ? x y. M = x$y & u = c(x,y)"
- Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \
+ Case_def "Case(c,d,M) == @u. (? x . M = In0(x) & u = c(x)) \
\ | (? y . M = In1(y) & u = d(y))"
@@ -101,10 +101,10 @@
diag_def "diag(A) == UN x:A. {<x,x>}"
- dprod_def "r<**>s == UN u:r. UN v:s. \
-\ split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
+ dprod_def "r<**>s == UN u:r. split(%x x'. \
+\ UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
- dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
-\ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"
+ dsum_def "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un \
+\ (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
end