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

set script TypePerspectives
set log TypePerspectives

%%% Proof Obligations for trait TypePerspectives

execute TypePerspectives_Axioms

%% Implications

declare variables
  obj: Object
  obj1: Object
  t: TYPE
  v: Value
  st: State
  ..


% main trait: TypePerspectives

set name TypePerspectivesTheorem

prove
  (~ allocated(obj, st) => types_of(obj, st) = { })
  ..
  res by ind
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    res by case stc=bottom
      <> case stc = bottom
      set immu on
      p bind(bottom, o, v, s)=bottom
        [] conjecture
      [] 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
          res by con
            <> contradiction subgoal
            crit *Hyp with *
            [] contradiction subgoal
          [] => subgoal
        [] case ~(objc = oc)
      [] case ~(stc = bottom)
    [] induction subgoal
  [] conjecture
qed
%% Conversions

freeze TypePerspectives

%% converts types_of, hasType

thaw TypePerspectives

declare operators
  types_of': Object, State -> Set[TYPE]
  , hasType': Object, State, TYPE -> Bool
  ..


% subtrait 0: TypePerspectives (types_of': Object, State -> Set[TYPE] for
%   types_of: Object, State -> Set[TYPE], hasType': Object, State, TYPE ->
%   Bool for hasType: Object, State, TYPE -> Bool)

set name TypePerspectives

assert
  (types_of'(obj, emptyState)) = ({ })
  ;(types_of'(obj, bottom)) = ({ })
  ;(~ isBottom(st) => types_of'(obj, bind(st, obj1, v, typs)) = (if obj = obj1
    then typs else types_of'(obj, st)))
  ;(hasType'(obj, st, t)) = (t \in types_of'(obj, st))
  ..

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


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


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


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


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


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


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


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


declare variables
  _x1_: Object
  _x2_: State
  _x3_: TYPE
  ..

set name conversionChecks

prove (types_of(_x1_, _x2_)) = (types_of'(_x1_, _x2_))
  res by ind
    <> basis subgoal
    [] basis subgoal
    <> basis subgoal
    [] basis subgoal
    <> induction subgoal
    res by case _x1_=o
      <> case _x1_c = oc
      res by case _x2_c=bottom
        <> case _x2_c = bottom
        set immu on
        p bind(bottom, oc, v, s)=bottom
          [] conjecture
        [] case _x2_c = bottom
        <> case ~(_x2_c = bottom)
        p types_of(oc, bind(_x2_c, oc, v, s))=s
          set immu off
          res by con
            <> contradiction subgoal
            crit *hyp with *
            [] contradiction subgoal
          [] conjecture
        res by con
          <> contradiction subgoal
          crit *Hyp with *
          [] contradiction subgoal
        [] case ~(_x2_c = bottom)
      [] case _x1_c = oc
      <> case ~(_x1_c = oc)
      res by case _x2_c=bottom
        <> case _x2_c = bottom
        set immu on
        p bind(bottom, oc, v, s)=bottom
          [] conjecture
        [] case _x2_c = bottom
        <> case ~(_x2_c = bottom)
        set immu off
        p types_of'(_x1_c, bind(_x2_c, oc, v, s)) = types_of'(_x1_c, _x2_c)
          res by con
            <> contradiction subgoal
            crit *Hyp with *
            [] contradiction subgoal
          [] conjecture
        set immu on
        ins st by _x2_c,obj by _x1_c, obj1 by obj, typs by s in TypePerspectives.3
        set immu off
        res by con
          <> contradiction subgoal
          crit *Hyp with *
          [] contradiction subgoal
        [] case ~(_x2_c = bottom)
      [] case ~(_x1_c = oc)
    [] induction subgoal
  [] conjecture
qed
prove (types_of(_x1_, _x2_)) = (types_of'(_x1_, _x2_))
  [] conjecture
qed
prove (hasType(_x1_, _x2_, _x3_)) = (hasType'(_x1_, _x2_, _x3_))
  [] conjecture
qed
prove (hasType(_x1_, _x2_, _x3_)) = (hasType'(_x1_, _x2_, _x3_))
  [] conjecture
qed
prove (hasType(_x1_, _x2_, _x3_)) = (hasType'(_x1_, _x2_, _x3_))
  [] conjecture
qed