src/finite_maps/sptreeScript.sml

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`