Changeset 2303 for src/RTLabs


Ignore:
Timestamp:
Aug 24, 2012, 5:41:18 PM (7 years ago)
Author:
campbell
Message:

Some preliminary checking of cost labelling properties in RTLabs.

Location:
src/RTLabs
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2297 r2303  
    1717   between labels to catch loops for soundness (is this sufficient?). *)
    1818
    19 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop
    20 λf,s. match s return λs. labels_present ? s → Prop with
     19definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → bool
     20λf,s. match s return λs. labels_present ? s → bool with
    2121[ St_cond _ l1 l2 ⇒ λH.
    22     is_cost_label (lookup_present … (f_graph f) l1 ?) = true
    23     is_cost_label (lookup_present … (f_graph f) l2 ?) = true
     22    is_cost_label (lookup_present … (f_graph f) l1 ?)
     23    is_cost_label (lookup_present … (f_graph f) l2 ?)
    2424(*| St_jumptable _ ls ⇒ λH.
    2525    (* I did have a dependent version of All here, but it's a pain. *)
    2626    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
    27 | _ ⇒ λ_. True
     27| _ ⇒ λ_. true
    2828]. whd in H;
    2929[ @(proj1 … H)
Note: See TracChangeset for help on using the changeset viewer.