Theory SML_Rings
section‹Relativization of the results about rings›
theory SML_Rings
imports
SML_Semirings
Complex_Main
begin
subsection‹Rings›
subsubsection‹Definitions and common properties›
locale ring_ow =
semiring_ow U plus times + ab_group_add_ow U plus zero minus uminus
for U :: "'ag set" and plus zero minus uminus times
begin
sublocale semiring_0_cancel_ow ..
end
lemma ring_ow: "class.ring = ring_ow UNIV"
unfolding class.ring_def ring_ow_def ab_group_add_ow semiring_ow
by (simp add: conj_commute)
lemma ring_ow_UNIV_axioms: "ring_ow (UNIV::'a::ring set) (+) 0 (-) uminus (*)"
by (fold ring_ow) (rule ring_class.ring_axioms)
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
lemma ring_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"(
(A ===> A ===> A) ===>
A ===>
(A ===> A ===> A) ===>
(A ===> A) ===>
(A ===> A ===> A) ===>
(=)
)
(ring_ow (Collect (Domainp A))) class.ring"
unfolding ring_ow_def class.ring_def
apply transfer_prover_start
apply transfer_step+
by blast
end
subsubsection‹Relativization›
context ring_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting ring_ow_axioms and zero.not_empty
applying
[
OF
plus_closed'
zero_closed
minus_closed'
add.inverse_closed''
times_closed'
]
begin
tts_lemma right_diff_distrib:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "a *⇩o⇩w (b -⇩o⇩w c) = a *⇩o⇩w b -⇩o⇩w a *⇩o⇩w c"
is Rings.ring_class.right_diff_distrib.
tts_lemma minus_mult_commute:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w a *⇩o⇩w b = a *⇩o⇩w -⇩o⇩w b"
is Rings.ring_class.minus_mult_commute.
tts_lemma left_diff_distrib:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "(a -⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c -⇩o⇩w b *⇩o⇩w c"
is Rings.ring_class.left_diff_distrib.
tts_lemma mult_minus_right:
assumes "a ∈ U" and "b ∈ U"
shows "a *⇩o⇩w -⇩o⇩w b = -⇩o⇩w (a *⇩o⇩w b)"
is Rings.ring_class.mult_minus_right.
tts_lemma minus_mult_right:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w (a *⇩o⇩w b) = a *⇩o⇩w -⇩o⇩w b"
is Rings.ring_class.minus_mult_right.
tts_lemma minus_mult_minus:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w a *⇩o⇩w -⇩o⇩w b = a *⇩o⇩w b"
is Rings.ring_class.minus_mult_minus.
tts_lemma mult_minus_left:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w a *⇩o⇩w b = -⇩o⇩w (a *⇩o⇩w b)"
is Rings.ring_class.mult_minus_left.
tts_lemma minus_mult_left:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w (a *⇩o⇩w b) = -⇩o⇩w a *⇩o⇩w b"
is Rings.ring_class.minus_mult_left.
tts_lemma ring_distribs:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows
"a *⇩o⇩w (b +⇩o⇩w c) = a *⇩o⇩w b +⇩o⇩w a *⇩o⇩w c"
"(a +⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c +⇩o⇩w b *⇩o⇩w c"
"(a -⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c -⇩o⇩w b *⇩o⇩w c"
"a *⇩o⇩w (b -⇩o⇩w c) = a *⇩o⇩w b -⇩o⇩w a *⇩o⇩w c"
is Rings.ring_class.ring_distribs.
tts_lemma eq_add_iff2:
assumes "a ∈ U" and "e ∈ U" and "c ∈ U" and "b ∈ U" and "d ∈ U"
shows "(a *⇩o⇩w e +⇩o⇩w c = b *⇩o⇩w e +⇩o⇩w d) = (c = (b -⇩o⇩w a) *⇩o⇩w e +⇩o⇩w d)"
is Rings.ring_class.eq_add_iff2.
tts_lemma eq_add_iff1:
assumes "a ∈ U" and "e ∈ U" and "c ∈ U" and "b ∈ U" and "d ∈ U"
shows "(a *⇩o⇩w e +⇩o⇩w c = b *⇩o⇩w e +⇩o⇩w d) = ((a -⇩o⇩w b) *⇩o⇩w e +⇩o⇩w c = d)"
is Rings.ring_class.eq_add_iff1.
tts_lemma mult_diff_mult:
assumes "x ∈ U" and "y ∈ U" and "a ∈ U" and "b ∈ U"
shows "x *⇩o⇩w y -⇩o⇩w a *⇩o⇩w b = x *⇩o⇩w (y -⇩o⇩w b) +⇩o⇩w (x -⇩o⇩w a) *⇩o⇩w b"
is Real.mult_diff_mult.
end
end
subsection‹Commutative rings›
subsubsection‹Definitions and common properties›
locale comm_ring_ow =
comm_semiring_ow U plus times + ab_group_add_ow U plus zero minus uminus
for U :: "'ag set" and plus zero minus uminus times
begin
sublocale ring_ow ..
sublocale comm_semiring_0_cancel_ow ..
end
lemma comm_ring_ow: "class.comm_ring = comm_ring_ow UNIV"
unfolding
class.comm_ring_def comm_ring_ow_def
ab_group_add_ow comm_semiring_ow
by (simp add: conj_commute)
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
lemma comm_ring_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"(
(A ===> A ===> A) ===>
A ===>
(A ===> A ===> A) ===>
(A ===> A) ===>
(A ===> A ===> A) ===>
(=)
)
(comm_ring_ow (Collect (Domainp A))) class.comm_ring"
unfolding comm_ring_ow_def class.comm_ring_def
apply transfer_prover_start
apply transfer_step+
by blast
end
subsubsection‹Relativization›
context comm_ring_ow
begin
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting comm_ring_ow_axioms and zero.not_empty
applying
[
OF
plus_closed'
zero_closed
minus_closed'
add.inverse_closed''
times_closed'
]
begin
tts_lemma square_diff_square_factored:
assumes "x ∈ U" and "y ∈ U"
shows "x *⇩o⇩w x -⇩o⇩w y *⇩o⇩w y = (x +⇩o⇩w y) *⇩o⇩w (x -⇩o⇩w y)"
is comm_ring_class.square_diff_square_factored.
end
end
subsection‹Rings with identity›
subsubsection‹Definitions and common properties›
locale ring_1_ow =
ring_ow U plus zero minus uminus times +
zero_neq_one_ow U one zero +
monoid_mult_ow U one times
for U :: "'ag set" and one times plus zero minus uminus
begin
sublocale semiring_1_cancel_ow ..
end
lemma ring_1_ow: "class.ring_1 = ring_1_ow UNIV"
unfolding
class.ring_1_def ring_1_ow_def monoid_mult_ow ring_ow zero_neq_one_ow
by (force simp: conj_commute)
lemma ring_1_ow_UNIV_axioms:
"ring_1_ow (UNIV::'a::ring_1 set) 1 (*) (+) 0 (-) uminus"
by (fold ring_1_ow) (rule ring_1_class.ring_1_axioms)
ud ‹ring_1.iszero› (‹(with _ : «iszero» _)› [1000, 1000] 10)
ud iszero' ‹iszero›
ud ‹ring_1.of_int›
(‹(with _ _ _ _ : «of'_int» _)› [1000, 999, 998, 997, 1000] 10)
ud of_int' ‹of_int›
ud ‹ring_1.Ints› (‹(with _ _ _ _ : ℤ)› [1000, 999, 998, 997] 10)
ud Ints' ‹Ints›
ud ‹diffs› (‹(with _ _ _ _ : «diffs» _)› [1000, 999, 998, 997, 1000] 10)
ctr parametricity
in iszero_ow: iszero.with_def
and of_int_ow: of_int.with_def
and Ints_ow: Ints.with_def
and diffs_ow: diffs.with_def
context ring_1_ow
begin
abbreviation iszero where "iszero ≡ iszero.with 0⇩o⇩w"
abbreviation of_int where "of_int ≡ of_int.with 1⇩o⇩w (+⇩o⇩w) 0⇩o⇩w (-⇩o⇩w)"
abbreviation Ints (‹«ℤ»›) where "«ℤ» ≡ Ints.with 1⇩o⇩w (+⇩o⇩w) 0⇩o⇩w (-⇩o⇩w)"
notation Ints (‹«ℤ»›)
end
context ring_1
begin
lemma Int_ss_UNIV: "ℤ ⊆ UNIV" by simp
end
subsubsection‹Transfer rules›
context
includes lifting_syntax
begin
lemma ring_1_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"(
A ===>
(A ===> A ===> A) ===>
(A ===> A ===> A) ===>
A ===>
(A ===> A ===> A) ===>
(A ===> A) ===>
(=)
)
(ring_1_ow (Collect (Domainp A))) class.ring_1"
unfolding ring_1_ow_def class.ring_1_def
apply transfer_prover_start
apply transfer_step+
by blast
end
subsubsection‹Relativization›
declare dvd.with[ud_with del]
declare dvd'.with[ud_with del]
context ring_1_ow
begin
tts_context
tts: (?'a to U)
substituting ring_1_ow_axioms and zero.not_empty
eliminating through simp
begin
tts_lemma Int_ss_UNIV[simp]: "«ℤ» ⊆ U"
is Int_ss_UNIV.
end
lemma Int_closed[simp,intro]: "a ∈ «ℤ» ⟹ a ∈ U" using Int_ss_UNIV by blast
tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting ring_1_ow_axioms and zero.not_empty
eliminating through