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)


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


20 


21 
types


22 
'a item = "'a node set"


23 


24 
consts


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


26 


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


28 
Push :: "[nat, nat=>nat] => (nat=>nat)"


29 


30 
Push_Node :: "[nat, 'a node] => 'a node"


31 
ndepth :: "'a node => nat"


32 


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


34 
Leaf :: "'a => 'a item"


35 
Numb :: "nat => 'a item"


36 
"$" :: "['a item, 'a item]=> 'a item" (infixr 60)


37 
In0,In1 :: "'a item => 'a item"


38 


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


40 


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


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


43 


44 
Split :: "[['a item, 'a item]=>'b, 'a item] => 'b"


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


46 


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


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)


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


61 
apfst_def "apfst == (%f. split(%x y. <f(x),y>))"


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


63 


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


65 


66 
(*Sexpression constructors*)


67 
Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})"


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


79 
ndepth_def "ndepth(n) == split (%f x. LEAST k. f(k)=0) (Rep_Node n)"


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 


89 
Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) \


90 
\  (? y . M = In1(y) & u = d(y))"


91 


92 


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


94 


95 
diag_def "diag(A) == UN x:A. {<x,x>}"


96 


97 
dprod_def "r<**>s == UN u:r. split (%x x'. \


98 
\ UN v:s. split (%y y'. {<x$y,x'$y'>}) v) u"


99 


100 
dsum_def "r<++>s == (UN u:r. split (%x x'. {<In0(x),In0(x')>}) u) Un \


101 
\ (UN v:s. split (%y y'. {<In1(y),In1(y')>}) v)"


102 


103 
end
