Lines Matching refs:lookup
50 val lookup_def = tzDefine "lookup" `
51 (lookup k LN = NONE) /\
52 (lookup k (LS a) = if k = 0 then SOME a else NONE) /\
53 (lookup k (BN t1 t2) =
55 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) /\
56 (lookup k (BS t1 a t2) =
58 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2))
148 ``!k a t. lookup k (insert k a t) = SOME a``,
177 ``!k2 v t k1. lookup k1 (insert k2 v t) =
178 if k1 = k2 then SOME v else lookup k1 t``,
239 ``!m1 m2 k. lookup k (union m1 m2) =
240 case lookup k m1 of
241 NONE => lookup k m2
329 ``lookup k (mk_BN t1 t2) = lookup k (BN t1 t2)``,
333 ``lookup k (mk_BS t1 x t2) = lookup k (BS t1 x t2)``,
338 ``!m1 m2 k. lookup k (inter m1 m2) =
339 case (lookup k m1,lookup k m2) of
348 ``!m1 m2 k. lookup k (inter_eq m1 m2) =
349 case lookup k m1 of
351 | SOME v => (if lookup k m2 = SOME v then SOME v else NONE)``,
358 ``((lookup x (inter t1 t2) = SOME y) <=>
359 (lookup x t1 = SOME y) /\ lookup x t2 <> NONE) /\
360 ((lookup x (inter t1 t2) = NONE) <=>
361 (lookup x t1 = NONE) \/ (lookup x t2 = NONE))``,
365 ``lookup x (inter t1 (inter t2 t3)) =
366 lookup x (inter (inter t1 t2) t3)``,
371 ``!m1 m2 k. lookup k (difference m1 m2) =
372 if lookup k m2 = NONE then lookup k m1 else NONE``,
507 ``lookup n (fromList l) = if n < LENGTH l then SOME (EL n l)
510 `!i n t. lookup n (SND (FOLDL (\ (i,t) a. (i+1,insert i a t)) (i,t) l)) =
511 if n < i then lookup n t
513 else lookup n t`
540 ``!t k. k IN domain t <=> ?v. lookup k t = SOME v``,
547 ``lookup x (inter t1 t2) =
548 if x IN domain t2 then lookup x t1 else NONE``,
550 \\ Cases_on `lookup x t2` \\ fs [] \\ Cases_on `lookup x t1` \\ fs []);
554 ``(lookup k t = NONE) <=> k NOTIN domain t``,
555 simp[domain_lookup] >> Cases_on `lookup k t` >> simp[]);
561 qx_gen_tac `k` >> Cases_on `lookup k t1` >> simp[]);
567 rw [] >> Cases_on `lookup x t1` >> fs[] >>
580 rw [] >> Cases_on `lookup x t1`
581 >> fs[] >> Cases_on `lookup x t2` >> rw[]);
606 lookup k1 (delete k2 t) = if k1 = k2 then NONE
607 else lookup k1 t``,
748 lookup k (mapi0 f i pt) =
749 case lookup k pt of NONE => NONE
756 `lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)`,
766 THE (lookup n t))) (domain t)``,
782 ``!t k v. MEM (k,v) (toAList t) <=> (lookup k t = SOME v)``,
784 \\ Cases_on `lookup k t` \\ fs []
788 ``!t x. ALOOKUP (toAList t) x = lookup x t``,
789 strip_tac>>strip_tac>>Cases_on `lookup x t` >-
982 ``!t acc x. MEM x (toListA acc t) <=> (MEM x acc \/ ?k. lookup k t = SOME x)``,
996 ``!x t. MEM x (toList t) <=> ?k. lookup k t = SOME x``,
1029 ((t1 = t2) <=> !n. lookup n t1 = lookup n t2)``,
1118 ``!x t. lookup x (mk_wf t) = lookup x t``,
1127 ``!t1 t2. (mk_wf t1 = mk_wf t2) <=> !x. lookup x t1 = lookup x t2``,
1133 !x. lookup x (inter t1 t2) = lookup x (inter t3 t4)``,
1183 \\ Cases_on `lookup x t1` \\ fs []
1184 \\ Cases_on `lookup x t2` \\ fs []
1185 \\ Cases_on `lookup x t3` \\ fs []);
1234 LIST_CONJ (prove (``lookup (NUMERAL n) t = lookup n t``,
1270 ``!ls x.lookup x (fromAList ls) = ALOOKUP ls x``,
1284 ``!t x. lookup x (fromAList (toAList t)) = lookup x t``,
1339 ``!s x. lookup x (map f s) = OPTION_MAP f (lookup x s)``,
1448 !x y. (lookup x t1 = SOME y) ==> (lookup x t2 = SOME y)`,
1473 \\ `lookup 0 t2 = SOME a` by
1495 (lookup k sp2 = lookup k sp1)`,
1530 lookup k (FOLDL union t ls) =
1531 FOLDL OPTION_CHOICE (lookup k t) (MAP (lookup k) ls)
1546 !k. (lookup k t1 = NONE) <=> (lookup k t2 = NONE)
1550 \\ Cases_on `lookup k t1` \\ fs []
1551 \\ Cases_on `lookup k t2` \\ fs [])
1553 \\ Cases_on `lookup x t1` \\ fs []
1554 \\ Cases_on `lookup x t2` \\ fs [])
1568 ``!k t f. lookup k (filter_v f t) = case lookup k t of
1602 `lookup i (mk_BN t1 t2) =
1604 else lookup ((i - 1) DIV 2) (if EVEN i then t1 else t2)`,
1648 Cases_on `lookup n t1` >> fs[] >> Cases_on `lookup n t2` >> fs[]);
1674 if lookup n t = NONE then size t else size t - 1`,
1681 `!k. LENGTH args <= k ==> (lookup k (fromList args) = NONE)`,
1725 `!t n. lookup n (map (K x) t) = if n IN domain t then SOME x else NONE`,
1765 \\ Cases_on `lookup x' z` \\ fs []
1803 !xs. lookup x (list_to_num_set xs) = if MEM x xs then SOME () else NONE
1825 !t n. lookup n (map (K x) t) = if n IN domain t then SOME x else NONE
1842 (lookup z (alist_insert x y t) =
1843 case ALOOKUP (ZIP(x,y)) z of SOME a => SOME a | NONE => lookup z t)
1934 (lookup x t = SOME y) ==> (insert x y t = t)
2015 !spt. lookup 0 spt = spt_center spt
2021 lookup i (spt_right spt) = lookup ((i * 2) + 1) spt
2029 lookup i (spt_left spt) = lookup ((i * 2) + 2) spt
2129 lookup i spt = SOME v <=>
2131 (?j. i = j * 2 + 1 /\ lookup j (spt_right spt) = SOME v) \/
2132 (?j. i = j * 2 + 2 /\ lookup j (spt_left spt) = SOME v)
2237 /\ lookup k (EL j (expand_rle xs)) = SOME x
2307 MEM (i, x) (toSortedAList spt) = (lookup i spt = SOME x)
2320 ALOOKUP (toSortedAList spt) i = lookup i spt
2322 Cases_on `lookup i spt`