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

%%% Proof Obligations for trait FreshSemantics

execute FreshSemantics_Axioms

%% Conversions

freeze FreshSemantics

%% converts isFresh exempting \forall loc: Loc[T], st: State isFresh(loc,
%%   bottom, st), isFresh(loc, st, bottom)

thaw FreshSemantics

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


% subtrait 0: FreshSemantics (isFresh': Loc[T], State, State -> Bool for
%   isFresh: Loc[T], State, State -> Bool)

set name FreshSemantics

assert
  (isFresh'(loc, pre, post)) = (~ allocated(loc, pre) /\ allocated(loc, post))
  ..

% subtrait 0.1: AllocatedAssigned (Loc for Loc, T for T, WithUnassigned[T] for
%   WithUnassigned[T], Loc[T] for Loc[T])


% subtrait 0.1.5: SortNames (Loc[T] for S, TYPE for SORTNAME, type_of: Loc[T]
%   -> TYPE for sort_of: S -> SORTNAME)
%   with renaming (Loc[T] for S, TYPE for SORTNAME, type_of: Loc[T] -> TYPE
%     for sort_of: S -> SORTNAME)


% subtrait 0.1.1: State


% subtrait 0.1.1.1: State_Basics


% subtrait 0.1.1.2: TypePerspectives


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


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


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


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


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


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


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


% subtrait 0.1.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.1.3: State_Updates


% subtrait 0.1.1.4: StateDeprecated


% subtrait 0.1.1.4.3: UntypedFreshSemantics


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


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


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

% duplicate of subtrait 2.2.2: Integer

% subtrait 0.1.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.1.2: WithUnassigned (T for T, WithUnassigned[T] for
%   WithUnassigned[T])


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


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


declare variables
  loc: Loc[T]
  st: State
  _x1_: Loc[T]
  _x2_: State
  _x3_: State
  ..

set name exemptions

assert
  isFresh(loc, bottom, st) = isFresh'(loc, bottom, st);
  isFresh(loc, st, bottom) = isFresh'(loc, st, bottom)
  ..

set name conversionChecks

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