Theory: ring

Parents

semi_ring

Types

ring(Arity = 1)

Constants

ring_R1_fupd :('a -> 'a) -> 'a ring -> 'a ring
ring_R0_update :'a -> 'a ring -> 'a ring
ii_internalring0 :'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'a ring
ring_size :('a -> num) -> 'a ring -> num
ring_R1_update :'a -> 'a ring -> 'a ring
ring_RP_update :('a -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RM_fupd :(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a ring -> 'a ring
semi_ring_of :'a ring -> 'a semi_ring
ring_R0_fupd :('a -> 'a) -> 'a ring -> 'a ring
ring_case :('a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'b) -> 'a ring -> 'b
ii_internal_dest_ring :'a ring -> ('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a) # ('a -> 'a)) recspace
ring_R0 :'a ring -> 'a
ring_R1 :'a ring -> 'a
ring_RM :'a ring -> 'a -> 'a -> 'a
ring_RN :'a ring -> 'a -> 'a
ring_RP :'a ring -> 'a -> 'a -> 'a
ii_internal_mk_ring :('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a) # ('a -> 'a)) recspace -> 'a ring
ring_RM_update :('a -> 'a -> 'a) -> 'a ring -> 'a ring
ring :'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a) -> 'a ring
ring_RN_fupd :(('a -> 'a) -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RP_fupd :(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a ring -> 'a ring
ring_RN_update :('a -> 'a) -> 'a ring -> 'a ring
is_ring :'a ring -> bool

Definitions

ii_internalring0_def

|- ii_internalring0 =
   (\a0 a1 a2 a3 a4.
      ii_internal_mk_ring
        ((\a0 a1 a2 a3 a4. CONSTR 0 (a0,a1,a2,a3,a4) (\n. BOTTOM)) a0 a1 a2 a3
           a4))

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)

ring

|- ring = ii_internalring0

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_R0

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

ring_R0_fupd

|- !f x. (x with R0 updated_by f) = (x with R0 := f x.R0)

ring_R0_update

|- !a1 a a0 f f0 f1. (ring a a0 f f0 f1 with R0 := a1) = ring a1 a0 f f0 f1

ring_R1

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

ring_R1_fupd

|- !f x. (x with R1 updated_by f) = (x with R1 := f x.R1)

ring_R1_update

|- !a1 a a0 f f0 f1. (ring a a0 f f0 f1 with R1 := a1) = ring a a1 f f0 f1

ring_repfns

|- (!a. ii_internal_mk_ring (ii_internal_dest_ring a) = a) /\
   !r.
     (\a0'.
        !'ring'.
          (!a0'.
             (?a0 a1 a2 a3 a4.
                a0' =
                (\a0 a1 a2 a3 a4. CONSTR 0 (a0,a1,a2,a3,a4) (\n. BOTTOM)) a0
                  a1 a2 a3 a4) ==>
             'ring' a0') ==>
          'ring' a0') r =
     (ii_internal_dest_ring (ii_internal_mk_ring r) = r)

ring_RM

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

ring_RM_fupd

|- !f x. (x with RM updated_by f) = (x with RM := f x.RM)

ring_RM_update

|- !f2 a a0 f f0 f1. (ring a a0 f f0 f1 with RM := f2) = ring a a0 f f2 f1

ring_RN

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

ring_RN_fupd

|- !f x. (x with RN updated_by f) = (x with RN := f x.RN)

ring_RN_update

|- !f2 a a0 f f0 f1. (ring a a0 f f0 f1 with RN := f2) = ring a a0 f f0 f2

ring_RP

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

ring_RP_fupd

|- !f x. (x with RP updated_by f) = (x with RP := f x.RP)

ring_RP_update

|- !f2 a a0 f f0 f1. (ring a a0 f f0 f1 with RP := f2) = ring a a0 f2 f0 f1

ring_size_def

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

ring_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'ring'.
            (!a0'.
               (?a0 a1 a2 a3 a4.
                  a0' =
                  (\a0 a1 a2 a3 a4. CONSTR 0 (a0,a1,a2,a3,a4) (\n. BOTTOM)) a0
                    a1 a2 a3 a4) ==>
               'ring' a0') ==>
            'ring' a0') rep

semi_ring_of_def

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

Theorems

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)

mult_assoc

|- !r. is_ring r ==> !n m p. r.RM n (r.RM m p) = r.RM (r.RM n m) p

mult_one_left

|- !r. is_ring r ==> !n. r.RM r.R1 n = n

mult_one_right

|- !r. is_ring r ==> !n. r.RM n r.R1 = n

mult_sym

|- !r. is_ring r ==> !n m. r.RM n m = r.RM m 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

neg_mult

|- !r. is_ring r ==> !m n. r.RM (r.RN a) b = r.RN (r.RM a b)

opp_def

|- !r. is_ring r ==> !n. r.RP n (r.RN n) = r.R0

plus_assoc

|- !r. is_ring r ==> !n m p. r.RP n (r.RP m p) = r.RP (r.RP n m) p

plus_sym

|- !r. is_ring r ==> !n m. r.RP n m = r.RP m n

plus_zero_left

|- !r. is_ring r ==> !n. r.RP r.R0 n = n

plus_zero_right

|- !r. is_ring r ==> !n. r.RP n r.R0 = n

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

|- (!r x. (r with R1 := x).R0 = r.R0) /\ (!r x. (r with RP := x).R0 = r.R0) /\
   (!r x. (r with RM := x).R0 = r.R0) /\ (!r x. (r with RN := x).R0 = r.R0) /\
   (!r x. (r with R0 := x).R1 = r.R1) /\ (!r x. (r with RP := x).R1 = r.R1) /\
   (!r x. (r with RM := x).R1 = r.R1) /\ (!r x. (r with RN := x).R1 = r.R1) /\
   (!r x. (r with R0 := x).RP = r.RP) /\ (!r x. (r with R1 := x).RP = r.RP) /\
   (!r x. (r with RM := x).RP = r.RP) /\ (!r x. (r with RN := x).RP = r.RP) /\
   (!r x. (r with R0 := x).RM = r.RM) /\ (!r x. (r with R1 := x).RM = r.RM) /\
   (!r x. (r with RP := x).RM = r.RM) /\ (!r x. (r with RN := x).RM = r.RM) /\
   (!r x. (r with R0 := x).RN = r.RN) /\ (!r x. (r with R1 := x).RN = r.RN) /\
   (!r x. (r with RP := x).RN = r.RN) /\ (!r x. (r with RM := x).RN = r.RN) /\
   (!r x. (r with R0 := x).R0 = x) /\ (!r x. (r with R1 := x).R1 = x) /\
   (!r x. (r with RP := x).RP = x) /\ (!r x. (r with RM := x).RM = x) /\
   !r x. (r with RN := x).RN = x

ring_Axiom

|- !f. ?fn. !a0 a1 a2 a3 a4. fn (ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

ring_case_cong

|- !f' f M' M.
     (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_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_cupdaccs

|- (!r val. (val = r.R0) ==> ((r with R0 := val) = r)) /\
   (!r val. (val = r.R1) ==> ((r with R1 := val) = r)) /\
   (!r val. (val = r.RP) ==> ((r with RP := val) = r)) /\
   (!r val. (val = r.RM) ==> ((r with RM := val) = r)) /\
   !r val. (val = r.RN) ==> ((r with RN := val) = r)

ring_fn_updates

|- (!f x. (x with R0 updated_by f) = (x with R0 := f x.R0)) /\
   (!f x. (x with R1 updated_by f) = (x with R1 := f x.R1)) /\
   (!f x. (x with RP updated_by f) = (x with RP := f x.RP)) /\
   (!f x. (x with RM updated_by f) = (x with RM := f x.RM)) /\
   !f x. (x with RN updated_by f) = (x with RN := f x.RN)

ring_induction

|- !P. (!a a0 f f0 f1. P (ring a a0 f f0 f1)) ==> !r. P r

ring_is_semi_ring

|- !r. is_ring r ==> is_semi_ring (semi_ring_of r)

ring_nchotomy

|- !r. ?a a0 f f0 f1. r = ring a a0 f f0 f1

ring_R0_update_semi11

|- !x y r1 r2. ((r1 with R0 := x) = (r2 with R0 := y)) ==> (x = y)

ring_R1_update_semi11

|- !x y r1 r2. ((r1 with R1 := x) = (r2 with R1 := y)) ==> (x = y)

ring_RM_update_semi11

|- !x y r1 r2. ((r1 with RM := x) = (r2 with RM := y)) ==> (x = y)

ring_RN_update_semi11

|- !x y r1 r2. ((r1 with RN := x) = (r2 with RN := y)) ==> (x = y)

ring_RP_update_semi11

|- !x y r1 r2. ((r1 with RP := x) = (r2 with RP := y)) ==> (x = y)

ring_updaccs

|- (!r. (r with R0 := r.R0) = r) /\ (!r. (r with R1 := r.R1) = r) /\
   (!r. (r with RP := r.RP) = r) /\ (!r. (r with RM := r.RM) = r) /\
   !r. (r with RN := r.RN) = r

ring_updates

|- (!a1 a a0 f f0 f1.
      (ring a a0 f f0 f1 with R0 := a1) = ring a1 a0 f f0 f1) /\
   (!a1 a a0 f f0 f1.
      (ring a a0 f f0 f1 with R1 := a1) = ring a a1 f f0 f1) /\
   (!f2 a a0 f f0 f1.
      (ring a a0 f f0 f1 with RP := f2) = ring a a0 f2 f0 f1) /\
   (!f2 a a0 f f0 f1.
      (ring a a0 f f0 f1 with RM := f2) = ring a a0 f f2 f1) /\
   !f2 a a0 f f0 f1. (ring a a0 f f0 f1 with RN := f2) = ring a a0 f f0 f2

ring_updates_eq_literal

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

ring_updcanon

|- (!r z x. (r with <|R1 := x; R0 := z|>) = (r with <|R0 := z; R1 := x|>)) /\
   (!r z x. (r with <|RP := x; R0 := z|>) = (r with <|R0 := z; RP := x|>)) /\
   (!r z x. (r with <|RP := x; R1 := z|>) = (r with <|R1 := z; RP := x|>)) /\
   (!r z x. (r with <|RM := x; R0 := z|>) = (r with <|R0 := z; RM := x|>)) /\
   (!r z x. (r with <|RM := x; R1 := z|>) = (r with <|R1 := z; RM := x|>)) /\
   (!r z x. (r with <|RM := x; RP := z|>) = (r with <|RP := z; RM := x|>)) /\
   (!r z x. (r with <|RN := x; R0 := z|>) = (r with <|R0 := z; RN := x|>)) /\
   (!r z x. (r with <|RN := x; R1 := z|>) = (r with <|R1 := z; RN := x|>)) /\
   (!r z x. (r with <|RN := x; RP := z|>) = (r with <|RP := z; RN := x|>)) /\
   !r z x. (r with <|RN := x; RM := z|>) = (r with <|RM := z; RN := x|>)

ring_updupds

|- (!r x2 x1. (r with <|R0 := x1; R0 := x2|>) = (r with R0 := x1)) /\
   (!r x2 x1. (r with <|R1 := x1; R1 := x2|>) = (r with R1 := x1)) /\
   (!r x2 x1. (r with <|RP := x1; RP := x2|>) = (r with RP := x1)) /\
   (!r x2 x1. (r with <|RM := x1; RM := x2|>) = (r with RM := x1)) /\
   !r x2 x1. (r with <|RN := x1; RN := x2|>) = (r with RN := x1)