Theory "semi_ring"

Signature

Definitions

semi_ring_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'semi_ring'.
            (!a0'.
               (?a0 a1 a2 a3.
                  a0' =
                  (\a0 a1 a2 a3.
                     ind_type$CONSTR 0 (a0,a1,a2,a3) (\n. ind_type$BOTTOM)) a0
                    a1 a2 a3) ==>
               'semi_ring' a0') ==>
            'semi_ring' a0') rep

semi_ring_repfns

|- (!a. mk_semi_ring (dest_semi_ring a) = a) /\
   !r.
     (\a0'.
        !'semi_ring'.
          (!a0'.
             (?a0 a1 a2 a3.
                a0' =
                (\a0 a1 a2 a3.
                   ind_type$CONSTR 0 (a0,a1,a2,a3) (\n. ind_type$BOTTOM)) a0
                  a1 a2 a3) ==>
             'semi_ring' a0') ==>
          'semi_ring' a0') r =
     (dest_semi_ring (mk_semi_ring r) = r)

semi_ring0_def

|- semi_ring0 =
   (\a0 a1 a2 a3.
      mk_semi_ring
        ((\a0 a1 a2 a3. ind_type$CONSTR 0 (a0,a1,a2,a3) (\n. ind_type$BOTTOM))
           a0 a1 a2 a3))

semi_ring

|- semi_ring = semi_ring0

semi_ring_case_def

|- !f a0 a1 a2 a3. semi_ring_case f (semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3

semi_ring_size_def

|- !f a0 a1 a2 a3.
     semi_ring_size f (semi_ring a0 a1 a2 a3) = 1 + (f a0 + f a1)

semi_ring_SR0

|- !a a0 f f0. SR0 (semi_ring a a0 f f0) = a

semi_ring_SR1

|- !a a0 f f0. SR1 (semi_ring a a0 f f0) = a0

semi_ring_SRP

|- !a a0 f f0. SRP (semi_ring a a0 f f0) = f

semi_ring_SRM

|- !a a0 f f0. SRM (semi_ring a a0 f f0) = f0

semi_ring_SR0_fupd

|- !f1 a a0 f f0.
     semi_ring a a0 f f0 with SR0 updated_by f1 = semi_ring (f1 a) a0 f f0

semi_ring_SR1_fupd

|- !f1 a a0 f f0.
     semi_ring a a0 f f0 with SR1 updated_by f1 = semi_ring a (f1 a0) f f0

semi_ring_SRP_fupd

|- !f1 a a0 f f0.
     semi_ring a a0 f f0 with SRP updated_by f1 = semi_ring a a0 (f1 f) f0

semi_ring_SRM_fupd

|- !f1 a a0 f f0.
     semi_ring a a0 f f0 with SRM updated_by f1 = semi_ring a a0 f (f1 f0)

is_semi_ring_def

|- !r.
     is_semi_ring r =
     (!n m. SRP r n m = SRP r m n) /\
     (!n m p. SRP r n (SRP r m p) = SRP r (SRP r n m) p) /\
     (!n m. SRM r n m = SRM r m n) /\
     (!n m p. SRM r n (SRM r m p) = SRM r (SRM r n m) p) /\
     (!n. SRP r (SR0 r) n = n) /\ (!n. SRM r (SR1 r) n = n) /\
     (!n. SRM r (SR0 r) n = SR0 r) /\
     !n m p. SRM r (SRP r n m) p = SRP r (SRM r n p) (SRM r m p)

Theorems

semi_ring_accessors

|- (!a a0 f f0. SR0 (semi_ring a a0 f f0) = a) /\
   (!a a0 f f0. SR1 (semi_ring a a0 f f0) = a0) /\
   (!a a0 f f0. SRP (semi_ring a a0 f f0) = f) /\
   !a a0 f f0. SRM (semi_ring a a0 f f0) = f0

semi_ring_fn_updates

|- (!f1 a a0 f f0.
      semi_ring a a0 f f0 with SR0 updated_by f1 =
      semi_ring (f1 a) a0 f f0) /\
   (!f1 a a0 f f0.
      semi_ring a a0 f f0 with SR1 updated_by f1 =
      semi_ring a (f1 a0) f f0) /\
   (!f1 a a0 f f0.
      semi_ring a a0 f f0 with SRP updated_by f1 =
      semi_ring a a0 (f1 f) f0) /\
   !f1 a a0 f f0.
     semi_ring a a0 f f0 with SRM updated_by f1 = semi_ring a a0 f (f1 f0)

semi_ring_accfupds

|- (!s f. SR0 (s with SR1 updated_by f) = SR0 s) /\
   (!s f. SR0 (s with SRP updated_by f) = SR0 s) /\
   (!s f. SR0 (s with SRM updated_by f) = SR0 s) /\
   (!s f. SR1 (s with SR0 updated_by f) = SR1 s) /\
   (!s f. SR1 (s with SRP updated_by f) = SR1 s) /\
   (!s f. SR1 (s with SRM updated_by f) = SR1 s) /\
   (!s f. SRP (s with SR0 updated_by f) = SRP s) /\
   (!s f. SRP (s with SR1 updated_by f) = SRP s) /\
   (!s f. SRP (s with SRM updated_by f) = SRP s) /\
   (!s f. SRM (s with SR0 updated_by f) = SRM s) /\
   (!s f. SRM (s with SR1 updated_by f) = SRM s) /\
   (!s f. SRM (s with SRP updated_by f) = SRM s) /\
   (!s f. SR0 (s with SR0 updated_by f) = f (SR0 s)) /\
   (!s f. SR1 (s with SR1 updated_by f) = f (SR1 s)) /\
   (!s f. SRP (s with SRP updated_by f) = f (SRP s)) /\
   !s f. SRM (s with SRM updated_by f) = f (SRM s)

semi_ring_fupdfupds

|- (!s g f.
      s with <|SR0 updated_by f; SR0 updated_by g|> =
      s with SR0 updated_by f o g) /\
   (!s g f.
      s with <|SR1 updated_by f; SR1 updated_by g|> =
      s with SR1 updated_by f o g) /\
   (!s g f.
      s with <|SRP updated_by f; SRP updated_by g|> =
      s with SRP updated_by f o g) /\
   !s g f.
     s with <|SRM updated_by f; SRM updated_by g|> =
     s with SRM updated_by f o g

semi_ring_fupdfupds_comp

|- ((!g f.
       semi_ring_SR0_fupd f o semi_ring_SR0_fupd g =
       semi_ring_SR0_fupd (f o g)) /\
    !h g f.
      semi_ring_SR0_fupd f o semi_ring_SR0_fupd g o h =
      semi_ring_SR0_fupd (f o g) o h) /\
   ((!g f.
       semi_ring_SR1_fupd f o semi_ring_SR1_fupd g =
       semi_ring_SR1_fupd (f o g)) /\
    !h g f.
      semi_ring_SR1_fupd f o semi_ring_SR1_fupd g o h =
      semi_ring_SR1_fupd (f o g) o h) /\
   ((!g f.
       semi_ring_SRP_fupd f o semi_ring_SRP_fupd g =
       semi_ring_SRP_fupd (f o g)) /\
    !h g f.
      semi_ring_SRP_fupd f o semi_ring_SRP_fupd g o h =
      semi_ring_SRP_fupd (f o g) o h) /\
   (!g f.
      semi_ring_SRM_fupd f o semi_ring_SRM_fupd g =
      semi_ring_SRM_fupd (f o g)) /\
   !h g f.
     semi_ring_SRM_fupd f o semi_ring_SRM_fupd g o h =
     semi_ring_SRM_fupd (f o g) o h

semi_ring_fupdcanon

|- (!s g f.
      s with <|SR1 updated_by f; SR0 updated_by g|> =
      s with <|SR0 updated_by g; SR1 updated_by f|>) /\
   (!s g f.
      s with <|SRP updated_by f; SR0 updated_by g|> =
      s with <|SR0 updated_by g; SRP updated_by f|>) /\
   (!s g f.
      s with <|SRP updated_by f; SR1 updated_by g|> =
      s with <|SR1 updated_by g; SRP updated_by f|>) /\
   (!s g f.
      s with <|SRM updated_by f; SR0 updated_by g|> =
      s with <|SR0 updated_by g; SRM updated_by f|>) /\
   (!s g f.
      s with <|SRM updated_by f; SR1 updated_by g|> =
      s with <|SR1 updated_by g; SRM updated_by f|>) /\
   !s g f.
     s with <|SRM updated_by f; SRP updated_by g|> =
     s with <|SRP updated_by g; SRM updated_by f|>

semi_ring_fupdcanon_comp

|- ((!g f.
       semi_ring_SR1_fupd f o semi_ring_SR0_fupd g =
       semi_ring_SR0_fupd g o semi_ring_SR1_fupd f) /\
    !h g f.
      semi_ring_SR1_fupd f o semi_ring_SR0_fupd g o h =
      semi_ring_SR0_fupd g o semi_ring_SR1_fupd f o h) /\
   ((!g f.
       semi_ring_SRP_fupd f o semi_ring_SR0_fupd g =
       semi_ring_SR0_fupd g o semi_ring_SRP_fupd f) /\
    !h g f.
      semi_ring_SRP_fupd f o semi_ring_SR0_fupd g o h =
      semi_ring_SR0_fupd g o semi_ring_SRP_fupd f o h) /\
   ((!g f.
       semi_ring_SRP_fupd f o semi_ring_SR1_fupd g =
       semi_ring_SR1_fupd g o semi_ring_SRP_fupd f) /\
    !h g f.
      semi_ring_SRP_fupd f o semi_ring_SR1_fupd g o h =
      semi_ring_SR1_fupd g o semi_ring_SRP_fupd f o h) /\
   ((!g f.
       semi_ring_SRM_fupd f o semi_ring_SR0_fupd g =
       semi_ring_SR0_fupd g o semi_ring_SRM_fupd f) /\
    !h g f.
      semi_ring_SRM_fupd f o semi_ring_SR0_fupd g o h =
      semi_ring_SR0_fupd g o semi_ring_SRM_fupd f o h) /\
   ((!g f.
       semi_ring_SRM_fupd f o semi_ring_SR1_fupd g =
       semi_ring_SR1_fupd g o semi_ring_SRM_fupd f) /\
    !h g f.
      semi_ring_SRM_fupd f o semi_ring_SR1_fupd g o h =
      semi_ring_SR1_fupd g o semi_ring_SRM_fupd f o h) /\
   (!g f.
      semi_ring_SRM_fupd f o semi_ring_SRP_fupd g =
      semi_ring_SRP_fupd g o semi_ring_SRM_fupd f) /\
   !h g f.
     semi_ring_SRM_fupd f o semi_ring_SRP_fupd g o h =
     semi_ring_SRP_fupd g o semi_ring_SRM_fupd f o h

semi_ring_component_equality

|- !s1 s2.
     (s1 = s2) =
     (SR0 s1 = SR0 s2) /\ (SR1 s1 = SR1 s2) /\ (SRP s1 = SRP s2) /\
     (SRM s1 = SRM s2)

semi_ring_updates_eq_literal

|- !s a0 a f0 f.
     s with <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|> =
     <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>

semi_ring_literal_nchotomy

|- !s. ?a0 a f0 f. s = <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>

FORALL_semi_ring

|- !P. (!s. P s) = !a0 a f0 f. P <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>

EXISTS_semi_ring

|- !P. (?s. P s) = ?a0 a f0 f. P <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>

semi_ring_literal_11

|- !a01 a1 f01 f1 a02 a2 f02 f2.
     (<|SR0 := a01; SR1 := a1; SRP := f01; SRM := f1|> =
      <|SR0 := a02; SR1 := a2; SRP := f02; SRM := f2|>) =
     (a01 = a02) /\ (a1 = a2) /\ (f01 = f02) /\ (f1 = f2)

datatype_semi_ring

|- DATATYPE (record semi_ring SR0 SR1 SRP SRM)

semi_ring_11

|- !a0 a1 a2 a3 a0' a1' a2' a3'.
     (semi_ring a0 a1 a2 a3 = semi_ring a0' a1' a2' a3') =
     (a0 = a0') /\ (a1 = a1') /\ (a2 = a2') /\ (a3 = a3')

semi_ring_case_cong

|- !M M' f.
     (M = M') /\
     (!a0 a1 a2 a3.
        (M' = semi_ring a0 a1 a2 a3) ==> (f a0 a1 a2 a3 = f' a0 a1 a2 a3)) ==>
     (semi_ring_case f M = semi_ring_case f' M')

semi_ring_nchotomy

|- !s. ?a a0 f f0. s = semi_ring a a0 f f0

semi_ring_Axiom

|- !f. ?fn. !a0 a1 a2 a3. fn (semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3

semi_ring_induction

|- !P. (!a a0 f f0. P (semi_ring a a0 f f0)) ==> !s. P s

plus_sym

|- !r. is_semi_ring r ==> !n m. SRP r n m = SRP r m n

plus_assoc

|- !r. is_semi_ring r ==> !n m p. SRP r n (SRP r m p) = SRP r (SRP r n m) p

mult_sym

|- !r. is_semi_ring r ==> !n m. SRM r n m = SRM r m n

mult_assoc

|- !r. is_semi_ring r ==> !n m p. SRM r n (SRM r m p) = SRM r (SRM r n m) p

plus_zero_left

|- !r. is_semi_ring r ==> !n. SRP r (SR0 r) n = n

mult_one_left

|- !r. is_semi_ring r ==> !n. SRM r (SR1 r) n = n

mult_zero_left

|- !r. is_semi_ring r ==> !n. SRM r (SR0 r) n = SR0 r

distr_left

|- !r.
     is_semi_ring r ==>
     !n m p. SRM r (SRP r n m) p = SRP r (SRM r n p) (SRM r m p)

plus_zero_right

|- !r. is_semi_ring r ==> !n. SRP r n (SR0 r) = n

mult_one_right

|- !r. is_semi_ring r ==> !n. SRM r n (SR1 r) = n

mult_zero_right

|- !r. is_semi_ring r ==> !n. SRM r n (SR0 r) = SR0 r

distr_right

|- !r.
     is_semi_ring r ==>
     !m n p. SRM r m (SRP r n p) = SRP r (SRM r m n) (SRM r m p)

plus_rotate

|- !r. is_semi_ring r ==> !m n p. SRP r (SRP r m n) p = SRP r (SRP r n p) m

plus_permute

|- !r. is_semi_ring r ==> !m n p. SRP r (SRP r m n) p = SRP r (SRP r m p) n

mult_rotate

|- !r. is_semi_ring r ==> !m n p. SRM r (SRM r m n) p = SRM r (SRM r n p) m

mult_permute

|- !r. is_semi_ring r ==> !m n p. SRM r (SRM r m n) p = SRM r (SRM r m p) n