% @(#)$Id: State.proof,v 1.2 1997/02/13 00:21:14 leavens Exp $

set script State
set log State

%%% Proof Obligations for trait State

execute State_Axioms

%% Inherited assumptions

declare variables
  x: int
  x: Set[TYPE]
  x: Set[Object]
  y: int
  y: Set[TYPE]
  y: Set[Object]
  i: int
  j: int
  z: int
  obj: Object
  st: State
  obj1: Object
  v: Value
  typs: Set[TYPE]
  t: TYPE
  e: TYPE
  e: Object
  e1: TYPE
  e1: Object
  e2: TYPE
  e2: Object
  s: Set[TYPE]
  s: Set[Object]
  s1: Set[TYPE]
  s1: Set[Object]
  s2: Set[TYPE]
  s2: Set[Object]
  ..


% subtrait 1.1: State_Basics

set name State_BasicsTheorem

prove
  sort State generated by emptyState, bottom, bind
  ..
qed
prove
  sort State partitioned by allocated, eval, isBottom
  ..
  res by =>
qed
prove
  (~ allocated(obj, emptyState))
  ..
qed
prove
  (~ allocated(obj, bottom))
  ..
qed
prove
  (allocated(obj, bind(st, obj1, v, typs))) = (~ isBottom(st) /\ (obj = obj1
    \/ allocated(obj, st)))
  ..
qed
prove
  (~ isBottom(st) => eval(obj1, bind(st, obj, v, typs)) = (if obj1 = obj then
    v else eval(obj1, st)))
  ..
qed
prove
  (~ isBottom(emptyState))
  ..
qed
prove
  (isBottom(bottom))
  ..
qed
prove
  (isBottom(bind(st, obj, v, typs))) = (isBottom(st))
  ..
qed
prove
  (bind(bottom, obj, v, typs)) = (bottom)
  ..
qed

% subtrait 1.1: State_Basics

% duplicate of subtrait 1.1: State_Basics

% subtrait 1.1: State_Basics

% duplicate of subtrait 1.1: State_Basics

%% Implications


% main trait: State

set name StateTheorem

prove
  (domain(emptyState)) = ({ }:Set[Object])
  ..

  apply SetBasics.6 to conjecture
  [] conjecture
qed
%% Conversions

freeze State

%% converts domain

thaw State

declare operators
  domain': State -> Set[Object]
  ..


% subtrait 0: State (domain': State -> Set[Object] for domain: State ->
%   Set[Object])

set name State

assert
  (obj \in domain'(st)) = (allocated(obj, st))
  ..

% subtrait 0.1: State_Basics


% subtrait 0.2: TypePerspectives


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


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


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


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


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


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


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


% subtrait 0.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.3: State_Updates


% subtrait 0.4: StateDeprecated


% subtrait 0.4.3: UntypedFreshSemantics


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


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


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

% duplicate of subtrait 2.2.2: Integer

% subtrait 0.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)


declare variables
  _x1_: State
  ..

set name conversionChecks

prove (domain(_x1_)) = (domain'(_x1_))
  apply SetBasics.6 to conjecture
  [] conjecture
qed