src/HOL/Univ.thy
 author clasohm Fri Dec 01 14:17:50 1995 +0100 (1995-12-01) changeset 1384 007ad29ce6ca parent 1370 7361ac9b024d child 1396 48bcde67391b permissions -rw-r--r--
removed quotes from types section
 clasohm@923 ` 1` ```(* Title: HOL/Univ.thy ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@923 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```Move LEAST to Nat.thy??? Could it be defined for all types 'a::ord? ``` clasohm@923 ` 7` clasohm@923 ` 8` ```Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat) ``` clasohm@923 ` 9` clasohm@923 ` 10` ```Defines "Cartesian Product" and "Disjoint Sum" as set operations. ``` clasohm@923 ` 11` ```Could <*> be generalized to a general summation (Sigma)? ``` clasohm@923 ` 12` ```*) ``` clasohm@923 ` 13` clasohm@923 ` 14` ```Univ = Arith + Sum + ``` clasohm@923 ` 15` clasohm@923 ` 16` ```(** lists, trees will be sets of nodes **) ``` clasohm@923 ` 17` clasohm@923 ` 18` ```subtype (Node) ``` clasohm@972 ` 19` ``` 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" ``` clasohm@923 ` 20` clasohm@923 ` 21` ```types ``` clasohm@1384 ` 22` ``` 'a item = 'a node set ``` clasohm@923 ` 23` clasohm@923 ` 24` ```consts ``` clasohm@1370 ` 25` ``` Least :: (nat=>bool) => nat (binder "LEAST " 10) ``` clasohm@923 ` 26` clasohm@923 ` 27` ``` apfst :: "['a=>'c, 'a*'b] => 'c*'b" ``` clasohm@1370 ` 28` ``` Push :: [nat, nat=>nat] => (nat=>nat) ``` clasohm@923 ` 29` clasohm@1370 ` 30` ``` Push_Node :: [nat, 'a node] => 'a node ``` clasohm@1370 ` 31` ``` ndepth :: 'a node => nat ``` clasohm@923 ` 32` clasohm@923 ` 33` ``` Atom :: "('a+nat) => 'a item" ``` clasohm@1370 ` 34` ``` Leaf :: 'a => 'a item ``` clasohm@1370 ` 35` ``` Numb :: nat => 'a item ``` clasohm@1370 ` 36` ``` "\$" :: ['a item, 'a item]=> 'a item (infixr 60) ``` clasohm@1370 ` 37` ``` In0,In1 :: 'a item => 'a item ``` clasohm@923 ` 38` clasohm@1370 ` 39` ``` ntrunc :: [nat, 'a item] => 'a item ``` clasohm@923 ` 40` clasohm@1370 ` 41` ``` "<*>" :: ['a item set, 'a item set]=> 'a item set (infixr 80) ``` clasohm@1370 ` 42` ``` "<+>" :: ['a item set, 'a item set]=> 'a item set (infixr 70) ``` clasohm@923 ` 43` clasohm@1370 ` 44` ``` Split :: [['a item, 'a item]=>'b, 'a item] => 'b ``` clasohm@1370 ` 45` ``` Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b ``` clasohm@923 ` 46` clasohm@923 ` 47` ``` diag :: "'a set => ('a * 'a)set" ``` clasohm@1151 ` 48` ``` "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] ``` clasohm@1151 ` 49` ``` => ('a item * 'a item)set" (infixr 80) ``` clasohm@1151 ` 50` ``` "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] ``` clasohm@1151 ` 51` ``` => ('a item * 'a item)set" (infixr 70) ``` clasohm@923 ` 52` clasohm@923 ` 53` ```defs ``` clasohm@923 ` 54` clasohm@923 ` 55` ``` (*least number operator*) ``` clasohm@923 ` 56` ``` Least_def "Least(P) == @k. P(k) & (ALL j. j ~P(j))" ``` clasohm@923 ` 57` clasohm@923 ` 58` ``` Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" ``` clasohm@923 ` 59` clasohm@923 ` 60` ``` (*crude "lists" of nats -- needed for the constructions*) ``` clasohm@972 ` 61` ``` apfst_def "apfst == (%f. split(%x y. (f(x),y)))" ``` clasohm@923 ` 62` ``` Push_def "Push == (%b h. nat_case (Suc b) h)" ``` clasohm@923 ` 63` clasohm@923 ` 64` ``` (** operations on S-expressions -- sets of nodes **) ``` clasohm@923 ` 65` clasohm@923 ` 66` ``` (*S-expression constructors*) ``` clasohm@972 ` 67` ``` Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" ``` clasohm@923 ` 68` ``` Scons_def "M\$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" ``` clasohm@923 ` 69` clasohm@923 ` 70` ``` (*Leaf nodes, with arbitrary or nat labels*) ``` clasohm@923 ` 71` ``` Leaf_def "Leaf == Atom o Inl" ``` clasohm@923 ` 72` ``` Numb_def "Numb == Atom o Inr" ``` clasohm@923 ` 73` clasohm@923 ` 74` ``` (*Injections of the "disjoint sum"*) ``` clasohm@923 ` 75` ``` In0_def "In0(M) == Numb(0) \$ M" ``` clasohm@923 ` 76` ``` In1_def "In1(M) == Numb(Suc(0)) \$ M" ``` clasohm@923 ` 77` clasohm@923 ` 78` ``` (*the set of nodes with depth less than k*) ``` nipkow@1068 ` 79` ``` ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)" ``` clasohm@923 ` 80` ``` ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)B == UN x:A. UN y:B. { (x\$y) }" ``` clasohm@923 ` 84` ``` usum_def "A<+>B == In0``A Un In1``B" ``` clasohm@923 ` 85` clasohm@923 ` 86` ``` (*the corresponding eliminators*) ``` clasohm@923 ` 87` ``` Split_def "Split c M == @u. ? x y. M = x\$y & u = c x y" ``` clasohm@923 ` 88` clasohm@1151 ` 89` ``` Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) ``` clasohm@1151 ` 90` ``` | (? y . M = In1(y) & u = d(y))" ``` clasohm@923 ` 91` clasohm@923 ` 92` clasohm@923 ` 93` ``` (** diagonal sets and equality for the "universe" **) ``` clasohm@923 ` 94` clasohm@972 ` 95` ``` diag_def "diag(A) == UN x:A. {(x,x)}" ``` clasohm@923 ` 96` nipkow@1068 ` 97` ``` dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x\$y,x'\$y')}" ``` clasohm@923 ` 98` clasohm@1151 ` 99` ``` dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un ``` clasohm@1151 ` 100` ``` (UN (y,y'):s. {(In1(y),In1(y'))})" ``` clasohm@923 ` 101` clasohm@923 ` 102` ```end ```