Changeset 2314 for src/RTLabs
 Timestamp:
 Aug 31, 2012, 4:12:35 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2313 r2314 1 1 2 2 include "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 *) 3 include "utilities/bool.ma". 4 include "utilities/listb.ma". 28 5 29 6 definition check_well_cost_fn : internal_function → bool ≝ … … 47 24 ] qed. 48 25 49 include "basics/lists/listb.ma".50 26 include alias "utilities/deqsets.ma". 51 27 … … 143 119 144 120 (* 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.157 121 158 122 lemma 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)) → 160 124 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → 161 125 check_label_bounded_spec g checking checking_tail to_check to_check'. … … 263 227 ] qed. 264 228 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 l275 [ //276  #h #t #IH277 normalize lapply (eqb_true … x h)278 cases (x==h) *279 [ #E #_ >(E (refl ??)) //280  #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct281  #H @IH @H282 ]283 ]284 ] qed.285 286 229 lemma successors_inv : ∀st,x,y,zs. 287 230 successors st = x::y::zs → … … 571 514 ] qed. 572 515 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 597 517 definition check_sound_cost_fn : internal_function → bool ≝ 598 518 λfn. 
src/RTLabs/Traces.ma
r2313 r2314 6 6 include "common/Executions.ma". 7 7 include "utilities/deqsets.ma". 8 include "utilities/listb.ma". 8 9 9 10 discriminator status_class. … … 2391 2392 ] qed. 2392 2393 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 l2398 [ //2399  #h #t #IH2400 normalize lapply (eqb_true … x h)2401 cases (x==h) *2402 [ #E #_ >(E (refl ??)) //2403  #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct2404  #H @IH @H2405 ]2406 ]2407 ] qed.2408 2394 2409 2395 (* 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.