title: Expressing a simple declarative proof about exponents in Isar
body: <p>I'm attempting to write a simple proof about integer exponents in isar.</p>
  
  <p>I've written the argument I want to make in the commented area, but I'm having a very hard time figuring out how to express it. I've been studying <code>src/HOL/Int.thy</code> but I either can't find an example proof along these lines or don't understand what I'm looking at yet. :) </p>
  
  <pre><code>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
  </code></pre>
  
  <p>This isn't a homework assignment, btw. I'm not in school. :)</p>
  
  <p><strong>update</strong>: my final version, based on Alexander's answer, below:</p>
  
  <pre><code>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
  </code></pre>