Changeset 2314


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
Files:
2 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2307 r2314  
    13891389qed.
    13901390
     1391lemma not_orb : ∀b,c:bool.
     1392  ¬ (b∨c) →
     1393  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
     1394* * normalize /2/
     1395qed.
     1396
    13911397lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    13921398 *; /2 by eq_true_false, I/
  • 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
  • src/common/Identifiers.ma

    r2307 r2314  
    347347] qed.
    348348
     349lemma present_member : ∀tag,A,m,id.
     350  present tag A m id → member tag A m id.
     351#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
     352qed.
     353
    349354definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
    350355λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     
    988993qed.
    989994 
    990 
     995(* Link a map with the set consisting of its domain. *)
     996
     997definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     998λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
     999
     1000lemma id_set_of_map_subset : ∀tag,A,m.
     1001  id_set_of_map tag A m ⊆ m.
     1002#tag #A * #m * #id normalize
     1003>lookup_opt_map normalize cases (lookup_opt ???) //
     1004qed.
     1005
     1006lemma id_set_of_map_present : ∀tag,A,m,id.
     1007  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
     1008#tag #A * #m * #id %
     1009normalize @not_to_not
     1010>lookup_opt_map cases (lookup_opt ???) normalize //
     1011#a #E destruct
     1012qed.
     1013
     1014lemma id_set_of_map_card : ∀tag,A,m.
     1015  |m| = |id_set_of_map tag A m|.
     1016#tag #A * #m whd in ⊢ (??%%); >map_size //
     1017qed.
     1018
     1019
     1020
  • src/utilities/lists.ma

    r2306 r2314  
    5858]
    5959qed.
     60
     61(* Boolean predicate version of All *)
     62
     63let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
     64match l with
     65[ nil ⇒ true
     66| cons h t ⇒ P h ∧ all A P t
     67].
     68
     69lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
     70#A #P #l elim l
     71[ % //
     72| #h #t * #IH #IH' %
     73  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
     74  | * #p #H whd in ⊢ (?%); >p /2/
     75  ]
     76] qed.
     77
    6078
    6179let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.