表达关于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)。