author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8735  bb2250ac9557 
child 9436  62bb04ab4b01 
permissions  rwrr 
923  1 
(* Title: HOL/Univ.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

6 
Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat) 
923  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 

7131  14 
setup arith_setup 
15 

16 

923  17 
(** lists, trees will be sets of nodes **) 
18 

1475  19 
typedef (Node) 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

20 
('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" 
923  21 

22 
types 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

23 
'a item = ('a, unit) node set 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

24 
('a, 'b) dtree = ('a, 'b) node set 
923  25 

26 
consts 

27 
apfst :: "['a=>'c, 'a*'b] => 'c*'b" 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

28 
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" 
923  29 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

30 
Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

31 
ndepth :: ('a, 'b) node => nat 
923  32 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

33 
Atom :: "('a + nat) => ('a, 'b) dtree" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

34 
Leaf :: 'a => ('a, 'b) dtree 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

35 
Numb :: nat => ('a, 'b) dtree 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

36 
Scons :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

37 
In0,In1 :: ('a, 'b) dtree => ('a, 'b) dtree 
923  38 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

39 
Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

40 
Funs :: "'u set => ('t => 'u) set" 
923  41 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

42 
ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

43 

7255  44 
uprod :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set 
45 
usum :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set 

923  46 

7255  47 
Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c 
48 
Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c 

923  49 

7255  50 
dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
51 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

52 
dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 

53 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

923  54 

3947  55 

923  56 
defs 
57 

58 
Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" 

59 

60 
(*crude "lists" of nats  needed for the constructions*) 

1396  61 
apfst_def "apfst == (%f (x,y). (f(x),y))" 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

62 
Push_def "Push == (%b h. nat_case b h)" 
923  63 

64 
(** operations on Sexpressions  sets of nodes **) 

65 

66 
(*Sexpression constructors*) 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

67 
Atom_def "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

68 
Scons_def "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)" 
923  69 

70 
(*Leaf nodes, with arbitrary or nat labels*) 

71 
Leaf_def "Leaf == Atom o Inl" 

72 
Numb_def "Numb == Atom o Inr" 

73 

74 
(*Injections of the "disjoint sum"*) 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3947
diff
changeset

75 
In0_def "In0(M) == Scons (Numb 0) M" 
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3947
diff
changeset

76 
In1_def "In1(M) == Scons (Numb 1) M" 
923  77 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

78 
(*Function spaces*) 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

79 
Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

80 
Funs_def "Funs S == {f. range f <= S}" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

81 

923  82 
(*the set of nodes with depth less than k*) 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
5978
diff
changeset

83 
ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" 
923  84 
ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}" 
85 

86 
(*products and sums for the "universe"*) 

7255  87 
uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }" 
88 
usum_def "usum A B == In0``A Un In1``B" 

923  89 

90 
(*the corresponding eliminators*) 

5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3947
diff
changeset

91 
Split_def "Split c M == @u. ? x y. M = Scons x y & u = c x y" 
923  92 

1151  93 
Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) 
7255  94 
 (? y . M = In1(y) & u = d(y))" 
923  95 

96 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5191
diff
changeset

97 
(** equality for the "universe" **) 
923  98 

7255  99 
dprod_def "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" 
923  100 

7255  101 
dsum_def "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
102 
(UN (y,y'):s. {(In1(y),In1(y'))})" 

923  103 

104 
end 