Revision ebafbc92ad9b52ae775ab3bd4f9ddbb32bd51e73 authored by Pierre-Yves Strub on 05 July 2014, 22:13:30 UTC, committed by Pierre-Yves Strub on 05 July 2014, 22:13:30 UTC
1 parent 7c527a4
Sum.ec
(* --------------------------------------------------------------------
* Copyright IMDEA Software Institute / INRIA - 2013, 2014
* -------------------------------------------------------------------- *)
require import FSet. import Interval.
require import Int.
require import Real.
require import Monoid.
(* temporary workaround *)
op intval : int -> int -> int set = interval.
lemma intval_def i i1 i2:
mem i (intval i1 i2) <=> (i1<= i /\ i <= i2)
by [].
lemma intval_card_0 i1 (i2 : int):
i1 <= i2 =>
card (intval i1 i2) = i2 - i1 + 1
by [].
lemma intval_card_1 (i1 i2:int):
i2 < i1 => card (intval i1 i2) = 0
by [].
op int_sum: (int -> real) -> int set -> real = Mrplus.sum.
pred is_cnst (f : int -> 'a) = forall i1 i2, f i1 = f i2.
lemma int_sum_const (f : int -> real) (s: int set):
is_cnst f => int_sum f s = (card s)%r * f 0.
proof strict.
by intros=> is_cnst;
rewrite /int_sum (Mrplus.NatMul.sum_const (f 0)) // => x hh;
apply is_cnst.
qed.
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...