Lines Matching refs:lookup
74 `(fdom cmp bmap = {a | ?x. lookup cmp a bmap = SOME x}) /\
75 (frange cmp bmap = {x | ?a. lookup cmp a bmap = SOME x})`;
128 !x. lookup cmp x bmap = FLOOKUP (to_fmap cmp bmap) {x}
137 ==> (lookup cmp b (insert cmp a y bmap) = SOME y)
148 ==> (lookup cmp b (insert cmp a y bmap) = lookup cmp b bmap)
159 (lookup cmp b (insert cmp a y bmap) =
162 else lookup cmp b bmap)
171 (lookup cmp x (bmap_of_list cmp fmap list) = SOME (fmap ' x))
183 (lookup cmp x (bmap_of_list cmp fmap list) = NONE)
195 (lookup cmp x (bmap_of cmp fmap) =
206 eq_cmp cmp ==> !x. FLOOKUP fmap x = lookup cmp x (bmap_of cmp fmap)
307 (lookup cmp x bmap = lookup cmp y bmap)
313 fapply cmp bmap x = THE (lookup cmp x bmap)
320 (lookup cmp x t1 = lookup cmp x t2)
325 member cmp x fmap <=> ?y. lookup cmp x fmap = SOME y
334 (lookup cmp r (Bin n k v fmap fmap') = SOME x)
337 ((cmp r k = Less) /\ (lookup cmp r fmap = SOME x)) \/
338 ((cmp r k = Greater) /\ (lookup cmp r fmap' = SOME x))
347 (lookup cmp k2 fmap = SOME x)
363 (lookup cmp k2 fmap = SOME x)
421 >> `lookup cmp x' (insert cmp x v bmap) = lookup cmp x' t` by metis_tac[]
557 (lookup cmp x (FOLDR (\(k,v:unit) t. insert cmp (f k) () t) bset list) = SOME ())
561 ((!a. MEM (a,()) list ==> (x <> f a)) /\ (lookup cmp x bset = SOME ()))
630 >> pat_elim `lookup _ __ ___ = SOME ()`