Changeset 2025


Ignore:
Timestamp:
Jun 7, 2012, 3:51:11 PM (5 years ago)
Author:
campbell
Message:

Silly typo and old comment.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1960 r2025  
    563563  well_cost_labelled_state s →
    564564  well_cost_labelled_state s'.
    565 #ge #s #tr' #s' #EV cases (eval_perserves … EV)
     565#ge #s #tr' #s' #EV cases (eval_preserves … EV)
    566566[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
    567567| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
     
    772772  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    773773  stack_preserved doesnt_end_with_ret s1 s2.
    774 #ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
     774#ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
    775775[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
    776776| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
     
    794794[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
    795795| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
    796   inversion (eval_perserves … EV)
     796  inversion (eval_preserves … EV)
    797797  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
    798798  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
     
    808808  ]
    809809| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
    810   inversion (eval_perserves … EV)
     810  inversion (eval_preserves … EV)
    811811  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
    812812  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
     
    834834[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
    835835| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
    836   inversion (eval_perserves … EV)
     836  inversion (eval_preserves … EV)
    837837  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
    838838  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
     
    848848  ]
    849849| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
    850   inversion (eval_perserves … EV)
     850  inversion (eval_preserves … EV)
    851851  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
    852852  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
     
    14461446    *)
    14471447    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
    1448     inversion (eval_perserves … EVAL)
     1448    inversion (eval_preserves … EVAL)
    14491449    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
    14501450      >(eval_steps … EVAL) in E2; #En normalize in En;
     
    14711471  /3/
    14721472| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
    1473   #EVAL #NC %2 inversion (eval_perserves … EVAL)
     1473  #EVAL #NC %2 inversion (eval_preserves … EVAL)
    14741474  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
    14751475  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
     
    15261526  soundly_labelled_state s'.
    15271527#ge #s #tr #s' #ENV #EV #S
    1528 inversion (eval_perserves … EV)
     1528inversion (eval_preserves … EV)
    15291529[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
    15301530  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
     
    16321632  RTLabs_is_final s' = None ?.
    16331633#ge #s #tr #s' #EV
    1634 inversion (eval_perserves … EV) //
     1634inversion (eval_preserves … EV) //
    16351635#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
    16361636@⊥ @(absurd ?? CL) @refl
     
    17181718      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
    17191719        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
    1720         inversion (eval_perserves … EV)
     1720        inversion (eval_preserves … EV)
    17211721        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
    17221722        #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
     
    18311831@bind_ok #f #_
    18321832#E destruct
    1833 #EV #SP inversion (eval_perserves … EV)
     1833#EV #SP inversion (eval_preserves … EV)
    18341834[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
    18351835     inversion SP
  • src/RTLabs/semantics.ma

    r1999 r2025  
    1 
    2 (* XXX NB: I haven't checked all of these semantics against the prototype
    3            compilers yet! *)
    41
    52include "basics/lists/list.ma".
     
    267264] qed.
    268265
    269 lemma eval_perserves : ∀ge,s,tr,s'.
     266lemma eval_preserves : ∀ge,s,tr,s'.
    270267  eval_statement ge s = Value ??? 〈tr,s'〉 →
    271268  state_rel ge s s'.
Note: See TracChangeset for help on using the changeset viewer.