Package word: Parametric theory of words

Information

nameword
version1.120
descriptionParametric theory of words
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
hol-light-int-filehol-light.int
hol-light-thm-filehol-light.art
checksume07d7d674090b50f2185c413b9773f91d7018127
requiresbase
natural-bits
natural-divides
probability
word-witness
showData.Bool
Data.List
Data.Word
Data.Word.Bits
Number.Natural
Probability.Random

Files

Defined Type Operator

Defined Constants

Theorems

¬(modulus = 0)

w. normal (fromWord w)

x. x x

fromNatural modulus = 0

toWord [] = 0

toNatural (toWord []) = 0

modulus mod modulus = 0

0 mod modulus = 0

x. ¬(x < x)

x. toNatural x < modulus

~0 = 0

x. ~~x = x

x. fromNatural (toNatural x) = x

w. toWord (fromWord w) = w

w. length (fromWord w) = width

w. Bits.width (toNatural w) width

n. n mod modulus < modulus

n. n mod modulus n

modulus = 2 width

q. compare q [] [] q

w. Bits.fromList (fromWord w) = toNatural w

x. x + 0 = x

x. x 1 = x

x. 0 + x = x

x. toNatural x div modulus = 0

l. toWord l = fromNatural (Bits.fromList l)

w. fromWord w = Bits.toVector (toNatural w) width

x. x 0 = 1

x. x * 0 = 0

x. x + ~x = 0

x. 0 * x = 0

x. ~x + x = 0

x. toNatural x mod modulus = toNatural x

w. Bits.bound (toNatural w) width = toNatural w

x. x * 1 = x

x. 1 * x = x

n. toNatural (fromNatural n) = n mod modulus

n. toNatural (fromNatural n) = Bits.bound n width

r. random r = fromNatural (Uniform.random modulus r)

l. normal l length l = width

x. ~x = fromNatural (modulus - toNatural x)

w. not w = toWord (map (¬) (fromWord w))

l. normal l fromWord (toWord l) = l

x y. x * y = y * x

x y. x + y = y + x

n. divides modulus n n mod modulus = 0

n. n < modulus toNatural (fromNatural n) = n

n. n < modulus n mod modulus = n

x. fromNatural x = 0 divides modulus x

n. n mod modulus mod modulus = n mod modulus

x y. x - y = x + ~y

x y. ¬(x < y) y x

x y. ¬(x y) y < x

w n. bit w n Bits.bit (toNatural w) n

x. ~x = 0 x = 0

l. toNatural (toWord l) < 2 length l

x y. x < y toNatural x < toNatural y

x y. x y toNatural x toNatural y

x y. x * ~y = ~(x * y)

x y. ~x * y = ~(x * y)

w1 w2. fromWord w1 = fromWord w2 w1 = w2

x y. ~x = ~y x = y

x y. toNatural x = toNatural y x = y

w1 w2. fromWord w1 = fromWord w2 w1 = w2

w n. shiftLeft w n = fromNatural (Bits.shiftLeft (toNatural w) n)

w n. shiftRight w n = fromNatural (Bits.shiftRight (toNatural w) n)

m n. fromNatural (m n) = fromNatural m n

w1 w2. and w1 w2 = fromNatural (Bits.and (toNatural w1) (toNatural w2))

w1 w2. or w1 w2 = fromNatural (Bits.or (toNatural w1) (toNatural w2))

x y. x + y = x y = 0

x y. y + x = x y = 0

x y. ~x + ~y = ~(x + y)

w1 w2. compare (fromWord w1) (fromWord w2) w1 < w2

w1 w2. compare (fromWord w1) (fromWord w2) w1 w2

x n. x suc n = x * x n

x1 y1. fromNatural (x1 * y1) = fromNatural x1 * fromNatural y1

x1 y1. fromNatural (x1 + y1) = fromNatural x1 + fromNatural y1

w1 w2. and w1 w2 = toWord (zipWith () (fromWord w1) (fromWord w2))

w1 w2. or w1 w2 = toWord (zipWith () (fromWord w1) (fromWord w2))

l n. shiftLeft (toWord l) n = toWord (replicate n @ l)

x y. toNatural (x * y) = toNatural x * toNatural y mod modulus

x y. toNatural (x + y) = (toNatural x + toNatural y) mod modulus

x y z. x * y * z = x * (y * z)

x y z. x + y + z = x + (y + z)

x y z. x + y = x + z y = z

x y z. y + x = z + x y = z

x1 x2 x3. x1 < x2 x2 < x3 x1 < x3

x1 x2 x3. x1 < x2 x2 x3 x1 < x3

x1 x2 x3. x1 x2 x2 < x3 x1 < x3

x1 x2 x3. x1 x2 x2 x3 x1 x3

n. 0 n = if n = 0 then 1 else 0

k w. bit (not w) k k < width ¬bit w k

x y. fromNatural x = fromNatural y x mod modulus = y mod modulus

x y z. x * (y + z) = x * y + x * z

x y z. (y + z) * x = y * x + z * x

x m n. x m * x n = x (m + n)

k w1 w2. bit (and w1 w2) k bit w1 k bit w2 k

k w1 w2. bit (or w1 w2) k bit w1 k bit w2 k

m n. (m mod modulus) * (n mod modulus) mod modulus = m * n mod modulus

m n. (m mod modulus + n mod modulus) mod modulus = (m + n) mod modulus

q w1 w2.
    compare q (fromWord w1) (fromWord w2) if q then w1 w2 else w1 < w2

w1 w2. (i. i < width (bit w1 i bit w2 i)) w1 = w2

x y. x < modulus y < modulus fromNatural x = fromNatural y x = y

l n. bit (toWord l) n n < width n < length l nth l n

q l1 l2.
    length l1 = length l2
    (compare q l1 l2
     Bits.compare q (Bits.fromList l1) (Bits.fromList l2))

l.
    fromWord (toWord l) =
    if length l width then l @ replicate (width - length l)
    else take width l

h t.
    toWord (h :: t) =
    if h then 1 + shiftLeft (toWord t) 1 else shiftLeft (toWord t) 1

l n.
    length l width
    shiftRight (toWord l) n =
    if length l n then toWord [] else toWord (drop n l)

l n.
    width length l
    shiftRight (toWord l) n =
    if width n then toWord [] else toWord (drop n (take width l))

q h1 h2 t1 t2.
    compare q (h1 :: t1) (h2 :: t2)
    compare (¬h1 h2 ¬(h1 ¬h2) q) t1 t2

l n.
    shiftRight (toWord l) n =
    if length l width then
      if length l n then toWord [] else toWord (drop n l)
    else if width n then toWord []
    else toWord (drop n (take width l))

External Type Operators

External Constants

Assumptions

¬

¬

length [] = 0

bit0 0 = 0

Bits.fromList [] = 0

t. t t

n. n n

p. p

t. t ¬t

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

x. replicate x 0 = []

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 * n = 0

n. 0 + n = n

m. m + 0 = m

n. n - n = 0

k. Bits.bound 0 k = 0

l. l @ [] = l

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m 0 = 1

k. Bits.fromList (replicate k) = 0

m. 1 * m = m

l. take (length l) l = l

l. Bits.width (Bits.fromList l) length l

m n. m m + n

n k. Bits.bound n k n

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

x n. length (replicate x n) = n

h t. head (h :: t) = h

h t. tail (h :: t) = t

n k. length (Bits.toVector n k) = k

b. fromBool b = if b then 1 else 0

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

l. length l = 0 l = []

x y. x = y y = x

t1 t2. t1 t2 t2 t1

m n. m * n = n * m

m n. m + n = n + m

m n. min m n = min n m

m n. m < n m n

f l. length (map f l) = length l

l. Bits.fromList l < 2 length l

h t. length (h :: t) = suc (length t)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

n k. Bits.fromList (Bits.toVector n k) = Bits.bound n k

() = λp q. (λf. f p q) = λf. f

n. Bits.shiftLeft n 1 = 2 * n

n. ¬(n = 0) n mod n = 0

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

h t. Bits.fromList (h :: t) = Bits.cons h (Bits.fromList t)

m n. m < n m div n = 0

m n. m < n m mod n = m

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

n k. Bits.toVector (Bits.bound n k) k = Bits.toVector n k

n. 0 n = if n = 0 then 1 else 0

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. min m n = if m n then m else n

m n. m suc n = m * m n

m n. ¬(n = 0) m mod n < n

m n. ¬(n = 0) m mod n m

n k. Bits.bound n k = n Bits.width n k

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

q n. Bits.compare q 0 n q ¬(n = 0)

n k. Bits.bound n k = n mod 2 k

m n. n m m - n + n = m

m n. m n n m m = n

n l. n length l length (take n l) = n

m n. m < n d. n = m + suc d

p. (x y. p x y) y x. p x y

h t. Bits.cons h t = fromBool h + 2 * t

n k. Bits.width n k n < 2 k

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

n j k. Bits.bound (Bits.bound n j) k = Bits.bound n (min j k)

m n p. m < n n < p m < p

m n p. m < n n p m < p

m n p. m n n < p m < p

m n p. m n n p m p

r. (x. y. r x y) f. x. r x (f x)

l i. Bits.bit (Bits.fromList l) i i < length l nth l i

l1 l2.
    Bits.fromList (l1 @ l2) =
    Bits.fromList l1 + Bits.shiftLeft (Bits.fromList l2) (length l1)

p. p 0 (n. p n p (suc n)) n. p n

a b. ¬(a = 0) (divides a b b mod a = 0)

n m. ¬(n = 0) m mod n mod n = m mod n

m n. m n = 0 m = 0 ¬(n = 0)

p q r. p (q r) p q p r

q m n. Bits.compare q m n if q then m n else m < n

m n i. Bits.bit (Bits.and m n) i Bits.bit m i Bits.bit n i

n i k. Bits.bit (Bits.bound n k) i i < k Bits.bit n i

m n i. Bits.bit (Bits.or m n) i Bits.bit m i Bits.bit n i

m n p. m * (n + p) = m * n + m * p

m n p. (m + n) * p = m * p + n * p

n j k.
    Bits.bound (Bits.shiftLeft n k) (j + k) =
    Bits.shiftLeft (Bits.bound n j) k

n j k.
    Bits.shiftRight (Bits.bound n (j + k)) k =
    Bits.bound (Bits.shiftRight n k) j

(∃!) = λp. () p x y. p x p y x = y

b f x y. f (if b then x else y) = if b then f x else f y

l k.
    Bits.shiftRight (Bits.fromList l) k =
    if length l k then 0 else Bits.fromList (drop k l)

m n k.
    Bits.toVector (Bits.and m n) k =
    zipWith () (Bits.toVector m k) (Bits.toVector n k)

m n k.
    Bits.toVector (Bits.or m n) k =
    zipWith () (Bits.toVector m k) (Bits.toVector n k)

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

m n. ¬(n = 0) (m div n) * n + m mod n = m

p. p [] (h t. p t p (h :: t)) l. p l

f l i. i < length l nth (map f l) i = f (nth l i)

p c x y. p (if c then x else y) (c p x) (¬c p y)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)

l k.
    Bits.toVector (Bits.fromList l) k =
    if length l k then l @ replicate (k - length l) else take k l

n m p. ¬(n = 0) (m mod n) * (p mod n) mod n = m * p mod n

n a b. ¬(n = 0) (a mod n + b mod n) mod n = (a + b) mod n

l1 l2.
    length l1 = length l2 (i. i < length l1 nth l1 i = nth l2 i)
    l1 = l2

q h1 h2 t1 t2.
    Bits.compare q (Bits.cons h1 t1) (Bits.cons h2 t2)
    Bits.compare (¬h1 h2 ¬(h1 ¬h2) q) t1 t2