:: Seat Reservation Problem :::::::::::::::::::::::::::::::::::::::::::::::::::
:: Specification in Mizar 
:: by P. Rudnicki
:: We try to follow, as closely as possible, the specification given in:
:: "An Elementary Tutorial on Formal Specification and Verification
:: Using PVS 2", by Ricky W. Butler, NASA Technical Memorandum 108991 (Revised)
:: and "A Less Elementary Tutorial for the PVS Specification and Verification 
:: System" by J. M. Rushby and D. W. J. Stringer-Calvert, SRI, TR CSL 95-10
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

environ

 vocabularies BOOLE, RELAT_1, FUNCT_1, CAT_1, FUNCT_4, NEWTON, MCART_1,
      FUNCOP_1, FLT_DB_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      FUNCT_2, DOMAIN_1, FUNCT_4, FUNCOP_1, CAT_1, CQC_LANG, WELLFND1;
 constructors DOMAIN_1, FUNCT_4, CAT_1, CQC_LANG, WELLFND1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, CQC_LANG, FUNCOP_1;
 requirements SUBSET, BOOLE;
 theorems TARSKI, XBOOLE_0, XBOOLE_1, MCART_1, RELAT_1, RELSET_1, FUNCOP_1,
      ZFMISC_1, FUNCT_2, FUNCT_4, CQC_LANG, MSPF_1;
 schemes FRAENKEL;

begin

::::::::::::::::::: Basic definitions :::::::::::::::::::::::::::::::::::::::::

 consider row        being non empty set;
 consider position   being non empty set;

 set Seats = [:row, position:];

 consider Flights    being non empty set;
 consider Planes     being non empty set;
 consider Preference being non empty set;
 consider Passengers being non empty set;
 
 set seat_assignments = [:Seats, Passengers:];

 reserve flt  for Element of Flights,
         pl   for Element of Planes,
         pref for Element of Preference,
         pas  for Element of Passengers,
         a, b for Element of seat_assignments,
         se   for Element of Seats;
 
definition let a;
 func seat(a) -> Element of Seats  equals                             :L_seat:
   a`1;
  coherence;
 func pass(a) -> Element of Passengers  equals                        :L_pass:
   a`2;
  coherence;
end;

 set flight_assignments = bool seat_assignments;

definition
 mode flt_db is Function of Flights, flight_assignments;
end;

reserve db  for flt_db;

definition let db, flt;
 redefine func db.flt -> Relation of Seats, Passengers;
 coherence @proof end;
end;

theorem pase_lemma:
 a in db.flt implies seat(a) in dom (db.flt) & pass(a) in rng(db.flt)
@proof end;

definition 
 func initial_state -> flt_db   equals                                 :L_init:
   Flights --> {};
  coherence @proof end;
end;

::::::::::::::::::: Attributtes of airplanes ::::::::::::::::::::::::::::::::::

 consider Seat_exists being Subset of [:Planes, Seats:];
 consider Meets_pref being Subset of [:Planes, Seats, Preference:];

definition let pl, se;
 pred seat_exists pl, se   means 
      [pl, se] in Seat_exists;
           let pref;
 pred meets_pref pl, se, pref   means 
      [pl, se, pref] in Meets_pref;
end;

 consider aircraft    being Function of Flights, Planes;

::::::::::::::::::: Operations ::::::::::::::::::::::::::::::::::::::::::::::::

definition let flt, pas, db;
 func Cancel_assn(flt, pas, db) -> flt_db   equals                   :L_Cancel:
   db +* (flt .--> {aa where aa is Element of seat_assignments : 
                            aa in db.flt & pass(aa) <> pas});
   coherence @proof end;
end;

definition let db, flt, pref;
 pred pref_filled db, flt, pref   means                         :L_pref_filled:
  seat_exists aircraft.flt, se & meets_pref aircraft.flt, se, pref 
    implies ex a st a in db.flt & seat(a) = se;
end;

definition let db , flt, pref; assume
A: not pref_filled db, flt, pref;
 func Ns_choice (db, flt, pref) -> non empty Subset of Seats   equals :L_Ns_ch:
  {se where se is Element of Seats : 
          seat_exists aircraft.flt, se & meets_pref aircraft.flt, se, pref &
          not se in dom (db.flt)};
 coherence @proof end;
end;

definition let db , flt, pref; 
 func Next_seat (db, flt, pref) -> Element of Seats    equals     :L_Next_seat:
  choose Ns_choice (db, flt, pref);
  coherence @proof end;
end;

theorem Next_seat_prop:
 not pref_filled db, flt, pref implies
      seat_exists aircraft.flt, Next_seat(db, flt, pref)      :: Next_seat_ax
& not Next_seat(db, flt, pref) in dom (db.flt)                :: Next_seat_ax_2
&     meets_pref aircraft.flt, Next_seat(db,flt,pref), pref   :: Next_seat_ax_3
@proof end;

definition let pas, flt, db;
 pred pass_on_flight pas, flt, db   means                         :L_pass_on_f:
  pas in rng (db.flt);
end;

definition let db, flt, pas, pref;
 func Make_assn(flt, pas, pref, db) -> flt_db   means                  :L_Make:
  it = db if pref_filled db, flt, pref or pass_on_flight pas, flt, db
          otherwise
  it = db +* (flt .--> (db.flt \/ {[Next_seat(db, flt, pref), pas]}));
 consistency;
 existence @proof end;
 uniqueness;
end;

definition let flt, pas, db; assume
A: pas in rng (db.flt);
 func Look_up (flt, pas, db) -> Element of Seats   means            :L_Look_up:
  ex a st a = choose {b where b is Element of seat_assignments : 
                        b in db.flt & pass(b) = pas}
        & a in db.flt & pass(a) = pas & it = seat(a);
 existence @proof end;
 uniqueness;
end;

::::::::::::::::::: Invariants ::::::::::::::::::::::::::::::::::::::::::::::::

definition let db;
 pred Existence db   means                                        :L_Existence:
  for a, flt st a in db.flt holds seat_exists aircraft.flt, seat(a);
 pred Uniqueness db  means                                       :L_Uniqueness:
  for a, b, flt st a in db.flt & b in db.flt & pass(a) = pass(b) holds a = b;
 pred one_per_seat db means                                   :L_one_per_seat:
  for a, b, flt st a in db.flt & b in db.flt & seat(a) = seat(b) holds a = b;
end;

definition let db;
 pred db_invariant db   means                                        :L_db_inv:
  Existence db & Uniqueness db;
end;

theorem Cancel_assn_inv:
 db_invariant db implies db_invariant Cancel_assn(flt, pas, db)
@proof end;

theorem MAe: 
 Existence db implies Existence Make_assn(flt, pas, pref, db)
@proof end;

theorem MAu: 
 Uniqueness db implies Uniqueness Make_assn(flt, pas, pref, db)
@proof end;

theorem Make_assn_inv:
 db_invariant db implies db_invariant Make_assn(flt, pas, pref, db)
@proof end;

theorem initial_state_inv:
 db_invariant initial_state
@proof end;

theorem Cancel_inv_one_per_seat:
 one_per_seat db implies one_per_seat Cancel_assn(flt, pas, db)
@proof end;

theorem Make_inv_one_per_seat: 
 one_per_seat db implies one_per_seat Make_assn(flt, pas, pref, db)
@proof end;

theorem initial_one_per_seat:
 one_per_seat initial_state
  @proof end;

::::::::::::::::::: Putative theorems :::::::::::::::::::::::::::::::::::::::::

theorem Make_cancel:
 not pass_on_flight pas, flt, db implies
  Cancel_assn(flt, pas, Make_assn(flt, pas, pref, db)) = db
@proof end;

theorem Cancel_putative:
 not (a in Cancel_assn(flt, pas, db).flt & pass(a) = pas)
@proof end;

theorem Make_putative:
 not pref_filled db, flt, pref implies
  ex a st a in Make_assn(flt, pas, pref,db).flt & pass(a) = pas
@proof end;  

theorem Lp2_lem:
 not (pref_filled db, flt, pref or pass_on_flight pas, flt, db)
  implies for a st a in Make_assn(flt,pas,pref,db).flt & pass(a) = pas 
           holds seat(a) = Next_seat(db, flt, pref)
@proof end;

theorem Lookup_putative:
 not (pref_filled db, flt, pref or pass_on_flight pas, flt, db)
  implies meets_pref aircraft.flt,
                     Look_up(flt, pas, Make_assn(flt, pas, pref, db)),
                     pref
@proof end;