Commit 953fa909 authored by Jean-Christophe's avatar Jean-Christophe

new lemma Power_s_alt in Exponentiation

parent 2b88dc1a
......@@ -38,10 +38,6 @@ module PrefixSumRec
(** The step must be a power of 2 *)
predicate is_power_of_2 (x:int) = exists k:int. (k >= 0 /\ x = power 2 k)
(** Needed for proving is_power_of_2_1.
Can it be added to the theory Power? *)
lemma is_power_of_2_0:
forall k:int. k > 0 -> power 2 k = 2 * power 2 (k-1)
lemma is_power_of_2_1:
forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x
......
......@@ -190,7 +190,8 @@ theory Exponentiation
type t
constant one : t
function (*) t t : t
clone algebra.CommutativeMonoid with type t = t, constant unit = one, function op = (*)
clone algebra.CommutativeMonoid
with type t = t, constant unit = one, function op = (*)
function power t int : t
......@@ -198,6 +199,8 @@ theory Exponentiation
axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n
lemma Power_s_alt: forall x: t, n: int. n > 0 -> power x n = x * power x (n-1)
lemma Power_1 : forall x : t. power x 1 = x
lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment