Theory: semi_ring

Parents

Types

semi_ring(Arity = 1)

Constants

semi_ring_SRM_fupd :(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a semi_ring -> 'a semi_ring
semi_ring :'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> 'a semi_ring
semi_ring_SR0_fupd :('a -> 'a) -> 'a semi_ring -> 'a semi_ring
semi_ring_size :('a -> num) -> 'a semi_ring -> num
semi_ring_SRM_update :('a -> 'a -> 'a) -> 'a semi_ring -> 'a semi_ring
ii_internal_dest_semi_ring :'a semi_ring -> ('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a)) recspace
is_semi_ring :'a semi_ring -> bool
semi_ring_SRP_fupd :(('a -> 'a -> 'a) -> 'a -> 'a -> 'a) -> 'a semi_ring -> 'a semi_ring
ii_internalsemi_ring0 :'a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> 'a semi_ring
semi_ring_SR0_update :'a -> 'a semi_ring -> 'a semi_ring
semi_ring_case :('a -> 'a -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> 'b) -> 'a semi_ring -> 'b
semi_ring_SR1_fupd :('a -> 'a) -> 'a semi_ring -> 'a semi_ring
semi_ring_SR0 :'a semi_ring -> 'a
semi_ring_SR1 :'a semi_ring -> 'a
semi_ring_SRM :'a semi_ring -> 'a -> 'a -> 'a
semi_ring_SRP :'a semi_ring -> 'a -> 'a -> 'a
semi_ring_SR1_update :'a -> 'a semi_ring -> 'a semi_ring
ii_internal_mk_semi_ring :('a # 'a # ('a -> 'a -> 'a) # ('a -> 'a -> 'a)) recspace -> 'a semi_ring
semi_ring_SRP_update :('a -> 'a -> 'a) -> 'a semi_ring -> 'a semi_ring

Definitions

ii_internalsemi_ring0_def

|- ii_internalsemi_ring0 =
   (\a0 a1 a2 a3.
      ii_internal_mk_semi_ring
        ((\a0 a1 a2 a3. CONSTR 0 (a0,a1,a2,a3) (\n. BOTTOM)) a0 a1 a2 a3))

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)

semi_ring

|- semi_ring = ii_internalsemi_ring0

semi_ring_case_def

|- !f a0 a1 a2 a3. semi_ring_case f (semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3

semi_ring_repfns

|- (!a. ii_internal_mk_semi_ring (ii_internal_dest_semi_ring a) = a) /\
   !r.
     (\a0'.
        !'semi_ring'.
          (!a0'.
             (?a0 a1 a2 a3.
                a0' =
                (\a0 a1 a2 a3. CONSTR 0 (a0,a1,a2,a3) (\n. BOTTOM)) a0 a1 a2
                  a3) ==>
             'semi_ring' a0') ==>
          'semi_ring' a0') r =
     (ii_internal_dest_semi_ring (ii_internal_mk_semi_ring r) = r)

semi_ring_size_def

|- !f a0 a1 a2 a3.
     semi_ring_size f (semi_ring a0 a1 a2 a3) = 1 + (f a0 + f a1)

semi_ring_SR0

|- !a a0 f f0. (semi_ring a a0 f f0).SR0 = a

semi_ring_SR0_fupd

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

semi_ring_SR0_update

|- !a1 a a0 f f0. (semi_ring a a0 f f0 with SR0 := a1) = semi_ring a1 a0 f f0

semi_ring_SR1

|- !a a0 f f0. (semi_ring a a0 f f0).SR1 = a0

semi_ring_SR1_fupd

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

semi_ring_SR1_update

|- !a1 a a0 f f0. (semi_ring a a0 f f0 with SR1 := a1) = semi_ring a a1 f f0

semi_ring_SRM

|- !a a0 f f0. (semi_ring a a0 f f0).SRM = f0

semi_ring_SRM_fupd

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

semi_ring_SRM_update

|- !f1 a a0 f f0. (semi_ring a a0 f f0 with SRM := f1) = semi_ring a a0 f f1

semi_ring_SRP

|- !a a0 f f0. (semi_ring a a0 f f0).SRP = f

semi_ring_SRP_fupd

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

semi_ring_SRP_update

|- !f1 a a0 f f0. (semi_ring a a0 f f0 with SRP := f1) = semi_ring a a0 f1 f0

semi_ring_TY_DEF

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

Theorems

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

|- (!s x. (s with SR1 := x).SR0 = s.SR0) /\
   (!s x. (s with SRP := x).SR0 = s.SR0) /\
   (!s x. (s with SRM := x).SR0 = s.SR0) /\
   (!s x. (s with SR0 := x).SR1 = s.SR1) /\
   (!s x. (s with SRP := x).SR1 = s.SR1) /\
   (!s x. (s with SRM := x).SR1 = s.SR1) /\
   (!s x. (s with SR0 := x).SRP = s.SRP) /\
   (!s x. (s with SR1 := x).SRP = s.SRP) /\
   (!s x. (s with SRM := x).SRP = s.SRP) /\
   (!s x. (s with SR0 := x).SRM = s.SRM) /\
   (!s x. (s with SR1 := x).SRM = s.SRM) /\
   (!s x. (s with SRP := x).SRM = s.SRM) /\
   (!s x. (s with SR0 := x).SR0 = x) /\ (!s x. (s with SR1 := x).SR1 = x) /\
   (!s x. (s with SRP := x).SRP = x) /\ !s x. (s with SRM := x).SRM = x

semi_ring_Axiom

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

semi_ring_case_cong

|- !f' f M' M.
     (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 f M = semi_ring_case f' M')

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_cupdaccs

|- (!s val. (val = s.SR0) ==> ((s with SR0 := val) = s)) /\
   (!s val. (val = s.SR1) ==> ((s with SR1 := val) = s)) /\
   (!s val. (val = s.SRP) ==> ((s with SRP := val) = s)) /\
   !s val. (val = s.SRM) ==> ((s with SRM := val) = s)

semi_ring_fn_updates

|- (!f x. (x with SR0 updated_by f) = (x with SR0 := f x.SR0)) /\
   (!f x. (x with SR1 updated_by f) = (x with SR1 := f x.SR1)) /\
   (!f x. (x with SRP updated_by f) = (x with SRP := f x.SRP)) /\
   !f x. (x with SRM updated_by f) = (x with SRM := f x.SRM)

semi_ring_induction

|- !P. (!a a0 f f0. P (semi_ring a a0 f f0)) ==> !s. P s

semi_ring_nchotomy

|- !s. ?a a0 f f0. s = semi_ring a a0 f f0

semi_ring_SR0_update_semi11

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

semi_ring_SR1_update_semi11

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

semi_ring_SRM_update_semi11

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

semi_ring_SRP_update_semi11

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

semi_ring_updaccs

|- (!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_updates

|- (!a1 a a0 f f0.
      (semi_ring a a0 f f0 with SR0 := a1) = semi_ring a1 a0 f f0) /\
   (!a1 a a0 f f0.
      (semi_ring a a0 f f0 with SR1 := a1) = semi_ring a a1 f f0) /\
   (!f1 a a0 f f0.
      (semi_ring a a0 f f0 with SRP := f1) = semi_ring a a0 f1 f0) /\
   !f1 a a0 f f0. (semi_ring a a0 f f0 with SRM := f1) = semi_ring a a0 f f1

semi_ring_updates_eq_literal

|- !s f f0 a a0.
     (s with <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>) =
     <|SR0 := a0; SR1 := a; SRP := f0; SRM := f|>

semi_ring_updcanon

|- (!s z x.
      (s with <|SR1 := x; SR0 := z|>) = (s with <|SR0 := z; SR1 := x|>)) /\
   (!s z x.
      (s with <|SRP := x; SR0 := z|>) = (s with <|SR0 := z; SRP := x|>)) /\
   (!s z x.
      (s with <|SRP := x; SR1 := z|>) = (s with <|SR1 := z; SRP := x|>)) /\
   (!s z x.
      (s with <|SRM := x; SR0 := z|>) = (s with <|SR0 := z; SRM := x|>)) /\
   (!s z x.
      (s with <|SRM := x; SR1 := z|>) = (s with <|SR1 := z; SRM := x|>)) /\
   !s z x. (s with <|SRM := x; SRP := z|>) = (s with <|SRP := z; SRM := x|>)

semi_ring_updupds

|- (!s x2 x1. (s with <|SR0 := x1; SR0 := x2|>) = (s with SR0 := x1)) /\
   (!s x2 x1. (s with <|SR1 := x1; SR1 := x2|>) = (s with SR1 := x1)) /\
   (!s x2 x1. (s with <|SRP := x1; SRP := x2|>) = (s with SRP := x1)) /\
   !s x2 x1. (s with <|SRM := x1; SRM := x2|>) = (s with SRM := x1)