---

Definition: poly-zero
poly-zero(p) ==  tree_leaf?(p) ∧b (tree_leaf-value(p) =z 0)

Lemma: poly-zero_wf
∀[p:tree(ℤ)]. (poly-zero(p) ∈ 𝔹)

Definition: poly-int
poly-int(p) ==  tree_ind(p; tree_leaf(x)⇒ tt; tree_node(l,r)⇒ lz,rz.lz ∧b poly-zero(r)) 

Lemma: poly-int_wf
∀[p:tree(ℤ)]. (poly-int(p) ∈ 𝔹)

Definition: ispolyform
ispolyform(p) ==  tree_ind(p; tree_leaf(x)⇒ λn.tt; tree_node(a,b)⇒ ra,rb.λn.(((ra (n - 1)) ∧b (rb n)) ∧b 0 <z n)) 

Lemma: ispolyform_node_lemma
∀n,b,a:Top.  (ispolyform(tree_node(a;b)) n ~ ((ispolyform(a) (n - 1)) ∧b (ispolyform(b) n)) ∧b 0 <z n)

Lemma: ispolyform_leaf_lemma
∀n,x:Top.  (ispolyform(tree_leaf(x)) n ~ tt)

Lemma: ispolyform_wf
∀[p:tree(ℤ)]. (ispolyform(p) ∈ ℤ ⟶ 𝔹)

Definition: polyform
polyform(n) ==  {p:tree(ℤ)| ↑(ispolyform(p) n)} 

Lemma: polyform_wf
∀[n:ℤ]. (polyform(n) ∈ Type)

Lemma: value-type-polyform
∀[n:ℤ]. value-type(polyform(n))

Lemma: polyform-subtype
∀[n,m:ℕ].  polyform(n) ⊆r polyform(m) supposing n ≤ m

Definition: polynom
polynom(n) ==  {p:polyform(n)| (↑poly-int(p)) ⇒ (↑tree_leaf?(p))} 

Lemma: polynom_wf
∀[n:ℤ]. (polynom(n) ∈ Type)

Definition: polyconst
polyconst(k) ==  tree_leaf(k)

Lemma: polyconst_wf
∀[k,n:ℤ].  (polyconst(k) ∈ polynom(n))

Definition: polyvar
polyvar(v)==r if v=0 then tree_node(tree_leaf(0);tree_leaf(1)) else eval a = polyvar(v - 1) in tree_node(a;tree_leaf(0))

Lemma: polyvar_wf
∀[v:ℕ]. (polyvar(v) ∈ polynom(v + 1))

Definition: poly-val-fun
poly-val-fun(p) ==
  tree_ind(p;
           tree_leaf(x)⇒ λl.x;
           tree_node(a,b)⇒ ra,rb.λl.eval t = tl(l) in
                                     eval av = ra t in
                                     eval bv = rb l in
                                       if bv=0 then av else eval h = hd(l) in av + (h * bv)) 

Lemma: poly-val-fun_wf
∀[n:ℕ]. ∀[p:polyform(n)].  (poly-val-fun(p) ∈ {l:ℤ List| n ≤ ||l||}  ⟶ ℤ)

Definition: poly-int-val
p@l ==  poly-val-fun(p) l

Lemma: poly-int-val_wf
∀[n:ℕ]. ∀[p:polyform(n)]. ∀[l:{l:ℤ List| n ≤ ||l||} ].  (p@l ∈ ℤ)

Lemma: polyvar-val
∀[v:ℕ]. ∀[l:{l:ℤ List| v < ||l||} ].  (polyvar(v)@l = l[v] ∈ ℤ)

Lemma: polyconst_val_lemma
∀l,k:Top.  (polyconst(k)@l ~ k)

Lemma: poly-zero-val
∀[p:tree(ℤ)]. ∀[l:Top]. (p@l = 0 ∈ ℤ) supposing ↑poly-zero(p)

Lemma: poly-int-value
∀[p:tree(ℤ)]. ∀[l:Top List]. (p@l = p@[] ∈ ℤ) supposing ↑poly-int(p)

Definition: add-polynom
add-polynom(p;q)
==r if tree_leaf?(p)
      then if tree_leaf?(q)
           then eval a = tree_leaf-value(p) + tree_leaf-value(q) in
                tree_leaf(a)
           else eval a = add-polynom(p;tree_node-left(q)) in
                eval b = tree_node-right(q) in
                  tree_node(a;b)
           fi 
    if tree_leaf?(q) then eval a = add-polynom(tree_node-left(p);q) in eval b = tree_node-right(p) in   tree_node(a;b)
    else eval a = add-polynom(tree_node-left(p);tree_node-left(q)) in
         eval b = add-polynom(tree_node-right(p);tree_node-right(q)) in
           if poly-zero(b) ∧b poly-int(a) then a else tree_node(a;b) fi 
    fi 

Lemma: add-polynom_wf
∀[n:ℕ]. ∀[p,q:polyform(n)].  (add-polynom(p;q) ∈ polyform(n))

Lemma: add-polynom-val
∀[n:ℕ]. ∀[p,q:polyform(n)]. ∀[l:{l:ℤ List| n ≤ ||l||} ].  (add-polynom(p;q)@l = (p@l + q@l) ∈ ℤ)

Definition: mul-polynom
mul-polynom(p;q)
==r if tree_leaf?(p)
      then if tree_leaf-value(p)=0
           then polyconst(0)
           else if tree_leaf-value(p)=1
                then q
                else if tree_leaf?(q)
                     then eval a = tree_leaf-value(p) * tree_leaf-value(q) in
                          tree_leaf(a)
                     else eval a = mul-polynom(p;tree_node-left(q)) in
                          eval b = mul-polynom(p;tree_node-right(q)) in
                            tree_node(a;b)
                     fi 
    if tree_leaf?(q)
      then if tree_leaf-value(q)=0
           then polyconst(0)
           else if tree_leaf-value(q)=1
                then p
                else eval a = mul-polynom(tree_node-left(p);q) in
                     eval b = mul-polynom(tree_node-right(p);q) in
                       tree_node(a;b)
    else eval aa = mul-polynom(tree_node-left(p);tree_node-left(q)) in
         eval ab = mul-polynom(tree_node(tree_node-left(p);polyconst(0));tree_node-right(q)) in
         eval ba = mul-polynom(tree_node-right(p);tree_node(tree_node-left(q);polyconst(0))) in
         eval bb = mul-polynom(tree_node-right(p);tree_node-right(q)) in
         eval mid = add-polynom(ab;ba) in
         eval bb' = add-polynom(mid;tree_node(polyconst(0);bb)) in
           tree_node(aa;bb')
    fi 

Lemma: mul-polynom_wf
∀[n:ℕ]. ∀[p,q:polyform(n)].  (mul-polynom(p;q) ∈ polyform(n))

Lemma: mul-polynom-val
∀[n:ℕ]. ∀[p,q:polyform(n)]. ∀[l:{l:ℤ List| n ≤ ||l||} ].  (mul-polynom(p;q)@l = (p@l * q@l) ∈ ℤ)

Definition: int_term_to_polynom
int_term_to_polynom(t) ==
  int_term_ind(t;
               itermConstant(c)⇒ polyconst(c);
               itermVar(v)⇒ polyvar(v);
               itermAdd(l,r)⇒ rl,rr.eval p = rl in
                                     eval q = rr in
                                       add-polynom(p;q);
               itermSubtract(l,r)⇒ rl,rr.eval p = rl in
                                          eval q = rr in
                                          eval mq = mul-polynom(polyconst(-1);q) in
                                            add-polynom(p;mq);
               itermMultiply(l,r)⇒ rl,rr.eval p = rl in
                                          eval q = rr in
                                            mul-polynom(p;q);
               itermMinus(x)⇒ rx.eval p = rx in
                                  mul-polynom(polyconst(-1);p)) 



Home Index