Theory "ring"

Parents semi_ring

Signature

Type	Arity
ring	1
Constant	Type
is_ring	:α ring -> bool
ring	:α -> α -> (α -> α -> α) -> (α -> α -> α) -> (α -> α) -> α ring
ring_CASE	:α ring -> (α -> α -> (α -> α -> α) -> (α -> α -> α) -> (α -> α) -> β) -> β
ring_R0	:α ring -> α
ring_R0_fupd	:(α -> α) -> α ring -> α ring
ring_R1	:α ring -> α
ring_R1_fupd	:(α -> α) -> α ring -> α ring
ring_RM	:α ring -> α -> α -> α
ring_RM_fupd	:((α -> α -> α) -> α -> α -> α) -> α ring -> α ring
ring_RN	:α ring -> α -> α
ring_RN_fupd	:((α -> α) -> α -> α) -> α ring -> α ring
ring_RP	:α ring -> α -> α -> α
ring_RP_fupd	:((α -> α -> α) -> α -> α -> α) -> α ring -> α ring
ring_size	:(α -> num) -> α ring -> num
semi_ring_of	:α ring -> α semi_ring

Definitions

ring_TY_DEF

|- ∃rep.
     TYPE_DEFINITION
       (λa0'.
          ∀'ring' .
            (∀a0'.
               (∃a0 a1 a2 a3 a4.
                  a0' =
                  (λa0 a1 a2 a3 a4.
                     ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (λn. ind_type$BOTTOM))
                    a0 a1 a2 a3 a4) ⇒
               'ring' a0') ⇒
            'ring' a0') rep

ring_case_def

|- ∀a0 a1 a2 a3 a4 f. ring_CASE (ring a0 a1 a2 a3 a4) f = f a0 a1 a2 a3 a4

ring_size_def

|- ∀f a0 a1 a2 a3 a4. ring_size f (ring a0 a1 a2 a3 a4) = 1 + (f a0 + f a1)

ring_R0

|- ∀a a0 f f0 f1. R0 (ring a a0 f f0 f1) = a

ring_R1

|- ∀a a0 f f0 f1. R1 (ring a a0 f f0 f1) = a0

ring_RP

|- ∀a a0 f f0 f1. RP (ring a a0 f f0 f1) = f

ring_RM

|- ∀a a0 f f0 f1. RM (ring a a0 f f0 f1) = f0

ring_RN

|- ∀a a0 f f0 f1. RN (ring a a0 f f0 f1) = f1

ring_R0_fupd

|- ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with R0 updated_by f2 = ring (f2 a) a0 f f0 f1

ring_R1_fupd

|- ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with R1 updated_by f2 = ring a (f2 a0) f f0 f1

ring_RP_fupd

|- ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with RP updated_by f2 = ring a a0 (f2 f) f0 f1

ring_RM_fupd

|- ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with RM updated_by f2 = ring a a0 f (f2 f0) f1

ring_RN_fupd

|- ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with RN updated_by f2 = ring a a0 f f0 (f2 f1)

is_ring_def

|- ∀r.
     is_ring r ⇔
     (∀n m. RP r n m = RP r m n) ∧
     (∀n m p. RP r n (RP r m p) = RP r (RP r n m) p) ∧
     (∀n m. RM r n m = RM r m n) ∧
     (∀n m p. RM r n (RM r m p) = RM r (RM r n m) p) ∧
     (∀n. RP r (R0 r) n = n) ∧ (∀n. RM r (R1 r) n = n) ∧
     (∀n. RP r n (RN r n) = R0 r) ∧
     ∀n m p. RM r (RP r n m) p = RP r (RM r n p) (RM r m p)

semi_ring_of_def

|- ∀r. semi_ring_of r = semi_ring (R0 r) (R1 r) (RP r) (RM r)

Theorems

ring_accessors

|- (∀a a0 f f0 f1. R0 (ring a a0 f f0 f1) = a) ∧
   (∀a a0 f f0 f1. R1 (ring a a0 f f0 f1) = a0) ∧
   (∀a a0 f f0 f1. RP (ring a a0 f f0 f1) = f) ∧
   (∀a a0 f f0 f1. RM (ring a a0 f f0 f1) = f0) ∧
   ∀a a0 f f0 f1. RN (ring a a0 f f0 f1) = f1

ring_fn_updates

|- (∀f2 a a0 f f0 f1.
      ring a a0 f f0 f1 with R0 updated_by f2 = ring (f2 a) a0 f f0 f1) ∧
   (∀f2 a a0 f f0 f1.
      ring a a0 f f0 f1 with R1 updated_by f2 = ring a (f2 a0) f f0 f1) ∧
   (∀f2 a a0 f f0 f1.
      ring a a0 f f0 f1 with RP updated_by f2 = ring a a0 (f2 f) f0 f1) ∧
   (∀f2 a a0 f f0 f1.
      ring a a0 f f0 f1 with RM updated_by f2 = ring a a0 f (f2 f0) f1) ∧
   ∀f2 a a0 f f0 f1.
     ring a a0 f f0 f1 with RN updated_by f2 = ring a a0 f f0 (f2 f1)

ring_accfupds

|- (∀r f. R0 (r with R1 updated_by f) = R0 r) ∧
   (∀r f. R0 (r with RP updated_by f) = R0 r) ∧
   (∀r f. R0 (r with RM updated_by f) = R0 r) ∧
   (∀r f. R0 (r with RN updated_by f) = R0 r) ∧
   (∀r f. R1 (r with R0 updated_by f) = R1 r) ∧
   (∀r f. R1 (r with RP updated_by f) = R1 r) ∧
   (∀r f. R1 (r with RM updated_by f) = R1 r) ∧
   (∀r f. R1 (r with RN updated_by f) = R1 r) ∧
   (∀r f. RP (r with R0 updated_by f) = RP r) ∧
   (∀r f. RP (r with R1 updated_by f) = RP r) ∧
   (∀r f. RP (r with RM updated_by f) = RP r) ∧
   (∀r f. RP (r with RN updated_by f) = RP r) ∧
   (∀r f. RM (r with R0 updated_by f) = RM r) ∧
   (∀r f. RM (r with R1 updated_by f) = RM r) ∧
   (∀r f. RM (r with RP updated_by f) = RM r) ∧
   (∀r f. RM (r with RN updated_by f) = RM r) ∧
   (∀r f. RN (r with R0 updated_by f) = RN r) ∧
   (∀r f. RN (r with R1 updated_by f) = RN r) ∧
   (∀r f. RN (r with RP updated_by f) = RN r) ∧
   (∀r f. RN (r with RM updated_by f) = RN r) ∧
   (∀r f. R0 (r with R0 updated_by f) = f (R0 r)) ∧
   (∀r f. R1 (r with R1 updated_by f) = f (R1 r)) ∧
   (∀r f. RP (r with RP updated_by f) = f (RP r)) ∧
   (∀r f. RM (r with RM updated_by f) = f (RM r)) ∧
   ∀r f. RN (r with RN updated_by f) = f (RN r)

ring_fupdfupds

|- (∀r g f.
      r with <|R0 updated_by f; R0 updated_by g|> =
      r with R0 updated_by f o g) ∧
   (∀r g f.
      r with <|R1 updated_by f; R1 updated_by g|> =
      r with R1 updated_by f o g) ∧
   (∀r g f.
      r with <|RP updated_by f; RP updated_by g|> =
      r with RP updated_by f o g) ∧
   (∀r g f.
      r with <|RM updated_by f; RM updated_by g|> =
      r with RM updated_by f o g) ∧
   ∀r g f.
     r with <|RN updated_by f; RN updated_by g|> = r with RN updated_by f o g

ring_fupdfupds_comp

|- ((∀g f.
        _ record fupdateR0 f o  _ record fupdateR0 g =
        _ record fupdateR0 (f o g)) ∧
    ∀h g f.
       _ record fupdateR0 f o  _ record fupdateR0 g o h =
       _ record fupdateR0 (f o g) o h) ∧
   ((∀g f.
        _ record fupdateR1 f o  _ record fupdateR1 g =
        _ record fupdateR1 (f o g)) ∧
    ∀h g f.
       _ record fupdateR1 f o  _ record fupdateR1 g o h =
       _ record fupdateR1 (f o g) o h) ∧
   ((∀g f.
        _ record fupdateRP f o  _ record fupdateRP g =
        _ record fupdateRP (f o g)) ∧
    ∀h g f.
       _ record fupdateRP f o  _ record fupdateRP g o h =
       _ record fupdateRP (f o g) o h) ∧
   ((∀g f.
        _ record fupdateRM f o  _ record fupdateRM g =
        _ record fupdateRM (f o g)) ∧
    ∀h g f.
       _ record fupdateRM f o  _ record fupdateRM g o h =
       _ record fupdateRM (f o g) o h) ∧
   (∀g f.
       _ record fupdateRN f o  _ record fupdateRN g =
       _ record fupdateRN (f o g)) ∧
   ∀h g f.
      _ record fupdateRN f o  _ record fupdateRN g o h =
      _ record fupdateRN (f o g) o h

ring_fupdcanon

|- (∀r g f.
      r with <|R1 updated_by f; R0 updated_by g|> =
      r with <|R0 updated_by g; R1 updated_by f|>) ∧
   (∀r g f.
      r with <|RP updated_by f; R0 updated_by g|> =
      r with <|R0 updated_by g; RP updated_by f|>) ∧
   (∀r g f.
      r with <|RP updated_by f; R1 updated_by g|> =
      r with <|R1 updated_by g; RP updated_by f|>) ∧
   (∀r g f.
      r with <|RM updated_by f; R0 updated_by g|> =
      r with <|R0 updated_by g; RM updated_by f|>) ∧
   (∀r g f.
      r with <|RM updated_by f; R1 updated_by g|> =
      r with <|R1 updated_by g; RM updated_by f|>) ∧
   (∀r g f.
      r with <|RM updated_by f; RP updated_by g|> =
      r with <|RP updated_by g; RM updated_by f|>) ∧
   (∀r g f.
      r with <|RN updated_by f; R0 updated_by g|> =
      r with <|R0 updated_by g; RN updated_by f|>) ∧
   (∀r g f.
      r with <|RN updated_by f; R1 updated_by g|> =
      r with <|R1 updated_by g; RN updated_by f|>) ∧
   (∀r g f.
      r with <|RN updated_by f; RP updated_by g|> =
      r with <|RP updated_by g; RN updated_by f|>) ∧
   ∀r g f.
     r with <|RN updated_by f; RM updated_by g|> =
     r with <|RM updated_by g; RN updated_by f|>

ring_fupdcanon_comp

|- ((∀g f.
        _ record fupdateR1 f o  _ record fupdateR0 g =
        _ record fupdateR0 g o  _ record fupdateR1 f) ∧
    ∀h g f.
       _ record fupdateR1 f o  _ record fupdateR0 g o h =
       _ record fupdateR0 g o  _ record fupdateR1 f o h) ∧
   ((∀g f.
        _ record fupdateRP f o  _ record fupdateR0 g =
        _ record fupdateR0 g o  _ record fupdateRP f) ∧
    ∀h g f.
       _ record fupdateRP f o  _ record fupdateR0 g o h =
       _ record fupdateR0 g o  _ record fupdateRP f o h) ∧
   ((∀g f.
        _ record fupdateRP f o  _ record fupdateR1 g =
        _ record fupdateR1 g o  _ record fupdateRP f) ∧
    ∀h g f.
       _ record fupdateRP f o  _ record fupdateR1 g o h =
       _ record fupdateR1 g o  _ record fupdateRP f o h) ∧
   ((∀g f.
        _ record fupdateRM f o  _ record fupdateR0 g =
        _ record fupdateR0 g o  _ record fupdateRM f) ∧
    ∀h g f.
       _ record fupdateRM f o  _ record fupdateR0 g o h =
       _ record fupdateR0 g o  _ record fupdateRM f o h) ∧
   ((∀g f.
        _ record fupdateRM f o  _ record fupdateR1 g =
        _ record fupdateR1 g o  _ record fupdateRM f) ∧
    ∀h g f.
       _ record fupdateRM f o  _ record fupdateR1 g o h =
       _ record fupdateR1 g o  _ record fupdateRM f o h) ∧
   ((∀g f.
        _ record fupdateRM f o  _ record fupdateRP g =
        _ record fupdateRP g o  _ record fupdateRM f) ∧
    ∀h g f.
       _ record fupdateRM f o  _ record fupdateRP g o h =
       _ record fupdateRP g o  _ record fupdateRM f o h) ∧
   ((∀g f.
        _ record fupdateRN f o  _ record fupdateR0 g =
        _ record fupdateR0 g o  _ record fupdateRN f) ∧
    ∀h g f.
       _ record fupdateRN f o  _ record fupdateR0 g o h =
       _ record fupdateR0 g o  _ record fupdateRN f o h) ∧
   ((∀g f.
        _ record fupdateRN f o  _ record fupdateR1 g =
        _ record fupdateR1 g o  _ record fupdateRN f) ∧
    ∀h g f.
       _ record fupdateRN f o  _ record fupdateR1 g o h =
       _ record fupdateR1 g o  _ record fupdateRN f o h) ∧
   ((∀g f.
        _ record fupdateRN f o  _ record fupdateRP g =
        _ record fupdateRP g o  _ record fupdateRN f) ∧
    ∀h g f.
       _ record fupdateRN f o  _ record fupdateRP g o h =
       _ record fupdateRP g o  _ record fupdateRN f o h) ∧
   (∀g f.
       _ record fupdateRN f o  _ record fupdateRM g =
       _ record fupdateRM g o  _ record fupdateRN f) ∧
   ∀h g f.
      _ record fupdateRN f o  _ record fupdateRM g o h =
      _ record fupdateRM g o  _ record fupdateRN f o h

ring_component_equality

|- ∀r1 r2.
     (r1 = r2) ⇔
     (R0 r1 = R0 r2) ∧ (R1 r1 = R1 r2) ∧ (RP r1 = RP r2) ∧ (RM r1 = RM r2) ∧
     (RN r1 = RN r2)

ring_updates_eq_literal

|- ∀r a0 a f1 f0 f.
     r with <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|> =
     <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>

ring_literal_nchotomy

|- ∀r. ∃a0 a f1 f0 f. r = <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>

FORALL_ring

|- ∀P.
     (∀r. P r) ⇔
     ∀a0 a f1 f0 f. P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>

EXISTS_ring

|- ∀P.
     (∃r. P r) ⇔
     ∃a0 a f1 f0 f. P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>

ring_literal_11

|- ∀a01 a1 f11 f01 f1 a02 a2 f12 f02 f2.
     (<|R0 := a01; R1 := a1; RP := f11; RM := f01; RN := f1|> =
      <|R0 := a02; R1 := a2; RP := f12; RM := f02; RN := f2|>) ⇔
     (a01 = a02) ∧ (a1 = a2) ∧ (f11 = f12) ∧ (f01 = f02) ∧ (f1 = f2)

datatype_ring

|- DATATYPE (record ring R0 R1 RP RM RN)

ring_11

|- ∀a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
     (ring a0 a1 a2 a3 a4 = ring a0' a1' a2' a3' a4') ⇔
     (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2') ∧ (a3 = a3') ∧ (a4 = a4')

ring_case_cong

|- ∀M M' f.
     (M = M') ∧
     (∀a0 a1 a2 a3 a4.
        (M' = ring a0 a1 a2 a3 a4) ⇒ (f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4)) ⇒
     (ring_CASE M f = ring_CASE M' f')

ring_nchotomy

|- ∀rr. ∃a a0 f f0 f1. rr = ring a a0 f f0 f1

ring_Axiom

|- ∀f. ∃fn. ∀a0 a1 a2 a3 a4. fn (ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

ring_induction

|- ∀P. (∀a a0 f f0 f1. P (ring a a0 f f0 f1)) ⇒ ∀r. P r

plus_sym

|- ∀r. is_ring r ⇒ ∀n m. RP r n m = RP r m n

plus_assoc

|- ∀r. is_ring r ⇒ ∀n m p. RP r n (RP r m p) = RP r (RP r n m) p

mult_sym

|- ∀r. is_ring r ⇒ ∀n m. RM r n m = RM r m n

mult_assoc

|- ∀r. is_ring r ⇒ ∀n m p. RM r n (RM r m p) = RM r (RM r n m) p

plus_zero_left

|- ∀r. is_ring r ⇒ ∀n. RP r (R0 r) n = n

mult_one_left

|- ∀r. is_ring r ⇒ ∀n. RM r (R1 r) n = n

opp_def

|- ∀r. is_ring r ⇒ ∀n. RP r n (RN r n) = R0 r

distr_left

|- ∀r. is_ring r ⇒ ∀n m p. RM r (RP r n m) p = RP r (RM r n p) (RM r m p)

plus_zero_right

|- ∀r. is_ring r ⇒ ∀n. RP r n (R0 r) = n

mult_zero_left

|- ∀r. is_ring r ⇒ ∀n. RM r (R0 r) n = R0 r

mult_zero_right

|- ∀r. is_ring r ⇒ ∀n. RM r n (R0 r) = R0 r

ring_is_semi_ring

|- ∀r. is_ring r ⇒ is_semi_ring (semi_ring_of r)

mult_one_right

|- ∀r. is_ring r ⇒ ∀n. RM r n (R1 r) = n

neg_mult

|- ∀r. is_ring r ⇒ ∀a b. RM r (RN r a) b = RN r (RM r a b)