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