% @(#)$Id: TypedObjEval.proof,v 1.2 1997/02/13 00:21:24 leavens Exp $
set script TypedObjEval
set log TypedObjEval

%%% Proof Obligations for trait TypedObjEval

execute TypedObjEval_Axioms

%% Conversions

freeze TypedObjEval

%% converts eval: Loc[T], State -> T exempting \forall loc: Loc[T], st: State,
%%   typs: Set[TYPE] eval(loc, bottom), eval(loc, emptyState), eval(loc,
%%   bind(st, widen(loc), widen(unassigned), typs))

thaw TypedObjEval

declare operators
  eval': Loc[T], State -> T
  ..


% subtrait 0: TypedObjEval (eval': Loc[T], State -> T for eval: Loc[T], State
%   -> T)

set name TypedObjEval

assert
  (eval'(loc, st)) = (extractTVal(narrow(eval(widen(loc), st))))
  ..

% subtrait 0.1: State


% subtrait 0.1.1: State_Basics


% subtrait 0.1.2: TypePerspectives


% subtrait 0.1.2.2: Set (TYPE for E, Set[TYPE] for C, int for Int)


% subtrait 0.1.2.2.1: SetBasics
%   with renaming (TYPE for E, Set[TYPE] for C)


% subtrait 0.1.2.2.2: Integer
%   with renaming (int for Int)


% subtrait 0.1.2.2.2.1: DecimalLiterals (Int for N)
%   with renaming (int for N)


% subtrait 0.1.2.2.2.2: TotalOrder (Int for T)
%   with renaming (int for T)


% subtrait 0.1.2.2.2.2.1: IsTO
%   with renaming (int for T)


% subtrait 0.1.2.2.2.2.2: DerivedOrders
%   with renaming (int for T)


% subtrait 0.1.2.2.3: DerivedOrders (C for T, __ \subseteq __: C, C -> Bool
%   for __ <= __: T, T -> Bool, __ \supseteq __: C, C -> Bool for __ >= __: T,
%   T -> Bool, __ \subset __: C, C -> Bool for __ < __: T, T -> Bool, __
%   \supset __: C, C -> Bool for __ > __: T, T -> Bool)
%   with renaming (Set[TYPE] for T, __ \subseteq __: Set[TYPE], Set[TYPE] ->
%     Bool for __ <= __: T, T -> Bool, __ \supseteq __: Set[TYPE], Set[TYPE]
%     -> Bool for __ >= __: T, T -> Bool, __ \subset __: Set[TYPE], Set[TYPE]
%     -> Bool for __ < __: T, T -> Bool, __ \supset __: Set[TYPE], Set[TYPE]
%     -> Bool for __ > __: T, T -> Bool)


% subtrait 0.1.3: State_Updates


% subtrait 0.1.4: StateDeprecated


% subtrait 0.1.4.3: UntypedFreshSemantics


% subtrait 0.1.5: Set (Object for E, Set[Object] for C, int for Int)


% subtrait 0.1.5.1: SetBasics
%   with renaming (Object for E, Set[Object] for C)


% subtrait 0.1.5.2: Integer
%   with renaming (int for Int)

% duplicate of subtrait 2.2.2: Integer

% subtrait 0.1.5.3: DerivedOrders (C for T, __ \subseteq __: C, C -> Bool for
%   __ <= __: T, T -> Bool, __ \supseteq __: C, C -> Bool for __ >= __: T, T
%   -> Bool, __ \subset __: C, C -> Bool for __ < __: T, T -> Bool, __ \supset
%   __: C, C -> Bool for __ > __: T, T -> Bool)
%   with renaming (Set[Object] for T, __ \subseteq __: Set[Object],
%     Set[Object] -> Bool for __ <= __: T, T -> Bool, __ \supseteq __:
%     Set[Object], Set[Object] -> Bool for __ >= __: T, T -> Bool, __ \subset
%     __: Set[Object], Set[Object] -> Bool for __ < __: T, T -> Bool, __
%     \supset __: Set[Object], Set[Object] -> Bool for __ > __: T, T -> Bool)


% subtrait 0.2: WithUnassigned (T for T, WithUnassigned[T] for
%   WithUnassigned[T])


% subtrait 0.3: WidenNarrow (Loc[T] for Typed, Object for Untyped)


% subtrait 0.4: WidenNarrow (WithUnassigned[T] for Typed, Value for Untyped)


declare variables
  loc: Loc[T]
  _x1_: Loc[T]
  st: State
  _x2_: State
  typs: Set[TYPE]
  ..

set name exemptions

assert
  eval(loc, bottom) = eval'(loc, bottom);
  eval(loc, emptyState) = eval'(loc, emptyState);
  eval(loc, bind(st, widen(loc), widen(unassigned), typs)) = eval'(loc,
    bind(st, widen(loc), widen(unassigned), typs))
  ..

set name conversionChecks

prove (eval(_x1_, _x2_)) = (eval'(_x1_, _x2_))
  [] conjecture
qed
prove (eval(_x1_, _x2_)) = (eval'(_x1_, _x2_))
  [] conjecture
qed