Changeset 2314 for src/RTLabs


Ignore:
Timestamp:
Aug 31, 2012, 4:12:35 PM (7 years ago)
Author:
campbell
Message:

Move generic definitions from recent commit to appropriate places.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2313 r2314  
    11
    22include "RTLabs/CostSpec.ma".
    3 
    4 (* TODO: move ----→ *)
    5 
    6 lemma Exists_to_All : ∀T,P,l.
    7   (∀x. Exists ? (λy. y = x) l → P x) →
    8   All T P l.
    9 #T #P #l elim l [ // | #h #t #IH #H % [ @H %1 % | @IH #t #E @H %2 @E ] ]
    10 qed.
    11 
    12 let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
    13 match l with
    14 [ nil ⇒ true
    15 | cons h t ⇒ P h ∧ all A P t
    16 ].
    17 
    18 lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
    19 #A #P #l elim l
    20 [ % //
    21 | #h #t * #IH #IH' %
    22   [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
    23   | * #p #H whd in ⊢ (?%); >p /2/
    24   ]
    25 ] qed.
    26 
    27 (* ←---- move *)
     3include "utilities/bool.ma".
     4include "utilities/listb.ma".
    285
    296definition check_well_cost_fn : internal_function → bool ≝
     
    4724] qed.
    4825
    49 include "basics/lists/listb.ma".
    5026include alias "utilities/deqsets.ma".
    5127
     
    143119
    144120(* TODO: move (or is it somewhere already?) *)
    145 lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
    146   (b → P e1) →
    147   (¬b → P e2) →
    148   P (if b then e1 else e2).
    149 #T * /2/
    150 qed.
    151 
    152 lemma not_orb : ∀b,c:bool.
    153   ¬ (b∨c) →
    154   (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
    155 * * normalize /2/
    156 qed.
    157121
    158122lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
    159   (∀l. l∈to_check → ¬ l∈checking::checking_tail) →
     123  (∀l. l∈to_check → ¬ memb ? l (checking::checking_tail)) →
    160124  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
    161125  check_label_bounded_spec g checking checking_tail to_check to_check'.
     
    263227] qed.
    264228
    265 lemma present_member : ∀tag,A,m,id.
    266   present tag A m id → member tag A m id.
    267 #tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
    268 qed.
    269 
    270 (* TODO: move and eliminate dup in Traces.ma *)
    271 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
    272   Exists S (λy. y = x) l →
    273   x ∈ l.
    274 #S #x #l elim l
    275 [ //
    276 | #h #t #IH
    277   normalize lapply (eqb_true … x h)
    278   cases (x==h) *
    279   [ #E #_ >(E (refl ??)) //
    280   | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
    281             | #H @IH @H
    282             ]
    283   ]
    284 ] qed.
    285 
    286229lemma successors_inv : ∀st,x,y,zs.
    287230  successors st = x::y::zs →
     
    571514] qed.
    572515
    573  
    574 (* TODO: move *)
    575 definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
    576 λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
    577 
    578 lemma id_set_of_map_subset : ∀tag,A,m.
    579   id_set_of_map tag A m ⊆ m.
    580 #tag #A * #m * #id normalize
    581 >lookup_opt_map normalize cases (lookup_opt ???) //
    582 qed.
    583 
    584 lemma id_set_of_map_present : ∀tag,A,m,id.
    585   present tag A m id ↔ present tag unit (id_set_of_map … m) id.
    586 #tag #A * #m * #id %
    587 normalize @not_to_not
    588 >lookup_opt_map cases (lookup_opt ???) normalize //
    589 #a #E destruct
    590 qed.
    591 
    592 lemma id_set_of_map_card : ∀tag,A,m.
    593   |m| = |id_set_of_map tag A m|.
    594 #tag #A * #m whd in ⊢ (??%%); >map_size //
    595 qed.
    596 
     516 
    597517definition check_sound_cost_fn : internal_function → bool ≝
    598518λfn.
  • src/RTLabs/Traces.ma

    r2313 r2314  
    66include "common/Executions.ma".
    77include "utilities/deqsets.ma".
     8include "utilities/listb.ma".
    89
    910discriminator status_class.
     
    23912392] qed.
    23922393
    2393 (* TODO: move *)
    2394 lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
    2395   Exists S (λy. y = x) l →
    2396   x ∈ l.
    2397 #S #x #l elim l
    2398 [ //
    2399 | #h #t #IH
    2400   normalize lapply (eqb_true … x h)
    2401   cases (x==h) *
    2402   [ #E #_ >(E (refl ??)) //
    2403   | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
    2404             | #H @IH @H
    2405             ]
    2406   ]
    2407 ] qed.
    24082394
    24092395(* We need to link the pcs, states of the semantics with the labels and graphs
Note: See TracChangeset for help on using the changeset viewer.