src/HOL/ex/Classpackage.thy
changeset 19933 16a5037f2d25
parent 19928 cb8472f4c5fd
child 19951 d58e2c564100
equal deleted inserted replaced
19932:63bd0eeb4e0d 19933:16a5037f2d25
   164 lemma (in monoid) nat_pow_mult:
   164 lemma (in monoid) nat_pow_mult:
   165   "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
   165   "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
   166 proof (induct n)
   166 proof (induct n)
   167   case 0 with neutl npow_def show ?case by simp
   167   case 0 with neutl npow_def show ?case by simp
   168 next
   168 next
   169   case (Suc n) with prems assoc npow_def show ?case by simp
   169   case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
   170 qed
   170 qed
   171 
   171 
   172 lemma (in monoid) nat_pow_pow:
   172 lemma (in monoid) nat_pow_pow:
   173   "npow n (npow m x) = npow (n * m) x"
   173   "npow n (npow m x) = npow (n * m) x"
   174 using npow_def nat_pow_mult by (induct n) simp_all
   174 using npow_def nat_pow_mult by (induct n) simp_all