src/HOL/Univ.thy
 author nipkow Mon Oct 21 09:50:50 1996 +0200 (1996-10-21) changeset 2115 9709f9188549 parent 1562 e98c7f6165c9 child 3947 eb707467f8c5 permissions -rw-r--r--
 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` ```Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat) ``` clasohm@923 ` 7` clasohm@923 ` 8` ```Defines "Cartesian Product" and "Disjoint Sum" as set operations. ``` clasohm@923 ` 9` ```Could <*> be generalized to a general summation (Sigma)? ``` clasohm@923 ` 10` ```*) ``` clasohm@923 ` 11` clasohm@923 ` 12` ```Univ = Arith + Sum + ``` clasohm@923 ` 13` clasohm@923 ` 14` ```(** lists, trees will be sets of nodes **) ``` clasohm@923 ` 15` clasohm@1475 ` 16` ```typedef (Node) ``` clasohm@972 ` 17` ``` 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" ``` clasohm@923 ` 18` clasohm@923 ` 19` ```types ``` clasohm@1384 ` 20` ``` 'a item = 'a node set ``` clasohm@923 ` 21` clasohm@923 ` 22` ```consts ``` clasohm@923 ` 23` ``` apfst :: "['a=>'c, 'a*'b] => 'c*'b" ``` clasohm@1370 ` 24` ``` Push :: [nat, nat=>nat] => (nat=>nat) ``` clasohm@923 ` 25` clasohm@1370 ` 26` ``` Push_Node :: [nat, 'a node] => 'a node ``` clasohm@1370 ` 27` ``` ndepth :: 'a node => nat ``` clasohm@923 ` 28` clasohm@923 ` 29` ``` Atom :: "('a+nat) => 'a item" ``` clasohm@1370 ` 30` ``` Leaf :: 'a => 'a item ``` clasohm@1370 ` 31` ``` Numb :: nat => 'a item ``` clasohm@1370 ` 32` ``` "\$" :: ['a item, 'a item]=> 'a item (infixr 60) ``` clasohm@1370 ` 33` ``` In0,In1 :: 'a item => 'a item ``` clasohm@923 ` 34` clasohm@1370 ` 35` ``` ntrunc :: [nat, 'a item] => 'a item ``` clasohm@923 ` 36` clasohm@1370 ` 37` ``` "<*>" :: ['a item set, 'a item set]=> 'a item set (infixr 80) ``` clasohm@1370 ` 38` ``` "<+>" :: ['a item set, 'a item set]=> 'a item set (infixr 70) ``` clasohm@923 ` 39` clasohm@1370 ` 40` ``` Split :: [['a item, 'a item]=>'b, 'a item] => 'b ``` clasohm@1370 ` 41` ``` Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b ``` clasohm@923 ` 42` clasohm@923 ` 43` ``` diag :: "'a set => ('a * 'a)set" ``` clasohm@1151 ` 44` ``` "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] ``` clasohm@1151 ` 45` ``` => ('a item * 'a item)set" (infixr 80) ``` clasohm@1151 ` 46` ``` "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] ``` clasohm@1151 ` 47` ``` => ('a item * 'a item)set" (infixr 70) ``` clasohm@923 ` 48` clasohm@923 ` 49` ```defs ``` clasohm@923 ` 50` clasohm@923 ` 51` ``` Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" ``` clasohm@923 ` 52` clasohm@923 ` 53` ``` (*crude "lists" of nats -- needed for the constructions*) ``` paulson@1396 ` 54` ``` apfst_def "apfst == (%f (x,y). (f(x),y))" ``` clasohm@923 ` 55` ``` Push_def "Push == (%b h. nat_case (Suc b) h)" ``` clasohm@923 ` 56` clasohm@923 ` 57` ``` (** operations on S-expressions -- sets of nodes **) ``` clasohm@923 ` 58` clasohm@923 ` 59` ``` (*S-expression constructors*) ``` clasohm@972 ` 60` ``` Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" ``` clasohm@923 ` 61` ``` Scons_def "M\$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" ``` clasohm@923 ` 62` clasohm@923 ` 63` ``` (*Leaf nodes, with arbitrary or nat labels*) ``` clasohm@923 ` 64` ``` Leaf_def "Leaf == Atom o Inl" ``` clasohm@923 ` 65` ``` Numb_def "Numb == Atom o Inr" ``` clasohm@923 ` 66` clasohm@923 ` 67` ``` (*Injections of the "disjoint sum"*) ``` clasohm@923 ` 68` ``` In0_def "In0(M) == Numb(0) \$ M" ``` clasohm@923 ` 69` ``` In1_def "In1(M) == Numb(Suc(0)) \$ M" ``` clasohm@923 ` 70` clasohm@923 ` 71` ``` (*the set of nodes with depth less than k*) ``` nipkow@1068 ` 72` ``` ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)" ``` clasohm@923 ` 73` ``` ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)B == UN x:A. UN y:B. { (x\$y) }" ``` clasohm@923 ` 77` ``` usum_def "A<+>B == In0``A Un In1``B" ``` clasohm@923 ` 78` clasohm@923 ` 79` ``` (*the corresponding eliminators*) ``` clasohm@923 ` 80` ``` Split_def "Split c M == @u. ? x y. M = x\$y & u = c x y" ``` clasohm@923 ` 81` clasohm@1151 ` 82` ``` Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) ``` clasohm@1151 ` 83` ``` | (? y . M = In1(y) & u = d(y))" ``` clasohm@923 ` 84` clasohm@923 ` 85` clasohm@923 ` 86` ``` (** diagonal sets and equality for the "universe" **) ``` clasohm@923 ` 87` clasohm@972 ` 88` ``` diag_def "diag(A) == UN x:A. {(x,x)}" ``` clasohm@923 ` 89` nipkow@1068 ` 90` ``` dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x\$y,x'\$y')}" ``` clasohm@923 ` 91` clasohm@1151 ` 92` ``` dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un ``` clasohm@1151 ` 93` ``` (UN (y,y'):s. {(In1(y),In1(y'))})" ``` clasohm@923 ` 94` clasohm@923 ` 95` ```end ```