Theory: EVAL

Type operators

ring : α ring

Constants

is_ring : α ring -> bool
recordtype.ring : α -> α -> (α -> α -> α) -> (α -> α -> α) -> (α -> α) -> α ring
recordtype.ring.seldef.R0 : α ring -> α
recordtype.ring.seldef.R0_fupd : (α -> α) -> α ring -> α ring
recordtype.ring.seldef.R1 : α ring -> α
recordtype.ring.seldef.R1_fupd : (α -> α) -> α ring -> α ring
recordtype.ring.seldef.RM : α ring -> α -> α -> α
recordtype.ring.seldef.RM_fupd : ((α -> α -> α) -> α -> α -> α) -> α ring -> α ring
recordtype.ring.seldef.RN : α ring -> α -> α
recordtype.ring.seldef.RN_fupd : ((α -> α) -> α -> α) -> α ring -> α ring
recordtype.ring.seldef.RP : α ring -> α -> α -> α
recordtype.ring.seldef.RP_fupd : ((α -> α -> α) -> α -> α -> α) -> α ring -> α ring
ring_ABS : 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1) -> 'b1 ring
ring_CASE : α ring -> (α -> α -> (α -> α -> α) -> (α -> α -> α) -> (α -> α) -> β) -> β
ring_CONS : 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1) -> 'b1 ring
ring_REP : 'b1 ring -> 'b1 # 'b1 # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1 -> 'b1) # ('b1 -> 'b1)
ring_size : (α -> num) -> α ring -> num
semi_ring_of : α ring -> α semi_ring

Definitions

is_ring_def recordtype_ring_seldef_R0_def recordtype_ring_seldef_R0_fupd_def recordtype_ring_seldef_R1_def recordtype_ring_seldef_R1_fupd_def recordtype_ring_seldef_RM_def recordtype_ring_seldef_RM_fupd_def recordtype_ring_seldef_RN_def recordtype_ring_seldef_RN_fupd_def recordtype_ring_seldef_RP_def recordtype_ring_seldef_RP_fupd_def ring_ABSREP ring_CONS_def ring_TY_DEF ring_case_def ring_size_def semi_ring_of_def

Theorems

Definitions

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)

recordtype_ring_seldef_R0_def

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

recordtype_ring_seldef_R0_fupd_def

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

recordtype_ring_seldef_R1_def

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

recordtype_ring_seldef_R1_fupd_def

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

recordtype_ring_seldef_RM_def

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

recordtype_ring_seldef_RM_fupd_def

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

recordtype_ring_seldef_RN_def

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

recordtype_ring_seldef_RN_fupd_def

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

recordtype_ring_seldef_RP_def

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

recordtype_ring_seldef_RP_fupd_def

⊢ ∀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_ABSREP

⊢ (∀a. ring_ABS (ring_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ ring_REP (ring_ABS r) = r

ring_CONS_def

⊢ ring_CONS = ring_ABS

ring_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λx. T) 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

⊢ ∀f0 a0 a1 a2 a3 a4.
    ring_size f0 (ring a0 a1 a2 a3 a4) = 1 + (f0 a0 + f0 a1)

semi_ring_of_def

⊢ ∀r. semi_ring_of r = semi_ring r.R0 r.R1 r.RP r.RM

Theorems

EXISTS_ring

⊢ ∀P. (∃r. P r) ⇔
      ∃a0 a f1 f0 f. P <|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|>

datatype_ring

⊢ DATATYPE (record ring R0 R1 RP RM RN)

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 ⇒ ∀a b. 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_Axiom

⊢ ∀f0. ∃h. ∀a0 a1 a2 a3 a4. h (ring a0 a1 a2 a3 a4) = f0 a0 a1 a2 a3 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_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_case_eq

⊢ ring_CASE x f = v ⇔
  ∃a a0 f' f0 f1. x = ring a a0 f' f0 f1 ∧ f a a0 f' f0 f1 = v

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

ring_fupdfupds

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

ring_fupdfupds_comp

⊢ ((∀g f. R0_fupd f ∘ R0_fupd g = R0_fupd (f ∘ g)) ∧
   ∀h g f. R0_fupd f ∘ R0_fupd g ∘ h = R0_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. R1_fupd f ∘ R1_fupd g = R1_fupd (f ∘ g)) ∧
   ∀h g f. R1_fupd f ∘ R1_fupd g ∘ h = R1_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. RP_fupd f ∘ RP_fupd g = RP_fupd (f ∘ g)) ∧
   ∀h g f. RP_fupd f ∘ RP_fupd g ∘ h = RP_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. RM_fupd f ∘ RM_fupd g = RM_fupd (f ∘ g)) ∧
   ∀h g f. RM_fupd f ∘ RM_fupd g ∘ h = RM_fupd (f ∘ g) ∘ h) ∧
  (∀g f. RN_fupd f ∘ RN_fupd g = RN_fupd (f ∘ g)) ∧
  ∀h g f. RN_fupd f ∘ RN_fupd g ∘ h = RN_fupd (f ∘ g) ∘ h

ring_fupdselfid

⊢ (∀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_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_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

ring_literal_nchotomy

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

ring_nchotomy

⊢ ∀rr. ∃a a0 f f0 f1. rr = ring a a0 f f0 f1

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

Theory EVAL_ring

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems