Changeset 1562 for src/common


Ignore:
Timestamp:
Nov 25, 2011, 1:20:41 PM (8 years ago)
Author:
mulligan
Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1535 r1562  
    5959qed.
    6060
     61axiom eq_identifier_sym:
     62  ∀tag: String.
     63  ∀l  : identifier tag.
     64  ∀r  : identifier tag.
     65    eq_identifier tag l r = eq_identifier tag r l.
     66
    6167lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
    6268#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     
    105111qed.
    106112
     113lemma lookup_def_add_hit : ∀tag,A,m,i,a,d.
     114  lookup_def tag A (add tag A m i a) i d = a.
     115#tag #A * #m * #i #a #d
     116@lookup_insert_hit
     117qed.
     118
    107119lemma lookup_add_miss : ∀tag,A,m,i,j,a.
    108120  i ≠ j →
     
    111123@lookup_opt_insert_miss /2/
    112124qed.
     125
     126axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d.
     127  i ≠ j →
     128  lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d.
    113129
    114130lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
  • src/common/PositiveMap.ma

    r1555 r1562  
    2424 | Some r ⇒ r
    2525 ].
    26  
     26
    2727let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
    2828match b with
     
    7777  ]
    7878] qed.
     79
     80axiom lookup_insert_hit:
     81  ∀a: Type[0].
     82  ∀v: a.
     83  ∀b: Pos.
     84  ∀t: positive_map a.
     85  ∀d: a.
     86    lookup … b (insert … b v t) d = v.
    7987
    8088lemma lookup_opt_insert_miss:
Note: See TracChangeset for help on using the changeset viewer.