Theory "ring"

Parents semi_ring

Signature

Type	Arity
ring	1
Constant	Type
is_ring	:α ring -> bool
recordtype.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. (ring a a0 f f0 f1).R0 = a

ring_R1

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

ring_RP

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

ring_RM

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

ring_RN

|- ∀a a0 f f0 f1. (ring a a0 f f0 f1).RN = 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. r.RP n m = r.RP m n) ∧
     (∀n m p. r.RP n (r.RP m p) = r.RP (r.RP n m) p) ∧
     (∀n m. r.RM n m = r.RM m n) ∧
     (∀n m p. r.RM n (r.RM m p) = r.RM (r.RM n m) p) ∧ (∀n. r.RP r.R0 n = n) ∧
     (∀n. r.RM r.R1 n = n) ∧ (∀n. r.RP n (r.RN n) = r.R0) ∧
     ∀n m p. r.RM (r.RP n m) p = r.RP (r.RM n p) (r.RM m p)

semi_ring_of_def

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

Theorems

ring_accessors

|- (∀a a0 f f0 f1. (ring a a0 f f0 f1).R0 = a) ∧
   (∀a a0 f f0 f1. (ring a a0 f f0 f1).R1 = a0) ∧
   (∀a a0 f f0 f1. (ring a a0 f f0 f1).RP = f) ∧
   (∀a a0 f f0 f1. (ring a a0 f f0 f1).RM = f0) ∧
   ∀a a0 f f0 f1. (ring a a0 f f0 f1).RN = 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. (r with R1 updated_by f).R0 = r.R0) ∧
   (∀r f. (r with RP updated_by f).R0 = r.R0) ∧
   (∀r f. (r with RM updated_by f).R0 = r.R0) ∧
   (∀r f. (r with RN updated_by f).R0 = r.R0) ∧
   (∀r f. (r with R0 updated_by f).R1 = r.R1) ∧
   (∀r f. (r with RP updated_by f).R1 = r.R1) ∧
   (∀r f. (r with RM updated_by f).R1 = r.R1) ∧
   (∀r f. (r with RN updated_by f).R1 = r.R1) ∧
   (∀r f. (r with R0 updated_by f).RP = r.RP) ∧
   (∀r f. (r with R1 updated_by f).RP = r.RP) ∧
   (∀r f. (r with RM updated_by f).RP = r.RP) ∧
   (∀r f. (r with RN updated_by f).RP = r.RP) ∧
   (∀r f. (r with R0 updated_by f).RM = r.RM) ∧
   (∀r f. (r with R1 updated_by f).RM = r.RM) ∧
   (∀r f. (r with RP updated_by f).RM = r.RM) ∧
   (∀r f. (r with RN updated_by f).RM = r.RM) ∧
   (∀r f. (r with R0 updated_by f).RN = r.RN) ∧
   (∀r f. (r with R1 updated_by f).RN = r.RN) ∧
   (∀r f. (r with RP updated_by f).RN = r.RN) ∧
   (∀r f. (r with RM updated_by f).RN = r.RN) ∧
   (∀r f. (r with R0 updated_by f).R0 = f r.R0) ∧
   (∀r f. (r with R1 updated_by f).R1 = f r.R1) ∧
   (∀r f. (r with RP updated_by f).RP = f r.RP) ∧
   (∀r f. (r with RM updated_by f).RM = f r.RM) ∧
   ∀r f. (r with RN updated_by f).RN = f r.RN

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. R0_fupd f o R0_fupd g = R0_fupd (f o g)) ∧
    ∀h g f. R0_fupd f o R0_fupd g o h = R0_fupd (f o g) o h) ∧
   ((∀g f. R1_fupd f o R1_fupd g = R1_fupd (f o g)) ∧
    ∀h g f. R1_fupd f o R1_fupd g o h = R1_fupd (f o g) o h) ∧
   ((∀g f. RP_fupd f o RP_fupd g = RP_fupd (f o g)) ∧
    ∀h g f. RP_fupd f o RP_fupd g o h = RP_fupd (f o g) o h) ∧
   ((∀g f. RM_fupd f o RM_fupd g = RM_fupd (f o g)) ∧
    ∀h g f. RM_fupd f o RM_fupd g o h = RM_fupd (f o g) o h) ∧
   (∀g f. RN_fupd f o RN_fupd g = RN_fupd (f o g)) ∧
   ∀h g f. RN_fupd f o RN_fupd g o h = RN_fupd (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. R1_fupd f o R0_fupd g = R0_fupd g o R1_fupd f) ∧
    ∀h g f. R1_fupd f o R0_fupd g o h = R0_fupd g o R1_fupd f o h) ∧
   ((∀g f. RP_fupd f o R0_fupd g = R0_fupd g o RP_fupd f) ∧
    ∀h g f. RP_fupd f o R0_fupd g o h = R0_fupd g o RP_fupd f o h) ∧
   ((∀g f. RP_fupd f o R1_fupd g = R1_fupd g o RP_fupd f) ∧
    ∀h g f. RP_fupd f o R1_fupd g o h = R1_fupd g o RP_fupd f o h) ∧
   ((∀g f. RM_fupd f o R0_fupd g = R0_fupd g o RM_fupd f) ∧
    ∀h g f. RM_fupd f o R0_fupd g o h = R0_fupd g o RM_fupd f o h) ∧
   ((∀g f. RM_fupd f o R1_fupd g = R1_fupd g o RM_fupd f) ∧
    ∀h g f. RM_fupd f o R1_fupd g o h = R1_fupd g o RM_fupd f o h) ∧
   ((∀g f. RM_fupd f o RP_fupd g = RP_fupd g o RM_fupd f) ∧
    ∀h g f. RM_fupd f o RP_fupd g o h = RP_fupd g o RM_fupd f o h) ∧
   ((∀g f. RN_fupd f o R0_fupd g = R0_fupd g o RN_fupd f) ∧
    ∀h g f. RN_fupd f o R0_fupd g o h = R0_fupd g o RN_fupd f o h) ∧
   ((∀g f. RN_fupd f o R1_fupd g = R1_fupd g o RN_fupd f) ∧
    ∀h g f. RN_fupd f o R1_fupd g o h = R1_fupd g o RN_fupd f o h) ∧
   ((∀g f. RN_fupd f o RP_fupd g = RP_fupd g o RN_fupd f) ∧
    ∀h g f. RN_fupd f o RP_fupd g o h = RP_fupd g o RN_fupd f o h) ∧
   (∀g f. RN_fupd f o RM_fupd g = RM_fupd g o RN_fupd f) ∧
   ∀h g f. RN_fupd f o RM_fupd g o h = RM_fupd g o RN_fupd f o h

ring_component_equality

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

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. r.RP n m = r.RP m n

plus_assoc

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

mult_sym

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

mult_assoc

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

plus_zero_left

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

mult_one_left

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

opp_def

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

distr_left

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

plus_zero_right

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

mult_zero_left

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

mult_zero_right

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

ring_is_semi_ring

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

mult_one_right

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

neg_mult

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