Changeset 2307 for src/RTLabs/CostSpec.ma

Timestamp:

Aug 30, 2012, 4:47:58 PM (8 years ago)

Author:

campbell

Message:

Half the proofs for sound cost labelling check.

File:

• src/RTLabs/CostSpec.ma (modified) (2 diffs)

src/RTLabs/CostSpec.ma

@@ -17 +17 @@
    between labels to catch loops for soundness (is this sufficient?). *)
 
-definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → bool ≝
-λf,s. match s return λs. labels_present ? s → bool with
+definition well_cost_labelled_statement : ∀g:graph statement. ∀s. labels_present g s → bool ≝
+λg,s. match s return λs. labels_present g s → bool with
 [ St_cond _ l1 l2 ⇒ λH.
-    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
-    is_cost_label (lookup_present … (f_graph f) l2 ?)
+    is_cost_label (lookup_present … g l1 ?) ∧
+    is_cost_label (lookup_present … g l2 ?)
 (*| St_jumptable _ ls ⇒ λH.
     (* I did have a dependent version of All here, but it's a pain. *)
-    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
+    All … (λl. ∃H. is_cost_label (lookup_present … g l H) = true) ls*)
 | _ ⇒ λ_. true
 ]. whd in H;
@@ -32 +32 @@
 
 definition well_cost_labelled_fn : internal_function → Prop ≝
-λf. (∀l. ∀H:present … (f_graph f) l.
-         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
+λf. (∀l,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (f_closed f l …)) ∧
     is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
 [ @lookup_lookup_present | cases (f_entry f) // ] qed.