Theory: EVAL_ringNorm

Type operators

polynom : α polynom

Constants

Pconst : α -> α polynom
Pmult : α polynom -> α polynom -> α polynom
Popp : α polynom -> α polynom
Pplus : α polynom -> α polynom -> α polynom
Pvar : index -> α polynom
interp_p : α ring -> α varmap -> α polynom -> α
polynomMAP : (α -> β) -> α polynom -> β polynom
polynomREL : (α -> β -> bool) -> α polynom -> β polynom -> bool
polynomSET : α polynom -> α -> bool
polynom_CASE : α polynom -> (index -> β) -> (α -> β) -> (α polynom -> α polynom -> β) -> (α polynom -> α polynom -> β) -> (α polynom -> β) -> β
polynom_CONS : index + 'b1 + 'b1 polynom # 'b1 polynom + 'b1 polynom # 'b1 polynom + 'b1 polynom -> 'b1 polynom
polynom_normalize : α ring -> α polynom -> α canonical_sum
polynom_simplify : α ring -> α polynom -> α canonical_sum
polynom_size : (α -> num) -> α polynom -> num
r_canonical_sum_merge : α ring -> α canonical_sum -> α canonical_sum -> α canonical_sum
r_canonical_sum_prod : α ring -> α canonical_sum -> α canonical_sum -> α canonical_sum
r_canonical_sum_scalar : α ring -> α -> α canonical_sum -> α canonical_sum
r_canonical_sum_scalar2 : α ring -> index list -> α canonical_sum -> α canonical_sum
r_canonical_sum_scalar3 : α ring -> α -> index list -> α canonical_sum -> α canonical_sum
r_canonical_sum_simplify : α ring -> α canonical_sum -> α canonical_sum
r_ics_aux : α ring -> α varmap -> α -> α canonical_sum -> α
r_interp_cs : α ring -> α varmap -> α canonical_sum -> α
r_interp_m : α ring -> α varmap -> α -> index list -> α
r_interp_sp : α ring -> α varmap -> α spolynom -> α
r_interp_vl : α ring -> α varmap -> index list -> α
r_ivl_aux : α ring -> α varmap -> index -> index list -> α
r_monom_insert : α ring -> α -> index list -> α canonical_sum -> α canonical_sum
r_spolynom_normalize : α ring -> α spolynom -> α canonical_sum
r_spolynom_simplify : α ring -> α spolynom -> α canonical_sum
r_varlist_insert : α ring -> index list -> α canonical_sum -> α canonical_sum

Definitions

Theorems

Definitions

interp_p_def

⊢ (∀r vm c. interp_p r vm (Pconst c) = c) ∧
  (∀r vm i. interp_p r vm (Pvar i) = varmap_find i vm) ∧
  (∀r vm p1 p2.
     interp_p r vm (Pplus p1 p2) =
     r.RP (interp_p r vm p1) (interp_p r vm p2)) ∧
  (∀r vm p1 p2.
     interp_p r vm (Pmult p1 p2) =
     r.RM (interp_p r vm p1) (interp_p r vm p2)) ∧
  ∀r vm p1. interp_p r vm (Popp p1) = r.RN (interp_p r vm p1)

polynomMAP_def

⊢ ∀f af.
    polynomMAP f (polynom_CONS af) =
    polynom_CONS
      (SUM_MAP I
         (SUM_MAP f
            (SUM_MAP (polynomMAP f ## polynomMAP f)
               (SUM_MAP (polynomMAP f ## polynomMAP f) (polynomMAP f)))) af)

polynomREL_def

⊢ polynomREL =
  (λR x y.
     ∃z. (∀p. p ∈ polynomSET z ⇒ R (FST p) (SND p)) ∧
         polynomMAP FST z = x ∧ polynomMAP SND z = y)

polynomSET_def

⊢ ∀af.
    polynomSET (polynom_CONS af) =
    S ($UNION ∘ BIMG (K ∅) ∘ setL)
      (BIMG
         (S ($UNION ∘ BIMG $= ∘ setL)
            (BIMG
               (S
                  ($UNION ∘
                   BIMG
                     (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
                        (BIMG (K ∅) ∘ setSND)) ∘ setL)
                  (BIMG
                     (S
                        ($UNION ∘
                         BIMG
                           (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
                              (BIMG (K ∅) ∘ setSND)) ∘ setL)
                        (BIMG (K ∅) ∘ setR)) ∘ setR)) ∘ setR)) ∘ setR) af ∪
    BIGUNION
      (IMAGE polynomSET
         (S ($UNION ∘ BIMG (K ∅) ∘ setL)
            (BIMG
               (S ($UNION ∘ BIMG (K ∅) ∘ setL)
                  (BIMG
                     (S
                        ($UNION ∘
                         BIMG
                           (S ($UNION ∘ BIMG $= ∘ setFST)
                              (BIMG $= ∘ setSND)) ∘ setL)
                        (BIMG
                           (S
                              ($UNION ∘
                               BIMG
                                 (S ($UNION ∘ BIMG $= ∘ setFST)
                                    (BIMG $= ∘ setSND)) ∘ setL)
                              (BIMG $= ∘ setR)) ∘ setR)) ∘ setR)) ∘ setR)
            af))

polynom_case_def

⊢ (∀a0 f f0 f1 f2 f3. polynom_CASE (Pvar a0) f f0 f1 f2 f3 = f a0) ∧
  (∀a0 f f0 f1 f2 f3. polynom_CASE (Pconst a0) f f0 f1 f2 f3 = f0 a0) ∧
  (∀a0 a1 f f0 f1 f2 f3.
     polynom_CASE (Pplus a0 a1) f f0 f1 f2 f3 = f1 a0 a1) ∧
  (∀a0 a1 f f0 f1 f2 f3.
     polynom_CASE (Pmult a0 a1) f f0 f1 f2 f3 = f2 a0 a1) ∧
  ∀a0 f f0 f1 f2 f3. polynom_CASE (Popp a0) f f0 f1 f2 f3 = f3 a0

polynom_normalize_def

⊢ (∀r i. polynom_normalize r (Pvar i) = Cons_varlist [i] Nil_monom) ∧
  (∀r c. polynom_normalize r (Pconst c) = Cons_monom c [] Nil_monom) ∧
  (∀r pl pr.
     polynom_normalize r (Pplus pl pr) =
     r_canonical_sum_merge r (polynom_normalize r pl)
       (polynom_normalize r pr)) ∧
  (∀r pl pr.
     polynom_normalize r (Pmult pl pr) =
     r_canonical_sum_prod r (polynom_normalize r pl)
       (polynom_normalize r pr)) ∧
  ∀r p.
    polynom_normalize r (Popp p) =
    r_canonical_sum_scalar3 r (r.RN r.R1) [] (polynom_normalize r p)

polynom_simplify_def

⊢ ∀r x.
    polynom_simplify r x =
    r_canonical_sum_simplify r (polynom_normalize r x)

polynom_size_def

⊢ (∀f0 a0. polynom_size f0 (Pvar a0) = 1 + index_size a0) ∧
  (∀f0 a0. polynom_size f0 (Pconst a0) = 1 + f0 a0) ∧
  (∀f0 a0 a1.
     polynom_size f0 (Pplus a0 a1) =
     1 + (polynom_size f0 a0 + polynom_size f0 a1)) ∧
  (∀f0 a0 a1.
     polynom_size f0 (Pmult a0 a1) =
     1 + (polynom_size f0 a0 + polynom_size f0 a1)) ∧
  ∀f0 a0. polynom_size f0 (Popp a0) = 1 + polynom_size f0 a0

r_canonical_sum_merge_def

⊢ ∀r. r_canonical_sum_merge r = canonical_sum_merge (semi_ring_of r)

r_canonical_sum_prod_def

⊢ ∀r. r_canonical_sum_prod r = canonical_sum_prod (semi_ring_of r)

r_canonical_sum_scalar2_def

⊢ ∀r. r_canonical_sum_scalar2 r = canonical_sum_scalar2 (semi_ring_of r)

r_canonical_sum_scalar3_def

⊢ ∀r. r_canonical_sum_scalar3 r = canonical_sum_scalar3 (semi_ring_of r)

r_canonical_sum_scalar_def

⊢ ∀r. r_canonical_sum_scalar r = canonical_sum_scalar (semi_ring_of r)

r_canonical_sum_simplify_def

⊢ ∀r. r_canonical_sum_simplify r = canonical_sum_simplify (semi_ring_of r)

r_ics_aux_def

⊢ ∀r. r_ics_aux r = ics_aux (semi_ring_of r)

r_interp_cs_def

⊢ ∀r. r_interp_cs r = interp_cs (semi_ring_of r)

r_interp_m_def

⊢ ∀r. r_interp_m r = interp_m (semi_ring_of r)

r_interp_sp_def

⊢ ∀r. r_interp_sp r = interp_sp (semi_ring_of r)

r_interp_vl_def

⊢ ∀r. r_interp_vl r = interp_vl (semi_ring_of r)

r_ivl_aux_def

⊢ ∀r. r_ivl_aux r = ivl_aux (semi_ring_of r)

r_monom_insert_def

⊢ ∀r. r_monom_insert r = monom_insert (semi_ring_of r)

r_spolynom_normalize_def

⊢ ∀r. r_spolynom_normalize r = spolynom_normalize (semi_ring_of r)

r_spolynom_simplify_def

⊢ ∀r. r_spolynom_simplify r = spolynom_simplify (semi_ring_of r)

r_varlist_insert_def

⊢ ∀r. r_varlist_insert r = varlist_insert (semi_ring_of r)

Theorems

canonical_sum_merge_def

⊢ ∀r. (∀t2 t1 l2 l1 c2 c1.
         r_canonical_sum_merge r (Cons_monom c1 l1 t1)
           (Cons_monom c2 l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS =>
             Cons_monom c1 l1
               (r_canonical_sum_merge r t1 (Cons_monom c2 l2 t2))
         | EQUAL =>
           Cons_monom (r.RP c1 c2) l1 (r_canonical_sum_merge r t1 t2)
         | GREATER =>
           Cons_monom c2 l2
             (r_canonical_sum_merge r (Cons_monom c1 l1 t1) t2)) ∧
      (∀t2 t1 l2 l1 c1.
         r_canonical_sum_merge r (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS =>
             Cons_monom c1 l1
               (r_canonical_sum_merge r t1 (Cons_varlist l2 t2))
         | EQUAL =>
           Cons_monom (r.RP c1 r.R1) l1 (r_canonical_sum_merge r t1 t2)
         | GREATER =>
           Cons_varlist l2
             (r_canonical_sum_merge r (Cons_monom c1 l1 t1) t2)) ∧
      (∀t2 t1 l2 l1 c2.
         r_canonical_sum_merge r (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS =>
             Cons_varlist l1
               (r_canonical_sum_merge r t1 (Cons_monom c2 l2 t2))
         | EQUAL =>
           Cons_monom (r.RP r.R1 c2) l1 (r_canonical_sum_merge r t1 t2)
         | GREATER =>
           Cons_monom c2 l2
             (r_canonical_sum_merge r (Cons_varlist l1 t1) t2)) ∧
      (∀t2 t1 l2 l1.
         r_canonical_sum_merge r (Cons_varlist l1 t1) (Cons_varlist l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS =>
             Cons_varlist l1
               (r_canonical_sum_merge r t1 (Cons_varlist l2 t2))
         | EQUAL =>
           Cons_monom (r.RP r.R1 r.R1) l1 (r_canonical_sum_merge r t1 t2)
         | GREATER =>
           Cons_varlist l2
             (r_canonical_sum_merge r (Cons_varlist l1 t1) t2)) ∧
      (∀s1. r_canonical_sum_merge r s1 Nil_monom = s1) ∧
      (∀v6 v5 v4.
         r_canonical_sum_merge r Nil_monom (Cons_monom v4 v5 v6) =
         Cons_monom v4 v5 v6) ∧
      ∀v8 v7.
        r_canonical_sum_merge r Nil_monom (Cons_varlist v7 v8) =
        Cons_varlist v7 v8

canonical_sum_prod_def

⊢ ∀r. (∀c1 l1 t1 s2.
         r_canonical_sum_prod r (Cons_monom c1 l1 t1) s2 =
         r_canonical_sum_merge r (r_canonical_sum_scalar3 r c1 l1 s2)
           (r_canonical_sum_prod r t1 s2)) ∧
      (∀l1 t1 s2.
         r_canonical_sum_prod r (Cons_varlist l1 t1) s2 =
         r_canonical_sum_merge r (r_canonical_sum_scalar2 r l1 s2)
           (r_canonical_sum_prod r t1 s2)) ∧
      ∀s2. r_canonical_sum_prod r Nil_monom s2 = Nil_monom

canonical_sum_scalar2_def

⊢ ∀r. (∀l0 c l t.
         r_canonical_sum_scalar2 r l0 (Cons_monom c l t) =
         r_monom_insert r c (list_merge index_lt l0 l)
           (r_canonical_sum_scalar2 r l0 t)) ∧
      (∀l0 l t.
         r_canonical_sum_scalar2 r l0 (Cons_varlist l t) =
         r_varlist_insert r (list_merge index_lt l0 l)
           (r_canonical_sum_scalar2 r l0 t)) ∧
      ∀l0. r_canonical_sum_scalar2 r l0 Nil_monom = Nil_monom

canonical_sum_scalar3_def

⊢ ∀r. (∀c0 l0 c l t.
         r_canonical_sum_scalar3 r c0 l0 (Cons_monom c l t) =
         r_monom_insert r (r.RM c0 c) (list_merge index_lt l0 l)
           (r_canonical_sum_scalar3 r c0 l0 t)) ∧
      (∀c0 l0 l t.
         r_canonical_sum_scalar3 r c0 l0 (Cons_varlist l t) =
         r_monom_insert r c0 (list_merge index_lt l0 l)
           (r_canonical_sum_scalar3 r c0 l0 t)) ∧
      ∀c0 l0. r_canonical_sum_scalar3 r c0 l0 Nil_monom = Nil_monom

canonical_sum_scalar_def

⊢ ∀r. (∀c0 c l t.
         r_canonical_sum_scalar r c0 (Cons_monom c l t) =
         Cons_monom (r.RM c0 c) l (r_canonical_sum_scalar r c0 t)) ∧
      (∀c0 l t.
         r_canonical_sum_scalar r c0 (Cons_varlist l t) =
         Cons_monom c0 l (r_canonical_sum_scalar r c0 t)) ∧
      ∀c0. r_canonical_sum_scalar r c0 Nil_monom = Nil_monom

canonical_sum_simplify_def

⊢ ∀r. (∀c l t.
         r_canonical_sum_simplify r (Cons_monom c l t) =
         if c = r.R0 then r_canonical_sum_simplify r t
         else if c = r.R1 then
           Cons_varlist l (r_canonical_sum_simplify r t)
         else Cons_monom c l (r_canonical_sum_simplify r t)) ∧
      (∀l t.
         r_canonical_sum_simplify r (Cons_varlist l t) =
         Cons_varlist l (r_canonical_sum_simplify r t)) ∧
      r_canonical_sum_simplify r Nil_monom = Nil_monom

datatype_polynom

⊢ DATATYPE (polynom Pvar Pconst Pplus Pmult Popp)

ics_aux_def

⊢ ∀r. (∀vm a. r_ics_aux r vm a Nil_monom = a) ∧
      (∀vm a l t.
         r_ics_aux r vm a (Cons_varlist l t) =
         r.RP a (r_ics_aux r vm (r_interp_vl r vm l) t)) ∧
      ∀vm a c l t.
        r_ics_aux r vm a (Cons_monom c l t) =
        r.RP a (r_ics_aux r vm (r_interp_m r vm c l) t)

interp_cs_def

⊢ ∀r. (∀vm. r_interp_cs r vm Nil_monom = r.R0) ∧
      (∀vm l t.
         r_interp_cs r vm (Cons_varlist l t) =
         r_ics_aux r vm (r_interp_vl r vm l) t) ∧
      ∀vm c l t.
        r_interp_cs r vm (Cons_monom c l t) =
        r_ics_aux r vm (r_interp_m r vm c l) t

interp_m_def

⊢ ∀r. (∀vm c. r_interp_m r vm c [] = c) ∧
      ∀vm c x t. r_interp_m r vm c (x::t) = r.RM c (r_ivl_aux r vm x t)

interp_sp_def

⊢ ∀r. (∀vm c. r_interp_sp r vm (SPconst c) = c) ∧
      (∀vm i. r_interp_sp r vm (SPvar i) = varmap_find i vm) ∧
      (∀vm p1 p2.
         r_interp_sp r vm (SPplus p1 p2) =
         r.RP (r_interp_sp r vm p1) (r_interp_sp r vm p2)) ∧
      ∀vm p1 p2.
        r_interp_sp r vm (SPmult p1 p2) =
        r.RM (r_interp_sp r vm p1) (r_interp_sp r vm p2)

interp_vl_def

⊢ ∀r. (∀vm. r_interp_vl r vm [] = r.R1) ∧
      ∀vm x t. r_interp_vl r vm (x::t) = r_ivl_aux r vm x t

ivl_aux_def

⊢ ∀r. (∀vm x. r_ivl_aux r vm x [] = varmap_find x vm) ∧
      ∀vm x x' t'.
        r_ivl_aux r vm x (x'::t') =
        r.RM (varmap_find x vm) (r_ivl_aux r vm x' t')

monom_insert_def

⊢ ∀r. (∀t2 l2 l1 c2 c1.
         r_monom_insert r c1 l1 (Cons_monom c2 l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS => Cons_monom c1 l1 (Cons_monom c2 l2 t2)
         | EQUAL => Cons_monom (r.RP c1 c2) l1 t2
         | GREATER => Cons_monom c2 l2 (r_monom_insert r c1 l1 t2)) ∧
      (∀t2 l2 l1 c1.
         r_monom_insert r c1 l1 (Cons_varlist l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS => Cons_monom c1 l1 (Cons_varlist l2 t2)
         | EQUAL => Cons_monom (r.RP c1 r.R1) l1 t2
         | GREATER => Cons_varlist l2 (r_monom_insert r c1 l1 t2)) ∧
      ∀l1 c1. r_monom_insert r c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom

polynomMAP_ind

⊢ ∀P'.
    (∀f. (∀i. P' f (Pvar i)) ∧ (∀a. P' f (Pconst a)) ∧
         (∀p p0. P' f p ∧ P' f p0 ⇒ P' f (Pplus p p0)) ∧
         (∀p p0. P' f p ∧ P' f p0 ⇒ P' f (Pmult p p0)) ∧
         ∀p. P' f p ⇒ P' f (Popp p)) ⇒
    ∀f p. P' f p

polynomMAP_thm

⊢ polynomMAP f (Pvar a0) = Pvar a0 ∧
  polynomMAP f (Pconst a0) = Pconst (f a0) ∧
  polynomMAP f (Pplus a0 a1) = Pplus (polynomMAP f a0) (polynomMAP f a1) ∧
  polynomMAP f (Pmult a0 a1) = Pmult (polynomMAP f a0) (polynomMAP f a1) ∧
  polynomMAP f (Popp a0) = Popp (polynomMAP f a0)

polynomSET_ind

⊢ ∀P'.
    (∀i. P' (Pvar i)) ∧ (∀a. P' (Pconst a)) ∧
    (∀p p0. P' p ∧ P' p0 ⇒ P' (Pplus p p0)) ∧
    (∀p p0. P' p ∧ P' p0 ⇒ P' (Pmult p p0)) ∧ (∀p. P' p ⇒ P' (Popp p)) ⇒
    ∀p. P' p

polynomSET_thm

⊢ polynomSET (Pvar a0) = ∅ ∧ polynomSET (Pconst a0) = {a0} ∧
  polynomSET (Pplus a0 a1) = polynomSET a0 ∪ polynomSET a1 ∧
  polynomSET (Pmult a0 a1) = polynomSET a0 ∪ polynomSET a1 ∧
  polynomSET (Popp a0) = polynomSET a0

polynom_11

⊢ (∀a0 a0'. Pvar a0 = Pvar a0' ⇔ a0 = a0') ∧
  (∀a0 a0'. Pconst a0 = Pconst a0' ⇔ a0 = a0') ∧
  (∀a0 a1 a0' a1'. Pplus a0 a1 = Pplus a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
  (∀a0 a1 a0' a1'. Pmult a0 a1 = Pmult a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
  ∀a0 a0'. Popp a0 = Popp a0' ⇔ a0 = a0'

polynom_Axiom

⊢ ∀f0 f1 f2 f3 f4. ∃h.
    (∀a0. h (Pvar a0) = f0 a0) ∧ (∀a0. h (Pconst a0) = f1 a0) ∧
    (∀a0 a1. h (Pplus a0 a1) = f2 a0 a1 (h a0) (h a1)) ∧
    (∀a0 a1. h (Pmult a0 a1) = f3 a0 a1 (h a0) (h a1)) ∧
    ∀a0. h (Popp a0) = f4 a0 (h a0)

polynom_MAP_CONG

⊢ ∀f g x.
    (∀a. a ∈ polynomSET x ⇒ f a = g a) ⇒ polynomMAP f x = polynomMAP g x

polynom_MAP_ID

⊢ polynomMAP I = I

polynom_MAP_IMAGE

⊢ ∀f n. polynomSET (polynomMAP f n) = IMAGE f (polynomSET n)

polynom_MAP_O

⊢ polynomMAP f ∘ polynomMAP g = polynomMAP (f ∘ g)

polynom_bnd

⊢ ∀n. cardleq (polynomSET n) 𝕌(:num)

polynom_case_cong

⊢ ∀M M' f f0 f1 f2 f3.
    M = M' ∧ (∀a0. M' = Pvar a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = Pconst a0 ⇒ f0 a0 = f0' a0) ∧
    (∀a0 a1. M' = Pplus a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ∧
    (∀a0 a1. M' = Pmult a0 a1 ⇒ f2 a0 a1 = f2' a0 a1) ∧
    (∀a0. M' = Popp a0 ⇒ f3 a0 = f3' a0) ⇒
    polynom_CASE M f f0 f1 f2 f3 = polynom_CASE M' f' f0' f1' f2' f3'

polynom_case_eq

⊢ polynom_CASE x f f0 f1 f2 f3 = v ⇔
  (∃i. x = Pvar i ∧ f i = v) ∨ (∃a. x = Pconst a ∧ f0 a = v) ∨
  (∃p p0. x = Pplus p p0 ∧ f1 p p0 = v) ∨
  (∃p p0. x = Pmult p p0 ∧ f2 p p0 = v) ∨ ∃p. x = Popp p ∧ f3 p = v

polynom_distinct

⊢ (∀a0' a0. Pvar a0 ≠ Pconst a0') ∧ (∀a1 a0' a0. Pvar a0 ≠ Pplus a0' a1) ∧
  (∀a1 a0' a0. Pvar a0 ≠ Pmult a0' a1) ∧ (∀a0' a0. Pvar a0 ≠ Popp a0') ∧
  (∀a1 a0' a0. Pconst a0 ≠ Pplus a0' a1) ∧
  (∀a1 a0' a0. Pconst a0 ≠ Pmult a0' a1) ∧
  (∀a0' a0. Pconst a0 ≠ Popp a0') ∧
  (∀a1' a1 a0' a0. Pplus a0 a1 ≠ Pmult a0' a1') ∧
  (∀a1 a0' a0. Pplus a0 a1 ≠ Popp a0') ∧ ∀a1 a0' a0. Pmult a0 a1 ≠ Popp a0'

polynom_induction

⊢ ∀P. (∀i. P (Pvar i)) ∧ (∀a. P (Pconst a)) ∧
      (∀p p0. P p ∧ P p0 ⇒ P (Pplus p p0)) ∧
      (∀p p0. P p ∧ P p0 ⇒ P (Pmult p p0)) ∧ (∀p. P p ⇒ P (Popp p)) ⇒
      ∀p. P p

polynom_inh

⊢ ∀a2. a2 ∈ polynomSET ((λa2. polynom_CONS (INR (INL a2))) a2)

polynom_nchotomy

⊢ ∀pp.
    (∃i. pp = Pvar i) ∨ (∃a. pp = Pconst a) ∨ (∃p p0. pp = Pplus p p0) ∨
    (∃p p0. pp = Pmult p p0) ∨ ∃p. pp = Popp p

polynom_normalize_ok

⊢ ∀r. is_ring r ⇒
      ∀vm p. r_interp_cs r vm (polynom_normalize r p) = interp_p r vm p

polynom_simplify_ok

⊢ ∀r. is_ring r ⇒
      ∀vm p. r_interp_cs r vm (polynom_simplify r p) = interp_p r vm p

polynom_wit

⊢ ∀a. polynomSET ((λa. polynom_CONS ((K ∘ INL) ARB ARB)) a) ⊆ ∅

spolynom_normalize_def

⊢ ∀r. (∀i. r_spolynom_normalize r (SPvar i) = Cons_varlist [i] Nil_monom) ∧
      (∀c. r_spolynom_normalize r (SPconst c) = Cons_monom c [] Nil_monom) ∧
      (∀l r'.
         r_spolynom_normalize r (SPplus l r') =
         r_canonical_sum_merge r (r_spolynom_normalize r l)
           (r_spolynom_normalize r r')) ∧
      ∀l r'.
        r_spolynom_normalize r (SPmult l r') =
        r_canonical_sum_prod r (r_spolynom_normalize r l)
          (r_spolynom_normalize r r')

spolynom_simplify_def

⊢ ∀r x.
    r_spolynom_simplify r x =
    r_canonical_sum_simplify r (r_spolynom_normalize r x)

varlist_insert_def

⊢ ∀r. (∀t2 l2 l1 c2.
         r_varlist_insert r l1 (Cons_monom c2 l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS => Cons_varlist l1 (Cons_monom c2 l2 t2)
         | EQUAL => Cons_monom (r.RP r.R1 c2) l1 t2
         | GREATER => Cons_monom c2 l2 (r_varlist_insert r l1 t2)) ∧
      (∀t2 l2 l1.
         r_varlist_insert r l1 (Cons_varlist l2 t2) =
         case list_compare index_compare l1 l2 of
           LESS => Cons_varlist l1 (Cons_varlist l2 t2)
         | EQUAL => Cons_monom (r.RP r.R1 r.R1) l1 t2
         | GREATER => Cons_varlist l2 (r_varlist_insert r l1 t2)) ∧
      ∀l1. r_varlist_insert r l1 Nil_monom = Cons_varlist l1 Nil_monom

Theory EVAL_ringNorm

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems