merc_syntax 2.0.0

% Author(s): Aad Mathijssen, Jeroen Keiren
% Copyright: see the accompanying file COPYING or copy at
% https://github.com/mCRL2org/mCRL2/blob/master/COPYING
%
% Distributed under the Boost Software License, Version 1.0.
% (See accompanying file LICENSE_1_0.txt or copy at
% http://www.boost.org/LICENSE_1_0.txt)
%
% Specification of the FSet data sort, denoting finite sets.
% Note that the data type relies on the underlying data type S to have a total ordering.
%
% FSet(S) was initially specified using:
%
% sort FSet(S) <"fset"> = struct {} <"empty"> | @fset_cons <"cons_"> : S <"left"> # FSet(S) <"right">;
%
% But this does not work as the automatically generated relation <= is not the subset relation as
% would be expected. The same holds for all other comparison operators. Therefore an explicit definition
% is put into place (Jan Friso Groote, April 2017; problem reported by Tim Willemse).
%
% Also changed @fset_insert and @fset_cons. @fset_insert generates unordered lists. @fset_cons is used
% for ordered lists only. This has especially an effect when generating finite sets using quantifiers
% and sums. When @fset_cons is a constructor unordered lists are generated, for which the rewrite rules
% below do not work properly.

cons {} : FSet(S);
     @fset_insert: S # FSet(S) -> FSet(S);

map  @fset_cons : S # FSet(S) -> FSet(S);
     @fset_cinsert: S # Bool # FSet(S) -> FSet(S);
     in: S # FSet(S) -> Bool;
%     @fset_union : (S -> Bool) # (S -> Bool) # FSet(S) # FSet(S) -> FSet(S);
%     @fset_inter: (S -> Bool) # (S -> Bool) # FSet(S) # FSet(S) -> FSet(S);
     -: FSet(S) # FSet(S) -> FSet(S);
     + : FSet(S) # FSet(S) -> FSet(S);
     * : FSet(S) # FSet(S) -> FSet(S);
     # : FSet(S) -> Nat;
     pick: FSet(S) -> S;

var d:S;
    e:S;
    s:FSet(S);
    t:FSet(S);
eqn {} == @fset_cons(d, s)  =  false;
    @fset_cons(d, s) == {}  =  false;
    @fset_cons(d, s) == @fset_cons(e, t)  =  (d == e) && (s == t);
    {} <= @fset_cons(d, s)  =  true;
    @fset_cons(d, s) <= {}  =  false;
    @fset_cons(d, s) <= @fset_cons(e, t)  =  if(d < e, false, if(d == e, s <= t, @fset_cons(d, s) <= t));
    {} < @fset_cons(d, s)  =  true;
    @fset_cons(d, s) < {}  =  false;
    @fset_cons(d, s) < @fset_cons(e, t)  =  if(d < e, false, if(d == e, s < t, @fset_cons(d, s) <= t));
    @fset_insert(d, {})  =  @fset_cons(d, {});
    @fset_insert(d, @fset_cons(d, s))  =  @fset_cons(d, s);
    d < e  ->  @fset_insert(d, @fset_cons(e, s))  =  @fset_cons(d, @fset_cons(e, s));
    e < d  ->  @fset_insert(d, @fset_cons(e, s))  =  @fset_cons(e, @fset_insert(d, s));
    @fset_cinsert(d, false, s)  =  s;
    @fset_cinsert(d, true, s)  =  @fset_insert(d, s);
    in(d, {})  =  false;
    in(d,@fset_cons(e,s)) = (d == e) || in(d,s);
% The rule below is added such that set membership can still be calculated although the set elements cannot be effectively ordered.
    in(d,@fset_insert(e,s)) = (d == e) || in(d,s);
    s - {} = s;
    {} - t = {};
    @fset_cons(d,s) - @fset_cons(d,t) = s - t;
    d < e -> @fset_cons(d,s) - @fset_cons(e,t) = @fset_cons(d, s - @fset_cons(e,t));
    e < d -> @fset_cons(d,s) - @fset_cons(e,t) = @fset_cons(d,s) - t;
    s + {} = s;
    {} + t = t;
    @fset_cons(d,s) + @fset_cons(d,t) = @fset_cons(d, s + t);
    d < e -> @fset_cons(d,s) + @fset_cons(e,t) = @fset_cons(d, s + @fset_cons(e,t));
    e < d -> @fset_cons(d,s) + @fset_cons(e,t) = @fset_cons(e, @fset_cons(d,s) + t);
    s * {} = {};
    {} * t = {};
    @fset_cons(d,s) * @fset_cons(d,t) = @fset_cons(d, s * t);
    d < e -> @fset_cons(d,s) * @fset_cons(e,t) = s * @fset_cons(e,t);
    e < d -> @fset_cons(d,s) * @fset_cons(e,t) = @fset_cons(d,s) * t;
    #({}) = @c0;
    #(@fset_cons(d,s)) = @cNat(succ(#(s)));
% It is odd that the rule below has to be added separately.
    s != t = !(s == t);
    pick(@fset_cons(d,s)) = d;