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)`

`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 `

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

`∀[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