Changeset 20
 Timestamp:
 Aug 19, 2010, 12:36:03 PM (11 years ago)
 Location:
 Csemantics
 Files:

 5 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Cexec.ma
r17 r20 865 865 nwhd; napply (star_step … IH); //; 866 866 nqed. 867 868 nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) : 869 res (trace×state) ≝ 870 match is_final_state s with 871 [ inl _ ⇒ OK ? 〈E0, s〉 872  inr _ ⇒ 873 match n with 874 [ O ⇒ OK ? 〈E0, s〉 875  S n' ⇒ 876 〈t,s'〉 ← exec_step ge s;: 877 〈t',s''〉 ← exec_steps_without_proof n' ge s';: 878 OK ? 〈t ⧺ t',s''〉 879 ] 880 ]. 
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.