Definition: equalf_from_lef
equalf_from_lef(lef;x;y) ==  if lef then lef else ff fi 

Lemma: equalf_from_lef_wf
[y:Type]. ∀[lef:y ─→ y ─→ 𝔹]. ∀[x,y:y].  (equalf_from_lef(lef;x;y) ∈ 𝔹)

Definition: l_treeco
l_treeco(L;T) ==
  corec(X.lbl:Atom × if lbl =a "leaf" then L
                     if lbl =a "node" then val:T × left_subtree:X × X
                     else Void
                     fi )

Lemma: l_treeco_wf
[L,T:Type].  (l_treeco(L;T) ∈ Type)

Lemma: l_treeco-ext
[L,T:Type].
  l_treeco(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
                             if lbl =a "node" then val:T × left_subtree:l_treeco(L;T) × l_treeco(L;T)
                             else Void
                             fi 

Definition: l_treeco_size
l_treeco_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "leaf" then 0
                   if lbl =a "node" then let val,left_subtree,z in (1 (size left_subtree)) (size z)
                   else 0
                   fi )) 
  p

Lemma: l_treeco_size_wf
[L,T:Type]. ∀[p:l_treeco(L;T)].  (l_treeco_size(p) ∈ partial(ℕ))

Definition: l_tree
l_tree(L;T) ==  {p:l_treeco(L;T)| (l_treeco_size(p))↓

Lemma: l_tree_wf
[L,T:Type].  (l_tree(L;T) ∈ Type)

Definition: l_tree_size
l_tree_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "leaf" then 0
                   if lbl =a "node" then let val,left_subtree,z in (1 (size left_subtree)) (size z)
                   else 0
                   fi )) 
  p

Lemma: l_tree_size_wf
[L,T:Type]. ∀[p:l_tree(L;T)].  (l_tree_size(p) ∈ ℕ)

Lemma: l_tree-ext
[L,T:Type].
  l_tree(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
                           if lbl =a "node" then val:T × left_subtree:l_tree(L;T) × l_tree(L;T)
                           else Void
                           fi 

Definition: l_tree_leaf
l_tree_leaf(val) ==  <"leaf", val>

Lemma: l_tree_leaf_wf
[L,T:Type]. ∀[val:L].  (l_tree_leaf(val) ∈ l_tree(L;T))

Definition: l_tree_node
l_tree_node(val;left_subtree;right_subtree) ==  <"node", val, left_subtree, right_subtree>

Lemma: l_tree_node_wf
[L,T:Type]. ∀[val:T]. ∀[left_subtree,right_subtree:l_tree(L;T)].
  (l_tree_node(val;left_subtree;right_subtree) ∈ l_tree(L;T))

Definition: l_tree_leaf?
l_tree_leaf?(v) ==  fst(v) =a "leaf"

Lemma: l_tree_leaf?_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  (l_tree_leaf?(v) ∈ 𝔹)

Definition: l_tree_leaf-val
l_tree_leaf-val(v) ==  snd(v)

Lemma: l_tree_leaf-val_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  l_tree_leaf-val(v) ∈ supposing ↑l_tree_leaf?(v)

Definition: l_tree_node?
l_tree_node?(v) ==  fst(v) =a "node"

Lemma: l_tree_node?_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  (l_tree_node?(v) ∈ 𝔹)

Definition: l_tree_node-val
l_tree_node-val(v) ==  fst(snd(v))

Lemma: l_tree_node-val_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  l_tree_node-val(v) ∈ supposing ↑l_tree_node?(v)

Definition: l_tree_node-left_subtree
l_tree_node-left_subtree(v) ==  fst(snd(snd(v)))

Lemma: l_tree_node-left_subtree_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  l_tree_node-left_subtree(v) ∈ l_tree(L;T) supposing ↑l_tree_node?(v)

Definition: l_tree_node-right_subtree
l_tree_node-right_subtree(v) ==  snd(snd(snd(v)))

Lemma: l_tree_node-right_subtree_wf
[L,T:Type]. ∀[v:l_tree(L;T)].  l_tree_node-right_subtree(v) ∈ l_tree(L;T) supposing ↑l_tree_node?(v)

Lemma: l_tree-induction
[L,T:Type]. ∀[P:l_tree(L;T) ─→ ℙ].
  ((∀val:L. P[l_tree_leaf(val)])
   (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
        (P[left_subtree]  P[right_subtree]  P[l_tree_node(val;left_subtree;right_subtree)]))
   {∀v:l_tree(L;T). P[v]})

Lemma: l_tree-definition
[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ].
  ((∀val:L. {x:A| R[x;l_tree_leaf(val)]} )
   (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
        ({x:A| R[x;left_subtree]} 
         {x:A| R[x;right_subtree]} 
         {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ))
   {∀v:l_tree(L;T). {x:A| R[x;v]} })

Definition: l_tree_ind
l_tree_ind(v;
           l_tree_leaf(val) leaf[val];
           l_tree_node(val,left_subtree,right_subtree) rec1,rec2.node[val; left_subtree; right_subtree; rec1;
                                                                        rec2])  ==
  fix((λl_tree_ind,v. let lbl,v1 
                      in if lbl="leaf" then leaf[v1]
                         if lbl="node"
                           then let val,v2 v1 
                                in let left_subtree,v3 v2 
                                   in node[val; left_subtree; v3; l_tree_ind left_subtree; l_tree_ind v3]
                         else ⊥
                         fi )) 
  v

Lemma: l_tree_ind_wf
[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ {x:A| R[x;l_tree_leaf(val)]} ].
[node:val:T
       ─→ left_subtree:l_tree(L;T)
       ─→ right_subtree:l_tree(L;T)
       ─→ {x:A| R[x;left_subtree]} 
       ─→ {x:A| R[x;right_subtree]} 
       ─→ {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ].
  (l_tree_ind(v;
              l_tree_leaf(val) leaf[val];
              l_tree_node(val,left_subtree,right_subtree) rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2]) 
   ∈ {x:A| R[x;v]} )

Lemma: l_tree_ind_wf_simple
[L,T,A:Type]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ A]. ∀[node:val:T
                                                            ─→ left_subtree:l_tree(L;T)
                                                            ─→ right_subtree:l_tree(L;T)
                                                            ─→ A
                                                            ─→ A
                                                            ─→ A].
  (l_tree_ind(v;
              l_tree_leaf(val) leaf[val];
              l_tree_node(val,left_subtree,right_subtree) rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2]) 
   ∈ A)

Lemma: l_tree_covariant
[A,B,T:Type].  l_tree(A;T) ⊆l_tree(B;T) supposing A ⊆B

Definition: max_w_ord
max_w_ord(t1;t2;f) ==  if f[t1] <f[t2] then t2 else t1 fi 

Lemma: max_w_ord_wf
[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ].  (max_w_ord(t1;t2;f) ∈ T)

Definition: max_w_unit_l_tree
max_w_unit_l_tree(u1;u2;f) ==
  case u1 of inl(val1) => case u2 of inl(val2) => inl max_w_ord(val1;val2;f) inr(unitval2) => u1 inr(unitval1) => u2

Lemma: max_w_unit_l_tree_wf
[T:Type]. ∀[u1,u2:T?]. ∀[f:T ─→ ℤ].  (max_w_unit_l_tree(u1;u2;f) ∈ T?)

Definition: max_l_tree
max_l_tree(t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v) inr ⋅ ;
             l_tree_node(v,ltr,rtr) ltrm,rtrm.max_w_unit_l_tree(inl v;rtrm;f)) 

Lemma: max_l_tree_wf
[L,T:Type].  ∀t:l_tree(L;T). ∀f:T ─→ ℤ.  (max_l_tree(t;f) ∈ T?)

Definition: min_w_ord
min_w_ord(t1;t2;f) ==  if f[t1] <f[t2] then t1 else t2 fi 

Lemma: min_w_ord_wf
[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ].  (min_w_ord(t1;t2;f) ∈ T)

Definition: min_w_unit_l_tree
min_w_unit_l_tree(u1;u2;f) ==
  case u1 of inl(val1) => case u2 of inl(val2) => inl min_w_ord(val1;val2;f) inr(unitval2) => u1 inr(unitval1) => u2

Lemma: min_w_unit_l_tree_wf
[T:Type]. ∀[u1,u2:T?]. ∀[f:T ─→ ℤ].  (min_w_unit_l_tree(u1;u2;f) ∈ T?)

Definition: min_l_tree
min_l_tree(t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v) inr ⋅ ;
             l_tree_node(v,ltr,rtr) ltrm,rtrm.min_w_unit_l_tree(inl v;ltrm;f)) 

Lemma: min_l_tree_wf
[L,T:Type].  ∀t:l_tree(L;T). ∀f:T ─→ ℤ.  (min_l_tree(t;f) ∈ T?)

Definition: bs_l_tree
bs_l_tree(t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v) tt;
             l_tree_node(v,ltr,rtr) ltrp,rtrp.ltrp
             ∧b rtrp
             ∧b case max_l_tree(ltr;f) of inl(maxl) => f[maxl] <f[v] inr(ul) => tt
             ∧b case min_l_tree(rtr;f) of inl(minr) => f[v] <f[minr] inr(ur) => tt) 

Lemma: bs_l_tree_wf
[L,T:Type]. ∀[t:l_tree(L;T)]. ∀[f:T ─→ ℤ].  (bs_l_tree(t;f) ∈ 𝔹)

Definition: bs_l_tree_member
bs_l_tree_member(x;t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v) tt;
             l_tree_node(v,ltr,rtr) ltrm,rtrm.(f[x] =z f[v]) ∨bif f[x] <f[v] then ltrm else rtrm fi 

Lemma: bs_l_tree_member_wf
[L,T:Type]. ∀[t:l_tree(L;T)]. ∀[x:T]. ∀[f:T ─→ ℤ].  (bs_l_tree_member(x;t;f) ∈ 𝔹)



Home Index