src/HOL/Library/Old_Datatype.thy
changeset 62145 5b946c81dfbf
parent 61952 546958347e05
child 65513 587433a18053
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -26,80 +26,67 @@
     1.4  type_synonym 'a item        = "('a, unit) node set"
     1.5  type_synonym ('a, 'b) dtree = "('a, 'b) node set"
     1.6  
     1.7 -consts
     1.8 -  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
     1.9 -
    1.10 -  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    1.11 -  ndepth    :: "('a, 'b) node => nat"
    1.12 +definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    1.13 +  (*crude "lists" of nats -- needed for the constructions*)
    1.14 +  where "Push == (%b h. case_nat b h)"
    1.15  
    1.16 -  Atom      :: "('a + nat) => ('a, 'b) dtree"
    1.17 -  Leaf      :: "'a => ('a, 'b) dtree"
    1.18 -  Numb      :: "nat => ('a, 'b) dtree"
    1.19 -  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.20 -  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.21 -  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.22 -  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    1.23 -
    1.24 -  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.25 -
    1.26 -  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.27 -  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.28 -
    1.29 -  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    1.30 -  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    1.31 -
    1.32 -  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    1.33 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.34 -  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    1.35 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    1.36 +definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    1.37 +  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.38  
    1.39  
    1.40 -defs
    1.41 +(** operations on S-expressions -- sets of nodes **)
    1.42  
    1.43 -  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.44 -
    1.45 -  (*crude "lists" of nats -- needed for the constructions*)
    1.46 -  Push_def:   "Push == (%b h. case_nat b h)"
    1.47 +(*S-expression constructors*)
    1.48 +definition Atom :: "('a + nat) => ('a, 'b) dtree"
    1.49 +  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    1.50 +definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.51 +  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    1.52  
    1.53 -  (** operations on S-expressions -- sets of nodes **)
    1.54 +(*Leaf nodes, with arbitrary or nat labels*)
    1.55 +definition Leaf :: "'a => ('a, 'b) dtree"
    1.56 +  where "Leaf == Atom o Inl"
    1.57 +definition Numb :: "nat => ('a, 'b) dtree"
    1.58 +  where "Numb == Atom o Inr"
    1.59  
    1.60 -  (*S-expression constructors*)
    1.61 -  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    1.62 -  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    1.63 -
    1.64 -  (*Leaf nodes, with arbitrary or nat labels*)
    1.65 -  Leaf_def:   "Leaf == Atom o Inl"
    1.66 -  Numb_def:   "Numb == Atom o Inr"
    1.67 +(*Injections of the "disjoint sum"*)
    1.68 +definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.69 +  where "In0(M) == Scons (Numb 0) M"
    1.70 +definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
    1.71 +  where "In1(M) == Scons (Numb 1) M"
    1.72  
    1.73 -  (*Injections of the "disjoint sum"*)
    1.74 -  In0_def:    "In0(M) == Scons (Numb 0) M"
    1.75 -  In1_def:    "In1(M) == Scons (Numb 1) M"
    1.76 +(*Function spaces*)
    1.77 +definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    1.78 +  where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
    1.79  
    1.80 -  (*Function spaces*)
    1.81 -  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
    1.82 +(*the set of nodes with depth less than k*)
    1.83 +definition ndepth :: "('a, 'b) node => nat"
    1.84 +  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    1.85 +definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    1.86 +  where "ntrunc k N == {n. n:N & ndepth(n)<k}"
    1.87  
    1.88 -  (*the set of nodes with depth less than k*)
    1.89 -  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    1.90 -  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
    1.91 +(*products and sums for the "universe"*)
    1.92 +definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.93 +  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
    1.94 +definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.95 +  where "usum A B == In0`A Un In1`B"
    1.96  
    1.97 -  (*products and sums for the "universe"*)
    1.98 -  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    1.99 -  usum_def:   "usum A B == In0`A Un In1`B"
   1.100 +(*the corresponding eliminators*)
   1.101 +definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   1.102 +  where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
   1.103  
   1.104 -  (*the corresponding eliminators*)
   1.105 -  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
   1.106 -
   1.107 -  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
   1.108 -                                  | (EX y . M = In1(y) & u = d(y))"
   1.109 +definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   1.110 +  where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
   1.111  
   1.112  
   1.113 -  (** equality for the "universe" **)
   1.114 -
   1.115 -  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   1.116 +(** equality for the "universe" **)
   1.117  
   1.118 -  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
   1.119 -                          (UN (y,y'):s. {(In1(y),In1(y'))})"
   1.120 +definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   1.121 +      => (('a, 'b) dtree * ('a, 'b) dtree)set"
   1.122 +  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   1.123  
   1.124 +definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   1.125 +      => (('a, 'b) dtree * ('a, 'b) dtree)set"
   1.126 +  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
   1.127  
   1.128  
   1.129  lemma apfst_convE: