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

Some preliminary checking of cost labelling properties in RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2222 r2303  
    286286          (match m with [ an_id_map m' ⇒ m' ]) [ ].
    287287
     288(* Test a predicate on all of the entries in a map.  The predicate is given a
     289   proof that the entry appears in the map. *)
     290
     291definition idmap_all : ∀tag,A. ∀m:identifier_map tag A. (∀id,a. lookup tag A m id = Some A a → bool) → bool ≝
     292λtag,A,m,f. pm_all A (match m with [ an_id_map m' ⇒ m' ])
     293                     (λp,a,H. f (an_identifier tag p) a ?).
     294cases m in H ⊢ %; #m' normalize //
     295qed.
     296
     297inductive idmap_pred_graph : ∀tag,A,m,id,a,L. ∀f:(∀id,a. lookup tag A m id = Some A a → bool). bool → Prop ≝
     298| idmappg : ∀tag,A,m,id,a,L,f. idmap_pred_graph tag A m id a L f (f id a L).
     299
     300lemma idmap_pred_irr : ∀tag,A,m,id,a,L,L'. ∀f:(∀id,a. lookup tag A m id = Some A a → bool).
     301  f id a L = f id a L'.
     302#tag #A #m #id #a #L #L' #f
     303cut (idmap_pred_graph tag A m id a L f (f id a L)) [ % ]
     304cases (f id a L) #H
     305cut (idmap_pred_graph tag A m id a L' f ?) [ 2,5: @H | 1,4: skip ] * //
     306qed.
     307
     308lemma idmap_all_ok : ∀tag,A,m,f.
     309  bool_to_Prop (idmap_all tag A m f) ↔ (∀id,a,H. f id a H).
     310#tag #A * #m #f
     311whd in match (idmap_all ????); @(iff_trans … (pm_all_ok …)) %
     312[ #H * #id #a #PR lapply (H id a PR) #X @eq_true_to_b <X @idmap_pred_irr
     313| #H #p #a #PR @H
     314] qed.
     315
     316
    288317axiom MissingId : String.
    289318
     
    318347] qed.
    319348
    320 include "ASM/Util.ma".
    321 
    322349definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
    323350λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     
    332359| #a #H @refl
    333360] qed.
     361
     362lemma lookup_is_present : ∀tag,T,m,id,t.
     363  lookup tag T m id = Some T t →
     364  present ?? m id.
     365#tag #T #m #id #t #L normalize >L % #E destruct
     366qed.
     367
     368lemma lookup_present_eq : ∀tag,T,m,id,t.
     369  lookup tag T m id = Some T t →
     370  ∀H. lookup_present tag T m id H = t.
     371#tag #T #m #id #t #L #H
     372lapply (lookup_lookup_present … H) >L #E destruct %
     373qed.
     374
    334375
    335376definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
Note: See TracChangeset for help on using the changeset viewer.