Quelle  imputations.pvs   Sprache: PVS

%---------------------------------------------------------------------
% A formal theory of cooperative TU-games in PVS 4.2 
%
% Author: Erik Martin-Dorel,
% University Montpellier 2 & University of Perpignan
%
%   THEORY imputations[U,N,v]
%
%   Version 1.0    2009/05/05    Initial version
%   Version 1.1    2009/05/07    subset_core_I added
%   Version 1.2    2009/05/10    Identifiers renamed
%
% This work has been done at the University of Perpignan
% within the Master's Thesis, under the supervision of
% Marc Daumas and Annick Truffert, with the help of Michel Ventou
%
% This library is available under GNU Lesser General Public License,
% either version 3 of the Licence, or any later version
%---------------------------------------------------------------------


imputations[U: TYPE+,     (IMPORTING players_set[U])
            N: players_set, (IMPORTING coalition_fun[U,N])
            v: coalition_fun]: THEORY
 BEGIN

  IMPORTING players_set[U],
            coalition_fun[U,N]

  % set_vect: TYPE = setof[[(N) -> real]]

  x: VAR [(N) -> real]
  i: VAR (N)
  S: VAR powset % = setof[(N)] = [(N) -> bool]

  % feasible payoffs
  setFP: set_vect = {x | tot(fullN, x) <= v(fullN)}

  % preimputations
  setPI: set_vect = {x | tot(fullN, x) = v(fullN)}

  % imputations
  setI: set_vect = {x | member(x, setPI) AND FORALL i: x(i) >= v(singleton(i))}

  % core: set_vect = {x: (setPI) | FORALL S: tot(S, x) >= v(S)}
  core: set_vect = {x | member(x, setPI) AND FORALL S: tot(S, x) >= v(S)}

  subset_core_I: LEMMA subset?(core, setI)

  subset_I_PI:   LEMMA subset?(setI, setPI)
  subset_PI_FP:  LEMMA subset?(setPI, setFP)

 END imputations


%---------------------------------------------------------------------
% License for use and distribution
%
% Copyright (C) 2009 Erik Martin-Dorel.
%
% GNU LGPL information:
% ---------------------
%
% This library is free software: you can redistribute it and/or
% modify it under the terms of the GNU Lesser General Public License
% as published by the Free Software Foundation, either version 3 of
% the License, or (at your option) any later version.
%
% This library is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU Lesser General Public
% License along with this library.
% If not, see <http://www.gnu.org/licenses/>.
%---------------------------------------------------------------------