Re: [isabelle] Lemmas about int_pow



 I will take care of this.  Thanks!

Clemens


On 29 October, 2013 11:28 CET, Joachim Breitner <mail at joachim-breitner.de> wrote:

> 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









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.