Theory Field_Of_Fractions
section ‹The field of fractions of an integral domain›
theory Field_Of_Fractions
imports Divisibility_Theory
begin
text ‹Given an integral domain ‹R› we construct its field of fractions as a carrier-set object,
mirroring the elementary construction of ‹ℚ› from ‹ℤ›: fractions are pairs ‹(a, b)› with
‹b ≠ 𝟬›, identified when they cross-multiply equal, and the field operations are the usual ones
on numerators and denominators. We reuse the @{locale Equivalence} machinery of
‹Set_Theory› for the quotient, then interpret @{locale Field} on it. The
canonical map ‹a ↦ a / 𝟭› is an injective ring homomorphism, giving the universal embedding
of the domain into a field.›
context integral_domain
begin
subsection ‹Fractions and their equivalence›
text ‹A fraction is a pair of ring elements with nonzero denominator.›
definition frac_set :: "('a × 'a) set"
where "frac_set = {(a, b). a ∈ R ∧ b ∈ R ∧ b ≠ 𝟬}"
lemma frac_setI [intro]: "⟦ a ∈ R; b ∈ R; b ≠ 𝟬 ⟧ ⟹ (a, b) ∈ frac_set"
unfolding frac_set_def by blast
lemma frac_setD [dest]: "(a, b) ∈ frac_set ⟹ a ∈ R ∧ b ∈ R ∧ b ≠ 𝟬"
unfolding frac_set_def by blast
text ‹The denominator of a fraction is a nonzero ring element; the product of two nonzero
denominators is again nonzero (no zero divisors).›
lemma frac_mult_denom_nonzero [intro]:
"⟦ b ∈ R; d ∈ R; b ≠ 𝟬; d ≠ 𝟬 ⟧ ⟹ b ⋅ d ≠ 𝟬"
using no_zero_divisors by blast
text ‹Cross-multiplication equivalence: ‹(a, b) ∼ (c, d)› iff ‹a ⋅ d = c ⋅ b›.›
definition frac_rel :: "(('a × 'a) × ('a × 'a)) set"
where "frac_rel = {((a, b), (c, d)). (a, b) ∈ frac_set ∧ (c, d) ∈ frac_set ∧ a ⋅ d = c ⋅ b}"
lemma frac_relI [intro]:
"⟦ (a, b) ∈ frac_set; (c, d) ∈ frac_set; a ⋅ d = c ⋅ b ⟧ ⟹ ((a, b), (c, d)) ∈ frac_rel"
unfolding frac_rel_def by blast
lemma frac_relE:
assumes "((a, b), (c, d)) ∈ frac_rel"
obtains "(a, b) ∈ frac_set" "(c, d) ∈ frac_set" "a ⋅ d = c ⋅ b"
using assms unfolding frac_rel_def by blast
text ‹Transitivity is where cancellation --- hence the domain hypothesis --- is used.›
lemma frac_rel_trans:
assumes 1: "((a, b), (c, d)) ∈ frac_rel" and 2: "((c, d), (e, f)) ∈ frac_rel"
shows "((a, b), (e, f)) ∈ frac_rel"
proof -
from 1 obtain ab: "(a, b) ∈ frac_set" and cd: "(c, d) ∈ frac_set" and e1: "a ⋅ d = c ⋅ b"
by (rule frac_relE)
from 2 obtain ef: "(e, f) ∈ frac_set" and e2: "c ⋅ f = e ⋅ d" by (rule frac_relE)
from ab cd ef have [simp]: "a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "e ∈ R" "f ∈ R"
and dnz: "d ≠ 𝟬" by auto
have "d ⋅ (a ⋅ f) = (a ⋅ d) ⋅ f" by (simp add: mult_ac)
also have "… = (c ⋅ b) ⋅ f" by (simp add: e1)
also have "… = (c ⋅ f) ⋅ b" by (simp add: mult_ac)
also have "… = (e ⋅ d) ⋅ b" by (simp add: e2)
also have "… = d ⋅ (e ⋅ b)" by (simp add: mult_ac)
finally have eq: "d ⋅ (a ⋅ f) = d ⋅ (e ⋅ b)" .
have "a ⋅ f = e ⋅ b"
by (rule mult_cancel_left[where c = d]) (use dnz eq in simp_all)
with ab ef show ?thesis by (rule frac_relI)
qed
text ‹The relation is an equivalence on the set of fractions.›
interpretation frac: Equivalence frac_set frac_rel
proof (rule equivalenceI)
show "frac_rel ⊆ frac_set × frac_set" by (auto simp: frac_rel_def)
next
fix x assume "x ∈ frac_set"
then show "(x, x) ∈ frac_rel" by (cases x) (auto simp: frac_rel_def)
next
fix x y assume "(x, y) ∈ frac_rel"
then show "(y, x) ∈ frac_rel" by (cases x; cases y) (auto simp: frac_rel_def)
next
fix x y z assume "(x, y) ∈ frac_rel" "(y, z) ∈ frac_rel"
then show "(x, z) ∈ frac_rel"
by (cases x; cases y; cases z) (blast intro: frac_rel_trans)
qed
subsection ‹The carrier and class equality›
text ‹The carrier of the field of fractions: the set of equivalence classes.›
abbreviation Fractions :: "('a × 'a) set set"
where "Fractions ≡ frac_set / frac_rel"
text ‹Class equality is cross-multiplication.›
lemma frac_eqI:
assumes "(a, b) ∈ frac_set" "(c, d) ∈ frac_set" "a ⋅ d = c ⋅ b"
shows "frac.Class (a, b) = frac.Class (c, d)"
using assms by (intro frac.Class_eq frac_relI)
lemma frac_eqD:
assumes "(a, b) ∈ frac_set" "(c, d) ∈ frac_set" "frac.Class (a, b) = frac.Class (c, d)"
shows "a ⋅ d = c ⋅ b"
using assms frac.Class_equivalence by (blast elim: frac_relE)
text ‹A class lies in the carrier exactly when it is the class of a fraction.›
lemma Class_in_Fractions [intro, simp]: "(a, b) ∈ frac_set ⟹ frac.Class (a, b) ∈ Fractions"
by (rule frac.Class_in_Partition)
lemma Fractions_cases:
assumes "A ∈ Fractions" obtains a b where "(a, b) ∈ frac_set" "A = frac.Class (a, b)"
using assms frac.representant_exists by (metis surj_pair)
text ‹A class equals the zero-class ‹Class (𝟬, 𝟭)› iff any (equivalently every) numerator is zero.
Later, we take ‹Class (𝟬, 𝟭)› as the additive unit and ‹Class (𝟭, 𝟭)› as the multiplicative unit
of ‹Fractions›.›
lemma frac_Class_zero_iff:
assumes ab: "(a, b) ∈ frac_set"
shows "frac.Class (a, b) = frac.Class (𝟬, 𝟭) ⟷ a = 𝟬"
proof
from ab have aR: "a ∈ R" and bR: "b ∈ R" by auto
have zero_in: "(𝟬, 𝟭) ∈ frac_set" by (auto intro!: frac_setI simp: nontrivial)
assume "frac.Class (a, b) = frac.Class (𝟬, 𝟭)"
from frac_eqD[OF ab zero_in this] show "a = 𝟬" using aR bR by simp
next
assume "a = 𝟬"
with ab show "frac.Class (a, b) = frac.Class (𝟬, 𝟭)"
by (intro frac_eqI) (auto intro!: frac_setI simp: nontrivial)
qed
subsection ‹The operations on classes›
text ‹We define addition, multiplication, negation, and inversion on classes by picking any
representative and applying the elementary fraction formulas. For each operation we prove a
congruence lemma (well-definedness under the equivalence) and a ‹Class›-formula giving the
computation on a canonical representative.›
definition frac_add :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
(infixl ‹[+]› 65)
where "A [+] B =
(let (a, b) = SOME p. p ∈ A ∧ p ∈ frac_set;
(c, d) = SOME p. p ∈ B ∧ p ∈ frac_set
in frac.Class (a ⋅ d + c ⋅ b, b ⋅ d))"
definition frac_mult :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
(infixl ‹[⋅]› 70)
where "A [⋅] B =
(let (a, b) = SOME p. p ∈ A ∧ p ∈ frac_set;
(c, d) = SOME p. p ∈ B ∧ p ∈ frac_set
in frac.Class (a ⋅ c, b ⋅ d))"
definition frac_neg :: "('a × 'a) set ⇒ ('a × 'a) set" (‹[-] _› [80] 80)
where "[-] A = (let (a, b) = SOME p. p ∈ A ∧ p ∈ frac_set in frac.Class (- a, b))"
text ‹Inversion is only used on nonzero classes.›
definition frac_inv :: "('a × 'a) set ⇒ ('a × 'a) set"
where "frac_inv A = (let (a, b) = SOME p. p ∈ A ∧ p ∈ frac_set in frac.Class (b, a))"
text ‹The zero and unit of the fraction field.›
abbreviation frac_zero :: "('a × 'a) set" (‹[𝟬]›)
where "[𝟬] ≡ frac.Class (𝟬, 𝟭)"
abbreviation frac_one :: "('a × 'a) set" (‹[𝟭]›)
where "[𝟭] ≡ frac.Class (𝟭, 𝟭)"
lemma one_in_frac_set: "(𝟭, 𝟭) ∈ frac_set"
by (rule frac_setI) (auto simp: nontrivial)
lemma zero_in_frac_set: "(𝟬, 𝟭) ∈ frac_set"
by (rule frac_setI) (auto simp: nontrivial)
lemma frac_zero_in [intro, simp]: "[𝟬] ∈ Fractions"
using zero_in_frac_set by (rule Class_in_Fractions)
lemma frac_one_in [intro, simp]: "[𝟭] ∈ Fractions"
using one_in_frac_set by (rule Class_in_Fractions)
lemma frac_one_neq_zero: "[𝟭] ≠ [𝟬]"
proof
assume eq: "[𝟭] = [𝟬]"
from frac_eqD[OF one_in_frac_set zero_in_frac_set eq] show False using nontrivial by simp
qed
subsubsection ‹Representative selection›
text ‹Any class of a fraction contains that fraction.›
lemma rep_in_frac_set:
assumes "(a, b) ∈ frac_set"
shows "(SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set) ∈ frac.Class (a, b) ∧
(SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set) ∈ frac_set"
proof (rule someI_ex)
from assms have "(a, b) ∈ frac.Class (a, b)" by (intro frac.Class_self)
with assms show "∃p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set" by blast
qed
subsubsection ‹Congruence: well-definedness under the equivalence›
lemma frac_add_cong:
assumes r1: "((a, b), (a', b')) ∈ frac_rel" and r2: "((c, d), (c', d')) ∈ frac_rel"
shows "((a ⋅ d + c ⋅ b, b ⋅ d), (a' ⋅ d' + c' ⋅ b', b' ⋅ d')) ∈ frac_rel"
proof -
from r1 obtain ab: "(a, b) ∈ frac_set" and ab': "(a', b') ∈ frac_set" and e1: "a ⋅ b' = a' ⋅ b"
by (rule frac_relE)
from r2 obtain cd: "(c, d) ∈ frac_set" and cd': "(c', d') ∈ frac_set" and e2: "c ⋅ d' = c' ⋅ d"
by (rule frac_relE)
from ab ab' cd cd' have [simp]:
"a ∈ R" "b ∈ R" "a' ∈ R" "b' ∈ R" "c ∈ R" "d ∈ R" "c' ∈ R" "d' ∈ R"
and bnz: "b ≠ 𝟬" and b'nz: "b' ≠ 𝟬" and dnz: "d ≠ 𝟬" and d'nz: "d' ≠ 𝟬" by auto
have step1: "(a ⋅ d + c ⋅ b) ⋅ (b' ⋅ d') = (a ⋅ b') ⋅ (d ⋅ d') + (c ⋅ d') ⋅ (b ⋅ b')"
proof -
have "(a ⋅ d + c ⋅ b) ⋅ (b' ⋅ d') = (a ⋅ d) ⋅ (b' ⋅ d') + (c ⋅ b) ⋅ (b' ⋅ d')"
by (simp add: distributive)
also have "(a ⋅ d) ⋅ (b' ⋅ d') = (a ⋅ b') ⋅ (d ⋅ d')" by (simp add: mult_ac)
also have "(c ⋅ b) ⋅ (b' ⋅ d') = (c ⋅ d') ⋅ (b ⋅ b')" by (simp add: mult_ac)
finally show ?thesis .
qed
also have "(a ⋅ b') ⋅ (d ⋅ d') + (c ⋅ d') ⋅ (b ⋅ b') = (a' ⋅ b) ⋅ (d ⋅ d') + (c' ⋅ d) ⋅ (b ⋅ b')"
by (simp add: e1 e2)
also have "… = (a' ⋅ d' + c' ⋅ b') ⋅ (b ⋅ d)"
proof -
have "(a' ⋅ d' + c' ⋅ b') ⋅ (b ⋅ d) = (a' ⋅ d') ⋅ (b ⋅ d) + (c' ⋅ b') ⋅ (b ⋅ d)"
by (simp add: distributive)
also have "(a' ⋅ d') ⋅ (b ⋅ d) = (a' ⋅ b) ⋅ (d ⋅ d')" by (simp add: mult_ac)
also have "(c' ⋅ b') ⋅ (b ⋅ d) = (c' ⋅ d) ⋅ (b ⋅ b')" by (simp add: mult_ac)
finally show ?thesis by simp
qed
finally have eq: "(a ⋅ d + c ⋅ b) ⋅ (b' ⋅ d') = (a' ⋅ d' + c' ⋅ b') ⋅ (b ⋅ d)" .
have s1: "(a ⋅ d + c ⋅ b, b ⋅ d) ∈ frac_set"
using bnz dnz frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
have s2: "(a' ⋅ d' + c' ⋅ b', b' ⋅ d') ∈ frac_set"
using b'nz d'nz frac_mult_denom_nonzero[of b' d'] by (auto intro!: frac_setI)
from s1 s2 eq show ?thesis by (rule frac_relI)
qed
lemma frac_mult_cong:
assumes r1: "((a, b), (a', b')) ∈ frac_rel" and r2: "((c, d), (c', d')) ∈ frac_rel"
shows "((a ⋅ c, b ⋅ d), (a' ⋅ c', b' ⋅ d')) ∈ frac_rel"
proof -
from r1 obtain ab: "(a, b) ∈ frac_set" and ab': "(a', b') ∈ frac_set" and e1: "a ⋅ b' = a' ⋅ b"
by (rule frac_relE)
from r2 obtain cd: "(c, d) ∈ frac_set" and cd': "(c', d') ∈ frac_set" and e2: "c ⋅ d' = c' ⋅ d"
by (rule frac_relE)
from ab ab' cd cd' have [simp]:
"a ∈ R" "b ∈ R" "a' ∈ R" "b' ∈ R" "c ∈ R" "d ∈ R" "c' ∈ R" "d' ∈ R"
and bnz: "b ≠ 𝟬" and b'nz: "b' ≠ 𝟬" and dnz: "d ≠ 𝟬" and d'nz: "d' ≠ 𝟬" by auto
have "(a ⋅ c) ⋅ (b' ⋅ d') = (a ⋅ b') ⋅ (c ⋅ d')" by (simp add: mult_ac)
also have "… = (a' ⋅ b) ⋅ (c' ⋅ d)" by (simp add: e1 e2)
also have "… = (a' ⋅ c') ⋅ (b ⋅ d)" by (simp add: mult_ac)
finally have eq: "(a ⋅ c) ⋅ (b' ⋅ d') = (a' ⋅ c') ⋅ (b ⋅ d)" .
have s1: "(a ⋅ c, b ⋅ d) ∈ frac_set"
using bnz dnz frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
have s2: "(a' ⋅ c', b' ⋅ d') ∈ frac_set"
using b'nz d'nz frac_mult_denom_nonzero[of b' d'] by (auto intro!: frac_setI)
from s1 s2 eq show ?thesis by (rule frac_relI)
qed
lemma frac_neg_cong:
assumes r: "((a, b), (a', b')) ∈ frac_rel"
shows "((- a, b), (- a', b')) ∈ frac_rel"
proof -
from r obtain ab: "(a, b) ∈ frac_set" and ab': "(a', b') ∈ frac_set" and e: "a ⋅ b' = a' ⋅ b"
by (rule frac_relE)
from ab ab' have [simp]: "a ∈ R" "b ∈ R" "a' ∈ R" "b' ∈ R"
and bnz: "b ≠ 𝟬" and b'nz: "b' ≠ 𝟬" by auto
have "(- a) ⋅ b' = - (a ⋅ b')" by (simp add: left_minus)
also have "… = - (a' ⋅ b)" by (simp add: e)
also have "… = (- a') ⋅ b" by (simp add: left_minus)
finally have eq: "(- a) ⋅ b' = (- a') ⋅ b" .
have s1: "(- a, b) ∈ frac_set" using bnz by (auto intro!: frac_setI)
have s2: "(- a', b') ∈ frac_set" using b'nz by (auto intro!: frac_setI)
from s1 s2 eq show ?thesis by (rule frac_relI)
qed
text ‹Inversion: well-defined provided the numerators are nonzero (i.e.\ the class is nonzero).›
lemma frac_inv_cong:
assumes r: "((a, b), (a', b')) ∈ frac_rel" and anz: "a ≠ 𝟬"
shows "((b, a), (b', a')) ∈ frac_rel"
proof -
from r obtain ab: "(a, b) ∈ frac_set" and ab': "(a', b') ∈ frac_set" and e: "a ⋅ b' = a' ⋅ b"
by (rule frac_relE)
from ab ab' have [simp]: "a ∈ R" "b ∈ R" "a' ∈ R" "b' ∈ R"
and bnz: "b ≠ 𝟬" and b'nz: "b' ≠ 𝟬" by auto
have a'nz: "a' ≠ 𝟬"
proof
assume "a' = 𝟬"
with e have "a ⋅ b' = 𝟬" by simp
then have "a = 𝟬 ∨ b' = 𝟬" using no_zero_divisors by simp
with anz b'nz show False by auto
qed
have s1: "(b, a) ∈ frac_set" using anz by (auto intro!: frac_setI)
have s2: "(b', a') ∈ frac_set" using a'nz by (auto intro!: frac_setI)
have "b ⋅ a' = a' ⋅ b" by (simp add: mult_ac)
also have "… = a ⋅ b'" by (simp add: e)
also have "… = b' ⋅ a" by (simp add: mult_ac)
finally have "b ⋅ a' = b' ⋅ a" .
with s1 s2 show ?thesis by (rule frac_relI)
qed
subsubsection ‹The ‹Class›-formulas›
text ‹Key auxiliary: if a class is chosen from a fraction, the SOME-representative is equivalent
to the given fraction.›
lemma some_rep_equiv:
assumes ab: "(a, b) ∈ frac_set"
defines "p ≡ SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
shows "(p, (a, b)) ∈ frac_rel" and "p ∈ frac_set"
proof -
have rep_prop: "p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
unfolding p_def using rep_in_frac_set[OF ab] by simp
then have "p ∈ frac.Class (a, b)" and "p ∈ frac_set" by auto
from frac.ClassD[OF this(1) ab] show "(p, (a, b)) ∈ frac_rel" .
from rep_prop show "p ∈ frac_set" by simp
qed
lemma frac_add_Class:
assumes ab: "(a, b) ∈ frac_set" and cd: "(c, d) ∈ frac_set"
shows "frac.Class (a, b) [+] frac.Class (c, d) = frac.Class (a ⋅ d + c ⋅ b, b ⋅ d)"
proof -
let ?p = "SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
let ?q = "SOME p. p ∈ frac.Class (c, d) ∧ p ∈ frac_set"
have p_equiv: "(?p, (a, b)) ∈ frac_rel" using some_rep_equiv(1)[OF ab] .
have q_equiv: "(?q, (c, d)) ∈ frac_rel" using some_rep_equiv(1)[OF cd] .
obtain a1 b1 where p_eq: "?p = (a1, b1)" by force
obtain c1 d1 where q_eq: "?q = (c1, d1)" by force
from p_eq p_equiv have "((a1, b1), (a, b)) ∈ frac_rel" by simp
moreover from q_eq q_equiv have "((c1, d1), (c, d)) ∈ frac_rel" by simp
ultimately have "((a1 ⋅ d1 + c1 ⋅ b1, b1 ⋅ d1), (a ⋅ d + c ⋅ b, b ⋅ d)) ∈ frac_rel"
by (rule frac_add_cong)
then have "frac.Class (a1 ⋅ d1 + c1 ⋅ b1, b1 ⋅ d1) = frac.Class (a ⋅ d + c ⋅ b, b ⋅ d)"
by (rule frac.Class_eq)
then show ?thesis
unfolding frac_add_def by (simp add: p_eq q_eq)
qed
lemma frac_mult_Class:
assumes ab: "(a, b) ∈ frac_set" and cd: "(c, d) ∈ frac_set"
shows "frac.Class (a, b) [⋅] frac.Class (c, d) = frac.Class (a ⋅ c, b ⋅ d)"
proof -
let ?p = "SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
let ?q = "SOME p. p ∈ frac.Class (c, d) ∧ p ∈ frac_set"
have p_equiv: "(?p, (a, b)) ∈ frac_rel" using some_rep_equiv(1)[OF ab] .
have q_equiv: "(?q, (c, d)) ∈ frac_rel" using some_rep_equiv(1)[OF cd] .
obtain a1 b1 where p_eq: "?p = (a1, b1)" by force
obtain c1 d1 where q_eq: "?q = (c1, d1)" by force
from p_eq p_equiv have "((a1, b1), (a, b)) ∈ frac_rel" by simp
moreover from q_eq q_equiv have "((c1, d1), (c, d)) ∈ frac_rel" by simp
ultimately have "((a1 ⋅ c1, b1 ⋅ d1), (a ⋅ c, b ⋅ d)) ∈ frac_rel"
by (rule frac_mult_cong)
then have "frac.Class (a1 ⋅ c1, b1 ⋅ d1) = frac.Class (a ⋅ c, b ⋅ d)"
by (rule frac.Class_eq)
then show ?thesis
unfolding frac_mult_def by (simp add: p_eq q_eq)
qed
lemma frac_neg_Class:
assumes ab: "(a, b) ∈ frac_set"
shows "[-] frac.Class (a, b) = frac.Class (- a, b)"
proof -
let ?p = "SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
have p_equiv: "(?p, (a, b)) ∈ frac_rel" using some_rep_equiv(1)[OF ab] .
obtain a1 b1 where p_eq: "?p = (a1, b1)" by force
from p_eq p_equiv have "((a1, b1), (a, b)) ∈ frac_rel" by simp
then have "((- a1, b1), (- a, b)) ∈ frac_rel" by (rule frac_neg_cong)
then have "frac.Class (- a1, b1) = frac.Class (- a, b)" by (rule frac.Class_eq)
then show ?thesis unfolding frac_neg_def by (simp add: p_eq)
qed
lemma frac_inv_Class:
assumes ab: "(a, b) ∈ frac_set" and anz: "a ≠ 𝟬"
shows "frac_inv (frac.Class (a, b)) = frac.Class (b, a)"
proof -
let ?p = "SOME p. p ∈ frac.Class (a, b) ∧ p ∈ frac_set"
have p_equiv: "(?p, (a, b)) ∈ frac_rel" using some_rep_equiv(1)[OF ab] .
obtain a1 b1 where p_eq: "?p = (a1, b1)" by force
from p_eq p_equiv have r: "((a1, b1), (a, b)) ∈ frac_rel" by simp
from r have r': "((a, b), (a1, b1)) ∈ frac_rel" by (rule frac.symmetric)
then have "((b, a), (b1, a1)) ∈ frac_rel" using anz by (rule frac_inv_cong)
then have "((b1, a1), (b, a)) ∈ frac_rel" by (rule frac.symmetric)
then have "frac.Class (b1, a1) = frac.Class (b, a)" by (rule frac.Class_eq)
then show ?thesis unfolding frac_inv_def by (simp add: p_eq)
qed
subsubsection ‹Closure under the operations›
lemma frac_add_closed [intro, simp]:
"A ∈ Fractions ⟹ B ∈ Fractions ⟹ A [+] B ∈ Fractions"
proof -
assume "A ∈ Fractions" "B ∈ Fractions"
then obtain a b c d
where A: "A = frac.Class (a, b)" "(a, b) ∈ frac_set"
and B: "B = frac.Class (c, d)" "(c, d) ∈ frac_set"
by (metis Fractions_cases)
then have [simp]: "b ∈ R" "d ∈ R" "b ≠ 𝟬" "d ≠ 𝟬" and abR: "a ∈ R" "c ∈ R" by auto
have "(a ⋅ d + c ⋅ b, b ⋅ d) ∈ frac_set" using abR frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
then show "A [+] B ∈ Fractions" using A B frac_add_Class[OF A(2) B(2)] by auto
qed
lemma frac_mult_closed [intro, simp]:
"A ∈ Fractions ⟹ B ∈ Fractions ⟹ A [⋅] B ∈ Fractions"
proof -
assume "A ∈ Fractions" "B ∈ Fractions"
then obtain a b c d
where A: "A = frac.Class (a, b)" "(a, b) ∈ frac_set"
and B: "B = frac.Class (c, d)" "(c, d) ∈ frac_set"
by (metis Fractions_cases)
then have [simp]: "b ∈ R" "d ∈ R" "b ≠ 𝟬" "d ≠ 𝟬" and abR: "a ∈ R" "c ∈ R" by auto
have "(a ⋅ c, b ⋅ d) ∈ frac_set" using abR frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
then show "A [⋅] B ∈ Fractions" using A B frac_mult_Class[OF A(2) B(2)] by auto
qed
lemma frac_neg_closed [intro, simp]: "A ∈ Fractions ⟹ [-] A ∈ Fractions"
proof -
assume "A ∈ Fractions"
then obtain a b where A: "A = frac.Class (a, b)" "(a, b) ∈ frac_set" by (metis Fractions_cases)
then have "(- a, b) ∈ frac_set" by (auto intro!: frac_setI)
then show "[-] A ∈ Fractions" using A frac_neg_Class[OF A(2)] by auto
qed
subsection ‹The field of fractions›
text ‹We assemble the additive abelian group and the multiplicative monoid as separate top-level
lemmas, then compose them via @{thm [source] Ring.intro} to obtain the ring structure. This
avoids taking on the (locale-qualified) @{term Monoid.invertible} obligation mid-interpretation:
we discharge it once, at the level of @{thm [source] GroupI}, which takes the raw
‹∃v ∈ G. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭› form directly.›
subsubsection ‹The additive abelian group of ‹Fractions››
text ‹The additive group. Associativity, unit, invertibility, and commutativity are established
on fraction representatives. Invertibility supplies the explicit inverse ‹Class(- a, b)› of
‹Class(a, b)›.›
lemma Frac_add_group: "Group Fractions ([+]) [𝟬]"
proof (rule GroupI)
fix A B assume "A ∈ Fractions" "B ∈ Fractions"
then show "A [+] B ∈ Fractions" by simp
next
show "[𝟬] ∈ Fractions" by simp
next
fix A B C assume A: "A ∈ Fractions" and B: "B ∈ Fractions" and C: "C ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
obtain e f where C': "C = frac.Class (e, f)" "(e, f) ∈ frac_set" using C by (metis Fractions_cases)
from A' B' C' have [simp]:
"a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "e ∈ R" "f ∈ R"
"b ≠ 𝟬" "d ≠ 𝟬" "f ≠ 𝟬" by auto
have s1: "(a ⋅ d + c ⋅ b, b ⋅ d) ∈ frac_set"
using frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
have s2: "(c ⋅ f + e ⋅ d, d ⋅ f) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] by (auto intro!: frac_setI)
have "(A [+] B) [+] C = frac.Class ((a ⋅ d + c ⋅ b) ⋅ f + e ⋅ (b ⋅ d), (b ⋅ d) ⋅ f)"
using A' B' C' by (simp add: frac_add_Class[OF A'(2) B'(2)] frac_add_Class[OF s1 C'(2)])
moreover have "A [+] (B [+] C) = frac.Class (a ⋅ (d ⋅ f) + (c ⋅ f + e ⋅ d) ⋅ b, b ⋅ (d ⋅ f))"
using A' B' C' by (simp add: frac_add_Class[OF B'(2) C'(2)] frac_add_Class[OF A'(2) s2])
moreover have "(a ⋅ d + c ⋅ b) ⋅ f + e ⋅ (b ⋅ d) = a ⋅ (d ⋅ f) + (c ⋅ f + e ⋅ d) ⋅ b"
proof -
have LHS: "(a ⋅ d + c ⋅ b) ⋅ f + e ⋅ (b ⋅ d) = a ⋅ (d ⋅ f) + c ⋅ f ⋅ b + e ⋅ d ⋅ b"
by (simp add: distributive mult_ac add_ac)
have RHS: "a ⋅ (d ⋅ f) + (c ⋅ f + e ⋅ d) ⋅ b = a ⋅ (d ⋅ f) + c ⋅ f ⋅ b + e ⋅ d ⋅ b"
by (simp add: distributive mult_ac add_ac)
from LHS RHS show ?thesis by simp
qed
moreover have "(b ⋅ d) ⋅ f = b ⋅ (d ⋅ f)" by (simp add: mult_ac)
ultimately show "(A [+] B) [+] C = A [+] (B [+] C)" by simp
next
fix A assume A: "A ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have [simp]: "a ∈ R" "b ∈ R" "b ≠ 𝟬" by auto
have "[𝟬] [+] A = frac.Class (𝟬 ⋅ b + a ⋅ 𝟭, 𝟭 ⋅ b)"
using A' by (simp add: frac_add_Class[OF zero_in_frac_set A'(2)])
also have "… = frac.Class (a, b)" by simp
finally show "[𝟬] [+] A = A" using A' by simp
next
fix A assume A: "A ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have [simp]: "a ∈ R" "b ∈ R" "b ≠ 𝟬" by auto
have "A [+] [𝟬] = frac.Class (a ⋅ 𝟭 + 𝟬 ⋅ b, b ⋅ 𝟭)"
using A' by (simp add: frac_add_Class[OF A'(2) zero_in_frac_set])
also have "… = frac.Class (a, b)" by simp
finally show "A [+] [𝟬] = A" using A' by simp
next
fix A assume A: "A ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have abR: "a ∈ R" "b ∈ R" and bnz: "b ≠ 𝟬" by auto
have bbR: "b ⋅ b ∈ R" and bbnz: "b ⋅ b ≠ 𝟬"
using abR bnz frac_mult_denom_nonzero[of b b] by auto
have negA_in_frac_set: "(- a, b) ∈ frac_set" using abR bnz by (auto intro!: frac_setI)
have negA: "[-] A = frac.Class (- a, b)" using A' by (simp add: frac_neg_Class[OF A'(2)])
have zero_bb_in: "(𝟬, b ⋅ b) ∈ frac_set" using bbR bbnz by (auto intro!: frac_setI)
have zero_bb_eq_zero: "frac.Class (𝟬, b ⋅ b) = frac.Class (𝟬, 𝟭)"
using bbR by (intro frac_eqI[OF zero_bb_in zero_in_frac_set]) simp
have right: "A [+] ([-] A) = [𝟬]"
proof -
have "A [+] ([-] A) = frac.Class (a ⋅ b + (- a) ⋅ b, b ⋅ b)"
using A' negA by (simp add: frac_add_Class[OF A'(2) negA_in_frac_set])
also have "a ⋅ b + (- a) ⋅ b = 𝟬" using abR by (simp add: left_minus)
finally have "A [+] ([-] A) = frac.Class (𝟬, b ⋅ b)" .
then show ?thesis using zero_bb_eq_zero by simp
qed
have left: "[-] A [+] A = [𝟬]"
proof -
have "[-] A [+] A = frac.Class ((- a) ⋅ b + a ⋅ b, b ⋅ b)"
using A' negA by (simp add: frac_add_Class[OF negA_in_frac_set A'(2)])
also have "(- a) ⋅ b + a ⋅ b = 𝟬" using abR by (simp add: left_minus)
finally have "[-] A [+] A = frac.Class (𝟬, b ⋅ b)" .
then show ?thesis using zero_bb_eq_zero by simp
qed
have negA_class: "[-] A ∈ Fractions" using A by simp
from right left negA_class show "∃v∈Fractions. A [+] v = [𝟬] ∧ v [+] A = [𝟬]" by blast
qed
lemma Frac_add_commutative: "⟦ A ∈ Fractions; B ∈ Fractions ⟧ ⟹ A [+] B = B [+] A"
proof -
fix A B assume A: "A ∈ Fractions" and B: "B ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
from A' B' have [simp]: "a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "b ≠ 𝟬" "d ≠ 𝟬" by auto
have "A [+] B = frac.Class (a ⋅ d + c ⋅ b, b ⋅ d)"
using A' B' by (simp add: frac_add_Class[OF A'(2) B'(2)])
moreover have "B [+] A = frac.Class (c ⋅ b + a ⋅ d, d ⋅ b)"
using A' B' by (simp add: frac_add_Class[OF B'(2) A'(2)])
moreover have "a ⋅ d + c ⋅ b = c ⋅ b + a ⋅ d" by (simp add: add_ac)
moreover have "b ⋅ d = d ⋅ b" by (simp add: mult_ac)
ultimately show "A [+] B = B [+] A" by simp
qed
lemma Frac_add_commutative_monoid: "commutative_monoid Fractions ([+]) [𝟬]"
proof -
interpret G: Group Fractions "([+])" "[𝟬]" by (rule Frac_add_group)
show ?thesis
by unfold_locales (simp_all add: Frac_add_commutative)
qed
lemma Frac_abelian_group: "Abelian_Group Fractions ([+]) [𝟬]"
by (rule Abelian_Group.intro[OF Frac_add_group Frac_add_commutative_monoid])
subsubsection ‹The multiplicative monoid of ‹Fractions››
lemma Frac_mult_monoid: "Monoid Fractions ([⋅]) [𝟭]"
proof
fix A B assume "A ∈ Fractions" "B ∈ Fractions"
then show "A [⋅] B ∈ Fractions" by simp
next
show "[𝟭] ∈ Fractions" by simp
next
fix A B C assume A: "A ∈ Fractions" and B: "B ∈ Fractions" and C: "C ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
obtain e f where C': "C = frac.Class (e, f)" "(e, f) ∈ frac_set" using C by (metis Fractions_cases)
from A' B' C' have [simp]:
"a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "e ∈ R" "f ∈ R"
"b ≠ 𝟬" "d ≠ 𝟬" "f ≠ 𝟬" by auto
have s1: "(a ⋅ c, b ⋅ d) ∈ frac_set"
using frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
have s2: "(c ⋅ e, d ⋅ f) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] by (auto intro!: frac_setI)
have "(A [⋅] B) [⋅] C = frac.Class ((a ⋅ c) ⋅ e, (b ⋅ d) ⋅ f)"
using A' B' C' by (simp add: frac_mult_Class[OF A'(2) B'(2)] frac_mult_Class[OF s1 C'(2)])
moreover have "A [⋅] (B [⋅] C) = frac.Class (a ⋅ (c ⋅ e), b ⋅ (d ⋅ f))"
using A' B' C' by (simp add: frac_mult_Class[OF B'(2) C'(2)] frac_mult_Class[OF A'(2) s2])
moreover have "(a ⋅ c) ⋅ e = a ⋅ (c ⋅ e)" by (simp add: mult_ac)
moreover have "(b ⋅ d) ⋅ f = b ⋅ (d ⋅ f)" by (simp add: mult_ac)
ultimately show "(A [⋅] B) [⋅] C = A [⋅] (B [⋅] C)" by simp
next
fix A assume A: "A ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have [simp]: "a ∈ R" "b ∈ R" "b ≠ 𝟬" by auto
have "[𝟭] [⋅] A = frac.Class (𝟭 ⋅ a, 𝟭 ⋅ b)"
using A' by (simp add: frac_mult_Class[OF one_in_frac_set A'(2)])
also have "… = frac.Class (a, b)" by simp
finally show "[𝟭] [⋅] A = A" using A' by simp
next
fix A assume A: "A ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have [simp]: "a ∈ R" "b ∈ R" "b ≠ 𝟬" by auto
have "A [⋅] [𝟭] = frac.Class (a ⋅ 𝟭, b ⋅ 𝟭)"
using A' by (simp add: frac_mult_Class[OF A'(2) one_in_frac_set])
also have "… = frac.Class (a, b)" by simp
finally show "A [⋅] [𝟭] = A" using A' by simp
qed
subsubsection ‹Distributivity and the ring axiom›
lemma Frac_Ring_axioms: "Ring_axioms Fractions ([+]) ([⋅])"
proof
fix A B C assume A: "A ∈ Fractions" and B: "B ∈ Fractions" and C: "C ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
obtain e f where C': "C = frac.Class (e, f)" "(e, f) ∈ frac_set" using C by (metis Fractions_cases)
from A' B' C' have [simp]:
"a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "e ∈ R" "f ∈ R"
"b ≠ 𝟬" "d ≠ 𝟬" "f ≠ 𝟬" by auto
have BC_in: "(c ⋅ f + e ⋅ d, d ⋅ f) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] by (auto intro!: frac_setI)
have AB_in: "(a ⋅ c, b ⋅ d) ∈ frac_set"
using frac_mult_denom_nonzero[of b d] by (auto intro!: frac_setI)
have AC_in: "(a ⋅ e, b ⋅ f) ∈ frac_set"
using frac_mult_denom_nonzero[of b f] by (auto intro!: frac_setI)
have "A [⋅] (B [+] C) = frac.Class (a ⋅ (c ⋅ f + e ⋅ d), b ⋅ (d ⋅ f))"
using A' B' C' by (simp add: frac_add_Class[OF B'(2) C'(2)] frac_mult_Class[OF A'(2) BC_in])
moreover have "A [⋅] B [+] A [⋅] C =
frac.Class ((a ⋅ c) ⋅ (b ⋅ f) + (a ⋅ e) ⋅ (b ⋅ d), (b ⋅ d) ⋅ (b ⋅ f))"
using A' B' C'
by (simp add: frac_mult_Class[OF A'(2) B'(2)] frac_mult_Class[OF A'(2) C'(2)]
frac_add_Class[OF AB_in AC_in])
moreover have
"(a ⋅ (c ⋅ f + e ⋅ d)) ⋅ ((b ⋅ d) ⋅ (b ⋅ f)) =
((a ⋅ c) ⋅ (b ⋅ f) + (a ⋅ e) ⋅ (b ⋅ d)) ⋅ (b ⋅ (d ⋅ f))"
proof -
have "a ⋅ (c ⋅ f + e ⋅ d) = a ⋅ (c ⋅ f) + a ⋅ (e ⋅ d)" by (simp add: distributive)
then have L: "(a ⋅ (c ⋅ f + e ⋅ d)) ⋅ ((b ⋅ d) ⋅ (b ⋅ f))
= a ⋅ (c ⋅ f) ⋅ ((b ⋅ d) ⋅ (b ⋅ f)) + a ⋅ (e ⋅ d) ⋅ ((b ⋅ d) ⋅ (b ⋅ f))"
by (simp add: distributive)
have "((a ⋅ c) ⋅ (b ⋅ f) + (a ⋅ e) ⋅ (b ⋅ d)) ⋅ (b ⋅ (d ⋅ f))
= (a ⋅ c) ⋅ (b ⋅ f) ⋅ (b ⋅ (d ⋅ f)) + (a ⋅ e) ⋅ (b ⋅ d) ⋅ (b ⋅ (d ⋅ f))"
by (simp add: distributive)
also have "(a ⋅ c) ⋅ (b ⋅ f) ⋅ (b ⋅ (d ⋅ f)) = a ⋅ (c ⋅ f) ⋅ ((b ⋅ d) ⋅ (b ⋅ f))"
by (simp add: mult_ac)
also have "(a ⋅ e) ⋅ (b ⋅ d) ⋅ (b ⋅ (d ⋅ f)) = a ⋅ (e ⋅ d) ⋅ ((b ⋅ d) ⋅ (b ⋅ f))"
by (simp add: mult_ac)
finally show ?thesis using L by simp
qed
moreover have "(a ⋅ (c ⋅ f + e ⋅ d), b ⋅ (d ⋅ f)) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] frac_mult_denom_nonzero[of b "d ⋅ f"]
by (auto intro!: frac_setI)
moreover have "((a ⋅ c) ⋅ (b ⋅ f) + (a ⋅ e) ⋅ (b ⋅ d), (b ⋅ d) ⋅ (b ⋅ f)) ∈ frac_set"
using frac_mult_denom_nonzero[of b d] frac_mult_denom_nonzero[of b f]
frac_mult_denom_nonzero[of "b ⋅ d" "b ⋅ f"]
by (auto intro!: frac_setI)
ultimately show "A [⋅] (B [+] C) = A [⋅] B [+] A [⋅] C"
by (metis frac_eqI)
next
fix A B C assume A: "A ∈ Fractions" and B: "B ∈ Fractions" and C: "C ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
obtain e f where C': "C = frac.Class (e, f)" "(e, f) ∈ frac_set" using C by (metis Fractions_cases)
from A' B' C' have [simp]:
"a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "e ∈ R" "f ∈ R"
"b ≠ 𝟬" "d ≠ 𝟬" "f ≠ 𝟬" by auto
have BC_in: "(c ⋅ f + e ⋅ d, d ⋅ f) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] by (auto intro!: frac_setI)
have BA_in: "(c ⋅ a, d ⋅ b) ∈ frac_set"
using frac_mult_denom_nonzero[of d b] by (auto intro!: frac_setI)
have CA_in: "(e ⋅ a, f ⋅ b) ∈ frac_set"
using frac_mult_denom_nonzero[of f b] by (auto intro!: frac_setI)
have "(B [+] C) [⋅] A = frac.Class ((c ⋅ f + e ⋅ d) ⋅ a, (d ⋅ f) ⋅ b)"
using A' B' C' by (simp add: frac_add_Class[OF B'(2) C'(2)] frac_mult_Class[OF BC_in A'(2)])
moreover have "B [⋅] A [+] C [⋅] A =
frac.Class ((c ⋅ a) ⋅ (f ⋅ b) + (e ⋅ a) ⋅ (d ⋅ b), (d ⋅ b) ⋅ (f ⋅ b))"
using A' B' C'
by (simp add: frac_mult_Class[OF B'(2) A'(2)] frac_mult_Class[OF C'(2) A'(2)]
frac_add_Class[OF BA_in CA_in])
moreover have
"((c ⋅ f + e ⋅ d) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b)) =
((c ⋅ a) ⋅ (f ⋅ b) + (e ⋅ a) ⋅ (d ⋅ b)) ⋅ ((d ⋅ f) ⋅ b)"
proof -
have "(c ⋅ f + e ⋅ d) ⋅ a = (c ⋅ f) ⋅ a + (e ⋅ d) ⋅ a" by (simp add: distributive)
then have L: "((c ⋅ f + e ⋅ d) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b))
= ((c ⋅ f) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b)) + ((e ⋅ d) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b))"
by (simp add: distributive)
have "((c ⋅ a) ⋅ (f ⋅ b) + (e ⋅ a) ⋅ (d ⋅ b)) ⋅ ((d ⋅ f) ⋅ b)
= (c ⋅ a) ⋅ (f ⋅ b) ⋅ ((d ⋅ f) ⋅ b) + (e ⋅ a) ⋅ (d ⋅ b) ⋅ ((d ⋅ f) ⋅ b)"
by (simp add: distributive)
also have "(c ⋅ a) ⋅ (f ⋅ b) ⋅ ((d ⋅ f) ⋅ b) = ((c ⋅ f) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b))"
by (simp add: mult_ac)
also have "(e ⋅ a) ⋅ (d ⋅ b) ⋅ ((d ⋅ f) ⋅ b) = ((e ⋅ d) ⋅ a) ⋅ ((d ⋅ b) ⋅ (f ⋅ b))"
by (simp add: mult_ac)
finally show ?thesis using L by simp
qed
moreover have "((c ⋅ f + e ⋅ d) ⋅ a, (d ⋅ f) ⋅ b) ∈ frac_set"
using frac_mult_denom_nonzero[of d f] frac_mult_denom_nonzero[of "d ⋅ f" b]
by (auto intro!: frac_setI)
moreover have "((c ⋅ a) ⋅ (f ⋅ b) + (e ⋅ a) ⋅ (d ⋅ b), (d ⋅ b) ⋅ (f ⋅ b)) ∈ frac_set"
using frac_mult_denom_nonzero[of d b] frac_mult_denom_nonzero[of f b]
frac_mult_denom_nonzero[of "d ⋅ b" "f ⋅ b"]
by (auto intro!: frac_setI)
ultimately show "(B [+] C) [⋅] A = B [⋅] A [+] C [⋅] A"
by (metis frac_eqI)
qed
text ‹Assemble the additive abelian group, multiplicative monoid, and the distributive laws into
the @{locale Ring} interpretation.›
interpretation Frac: Ring Fractions "([+])" "([⋅])" "[𝟬]" "[𝟭]"
by (rule Ring.intro[OF Frac_abelian_group Frac_mult_monoid Frac_Ring_axioms])
interpretation Frac: commutative_ring Fractions "([+])" "([⋅])" "[𝟬]" "[𝟭]"
proof
fix A B assume A: "A ∈ Fractions" and B: "B ∈ Fractions"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
obtain c d where B': "B = frac.Class (c, d)" "(c, d) ∈ frac_set" using B by (metis Fractions_cases)
from A' B' have [simp]: "a ∈ R" "b ∈ R" "c ∈ R" "d ∈ R" "b ≠ 𝟬" "d ≠ 𝟬" by auto
have "A [⋅] B = frac.Class (a ⋅ c, b ⋅ d)"
using A' B' by (simp add: frac_mult_Class[OF A'(2) B'(2)])
moreover have "B [⋅] A = frac.Class (c ⋅ a, d ⋅ b)"
using A' B' by (simp add: frac_mult_Class[OF B'(2) A'(2)])
moreover have "a ⋅ c = c ⋅ a" by (simp add: mult_ac)
moreover have "b ⋅ d = d ⋅ b" by (simp add: mult_ac)
ultimately show "A [⋅] B = B [⋅] A" by simp
qed
interpretation Frac: Field Fractions "([+])" "([⋅])" "[𝟬]" "[𝟭]"
proof
show "[𝟭] ≠ [𝟬]" using frac_one_neq_zero .
next
fix A assume A: "A ∈ Fractions" and Anz: "A ≠ [𝟬]"
obtain a b where A': "A = frac.Class (a, b)" "(a, b) ∈ frac_set" using A by (metis Fractions_cases)
from A' have abR: "a ∈ R" "b ∈ R" and bnz: "b ≠ 𝟬" by auto
have anz: "a ≠ 𝟬" using Anz A' frac_Class_zero_iff[OF A'(2)] by blast
have inv_in: "(b, a) ∈ frac_set" using abR anz by (auto intro!: frac_setI)
have inv_class: "frac_inv A = frac.Class (b, a)"
using A' by (simp add: frac_inv_Class[OF A'(2) anz])
have "A [⋅] frac_inv A = frac.Class (a ⋅ b, b ⋅ a)"
using A' inv_class by (simp add: frac_mult_Class[OF A'(2) inv_in])
moreover have "frac.Class (a ⋅ b, b ⋅ a) = [𝟭]"
proof -
have "(a ⋅ b, b ⋅ a) ∈ frac_set"
using abR anz bnz frac_mult_denom_nonzero[of b a] by (auto intro!: frac_setI)
moreover have "(𝟭, 𝟭) ∈ frac_set" by (auto simp: nontrivial)
moreover have "(a ⋅ b) ⋅ 𝟭 = 𝟭 ⋅ (b ⋅ a)" using abR by (simp add: mult_ac)
ultimately show ?thesis by (rule frac_eqI)
qed
ultimately have right_inv: "A [⋅] frac_inv A = [𝟭]" by simp
have "frac_inv A [⋅] A = frac.Class (b ⋅ a, a ⋅ b)"
using A' inv_class by (simp add: frac_mult_Class[OF inv_in A'(2)])
moreover have "frac.Class (b ⋅ a, a ⋅ b) = [𝟭]"
proof -
have "(b ⋅ a, a ⋅ b) ∈ frac_set"
using abR anz bnz frac_mult_denom_nonzero[of a b] by (auto intro!: frac_setI)
moreover have "(𝟭, 𝟭) ∈ frac_set" by (auto simp: nontrivial)
moreover have "(b ⋅ a) ⋅ 𝟭 = 𝟭 ⋅ (a ⋅ b)" using abR by (simp add: mult_ac)
ultimately show ?thesis by (rule frac_eqI)
qed
ultimately have left_inv: "frac_inv A [⋅] A = [𝟭]" by simp
have inv_in_carrier: "frac_inv A ∈ Fractions" using inv_class inv_in by simp
show "Frac.multiplicative.invertible A" using right_inv left_inv A inv_in_carrier
by (blast intro: Frac.multiplicative.invertibleI)
qed
subsection ‹The canonical embedding ‹R → Fractions››
text ‹The canonical map ‹a ↦ ‹Class(a, 𝟭)›› embeds ‹R› into its field of fractions. It is an
injective ring homomorphism. Together with the field structure, this is the universal
embedding of an integral domain into a field: every nonzero element of ‹R› acquires a
multiplicative inverse in ‹Fractions›.›
definition to_frac :: "'a ⇒ ('a × 'a) set"
where "to_frac = (λa ∈ R. frac.Class (a, 𝟭))"
lemma to_frac_apply [simp]: "a ∈ R ⟹ to_frac a = frac.Class (a, 𝟭)"
unfolding to_frac_def by simp
lemma to_frac_undefined [simp]: "a ∉ R ⟹ to_frac a = undefined"
unfolding to_frac_def by simp
lemma to_frac_pair: "a ∈ R ⟹ (a, 𝟭) ∈ frac_set"
by (auto intro!: frac_setI simp: nontrivial)
lemma to_frac_in_Fractions [intro, simp]: "a ∈ R ⟹ to_frac a ∈ Fractions"
using to_frac_pair by (simp add: to_frac_apply)
lemma to_frac_zero: "to_frac 𝟬 = [𝟬]" by simp
lemma to_frac_one: "to_frac 𝟭 = [𝟭]" by simp
lemma to_frac_add:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "to_frac (a + b) = to_frac a [+] to_frac b"
proof -
have "to_frac a [+] to_frac b = frac.Class (a ⋅ 𝟭 + b ⋅ 𝟭, 𝟭 ⋅ 𝟭)"
using a b by (simp add: frac_add_Class[OF to_frac_pair[OF a] to_frac_pair[OF b]])
also have "… = frac.Class (a + b, 𝟭)" using a b by simp
finally show ?thesis using a b by simp
qed
lemma to_frac_mult:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "to_frac (a ⋅ b) = to_frac a [⋅] to_frac b"
proof -
have "to_frac a [⋅] to_frac b = frac.Class (a ⋅ b, 𝟭 ⋅ 𝟭)"
using a b by (simp add: frac_mult_Class[OF to_frac_pair[OF a] to_frac_pair[OF b]])
also have "… = frac.Class (a ⋅ b, 𝟭)" by simp
finally show ?thesis using a b by simp
qed
lemma to_frac_inj:
assumes a: "a ∈ R" and b: "b ∈ R" and eq: "to_frac a = to_frac b"
shows "a = b"
proof -
have "a ⋅ 𝟭 = b ⋅ 𝟭"
by (rule frac_eqD[OF to_frac_pair[OF a] to_frac_pair[OF b]]) (use eq a b in simp)
with a b show ?thesis by simp
qed
interpretation to_frac: ring_homomorphism to_frac R "addition" "(⋅)" 𝟬 𝟭
Fractions "([+])" "([⋅])" "[𝟬]" "[𝟭]"
proof
have "⋀x. x ∈ R ⟹ to_frac x ∈ Fractions" by (rule to_frac_in_Fractions)
moreover have "⋀x. x ∉ R ⟹ to_frac x = undefined" by (rule to_frac_undefined)
ultimately show "to_frac ∈ R →⇩E Fractions"
unfolding PiE_def extensional_def by blast
next
fix a b assume "a ∈ R" "b ∈ R"
then show "to_frac (a + b) = to_frac a [+] to_frac b" by (rule to_frac_add)
from ‹a ∈ R› ‹b ∈ R› show "to_frac (a ⋅ b) = to_frac a [⋅] to_frac b" by (rule to_frac_mult)
next
show "to_frac 𝟬 = [𝟬]" by (rule to_frac_zero)
show "to_frac 𝟭 = [𝟭]" by (rule to_frac_one)
qed
end
end