Changeset 1070 for src/common


Ignore:
Timestamp:
Jul 15, 2011, 12:56:48 PM (8 years ago)
Author:
campbell
Message:

Show that entry and exit labels are in the RTLabs graph.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1068 r1070  
    4343  else OK ? it.
    4444
    45 definition eq_identifier ≝
    46   λt.
    47   λl, r: identifier t.
     45definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     46  λt,l,r.
    4847  match l with
    4948  [ an_identifier l' ⇒
     
    5352    ]
    5453  ].
     54
     55lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
     56  (x = y → P true) → (x ≠ y → P false) →
     57  P (eq_identifier t x y).
     58#P #t * #x * #y #T #F
     59change with (P (eq_bv ???))
     60@eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
     61qed.
    5562   
    5663definition word_of_identifier ≝
     
    9097λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    9198                                           (match m with [ an_id_map m' ⇒ m' ])).
     99
     100lemma lookup_add_hit : ∀tag,A,m,i,a.
     101  lookup tag A (add tag A m i a) i = Some ? a.
     102#tag #A * #m * #i #a
     103@lookup_opt_insert_hit
     104qed.
     105
     106lemma lookup_add_miss : ∀tag,A,m,i,j,a.
     107  (notb (eq_identifier tag i j)) →
     108  lookup tag A (add tag A m j a) i = lookup tag A m i.
     109#tag #A * #m * #i * #j #a
     110change with (notb (eq_bv ???) → ?)
     111@lookup_opt_insert_miss
     112qed.
     113
     114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
     115  (∃v. lookup tag A m i = Some ? v) →
     116  ∃v. lookup tag A (add tag A m j a) i = Some ? v.
     117#tag #A #m #i #j #a * #v #H
     118lapply (lookup_add_miss … m i j a)
     119@eq_identifier_elim
     120[ #E #_ %{a} >E @lookup_add_hit
     121| #_ #H' %{v} <H @H' %
     122] qed.
    92123
    93124(* Extract every identifier, value pair from the map. *)
Note: See TracChangeset for help on using the changeset viewer.