|
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 |