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

%%% Proof Obligations for trait TypeTag

execute TypeTag_Axioms

%% Inherited assumptions

declare variables
  _x1_: Object
  _x2_: TYPE
  _y1_: Object
  _y2_: TYPE
  ..


% subtrait 3.1: TypeTaggedObject (TYPE for TYPE)

set name TypeTaggedObjectTheorem

prove
  sort TypeTaggedObject generated freely by [ __ , __ ]
  ..
  [] conjecture
qed
prove
  sort TypeTaggedObject partitioned by __.obj, __.type_tag
  ..
    <> deduction rule
    res by =>
      <> => subgoal
      [] => subgoal
    [] deduction rule
  [] conjecture
qed
prove
  (([ _x1_, _x2_ ]).obj) = (_x1_)
  ..
  [] conjecture
qed
prove
  (set_obj([ _x1_, _x2_ ], _y1_)) = ([ _y1_, _x2_ ])
  ..
  [] conjecture
qed
prove
  (([ _x1_, _x2_ ]).type_tag) = (_x2_)
  ..
  [] conjecture
qed
prove
  (set_type_tag([ _x1_, _x2_ ], _y2_)) = ([ _x1_, _y2_ ])
  ..
  [] conjecture
qed

%% Implications

declare variables
  o: T
  ..


% main trait: TypeTag

set name TypeTagTheorem

prove
  (asTypeTaggedObject(o).obj) = (widen(o))
  ..
  [] conjecture
qed