Changeset 3030 for src/Clight/label.ma


Ignore:
Timestamp:
Mar 29, 2013, 12:09:07 PM (7 years ago)
Author:
campbell
Message:

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r3021 r3030  
    280280
    281281
    282 
    283 definition clight_label : clight_program → clight_program × costlabel ≝
    284 λp.
     282(* Use a let rec to prevent premature unfolding in correctness.ma. *)
     283
     284let rec clight_label (p:clight_program) : clight_program × costlabel ≝
    285285  let costgen ≝ new_universe CostTag in
    286286  let 〈init_cost, costgen〉 ≝ fresh … costgen in
    287287  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
     288
     289
     290lemma unfold_clight_label : ∀p.
     291  clight_label p =
     292  (let costgen ≝ new_universe CostTag in
     293  let 〈init_cost, costgen〉 ≝ fresh … costgen in
     294  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉).
     295* //
     296qed.
Note: See TracChangeset for help on using the changeset viewer.