*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Lemmas about int_pow*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Tue, 29 Oct 2013 11:28:07 +0100

Hi, I had a look at my old Free-Groups AFP entry, where I had some partial refactoring in my local branch. While continuing a bit on it, I had a need for these lemmas, and I believe they should go into the Algebra/Groups (also attached): lemma (in group) int_pow_one' [simp]: "x ∈ carrier G ⟹ x (^) (1::int) = x" by (simp add: int_pow_def2) lemma (in group) int_pow_neg [simp]: "x ∈ carrier G ⟹ x (^) (-i::int) = inv (x (^) i)" by (simp add: int_pow_def2) lemma (in group) int_pow_closed [intro, simp]: "x ∈ carrier G ==> x (^) (i::int) ∈ carrier G" by (simp add: int_pow_def2) lemma (in group) int_pow_add [simp]: assumes "x ∈ carrier G" shows "x (^) (i + j::int) = x (^) i ⊗ x (^) j" proof- (* A simple solver for equations with inv and ⊗ *) have [simp]:"⋀ a b c. a ∈ carrier G ⟹ b ∈ carrier G ⟹ c ∈ carrier G ⟹ a = inv b ⊗ c ⟷ c = b ⊗ a" by (metis inv_equality l_inv_ex l_one m_assoc r_inv) have [simp]:"⋀ a b c. a ∈ carrier G ⟹ b ∈ carrier G ⟹ c ∈ carrier G ⟹ a = b ⊗ inv c ⟷ b = a ⊗ c" by (metis inv_equality l_inv_ex l_one m_assoc r_inv) have [simp]:"- i - j = - j - i" by simp from assms show ?thesis by (auto simp add: int_pow_def2 nat_add_distrib[symmetric] nat_pow_mult inv_mult_group[symmetric]) qed The [simp] on the last lemma is probably debatable, I don’t have strong opinions about it. Greetings, Joachim -- Joachim “nomeata” Breitner mail at joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata at joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata at debian.org

theory Submission imports "~~/src/HOL/Algebra/Group" begin lemma (in group) int_pow_one' [simp]: "x \<in> carrier G \<Longrightarrow> x (^) (1::int) = x" by (simp add: int_pow_def2) lemma (in group) int_pow_neg [simp]: "x \<in> carrier G \<Longrightarrow> x (^) (-i::int) = inv (x (^) i)" by (simp add: int_pow_def2) lemma (in group) int_pow_closed [intro, simp]: "x \<in> carrier G ==> x (^) (i::int) \<in> carrier G" by (simp add: int_pow_def2) lemma (in group) int_pow_add [simp]: assumes "x \<in> carrier G" shows "x (^) (i + j::int) = x (^) i \<otimes> x (^) j" proof- (* A simple solver for equations with inv and \<otimes> *) have [simp]:"\<And> a b c. a \<in> carrier G \<Longrightarrow> b \<in> carrier G \<Longrightarrow> c \<in> carrier G \<Longrightarrow> a = inv b \<otimes> c \<longleftrightarrow> c = b \<otimes> a" by (metis inv_equality l_inv_ex l_one m_assoc r_inv) have [simp]:"\<And> a b c. a \<in> carrier G \<Longrightarrow> b \<in> carrier G \<Longrightarrow> c \<in> carrier G \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c" by (metis inv_equality l_inv_ex l_one m_assoc r_inv) have [simp]:"- i - j = - j - i" by simp from assms show ?thesis by (auto simp add: int_pow_def2 nat_add_distrib[symmetric] nat_pow_mult inv_mult_group[symmetric]) qed end

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Lemmas about int_pow***From:*Clemens Ballarin

- Previous by Date: Re: [isabelle] Evaluation of record expressions
- Next by Date: [isabelle] Problems with elder Isabelle Versions under MacOSX Maverick
- Previous by Thread: [isabelle] WRLA 2014 Call for papers
- Next by Thread: Re: [isabelle] Lemmas about int_pow
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list