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

set script State_Updates
set log State_Updates

%%% Proof Obligations for trait State_Updates

execute State_Updates_Axioms

%% Implications

declare variables
  obj: Object
  typs: Set[TYPE]
  v: Value
  st: State
  ..


% main trait: State_Updates

set name State_UpdatesTheorem

prove
  (~ allocated(obj, st) => \A v (updateValue(st, obj, v) = st))
  ..
  res by ind
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    res by =>
      <> => subgoal
      res by case oc = objc
        <> case oc = objc
        set immu on
        p bind(bottom, objc, v, s)=bottom
          [] conjecture
        [] case oc = objc
        <> case ~(oc = objc)
        set immu off
        res by case stc=bottom
          <> case stc = bottom
          [] case stc = bottom
          <> case ~(stc = bottom)
          p updateValue(stc, objc, v)=stc
            res by con
              <> contradiction subgoal
              crit *Hyp with *
              [] contradiction subgoal
            [] conjecture
          [] case ~(stc = bottom)
        [] case ~(oc = objc)
      [] => subgoal
    [] induction subgoal
  [] conjecture
qed
prove
  (~ allocated(obj, st) => \A v (updateTypes(st, obj, typs) = st))
  ..
  res by ind on st
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    res by case stc = bottom
      <> case stc = bottom
      res by case o = obj
        <> case oc = objc
        set immu on
        p bind(bottom, objc, v, typs)=bottom
          [] conjecture
        [] case oc = objc
        <> case ~(oc = objc)
        [] case ~(oc = objc)
      [] case stc = bottom
      <> case ~(stc = bottom)
      set immu off
      res by case obj=o
        <> case objc = oc
        [] case objc = oc
        <> case ~(objc = oc)
        res by =>
          <> => subgoal
          p updateTypes(stc, objc, typs) = stc
            res by con
              <> contradiction subgoal
              crit *Hyp with *
              [] contradiction subgoal
            [] conjecture
          [] => subgoal
        [] case ~(objc = oc)
      [] case ~(stc = bottom)
    [] induction subgoal
  [] conjecture
qed

%% Conversions

freeze State_Updates

%% converts updateValue, updateTypes

thaw State_Updates

declare operators
  updateValue': State, Object, Value -> State
  , updateTypes': State, Object, Set[TYPE] -> State
  ..


% subtrait 0: State_Updates (updateValue': State, Object, Value -> State for
%   updateValue: State, Object, Value -> State, updateTypes': State, Object,
%   Set[TYPE] -> State for updateTypes: State, Object, Set[TYPE] -> State)

set name State_Updates

assert
  (updateValue'(emptyState, obj1, v1)) = (emptyState)
  ;(updateValue'(bottom, obj1, v1)) = (bottom)
  ;(updateValue'(bind(st, obj, v, typs), obj1, v1)) = (if obj = obj1 then
    bind(st, obj, v1, typs) else bind(updateValue'(st, obj1, v1), obj, v,
    typs))
  ;(updateTypes'(emptyState, obj1, typs1)) = (emptyState)
  ;(updateTypes'(bottom, obj1, typs1)) = (bottom)
  ;(updateTypes'(bind(st, obj, v, typs), obj1, typs1)) = (if obj = obj1 then
    bind(st, obj, v, typs1) else bind(updateTypes'(st, obj1, typs1), obj, v,
    typs))
  ..

% 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.2.1: State_Basics

% duplicate of subtrait 1: State_Basics

declare variables
  _x1_: State
  _x2_: Object
  _x3_: Value
  _x3_: Set[TYPE]
  ..

set name conversionChecks

prove (updateValue(_x1_, _x2_, _x3_:Value)) = (updateValue'(_x1_, _x2_,_x3_:Value))
  res by ind on _x1_
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    [] induction subgoal
  [] conjecture
qed
prove (updateValue(_x1_, _x2_, _x3_:Value)) = (updateValue'(_x1_, _x2_,_x3_:Value))
  [] conjecture
qed
prove (updateValue(_x1_, _x2_, _x3_:Value)) = (updateValue'(_x1_, _x2_,_x3_:Value))
  [] conjecture
qed
prove (updateTypes(_x1_, _x2_, _x3_:Set[TYPE])) = (updateTypes'(_x1_, _x2_,_x3_:Set[TYPE]))
  res by ind on _x1_
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    [] induction subgoal
  [] conjecture
qed
prove (updateTypes(_x1_, _x2_, _x3_:Set[TYPE])) = (updateTypes'(_x1_, _x2_,_x3_:Set[TYPE]))
  [] conjecture
qed
prove (updateTypes(_x1_, _x2_, _x3_:Set[TYPE])) = (updateTypes'(_x1_, _x2_,_x3_:Set[TYPE]))
  [] conjecture
qed