Theory Groups_mult

section ‹ Multiplication Groups ›

theory Groups_mult
  imports Main
begin

text ‹ The HOL standard library only has groups based on addition. Here, we build one based on
  multiplication. ›

notation times (infixl "⋅" 70)

class group_mult = inverse + monoid_mult +
  assumes left_inverse: "inverse a ⋅ a = 1"
  assumes multi_inverse_conv_div [simp]: "a ⋅ (inverse b) = a / b"
begin

lemma div_conv_mult_inverse: "a / b = a ⋅ (inverse b)"
  by simp

sublocale mult: group times 1 inverse
  by standard (simp_all add: left_inverse)

lemma diff_self [simp]: "a / a = 1"
  using mult.right_inverse by auto

lemma mult_distrib_inverse [simp]: "(a * b) / b = a"
  by (metis local.mult_1_right local.multi_inverse_conv_div mult.right_inverse mult_assoc)

end

class ab_group_mult = comm_monoid_mult + group_mult
begin

lemma mult_distrib_inverse' [simp]: "(a * b) / a = b"
  using local.mult_distrib_inverse mult_commute by fastforce

lemma inverse_distrib: "inverse (a * b)  =  (inverse a) * (inverse b)"
  by (simp add: local.mult.inverse_distrib_swap mult_commute)

lemma inverse_divide [simp]: "inverse (a / b) = b / a"
  by (metis div_conv_mult_inverse inverse_distrib mult.commute mult.inverse_inverse)

end

abbreviation (input) npower :: "'a::{power,inverse} ⇒ nat ⇒ 'a"  ("(_⇧-⇧_)" [1000,999] 999) 
  where "npower x n ≡ inverse (x ^ n)"

end