Changeset 2314

Timestamp:

Aug 31, 2012, 4:12:35 PM (9 years ago)

Author:

campbell

Message:

Move generic definitions from recent commit to appropriate places.

Location:

src

Files:

• ASM/Util.ma (modified) (1 diff)
• RTLabs/CostCheck.ma (modified) (5 diffs)
• RTLabs/Traces.ma (modified) (2 diffs)
• common/Identifiers.ma (modified) (2 diffs)
• utilities/bool.ma (added)
• utilities/listb.ma (added)
• utilities/lists.ma (modified) (1 diff)

src/ASM/Util.ma

@@ -1389 +1389 @@
 qed.
 
+lemma not_orb : ∀b,c:bool.
+  ¬ (b∨c) →
+  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
+* * normalize /2/
+qed.
+
 lemma eq_false_to_notb: ∀b. b = false → ¬ b.
  *; /2 by eq_true_false, I/

src/RTLabs/CostCheck.ma

@@ -1 +1 @@
 
 include "RTLabs/CostSpec.ma".
-
-(* TODO: move ----→ *)
-
-lemma Exists_to_All : ∀T,P,l.
-  (∀x. Exists ? (λy. y = x) l → P x) →
-  All T P l.
-#T #P #l elim l [ // | #h #t #IH #H % [ @H %1 % | @IH #t #E @H %2 @E ] ]
-qed.
-
-let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
-match l with
-[ nil ⇒ true
-| cons h t ⇒ P h ∧ all A P t
-].
-
-lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
-#A #P #l elim l
-[ % //
-| #h #t * #IH #IH' %
-  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
-  | * #p #H whd in ⊢ (?%); >p /2/
-  ]
-] qed.
-
-(* ←---- move *)
+include "utilities/bool.ma".
+include "utilities/listb.ma".
 
 definition check_well_cost_fn : internal_function → bool ≝
@@ -47 +24 @@
 ] qed.
 
-include "basics/lists/listb.ma".
 include alias "utilities/deqsets.ma".
 
@@ -143 +119 @@
 
 (* TODO: move (or is it somewhere already?) *)
-lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
-  (b → P e1) →
-  (¬b → P e2) →
-  P (if b then e1 else e2).
-#T * /2/
-qed.
-
-lemma not_orb : ∀b,c:bool.
-  ¬ (b∨c) →
-  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
-* * normalize /2/
-qed.
 
 lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
-  (∀l. l∈to_check → ¬ l∈checking::checking_tail) →
+  (∀l. l∈to_check → ¬ memb ? l (checking::checking_tail)) →
   check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
   check_label_bounded_spec g checking checking_tail to_check to_check'.
@@ -263 +227 @@
 ] qed.
 
-lemma present_member : ∀tag,A,m,id.
-  present tag A m id → member tag A m id.
-#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
-qed.
-
-(* TODO: move and eliminate dup in Traces.ma *)
-lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
-  Exists S (λy. y = x) l →
-  x ∈ l.
-#S #x #l elim l 
-[ //
-| #h #t #IH
-  normalize lapply (eqb_true … x h)
-  cases (x==h) *
-  [ #E #_ >(E (refl ??)) //
-  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
-            | #H @IH @H
-            ]
-  ]
-] qed.
-
 lemma successors_inv : ∀st,x,y,zs.
   successors st = x::y::zs →
@@ -571 +514 @@
 ] qed.
 
-  
-(* TODO: move *)
-definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
-λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
-
-lemma id_set_of_map_subset : ∀tag,A,m.
-  id_set_of_map tag A m ⊆ m.
-#tag #A * #m * #id normalize
->lookup_opt_map normalize cases (lookup_opt ???) //
-qed.
-
-lemma id_set_of_map_present : ∀tag,A,m,id.
-  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
-#tag #A * #m * #id %
-normalize @not_to_not
->lookup_opt_map cases (lookup_opt ???) normalize //
-#a #E destruct
-qed.
-
-lemma id_set_of_map_card : ∀tag,A,m.
-  |m| = |id_set_of_map tag A m|.
-#tag #A * #m whd in ⊢ (??%%); >map_size //
-qed.
-
+ 
 definition check_sound_cost_fn : internal_function → bool ≝
 λfn.

src/RTLabs/Traces.ma

@@ -6 +6 @@
 include "common/Executions.ma".
 include "utilities/deqsets.ma".
+include "utilities/listb.ma".
 
 discriminator status_class.
@@ -2391 +2392 @@
 ] qed.
 
-(* TODO: move *)
-lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
-  Exists S (λy. y = x) l →
-  x ∈ l.
-#S #x #l elim l 
-[ //
-| #h #t #IH
-  normalize lapply (eqb_true … x h)
-  cases (x==h) *
-  [ #E #_ >(E (refl ??)) //
-  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
-            | #H @IH @H
-            ]
-  ]
-] qed.
 
 (* We need to link the pcs, states of the semantics with the labels and graphs

src/common/Identifiers.ma

@@ -347 +347 @@
 ] qed.
 
+lemma present_member : ∀tag,A,m,id.
+  present tag A m id → member tag A m id.
+#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
+qed.
+
 definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
 λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
@@ -988 +993 @@
 qed.
   
-
+(* Link a map with the set consisting of its domain. *)
+
+definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
+λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
+
+lemma id_set_of_map_subset : ∀tag,A,m.
+  id_set_of_map tag A m ⊆ m.
+#tag #A * #m * #id normalize
+>lookup_opt_map normalize cases (lookup_opt ???) //
+qed.
+
+lemma id_set_of_map_present : ∀tag,A,m,id.
+  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
+#tag #A * #m * #id %
+normalize @not_to_not
+>lookup_opt_map cases (lookup_opt ???) normalize //
+#a #E destruct
+qed.
+
+lemma id_set_of_map_card : ∀tag,A,m.
+  |m| = |id_set_of_map tag A m|.
+#tag #A * #m whd in ⊢ (??%%); >map_size //
+qed.
+
+
+

src/utilities/lists.ma

@@ -58 +58 @@
 ]
 qed.
+
+(* Boolean predicate version of All *)
+
+let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
+match l with
+[ nil ⇒ true
+| cons h t ⇒ P h ∧ all A P t
+].
+
+lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
+#A #P #l elim l
+[ % //
+| #h #t * #IH #IH' %
+  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
+  | * #p #H whd in ⊢ (?%); >p /2/
+  ]
+] qed.
+
 
 let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝