Theory "semi_ring"

Signature

Type	Arity
semi_ring	1
Constant	Type
is_semi_ring	:α semi_ring -> bool
recordtype.semi_ring	:α -> α -> (α -> α -> α) -> (α -> α -> α) -> α semi_ring
semi_ring_CASE	:α semi_ring -> (α -> α -> (α -> α -> α) -> (α -> α -> α) -> β) -> β
semi_ring_SR0	:α semi_ring -> α
semi_ring_SR0_fupd	:(α -> α) -> α semi_ring -> α semi_ring
semi_ring_SR1	:α semi_ring -> α
semi_ring_SR1_fupd	:(α -> α) -> α semi_ring -> α semi_ring
semi_ring_SRM	:α semi_ring -> α -> α -> α
semi_ring_SRM_fupd	:((α -> α -> α) -> α -> α -> α) -> α semi_ring -> α semi_ring
semi_ring_SRP	:α semi_ring -> α -> α -> α
semi_ring_SRP_fupd	:((α -> α -> α) -> α -> α -> α) -> α semi_ring -> α semi_ring
semi_ring_size	:(α -> num) -> α semi_ring -> num

Definitions

semi_ring_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀ $var$('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) ⇒
                      $var$('semi_ring') a0') ⇒
                 $var$('semi_ring') a0') rep

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_SRP

⊢ ∀a a0 f f0. (semi_ring a a0 f f0).SRP = f

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)

semi_ring_SRM

⊢ ∀a a0 f f0. (semi_ring a a0 f f0).SRM = 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_SR1

⊢ ∀a a0 f f0. (semi_ring a a0 f f0).SR1 = a0

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_SR0

⊢ ∀a a0 f f0. (semi_ring a a0 f f0).SR0 = a

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_case_def

⊢ ∀a0 a1 a2 a3 f. semi_ring_CASE (semi_ring a0 a1 a2 a3) f = f a0 a1 a2 a3

is_semi_ring_def

⊢ ∀r.
      is_semi_ring r ⇔
      (∀n m. r.SRP n m = r.SRP m n) ∧
      (∀n m p. r.SRP n (r.SRP m p) = r.SRP (r.SRP n m) p) ∧
      (∀n m. r.SRM n m = r.SRM m n) ∧
      (∀n m p. r.SRM n (r.SRM m p) = r.SRM (r.SRM n m) p) ∧
      (∀n. r.SRP r.SR0 n = n) ∧ (∀n. r.SRM r.SR1 n = n) ∧
      (∀n. r.SRM r.SR0 n = r.SR0) ∧
      ∀n m p. r.SRM (r.SRP n m) p = r.SRP (r.SRM n p) (r.SRM m p)

Theorems

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_nchotomy

⊢ ∀ss. ∃a a0 f f0. ss = semi_ring a a0 f f0

semi_ring_literal_nchotomy

⊢ ∀s. ∃a0 a f0 f. s = <|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)

semi_ring_induction

⊢ ∀P. (∀a a0 f f0. P (semi_ring a a0 f f0)) ⇒ ∀s. P s

semi_ring_fupdfupds_comp

⊢ ((∀g f. SR0_fupd f ∘ SR0_fupd g = SR0_fupd (f ∘ g)) ∧
   ∀h g f. SR0_fupd f ∘ SR0_fupd g ∘ h = SR0_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. SR1_fupd f ∘ SR1_fupd g = SR1_fupd (f ∘ g)) ∧
   ∀h g f. SR1_fupd f ∘ SR1_fupd g ∘ h = SR1_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. SRP_fupd f ∘ SRP_fupd g = SRP_fupd (f ∘ g)) ∧
   ∀h g f. SRP_fupd f ∘ SRP_fupd g ∘ h = SRP_fupd (f ∘ g) ∘ h) ∧
  (∀g f. SRM_fupd f ∘ SRM_fupd g = SRM_fupd (f ∘ g)) ∧
  ∀h g f. SRM_fupd f ∘ SRM_fupd g ∘ h = SRM_fupd (f ∘ g) ∘ h

semi_ring_fupdfupds

⊢ (∀s g f.
       s with <|SR0 updated_by f; SR0 updated_by g|> =
       s with SR0 updated_by f ∘ g) ∧
  (∀s g f.
       s with <|SR1 updated_by f; SR1 updated_by g|> =
       s with SR1 updated_by f ∘ g) ∧
  (∀s g f.
       s with <|SRP updated_by f; SRP updated_by g|> =
       s with SRP updated_by f ∘ g) ∧
  ∀s g f.
      s with <|SRM updated_by f; SRM updated_by g|> =
      s with SRM updated_by f ∘ g

semi_ring_fupdcanon_comp

⊢ ((∀g f. SR1_fupd f ∘ SR0_fupd g = SR0_fupd g ∘ SR1_fupd f) ∧
   ∀h g f. SR1_fupd f ∘ SR0_fupd g ∘ h = SR0_fupd g ∘ SR1_fupd f ∘ h) ∧
  ((∀g f. SRP_fupd f ∘ SR0_fupd g = SR0_fupd g ∘ SRP_fupd f) ∧
   ∀h g f. SRP_fupd f ∘ SR0_fupd g ∘ h = SR0_fupd g ∘ SRP_fupd f ∘ h) ∧
  ((∀g f. SRP_fupd f ∘ SR1_fupd g = SR1_fupd g ∘ SRP_fupd f) ∧
   ∀h g f. SRP_fupd f ∘ SR1_fupd g ∘ h = SR1_fupd g ∘ SRP_fupd f ∘ h) ∧
  ((∀g f. SRM_fupd f ∘ SR0_fupd g = SR0_fupd g ∘ SRM_fupd f) ∧
   ∀h g f. SRM_fupd f ∘ SR0_fupd g ∘ h = SR0_fupd g ∘ SRM_fupd f ∘ h) ∧
  ((∀g f. SRM_fupd f ∘ SR1_fupd g = SR1_fupd g ∘ SRM_fupd f) ∧
   ∀h g f. SRM_fupd f ∘ SR1_fupd g ∘ h = SR1_fupd g ∘ SRM_fupd f ∘ h) ∧
  (∀g f. SRM_fupd f ∘ SRP_fupd g = SRP_fupd g ∘ SRM_fupd f) ∧
  ∀h g f. SRM_fupd f ∘ SRP_fupd g ∘ h = SRP_fupd g ∘ SRM_fupd f ∘ 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_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_component_equality

⊢ ∀s1 s2.
      (s1 = s2) ⇔
      (s1.SR0 = s2.SR0) ∧ (s1.SR1 = s2.SR1) ∧ (s1.SRP = s2.SRP) ∧
      (s1.SRM = s2.SRM)

semi_ring_case_eq

⊢ (semi_ring_CASE x f = v) ⇔
  ∃a a0 f' f0. (x = semi_ring a a0 f' f0) ∧ (f a a0 f' f0 = v)

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 M f = semi_ring_CASE M' f')

semi_ring_Axiom

⊢ ∀f. ∃fn. ∀a0 a1 a2 a3. fn (semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3

semi_ring_accfupds

⊢ (∀s f. (s with SR1 updated_by f).SR0 = s.SR0) ∧
  (∀s f. (s with SRP updated_by f).SR0 = s.SR0) ∧
  (∀s f. (s with SRM updated_by f).SR0 = s.SR0) ∧
  (∀s f. (s with SR0 updated_by f).SR1 = s.SR1) ∧
  (∀s f. (s with SRP updated_by f).SR1 = s.SR1) ∧
  (∀s f. (s with SRM updated_by f).SR1 = s.SR1) ∧
  (∀s f. (s with SR0 updated_by f).SRP = s.SRP) ∧
  (∀s f. (s with SR1 updated_by f).SRP = s.SRP) ∧
  (∀s f. (s with SRM updated_by f).SRP = s.SRP) ∧
  (∀s f. (s with SR0 updated_by f).SRM = s.SRM) ∧
  (∀s f. (s with SR1 updated_by f).SRM = s.SRM) ∧
  (∀s f. (s with SRP updated_by f).SRM = s.SRM) ∧
  (∀s f. (s with SR0 updated_by f).SR0 = f s.SR0) ∧
  (∀s f. (s with SR1 updated_by f).SR1 = f s.SR1) ∧
  (∀s f. (s with SRP updated_by f).SRP = f s.SRP) ∧
  ∀s f. (s with SRM updated_by f).SRM = f s.SRM

semi_ring_accessors

⊢ (∀a a0 f f0. (semi_ring a a0 f f0).SR0 = a) ∧
  (∀a a0 f f0. (semi_ring a a0 f f0).SR1 = a0) ∧
  (∀a a0 f f0. (semi_ring a a0 f f0).SRP = f) ∧
  ∀a a0 f f0. (semi_ring a a0 f f0).SRM = f0

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

plus_zero_right

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRP n r.SR0 = n

plus_zero_left

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRP r.SR0 n = n

plus_sym

⊢ ∀r. is_semi_ring r ⇒ ∀n m. r.SRP n m = r.SRP m n

plus_rotate

⊢ ∀r. is_semi_ring r ⇒ ∀m n p. r.SRP (r.SRP m n) p = r.SRP (r.SRP n p) m

plus_permute

⊢ ∀r. is_semi_ring r ⇒ ∀m n p. r.SRP (r.SRP m n) p = r.SRP (r.SRP m p) n

plus_assoc

⊢ ∀r. is_semi_ring r ⇒ ∀n m p. r.SRP n (r.SRP m p) = r.SRP (r.SRP n m) p

mult_zero_right

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRM n r.SR0 = r.SR0

mult_zero_left

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRM r.SR0 n = r.SR0

mult_sym

⊢ ∀r. is_semi_ring r ⇒ ∀n m. r.SRM n m = r.SRM m n

mult_rotate

⊢ ∀r. is_semi_ring r ⇒ ∀m n p. r.SRM (r.SRM m n) p = r.SRM (r.SRM n p) m

mult_permute

⊢ ∀r. is_semi_ring r ⇒ ∀m n p. r.SRM (r.SRM m n) p = r.SRM (r.SRM m p) n

mult_one_right

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRM n r.SR1 = n

mult_one_left

⊢ ∀r. is_semi_ring r ⇒ ∀n. r.SRM r.SR1 n = n

mult_assoc

⊢ ∀r. is_semi_ring r ⇒ ∀n m p. r.SRM n (r.SRM m p) = r.SRM (r.SRM n m) p

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

distr_right

⊢ ∀r.
      is_semi_ring r ⇒
      ∀m n p. r.SRM m (r.SRP n p) = r.SRP (r.SRM m n) (r.SRM m p)

distr_left

⊢ ∀r.
      is_semi_ring r ⇒
      ∀n m p. r.SRM (r.SRP n m) p = r.SRP (r.SRM n p) (r.SRM m p)

datatype_semi_ring

⊢ DATATYPE (record semi_ring SR0 SR1 SRP SRM)