proposition: Theorem sem_rac1_correct_sem_rac: forall p, (forall e st_sem st_sem' s, OpSem.ExpressionStep p e st_sem st_sem' s -> forall st_rac, CorrespondingState p st_rac st_sem -> exists st_rac', CorrespondingState p st_rac' st_sem' /\ OpRac1.ExpressionStep p e st_rac st_rac' s) /\ (forall l st_sem st_sem' s, OpSem.ListSteps p l st_sem st_sem' s -> forall st_rac, CorrespondingState p st_rac st_sem -> exists st_rac', CorrespondingState p st_rac' st_sem' /\ OpRac1.ListSteps p l st_rac st_rac' s) /\ (forall m b st_sem st_sem' s, OpSem.StatementStep p m b st_sem st_sem' s -> forall st_rac, CorrespondingState p st_rac st_sem -> exists st_rac', CorrespondingState p st_rac' st_sem' /\ OpRac1.StatementStep p m b st_rac st_rac' s) /\ (forall m b st_sem st_sem' s, OpSem.BlockStep p m b st_sem st_sem' s -> forall st_rac, CorrespondingState p st_rac st_sem -> exists st_rac', CorrespondingState p st_rac' st_sem' /\ OpRac1.BlockStep p m b st_rac st_rac' s).
proof: Proof. intro p. apply OpSem.mutual_ind; intros; simpl in *. rewrite <- H9 in H10. destruct H2 with (st_rac := st_rac) as (st1_rac, H21); trivial. destruct H21. destruct H5 with (st_rac := st1_rac) as (st2_rac, H61); trivial. destruct H61. exists (st2_rac) [h := Heap.update (st2_rac) @h loc v]. split. rewrite H10 in |- *. unfold CorrespondingState in H14. destruct H14. split; trivial. rewrite H14 in |- *; trivial. destruct H14. apply (OpRac1.assignment_instance_field_ok p e v obj fsig expr target st_rac st1_rac st2_rac (st2_rac) [h := Heap.update (st2_rac) @h loc v] st2_rac loc cn um); trivial. apply (Assignables.FieldUpdateCheck_Correct loc p st1_rac st1); trivial. rewrite <- H14;trivial. rewrite <- H14;trivial. destruct H1 with st_rac as (st1_rac, Htmp); trivial. destruct Htmp. clear H1. destruct H6 with st1_rac as (st2_rac, Htmp); trivial. destruct Htmp. clear H6. set (fr_c1_rac := NewFrame m' (lv2params m' (Ref this0 :: psv)) st2_rac) in |- *. set (st3_rac := (st2_rac) [fr := fr_c1_rac]) in |- *. set (st_c_rac := Assignables.MethodCallAction p c' m' st3_rac) in |- *. destruct H15 with st_c_rac as (st_c'_rac, Htmp). assert (CorrespondingState p st3_rac st3). unfold st3_rac 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_rac) (st_sem := st2); trivial. split; trivial. unfold st_c_rac in |- *. rewrite <- H11 in |- *. unfold NewFrame in fr_c1_rac. unfold Sem.NewFrame in H9. apply Assignables.MethodCallAction_Correct with (c := c') (m := m') (st_rac := st3_rac) (st_sem := st3) (st_rac_assignables := st2_rac@fr@assignables) (st_rac_fresh := st2_rac@fr@fresh); trivial. intuition. rewrite H9 in H10. rewrite H10. trivial. destruct Htmp. set (st'_rac := Assignables.MethodReturnAction p st_c'_rac st2_rac) in |- *. exists st'_rac. split. unfold st'_rac in |- *. rewrite <- H17 in |- *. apply Assignables.MethodReturnAction_Correct with st2_rac st_c'_rac st2 st_c';trivial. apply (OpRac1.method_vcall_ok p e st_rac st1_rac st2_rac st3_rac st_c_rac st_c'_rac st'_rac fr_c1_rac 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_rac := Assignables.NewObjectAction p o st_rac) in |- *. exists (st1_rac) [h := h']. split. assert (CorrespondingState p st1_rac st1). unfold st1_rac in |- *. rewrite <- H1 in |- *. apply Assignables.NewObjectAction_Correct with o st_rac st; trivial. rewrite H2. destruct H4. split; trivial. apply OpRac1.new_object_ok with (st1 := st1_rac) (h' := h') (cn := cn) (um := um); trivial. destruct H3. rewrite H3 in H0; trivial. exists st_rac. rewrite <- H in |- *. split; trivial. apply OpRac1.ListSteps_nil; trivial. destruct H1 with st_rac as (st1_rac, Htmp); trivial. destruct Htmp. destruct H3 with st1_rac as (st'_rac, Htmp); trivial. destruct Htmp. exists st'_rac. split; trivial. apply OpRac1.ListSteps_cons_ok with (e := e) (le := le) (st1 := st1_rac); trivial. destruct H1 with st_rac as (st'_rac, Htmp); trivial. destruct Htmp. exists st'_rac. split; trivial. apply OpRac1.expr_stmt_ok with (v := v) (e := e); trivial. destruct H2. destruct H5. rewrite <- H7 in |- *; trivial. destruct H1 with st_rac as (st1_rac, Htmp); trivial. destruct Htmp. set (fr2_rac := State.Frame.set_pc (st1_rac) @fr pc') in |- *. destruct H4 with (st1_rac) [fr := fr2_rac] as (st'_rac, Htmp); trivial. destruct H6. split; trivial. simpl in |- *. rewrite H2 in |- *. unfold fr2_rac in |- *. destruct H8. split; trivial. destruct Htmp. exists st'_rac. split; trivial. apply OpRac1.BlockStep_ok_next with (pc' := pc') (st1 := st1_rac) (fr2 := fr2_rac); trivial. destruct H5. destruct H10. rewrite <- H12 in |- *. trivial. destruct H1 with st_rac as (st'_rac, Htmp); trivial. destruct Htmp. exists st'_rac. split; trivial. apply OpRac1.BlockStep_ok_last; trivial. destruct H2. destruct H5. rewrite <- H7 in |- *; trivial. Qed.
imports: Coq(List)