Algebraic structures in Isabelle using Locales

Alg.thy

theory Alg
 imports Main
begin 

text‹
  Define algebraic structures as Locales
›
locale monoid =
  fixes M and composition (infixl "⋅" 70) and unit ("𝟭")
  assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
    and unit_closed [intro, simp]: "𝟭 ∈ M"
    and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
    and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a"
    and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"

locale group = monoid + 
  fixes inv 
  assumes
        left_inv : "⟦x ∈ M ; inv x ∈ M ⟧ ⟹ inv x ⋅ x = unit "
    and right_inf: "⟦x ∈ M ; inv x ∈ M ⟧ ⟹ x ⋅ (inv x) = unit"

text‹
  Define the set ℕ⇩4, addition mod 4, and inverse for ℕ⇩4
›
definition N_4 :: "nat set" where "N_4 = {x | x :: nat . x < 4 }"

definition op :: "nat ⇒ nat ⇒ nat" where
  "op n m = (n + m) mod 4"

fun n4inv :: "nat ⇒ nat" where
  "n4inv 0 = 0" |
  "n4inv (Suc 0) = 3" |
  "n4inv (Suc (Suc 0)) = 2" |
  "n4inv (Suc (Suc (Suc 0))) = 1" |
  "n4inv _ = 4"

(* a lemma to prove n4inv is the left inverse *)
lemma n4inv_correct:"∀x. x ∈ {0, 1, 2, 3} ⟶
        n4inv x ∈ {0, 1, 2, 3} ⟶
        (n4inv x + x) mod 4 = 0"
  apply(auto simp add :  numeral_2_eq_2)+ 
  apply(simp add: numeral_3_eq_3)+
  done

(* a simp rule to unfold N_4 *)
lemma n4eq[simp]:"N_4 = {0,1,2,3}" unfolding N_4_def by auto

text‹
  Show that (ℕ⇩4,+,0) is a monoid 
›
interpretation m : monoid "N_4" op 0 
  unfolding monoid_def op_def by simp

text‹
  Show that (ℕ⇩4,+,0,inv) is a group
›
interpretation group "N_4" op 0 n4inv
proof -

  (* show it is a monoid, using previous proof *)
  have monoid_instance:"monoid {0, 1, 2, 3} op 0" using m.monoid_axioms by simp

  (* show it obeys group axioms *)
  have left_inv : 
      "∀ x .x ∈ N_4 ⟶
      n4inv x ∈ N_4 ⟶
      op (n4inv x) x = 0" 
    using n4inv_correct op_def by simp 

  have right_inv :
      "∀ x .x ∈ N_4 ⟶
      n4inv x ∈ N_4 ⟶
      op x (n4inv x) = 0" 
    using n4inv_correct add.commute op_def by simp

  have group_instance:"group_axioms N_4 op 0 n4inv" 
    apply(unfold group_axioms_def) using N_4_def left_inv right_inv by simp 

  (* combine the monoid and group instance proofs *)
  show "group N_4 op 0 n4inv" 
    unfolding group_def 
    using monoid_instance group_instance 
    by simp
qed

end