Theory "ring"

Parents semi_ring

Signature

Type	Arity
ring	1
Constant	Type
semi_ring_of	:'a ring -> 'a semi_ring
ring_size	:('a -> num) -> 'a ring -> num
ring_case	:('a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'b) -> 'a ring -> 'b
ring_RP_fupd	:(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RP	:'a ring -> 'a -> 'a -> 'a
ring_RN_fupd	:(('a -> 'a) -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RN	:'a ring -> 'a -> 'a
ring_RM_fupd	:(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RM	:'a ring -> 'a -> 'a -> 'a
ring_R1_fupd	:('a -> 'a) -> 'a ring -> 'a ring
ring_R1	:'a ring -> 'a
ring_R0_fupd	:('a -> 'a) -> 'a ring -> 'a ring
ring_R0	:'a ring -> 'a
ring0	:'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'a ring
ring	:'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'a ring
mk_ring	:('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a) # ('a -> 'a)) recspace -> 'a ring
is_ring	:'a ring -> bool
dest_ring	:'a ring -> ('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a) # ('a -> 'a)) recspace

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_repfns

|- (!a. mk_ring (dest_ring a) = a) /\
   !r.
     (\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') r =
     (dest_ring (mk_ring r) = r)

ring0_def

|- ring0 =
   (\a0 a1 a2 a3 a4.
      mk_ring
        ((\a0 a1 a2 a3 a4.
            ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM)) a0 a1 a2
           a3 a4))

ring

|- ring = ring0

ring_case_def

|- !f a0 a1 a2 a3 a4. ring_case f (ring a0 a1 a2 a3 a4) = 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. ring_R0_fupd f o ring_R0_fupd g = ring_R0_fupd (f o g)) /\
    !h g f. ring_R0_fupd f o ring_R0_fupd g o h = ring_R0_fupd (f o g) o h) /\
   ((!g f. ring_R1_fupd f o ring_R1_fupd g = ring_R1_fupd (f o g)) /\
    !h g f. ring_R1_fupd f o ring_R1_fupd g o h = ring_R1_fupd (f o g) o h) /\
   ((!g f. ring_RP_fupd f o ring_RP_fupd g = ring_RP_fupd (f o g)) /\
    !h g f. ring_RP_fupd f o ring_RP_fupd g o h = ring_RP_fupd (f o g) o h) /\
   ((!g f. ring_RM_fupd f o ring_RM_fupd g = ring_RM_fupd (f o g)) /\
    !h g f. ring_RM_fupd f o ring_RM_fupd g o h = ring_RM_fupd (f o g) o h) /\
   (!g f. ring_RN_fupd f o ring_RN_fupd g = ring_RN_fupd (f o g)) /\
   !h g f. ring_RN_fupd f o ring_RN_fupd g o h = ring_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.
       ring_R1_fupd f o ring_R0_fupd g = ring_R0_fupd g o ring_R1_fupd f) /\
    !h g f.
      ring_R1_fupd f o ring_R0_fupd g o h =
      ring_R0_fupd g o ring_R1_fupd f o h) /\
   ((!g f.
       ring_RP_fupd f o ring_R0_fupd g = ring_R0_fupd g o ring_RP_fupd f) /\
    !h g f.
      ring_RP_fupd f o ring_R0_fupd g o h =
      ring_R0_fupd g o ring_RP_fupd f o h) /\
   ((!g f.
       ring_RP_fupd f o ring_R1_fupd g = ring_R1_fupd g o ring_RP_fupd f) /\
    !h g f.
      ring_RP_fupd f o ring_R1_fupd g o h =
      ring_R1_fupd g o ring_RP_fupd f o h) /\
   ((!g f.
       ring_RM_fupd f o ring_R0_fupd g = ring_R0_fupd g o ring_RM_fupd f) /\
    !h g f.
      ring_RM_fupd f o ring_R0_fupd g o h =
      ring_R0_fupd g o ring_RM_fupd f o h) /\
   ((!g f.
       ring_RM_fupd f o ring_R1_fupd g = ring_R1_fupd g o ring_RM_fupd f) /\
    !h g f.
      ring_RM_fupd f o ring_R1_fupd g o h =
      ring_R1_fupd g o ring_RM_fupd f o h) /\
   ((!g f.
       ring_RM_fupd f o ring_RP_fupd g = ring_RP_fupd g o ring_RM_fupd f) /\
    !h g f.
      ring_RM_fupd f o ring_RP_fupd g o h =
      ring_RP_fupd g o ring_RM_fupd f o h) /\
   ((!g f.
       ring_RN_fupd f o ring_R0_fupd g = ring_R0_fupd g o ring_RN_fupd f) /\
    !h g f.
      ring_RN_fupd f o ring_R0_fupd g o h =
      ring_R0_fupd g o ring_RN_fupd f o h) /\
   ((!g f.
       ring_RN_fupd f o ring_R1_fupd g = ring_R1_fupd g o ring_RN_fupd f) /\
    !h g f.
      ring_RN_fupd f o ring_R1_fupd g o h =
      ring_R1_fupd g o ring_RN_fupd f o h) /\
   ((!g f.
       ring_RN_fupd f o ring_RP_fupd g = ring_RP_fupd g o ring_RN_fupd f) /\
    !h g f.
      ring_RN_fupd f o ring_RP_fupd g o h =
      ring_RP_fupd g o ring_RN_fupd f o h) /\
   (!g f.
      ring_RN_fupd f o ring_RM_fupd g = ring_RM_fupd g o ring_RN_fupd f) /\
   !h g f.
     ring_RN_fupd f o ring_RM_fupd g o h = ring_RM_fupd g o ring_RN_fupd 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 f M = ring_case f' M')

ring_nchotomy

|- !r. ?a a0 f f0 f1. r = 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)