src/HOL/Datatype_Universe.thy
changeset 10213 01c2744a3786
child 10214 77349ed89f45
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Universe.thy	Thu Oct 12 18:44:35 2000 +0200
     1.3 @@ -0,0 +1,102 @@
     1.4 +(*  Title:      HOL/Datatype_Universe.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
    1.10 +
    1.11 +Defines "Cartesian Product" and "Disjoint Sum" as set operations.
    1.12 +Could <*> be generalized to a general summation (Sigma)?
    1.13 +*)
    1.14 +
    1.15 +Datatype_Universe = Arithmetic + Sum_Type +
    1.16 +
    1.17 +
    1.18 +(** lists, trees will be sets of nodes **)
    1.19 +
    1.20 +typedef (Node)
    1.21 +  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.22 +
    1.23 +types
    1.24 +  'a item = ('a, unit) node set
    1.25 +  ('a, 'b) dtree = ('a, 'b) node set
    1.26 +
    1.27 +consts
    1.28 +  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    1.29 +  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    1.30 +
    1.31 +  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    1.32 +  ndepth    :: ('a, 'b) node => nat
    1.33 +
    1.34 +  Atom      :: "('a + nat) => ('a, 'b) dtree"
    1.35 +  Leaf      :: 'a => ('a, 'b) dtree
    1.36 +  Numb      :: nat => ('a, 'b) dtree
    1.37 +  Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
    1.38 +  In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
    1.39 +
    1.40 +  Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
    1.41 +  Funs      :: "'u set => ('t => 'u) set"
    1.42 +
    1.43 +  ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
    1.44 +
    1.45 +  uprod     :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
    1.46 +  usum      :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
    1.47 +
    1.48 +  Split     :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
    1.49 +  Case      :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
    1.50 +
    1.51 +  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
    1.52 +                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.53 +  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
    1.54 +                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.55 +
    1.56 +
    1.57 +defs
    1.58 +
    1.59 +  Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.60 +
    1.61 +  (*crude "lists" of nats -- needed for the constructions*)
    1.62 +  apfst_def  "apfst == (%f (x,y). (f(x),y))"
    1.63 +  Push_def   "Push == (%b h. nat_case b h)"
    1.64 +
    1.65 +  (** operations on S-expressions -- sets of nodes **)
    1.66 +
    1.67 +  (*S-expression constructors*)
    1.68 +  Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    1.69 +  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
    1.70 +
    1.71 +  (*Leaf nodes, with arbitrary or nat labels*)
    1.72 +  Leaf_def   "Leaf == Atom o Inl"
    1.73 +  Numb_def   "Numb == Atom o Inr"
    1.74 +
    1.75 +  (*Injections of the "disjoint sum"*)
    1.76 +  In0_def    "In0(M) == Scons (Numb 0) M"
    1.77 +  In1_def    "In1(M) == Scons (Numb 1) M"
    1.78 +
    1.79 +  (*Function spaces*)
    1.80 +  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
    1.81 +  Funs_def "Funs S == {f. range f <= S}"
    1.82 +
    1.83 +  (*the set of nodes with depth less than k*)
    1.84 +  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    1.85 +  ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
    1.86 +
    1.87 +  (*products and sums for the "universe"*)
    1.88 +  uprod_def  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    1.89 +  usum_def   "usum A B == In0``A Un In1``B"
    1.90 +
    1.91 +  (*the corresponding eliminators*)
    1.92 +  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
    1.93 +
    1.94 +  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
    1.95 +                               | (? y . M = In1(y) & u = d(y))"
    1.96 +
    1.97 +
    1.98 +  (** equality for the "universe" **)
    1.99 +
   1.100 +  dprod_def  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   1.101 +
   1.102 +  dsum_def   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
   1.103 +                          (UN (y,y'):s. {(In1(y),In1(y'))})"
   1.104 +
   1.105 +end