monoid.mlw 1.93 KB
 Martin Clochard committed Aug 29, 2014 1 2 3 4 5 6 7 `````` (** {1 Abstract monoids} Author: Martin Clochard *) (** {2 Abstract logic monoid} *) module Monoid `````` Andrei Paskevich committed Oct 22, 2014 8 `````` `````` Martin Clochard committed Aug 29, 2014 9 10 `````` (** Elements of the monoid. *) type t `````` Andrei Paskevich committed Oct 22, 2014 11 `````` `````` Martin Clochard committed Aug 29, 2014 12 13 14 15 `````` (** Neutral element. *) constant zero : t (** Composition law. *) function op (a b:t) : t `````` Andrei Paskevich committed Oct 22, 2014 16 `````` `````` Martin Clochard committed Aug 29, 2014 17 18 19 `````` (** 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 `````` Andrei Paskevich committed Oct 22, 2014 20 `````` `````` Martin Clochard committed Aug 29, 2014 21 22 23 24 ``````end (** {2 Abstract monoid with aggregation} *) module MonoidSum `````` Andrei Paskevich committed Oct 22, 2014 25 `````` `````` Martin Clochard committed Aug 29, 2014 26 27 28 29 `````` use import list.List use import list.Append use import HighOrd clone import Monoid as M `````` Andrei Paskevich committed Oct 22, 2014 30 `````` `````` Martin Clochard committed Aug 29, 2014 31 32 33 34 35 36 37 38 `````` (** Axiomatized definition of the monoidal aggregation of elements obtained from a list: using infix notation for the monoid law, [sum f [a_1;a_2;...;a_n]] is [a_1 op a_2 ... op a_n]. This axiomatization must be kept until the monoid is instantiated *) function sum (f:'a -> t) (l:list 'a) : t axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero axiom sum_def_cons : forall f:'a -> t,x,q. sum f (Cons x q) = op (f x) (sum f q) `````` Andrei Paskevich committed Oct 22, 2014 39 `````` `````` Martin Clochard committed Aug 29, 2014 40 41 42 43 44 `````` (** Consequence of associativity *) let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit ensures { sum f (l ++ r) = op (sum f l) (sum f r) } variant { l } = match l with Cons _ q -> sum_append f q r | _ -> () end `````` Andrei Paskevich committed Oct 22, 2014 45 `````` `````` Martin Clochard committed Aug 29, 2014 46 47 48 49 50 51 ``````end (** {2 Definition of aggregation} *) module MonoidSumDef use import list.List use import HighOrd `````` Andrei Paskevich committed Oct 22, 2014 52 `````` `````` Martin Clochard committed Aug 29, 2014 53 54 55 56 57 58 59 60 61 62 63 64 `````` namespace M type t constant zero : t function op (a b:t) : t end function sum (f:'a -> M.t) (l:list 'a) : M.t = match l with | Nil -> M.zero | Cons x q -> M.op (f x) (sum f q) end clone export MonoidSum with type M.t = M.t,constant M.zero = M.zero, function M.op = M.op,function sum = sum, goal sum_def_nil,goal sum_def_cons `````` Andrei Paskevich committed Oct 22, 2014 65 `````` `````` Martin Clochard committed Aug 29, 2014 66 67 68 69 ``````end (** {2 Computable monoid} *) module ComputableMonoid `````` Andrei Paskevich committed Oct 22, 2014 70 `````` `````` Martin Clochard committed Aug 29, 2014 71 `````` clone export Monoid `````` Andrei Paskevich committed Oct 22, 2014 72 `````` `````` Martin Clochard committed Aug 29, 2014 73 74 `````` (** Abstract routines computing operations in the monoid. *) val zero () : t ensures { result = zero } `````` Andrei Paskevich committed Oct 22, 2014 75 `````` `````` Martin Clochard committed Aug 29, 2014 76 `````` val op (a b:t) : t ensures { result = op a b } `````` Andrei Paskevich committed Oct 22, 2014 77 `````` `````` Martin Clochard committed Aug 29, 2014 78 79 ``````end ``````