Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r3063 r3081  
    170170qed.
    171171
    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. *)
    173177
    174178lemma prefix_preserved :
     
    429433  @IH @Ntl
    430434] 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. *)
    431442
    432443lemma measurable_subtrace_preserved :
     
    777788] qed.
    778789
    779 (* TODO: move*)
    780 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
    781 #x0 elim x0
    782 [ #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 l1
    796 [ //
    797 | #h #t #IH #l2
    798   whd in ⊢ (?% → ?(?%?));
    799   cases (p h) //
    800   @IH
    801 ] qed.
    802 
    803790
    804791lemma ends_at_return_normal : ∀C,g,t1,t2.
     
    825812
    826813
     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. *)
    827819
    828820theorem measured_subtrace_preserved :
Note: See TracChangeset for help on using the changeset viewer.