author  paulson 
Mon, 11 Mar 1996 14:05:45 +0100  
changeset 1562  e98c7f6165c9 
parent 1531  e5eb247ad13c 
child 3947  eb707467f8c5 
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 

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

12 
Univ = Arith + Sum + 

13 

14 
(** lists, trees will be sets of nodes **) 

15 

1475  16 
typedef (Node) 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

17 
'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" 
923  18 

19 
types 

1384  20 
'a item = 'a node set 
923  21 

22 
consts 

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

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

24 
Push :: [nat, nat=>nat] => (nat=>nat) 
923  25 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

26 
Push_Node :: [nat, 'a node] => 'a node 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

27 
ndepth :: 'a node => nat 
923  28 

29 
Atom :: "('a+nat) => 'a item" 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

30 
Leaf :: 'a => 'a item 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

31 
Numb :: nat => 'a item 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

32 
"$" :: ['a item, 'a item]=> 'a item (infixr 60) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

33 
In0,In1 :: 'a item => 'a item 
923  34 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

35 
ntrunc :: [nat, 'a item] => 'a item 
923  36 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

37 
"<*>" :: ['a item set, 'a item set]=> 'a item set (infixr 80) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

38 
"<+>" :: ['a item set, 'a item set]=> 'a item set (infixr 70) 
923  39 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

40 
Split :: [['a item, 'a item]=>'b, 'a item] => 'b 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

41 
Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b 
923  42 

43 
diag :: "'a set => ('a * 'a)set" 

1151  44 
"<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
45 
=> ('a item * 'a item)set" (infixr 80) 

46 
"<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 

47 
=> ('a item * 'a item)set" (infixr 70) 

923  48 

49 
defs 

50 

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

52 

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

1396  54 
apfst_def "apfst == (%f (x,y). (f(x),y))" 
923  55 
Push_def "Push == (%b h. nat_case (Suc b) h)" 
56 

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

58 

59 
(*Sexpression constructors*) 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

60 
Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" 
923  61 
Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" 
62 

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

64 
Leaf_def "Leaf == Atom o Inl" 

65 
Numb_def "Numb == Atom o Inr" 

66 

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

68 
In0_def "In0(M) == Numb(0) $ M" 

69 
In1_def "In1(M) == Numb(Suc(0)) $ M" 

70 

71 
(*the set of nodes with depth less than k*) 

1068  72 
ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)" 
923  73 
ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}" 
74 

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

76 
uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }" 

77 
usum_def "A<+>B == In0``A Un In1``B" 

78 

79 
(*the corresponding eliminators*) 

80 
Split_def "Split c M == @u. ? x y. M = x$y & u = c x y" 

81 

1151  82 
Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) 
83 
 (? y . M = In1(y) & u = d(y))" 

923  84 

85 

86 
(** diagonal sets and equality for the "universe" **) 

87 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

88 
diag_def "diag(A) == UN x:A. {(x,x)}" 
923  89 

1068  90 
dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}" 
923  91 

1151  92 
dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
93 
(UN (y,y'):s. {(In1(y),In1(y'))})" 

923  94 

95 
end 