(** {1 Abstract monoids} Author: Martin Clochard *) (** {2 Abstract logic monoid} *) module Monoid (** Elements of the monoid. *) type t (** Neutral element. *) constant zero : t (** Composition law. *) function op (a b:t) : t (** Monoid properties. *) axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c axiom neutral : forall x:t. op x zero = x = op zero x end (** {2 Abstract monoid with aggregation} *) module MonoidSum use import seq.Seq clone import Monoid as M with axiom . function agg (f:'a -> t) (s:seq 'a) : t axiom agg_empty : forall f:'a -> t. agg f empty = zero axiom agg_sing : forall f,s:seq 'a. length s = 1 -> agg f s = f s[0] axiom agg_cat : forall f,s1 s2:seq 'a. agg f (s1 ++ s2) = op (agg f s1) (agg f s2) end (** {2 Definition of aggregation (refinement of MonoidSum} *) module MonoidSumDef use import seq.Seq use import seq.FreeMonoid (* TODO: do that refinement correctly ! *) clone import Monoid as M with axiom . let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t variant { length s } = if length s = 0 then zero else op (f s[0]) (agg f s[1 ..]) lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a) ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) } variant { length s1 } = if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2 clone MonoidSum as MS with type M.t = M.t, constant M.zero = M.zero, function M.op = M.op, goal M.assoc, goal M.neutral, function agg = agg, goal agg_empty, goal agg_sing, goal agg_cat end (** {2 Computable monoid} *) module ComputableMonoid clone export Monoid with axiom . (** Abstract routines computing operations in the monoid. *) val zero () : t ensures { result = zero } val op (a b:t) : t ensures { result = op a b } end