proposition: Theorem sem_rac1_correct_rac_sem: forall p, (forall e st_rac st_rac' s, OpRac1.ExpressionStep p e st_rac st_rac' s -> forall st_sem, CorrespondingState p st_rac st_sem -> exists st_sem', CorrespondingState p st_rac' st_sem' /\ OpSem.ExpressionStep p e st_sem st_sem' s) /\ (forall l st_rac st_rac' s, OpRac1.ListSteps p l st_rac st_rac' s -> forall st_sem, CorrespondingState p st_rac st_sem -> exists st_sem', CorrespondingState p st_rac' st_sem' /\ OpSem.ListSteps p l st_sem st_sem' s) /\ (forall m b st_rac st_rac' s, OpRac1.StatementStep p m b st_rac st_rac' s -> forall st_sem, CorrespondingState p st_rac st_sem -> exists st_sem', CorrespondingState p st_rac' st_sem' /\ OpSem.StatementStep p m b st_sem st_sem' s) /\ (forall m b st_rac st_rac' s, OpRac1.BlockStep p m b st_rac st_rac' s -> forall st_sem, CorrespondingState p st_rac st_sem -> exists st_sem', CorrespondingState p st_rac' st_sem' /\ OpSem.BlockStep p m b st_sem st_sem' s).
proof: Proof. intro p. apply OpRac1.mutual_ind; intros; simpl in *. unfold Sem.Assignables.FieldUpdateAction in H6. rewrite <- H9 in H10. replace (st2) [fr := (st2) @fr]%rac1 with st2 in H5 by (destruct st2; trivial). destruct H2 with (st_sem := st_sem) as (st1_sem, H21); trivial. destruct H21. destruct H5 with (st_sem := st1_sem) as (st2_sem, H61); trivial. destruct H61. exists (st2_sem) [h := Heap.update (st2_sem) @h loc v]. split. rewrite H10 in |- *. unfold CorrespondingState in H14. destruct H14. split; trivial. rewrite H14 in |- *; trivial. destruct H14. apply (OpSem.assignment_instance_field_ok p e v obj fsig expr target st_sem st1_sem st2_sem (st2_sem) [h := Heap.update (st2_sem) @h loc v] st2_sem loc cn um); trivial. apply (Assignables.FieldUpdateCheck_Correct loc p st1 st1_sem); trivial. rewrite H14;trivial. rewrite H14;trivial. destruct H1 with st_sem as (st1_sem, Htmp); trivial. destruct Htmp. clear H1. destruct H6 with st1_sem as (st2_sem, Htmp); trivial. destruct Htmp. clear H6. set (fr_c1_sem := Sem.NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_sem) in |- *. set (st3_sem := (st2_sem) [fr := fr_c1_sem]) in |- *. set (st_c_sem := Sem.Assignables.MethodCallAction p c' m' st3_sem) in |- *. destruct H15 with st_c_sem as (st_c'_sem, Htmp). assert (CorrespondingState p st3 st3_sem). unfold st3_sem in |- *. rewrite H10 in |- *. destruct H1. split; trivial. simpl in |- *. apply Assignables.NewFrame_Correct with (m := m') (param := lv2params m' (Ref this0 :: psv)) (st_rac := st2) (st_sem := st2_sem); trivial. split; trivial. unfold st_c_sem in |- *. rewrite <- H11 in |- *. unfold NewFrame in H9. unfold Sem.NewFrame in fr_c1_sem. apply Assignables.MethodCallAction_Correct with (c := c') (m := m') (st_rac := st3) (st_sem := st3_sem) (st_rac_assignables := st2@fr@assignables%rac1) (st_rac_fresh := st2@fr@fresh%rac1); trivial. intuition. rewrite H9 in H10. rewrite H10. trivial. rewrite H9 in H10. rewrite H10. trivial. destruct Htmp. set (st'_sem := Sem.Assignables.MethodReturnAction p st_c'_sem st2_sem) in |- *. exists st'_sem. split. unfold st'_sem in |- *. rewrite <- H17 in |- *. apply Assignables.MethodReturnAction_Correct with st2 st_c' st2_sem st_c'_sem; trivial. apply (OpSem.method_vcall_ok p e st_sem st1_sem st2_sem st3_sem st_c_sem st_c'_sem st'_sem fr_c1_sem msig o cn um this0 ps psnv psv v cn' m' c' b body); trivial. destruct H19. rewrite H19 in |- *. trivial. destruct H6. destruct H23. rewrite H26 in |- *. trivial. set (st1_sem := Sem.Assignables.NewObjectAction p o st_sem) in |- *. exists (st1_sem) [h := h']. split. rewrite H2. assert (CorrespondingState p st1 st1_sem). unfold st1_sem in |- *. rewrite <- H1. apply Assignables.NewObjectAction_Correct with o st st_sem; trivial. destruct H4. split; trivial. apply OpSem.new_object_ok with (st1 := st1_sem) (h' := h') (cn := cn) (um := um); trivial. destruct H3. rewrite <- H3 in H0; trivial. exists st_sem. rewrite <- H in |- *. split; trivial. apply OpSem.ListSteps_nil; trivial. destruct H1 with st_sem as (st1_sem, Htmp); trivial. destruct Htmp. destruct H3 with st1_sem as (st'_sem, Htmp); trivial. destruct Htmp. exists st'_sem. split; trivial. apply OpSem.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_sem); trivial. destruct H1 with st_sem as (st'_sem, Htmp); trivial. destruct Htmp. exists st'_sem. split; trivial. apply OpSem.expr_stmt_ok with (v := v) (e := e); trivial. destruct H2. destruct H5. rewrite H7 in |- *; trivial. destruct H1 with st_sem as (st1_sem, Htmp); trivial. destruct Htmp. set (fr2_sem := Sem.State.Frame.set_pc (st1_sem) @fr pc') in |- *. destruct H4 with (st1_sem) [fr := fr2_sem] as (st'_sem, Htmp); trivial. destruct H6. split; trivial. simpl in |- *. rewrite H2 in |- *. unfold fr2_sem in |- *. destruct H8. split; trivial. destruct Htmp. exists st'_sem. split; trivial. apply OpSem.BlockStep_ok_next with (pc' := pc') (st1 := st1_sem) (fr2 := fr2_sem); trivial. destruct H5. destruct H10. rewrite H12 in |- *. trivial. destruct H1 with st_sem as (st'_sem, Htmp); trivial. destruct Htmp. exists st'_sem. split; trivial. apply OpSem.BlockStep_ok_last; trivial. destruct H2. destruct H5. rewrite H7 in |- *; trivial. Qed.
imports: Coq(List)