author  clasohm 
Wed, 29 Nov 1995 16:44:59 +0100  
changeset 1370  7361ac9b024d 
parent 1151  c820b3cc3df0 
child 1384  007ad29ce6ca 
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 
Move LEAST to Nat.thy??? Could it be defined for all types 'a::ord? 

7 

8 
Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat) 

9 

10 
Defines "Cartesian Product" and "Disjoint Sum" as set operations. 

11 
Could <*> be generalized to a general summation (Sigma)? 

12 
*) 

13 

14 
Univ = Arith + Sum + 

15 

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

17 

18 
subtype (Node) 

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

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

21 
types 

22 
'a item = "'a node set" 

23 

24 
consts 

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

25 
Least :: (nat=>bool) => nat (binder "LEAST " 10) 
923  26 

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

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

28 
Push :: [nat, nat=>nat] => (nat=>nat) 
923  29 

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

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

31 
ndepth :: 'a node => nat 
923  32 

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

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

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

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

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

37 
In0,In1 :: 'a item => 'a item 
923  38 

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

39 
ntrunc :: [nat, 'a item] => 'a item 
923  40 

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

41 
"<*>" :: ['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

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

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

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

45 
Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b 
923  46 

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

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

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

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

923  52 

53 
defs 

54 

55 
(*least number operator*) 

56 
Least_def "Least(P) == @k. P(k) & (ALL j. j<k > ~P(j))" 

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*) 

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

61 
apfst_def "apfst == (%f. split(%x y. (f(x),y)))" 
923  62 
Push_def "Push == (%b h. nat_case (Suc b) h)" 
63 

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

65 

66 
(*Sexpression constructors*) 

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

67 
Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" 
923  68 
Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" 
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"*) 

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

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

77 

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

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

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

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

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

85 

86 
(*the corresponding eliminators*) 

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

88 

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

923  91 

92 

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

94 

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

95 
diag_def "diag(A) == UN x:A. {(x,x)}" 
923  96 

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

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

923  101 

102 
end 