src/n-bit/wordsScript.sml

188     (FCP i. l <= i /\ i <= MIN h ^HB /\ w ' i):'a word`
192     (FCP i. i + l <= MIN h ^HB /\ w ' (i + l)):'a word`
196     (FCP i. l <= MIN h ^HB /\ w ' (MIN (i + l) (MIN h ^HB))):'a word`
1306              (n2w (SLICE (MIN h ^HB) l n)):'a word`,
1311              (n2w (BITS (MIN h ^HB) l n)):'a word`,
1312   FIELD_WORD_TAC \\ Cases_on `i + l <= MIN h ^HB`
1328      n2w (SIGN_EXTEND (MIN (SUC h) (dimindex(:'a)) - l) (dimindex(:'a))
1329             (BITS (MIN h ^HB) l n))`,
1361   `!h t. MIN (MIN h t) (t + l) = MIN h t`,
1367      word_sign_extend (MIN (SUC h) (dimindex(:'a)) - l) ((h -- l) w)`,
1389  `(!m n. MIN m (m + n) = m) /\ !m n. MIN (m + n) m = m`,
1393   `MIN a (MIN b (MIN (c + a) (c + b))) = MIN a b`,
1397   `!x y. x <= y ==> (MIN x y = x)`, RW_TAC arith_ss [MIN_DEF])
1401        w2w ((MIN h (dimindex (:'b) - 1) -- l) w)`,
1540 val lem = Q.prove(`MIN d (l1 + MIN h2 d) = MIN (h2 + l1) d`,
1545                    ((MIN h1 (h2 + l1)) -- (l2 + l1)) w`,
1630          (MIN m (MIN (h + n)
1631            (MIN (dimindex(:'c) - 1) (dimindex(:'b) + n - 1))) >< l + n) w`,
1659          simpLib.SIMP_PROVE arith_ss [MIN_DEF] ``l <= h ==> (MIN h l = l)``])
1724          (MIN h (MIN (dimindex(:'b) + l - 1)
1749          (MIN h (MIN (dimindex(:'b) + l - 1)
1906   `!i a b. MIN (LOG2 a) (LOG2 b) < i ==> ~BIT i a \/ ~BIT i b`,
1925         BIT i (BITWISE (SUC (MIN (LOG2 a) (LOG2 b))) op a b))`,
1927     \\ Cases_on `l <= SUC (MIN (LOG2 a) (LOG2 b))`
1929     \\ Cases_on `i < SUC (MIN (LOG2 a) (LOG2 b))`
1932     \\ `MIN (LOG2 a) (LOG2 b) < i` by DECIDE_TAC
1953   `!n m. n2w n && n2w m = n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m)`,
1980       ~(n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m))`,
2645            ``0 < m /\ SUC n < m ==> (MIN n (m - 1) = n)``]
2919        Tw << (^WL - MIN n ^WL) || w >>> n
3038        simpLib.SIMP_PROVE arith_ss [MIN_DEF] ``MIN a (a + b) = a``,
3196          ((MIN h (MIN (dimindex(:'b) + l - 1)
3207          ((MIN h (MIN (dimindex(:'b) + l - 1)