[isabelle] Lemmas about int_pow



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
Description: This is a digitally signed message part



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