src/HOL/Library/Power_By_Squaring.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 69790 154cf64e403e permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*
```
```     2   File:     Power_By_Squaring.thy
```
```     3   Author:   Manuel Eberl, TU München
```
```     4
```
```     5   Fast computing of funpow (applying some functon n times) for weakly associative binary
```
```     6   functions using exponentiation by squaring. Yields efficient exponentiation algorithms on
```
```     7   monoid_mult and for modular exponentiation "b ^ e mod m" (and thus also for "cong")
```
```     8 *)
```
```     9 section \<open>Exponentiation by Squaring\<close>
```
```    10 theory Power_By_Squaring
```
```    11   imports Main
```
```    12 begin
```
```    13
```
```    14 context
```
```    15   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    16 begin
```
```    17
```
```    18 function efficient_funpow :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" where
```
```    19   "efficient_funpow y x 0 = y"
```
```    20 | "efficient_funpow y x (Suc 0) = f x y"
```
```    21 | "n \<noteq> 0 \<Longrightarrow> even n \<Longrightarrow> efficient_funpow y x n = efficient_funpow y (f x x) (n div 2)"
```
```    22 | "n \<noteq> 1 \<Longrightarrow> odd n \<Longrightarrow> efficient_funpow y x n = efficient_funpow (f x y) (f x x) (n div 2)"
```
```    23   by force+
```
```    24 termination by (relation "measure (snd \<circ> snd)") (auto elim: oddE)
```
```    25
```
```    26 lemma efficient_funpow_code [code]:
```
```    27   "efficient_funpow y x n =
```
```    28      (if n = 0 then y
```
```    29       else if n = 1 then f x y
```
```    30       else if even n then efficient_funpow y (f x x) (n div 2)
```
```    31       else efficient_funpow (f x y) (f x x) (n div 2))"
```
```    32   by (induction y x n rule: efficient_funpow.induct) auto
```
```    33
```
```    34 end
```
```    35
```
```    36 lemma efficient_funpow_correct:
```
```    37   assumes f_assoc: "\<And>x z. f x (f x z) = f (f x x) z"
```
```    38   shows "efficient_funpow f y x n = (f x ^^ n) y"
```
```    39 proof -
```
```    40   have [simp]: "f ^^ 2 = (\<lambda>x. f (f x))" for f :: "'a \<Rightarrow> 'a"
```
```    41     by (simp add: eval_nat_numeral o_def)
```
```    42   show ?thesis
```
```    43     by (induction y x n rule: efficient_funpow.induct[of _ f])
```
```    44        (auto elim!: evenE oddE simp: funpow_mult [symmetric] funpow_Suc_right f_assoc
```
```    45              simp del: funpow.simps(2))
```
```    46 qed
```
```    47
```
```    48 (*
```
```    49   TODO: This could be used as a code_unfold rule or something like that but the
```
```    50   implications are not quite clear. Would this be a good default implementation
```
```    51   for powers?
```
```    52 *)
```
```    53 context monoid_mult
```
```    54 begin
```
```    55
```
```    56 lemma power_by_squaring: "efficient_funpow (*) (1 :: 'a) = (^)"
```
```    57 proof (intro ext)
```
```    58   fix x :: 'a and n
```
```    59   have "efficient_funpow (*) 1 x n = ((*) x ^^ n) 1"
```
```    60     by (subst efficient_funpow_correct) (simp_all add: mult.assoc)
```
```    61   also have "\<dots> = x ^ n"
```
```    62     by (induction n) simp_all
```
```    63   finally show "efficient_funpow (*) 1 x n = x ^ n" .
```
```    64 qed
```
```    65
```
```    66 end
```
```    67
```
```    68 end
```