Theory Missing_Ring
section ‹Missing Ring›
text ‹This theory contains several lemmas which might be of interest to the Isabelle distribution.›
theory Missing_Ring
imports
"Missing_Misc"
"HOL-Algebra.Ring"
begin
context ordered_cancel_semiring
begin
subclass ordered_cancel_ab_semigroup_add ..
end
text ‹partially ordered variant›
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
assumes mult_strict_right_mono: "a < b ⟹ 0 < c ⟹ a * c < b * c"
begin
subclass semiring_0_cancel ..
subclass ordered_semiring
proof
fix a b c :: 'a
assume A: "a ≤ b" "0 ≤ c"
from A show "c * a ≤ c * b"
unfolding le_less
using mult_strict_left_mono by (cases "c = 0") auto
from A show "a * c ≤ b * c"
unfolding le_less
using mult_strict_right_mono by (cases "c = 0") auto
qed
lemma mult_pos_pos[simp]: "0 < a ⟹ 0 < b ⟹ 0 < a * b"
using mult_strict_left_mono [of 0 b a] by simp
lemma mult_pos_neg: "0 < a ⟹ b < 0 ⟹ a * b < 0"
using mult_strict_left_mono [of b 0 a] by simp
lemma mult_neg_pos: "a < 0 ⟹ 0 < b ⟹ a * b < 0"
using mult_strict_right_mono [of a 0 b] by simp
text ‹Legacy - use ‹mult_neg_pos››
lemma mult_pos_neg2: "0 < a ⟹ b < 0 ⟹ b * a < 0"
by (drule mult_strict_right_mono [of b 0], auto)
text‹Strict monotonicity in both arguments›
lemma mult_strict_mono:
assumes "a < b" and "c < d" and "0 < b" and "0 ≤ c"
shows "a * c < b * d"
using assms apply (cases "c=0")
apply (simp)
apply (erule mult_strict_right_mono [THEN less_trans])
apply (force simp add: le_less)
apply (erule mult_strict_left_mono, assumption)
done
text‹This weaker variant has more natural premises›
lemma mult_strict_mono':
assumes "a < b" and "c < d" and "0 ≤ a" and "0 ≤ c"
shows "a * c < b * d"
by (rule mult_strict_mono) (insert assms, auto)
lemma mult_less_le_imp_less:
assumes "a < b" and "c ≤ d" and "0 ≤ a" and "0 < c"
shows "a * c < b * d"
using assms apply (subgoal_tac "a * c < b * c")
apply (erule less_le_trans)
apply (erule mult_left_mono)
apply simp
apply (erule mult_strict_right_mono)
apply assumption
done
lemma mult_le_less_imp_less:
assumes "a ≤ b" and "c < d" and "0 < a" and "0 ≤ c"
shows "a * c < b * d"
using assms apply (subgoal_tac "a * c ≤ b * c")
apply (erule le_less_trans)
apply (erule mult_strict_left_mono)
apply simp
apply (erule mult_right_mono)
apply simp
done
end
class ordered_idom = idom + ordered_semiring_strict +
assumes zero_less_one [simp]: "0 < 1" begin
subclass semiring_1 ..
subclass comm_ring_1 ..
subclass ordered_ring ..
subclass ordered_comm_semiring by(unfold_locales, fact mult_left_mono)
subclass ordered_ab_semigroup_add ..
lemma of_nat_ge_0[simp]: "of_nat x ≥ 0"
proof (induct x)
case 0 thus ?case by auto
next case (Suc x)
hence "0 ≤ of_nat x" by auto
also have "of_nat x < of_nat (Suc x)" by auto
finally show ?case by auto
qed
lemma of_nat_eq_0[simp]: "of_nat x = 0 ⟷ x = 0"
proof(induct x,simp)
case (Suc x)
have "of_nat (Suc x) > 0" apply(rule le_less_trans[of _ "of_nat x"]) by auto
thus ?case by auto
qed
lemma inj_of_nat: "inj (of_nat :: nat ⇒ 'a)"
proof(rule injI)
fix x y show "of_nat x = of_nat y ⟹ x = y"
proof (induct x arbitrary: y)
case 0 thus ?case
proof (induct y)
case 0 thus ?case by auto
next case (Suc y)
hence "of_nat (Suc y) = 0" by auto
hence "Suc y = 0" unfolding of_nat_eq_0 by auto
hence False by auto
thus ?case by auto
qed
next case (Suc x)
thus ?case
proof (induct y)
case 0
hence "of_nat (Suc x) = 0" by auto
hence "Suc x = 0" unfolding of_nat_eq_0 by auto
hence False by auto
thus ?case by auto
next case (Suc y) thus ?case by auto
qed
qed
qed
subclass ring_char_0 by(unfold_locales, fact inj_of_nat)
end
context comm_monoid
begin
lemma finprod_reindex_bij_betw: "bij_betw h S T
⟹ g ∈ h ` S → carrier G
⟹ finprod G (λx. g (h x)) S = finprod G g T"
using finprod_reindex[of g h S] unfolding bij_betw_def by auto
lemma finprod_reindex_bij_witness:
assumes witness:
"⋀a. a ∈ S ⟹ i (j a) = a"
"⋀a. a ∈ S ⟹ j a ∈ T"
"⋀b. b ∈ T ⟹ j (i b) = b"
"⋀b. b ∈ T ⟹ i b ∈ S"
assumes eq:
"⋀a. a ∈ S ⟹ h (j a) = g a"
assumes g: "g ∈ S → carrier G"
and h: "h ∈ j ` S → carrier G"
shows "finprod G g S = finprod G h T"
proof -
have b: "bij_betw j S T"
using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
have fp: "finprod G g S = finprod G (λx. h (j x)) S"
by (rule finprod_cong, insert eq g, auto)
show ?thesis
using finprod_reindex_bij_betw[OF b h] unfolding fp .
qed
end
lemmas (in abelian_monoid) finsum_reindex_bij_witness = add.finprod_reindex_bij_witness
locale csemiring = semiring + comm_monoid R
context cring
begin
sublocale csemiring ..
end
lemma (in comm_monoid) finprod_one':
"(⋀ a. a ∈ A ⟹ f a = 𝟭) ⟹ finprod G f A = 𝟭"
by (induct A rule: infinite_finite_induct, auto)
lemma (in comm_monoid) finprod_split:
"finite A ⟹ f ` A ⊆ carrier G ⟹ a ∈ A ⟹ finprod G f A = f a ⊗ finprod G f (A - {a})"
by (rule trans[OF trans[OF _ finprod_Un_disjoint[of "{a}" "A - {a}" f]]], auto,
rule arg_cong[of _ _ "finprod G f"], auto)
lemma (in comm_monoid) finprod_finprod:
"finite A ⟹ finite B ⟹ (⋀ a b. a ∈ A ⟹ b ∈ B ⟹ g a b ∈ carrier G) ⟹
finprod G (λ a. finprod G (g a) B) A = finprod G (λ (a,b). g a b) (A × B)"
proof (induct A rule: finite_induct)
case (insert a' A)
note IH = this
let ?l = "(⨂a∈insert a' A. finprod G (g a) B)"
let ?r = "(⨂a∈insert a' A × B. case a of (a, b) ⇒ g a b)"
have "?l = finprod G (g a') B ⊗ (⨂a∈A. finprod G (g a) B)"
using IH by simp
also have "(⨂a∈A. finprod G (g a) B) = finprod G (λ (a,b). g a b) (A × B)"
by (rule IH(3), insert IH, auto)
finally have idl: "?l = finprod G (g a') B ⊗ finprod G (λ (a,b). g a b) (A × B)" .
from IH(2) have "insert a' A × B = {a'} × B ∪ A × B" by auto
hence "?r = (⨂a∈{a'} × B ∪ A × B. case a of (a, b) ⇒ g a b)" by simp
also have "… = (⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) ⊗ (⨂a∈ A × B. case a of (a, b) ⇒ g a b)"
by (rule finprod_Un_disjoint, insert IH, auto)
also have "(⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) = finprod G (g a') B"
using IH(4) IH(5)
proof (induct B rule: finite_induct)
case (insert b' B)
note IH = this
have id: "(⨂a∈{a'} × B. case a of (a, b) ⇒ g a b) = finprod G (g a') B"
by (rule IH(3)[OF IH(4)], auto)
have id2: "⋀ x F. {a'} × insert x F = insert (a',x) ({a'} × F)" by auto
have id3: "(⨂a∈insert (a', b') ({a'} × B). case a of (a, b) ⇒ g a b)
= g a' b' ⊗ (⨂a∈({a'} × B). case a of (a, b) ⇒ g a b)"
by (rule trans[OF finprod_insert], insert IH, auto)
show ?case unfolding id2 id3 id
by (rule sym, rule finprod_insert, insert IH, auto)
qed simp
finally have idr: "?r = finprod G (g a') B ⊗ (⨂a∈A × B. case a of (a, b) ⇒ g a b)" .
show ?case unfolding idl idr ..
qed simp
lemma (in comm_monoid) finprod_swap:
assumes "finite A" "finite B" "⋀ a b. a ∈ A ⟹ b ∈ B ⟹ g a b ∈ carrier G"
shows "finprod G (λ (b,a). g a b) (B × A) = finprod G (λ (a,b). g a b) (A × B)"
proof -
have [simp]: "(λ(a, b). (b, a)) ` (A × B) = B × A" by auto
have [simp]: "(λ x. case case x of (a, b) ⇒ (b, a) of (a, b) ⇒ g b a) = (λ (a,b). g a b)"
by (intro ext, auto)
show ?thesis
by (rule trans[OF trans[OF _ finprod_reindex[of "λ (a,b). g b a" "λ (a,b). (b,a)"]]],
insert assms, auto simp: inj_on_def)
qed
lemma (in comm_monoid) finprod_finprod_swap:
"finite A ⟹ finite B ⟹ (⋀ a b. a ∈ A ⟹ b ∈ B ⟹ g a b ∈ carrier G) ⟹
finprod G (λ a. finprod G (g a) B) A = finprod G (λ b. finprod G (λ a. g a b) A) B"
using finprod_finprod[of A B] finprod_finprod[of B A] finprod_swap[of A B]
by simp
lemmas (in semiring) finsum_zero' = add.finprod_one'
lemmas (in semiring) finsum_split = add.finprod_split
lemmas (in semiring) finsum_finsum_swap = add.finprod_finprod_swap
lemma (in csemiring) finprod_zero:
"finite A ⟹ f ∈ A → carrier R ⟹ ∃a∈A. f a = 𝟬
⟹ finprod R f A = 𝟬"
proof (induct A rule: finite_induct)
case (insert a A)
from finprod_insert[OF insert(1-2), of f] insert(4)
have ins: "finprod R f (insert a A) = f a ⊗ finprod R f A" by simp
have fA: "finprod R f A ∈ carrier R"
by (rule finprod_closed, insert insert, auto)
show ?case
proof (cases "f a = 𝟬")
case True
with fA show ?thesis unfolding ins by simp
next
case False
with insert(5) have "∃ a ∈ A. f a = 𝟬" by auto
from insert(3)[OF _ this] insert have "finprod R f A = 𝟬" by auto
with insert show ?thesis unfolding ins by auto
qed
qed simp
lemma (in semiring) finsum_product:
assumes A: "finite A" and B: "finite B"
and f: "f ∈ A → carrier R" and g: "g ∈ B → carrier R"
shows "finsum R f A ⊗ finsum R g B = (⨁i∈A. ⨁j∈B. f i ⊗ g j)"
unfolding finsum_ldistr[OF A finsum_closed[OF g] f]
proof (rule finsum_cong'[OF refl])
fix a
assume a: "a ∈ A"
show "f a ⊗ finsum R g B = (⨁j∈B. f a ⊗ g j)"
by (rule finsum_rdistr[OF B _ g], insert a f, auto)
qed (insert f g B, auto intro: finsum_closed)
lemma (in semiring) Units_one_side_I:
"a ∈ carrier R ⟹ p ∈ Units R ⟹ p ⊗ a = 𝟭 ⟹ a ∈ Units R"
"a ∈ carrier R ⟹ p ∈ Units R ⟹ a ⊗ p = 𝟭 ⟹ a ∈ Units R"
by (metis Units_closed Units_inv_Units Units_l_inv inv_unique)+
lemma permutes_funcset: "p permutes A ⟹ (p ` A → B) = (A → B)"
by (simp add: permutes_image)
context comm_monoid
begin
lemma finprod_permute:
assumes p: "p permutes S"
and f: "f ∈ S → carrier G"
shows "finprod G f S = finprod G (f ∘ p) S"
proof -
from ‹p permutes S› have "inj p"
by (rule permutes_inj)
then have "inj_on p S"
by (auto intro: subset_inj_on)
from finprod_reindex[OF _ this, unfolded permutes_image[OF p], OF f]
show ?thesis unfolding o_def .
qed
lemma finprod_singleton_set[simp]: assumes "f a ∈ carrier G"
shows "finprod G f {a} = f a"
proof -
have "finprod G f {a} = f a ⊗ finprod G f {}"
by (rule finprod_insert, insert assms, auto)
also have "… = f a" using assms by auto
finally show ?thesis .
qed
end
lemmas (in semiring) finsum_permute = add.finprod_permute
lemmas (in semiring) finsum_singleton_set = add.finprod_singleton_set
context cring
begin
lemma finsum_permutations_inverse:
assumes f: "f ∈ {p. p permutes S} → carrier R"
shows "finsum R f {p. p permutes S} = finsum R (λp. f(Hilbert_Choice.inv p)) {p. p permutes S}"
(is "?lhs = ?rhs")
proof -
let ?inv = "Hilbert_Choice.inv"
let ?S = "{p . p permutes S}"
have th0: "inj_on ?inv ?S"
proof (auto simp add: inj_on_def)
fix q r
assume q: "q permutes S"
and r: "r permutes S"
and qr: "?inv q = ?inv r"
then have "?inv (?inv q) = ?inv (?inv r)"
by simp
with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
by metis
qed
have th1: "?inv ` ?S = ?S"
using image_inverse_permutations by blast
have th2: "?rhs = finsum R (f ∘ ?inv) ?S"
by (simp add: o_def)
from finsum_reindex[OF _ th0, of f] show ?thesis unfolding th1 th2 using f .
qed
lemma finsum_permutations_compose_right: assumes q: "q permutes S"
and *: "f ∈ {p. p permutes S} → carrier R"
shows "finsum R f {p. p permutes S} = finsum R (λp. f(p ∘ q)) {p. p permutes S}"
(is "?lhs = ?rhs")
proof -
let ?S = "{p. p permutes S}"
let ?inv = "Hilbert_Choice.inv"
have th0: "?rhs = finsum R (f ∘ (λp. p ∘ q)) ?S"
by (simp add: o_def)
have th1: "inj_on (λp. p ∘ q) ?S"
proof (auto simp add: inj_on_def)
fix p r
assume "p permutes S"
and r: "r permutes S"
and rp: "p ∘ q = r ∘ q"
then have "p ∘ (q ∘ ?inv q) = r ∘ (q ∘ ?inv q)"
by (simp add: o_assoc)
with permutes_surj[OF q, unfolded surj_iff] show "p = r"
by simp
qed
have th3: "(λp. p ∘ q) ` ?S = ?S"
using image_compose_permutations_right[OF q] by auto
from finsum_reindex[OF _ th1, of f]
show ?thesis unfolding th0 th1 th3 using * .
qed
end
end