Theory ISQ_Algebra

section ‹ Algebraic Laws ›

theory ISQ_Algebra
  imports ISQ_Proof
begin

subsection ‹ Quantity Scale ›

lemma scaleQ_add_right: "a *⇩Q x + y = (a *⇩Q x) + (a *⇩Q y)"
  by (si_simp add: distrib_left)

lemma scaleQ_add_left: "a + b *⇩Q x = (a *⇩Q x) + (b *⇩Q x)"
  by (si_simp add: distrib_right)

lemma scaleQ_scaleQ [simp]: "a *⇩Q b *⇩Q x = a ⋅ b *⇩Q x"
  by si_simp

lemma scaleQ_one [simp]: "1 *⇩Q x = x"
  by si_simp

lemma scaleQ_zero [simp]: "0 *⇩Q x = 0"
  by si_simp

lemma scaleQ_inv: "-a *⇩Q x = a *⇩Q -x"
  by si_calc

lemma scaleQ_as_qprod: "a *⇩Q x ≅⇩Q (a *⇩Q 𝟭) ❙⋅ x"
  by si_simp

lemma mult_scaleQ_left [simp]: "(a *⇩Q x) ❙⋅ y = a *⇩Q x ❙⋅ y"
  by si_simp

lemma mult_scaleQ_right [simp]: "x ❙⋅ (a *⇩Q y) = a *⇩Q x ❙⋅ y"
  by si_simp

subsection ‹ Field Laws ›

lemma qtimes_commute: "x ❙⋅ y ≅⇩Q y ❙⋅ x"
  by si_calc

lemma qtimes_assoc: "(x ❙⋅ y) ❙⋅ z  ≅⇩Q  x ❙⋅ (y ❙⋅ z)"
  by (si_calc)

lemma qtimes_left_unit: "𝟭 ❙⋅ x ≅⇩Q x"
  by (si_calc)

lemma qtimes_right_unit: "x ❙⋅ 𝟭 ≅⇩Q x"
  by (si_calc)

text‹The following weak congruences will allow for replacing equivalences in contexts
     built from product and inverse. ›

lemma qtimes_weak_cong_left:
  assumes "x ≅⇩Q y"
  shows  "x❙⋅z ≅⇩Q y❙⋅z"
  using assms by si_simp

lemma qtimes_weak_cong_right:
  assumes "x ≅⇩Q y"
  shows  "z❙⋅x ≅⇩Q z❙⋅y"
  using assms by si_calc

lemma qinverse_weak_cong:
  assumes "x ≅⇩Q y"
  shows   "x⇧-⇧𝟭 ≅⇩Q y⇧-⇧𝟭"
  using assms by si_calc

lemma scaleQ_cong:
  assumes "y ≅⇩Q z"
  shows "x *⇩Q y ≅⇩Q x *⇩Q z"
  using assms by si_calc

lemma qinverse_qinverse: "x⇧-⇧𝟭⇧-⇧𝟭 ≅⇩Q x"
  by si_calc

lemma qinverse_nonzero_iff_nonzero: "x⇧-⇧𝟭 = 0 ⟷ x = 0"
  by (auto, si_calc+)

lemma qinverse_qtimes: "(x ❙⋅ y)⇧-⇧𝟭 ≅⇩Q x⇧-⇧𝟭 ❙⋅ y⇧-⇧𝟭"
  by (si_simp add: inverse_distrib)

lemma qinverse_qdivide: "(x ❙/ y)⇧-⇧𝟭 ≅⇩Q y ❙/ x"
  by si_simp

lemma qtimes_cancel: "x ≠ 0 ⟹ x ❙/ x ≅⇩Q 𝟭"
  by si_calc

end