Changeset 3081 for src/common/FEMeasurable.ma
 Timestamp:
 Apr 3, 2013, 5:54:34 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r3063 r3081 170 170 qed. 171 171 172 172 (* First show that the trace up to the start of the measurable subtrace (i.e., 173 the prefix of the execution) is preserved using the simulation results in 174 the meas_sim record. Note that this doesn't end cleanly  the first states 175 in the measurable subtrace may not be in the simulation relation, see the 176 comment below. *) 173 177 174 178 lemma prefix_preserved : … … 429 433 @IH @Ntl 430 434 ] qed. 435 436 (* Now show the preservation of parts of the measurable subtrace from states in 437 simulation to the end. (We'll deal with any extra steps at the start from 438 the prefix lemma in the theorem below.) The basic idea here is that having 439 broken up the simulation results into normal, call, return and cost lemmas, 440 we can match up the structure of the two executions, and in particular 441 prove the will_return_aux predicate for the target execution. *) 431 442 432 443 lemma measurable_subtrace_preserved : … … 777 788 ] qed. 778 789 779 (* TODO: move*)780 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.781 #x0 elim x0782 [ #y %{y} %2 %783  #x #IH *784 [ %{(S x)} %1 %785  #y cases (IH y) #z *786 [ #H %{z} %1 >H //787  #H %{z} %2 >H //788 ]789 ]790 ] qed.791 792 lemma all_append : ∀A,p,l1,l2.793 all A p (l1@l2) →794 all A p l1 ∧ all A p l2.795 #A #p #l1 elim l1796 [ //797  #h #t #IH #l2798 whd in ⊢ (?% → ?(?%?));799 cases (p h) //800 @IH801 ] qed.802 803 790 804 791 lemma ends_at_return_normal : ∀C,g,t1,t2. … … 825 812 826 813 814 (* Now put the two main lemmas above together to show that the target has a 815 [measurable] subtrace, and that the observables are the same. 816 817 To deal with the extra steps from the prefix lemma, note that they are 818 "normal" steps, and so cannot interfere with the structure. *) 827 819 828 820 theorem measured_subtrace_preserved :
Note: See TracChangeset
for help on using the changeset viewer.