src/HOL/Power.thy
 changeset 62481 b5d8e57826df parent 62366 95c6cf433c91 child 63040 eb4ddd18d635
equal inserted replaced
`     4 *)`
`     4 *)`
`     5 `
`     5 `
`     6 section \<open>Exponentiation\<close>`
`     6 section \<open>Exponentiation\<close>`
`     7 `
`     7 `
`     8 theory Power`
`     8 theory Power`
`     9 imports Num Equiv_Relations`
`     9 imports Num`
`    10 begin`
`    10 begin`
`    11 `
`    11 `
`    12 subsection \<open>Powers for Arbitrary Monoids\<close>`
`    12 subsection \<open>Powers for Arbitrary Monoids\<close>`
`    13 `
`    13 `
`    14 class power = one + times`
`    14 class power = one + times`
`   230   then show "x dvd (x ^ n)" by simp`
`   230   then show "x dvd (x ^ n)" by simp`
`   231 qed`
`   231 qed`
`   232 `
`   232 `
`   233 end`
`   233 end`
`   234 `
`   234 `
`   235 class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors`
`   235 context semiring_1_no_zero_divisors`
`   236 begin`
`   236 begin`
`   237 `
`   237 `
`   238 subclass power .`
`   238 subclass power .`
`   239 `
`   239 `
`   240 lemma power_eq_0_iff [simp]:`
`   240 lemma power_eq_0_iff [simp]:`
`   246   by (induct n) auto`
`   246   by (induct n) auto`
`   247 `
`   247 `
`   248 lemma zero_eq_power2 [simp]:`
`   248 lemma zero_eq_power2 [simp]:`
`   249   "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"`
`   249   "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"`
`   250   unfolding power2_eq_square by simp`
`   250   unfolding power2_eq_square by simp`
`   258 `
`   251 `
`   259 end`
`   252 end`
`   260 `
`   253 `
`   261 context ring_1`
`   254 context ring_1`
`   262 begin`
`   255 begin`
`   304 `
`   297 `
`   305 end`
`   298 end`
`   306 `
`   299 `
`   307 context ring_1_no_zero_divisors`
`   300 context ring_1_no_zero_divisors`
`   308 begin`
`   301 begin`
`   311 `
`   302 `
`   312 lemma power2_eq_1_iff:`
`   303 lemma power2_eq_1_iff:`
`   313   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"`
`   304   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"`
`   314   using square_eq_1_iff [of a] by (simp add: power2_eq_square)`
`   305   using square_eq_1_iff [of a] by (simp add: power2_eq_square)`
`   315 `
`   306 `
`   849     apply (subst card_Un_disjoint, auto)`
`   840     apply (subst card_Un_disjoint, auto)`
`   850     done`
`   841     done`
`   851 qed`
`   842 qed`
`   852 `
`   843 `
`   853 `
`   844 `
`   918 subsection \<open>Code generator tweak\<close>`
`   845 subsection \<open>Code generator tweak\<close>`
`   919 `
`   846 `
`   920 code_identifier`
`   847 code_identifier`
`   921   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith`
`   848   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith`
`   922 `
`   849 `