th_E: THEORY

%%%
%%% This exercise comes from the NASA/Langley PVS school exercise set
%%% from August 1998.  Try GROUND to finish off simple logic-arithmetic
%%% propositions.  If GROUND fails, try ASSERT. To complete the
%%% logic puzzle in this theory, you will need to use TYPEPRED to expose
%%% information about the individuals.
%%%
%%%
%%%
%%%  Senators:  Loquacius, Repetitius, Tedius, Verbosus
%%%  Projects:  Stealth blimp, Supersonic helicopter,
%%%             Solar-powered cargo plane, Flying submarine
%%%  Budgets:   $58 million, $72 million, $79 million, $86 million
%%%
%%%

BEGIN

  senator: TYPE = {Loq, Rep, Ted, Verb}
  project: TYPE = {Blimp, Copter, Plane, Sub}
  budget:  TYPE = {i: int | i = 58 OR i = 72 OR i = 79 OR i = 86}
                  CONTAINING 58

%%% If an expression e is of type budget, the prover command
%%% (typepred "e") will apply the subtype predicate above to e.
%%%

  s,x,y,z: VAR senator
  p,q:     VAR project
  b,c:     VAR budget

%%%
%%% The following functions that relate senators, projects, and budgets
%%% are required to be injective (one-to-one).  Use (typepred "f_name")
%%% in the prover to make these conditions appear.
%%%

  proj:   {f: [senator -> project] | FORALL x,y: f(x) = f(y) => x = y}
  budget: {f: [senator -> budget]  | FORALL x,y: f(x) = f(y) => x = y}
  cost:   {f: [project -> budget]  | FORALL p,q: f(p) = f(q) => p = q}

%%%
%%% One additional constraint on these three functions is referred to below
%%% as the "project rule", expressed by the following axiom:
%%%

  project_rule: AXIOM cost(p) = budget(s) IMPLIES proj(s) = p

%%%
%%% This rule expresses a type of "triangulation" constraint, namely, that
%%% if the cost of a project and a senator's budget match, the senator
%%% must be promoting that particular project.  This restriction could
%%% (and should, to be safe) be expressed as additional constraints on the
%%% proj, cost, and budget functions.  This would require a more elaborate
%%% setup than is warranted here.
%%%
%%% The three puzzle clues are formalized as axioms.  Again, a formulation
%%% without axioms would be preferred in practice.
%%%

  clue1: AXIOM budget(Loq) < budget(Ted) AND
               budget(Loq) = cost(Copter) + 7

  clue2: AXIOM cost(Sub) /= 58 AND cost(Sub) < cost(Blimp)

  clue3: AXIOM budget(Verb) = cost(Plane) + 14


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The solution to the puzzle is expressed by the following lemmas.
%%% Each can be proved using only the prover commands from the set
%%% {SPLIT, FLATTEN, LEMMA, TYPEPRED, GROUND, INST (and its variants)}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 E_1: LEMMA budget(Loq) = 79

      % Hint:  From Clue 1, we know that budget(Loq) is neither the
      %        min nor the max value, so 58 < budget(Loq) < 86.  Also,
      %        cost(Copter) can't be 58 because the next possible value 
      %        is 72.  Hence, the only remaining choice is 79.


 E_2: LEMMA  cost(Copter) = 72

      % Hint:  Follows from Clue 1 and lemma L1.


 E_3a: LEMMA  cost(Sub) = 79

      % Hint:  From Clue 2 it follows that
      %        58 < cost(Sub) < cost(Blimp) <= 86,
      %        narrowing cost(Sub) to two choices.  Lemma 2 gives 
      %        cost(Copter) = 72, so only one choice remains.

 E_3b: LEMMA  cost(Blimp) = 86

      % Hint:  Clue 2 and lemma L3a give 79 = cost(Sub) < cost(Blimp),
      %        meaning 86 is the only possibility.

 E_3c: LEMMA  cost(Plane) = 58

      % Hint:  Lemmas L2, L3a, L3b give costs for Copter, Sub, Blimp.
      %        cost(Plane) must be the fourth alternative.


 E_4: LEMMA proj(Loq) = Sub

      % Hint:  Lemmas L1 and L3a give matching values for budget(Loq)
      %        and cost(Sub).  The project rule implies the Sub must be
      %        Loq's project.


 E_5a: LEMMA budget(Verb) = 72

      % Hint:  Follows from Clue 3 and lemma L3c.

 E_5b: LEMMA budget(Ted) = 86

      % Hint:  Follows from Clue 1 and lemma L1.

 E_5c: LEMMA budget(Rep) = 58

      % Hint:  The budget for Rep is the only one remaining after
      %        considering those in lemmas L1, L5a, L5b.


 E_6a: LEMMA proj(Rep) = Plane

      % Hint:  Using the project rule, this result follows from lemmas
      %        L3c and L5c.

 E_6b: LEMMA proj(Ted) = Blimp

      % Hint:  Similar to L6a.

 E_6c: LEMMA proj(Verb) = Copter

      % Hint:  Similar to L6a.

END th_E