Theory: EVAL_semiring

Type operators

semi_ring : α semi_ring

Constants

is_semi_ring : α semi_ring -> bool
recordtype.semi_ring : α -> α -> (α -> α -> α) -> (α -> α -> α) -> α semi_ring
recordtype.semi_ring.seldef.SR0 : α semi_ring -> α
recordtype.semi_ring.seldef.SR0_fupd : (α -> α) -> α semi_ring -> α semi_ring
recordtype.semi_ring.seldef.SR1 : α semi_ring -> α
recordtype.semi_ring.seldef.SR1_fupd : (α -> α) -> α semi_ring -> α semi_ring
recordtype.semi_ring.seldef.SRM : α semi_ring -> α -> α -> α
recordtype.semi_ring.seldef.SRM_fupd : ((α -> α -> α) -> α -> α -> α) -> α semi_ring -> α semi_ring
recordtype.semi_ring.seldef.SRP : α semi_ring -> α -> α -> α
recordtype.semi_ring.seldef.SRP_fupd : ((α -> α -> α) -> α -> α -> α) -> α semi_ring -> α semi_ring
semi_ring_ABS : 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1) -> 'b1 semi_ring
semi_ring_CASE : α semi_ring -> (α -> α -> (α -> α -> α) -> (α -> α -> α) -> β) -> β
semi_ring_CONS : 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1) -> 'b1 semi_ring
semi_ring_REP : 'b1 semi_ring -> 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1)
semi_ring_size : (α -> num) -> α semi_ring -> num

Definitions

is_semi_ring_def recordtype_semi_ring_seldef_SR0_def recordtype_semi_ring_seldef_SR0_fupd_def recordtype_semi_ring_seldef_SR1_def recordtype_semi_ring_seldef_SR1_fupd_def recordtype_semi_ring_seldef_SRM_def recordtype_semi_ring_seldef_SRM_fupd_def recordtype_semi_ring_seldef_SRP_def recordtype_semi_ring_seldef_SRP_fupd_def semi_ring_ABSREP semi_ring_CONS_def semi_ring_TY_DEF semi_ring_case_def semi_ring_size_def

Theorems

Definitions

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)

recordtype_semi_ring_seldef_SR0_def

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

recordtype_semi_ring_seldef_SR0_fupd_def

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

recordtype_semi_ring_seldef_SR1_def

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

recordtype_semi_ring_seldef_SR1_fupd_def

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

recordtype_semi_ring_seldef_SRM_def

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

recordtype_semi_ring_seldef_SRM_fupd_def

⊢ ∀f1 a a0 f f0.
    semi_ring a a0 f f0 with SRM updated_by f1 = semi_ring a a0 f (f1 f0)

recordtype_semi_ring_seldef_SRP_def

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

recordtype_semi_ring_seldef_SRP_fupd_def

⊢ ∀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_ABSREP

⊢ (∀a. semi_ring_ABS (semi_ring_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ (semi_ring_REP (semi_ring_ABS r) = r)

semi_ring_CONS_def

⊢ semi_ring_CONS = semi_ring_ABS

semi_ring_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λx. T) rep

semi_ring_case_def

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

semi_ring_size_def

⊢ ∀f0 a0 a1 a2 a3.
    semi_ring_size f0 (semi_ring a0 a1 a2 a3) = 1 + (f0 a0 + f0 a1)

Theorems

EXISTS_semi_ring

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

datatype_semi_ring

⊢ DATATYPE (record semi_ring SR0 SR1 SRP SRM)

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)

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)

mult_assoc

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

mult_one_left

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

mult_one_right

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

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_rotate

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

mult_sym

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

mult_zero_left

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

mult_zero_right

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

plus_assoc

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

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_rotate

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

plus_sym

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

plus_zero_left

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

plus_zero_right

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

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_Axiom

⊢ ∀f0. ∃h. ∀a0 a1 a2 a3. h (semi_ring a0 a1 a2 a3) = f0 a0 a1 a2 a3

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

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

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_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. 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_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_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_fupdselfid

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

semi_ring_induction

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

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_literal_nchotomy

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

Theory EVAL_semiring

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems