表達關於Isar中指數的簡單陳述性證明

Question

我正在嘗試編寫關於isar中整數指數的簡單證明。

我已經寫了我想在評論區域做出的論點，但我很難搞清楚如何表達它。我一直在研究src/HOL/Int.thy，但是我無法找到一個沿着這些線路的例子證明，或者不明白我在看什麼。 :)

theory Exponents 
imports Main 
begin 

lemma rMulComm: "(a*b ::int) = (b*a ::int)" 
by (rule Groups.ab_semigroup_mult_class.mult.commute) 

lemma rExpMul: "((a^b)^c ::int) = (a^(b*c) ::int)" 
by (rule Int.zpower_zpower) 

theorem HELP: "((a^b)^c ::int) = ((a^c)^b :: int)" 
    (* 0. (a^b)^c 
     1. a^(b*c) by rExpMul 
     2. a^(c*b) by rMulComm 
     3. (a^c)^b by rExpMul *) 
end 

這不是一個家庭作業，順便說一句。我不在學校。 :)

更新：我的最終版本的基礎上，亞歷山大的回答，如下：

theorem "((a^b)^c ::int) = ((a^c)^b :: int)" 
proof - 
    have "(a^b)^c = a^(b*c)" by (simp only: rExpMul) 
    hence " ... = a^(c*b)" by (simp only: rMulComm) 
    thus "(a^b)^c = (a^c)^b" by (simp only: rExpMul) 
qed 

Answer 1

問題有做的定理HELP類型的b和c以及在引理rExpMul：運營商^的指數是一個自然數。因此指定爲整數的rMulComm不能用於證明該定理。重申它自然數

lemma rMulComm: "(a * b :: nat) = (b * a :: nat)" 

後證明直接進入：

theorem HELP: "((a^b)^c ::int) = ((a^c)^b :: int)" 
proof - 
    have "(a^b)^c = a^(b * c)" by (simp only: rExpMul) 
    also have "… = a^(c * b)" by (simp only: rMulComm) 
    finally show ?thesis by (simp only: rExpMul) 
qed 

和可縮短至僅僅by (simp only: rExpMul rMulComm)。