Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2303 r2307  
    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 → bool ≝
    20 λf,s. match s return λs. labels_present ? s → bool with
     19definition well_cost_labelled_statement : ∀g:graph statement. ∀s. labels_present g s → bool ≝
     20λg,s. match s return λs. labels_present g s → bool with
    2121[ St_cond _ l1 l2 ⇒ λH.
    22     is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
    23     is_cost_label (lookup_present … (f_graph f) l2 ?)
     22    is_cost_label (lookup_present … g l1 ?) ∧
     23    is_cost_label (lookup_present … g l2 ?)
    2424(*| St_jumptable _ ls ⇒ λH.
    2525    (* I did have a dependent version of All here, but it's a pain. *)
    26     All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
     26    All … (λl. ∃H. is_cost_label (lookup_present … g l H) = true) ls*)
    2727| _ ⇒ λ_. true
    2828]. whd in H;
     
    3232
    3333definition well_cost_labelled_fn : internal_function → Prop ≝
    34 λf. (∀l. ∀H:present … (f_graph f) l.
    35          well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
     34λf. (∀l,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (f_closed f l …)) ∧
    3635    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
    3736[ @lookup_lookup_present | cases (f_entry f) // ] qed.
Note: See TracChangeset for help on using the changeset viewer.