Require Arith.
Require machine.
Require axioms.
Require invar.
Require induction.
Require jsize.

Section upd_respects.

Hint ofType : axioms := Constructors ofType.
Hint ptr : axioms := Constructors ptr.
Hint ofmem : axioms := Constructors ofmem.

Lemma same_pseudo_preserves_preds :
  (s:state')(ms2:state)
  [s2 := (mkstate' ms2 (rep_of s) (last_alloc_of s))]
  (((e:exp; t:type)(ofType s2 e t)->(ofType s e t))
    /\ ((e:exp; r:rorw; t:type)(ptr s2 e r t)->(ptr s e r t))
    /\ ((m:mem)(ofmem s2 m)->(ofmem s m))).
Proof.
Intros.
Apply ofType_ptr_ofmem_simul_ind; EAuto with axioms.
Change (ofmem s (last_alloc_of s)).
Auto with axioms.
Qed.

Lemma same_pseudo_preserves_ptr :
  (s:state')(ms2:state)
  [s2 := (mkstate' ms2 (rep_of s) (last_alloc_of s))]
  (e:exp; r:rorw; t:type)(ptr s2 e r t)->(ptr s e r t).
Proof.
Intros until s2.
EApply proj1; EApply proj2.
Unfold s2.
EApply same_pseudo_preserves_preds.
Qed.

Lemma same_pseudo_preserves_ofmem :
  (s:state')(ms2:state)
  [s2 := (mkstate' ms2 (rep_of s) (last_alloc_of s))]
  (m:mem)(ofmem s2 m)->(ofmem s m).
Proof.
Intros until s2.
EApply proj2; EApply proj2.
Unfold s2.
EApply same_pseudo_preserves_preds.
Qed.


(* MAIN LEMMA: upd respects the invariant *)

Hints Resolve same_pseudo_preserves_ptr 
  same_pseudo_preserves_ofmem addr_updn : temp.

Lemma upd_respects : (s:state')(ADDR,E:exp)(T:type)(SZ:nat)
  (invariant s) ->
  (ptr s ADDR rw T) ->
  (ofType s E T) ->
  (jsize T SZ) ->
  (a,b:exp)(h:hist)
  [s2 := (mkstate' 
    (mkstate a b (updn SZ (mem_of' s) ADDR E) h) 
    (rep_of s)
    (last_alloc_of s))]
  (invariant s2).
Proof.
Intros.
Unfold_invar H.
Unfold_invar_Goal.
  Intros.
  Unfold s2 mem_of'.
  Simpl.
  Fold (mem_of' s).
  Unfold s2 in H9.
  EAuto with temp.

  Intros.
  Unfold s2 in H7 H10.
  EAuto with temp.

  Intros.
  Unfold s2 mem_of'.
  Simpl.
  Fold (mem_of' s).
  EAuto with temp.

  Intros.  
  Unfold s2 in H7.
  EAuto with temp.  

  Unfold s2.
  Apply same_pseudo_preserves_ofmem with ms2 := (machine_state_of s).
  Simpl.
  Replace (mkstate' (machine_state_of s) (rep_of s) (last_alloc_of s))
    with s; [Idtac | Case s; Trivial].
  Change (ofmem s (updn SZ (mem_of' s) ADDR E)).
  Rewrite_4or8 SZ; EAuto with axioms.
Qed.

End upd_respects.