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

%%% Proof Obligations for trait TypedObj

execute TypedObj_Axioms

%% Inherited assumptions

declare variables
  x: int
  x: Set[TYPE]
  x: Set[Object]
  y: int
  y: Set[TYPE]
  pre: State
  y: Set[Object]
  post: State
  tval: T
  u: Object
  u: Value
  i: int
  j: int
  loc: Loc[T]
  z: int
  obj: Object
  st: State
  obj1: Object
  v: Value
  typs: Set[TYPE]
  v1: Value
  typs1: Set[TYPE]
  t: TYPE
  t: Loc[T]
  t: WithUnassigned[T]
  e: TYPE
  e: Object
  e1: TYPE
  e1: Object
  e2: TYPE
  e2: Object
  s: Set[TYPE]
  s: Set[Object]
  s: Loc[T]
  s1: Set[TYPE]
  s1: Set[Object]
  s2: Set[TYPE]
  s2: Set[Object]
  ..


% subtrait 1.1: State

set name StateTheorem

prove
  (obj \in domain(st)) = (allocated(obj, st))
  ..
  [] conjecture
qed

% subtrait 1.1.1: State_Basics

set name State_BasicsTheorem

prove
  sort State generated by emptyState, bottom, bind
  ..
  [] conjecture
qed
prove
  sort State partitioned by allocated: Object, State -> Bool, eval: Object,
    State -> Value, isBottom
  ..
    <> deduction rule
    res by =>
      <> => subgoal
      [] => subgoal
    [] deduction rule
  [] conjecture
qed
prove
  (~ allocated(obj, emptyState))
  ..
  [] conjecture
qed
prove
  (~ allocated(obj, bottom))
  ..
  [] conjecture
qed
prove
  (allocated(obj, bind(st, obj1, v, typs))) = (obj = obj1 \/ allocated(obj,
    st))
  ..
  [] conjecture
qed
prove
  (eval(obj1, bind(st, obj, v, typs))) = (if obj1 = obj then v else eval(obj1,
    st))
  ..
  [] conjecture
qed
prove
  (~ isBottom(emptyState))
  ..
  [] conjecture
qed
prove
  (isBottom(bottom))
  ..
  [] conjecture
qed
prove
  (~ isBottom(bind(st, obj, v, typs)))
  ..
  [] conjecture
qed

% subtrait 1.1.2: TypePerspectives

set name TypePerspectivesTheorem

prove
  (types_of(obj, emptyState)) = ({ }:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (types_of(obj, bottom)) = ({ }:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (types_of(obj, bind(st, obj1, v, typs))) = (typs)
  ..
  [] conjecture
qed
prove
  (hasType(obj, st, t:TYPE)) = (t:TYPE \in types_of(obj, st))
  ..
  [] conjecture
qed

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

set name SetTheorem

prove
  (e:TYPE \notin s:Set[TYPE]) = (~ (e:TYPE \in s:Set[TYPE]))
  ..
  [] conjecture
qed
prove
  ({ e:TYPE }) = (insert(e:TYPE, { }:Set[TYPE]))
  ..
  [] conjecture
qed
prove
  (e1:TYPE \in delete(e2:TYPE, s:Set[TYPE])) = (e1:TYPE ~= e2:TYPE /\ e1:TYPE
    \in s:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (e:TYPE \in (s1:Set[TYPE] \U s2:Set[TYPE])) = (e:TYPE \in s1:Set[TYPE] \/
    e:TYPE \in s2:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (e:TYPE \in (s1:Set[TYPE] \I s2:Set[TYPE])) = (e:TYPE \in s1:Set[TYPE] /\
    e:TYPE \in s2:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (e:TYPE \in (s1:Set[TYPE] - s2:Set[TYPE])) = (e:TYPE \in s1:Set[TYPE] /\
    e:TYPE \notin s2:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (size({ }:Set[TYPE])) = (0)
  ..
  [] conjecture
qed
prove
  (size(insert(e:TYPE, s:Set[TYPE]))) = (if e:TYPE \notin s:Set[TYPE] then
    size(s:Set[TYPE]) + 1 else size(s:Set[TYPE]))
  ..
  [] conjecture
qed
prove
  (s1:Set[TYPE] \subseteq s2:Set[TYPE]) = (s1:Set[TYPE] - s2:Set[TYPE] = {
    }:Set[TYPE])
  ..
  [] conjecture
qed

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

set name SetBasicsTheorem

prove
  sort Set[TYPE] generated by {}: -> Set[TYPE], insert: TYPE, Set[TYPE] ->
    Set[TYPE]
  ..
  [] conjecture
qed
prove
  sort Set[TYPE] partitioned by __ \in __: TYPE, Set[TYPE] -> Bool
  ..
    <> deduction rule
    res by =>
      <> => subgoal
      [] => subgoal
    [] deduction rule
  [] conjecture
qed
prove
  (~ (e:TYPE \in { }:Set[TYPE]))
  ..
  [] conjecture
qed
prove
  (e1:TYPE \in insert(e2:TYPE, s:Set[TYPE])) = (e1:TYPE = e2:TYPE \/ e1:TYPE
    \in s:Set[TYPE])
  ..
  [] conjecture
qed

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

set name IntegerTheorem

prove
  sort int generated by 0, succ, pred
  ..
  [] conjecture
qed
prove
  (succ(pred(x:int))) = (x:int)
  ..
  [] conjecture
qed
prove
  (pred(succ(x:int))) = (x:int)
  ..
  [] conjecture
qed
prove
  (- 0) = (0)
  ..
  [] conjecture
qed
prove
  (- succ(x:int)) = (pred(- x:int))
  ..
  [] conjecture
qed
prove
  (- pred(x:int)) = (succ(- x:int))
  ..
  [] conjecture
qed
prove
  (abs(x:int)) = (max(- x:int, x:int))
  ..
  [] conjecture
qed
prove
  (x:int + 0) = (x:int)
  ..
  [] conjecture
qed
prove
  (x:int + succ(y:int)) = (succ(x:int + y:int))
  ..
  [] conjecture
qed
prove
  (x:int + pred(y:int)) = (pred(x:int + y:int))
  ..
  [] conjecture
qed
prove
  (x:int - y:int) = (x:int + (- y:int))
  ..
  [] conjecture
qed
prove
  (x:int * 0) = (0)
  ..
  [] conjecture
qed
prove
  (x:int * succ(y:int)) = ((x:int * y:int) + x:int)
  ..
  [] conjecture
qed
prove
  (x:int * pred(y:int)) = ((x:int * y:int) - x:int)
  ..
  [] conjecture
qed
prove
  (y:int > 0 => mod(x:int, y:int) + (div(x:int, y:int) * y:int) = x:int)
  ..
  [] conjecture
qed
prove
  (y:int > 0 => mod(x:int, y:int) >= 0)
  ..
  [] conjecture
qed
prove
  (y:int > 0 => mod(x:int, y:int) < y:int)
  ..
  [] conjecture
qed
prove
  (min(x:int, y:int)) = (if x:int <= y:int then x:int else y:int)
  ..
  [] conjecture
qed
prove
  (max(x:int, y:int)) = (if x:int <= y:int then y:int else x:int)
  ..
  [] conjecture
qed
prove
  (x:int < succ(x:int))
  ..
  [] conjecture
qed

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

set name DecimalLiteralsTheorem

prove
  (times10plus(0, j)) = (j)
  ..
  res by ind using Integer.1
    <> basis subgoal
    res by con
      <> contradiction subgoal
      crit *Hyp with *
      [] contradiction subgoal
    [] basis subgoal
    <> induction subgoal
    res by con
      <> contradiction subgoal
      crit *Hyp with *
      [] contradiction subgoal
    [] induction subgoal
    <> induction subgoal
    res by con
      <> contradiction subgoal
      crit *Hyp with *
      [] contradiction subgoal
    [] induction subgoal
  [] conjecture
qed
prove
  (times10plus(i, succ(j))) = (succ(times10plus(i, j))) by con
  ..
    <> contradiction subgoal
    crit *Hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (times10plus(succ(i), 0)) = (succ(times10plus(i, 9)))
  ..
  res by con
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (1) = (succ(0)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (2) = (succ(1)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (3) = (succ(2)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (4) = (succ(3)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (5) = (succ(4)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (6) = (succ(5)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (7) = (succ(6)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (8) = (succ(7)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
prove
  (9) = (succ(8)) by con
  ..
    <> contradiction subgoal
    crit *hyp with *
    [] contradiction subgoal
  [] conjecture
qed
%  subtrait 1.1.2.2.2.2: TotalOrder (Int for T)
%   with renaming (int for T)


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

set name IsTOTheorem

prove
  (x:int <= x:int)
  ..
  [] conjecture
qed
prove
  ((x:int <= y:int /\ y:int <= z:int) => x:int <= z:int)
  ..
  [] conjecture
qed
prove
  (x:int <= y:int /\ y:int <= x:int) = (x:int = y:int)
  ..
  [] conjecture
qed
prove
  (x:int <= y:int \/ y:int <= x:int)
  ..
  [] conjecture
qed

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

set name DerivedOrdersTheorem

prove
  (x:int < y:int) = (x:int <= y:int /\ ~ (x:int = y:int))
  ..
  [] conjecture
qed
prove
  (x:int >= y:int) = (y:int <= x:int)
  ..
  [] conjecture
qed
prove
  (x:int > y:int) = (y:int < x:int)
  ..
  [] conjecture
qed

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

set name DerivedOrdersTheorem

prove
  (x:Set[TYPE] \subset y:Set[TYPE]) = (x:Set[TYPE] \subseteq y:Set[TYPE] /\ ~
    (x:Set[TYPE] = y:Set[TYPE]))
  ..
  [] conjecture
qed
prove
  (x:Set[TYPE] \supseteq y:Set[TYPE]) = (y:Set[TYPE] \subseteq x:Set[TYPE])
  ..
  [] conjecture
qed
prove
  (x:Set[TYPE] \supset y:Set[TYPE]) = (y:Set[TYPE] \subset x:Set[TYPE])
  ..
  [] conjecture
qed

% subtrait 1.1.3: State_Updates

set name State_UpdatesTheorem

prove
  (updateValue(emptyState, obj1, v1)) = (emptyState)
  ..
  [] conjecture
qed
prove
  (updateValue(bottom, obj1, v1)) = (bottom)
  ..
  [] conjecture
qed
prove
  (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))
  ..
  [] conjecture
qed
prove
  (updateTypes(emptyState, obj1, typs1)) = (emptyState)
  ..
  [] conjecture
qed
prove
  (updateTypes(bottom, obj1, typs1)) = (bottom)
  ..
  [] conjecture
qed
prove
  (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))
  ..
  [] conjecture
qed

% subtrait 1.1.4: StateDeprecated

set name StateDeprecatedTheorem

prove
  (empty) = (emptyState)
  ..
  [] conjecture
qed
prove
  (obj \in st) = (allocated(obj, st))
  ..
qed
prove
  (obj \in objs(st)) = (obj \in st)
  ..
  [] conjecture
qed

% subtrait 1.1.4.3: UntypedFreshSemantics

set name UntypedFreshSemanticsTheorem

prove
  (obj \in added(pre, post)) = (~ allocated(obj, pre) /\ allocated(obj, post))
  ..
  [] conjecture
qed

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

set name SetTheorem

prove
  (e:Object \notin s:Set[Object]) = (~ (e:Object \in s:Set[Object]))
  ..
  [] conjecture
qed
prove
  ({ e:Object }) = (insert(e:Object, { }:Set[Object]))
  ..
  [] conjecture
qed
prove
  (e1:Object \in delete(e2:Object, s:Set[Object])) = (e1:Object ~= e2:Object
    /\ e1:Object \in s:Set[Object])
  ..
  [] conjecture
qed
prove
  (e:Object \in (s1:Set[Object] \U s2:Set[Object])) = (e:Object \in
    s1:Set[Object] \/ e:Object \in s2:Set[Object])
  ..
  [] conjecture
qed
prove
  (e:Object \in (s1:Set[Object] \I s2:Set[Object])) = (e:Object \in
    s1:Set[Object] /\ e:Object \in s2:Set[Object])
  ..
  [] conjecture
qed
prove
  (e:Object \in (s1:Set[Object] - s2:Set[Object])) = (e:Object \in
    s1:Set[Object] /\ e:Object \notin s2:Set[Object])
  ..
  [] conjecture
qed
prove
  (size({ }:Set[Object])) = (0)
  ..
  [] conjecture
qed
prove
  (size(insert(e:Object, s:Set[Object]))) = (if e:Object \notin s:Set[Object]
    then size(s:Set[Object]) + 1 else size(s:Set[Object]))
  ..
  [] conjecture
qed
prove
  (s1:Set[Object] \subseteq s2:Set[Object]) = (s1:Set[Object] - s2:Set[Object]
    = { }:Set[Object])
  ..
  [] conjecture
qed

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

set name SetBasicsTheorem

prove
  sort Set[Object] generated by {}: -> Set[Object], insert: Object,
    Set[Object] -> Set[Object]
  ..
  [] conjecture
qed
prove
  sort Set[Object] partitioned by __ \in __: Object, Set[Object] -> Bool
  ..
    <> deduction rule
    res by =>
      <> => subgoal
      [] => subgoal
    [] deduction rule
  [] conjecture
qed
prove
  (~ (e:Object \in { }:Set[Object]))
  ..
  [] conjecture
qed
prove
  (e1:Object \in insert(e2:Object, s:Set[Object])) = (e1:Object = e2:Object \/
    e1:Object \in s:Set[Object])
  ..
  [] conjecture
qed

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

% duplicate of subtrait 2.2.2: Integer

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

set name DerivedOrdersTheorem

prove
  (x:Set[Object] \subset y:Set[Object]) = (x:Set[Object] \subseteq
    y:Set[Object] /\ ~ (x:Set[Object] = y:Set[Object]))
  ..
  [] conjecture
qed
prove
  (x:Set[Object] \supseteq y:Set[Object]) = (y:Set[Object] \subseteq
    x:Set[Object])
  ..
  [] conjecture
qed
prove
  (x:Set[Object] \supset y:Set[Object]) = (y:Set[Object] \subset
    x:Set[Object])
  ..
  [] conjecture
qed

% subtrait 1.2: WithUnassigned (T for T, WithUnassigned[T] for
%   WithUnassigned[T])

set name WithUnassignedTheorem

prove
  sort WithUnassigned[T] generated by injectTVal, unassigned
  ..
  [] conjecture
qed
prove
  sort WithUnassigned[T] partitioned by isUnassigned, extractTVal
  ..
    <> deduction rule
    resume by =>
      <> => subgoal
      [] => subgoal
    [] deduction rule
  [] conjecture
qed
prove
  (extractTVal(injectTVal(tval))) = (tval)
  ..
  [] conjecture
qed
prove
  (~ isUnassigned(injectTVal(tval)))
  ..
  [] conjecture
qed
prove
  (isUnassigned(unassigned))
  ..
  [] conjecture
qed

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

set name WidenNarrowTheorem

prove
  (widen(narrow(u:Object))) = (u:Object)
  ..
  [] conjecture
qed
prove
  (narrow(widen(t:Loc[T]))) = (t:Loc[T])
  ..
  [] conjecture
qed

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

set name WidenNarrowTheorem

prove
  (widen(narrow(u:Value))) = (u:Value)
  ..
  [] conjecture
qed
prove
  (narrow(widen(t:WithUnassigned[T]))) = (t:WithUnassigned[T])
  ..
  [] conjecture
qed

% subtrait 1.1: State

% duplicate of subtrait 1.1: State

% subtrait 1.1: State

% duplicate of subtrait 1.1: State

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

set name AllocatedAssignedTheorem

prove
  (allocated(loc, st)) = (allocated(widen(loc), st) /\ type_of(loc) \in
    types_of(widen(loc), st))
  ..
  [] conjecture
qed
prove
  (assigned(loc, st)) = (allocated(loc, st) /\ narrow(eval(widen(loc), st)) ~=
    unassigned)
  ..
  [] conjecture
qed

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

set name SortNamesTheorem

prove
  (type_of(s:Loc[T])) = (c)
  ..
  [] conjecture
qed

% subtrait 1.1.1: State

% duplicate of subtrait 1.1: State

% subtrait 1.1.2: WithUnassigned (T for T, WithUnassigned[T] for
%   WithUnassigned[T])

% duplicate of subtrait 1.2: WithUnassigned

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

% duplicate of subtrait 1.3: WidenNarrow

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

% duplicate of subtrait 1.4: WidenNarrow

% subtrait 1.1: State

% duplicate of subtrait 1.1: State

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

% duplicate of subtrait 1.1: AllocatedAssigned