Changeset 2307 for src/RTLabs/CostSpec.ma
- Timestamp:
- Aug 30, 2012, 4:47:58 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/CostSpec.ma
r2303 r2307 17 17 between labels to catch loops for soundness (is this sufficient?). *) 18 18 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 with19 definition 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 21 21 [ 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 ?) 24 24 (*| St_jumptable _ ls ⇒ λH. 25 25 (* 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*) 27 27 | _ ⇒ λ_. true 28 28 ]. whd in H; … … 32 32 33 33 definition 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 …)) ∧ 36 35 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true. 37 36 [ @lookup_lookup_present | cases (f_entry f) // ] qed.
Note: See TracChangeset
for help on using the changeset viewer.