(* 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)" by (simp add: m_assoc) (simp add: m_assoc [symmetric]) 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" by (metis le_iff_add add.commute nat_le_linear) 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)" by (simp add: mult_same_comm) also have "… = inv (a [^] k) ⊗ (a [^] l ⊗ inv (a [^] m))" (is "_ = ?rhs") by (simp add: m_assoc Units_closed) 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