Theory "canonical"

Parents semi_ring quote

Signature

Type	Arity
spolynom	1
canonical_sum	1
Constant	Type
varlist_insert_tupled	:'a semi_ring # index list # 'a canonical_sum -> 'a canonical_sum
varlist_insert	:'a semi_ring -> index list -> 'a canonical_sum -> 'a canonical_sum
spolynom_size	:('a -> num) -> 'a spolynom -> num
spolynom_simplify	:'a semi_ring -> 'a spolynom -> 'a canonical_sum
spolynom_normalize	:'a semi_ring -> 'a spolynom -> 'a canonical_sum
spolynom_case	:(index -> 'b) -> ('a -> 'b) -> ('a spolynom -> 'a spolynom -> 'b) -> ('a spolynom -> 'a spolynom -> 'b) -> 'a spolynom -> 'b
monom_insert_tupled	:'a semi_ring # 'a # index list # 'a canonical_sum -> 'a canonical_sum
monom_insert	:'a semi_ring -> 'a -> index list -> 'a canonical_sum -> 'a canonical_sum
mk_spolynom	:(index # 'a) recspace -> 'a spolynom
mk_canonical_sum	:('a # index list) recspace -> 'a canonical_sum
ivl_aux	:'a semi_ring -> 'a varmap -> index -> index list -> 'a
interp_vl	:'a semi_ring -> 'a varmap -> index list -> 'a
interp_sp	:'a semi_ring -> 'a varmap -> 'a spolynom -> 'a
interp_m	:'a semi_ring -> 'a varmap -> 'a -> index list -> 'a
interp_cs	:'a semi_ring -> 'a varmap -> 'a canonical_sum -> 'a
ics_aux	:'a semi_ring -> 'a varmap -> 'a -> 'a canonical_sum -> 'a
dest_spolynom	:'a spolynom -> (index # 'a) recspace
dest_canonical_sum	:'a canonical_sum -> ('a # index list) recspace
canonical_sum_size	:('a -> num) -> 'a canonical_sum -> num
canonical_sum_simplify	:'a semi_ring -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_scalar3	:'a semi_ring -> 'a -> index list -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_scalar2	:'a semi_ring -> index list -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_scalar	:'a semi_ring -> 'a -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_prod	:'a semi_ring -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_merge_tupled	:'a semi_ring # 'a canonical_sum # 'a canonical_sum -> 'a canonical_sum
canonical_sum_merge	:'a semi_ring -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
canonical_sum_case	:'b -> ('a -> index list -> 'a canonical_sum -> 'b) -> (index list -> 'a canonical_sum -> 'b) -> 'a canonical_sum -> 'b
canonical6	:'a spolynom -> 'a spolynom -> 'a spolynom
canonical5	:'a spolynom -> 'a spolynom -> 'a spolynom
canonical4	:'a -> 'a spolynom
canonical3	:index -> 'a spolynom
canonical2	:index list -> 'a canonical_sum -> 'a canonical_sum
canonical1	:'a -> index list -> 'a canonical_sum -> 'a canonical_sum
canonical0	:'a canonical_sum
SPvar	:index -> 'a spolynom
SPplus	:'a spolynom -> 'a spolynom -> 'a spolynom
SPmult	:'a spolynom -> 'a spolynom -> 'a spolynom
SPconst	:'a -> 'a spolynom
Nil_monom	:'a canonical_sum
Cons_varlist	:index list -> 'a canonical_sum -> 'a canonical_sum
Cons_monom	:'a -> index list -> 'a canonical_sum -> 'a canonical_sum

Definitions

canonical_sum_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'canonical_sum'.
            (!a0'.
               (a0' =
                ind_type$CONSTR 0 ((@v. T), @v. T) (\n. ind_type$BOTTOM)) \/
               (?a0 a1 a2.
                  (a0' =
                   (\a0 a1 a2.
                      ind_type$CONSTR (SUC 0) (a0,a1)
                        (FCONS a2 (\n. ind_type$BOTTOM))) a0 a1 a2) /\
                  'canonical_sum' a2) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC 0)) ((@v. T),a0)
                        (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
                  'canonical_sum' a1) ==>
               'canonical_sum' a0') ==>
            'canonical_sum' a0') rep

canonical_sum_repfns

|- (!a. mk_canonical_sum (dest_canonical_sum a) = a) /\
   !r.
     (\a0'.
        !'canonical_sum'.
          (!a0'.
             (a0' =
              ind_type$CONSTR 0 ((@v. T), @v. T) (\n. ind_type$BOTTOM)) \/
             (?a0 a1 a2.
                (a0' =
                 (\a0 a1 a2.
                    ind_type$CONSTR (SUC 0) (a0,a1)
                      (FCONS a2 (\n. ind_type$BOTTOM))) a0 a1 a2) /\
                'canonical_sum' a2) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC 0)) ((@v. T),a0)
                      (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
                'canonical_sum' a1) ==>
             'canonical_sum' a0') ==>
          'canonical_sum' a0') r =
     (dest_canonical_sum (mk_canonical_sum r) = r)

canonical0_def

|- canonical0 =
   mk_canonical_sum (ind_type$CONSTR 0 ((@v. T), @v. T) (\n. ind_type$BOTTOM))

canonical1_def

|- canonical1 =
   (\a0 a1 a2.
      mk_canonical_sum
        ((\a0 a1 a2.
            ind_type$CONSTR (SUC 0) (a0,a1) (FCONS a2 (\n. ind_type$BOTTOM)))
           a0 a1 (dest_canonical_sum a2)))

canonical2_def

|- canonical2 =
   (\a0 a1.
      mk_canonical_sum
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC 0)) ((@v. T),a0)
              (FCONS a1 (\n. ind_type$BOTTOM))) a0 (dest_canonical_sum a1)))

Nil_monom

|- Nil_monom = canonical0

Cons_monom

|- Cons_monom = canonical1

Cons_varlist

|- Cons_varlist = canonical2

canonical_sum_case_def

|- (!v f f1. canonical_sum_case v f f1 Nil_monom = v) /\
   (!v f f1 a0 a1 a2.
      canonical_sum_case v f f1 (Cons_monom a0 a1 a2) = f a0 a1 a2) /\
   !v f f1 a0 a1. canonical_sum_case v f f1 (Cons_varlist a0 a1) = f1 a0 a1

canonical_sum_size_def

|- (!f. canonical_sum_size f Nil_monom = 0) /\
   (!f a0 a1 a2.
      canonical_sum_size f (Cons_monom a0 a1 a2) =
      1 + (f a0 + (list_size index_size a1 + canonical_sum_size f a2))) /\
   !f a0 a1.
     canonical_sum_size f (Cons_varlist a0 a1) =
     1 + (list_size index_size a0 + canonical_sum_size f a1)

canonical_sum_merge_tupled_primitive_def

|- canonical_sum_merge_tupled =
   WFREC
     (@R.
        WF R /\
        (!l2 c2 t2 t1 l1 c1 sr.
           R (sr,Cons_monom c1 l1 t1,t2)
             (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) /\
        (!l1 c1 t2 l2 c2 t1 sr.
           R (sr,t1,Cons_monom c2 l2 t2)
             (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) /\
        (!l2 c2 l1 c1 t2 t1 sr.
           R (sr,t1,t2) (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) /\
        (!l2 t2 t1 l1 c1 sr.
           R (sr,Cons_monom c1 l1 t1,t2)
             (sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) /\
        (!l1 c1 t2 l2 t1 sr.
           R (sr,t1,Cons_varlist l2 t2)
             (sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) /\
        (!l2 l1 c1 t2 t1 sr.
           R (sr,t1,t2) (sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) /\
        (!l2 c2 t2 t1 l1 sr.
           R (sr,Cons_varlist l1 t1,t2)
             (sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) /\
        (!l1 t2 l2 c2 t1 sr.
           R (sr,t1,Cons_monom c2 l2 t2)
             (sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) /\
        (!l2 c2 l1 t2 t1 sr.
           R (sr,t1,t2) (sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) /\
        (!l2 l1 t2 t1 sr.
           R (sr,t1,t2) (sr,Cons_varlist l1 t1,Cons_varlist l2 t2)) /\
        (!l1 t2 l2 t1 sr.
           R (sr,t1,Cons_varlist l2 t2)
             (sr,Cons_varlist l1 t1,Cons_varlist l2 t2)) /\
        !l2 t2 t1 l1 sr.
          R (sr,Cons_varlist l1 t1,t2)
            (sr,Cons_varlist l1 t1,Cons_varlist l2 t2))
     (\canonical_sum_merge_tupled a.
        case a of
           (sr,Nil_monom,Nil_monom) -> I Nil_monom
        || (sr,Nil_monom,Cons_monom v19 v20 v21) -> I (Cons_monom v19 v20 v21)
        || (sr,Nil_monom,Cons_varlist v22 v23) -> I (Cons_varlist v22 v23)
        || (sr,Cons_monom c1 l1 t1,Nil_monom) -> I (Cons_monom c1 l1 t1)
        || (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2) ->
             I
               (compare (list_compare index_compare l1 l2)
                  (Cons_monom c1 l1
                     (canonical_sum_merge_tupled (sr,t1,Cons_monom c2 l2 t2)))
                  (Cons_monom (SRP sr c1 c2) l1
                     (canonical_sum_merge_tupled (sr,t1,t2)))
                  (Cons_monom c2 l2
                     (canonical_sum_merge_tupled
                        (sr,Cons_monom c1 l1 t1,t2))))
        || (sr,Cons_monom c1 l1 t1,Cons_varlist l2' t2') ->
             I
               (compare (list_compare index_compare l1 l2')
                  (Cons_monom c1 l1
                     (canonical_sum_merge_tupled
                        (sr,t1,Cons_varlist l2' t2')))
                  (Cons_monom (SRP sr c1 (SR1 sr)) l1
                     (canonical_sum_merge_tupled (sr,t1,t2')))
                  (Cons_varlist l2'
                     (canonical_sum_merge_tupled
                        (sr,Cons_monom c1 l1 t1,t2'))))
        || (sr,Cons_varlist l1' t1',Nil_monom) -> I (Cons_varlist l1' t1')
        || (sr,Cons_varlist l1' t1',Cons_monom c2' l2'' t2'') ->
             I
               (compare (list_compare index_compare l1' l2'')
                  (Cons_varlist l1'
                     (canonical_sum_merge_tupled
                        (sr,t1',Cons_monom c2' l2'' t2'')))
                  (Cons_monom (SRP sr (SR1 sr) c2') l1'
                     (canonical_sum_merge_tupled (sr,t1',t2'')))
                  (Cons_monom c2' l2''
                     (canonical_sum_merge_tupled
                        (sr,Cons_varlist l1' t1',t2''))))
        || (sr,Cons_varlist l1' t1',Cons_varlist l2''' t2''') ->
             I
               (compare (list_compare index_compare l1' l2''')
                  (Cons_varlist l1'
                     (canonical_sum_merge_tupled
                        (sr,t1',Cons_varlist l2''' t2''')))
                  (Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1'
                     (canonical_sum_merge_tupled (sr,t1',t2''')))
                  (Cons_varlist l2'''
                     (canonical_sum_merge_tupled
                        (sr,Cons_varlist l1' t1',t2''')))))

canonical_sum_merge_curried_def

|- !x x1 x2.
     canonical_sum_merge x x1 x2 = canonical_sum_merge_tupled (x,x1,x2)

monom_insert_tupled_primitive_def

|- monom_insert_tupled =
   WFREC
     (@R.
        WF R /\
        (!l2 c2 t2 l1 c1 sr.
           R (sr,c1,l1,t2) (sr,c1,l1,Cons_monom c2 l2 t2)) /\
        !l2 t2 l1 c1 sr. R (sr,c1,l1,t2) (sr,c1,l1,Cons_varlist l2 t2))
     (\monom_insert_tupled a.
        case a of
           (sr,c1,l1,Nil_monom) -> I (Cons_monom c1 l1 Nil_monom)
        || (sr,c1,l1,Cons_monom c2 l2 t2) ->
             I
               (compare (list_compare index_compare l1 l2)
                  (Cons_monom c1 l1 (Cons_monom c2 l2 t2))
                  (Cons_monom (SRP sr c1 c2) l1 t2)
                  (Cons_monom c2 l2 (monom_insert_tupled (sr,c1,l1,t2))))
        || (sr,c1,l1,Cons_varlist l2' t2') ->
             I
               (compare (list_compare index_compare l1 l2')
                  (Cons_monom c1 l1 (Cons_varlist l2' t2'))
                  (Cons_monom (SRP sr c1 (SR1 sr)) l1 t2')
                  (Cons_varlist l2' (monom_insert_tupled (sr,c1,l1,t2')))))

monom_insert_curried_def

|- !x x1 x2 x3. monom_insert x x1 x2 x3 = monom_insert_tupled (x,x1,x2,x3)

varlist_insert_tupled_primitive_def

|- varlist_insert_tupled =
   WFREC
     (@R.
        WF R /\ (!l2 c2 t2 l1 sr. R (sr,l1,t2) (sr,l1,Cons_monom c2 l2 t2)) /\
        !l2 t2 l1 sr. R (sr,l1,t2) (sr,l1,Cons_varlist l2 t2))
     (\varlist_insert_tupled a.
        case a of
           (sr,l1,Nil_monom) -> I (Cons_varlist l1 Nil_monom)
        || (sr,l1,Cons_monom c2 l2 t2) ->
             I
               (compare (list_compare index_compare l1 l2)
                  (Cons_varlist l1 (Cons_monom c2 l2 t2))
                  (Cons_monom (SRP sr (SR1 sr) c2) l1 t2)
                  (Cons_monom c2 l2 (varlist_insert_tupled (sr,l1,t2))))
        || (sr,l1,Cons_varlist l2' t2') ->
             I
               (compare (list_compare index_compare l1 l2')
                  (Cons_varlist l1 (Cons_varlist l2' t2'))
                  (Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1 t2')
                  (Cons_varlist l2' (varlist_insert_tupled (sr,l1,t2')))))

varlist_insert_curried_def

|- !x x1 x2. varlist_insert x x1 x2 = varlist_insert_tupled (x,x1,x2)

canonical_sum_scalar_def

|- (!sr c0 c l t.
      canonical_sum_scalar sr c0 (Cons_monom c l t) =
      Cons_monom (SRM sr c0 c) l (canonical_sum_scalar sr c0 t)) /\
   (!sr c0 l t.
      canonical_sum_scalar sr c0 (Cons_varlist l t) =
      Cons_monom c0 l (canonical_sum_scalar sr c0 t)) /\
   !sr c0. canonical_sum_scalar sr c0 Nil_monom = Nil_monom

canonical_sum_scalar2_def

|- (!sr l0 c l t.
      canonical_sum_scalar2 sr l0 (Cons_monom c l t) =
      monom_insert sr c (list_merge index_lt l0 l)
        (canonical_sum_scalar2 sr l0 t)) /\
   (!sr l0 l t.
      canonical_sum_scalar2 sr l0 (Cons_varlist l t) =
      varlist_insert sr (list_merge index_lt l0 l)
        (canonical_sum_scalar2 sr l0 t)) /\
   !sr l0. canonical_sum_scalar2 sr l0 Nil_monom = Nil_monom

canonical_sum_scalar3_def

|- (!sr c0 l0 c l t.
      canonical_sum_scalar3 sr c0 l0 (Cons_monom c l t) =
      monom_insert sr (SRM sr c0 c) (list_merge index_lt l0 l)
        (canonical_sum_scalar3 sr c0 l0 t)) /\
   (!sr c0 l0 l t.
      canonical_sum_scalar3 sr c0 l0 (Cons_varlist l t) =
      monom_insert sr c0 (list_merge index_lt l0 l)
        (canonical_sum_scalar3 sr c0 l0 t)) /\
   !sr c0 l0. canonical_sum_scalar3 sr c0 l0 Nil_monom = Nil_monom

canonical_sum_prod_def

|- (!sr c1 l1 t1 s2.
      canonical_sum_prod sr (Cons_monom c1 l1 t1) s2 =
      canonical_sum_merge sr (canonical_sum_scalar3 sr c1 l1 s2)
        (canonical_sum_prod sr t1 s2)) /\
   (!sr l1 t1 s2.
      canonical_sum_prod sr (Cons_varlist l1 t1) s2 =
      canonical_sum_merge sr (canonical_sum_scalar2 sr l1 s2)
        (canonical_sum_prod sr t1 s2)) /\
   !sr s2. canonical_sum_prod sr Nil_monom s2 = Nil_monom

canonical_sum_simplify_def

|- (!sr c l t.
      canonical_sum_simplify sr (Cons_monom c l t) =
      (if c = SR0 sr then
         canonical_sum_simplify sr t
       else
         (if c = SR1 sr then
            Cons_varlist l (canonical_sum_simplify sr t)
          else
            Cons_monom c l (canonical_sum_simplify sr t)))) /\
   (!sr l t.
      canonical_sum_simplify sr (Cons_varlist l t) =
      Cons_varlist l (canonical_sum_simplify sr t)) /\
   !sr. canonical_sum_simplify sr Nil_monom = Nil_monom

ivl_aux_def

|- (!sr vm x. ivl_aux sr vm x [] = varmap_find x vm) /\
   !sr vm x x' t'.
     ivl_aux sr vm x (x'::t') =
     SRM sr (varmap_find x vm) (ivl_aux sr vm x' t')

interp_vl_def

|- (!sr vm. interp_vl sr vm [] = SR1 sr) /\
   !sr vm x t. interp_vl sr vm (x::t) = ivl_aux sr vm x t

interp_m_def

|- (!sr vm c. interp_m sr vm c [] = c) /\
   !sr vm c x t. interp_m sr vm c (x::t) = SRM sr c (ivl_aux sr vm x t)

ics_aux_def

|- (!sr vm a. ics_aux sr vm a Nil_monom = a) /\
   (!sr vm a l t.
      ics_aux sr vm a (Cons_varlist l t) =
      SRP sr a (ics_aux sr vm (interp_vl sr vm l) t)) /\
   !sr vm a c l t.
     ics_aux sr vm a (Cons_monom c l t) =
     SRP sr a (ics_aux sr vm (interp_m sr vm c l) t)

interp_cs_def

|- (!sr vm. interp_cs sr vm Nil_monom = SR0 sr) /\
   (!sr vm l t.
      interp_cs sr vm (Cons_varlist l t) =
      ics_aux sr vm (interp_vl sr vm l) t) /\
   !sr vm c l t.
     interp_cs sr vm (Cons_monom c l t) = ics_aux sr vm (interp_m sr vm c l) t

spolynom_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'spolynom'.
            (!a0'.
               (?a.
                  a0' =
                  (\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM))
                    a) \/
               (?a.
                  a0' =
                  (\a.
                     ind_type$CONSTR (SUC 0) ((@v. T),a)
                       (\n. ind_type$BOTTOM)) a) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC 0)) ((@v. T), @v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'spolynom' a0 /\ 'spolynom' a1) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC (SUC 0))) ((@v. T), @v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'spolynom' a0 /\ 'spolynom' a1) ==>
               'spolynom' a0') ==>
            'spolynom' a0') rep

spolynom_repfns

|- (!a. mk_spolynom (dest_spolynom a) = a) /\
   !r.
     (\a0'.
        !'spolynom'.
          (!a0'.
             (?a.
                a0' =
                (\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM)) a) \/
             (?a.
                a0' =
                (\a.
                   ind_type$CONSTR (SUC 0) ((@v. T),a) (\n. ind_type$BOTTOM))
                  a) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC 0)) ((@v. T), @v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'spolynom' a0 /\ 'spolynom' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) ((@v. T), @v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'spolynom' a0 /\ 'spolynom' a1) ==>
             'spolynom' a0') ==>
          'spolynom' a0') r =
     (dest_spolynom (mk_spolynom r) = r)

canonical3_def

|- canonical3 =
   (\a.
      mk_spolynom
        ((\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM)) a))

canonical4_def

|- canonical4 =
   (\a.
      mk_spolynom
        ((\a. ind_type$CONSTR (SUC 0) ((@v. T),a) (\n. ind_type$BOTTOM)) a))

canonical5_def

|- canonical5 =
   (\a0 a1.
      mk_spolynom
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC 0)) ((@v. T), @v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_spolynom a0)
           (dest_spolynom a1)))

canonical6_def

|- canonical6 =
   (\a0 a1.
      mk_spolynom
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC 0))) ((@v. T), @v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_spolynom a0)
           (dest_spolynom a1)))

SPvar

|- SPvar = canonical3

SPconst

|- SPconst = canonical4

SPplus

|- SPplus = canonical5

SPmult

|- SPmult = canonical6

spolynom_case_def

|- (!f f1 f2 f3 a. spolynom_case f f1 f2 f3 (SPvar a) = f a) /\
   (!f f1 f2 f3 a. spolynom_case f f1 f2 f3 (SPconst a) = f1 a) /\
   (!f f1 f2 f3 a0 a1. spolynom_case f f1 f2 f3 (SPplus a0 a1) = f2 a0 a1) /\
   !f f1 f2 f3 a0 a1. spolynom_case f f1 f2 f3 (SPmult a0 a1) = f3 a0 a1

spolynom_size_def

|- (!f a. spolynom_size f (SPvar a) = 1 + index_size a) /\
   (!f a. spolynom_size f (SPconst a) = 1 + f a) /\
   (!f a0 a1.
      spolynom_size f (SPplus a0 a1) =
      1 + (spolynom_size f a0 + spolynom_size f a1)) /\
   !f a0 a1.
     spolynom_size f (SPmult a0 a1) =
     1 + (spolynom_size f a0 + spolynom_size f a1)

spolynom_normalize_def

|- (!sr i. spolynom_normalize sr (SPvar i) = Cons_varlist [i] Nil_monom) /\
   (!sr c. spolynom_normalize sr (SPconst c) = Cons_monom c [] Nil_monom) /\
   (!sr l r.
      spolynom_normalize sr (SPplus l r) =
      canonical_sum_merge sr (spolynom_normalize sr l)
        (spolynom_normalize sr r)) /\
   !sr l r.
     spolynom_normalize sr (SPmult l r) =
     canonical_sum_prod sr (spolynom_normalize sr l) (spolynom_normalize sr r)

spolynom_simplify_def

|- !sr x.
     spolynom_simplify sr x =
     canonical_sum_simplify sr (spolynom_normalize sr x)

interp_sp_def

|- (!sr vm c. interp_sp sr vm (SPconst c) = c) /\
   (!sr vm i. interp_sp sr vm (SPvar i) = varmap_find i vm) /\
   (!sr vm p1 p2.
      interp_sp sr vm (SPplus p1 p2) =
      SRP sr (interp_sp sr vm p1) (interp_sp sr vm p2)) /\
   !sr vm p1 p2.
     interp_sp sr vm (SPmult p1 p2) =
     SRM sr (interp_sp sr vm p1) (interp_sp sr vm p2)

Theorems

datatype_canonical_sum

|- DATATYPE (canonical_sum Nil_monom Cons_monom Cons_varlist)

canonical_sum_11

|- (!a0 a1 a2 a0' a1' a2'.
      (Cons_monom a0 a1 a2 = Cons_monom a0' a1' a2') =
      (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\
   !a0 a1 a0' a1'.
     (Cons_varlist a0 a1 = Cons_varlist a0' a1') = (a0 = a0') /\ (a1 = a1')

canonical_sum_distinct

|- (!a2 a1 a0. ~(Nil_monom = Cons_monom a0 a1 a2)) /\
   (!a1 a0. ~(Nil_monom = Cons_varlist a0 a1)) /\
   !a2 a1' a1 a0' a0. ~(Cons_monom a0 a1 a2 = Cons_varlist a0' a1')

canonical_sum_case_cong

|- !M M' v f f1.
     (M = M') /\ ((M' = Nil_monom) ==> (v = v')) /\
     (!a0 a1 a2. (M' = Cons_monom a0 a1 a2) ==> (f a0 a1 a2 = f' a0 a1 a2)) /\
     (!a0 a1. (M' = Cons_varlist a0 a1) ==> (f1 a0 a1 = f1' a0 a1)) ==>
     (canonical_sum_case v f f1 M = canonical_sum_case v' f' f1' M')

canonical_sum_nchotomy

|- !c.
     (c = Nil_monom) \/ (?a l c'. c = Cons_monom a l c') \/
     ?l c'. c = Cons_varlist l c'

canonical_sum_Axiom

|- !f0 f1 f2.
     ?fn.
       (fn Nil_monom = f0) /\
       (!a0 a1 a2. fn (Cons_monom a0 a1 a2) = f1 a0 a1 a2 (fn a2)) /\
       !a0 a1. fn (Cons_varlist a0 a1) = f2 a0 a1 (fn a1)

canonical_sum_induction

|- !P.
     P Nil_monom /\ (!c. P c ==> !l a. P (Cons_monom a l c)) /\
     (!c. P c ==> !l. P (Cons_varlist l c)) ==>
     !c. P c

canonical_sum_merge_ind

|- !P.
     (!sr c1 l1 t1 c2 l2 t2.
        P sr t1 t2 /\ P sr t1 (Cons_monom c2 l2 t2) /\
        P sr (Cons_monom c1 l1 t1) t2 ==>
        P sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2)) /\
     (!sr c1 l1 t1 l2 t2.
        P sr t1 t2 /\ P sr t1 (Cons_varlist l2 t2) /\
        P sr (Cons_monom c1 l1 t1) t2 ==>
        P sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2)) /\
     (!sr l1 t1 c2 l2 t2.
        P sr t1 t2 /\ P sr t1 (Cons_monom c2 l2 t2) /\
        P sr (Cons_varlist l1 t1) t2 ==>
        P sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2)) /\
     (!sr l1 t1 l2 t2.
        P sr t1 t2 /\ P sr t1 (Cons_varlist l2 t2) /\
        P sr (Cons_varlist l1 t1) t2 ==>
        P sr (Cons_varlist l1 t1) (Cons_varlist l2 t2)) /\
     (!sr v7 v8. P sr (Cons_varlist v7 v8) Nil_monom) /\
     (!sr v4 v5 v6. P sr (Cons_monom v4 v5 v6) Nil_monom) /\
     (!sr. P sr Nil_monom Nil_monom) /\
     (!sr v17 v18. P sr Nil_monom (Cons_varlist v17 v18)) /\
     (!sr v14 v15 v16. P sr Nil_monom (Cons_monom v14 v15 v16)) ==>
     !v v1 v2. P v v1 v2

canonical_sum_merge_def

|- (canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2)))
      (Cons_monom (SRP sr c1 c2) l1 (canonical_sum_merge sr t1 t2))
      (Cons_monom c2 l2 (canonical_sum_merge sr (Cons_monom c1 l1 t1) t2))) /\
   (canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2)))
      (Cons_monom (SRP sr c1 (SR1 sr)) l1 (canonical_sum_merge sr t1 t2))
      (Cons_varlist l2 (canonical_sum_merge sr (Cons_monom c1 l1 t1) t2))) /\
   (canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2)))
      (Cons_monom (SRP sr (SR1 sr) c2) l1 (canonical_sum_merge sr t1 t2))
      (Cons_monom c2 l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2))) /\
   (canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_varlist l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2)))
      (Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1
         (canonical_sum_merge sr t1 t2))
      (Cons_varlist l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2))) /\
   (canonical_sum_merge sr (Cons_varlist v7 v8) Nil_monom =
    Cons_varlist v7 v8) /\
   (canonical_sum_merge sr (Cons_monom v4 v5 v6) Nil_monom =
    Cons_monom v4 v5 v6) /\
   (canonical_sum_merge sr Nil_monom Nil_monom = Nil_monom) /\
   (canonical_sum_merge sr Nil_monom (Cons_varlist v17 v18) =
    Cons_varlist v17 v18) /\
   (canonical_sum_merge sr Nil_monom (Cons_monom v14 v15 v16) =
    Cons_monom v14 v15 v16)

monom_insert_ind

|- !P.
     (!sr c1 l1 c2 l2 t2.
        P sr c1 l1 t2 ==> P sr c1 l1 (Cons_monom c2 l2 t2)) /\
     (!sr c1 l1 l2 t2. P sr c1 l1 t2 ==> P sr c1 l1 (Cons_varlist l2 t2)) /\
     (!sr c1 l1. P sr c1 l1 Nil_monom) ==>
     !v v1 v2 v3. P v v1 v2 v3

monom_insert_def

|- (monom_insert sr c1 l1 (Cons_monom c2 l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_monom c1 l1 (Cons_monom c2 l2 t2))
      (Cons_monom (SRP sr c1 c2) l1 t2)
      (Cons_monom c2 l2 (monom_insert sr c1 l1 t2))) /\
   (monom_insert sr c1 l1 (Cons_varlist l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_monom c1 l1 (Cons_varlist l2 t2))
      (Cons_monom (SRP sr c1 (SR1 sr)) l1 t2)
      (Cons_varlist l2 (monom_insert sr c1 l1 t2))) /\
   (monom_insert sr c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom)

varlist_insert_ind

|- !P.
     (!sr l1 c2 l2 t2. P sr l1 t2 ==> P sr l1 (Cons_monom c2 l2 t2)) /\
     (!sr l1 l2 t2. P sr l1 t2 ==> P sr l1 (Cons_varlist l2 t2)) /\
     (!sr l1. P sr l1 Nil_monom) ==>
     !v v1 v2. P v v1 v2

varlist_insert_def

|- (varlist_insert sr l1 (Cons_monom c2 l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_varlist l1 (Cons_monom c2 l2 t2))
      (Cons_monom (SRP sr (SR1 sr) c2) l1 t2)
      (Cons_monom c2 l2 (varlist_insert sr l1 t2))) /\
   (varlist_insert sr l1 (Cons_varlist l2 t2) =
    compare (list_compare index_compare l1 l2)
      (Cons_varlist l1 (Cons_varlist l2 t2))
      (Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1 t2)
      (Cons_varlist l2 (varlist_insert sr l1 t2))) /\
   (varlist_insert sr l1 Nil_monom = Cons_varlist l1 Nil_monom)

ivl_aux_ok

|- !sr.
     is_semi_ring sr ==>
     !vm v i.
       ivl_aux sr vm i v = SRM sr (varmap_find i vm) (interp_vl sr vm v)

varlist_merge_ok

|- !sr.
     is_semi_ring sr ==>
     !vm x y.
       interp_vl sr vm (list_merge index_lt x y) =
       SRM sr (interp_vl sr vm x) (interp_vl sr vm y)

ics_aux_ok

|- !sr.
     is_semi_ring sr ==>
     !vm x s. ics_aux sr vm x s = SRP sr x (interp_cs sr vm s)

interp_m_ok

|- !sr.
     is_semi_ring sr ==>
     !vm x l. interp_m sr vm x l = SRM sr x (interp_vl sr vm l)

canonical_sum_merge_ok

|- !sr.
     is_semi_ring sr ==>
     !vm x y.
       interp_cs sr vm (canonical_sum_merge sr x y) =
       SRP sr (interp_cs sr vm x) (interp_cs sr vm y)

monom_insert_ok

|- !sr.
     is_semi_ring sr ==>
     !vm a l s.
       interp_cs sr vm (monom_insert sr a l s) =
       SRP sr (SRM sr a (interp_vl sr vm l)) (interp_cs sr vm s)

varlist_insert_ok

|- !sr.
     is_semi_ring sr ==>
     !vm l s.
       interp_cs sr vm (varlist_insert sr l s) =
       SRP sr (interp_vl sr vm l) (interp_cs sr vm s)

canonical_sum_scalar_ok

|- !sr.
     is_semi_ring sr ==>
     !vm a s.
       interp_cs sr vm (canonical_sum_scalar sr a s) =
       SRM sr a (interp_cs sr vm s)

canonical_sum_scalar2_ok

|- !sr.
     is_semi_ring sr ==>
     !vm l s.
       interp_cs sr vm (canonical_sum_scalar2 sr l s) =
       SRM sr (interp_vl sr vm l) (interp_cs sr vm s)

canonical_sum_scalar3_ok

|- !sr.
     is_semi_ring sr ==>
     !vm c l s.
       interp_cs sr vm (canonical_sum_scalar3 sr c l s) =
       SRM sr (SRM sr c (interp_vl sr vm l)) (interp_cs sr vm s)

canonical_sum_prod_ok

|- !sr.
     is_semi_ring sr ==>
     !vm x y.
       interp_cs sr vm (canonical_sum_prod sr x y) =
       SRM sr (interp_cs sr vm x) (interp_cs sr vm y)

canonical_sum_simplify_ok

|- !sr.
     is_semi_ring sr ==>
     !vm s. interp_cs sr vm (canonical_sum_simplify sr s) = interp_cs sr vm s

datatype_spolynom

|- DATATYPE (spolynom SPvar SPconst SPplus SPmult)

spolynom_11

|- (!a a'. (SPvar a = SPvar a') = (a = a')) /\
   (!a a'. (SPconst a = SPconst a') = (a = a')) /\
   (!a0 a1 a0' a1'.
      (SPplus a0 a1 = SPplus a0' a1') = (a0 = a0') /\ (a1 = a1')) /\
   !a0 a1 a0' a1'. (SPmult a0 a1 = SPmult a0' a1') = (a0 = a0') /\ (a1 = a1')

spolynom_distinct

|- (!a' a. ~(SPvar a = SPconst a')) /\
   (!a1 a0 a. ~(SPvar a = SPplus a0 a1)) /\
   (!a1 a0 a. ~(SPvar a = SPmult a0 a1)) /\
   (!a1 a0 a. ~(SPconst a = SPplus a0 a1)) /\
   (!a1 a0 a. ~(SPconst a = SPmult a0 a1)) /\
   !a1' a1 a0' a0. ~(SPplus a0 a1 = SPmult a0' a1')

spolynom_case_cong

|- !M M' f f1 f2 f3.
     (M = M') /\ (!a. (M' = SPvar a) ==> (f a = f' a)) /\
     (!a. (M' = SPconst a) ==> (f1 a = f1' a)) /\
     (!a0 a1. (M' = SPplus a0 a1) ==> (f2 a0 a1 = f2' a0 a1)) /\
     (!a0 a1. (M' = SPmult a0 a1) ==> (f3 a0 a1 = f3' a0 a1)) ==>
     (spolynom_case f f1 f2 f3 M = spolynom_case f' f1' f2' f3' M')

spolynom_nchotomy

|- !s.
     (?i. s = SPvar i) \/ (?a. s = SPconst a) \/ (?s' s0. s = SPplus s' s0) \/
     ?s' s0. s = SPmult s' s0

spolynom_Axiom

|- !f0 f1 f2 f3.
     ?fn.
       (!a. fn (SPvar a) = f0 a) /\ (!a. fn (SPconst a) = f1 a) /\
       (!a0 a1. fn (SPplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) /\
       !a0 a1. fn (SPmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)

spolynom_induction

|- !P.
     (!i. P (SPvar i)) /\ (!a. P (SPconst a)) /\
     (!s s0. P s /\ P s0 ==> P (SPplus s s0)) /\
     (!s s0. P s /\ P s0 ==> P (SPmult s s0)) ==>
     !s. P s

spolynomial_normalize_ok

|- !sr.
     is_semi_ring sr ==>
     !vm p. interp_cs sr vm (spolynom_normalize sr p) = interp_sp sr vm p

spolynomial_simplify_ok

|- !sr.
     is_semi_ring sr ==>
     !vm p. interp_cs sr vm (spolynom_simplify sr p) = interp_sp sr vm p