Package word: Parametric theory of words

Information

nameword
version1.1
descriptionParametric theory of words
authorJoe Hurd <joe@gilith.com>
licenseMIT
show Data.Bool
Data.List
Data.Word
Number.Numeral

Files

Defined Type Operator

Defined Constants

Theorems

¬(modulus = 0)

w. Bits.normal (Bits.fromWord w)

toNatural (Bits.toWord []) = 0

x. Number.Natural.< (toNatural x) modulus

x. fromNatural (toNatural x) = x

w. Bits.toWord (Bits.fromWord w) = w

w. length (Bits.fromWord w) = width

n. Number.Natural.< (Number.Natural.mod n modulus) modulus

modulus = Number.Natural.exp 2 width

x. Number.Natural.div (toNatural x) modulus = 0

x. toNatural (fromNatural x) = Number.Natural.mod x modulus

l. Bits.normal l length l = width

x. ¬x = fromNatural (Number.Natural.- modulus (toNatural x))

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

w. Bits.fromWord w = map (bit w) (interval 0 width)

n. Number.Natural.< n modulus Number.Natural.mod n modulus = n

n.
    Number.Natural.mod (Number.Natural.mod n modulus) modulus =
    Number.Natural.mod n modulus

x y. x < y ¬(y x)

x y. x - y = x + ¬y

l.
    Number.Natural.< (toNatural (Bits.toWord l))
      (Number.Natural.exp 2 (length l))

l. length l = width Bits.fromWord (Bits.toWord l) = l

x y. x < y Number.Natural.< (toNatural x) (toNatural y)

x y. x y Number.Natural.≤ (toNatural x) (toNatural y)

w1 w2. Bits.fromWord w1 = Bits.fromWord w2 w1 = w2

x y. toNatural x = toNatural y x = y

w1 w2. Bits.fromWord w1 = Bits.fromWord w2 w1 = w2

w n. bit w n Number.Natural.odd (toNatural (shiftRight w n))

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

w1 w2. Bits.compare T (Bits.fromWord w1) (Bits.fromWord w2) w1 w2

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

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

l.
    Number.Natural.≤ width (length l)
    Bits.fromWord (Bits.toWord l) = take width l

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

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

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

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

n.
    Bits.toWord
      (Number.Natural.odd n ::
       Bits.fromWord (fromNatural (Number.Natural.div n 2))) =
    fromNatural n

w n.
    bit w n
    Number.Natural.odd
      (Number.Natural.div (toNatural w) (Number.Natural.exp 2 n))

w n.
    shiftLeft w n =
    fromNatural (Number.Natural.* (Number.Natural.exp 2 n) (toNatural w))

w n.
    shiftRight w n =
    fromNatural (Number.Natural.div (toNatural w) (Number.Natural.exp 2 n))

x y.
    fromNatural x = fromNatural y
    Number.Natural.mod x modulus = Number.Natural.mod y modulus

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

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

l.
    Number.Natural.≤ (length l) width
    Bits.fromWord (Bits.toWord l) =
    l @ replicate (Number.Natural.- width (length l)) F

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

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

l.
    Number.Natural.<
      (Number.Natural.+ (Number.Natural.* 2 (toNatural (Bits.toWord l))) 1)
      (Number.Natural.exp 2 (Number.Natural.suc (length l)))

x y.
    Number.Natural.< x modulus Number.Natural.< y modulus
    fromNatural x = fromNatural y x = y

l n.
    bit (Bits.toWord l) n
    Number.Natural.< n width Number.Natural.< n (length l) nth n l

n.
    fromNatural n =
    Bits.toWord
      (if n = 0 then []
       else
         Number.Natural.odd n ::
         Bits.fromWord (fromNatural (Number.Natural.div n 2)))

l.
    Bits.fromWord (Bits.toWord l) =
    if Number.Natural.≤ (length l) width then
      l @ replicate (Number.Natural.- width (length l)) F
    else take width l

h t.
    toNatural (Bits.toWord (h :: t)) =
    Number.Natural.mod
      (Number.Natural.+ (Number.Natural.* 2 (toNatural (Bits.toWord t)))
         (if h then 1 else 0)) modulus

h t.
    Number.Natural.<
      (Number.Natural.+ (Number.Natural.* 2 (toNatural (Bits.toWord t)))
         (if h then 1 else 0))
      (Number.Natural.exp 2 (Number.Natural.suc (length t)))

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

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

Bits.toWord [] = fromNatural 0
  h t.
    Bits.toWord (h :: t) =
    if h then shiftLeft (Bits.toWord t) 1 + fromNatural 1
    else shiftLeft (Bits.toWord t) 1

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

(q. Bits.compare q [] [] q)
  q h1 h2 t1 t2.
    Bits.compare q (h1 :: t1) (h2 :: t2)
    Bits.compare (¬h1 h2 ¬(h1 ¬h2) q) t1 t2

Input Type Operators

Input Constants

Assumptions

T

n. Number.Natural.≤ 0 n

n. Number.Natural.≤ n n

F p. p

x. Function.id x = x

t. t ¬t

n. Number.Natural.< 0 (Number.Natural.suc n)

(¬) = λp. p F

() = λP. P ((select) P)

a. x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx. T

x. x = x T

n. ¬(Number.Natural.suc n = 0)

n. Number.Natural.even n Number.Natural.odd n

m. Number.Natural.+ m 0 = m

n. Number.Natural.- n n = 0

n. Number.Natural.even (Number.Natural.* 2 n)

n. bit0 n = Number.Natural.+ n n

n. ¬Number.Natural.even n Number.Natural.odd n

n. ¬Number.Natural.odd n Number.Natural.even n

n. Number.Natural.div n 1 = n

n. Number.Natural.exp n 1 = n

n. Number.Natural.mod n 1 = 0

l. take (length l) l = l

x. (select y. y = x) = x

m n. Number.Natural.≤ m (Number.Natural.+ m n)

m n. Number.Natural.≤ n (Number.Natural.+ m n)

() = λp q. p q p

t. (t T) (t F)

n. Number.Natural.odd (Number.Natural.suc (Number.Natural.* 2 n))

m. Number.Natural.suc m = Number.Natural.+ m 1

n. bit1 n = Number.Natural.suc (Number.Natural.+ n n)

x y. Data.Pair.fst (Data.Pair., x y) = x

x y. Data.Pair.snd (Data.Pair., x y) = y

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

n x. length (replicate n x) = n

m n. length (interval m n) = n

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

P x. P x P ((select) P)

(¬T F) (¬F T)

n. Number.Natural.< 0 n ¬(n = 0)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

a b. (a b) a b

m n. Number.Natural.* m n = Number.Natural.* n m

m n. m = n Number.Natural.≤ m n

m n. Number.Natural.< m n Number.Natural.≤ m n

m n. Number.Natural.< m n Number.Natural.≤ n m

m n. Number.Natural.≤ m n Number.Natural.≤ n m

m n. Number.Natural.- m (Number.Natural.+ m n) = 0

m n. Number.Natural.- (Number.Natural.+ m n) m = n

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

n. Number.Natural.* 2 n = Number.Natural.+ n n

m n. ¬(Number.Natural.< m n Number.Natural.≤ n m)

m n. ¬(Number.Natural.≤ m n Number.Natural.< n m)

m n. ¬Number.Natural.< m n Number.Natural.≤ n m

m n. ¬Number.Natural.≤ m n Number.Natural.< n m

m n. Number.Natural.< m (Number.Natural.suc n) Number.Natural.≤ m n

m n. Number.Natural.≤ (Number.Natural.suc m) n Number.Natural.< m n

m. m = 0 n. m = Number.Natural.suc n

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

n. Number.Natural.even n Number.Natural.mod n 2 = 0

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

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

m n. Number.Natural.< m n Number.Natural.div m n = 0

m n. Number.Natural.< m n Number.Natural.mod m n = m

m n. Number.Natural.< m (Number.Natural.+ m n) Number.Natural.< 0 n

m n. Number.Natural.suc m = Number.Natural.suc n m = n

m n.
    Number.Natural.< (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.< m n

m n.
    Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.≤ m n

m n. Number.Natural.+ m n = m n = 0

m n. Number.Natural.- m n = 0 Number.Natural.≤ m n

n. Number.Natural.odd n Number.Natural.mod n 2 = 1

m. Number.Natural.- 0 m = 0 Number.Natural.- m 0 = m

m n.
    Number.Natural.even (Number.Natural.* m n)
    Number.Natural.even m Number.Natural.even n

m n.
    Number.Natural.even (Number.Natural.+ m n) Number.Natural.even m
    Number.Natural.even n

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

m n. ¬(n = 0) Number.Natural.≤ (Number.Natural.div m n) m

m n. ¬(n = 0) Number.Natural.≤ (Number.Natural.mod m n) m

l m. length (l @ m) = Number.Natural.+ (length l) (length m)

P. (p. P p) p1 p2. P (Data.Pair., p1 p2)

m n. Number.Natural.≤ m n d. n = Number.Natural.+ m d

f g. f = g x. f x = g x

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

(Number.Natural.even 0 T)
  n. Number.Natural.even (Number.Natural.suc n) ¬Number.Natural.even n

(Number.Natural.odd 0 F)
  n. Number.Natural.odd (Number.Natural.suc n) ¬Number.Natural.odd n

m n. Number.Natural.≤ m n Number.Natural.< m n m = n

m n. Number.Natural.≤ m n Number.Natural.≤ n m m = n

n l. Number.Natural.≤ n (length l) length (take n l) = n

m n.
    Number.Natural.< m n
    d. n = Number.Natural.+ m (Number.Natural.suc d)

P. (x y. P x y) y x. P x y

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

m n. ¬(m = 0) Number.Natural.div (Number.Natural.* m n) m = n

m n. ¬(m = 0) Number.Natural.mod (Number.Natural.* m n) m = 0

P Q. (x. P x Q) (x. P x) Q

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

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

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

p q r. p q r p q r

n x i. Number.Natural.< i n nth i (replicate n x) = x

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

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

m n p. Number.Natural.+ m n = Number.Natural.+ m p n = p

m n p.
    Number.Natural.< (Number.Natural.+ m n) (Number.Natural.+ m p)
    Number.Natural.< n p

m n p.
    Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ m p)
    Number.Natural.≤ n p

m n p.
    Number.Natural.≤ (Number.Natural.+ m p) (Number.Natural.+ n p)
    Number.Natural.≤ m n

m n p.
    Number.Natural.- (Number.Natural.+ m n) (Number.Natural.+ m p) =
    Number.Natural.- n p

m n p.
    Number.Natural.< m n Number.Natural.≤ n p Number.Natural.< m p

m n p.
    Number.Natural.≤ m n Number.Natural.< n p Number.Natural.< m p

m n p.
    Number.Natural.≤ m n Number.Natural.≤ n p Number.Natural.≤ m p

P x. (y. P y y = x) (select) P = x

P. (x. y. P x y) y. x. P x (y x)

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

m n. Number.Natural.* m n = 0 m = 0 n = 0

m n. Number.Natural.+ m n = 0 m = 0 n = 0

length [] = 0 h t. length (h :: t) = Number.Natural.suc (length t)

P. P 0 (n. P n P (Number.Natural.suc n)) n. P n

(t. ¬¬t t) (¬T F) (¬F T)

m n. ¬(n = 0) (Number.Natural.div m n = 0 Number.Natural.< m n)

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

m n. Number.Natural.exp m n = 0 m = 0 ¬(n = 0)

m n i.
    Number.Natural.< i n nth i (interval m n) = Number.Natural.+ m i

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

m n p.
    Number.Natural.* m (Number.Natural.- n p) =
    Number.Natural.- (Number.Natural.* m n) (Number.Natural.* m p)

m n p.
    Number.Natural.exp m (Number.Natural.+ n p) =
    Number.Natural.* (Number.Natural.exp m n) (Number.Natural.exp m p)

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

m n p.
    Number.Natural.* (Number.Natural.- m n) p =
    Number.Natural.- (Number.Natural.* m p) (Number.Natural.* n p)

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x) (x. Q x) x. P x Q x

P Q. (x. P x) (x. Q x) x. P x Q x

e f. fn. fn 0 = e n. fn (Number.Natural.suc n) = f (fn n) n

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

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

m n p. Number.Natural.* m n = Number.Natural.* m p m = 0 n = p

m n p.
    Number.Natural.≤ (Number.Natural.* m n) (Number.Natural.* m p)
    m = 0 Number.Natural.≤ n p

m n p.
    Number.Natural.≤ (Number.Natural.* m p) (Number.Natural.* n p)
    Number.Natural.≤ m n p = 0

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

m n p.
    Number.Natural.< (Number.Natural.* m n) (Number.Natural.* m p)
    ¬(m = 0) Number.Natural.< n p

(x. replicate 0 x = [])
  n x. replicate (Number.Natural.suc n) x = x :: replicate n x

x y a b. Data.Pair., x y = Data.Pair., a b x = a y = b

m n p q.
    Number.Natural.< m p Number.Natural.< n q
    Number.Natural.< (Number.Natural.+ m n) (Number.Natural.+ p q)

m n p q.
    Number.Natural.≤ m n Number.Natural.≤ p q
    Number.Natural.≤ (Number.Natural.* m p) (Number.Natural.* n q)

m n p q.
    Number.Natural.≤ m p Number.Natural.≤ n q
    Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ p q)

(m. interval m 0 = [])
  m n.
    interval m (Number.Natural.suc n) =
    m :: interval (Number.Natural.suc m) n

(m. Number.Natural.exp m 0 = 1)
  m n.
    Number.Natural.exp m (Number.Natural.suc n) =
    Number.Natural.* m (Number.Natural.exp m n)

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

(l. drop 0 l = l)
  n h t. drop (Number.Natural.suc n) (h :: t) = drop n t

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

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

m n p.
    ¬(Number.Natural.* n p = 0)
    Number.Natural.div (Number.Natural.div m n) p =
    Number.Natural.div m (Number.Natural.* n p)

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

n l i.
    Number.Natural.≤ n (length l) Number.Natural.< i n
    nth i (take n l) = nth i l

(m. Number.Natural.< m 0 F)
  m n.
    Number.Natural.< m (Number.Natural.suc n)
    m = n Number.Natural.< m n

(l. [] @ l = l) h t l. (h :: t) @ l = h :: t @ l

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

(f. map f [] = []) f h t. map f (h :: t) = f h :: map f t

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

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

m n p.
    ¬(Number.Natural.* n p = 0)
    Number.Natural.mod (Number.Natural.div m n) p =
    Number.Natural.div (Number.Natural.mod m (Number.Natural.* n p)) n

k l m.
    nth k (l @ m) =
    if Number.Natural.< k (length l) then nth k l
    else nth (Number.Natural.- k (length l)) m

(m. Number.Natural.≤ m 0 m = 0)
  m n.
    Number.Natural.≤ m (Number.Natural.suc n)
    m = Number.Natural.suc n Number.Natural.≤ m n

(h t. nth 0 (h :: t) = h)
  h t n. nth (Number.Natural.suc n) (h :: t) = nth n t

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

l m.
    length l = length m
    (i. Number.Natural.< i (length l) nth i l = nth i m) l = m

m n q r.
    m = Number.Natural.+ (Number.Natural.* q n) r Number.Natural.< r n
    Number.Natural.div m n = q Number.Natural.mod m n = r

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)

x m n.
    Number.Natural.≤ (Number.Natural.exp x m) (Number.Natural.exp x n)
    if x = 0 then m = 0 n = 0 else x = 1 Number.Natural.≤ m n

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

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

a b n.
    ¬(n = 0)
    (Number.Natural.mod (Number.Natural.+ a b) n =
     Number.Natural.+ (Number.Natural.mod a n) (Number.Natural.mod b n)
     Number.Natural.div (Number.Natural.+ a b) n =
     Number.Natural.+ (Number.Natural.div a n) (Number.Natural.div b n))

(n. Number.Natural.+ 0 n = n) (m. Number.Natural.+ m 0 = m)
  (m n.
     Number.Natural.+ (Number.Natural.suc m) n =
     Number.Natural.suc (Number.Natural.+ m n))
  m n.
    Number.Natural.+ m (Number.Natural.suc n) =
    Number.Natural.suc (Number.Natural.+ m n)

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

(n. Number.Natural.* 0 n = 0) (m. Number.Natural.* m 0 = 0)
  (n. Number.Natural.* 1 n = n) (m. Number.Natural.* m 1 = m)
  (m n.
     Number.Natural.* (Number.Natural.suc m) n =
     Number.Natural.+ (Number.Natural.* m n) n)
  m n.
    Number.Natural.* m (Number.Natural.suc n) =
    Number.Natural.+ m (Number.Natural.* m n)