Structure ringTheory
signature ringTheory =
sig
type thm = Thm.thm
(* Definitions *)
val is_ring_def : thm
val ring_R0 : thm
val ring_R0_fupd : thm
val ring_R1 : thm
val ring_R1_fupd : thm
val ring_RM : thm
val ring_RM_fupd : thm
val ring_RN : thm
val ring_RN_fupd : thm
val ring_RP : thm
val ring_RP_fupd : thm
val ring_TY_DEF : thm
val ring_case_def : thm
val ring_size_def : thm
val semi_ring_of_def : thm
(* Theorems *)
val EXISTS_ring : thm
val FORALL_ring : thm
val datatype_ring : thm
val distr_left : thm
val mult_assoc : thm
val mult_one_left : thm
val mult_one_right : thm
val mult_sym : thm
val mult_zero_left : thm
val mult_zero_right : thm
val neg_mult : thm
val opp_def : thm
val plus_assoc : thm
val plus_sym : thm
val plus_zero_left : thm
val plus_zero_right : thm
val ring_11 : thm
val ring_Axiom : thm
val ring_accessors : thm
val ring_accfupds : thm
val ring_case_cong : thm
val ring_case_eq : thm
val ring_component_equality : thm
val ring_fn_updates : thm
val ring_fupdcanon : thm
val ring_fupdcanon_comp : thm
val ring_fupdfupds : thm
val ring_fupdfupds_comp : thm
val ring_induction : thm
val ring_is_semi_ring : thm
val ring_literal_11 : thm
val ring_literal_nchotomy : thm
val ring_nchotomy : thm
val ring_updates_eq_literal : thm
val ring_grammars : type_grammar.grammar * term_grammar.grammar
val IMPORT : abstraction.inst_infos ->
{ is_ring_def : thm,
ring_case_def : thm,
ring_R0 : thm,
ring_R0_fupd : thm,
ring_R1 : thm,
ring_R1_fupd : thm,
ring_RM : thm,
ring_RM_fupd : thm,
ring_RN : thm,
ring_RN_fupd : thm,
ring_RP : thm,
ring_RP_fupd : thm,
ring_size_def : thm,
ring_TY_DEF : thm,
semi_ring_of_def : thm,
datatype_ring : thm,
distr_left : thm,
EXISTS_ring : thm,
FORALL_ring : thm,
mult_assoc : thm,
mult_one_left : thm,
mult_one_right : thm,
mult_sym : thm,
mult_zero_left : thm,
mult_zero_right : thm,
neg_mult : thm,
opp_def : thm,
plus_assoc : thm,
plus_sym : thm,
plus_zero_left : thm,
plus_zero_right : thm,
ring_11 : thm,
ring_accessors : thm,
ring_accfupds : thm,
ring_Axiom : thm,
ring_case_cong : thm,
ring_case_eq : thm,
ring_component_equality : thm,
ring_fn_updates : thm,
ring_fupdcanon : thm,
ring_fupdcanon_comp : thm,
ring_fupdfupds : thm,
ring_fupdfupds_comp : thm,
ring_induction : thm,
ring_is_semi_ring : thm,
ring_literal_11 : thm,
ring_literal_nchotomy : thm,
ring_nchotomy : thm,
ring_updates_eq_literal : thm }
(*
[semi_ring] Parent theory of "ring"
[is_ring_def] Definition
⊢ ∀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_R0] Definition
⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).R0 = a
[ring_R0_fupd] Definition
⊢ ∀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] Definition
⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).R1 = a0
[ring_R1_fupd] Definition
⊢ ∀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_RM] Definition
⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RM = f0
[ring_RM_fupd] Definition
⊢ ∀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] Definition
⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RN = f1
[ring_RN_fupd] Definition
⊢ ∀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_RP] Definition
⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RP = f
[ring_RP_fupd] Definition
⊢ ∀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_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('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) ⇒
$var$('ring') a0') ⇒
$var$('ring') a0') rep
[ring_case_def] Definition
⊢ ∀a0 a1 a2 a3 a4 f.
ring_CASE (ring a0 a1 a2 a3 a4) f = f a0 a1 a2 a3 a4
[ring_size_def] Definition
⊢ ∀f a0 a1 a2 a3 a4.
ring_size f (ring a0 a1 a2 a3 a4) = 1 + (f a0 + f a1)
[semi_ring_of_def] Definition
⊢ ∀r. semi_ring_of r = semi_ring r.R0 r.R1 r.RP r.RM
[EXISTS_ring] Theorem
⊢ ∀P.
(∃r. P r) ⇔
∃a0 a f1 f0 f.
P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
[FORALL_ring] Theorem
⊢ ∀P.
(∀r. P r) ⇔
∀a0 a f1 f0 f.
P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
[datatype_ring] Theorem
⊢ DATATYPE (record ring R0 R1 RP RM RN)
[distr_left] Theorem
⊢ ∀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] Theorem
⊢ ∀r. is_ring r ⇒ ∀n m p. r.RM n (r.RM m p) = r.RM (r.RM n m) p
[mult_one_left] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RM r.R1 n = n
[mult_one_right] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RM n r.R1 = n
[mult_sym] Theorem
⊢ ∀r. is_ring r ⇒ ∀n m. r.RM n m = r.RM m n
[mult_zero_left] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RM r.R0 n = r.R0
[mult_zero_right] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RM n r.R0 = r.R0
[neg_mult] Theorem
⊢ ∀r. is_ring r ⇒ ∀a b. r.RM (r.RN a) b = r.RN (r.RM a b)
[opp_def] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RP n (r.RN n) = r.R0
[plus_assoc] Theorem
⊢ ∀r. is_ring r ⇒ ∀n m p. r.RP n (r.RP m p) = r.RP (r.RP n m) p
[plus_sym] Theorem
⊢ ∀r. is_ring r ⇒ ∀n m. r.RP n m = r.RP m n
[plus_zero_left] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RP r.R0 n = n
[plus_zero_right] Theorem
⊢ ∀r. is_ring r ⇒ ∀n. r.RP n r.R0 = n
[ring_11] Theorem
⊢ ∀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] Theorem
⊢ ∀f.
∃fn.
∀a0 a1 a2 a3 a4.
fn (ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4
[ring_accessors] Theorem
⊢ (∀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] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ 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] Theorem
⊢ ∀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] Theorem
⊢ (∀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] Theorem
⊢ (∀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] Theorem
⊢ ((∀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] Theorem
⊢ (∀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] Theorem
⊢ ((∀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_induction] Theorem
⊢ ∀P. (∀a a0 f f0 f1. P (ring a a0 f f0 f1)) ⇒ ∀r. P r
[ring_is_semi_ring] Theorem
⊢ ∀r. is_ring r ⇒ is_semi_ring (semi_ring_of r)
[ring_literal_11] Theorem
⊢ ∀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] Theorem
⊢ ∀r.
∃a0 a f1 f0 f.
r = <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
[ring_nchotomy] Theorem
⊢ ∀rr. ∃a a0 f f0 f1. rr = ring a a0 f f0 f1
[ring_updates_eq_literal] Theorem
⊢ ∀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|>
*)
end
HOL 4, Kananaskis-13