# Theory Int_Pow

```(*  Title:      HOL/Quotient_Examples/Int_Pow.thy
Author:     Ondrej Kuncar
Author:     Lars Noschinski
*)

theory Int_Pow
imports Main "HOL-Algebra.Group"
begin

(*
This file demonstrates how to restore Lifting/Transfer enviromenent.

We want to define int_pow (a power with an integer exponent) by directly accessing
the representation type "nat * nat" that was used to define integers.
*)

context monoid
begin

(* first some additional lemmas that are missing in monoid *)

lemma Units_nat_pow_Units [intro, simp]:
"a ∈ Units G ⟹ a [^] (c :: nat) ∈ Units G" by (induct c) auto

lemma Units_r_cancel [simp]:
"[| z ∈ Units G; x ∈ carrier G; y ∈ carrier G |] ==>
(x ⊗ z = y ⊗ z) = (x = y)"
proof
assume eq: "x ⊗ z = y ⊗ z"
and G: "z ∈ Units G"  "x ∈ carrier G"  "y ∈ carrier G"
then have "x ⊗ (z ⊗ inv z) = y ⊗ (z ⊗ inv z)"
by (simp add: m_assoc[symmetric] Units_closed del: Units_r_inv)
with G show "x = y" by simp
next
assume eq: "x = y"
and G: "z ∈ Units G"  "x ∈ carrier G"  "y ∈ carrier G"
then show "x ⊗ z = y ⊗ z" by simp
qed

lemma inv_mult_units:
"[| x ∈ Units G; y ∈ Units G |] ==> inv (x ⊗ y) = inv y ⊗ inv x"
proof -
assume G: "x ∈ Units G"  "y ∈ Units G"
then have "x ∈ carrier G"  "y ∈ carrier G" by auto
with G have "inv (x ⊗ y) ⊗ (x ⊗ y) = (inv y ⊗ inv x) ⊗ (x ⊗ y)"
with G show ?thesis by (simp del: Units_l_inv)
qed

lemma mult_same_comm:
assumes [simp, intro]: "a ∈ Units G"
shows "a [^] (m::nat) ⊗ inv (a [^] (n::nat)) = inv (a [^] n) ⊗ a [^] m"
proof (cases "m≥n")
have [simp]: "a ∈ carrier G" using ‹a ∈ _› by (rule Units_closed)
case True
then obtain k where *:"m = k + n" and **:"m = n + k" by (metis le_iff_add add.commute)
have "a [^] (m::nat) ⊗ inv (a [^] (n::nat)) = a [^] k"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
also have "… = inv (a [^] n) ⊗ a [^] m"
using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
finally show ?thesis .
next
have [simp]: "a ∈ carrier G" using ‹a ∈ _› by (rule Units_closed)
case False
then obtain k where *:"n = k + m" and **:"n = m + k"
have "a [^] (m::nat) ⊗ inv (a [^] (n::nat)) = inv(a [^] k)"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
also have "… = inv (a [^] n) ⊗ a [^] m"
using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units)
finally show ?thesis .
qed

lemma mult_inv_same_comm:
"a ∈ Units G ⟹ inv (a [^] (m::nat)) ⊗ inv (a [^] (n::nat)) = inv (a [^] n) ⊗ inv (a [^] m)"
by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)

context
includes int.lifting (* restores Lifting/Transfer for integers *)
begin

lemma int_pow_rsp:
assumes eq: "(b::nat) + e = d + c"
assumes a_in_G [simp, intro]: "a ∈ Units G"
shows "a [^] b ⊗ inv (a [^] c) = a [^] d ⊗ inv (a [^] e)"
proof(cases "b≥c")
have [simp]: "a ∈ carrier G" using ‹a ∈ _› by (rule Units_closed)
case True
then obtain n where "b = n + c" by (metis le_iff_add add.commute)
then have "d = n + e" using eq by arith
from ‹b = _› have "a [^] b ⊗ inv (a [^] c) = a [^] n"
by (auto simp add: nat_pow_mult[symmetric] m_assoc)
also from ‹d = _›  have "… = a [^] d ⊗ inv (a [^] e)"
by (auto simp add: nat_pow_mult[symmetric] m_assoc)
finally show ?thesis .
next
have [simp]: "a ∈ carrier G" using ‹a ∈ _› by (rule Units_closed)
case False
then obtain n where "c = n + b" by (metis le_iff_add add.commute nat_le_linear)
then have "e = n + d" using eq by arith
from ‹c = _› have "a [^] b ⊗ inv (a [^] c) = inv (a [^] n)"
by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
also from ‹e = _› have "… = a [^] d ⊗ inv (a [^] e)"
by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
finally show ?thesis .
qed

(*
This definition is more convinient than the definition in HOL/Algebra/Group because
it doesn't contain a test z < 0 when a [^] z is being defined.
*)

lift_definition int_pow :: "('a, 'm) monoid_scheme ⇒ 'a ⇒ int ⇒ 'a" is
"λG a (n1, n2). if a ∈ Units G ∧ monoid G then (a [^]⇘G⇙ n1) ⊗⇘G⇙ (inv⇘G⇙ (a [^]⇘G⇙ n2)) else 𝟭⇘G⇙"
unfolding intrel_def by (auto intro: monoid.int_pow_rsp)

(*
Thus, for example, the proof of distributivity of int_pow and addition
doesn't require a substantial number of case distinctions.
*)

lemma int_pow_dist:
assumes [simp]: "a ∈ Units G"
shows "int_pow G a ((n::int) + m) = int_pow G a n ⊗⇘G⇙ int_pow G a m"
proof -
{
fix k l m :: nat
have "a [^] l ⊗ (inv (a [^] m) ⊗ inv (a [^] k)) = (a [^] l ⊗ inv (a [^] k)) ⊗ inv (a [^] m)"
(is "?lhs = _")
by (simp add: mult_inv_same_comm m_assoc Units_closed)
also have "… = (inv (a [^] k) ⊗ a [^] l) ⊗ inv (a [^] m)"
also have "… = inv (a [^] k) ⊗ (a [^] l ⊗ inv (a [^] m))" (is "_ = ?rhs")
finally have "?lhs = ?rhs" .
}
then show ?thesis
by (transfer fixing: G) (auto simp add: nat_pow_mult[symmetric] inv_mult_units m_assoc Units_closed)
qed

end

lifting_update int.lifting
lifting_forget int.lifting

end

end
```