%---------------------------------------------------------------------
% A formal theory of cooperative TU-games in PVS 4.2
%
% Author: Erik Martin-Dorel,
% University Montpellier 2 & University of Perpignan
%
% THEORIES players_set[U] and
% coalition_fun[U,N]
%
% Version 1.0 2009/05/01 Initial version
% Version 1.1 2009/05/10 Identifiers renamed
% Version 1.2 2009/05/14 Lemmas added
% Version 1.3 2009/10/03 Conversion avoided in Judgement proof
%
% 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
%---------------------------------------------------------------------
%players_set[U: TYPE+]: THEORY
% BEGIN
% elt: U
% players_set: TYPE+ = non_empty_finite_set[U] CONTAINING singleton(elt)
% END players_set
coalition_fun[U: TYPE+, (IMPORTING players_set[U])
N: players_set]: THEORY
BEGIN
IMPORTING players_set[U]
powset: TYPE = setof[(N)] % rather than (powerset[U](N))
fullN: powset = fullset[(N)]
v: VAR [powset -> real]
S: VAR powset
x, y: VAR [(N) -> real]
i: VAR (N)
c: VAR real
a: VAR nzreal
zero_fun(S): real = 0
coalition_fun?(v): bool = v(emptyset) = 0
coalition_fun: TYPE+ = (coalition_fun?) CONTAINING zero_fun
subsets_are_finite: JUDGEMENT setof[(N)] SUBTYPE_OF finite_set[(N)]
IMPORTING %finite_sets@finite_sets_sum[(N),real,0,+],
finite_sets@finite_sets_sum_real[(N)]
tot(S, x): real = sum(S, x)
tot_S_0: LEMMA tot(S, LAMBDA i: 0) = 0
tot_distrib: LEMMA tot(S, LAMBDA i: x(i) + y(i)) = tot(S, x) + tot(S, y)
tot_mult_const: LEMMA tot(S, LAMBDA i: c * x(i)) = c * tot(S,x)
tot_distrib_sub: LEMMA tot(S, LAMBDA i: x(i) - y(i)) = tot(S, x) - tot(S, y)
tot_div_const: LEMMA tot(S, LAMBDA i: x(i) / a) = tot(S,x) / a
set_vect: TYPE = setof[[(N) -> real]]
END coalition_fun
%---------------------------------------------------------------------
% 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/>.
%---------------------------------------------------------------------
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
