Changeset 20 for Csemantics/Smallstep.ma
 Timestamp:
 Aug 19, 2010, 12:36:03 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Smallstep.ma
r3 r20 461 461 Variable final_state1: state1 > int > Prop. 462 462 Variable ge1: genv1. 463 463 *) 464 465 nrecord semantics : Type[1] ≝ 466 { trans :> transrel 467 ; initial : (state trans) → Prop 468 ; final : (state trans) → int → Prop 469 ; ge : (genv trans) 470 }. 471 472 (* 464 473 (** The second smallstep semantics is also axiomatized. *) 465 474 … … 486 495 final_state1 st1 r > 487 496 final_state2 st2 r. 488 497 *) 498 499 nrecord related_semantics : Type[1] ≝ 500 { sem1 : semantics 501 ; sem2 : semantics 502 ; match_states : state sem1 → state sem2 → Prop 503 ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2 504 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r 505 }. 506 507 (* 489 508 (** Simulation when one transition in the first program 490 509 corresponds to zero, one or several transitions in the second program. … … 508 527 (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1)) 509 528 /\ match_states st1' st2'. 510 511 Lemma simulation_star_star: 512 forall st1 t st1', star step1 ge1 st1 t st1' > 513 forall st2, match_states st1 st2 > 514 exists st2', star step2 ge2 st2 t st2' /\ match_states st1' st2'. 515 Proof. 516 induction 1; intros. 517 exists st2; split. apply star_refl. auto. 518 destruct (simulation H H2) as [st2' [A B]]. 519 destruct (IHstar _ B) as [st3' [C D]]. 520 exists st3'; split; auto. 521 apply star_trans with t1 st2' t2; auto. 522 destruct A as [F  [F G]]. 523 apply plus_star; auto. 524 auto. 525 Qed. 526 529 *) 530 nrecord order_sim : Type[1] ≝ 531 { sem :> related_semantics 532 ; order : state (sem1 sem) → state (sem1 sem) → Prop 533 (* ; order_wf ? *) 534 ; simulation : ∀st1,t,st1'. step (sem1 sem) (ge (sem1 sem)) st1 t st1' → 535 ∀st2. match_states sem st1 st2 → 536 ∃st2'. (plus (sem2 sem) (ge (sem2 sem)) st2 t st2' ∨ 537 (star (sem2 sem) (ge (sem2 sem)) st2 t st2' ∧ 538 order st1' st1)) 539 ∧ match_states sem st1' st2' 540 }. 541 542 nlemma simulation_star_star: ∀sim:order_sim. 543 ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' → 544 ∀st2. match_states sim st1 st2 → 545 ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'. 546 #sim st1 t st1' H; nelim H; 547 ##[ #st1'' st2 Hmatch; 548 @ st2; @; //; 549 ## #st1 tA st1A tB st1B t Hstep Hstar Ht IH st2 Hmatch; 550 nelim (simulation sim ??? Hstep ? Hmatch); #st2'; *; #A B; 551 nelim (IH ? B); #st3'; *; #C D; 552 @ st3'; @; //; 553 napply (star_trans ??? tA st2' ? tB); //; 554 nelim A; /2/; *; //; 555 ##] nqed. 556 557 (* 527 558 Lemma simulation_star_forever_silent: 528 559 forall st1 st2,
Note: See TracChangeset
for help on using the changeset viewer.