Changeset 2314
- Timestamp:
- Aug 31, 2012, 4:12:35 PM (9 years ago)
- Location:
- src
- Files:
-
- 2 added
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r2307 r2314 1389 1389 qed. 1390 1390 1391 lemma not_orb : ∀b,c:bool. 1392 ¬ (b∨c) → 1393 (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)). 1394 * * normalize /2/ 1395 qed. 1396 1391 1397 lemma eq_false_to_notb: ∀b. b = false → ¬ b. 1392 1398 *; /2 by eq_true_false, I/ -
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 -
src/common/Identifiers.ma
r2307 r2314 347 347 ] qed. 348 348 349 lemma 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 ??)) 352 qed. 353 349 354 definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝ 350 355 λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ]. … … 988 993 qed. 989 994 990 995 (* Link a map with the set consisting of its domain. *) 996 997 definition 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 1000 lemma 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 ???) // 1004 qed. 1005 1006 lemma 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 % 1009 normalize @not_to_not 1010 >lookup_opt_map cases (lookup_opt ???) normalize // 1011 #a #E destruct 1012 qed. 1013 1014 lemma 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 // 1017 qed. 1018 1019 1020 -
src/utilities/lists.ma
r2306 r2314 58 58 ] 59 59 qed. 60 61 (* Boolean predicate version of All *) 62 63 let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝ 64 match l with 65 [ nil ⇒ true 66 | cons h t ⇒ P h ∧ all A P t 67 ]. 68 69 lemma 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 60 78 61 79 let 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.