Package hol-sort: HOL sorting theories
Information
| name | hol-sort |
| version | 1.0 |
| description | HOL sorting theories |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 2a19552fa096e1ae820a442a23ebdf3cf7723373 |
| requires | base hol-base |
| show | Data.Bool Data.List Data.Pair Function HOL4 Number.Natural Relation |
Files
- Package tarball hol-sort-1.0.tgz
- Theory source file hol-sort.thy (included in the package tarball)
Defined Constants
- HOL4
- mergesort
- mergesort.merge
- mergesort.merge_tail
- mergesort.merge_tail_tupled
- mergesort.merge_tupled
- mergesort.mergesort
- mergesort.mergesortN
- mergesort.mergesortN_tail
- mergesort.mergesortN_tail_tupled
- mergesort.mergesortN_tupled
- mergesort.mergesort_tail
- mergesort.sort2
- mergesort.sort2_tail
- mergesort.sort3
- mergesort.sort3_tail
- mergesort.stable
- sorting
- sorting.PART
- sorting.PART3
- sorting.PARTITION
- sorting.PERM
- sorting.PERM_SINGLE_SWAP
- sorting.QSORT
- sorting.QSORT3
- sorting.QSORT3_tupled
- sorting.QSORT_tupled
- sorting.SORTED
- sorting.SORTED_tupled
- sorting.SORTS
- sorting.STABLE
- mergesort
Theorems
⊦ relation.equivalence sorting.PERM
⊦ transitive sorting.PERM
⊦ sorting.PERM = relation.EQC sorting.PERM_SINGLE_SWAP
⊦ sorting.PERM = relation.RTC sorting.PERM_SINGLE_SWAP
⊦ sorting.PERM = transitiveClosure sorting.PERM_SINGLE_SWAP
⊦ sorting.PERM ls (reverse ls)
⊦ ∀L. sorting.PERM L L
⊦ ∀l. sorting.PERM_SINGLE_SWAP l l
⊦ ∀R. sorting.SORTED R []
⊦ ∀n. sorting.SORTED (≤) (rich_list.COUNT_LIST n)
⊦ sorting.PERM (list.SET_TO_LIST (pred_set.count n))
(rich_list.COUNT_LIST n)
⊦ sorting.PERM_SINGLE_SWAP (x2 @ x3) (x3 @ x2)
⊦ ∀l R. sorting.PERM l (sorting.QSORT3 R l)
⊦ ∀R x. sorting.SORTED R (x :: [])
⊦ ∀R l. sorting.PERM l (mergesort.mergesort R l)
⊦ ∀R L. sorting.PERM L (sorting.QSORT R L)
⊦ ∀n k. sorting.SORTED (<) (list.GENLIST ((+) k) n)
⊦ pred_set.SUM_IMAGE f (pred_set.count n) = list.SUM (list.GENLIST f n)
⊦ sorting.SORTED R (x :: xs) ⇒ sorting.SORTED R xs
⊦ ∀ls.
list.ALL_DISTINCT ls ⇔
sorting.PERM ls (list.SET_TO_LIST (list.LIST_TO_SET ls))
⊦ ∀l1 l2. sorting.PERM l1 l2 ⇔ sorting.PERM l2 l1
⊦ ∀l1 l2. sorting.PERM_SINGLE_SWAP l1 l2 ⇔ sorting.PERM_SINGLE_SWAP l2 l1
⊦ ∀x y. x = y ⇒ sorting.PERM x y
⊦ ∀l1 l2. sorting.PERM (l1 @ l2) (l2 @ l1)
⊦ ∀R. transitive R ∧ relation.total R ⇒ sorting.SORTS sorting.QSORT R
⊦ ∀R. transitive R ∧ relation.total R ⇒ sorting.SORTS sorting.QSORT3 R
⊦ ∀R.
transitive R ∧ relation.total R ⇒ sorting.STABLE mergesort.mergesort R
⊦ ∀R. transitive R ∧ relation.total R ⇒ sorting.STABLE sorting.QSORT3 R
⊦ ∀x x1. sorting.SORTED x x1 ⇔ sorting.SORTED_tupled (x, x1)
⊦ ∀x x1. sorting.QSORT x x1 = sorting.QSORT_tupled (x, x1)
⊦ ∀x x1. sorting.QSORT3 x x1 = sorting.QSORT3_tupled (x, x1)
⊦ sorting.PERM_SINGLE_SWAP M N ⇒ sorting.PERM_SINGLE_SWAP (x :: M) (x :: N)
⊦ sorting.PERM_SINGLE_SWAP ((x1 @ x2) @ x3) ((x1 @ x3) @ x2)
⊦ ∀x y. sorting.PERM x y ⇔ sorting.PERM x = sorting.PERM y
⊦ ∀l1 l2.
sorting.PERM l1 l2 ⇒ (list.ALL_DISTINCT l1 ⇔ list.ALL_DISTINCT l2)
⊦ ∀l1 l2. sorting.PERM l1 l2 ⇒ length l1 = length l2
⊦ ∀l1 l2. sorting.PERM l1 l2 ⇒ list.LIST_TO_SET l1 = list.LIST_TO_SET l2
⊦ ∀l1 l2. sorting.PERM (l1 @ l2) = sorting.PERM (l2 @ l1)
⊦ ∀l1 l2. sorting.PERM l1 l2 ⇒ list.SUM l1 = list.SUM l2
⊦ ∀P l. sorting.PARTITION P l = sorting.PART P l [] []
⊦ ∀R l. mergesort.mergesort R l = mergesort.mergesortN R (length l) l
⊦ filter ((=) x) l = rich_list.REPLICATE (length (filter ((=) x) l)) x
⊦ ∀R n l. sorting.PERM (list.TAKE n l) (mergesort.mergesortN R n l)
⊦ ∀R l1 l2. sorting.PERM (l1 @ l2) (mergesort.merge R l1 l2)
⊦ ∀R l.
mergesort.mergesort_tail R l =
mergesort.mergesortN_tail ⊥ R (length l) l
⊦ ∀R x y. relation.total R ⇒ sorting.SORTED R (mergesort.sort2 R x y)
⊦ irreflexive R ∧ transitive R ⇒
∀ls. sorting.SORTED R ls ⇒ list.ALL_DISTINCT ls
⊦ ∀P l. sorting.PERM l (filter P l @ filter ((¬) ∘ P) l)
⊦ ∀%%genvar%%7817 l.
transitive %%genvar%%7817 ∧ relation.total %%genvar%%7817 ⇒
sorting.SORTED %%genvar%%7817 (mergesort.mergesort %%genvar%%7817 l)
⊦ ∀R L.
transitive R ∧ relation.total R ⇒ sorting.SORTED R (sorting.QSORT R L)
⊦ ∀R L.
transitive R ∧ relation.total R ⇒ sorting.SORTED R (sorting.QSORT3 R L)
⊦ ∀R x y. sorting.PERM (x :: y :: []) (mergesort.sort2 R x y)
⊦ ∀R ls.
transitive R ⇒ sorting.SORTED R ls ⇒ sorting.SORTED R (filter P ls)
⊦ ∀%%genvar%%9194 l.
transitive %%genvar%%9194 ∧ relation.total %%genvar%%9194 ⇒
mergesort.stable %%genvar%%9194 l
(mergesort.mergesort %%genvar%%9194 l)
⊦ sorting.PERM (x :: y :: l1) (y :: x :: l2) ⇔ sorting.PERM l1 l2
⊦ ∀x l2 l1. sorting.PERM (x :: l1) (x :: l2) ⇔ sorting.PERM l1 l2
⊦ ∀l1 l2 x. sorting.PERM l1 l2 ⇒ sorting.PERM (x :: l1) (x :: l2)
⊦ ∀A B C. sorting.PERM (A @ B) C ⇒ sorting.PERM (B @ A) C
⊦ ∀%%genvar%%648 y z.
sorting.PERM %%genvar%%648 y ∧ sorting.PERM y z ⇒
sorting.PERM %%genvar%%648 z
⊦ ∀f l1 l2. sorting.PERM l1 l2 ⇒ sorting.PERM (map f l1) (map f l2)
⊦ ∀P l1 l2. sorting.PERM l1 l2 ⇒ sorting.PERM (filter P l1) (filter P l2)
⊦ ∀R x y. mergesort.stable R (x :: y :: []) (mergesort.sort2 R x y)
⊦ ∀x x1 x2.
mergesort.mergesortN x x1 x2 = mergesort.mergesortN_tupled (x, x1, x2)
⊦ ∀%%genvar%%9316 L x.
bool.IN x (list.LIST_TO_SET (mergesort.mergesort %%genvar%%9316 L)) ⇔
bool.IN x (list.LIST_TO_SET L)
⊦ ∀R L x.
bool.IN x (list.LIST_TO_SET (sorting.QSORT R L)) ⇔
bool.IN x (list.LIST_TO_SET L)
⊦ ∀R L x.
bool.IN x (list.LIST_TO_SET (sorting.QSORT3 R L)) ⇔
bool.IN x (list.LIST_TO_SET L)
⊦ ∀x x1 x2. mergesort.merge x x1 x2 = mergesort.merge_tupled (x, x1, x2)
⊦ ∀M N.
transitiveClosure sorting.PERM_SINGLE_SWAP M N ⇒
transitiveClosure sorting.PERM_SINGLE_SWAP (x :: M) (x :: N)
⊦ ∀R x y z. relation.total R ⇒ sorting.SORTED R (mergesort.sort3 R x y z)
⊦ ∀R l.
relation.total R ∧ transitive R ⇒
mergesort.mergesort_tail R l = mergesort.mergesort R l
⊦ ∀L. (sorting.PERM L [] ⇔ L = []) ∧ (sorting.PERM [] L ⇔ L = [])
⊦ ∀R n l.
relation.total R ∧ transitive R ⇒
sorting.SORTED R (mergesort.mergesortN R n l)
⊦ ∀R ls P.
transitive R ∧ sorting.SORTED R ls ⇒ sorting.SORTED R (filter P ls)
⊦ (sorting.PERM (reverse l1) l2 ⇔ sorting.PERM l1 l2) ∧
(sorting.PERM l1 (reverse l2) ⇔ sorting.PERM l1 l2)
⊦ ∀x y l. sorting.PERM (x :: y :: l) = sorting.PERM (y :: x :: l)
⊦ ∀%%genvar%%4417 l1 l2.
sorting.PERM (l1 @ %%genvar%%4417 :: l2) =
sorting.PERM ((%%genvar%%4417 :: l1) @ l2)
⊦ ∀L1 L2. sorting.PERM L1 L2 ⇔ ∀x. filter ((=) x) L1 = filter ((=) x) L2
⊦ ∀l1 l2.
sorting.PERM l1 l2 ⇒
∀a. bool.IN a (list.LIST_TO_SET l1) ⇔ bool.IN a (list.LIST_TO_SET l2)
⊦ ∀l R. transitive R ⇒ sorting.SORTED R (filter (λx. R x hd ∧ R hd x) l)
⊦ ∀R l acc. mergesort.merge R l [] = l ∧ mergesort.merge R [] l = l
⊦ ∀x y. sorting.PERM ((x @ y) @ l1) ((y @ x) @ l2) ⇔ sorting.PERM l1 l2
⊦ ∀R f l.
transitive R ⇒
(sorting.SORTED R (map f l) ⇔
sorting.SORTED (relation.inv_image R f) l)
⊦ ∀R x y z. sorting.PERM (x :: y :: z :: []) (mergesort.sort3 R x y z)
⊦ ∀x l1 l2.
sorting.PERM l1 = sorting.PERM l2 ⇒
sorting.PERM (x :: l1) = sorting.PERM (x :: l2)
⊦ ∀l l1 l2.
sorting.PERM l1 = sorting.PERM l2 ⇒
sorting.PERM (l @ l1) = sorting.PERM (l @ l2)
⊦ ∀L1 L2.
sorting.PERM L1 L2 ⇔
∀x. length (filter ((=) x) L1) = length (filter ((=) x) L2)
⊦ ∀R n l.
relation.total R ∧ transitive R ⇒
mergesort.stable R (list.TAKE n l) (mergesort.mergesortN R n l)
⊦ ∀f R.
sorting.SORTS f R ⇔
∀l. sorting.PERM l (f R l) ∧ sorting.SORTED R (f R l)
⊦ ∀x x1 x2 x3.
mergesort.mergesortN_tail x x1 x2 x3 =
mergesort.mergesortN_tail_tupled (x, x1, x2, x3)
⊦ ∀R l1 l2 l3.
mergesort.stable R l1 l2 ∧ mergesort.stable R l2 l3 ⇒
mergesort.stable R l1 l3
⊦ ∀R l1 l2.
transitive R ∧ sorting.SORTED R l1 ⇒
mergesort.stable R (l1 @ l2) (mergesort.merge R l1 l2)
⊦ ∀x L M N. sorting.PERM L (M @ N) ⇒ sorting.PERM (x :: L) (M @ x :: N)
⊦ ∀%%genvar%%4726 l1' l2 l2'.
sorting.PERM %%genvar%%4726 l1' ⇒ sorting.PERM l2 l2' ⇒
(sorting.PERM %%genvar%%4726 l2 ⇔ sorting.PERM l1' l2')
⊦ ∀l r l1 l2.
sorting.PERM l r ⇒
(sorting.PERM (l @ l1) l2 ⇔ sorting.PERM (r @ l1) l2)
⊦ ∀%%genvar%%4749 l1 l1' l2.
sorting.PERM %%genvar%%4749 (l1 @ l2) ⇒ sorting.PERM l1' l1 ⇒
sorting.PERM %%genvar%%4749 (l1' @ l2)
⊦ ∀L1 L2 L3 L4.
sorting.PERM L1 L3 ∧ sorting.PERM L2 L4 ⇒
sorting.PERM (L1 @ L2) (L3 @ L4)
⊦ length (filter ((=) x) l1) = length (filter ((=) x) l2) ⇒
filter ((=) x) l1 = filter ((=) x) l2
⊦ pred_set.SUM_IMAGE (λm. pred_set.SUM_IMAGE (f m) (pred_set.count a))
(pred_set.count b) =
pred_set.SUM_IMAGE (λm. f (m div a) (m mod a)) (pred_set.count (a * b))
⊦ ∀L x.
sorting.SORTED (<) (x :: L) ⇔
sorting.SORTED (<) L ∧ ∀y. bool.IN y (list.LIST_TO_SET L) ⇒ x < y
⊦ ∀R ls.
sorting.SORTED R ls ⇔
∀n. suc n < length ls ⇒ R (list.EL n ls) (list.EL (suc n) ls)
⊦ ∀neg R x y.
mergesort.sort2_tail neg R x y =
if neg then reverse (mergesort.sort2 R x y) else mergesort.sort2 R x y
⊦ ∀P Q l. all (λx. P x ⇔ ¬Q x) l ⇒ sorting.PERM l (filter P l @ filter Q l)
⊦ (sorting.PERM L (x :: []) ⇔ L = x :: []) ∧
(sorting.PERM (x :: []) L ⇔ L = x :: [])
⊦ ∀l1 l2.
list.ALL_DISTINCT l1 ∧ list.ALL_DISTINCT l2 ∧
(∀a.
bool.IN a (list.LIST_TO_SET l1) ⇔ bool.IN a (list.LIST_TO_SET l2)) ⇒
sorting.PERM l1 l2
⊦ ∀R x y.
mergesort.sort2 R x y = if R x y then x :: y :: [] else y :: x :: []
⊦ ∀x x1 x2 x3 x4.
mergesort.merge_tail x x1 x2 x3 x4 =
mergesort.merge_tail_tupled (x, x1, x2, x3, x4)
⊦ ∀R l1 l2.
transitive R ∧ relation.total R ∧ sorting.SORTED R l1 ∧
sorting.SORTED R l2 ⇒ sorting.SORTED R (mergesort.merge R l1 l2)
⊦ ∀R.
relation.total R ∧ transitive R ∧ relation.antisymmetric R ⇒
∀l1 l2. sorting.QSORT R l1 = sorting.QSORT R l2 ⇔ sorting.PERM l1 l2
⊦ ∀y l1 x l2.
sorting.PERM l1 = sorting.PERM (x :: l2) ⇒
sorting.PERM (y :: l1) = sorting.PERM (x :: y :: l2)
⊦ ∀y l1 l2 l3.
sorting.PERM l1 = sorting.PERM (l2 @ l3) ⇒
sorting.PERM (y :: l1) = sorting.PERM (l2 @ y :: l3)
⊦ ∀y f l n.
sorting.SORTED (relation.inv_image (≤) f) l ∧
sorting.PERM (map f l) (rich_list.COUNT_LIST n) ⇒
map f l = rich_list.COUNT_LIST n
⊦ ∀L h.
sorting.PERM (h :: t) L ⇔ ∃M N. L = M @ h :: N ∧ sorting.PERM t (M @ N)
⊦ ∀l l1 x l2.
sorting.PERM l1 = sorting.PERM (x :: l2) ⇒
sorting.PERM (l @ l1) = sorting.PERM (x :: l @ l2)
⊦ ∀l l1 x l2.
sorting.PERM l1 = sorting.PERM (x :: l2) ⇒
sorting.PERM (l1 @ l) = sorting.PERM (x :: l2 @ l)
⊦ ∀%%genvar%%4718 l1' l2 l2'.
sorting.PERM %%genvar%%4718 = sorting.PERM l1' ⇒
sorting.PERM l2 = sorting.PERM l2' ⇒
(sorting.PERM %%genvar%%4718 l2 ⇔ sorting.PERM l1' l2')
⊦ ∀l1 l2 l3 l4.
sorting.PERM l1 = sorting.PERM (l2 @ l3) ⇒
sorting.PERM (l1 @ l4) = sorting.PERM (l2 @ l3 @ l4)
⊦ ∀l1 l2 l3 l4.
sorting.PERM l1 = sorting.PERM (l2 @ l3) ⇒
sorting.PERM (l4 @ l1) = sorting.PERM (l2 @ l4 @ l3)
⊦ ∀f l1 l2 e.
combin.ASSOC f ∧ combin.COMM f ⇒ sorting.PERM l1 l2 ⇒
list.FOLDR f e l1 = list.FOLDR f e l2
⊦ ∀neg R l1 l2 acc.
(neg ⇔ ⊥) ⇒
mergesort.merge_tail neg R l1 l2 acc =
reverse (mergesort.merge R l1 l2) @ acc
⊦ ∀R l1 l2 l3 l4.
mergesort.stable R l1 l2 ∧ mergesort.stable R l3 l4 ⇒
mergesort.stable R (l1 @ l3) (l2 @ l4)
⊦ ∀R.
transitive R ∧ relation.antisymmetric R ⇒
∀l1 l2.
sorting.SORTED R l1 ∧ sorting.SORTED R l2 ∧ sorting.PERM l1 l2 ⇒
l1 = l2
⊦ ∀R x y z.
relation.total R ∧ transitive R ⇒
mergesort.stable R (x :: y :: z :: []) (mergesort.sort3 R x y z)
⊦ ∀%%genvar%%4734 l1 l1' l2 l2'.
sorting.PERM l1 (%%genvar%%4734 @ l1') ⇒
sorting.PERM l2 (%%genvar%%4734 @ l2') ⇒
(sorting.PERM l1 l2 ⇔ sorting.PERM l1' l2')
⊦ ∀l1 l2.
sorting.PERM_SINGLE_SWAP l1 l2 ⇔
∃x1 x2 x3. l1 = (x1 @ x2) @ x3 ∧ l2 = (x1 @ x3) @ x2
⊦ ∀l1 l1' l2 l2'.
sorting.PERM l1 = sorting.PERM l1' ⇒
sorting.PERM l2 = sorting.PERM l2' ⇒
sorting.PERM (l1 @ l2) = sorting.PERM (l1' @ l2')
⊦ ∀R L x.
transitive R ⇒
(sorting.SORTED R (x :: L) ⇔
sorting.SORTED R L ∧ ∀y. bool.IN y (list.LIST_TO_SET L) ⇒ R x y)
⊦ ∀neg R x y z.
mergesort.sort3_tail neg R x y z =
if neg then reverse (mergesort.sort3 R x y z)
else mergesort.sort3 R x y z
⊦ ∀neg R x y.
mergesort.sort2_tail neg R x y =
if ¬(R x y ⇔ neg) then x :: y :: [] else y :: x :: []
⊦ ∀negate R n l.
relation.total R ∧ transitive R ⇒
mergesort.mergesortN_tail negate R n l =
if negate then reverse (mergesort.mergesortN R n l)
else mergesort.mergesortN R n l
⊦ ∀R.
transitive R ⇒
∀ls.
sorting.SORTED R ls ⇔
∀m n. m < n ∧ n < length ls ⇒ R (list.EL m ls) (list.EL n ls)
⊦ (∀m.
m < n ⇒
g m = pred_set.SUM_IMAGE (λx. f (x + k * m)) (pred_set.count k)) ⇒
pred_set.SUM_IMAGE f (pred_set.count (k * n)) =
pred_set.SUM_IMAGE g (pred_set.count n)
⊦ ∀R l1 l2.
mergesort.stable R l1 l2 ⇔
∀p. (∀x y. p x ∧ p y ⇒ R x y) ⇒ filter p l1 = filter p l2
⊦ ∀R L1 L2.
sorting.SORTED R (L1 @ L2) ⇔
sorting.SORTED R L1 ∧ sorting.SORTED R L2 ∧
(L1 = [] ∨ L2 = [] ∨ R (last L1) (head L2))
⊦ ∀f.
(∀x1 x2 x3. f ((x1 @ x2) @ x3) = f ((x1 @ x3) @ x2)) ⇒
∀x y. sorting.PERM x y ⇒ f x = f y
⊦ ∀P.
(∀x1 x2 x3. P ((x1 @ x2) @ x3) ⇒ P ((x1 @ x3) @ x2)) ⇒
∀x y. P x ∧ sorting.PERM x y ⇒ P y
⊦ (∀l l1 l2. sorting.PERM (l @ l1) (l @ l2) ⇔ sorting.PERM l1 l2) ∧
∀l l1 l2. sorting.PERM (l1 @ l) (l2 @ l) ⇔ sorting.PERM l1 l2
⊦ ∀R R' ls.
sorting.SORTED R ls ∧
(∀x y.
bool.IN x (list.LIST_TO_SET ls) ∧ bool.IN y (list.LIST_TO_SET ls) ∧
R x y ⇒ R' x y) ⇒ sorting.SORTED R' ls
⊦ ∀P L l1 l2 p q.
(p, q) = sorting.PART P L l1 l2 ⇒
length L + length l1 + length l2 = length p + length q
⊦ ∀l h.
sorting.PERM l
((filter (λx. R x h ∧ ¬R h x) l @ filter (λx. R x h ∧ R h x) l) @
filter (λx. ¬R x h) l)
⊦ ∀P L a1 a2 l1 l2.
(a1, a2) = sorting.PART P L l1 l2 ⇒
∀x.
bool.IN x (list.LIST_TO_SET (L @ l1 @ l2)) ⇔
bool.IN x (list.LIST_TO_SET (a1 @ a2))
⊦ ∀sort r.
sorting.STABLE sort r ⇔
sorting.SORTS sort r ∧
∀p. (∀x y. p x ∧ p y ⇒ r x y) ⇒ ∀l. filter p l = filter p (sort r l)
⊦ ∀tl hd.
sorting.PART3 R hd tl =
(filter (λx. R x hd ∧ ¬R hd x) tl, filter (λx. R x hd ∧ R hd x) tl,
filter (λx. ¬R x hd) tl)
⊦ ∀f Q.
(∀x1 x2 x3. Q (f ((x1 @ x2) @ x3)) (f ((x1 @ x3) @ x2))) ∧
transitive Q ⇒ ∀x y. sorting.PERM x y ⇒ Q (f x) (f y)
⊦ ∀x a a' b b' c c'.
(sorting.PERM a a' ∧ sorting.PERM b b' ∧ sorting.PERM c c') ∧
sorting.PERM x ((a @ b) @ c) ⇒ sorting.PERM x ((a' @ b') @ c')
⊦ ∀R L1 L2.
transitive R ∧ sorting.SORTED R L1 ∧ sorting.SORTED R L2 ∧
(∀x y.
bool.IN x (list.LIST_TO_SET L1) ∧ bool.IN y (list.LIST_TO_SET L2) ⇒
R x y) ⇒ sorting.SORTED R (L1 @ L2)
⊦ (∀ord. sorting.QSORT ord [] = []) ∧
∀t ord h.
sorting.QSORT ord (h :: t) =
bool.LET
(pair.UNCURRY
(λl1 l2. (sorting.QSORT ord l1 @ h :: []) @ sorting.QSORT ord l2))
(sorting.PARTITION (λy. ord y h) t)
⊦ (∀R. sorting.QSORT3 R [] = []) ∧
∀tl hd R.
sorting.QSORT3 R (hd :: tl) =
bool.LET
(pair.UNCURRY
(λlo.
pair.UNCURRY
(λeq hi.
(sorting.QSORT3 R lo @ hd :: eq) @ sorting.QSORT3 R hi)))
(sorting.PART3 R hd tl)
⊦ ∀P R l1 l2.
transitive R ∧ (∀x y. P x ∧ P y ⇒ R x y) ∧ sorting.SORTED R l1 ⇒
filter P (mergesort.merge R l1 l2) = filter P (l1 @ l2)
⊦ ∀neg R l1 l2 acc.
(neg ⇔ ⊤) ∧ transitive R ∧ sorting.SORTED R (reverse l1) ∧
sorting.SORTED R (reverse l2) ⇒
mergesort.merge_tail neg R l1 l2 acc =
mergesort.merge R (reverse l1) (reverse l2) @ acc
⊦ (∀R. sorting.SORTED R [] ⇔ ⊤) ∧ (∀x R. sorting.SORTED R (x :: []) ⇔ ⊤) ∧
∀y x rst R.
sorting.SORTED R (x :: y :: rst) ⇔ R x y ∧ sorting.SORTED R (y :: rst)
⊦ ∀P L l1 l2 p q.
(p, q) = sorting.PART P L l1 l2 ⇒
length p ≤ length L + length l1 + length l2 ∧
length q ≤ length L + length l1 + length l2
⊦ ∀P.
(∀R. P R []) ∧ (∀R x. P R (x :: [])) ∧
(∀R x y rst. P R (y :: rst) ⇒ P R (x :: y :: rst)) ⇒ ∀R ls. P R ls
⊦ ∀R.
transitive R ∧ relation.total R ⇒
∀l e.
sorting.QSORT3 R l =
(sorting.QSORT3 R (filter (λx. R x e ∧ ¬R e x) l) @
filter (λx. R x e ∧ R e x) l) @
sorting.QSORT3 R (filter (λx. ¬R x e) l)
⊦ (∀P l1 l2. sorting.PART P [] l1 l2 = (l1, l2)) ∧
∀P h rst l1 l2.
sorting.PART P (h :: rst) l1 l2 =
if P h then sorting.PART P rst (h :: l1) l2
else sorting.PART P rst l1 (h :: l2)
⊦ ∀f.
(∀x1 x2 x3.
∃x1' x2' x3'.
f ((x1 @ x2) @ x3) = (x1' @ x2') @ x3' ∧
f ((x1 @ x3) @ x2) = (x1' @ x3') @ x2') ⇒
∀x y. sorting.PERM x y ⇒ sorting.PERM (f x) (f y)
⊦ sorting.SORTED_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧ ∀x rst y R. R' (R, y :: rst) (R, x :: y :: rst))
(λSORTED_tupled a.
pair.pair_CASE a
(λR v1.
list.list_CASE v1 (id ⊤)
(λx v3.
list.list_CASE v3 (id ⊤)
(λy rst. id (R x y ∧ SORTED_tupled (R, y :: rst))))))
⊦ ∀P L A B l1 l2.
(A, B) = sorting.PART P L l1 l2 ∧
(∀x. bool.IN x (list.LIST_TO_SET l1) ⇒ P x) ∧
(∀x. bool.IN x (list.LIST_TO_SET l2) ⇒ ¬P x) ⇒
(∀z. bool.IN z (list.LIST_TO_SET A) ⇒ P z) ∧
∀z. bool.IN z (list.LIST_TO_SET B) ⇒ ¬P z
⊦ ∀P.
(∀R. P R []) ∧
(∀ord h t.
(∀l1 l2. (l1, l2) = sorting.PARTITION (λy. ord y h) t ⇒ P ord l2) ∧
(∀l1 l2. (l1, l2) = sorting.PARTITION (λy. ord y h) t ⇒ P ord l1) ⇒
P ord (h :: t)) ⇒ ∀R ls. P R ls
⊦ ∀P.
(∀R. P R []) ∧
(∀R hd tl.
(∀lo eq hi. (lo, eq, hi) = sorting.PART3 R hd tl ⇒ P R hi) ∧
(∀lo eq hi. (lo, eq, hi) = sorting.PART3 R hd tl ⇒ P R lo) ⇒
P R (hd :: tl)) ⇒ ∀R ls. P R ls
⊦ (∀R h. sorting.PART3 R h [] = ([], [], [])) ∧
∀R h hd tl.
sorting.PART3 R h (hd :: tl) =
if R h hd ∧ R hd h then
pair.## id (pair.## ((::) hd) id) (sorting.PART3 R h tl)
else if R hd h then
pair.## ((::) hd) (pair.## id id) (sorting.PART3 R h tl)
else pair.## id (pair.## id ((::) hd)) (sorting.PART3 R h tl)
⊦ ∀P.
P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x :: l1) (x :: l2)) ∧
(∀x y l1 l2. P l1 l2 ⇒ P (x :: y :: l1) (y :: x :: l2)) ∧
(∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒
∀l1 l2. sorting.PERM l1 l2 ⇒ P l1 l2
⊦ ∀R x y z.
mergesort.sort3 R x y z =
if R x y then
if R y z then x :: y :: z :: []
else if R x z then x :: z :: y :: []
else z :: x :: y :: []
else if R y z then
if R x z then y :: x :: z :: [] else y :: z :: x :: []
else z :: y :: x :: []
⊦ (∀R. mergesort.merge R [] [] = []) ∧
(∀v9 v8 R. mergesort.merge R (v8 :: v9) [] = v8 :: v9) ∧
(∀v5 v4 R. mergesort.merge R [] (v4 :: v5) = v4 :: v5) ∧
∀y x l2 l1 R.
mergesort.merge R (x :: l1) (y :: l2) =
if R x y then x :: mergesort.merge R l1 (y :: l2)
else y :: mergesort.merge R (x :: l1) l2
⊦ ∀P.
(∀R. P R [] []) ∧ (∀R v8 v9. P R (v8 :: v9) []) ∧
(∀R v4 v5. P R [] (v4 :: v5)) ∧
(∀R x l1 y l2.
(¬R x y ⇒ P R (x :: l1) l2) ∧ (R x y ⇒ P R l1 (y :: l2)) ⇒
P R (x :: l1) (y :: l2)) ⇒ ∀R l1 l2. P R l1 l2
⊦ ∀P.
P [] [] ∧
(∀x l1 l2. sorting.PERM l1 l2 ∧ P l1 l2 ⇒ P (x :: l1) (x :: l2)) ∧
(∀x y l1 l2.
sorting.PERM l1 l2 ∧ P l1 l2 ⇒ P (x :: y :: l1) (y :: x :: l2)) ∧
(∀l1 l2 l3.
sorting.PERM l1 l2 ∧ P l1 l2 ∧ sorting.PERM l2 l3 ∧ P l2 l3 ⇒
P l1 l3) ⇒ ∀l1 l2. sorting.PERM l1 l2 ⇒ P l1 l2
⊦ ∀neg R x y z.
mergesort.sort3_tail neg R x y z =
if ¬(R x y ⇔ neg) then
if ¬(R y z ⇔ neg) then x :: y :: z :: []
else if ¬(R x z ⇔ neg) then x :: z :: y :: []
else z :: x :: y :: []
else if ¬(R y z ⇔ neg) then
if ¬(R x z ⇔ neg) then y :: x :: z :: [] else y :: z :: x :: []
else z :: y :: x :: []
⊦ sorting.QSORT_tupled =
relation.WFREC
(select R.
wellFounded R ∧
(∀t h ord l1 l2.
(l1, l2) = sorting.PARTITION (λy. ord y h) t ⇒
R (ord, l2) (ord, h :: t)) ∧
∀t h ord l1 l2.
(l1, l2) = sorting.PARTITION (λy. ord y h) t ⇒
R (ord, l1) (ord, h :: t))
(λQSORT_tupled a.
pair.pair_CASE a
(λord v1.
list.list_CASE v1 (id [])
(λh t.
id
(bool.LET
(pair.UNCURRY
(λl1 l2.
(QSORT_tupled (ord, l1) @ h :: []) @
QSORT_tupled (ord, l2)))
(sorting.PARTITION (λy. ord y h) t)))))
⊦ sorting.QSORT3_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧
(∀tl hd R lo eq hi.
(lo, eq, hi) = sorting.PART3 R hd tl ⇒
R' (R, hi) (R, hd :: tl)) ∧
∀tl hd R lo eq hi.
(lo, eq, hi) = sorting.PART3 R hd tl ⇒ R' (R, lo) (R, hd :: tl))
(λQSORT3_tupled a.
pair.pair_CASE a
(λR v1.
list.list_CASE v1 (id [])
(λhd tl.
id
(bool.LET
(pair.UNCURRY
(λlo.
pair.UNCURRY
(λeq hi.
(QSORT3_tupled (R, lo) @ hd :: eq) @
QSORT3_tupled (R, hi))))
(sorting.PART3 R hd tl)))))
⊦ (∀negate acc R. mergesort.merge_tail negate R [] [] acc = acc) ∧
(∀v13 v12 negate acc R.
mergesort.merge_tail negate R (v12 :: v13) [] acc =
list.REV (v12 :: v13) acc) ∧
(∀v9 v8 negate acc R.
mergesort.merge_tail negate R [] (v8 :: v9) acc =
list.REV (v8 :: v9) acc) ∧
∀y x negate l2 l1 acc R.
mergesort.merge_tail negate R (x :: l1) (y :: l2) acc =
if ¬(R x y ⇔ negate) then
mergesort.merge_tail negate R l1 (y :: l2) (x :: acc)
else mergesort.merge_tail negate R (x :: l1) l2 (y :: acc)
⊦ mergesort.merge_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧
(∀l2 l1 y x R. ¬R x y ⇒ R' (R, x :: l1, l2) (R, x :: l1, y :: l2)) ∧
∀l2 l1 y x R. R x y ⇒ R' (R, l1, y :: l2) (R, x :: l1, y :: l2))
(λmerge_tupled a.
pair.pair_CASE a
(λR v1.
pair.pair_CASE v1
(λv2 v3.
list.list_CASE v3
(list.list_CASE v2 (id []) (λv10 v11. id (v10 :: v11)))
(λy l2.
list.list_CASE v2 (id (y :: l2))
(λx l1.
id
(if R x y then
x :: merge_tupled (R, l1, y :: l2)
else y :: merge_tupled (R, x :: l1, l2)))))))
⊦ ∀P.
(∀negate R acc. P negate R [] [] acc) ∧
(∀negate R v12 v13 acc. P negate R (v12 :: v13) [] acc) ∧
(∀negate R v8 v9 acc. P negate R [] (v8 :: v9) acc) ∧
(∀negate R x l1 y l2 acc.
(¬¬(R x y ⇔ negate) ⇒ P negate R (x :: l1) l2 (y :: acc)) ∧
(¬(R x y ⇔ negate) ⇒ P negate R l1 (y :: l2) (x :: acc)) ⇒
P negate R (x :: l1) (y :: l2) acc) ⇒
∀neg R l1 l2 acc. P neg R l1 l2 acc
⊦ mergesort.merge_tail_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧
(∀acc l2 l1 negate y x R.
¬¬(R x y ⇔ negate) ⇒
R' (negate, R, x :: l1, l2, y :: acc)
(negate, R, x :: l1, y :: l2, acc)) ∧
∀acc l2 l1 negate y x R.
¬(R x y ⇔ negate) ⇒
R' (negate, R, l1, y :: l2, x :: acc)
(negate, R, x :: l1, y :: l2, acc))
(λmerge_tail_tupled a.
pair.pair_CASE a
(λnegate v1.
pair.pair_CASE v1
(λR v3.
pair.pair_CASE v3
(λv4 v5.
pair.pair_CASE v5
(λv6 acc.
list.list_CASE v6
(list.list_CASE v4 (id acc)
(λv14 v15. id (list.REV (v14 :: v15) acc)))
(λy l2.
list.list_CASE v4
(id (list.REV (y :: l2) acc))
(λx l1.
id
(if ¬(R x y ⇔ negate) then
merge_tail_tupled
(negate, R, l1, y :: l2,
x :: acc)
else
merge_tail_tupled
(negate, R, x :: l1, l2,
y :: acc)))))))))
⊦ mergesort.mergesortN_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧
(∀l R v4 len1.
¬(v4 = 0) ∧ ¬(v4 = 1) ∧ ¬(v4 = arithmetic.BIT2 0) ∧ ¬(v4 = 3) ∧
len1 = arithmetic.DIV2 v4 ⇒
R' (R, arithmetic.DIV2 v4, l) (R, v4, l)) ∧
∀l R v4 len1.
¬(v4 = 0) ∧ ¬(v4 = 1) ∧ ¬(v4 = arithmetic.BIT2 0) ∧ ¬(v4 = 3) ∧
len1 = arithmetic.DIV2 v4 ⇒
R' (R, arithmetic.- v4 len1, list.DROP len1 l) (R, v4, l))
(λmergesortN_tupled a.
pair.pair_CASE a
(λR v1.
pair.pair_CASE v1
(λv2 l.
bool.literal_case
(λn.
if n = 0 then id []
else if n = 1 then
list.list_CASE l (id []) (λx l'. id (x :: []))
else if n = arithmetic.BIT2 0 then
list.list_CASE l (id [])
(λx' v17.
list.list_CASE v17 (id (x' :: []))
(λy l''. id (mergesort.sort2 R x' y)))
else if n = 3 then
list.list_CASE l (id [])
(λx'' v25.
list.list_CASE v25 (id (x'' :: []))
(λy' v29.
list.list_CASE v29
(id (mergesort.sort2 R x'' y'))
(λz l'''.
id (mergesort.sort3 R x'' y' z))))
else
id
(bool.LET
(λlen1.
mergesort.merge R
(mergesortN_tupled
(R, arithmetic.DIV2 n, l))
(mergesortN_tupled
(R, arithmetic.- n len1,
list.DROP len1 l)))
(arithmetic.DIV2 n))) v2)))
⊦ ∀P.
(∀R l. P R 0 l) ∧ (∀R x l. P R 1 (x :: l)) ∧ (∀R. P R 1 []) ∧
(∀R x y l. P R (arithmetic.BIT2 0) (x :: y :: l)) ∧
(∀R x. P R (arithmetic.BIT2 0) (x :: [])) ∧
(∀R. P R (arithmetic.BIT2 0) []) ∧
(∀R x y z l. P R 3 (x :: y :: z :: l)) ∧
(∀R x y. P R 3 (x :: y :: [])) ∧ (∀R x. P R 3 (x :: [])) ∧
(∀R. P R 3 []) ∧
(∀R v4 l.
(∀len1.
¬(v4 = 0) ∧ ¬(v4 = 1) ∧ ¬(v4 = arithmetic.BIT2 0) ∧ ¬(v4 = 3) ∧
len1 = arithmetic.DIV2 v4 ⇒ P R (arithmetic.DIV2 v4) l) ∧
(∀len1.
¬(v4 = 0) ∧ ¬(v4 = 1) ∧ ¬(v4 = arithmetic.BIT2 0) ∧ ¬(v4 = 3) ∧
len1 = arithmetic.DIV2 v4 ⇒
P R (arithmetic.- v4 len1) (list.DROP len1 l)) ⇒ P R v4 l) ⇒
∀v v1 v2. P v v1 v2
⊦ (∀l R. mergesort.mergesortN R 0 l = []) ∧
(∀x l R. mergesort.mergesortN R 1 (x :: l) = x :: []) ∧
(∀R. mergesort.mergesortN R 1 [] = []) ∧
(∀y x l R.
mergesort.mergesortN R (arithmetic.BIT2 0) (x :: y :: l) =
mergesort.sort2 R x y) ∧
(∀x R. mergesort.mergesortN R (arithmetic.BIT2 0) (x :: []) = x :: []) ∧
(∀R. mergesort.mergesortN R (arithmetic.BIT2 0) [] = []) ∧
(∀z y x l R.
mergesort.mergesortN R 3 (x :: y :: z :: l) =
mergesort.sort3 R x y z) ∧
(∀y x R.
mergesort.mergesortN R 3 (x :: y :: []) = mergesort.sort2 R x y) ∧
(∀x R. mergesort.mergesortN R 3 (x :: []) = x :: []) ∧
(∀R. mergesort.mergesortN R 3 [] = []) ∧
∀v4 l R.
mergesort.mergesortN R v4 l =
if v4 = 0 then []
else if v4 = 1 then list.list_CASE l [] (λx l'. x :: [])
else if v4 = arithmetic.BIT2 0 then
list.list_CASE l []
(λx' v17.
list.list_CASE v17 (x' :: []) (λy l''. mergesort.sort2 R x' y))
else if v4 = 3 then
list.list_CASE l []
(λx'' v25.
list.list_CASE v25 (x'' :: [])
(λy' v29.
list.list_CASE v29 (mergesort.sort2 R x'' y')
(λz l'''. mergesort.sort3 R x'' y' z)))
else
bool.LET
(λlen1.
mergesort.merge R
(mergesort.mergesortN R (arithmetic.DIV2 v4) l)
(mergesort.mergesortN R (arithmetic.- v4 len1)
(list.DROP len1 l))) (arithmetic.DIV2 v4)
⊦ mergesort.mergesortN_tail_tupled =
relation.WFREC
(select R'.
wellFounded R' ∧
(∀l R negate v6 len1 neg.
¬(v6 = 0) ∧ ¬(v6 = 1) ∧ ¬(v6 = arithmetic.BIT2 0) ∧ ¬(v6 = 3) ∧
len1 = arithmetic.DIV2 v6 ∧ (neg ⇔ ¬negate) ⇒
R' (neg, R, arithmetic.DIV2 v6, l) (negate, R, v6, l)) ∧
∀l R negate v6 len1 neg.
¬(v6 = 0) ∧ ¬(v6 = 1) ∧ ¬(v6 = arithmetic.BIT2 0) ∧ ¬(v6 = 3) ∧
len1 = arithmetic.DIV2 v6 ∧ (neg ⇔ ¬negate) ⇒
R' (neg, R, arithmetic.- v6 len1, list.DROP len1 l)
(negate, R, v6, l))
(λmergesortN_tail_tupled a.
pair.pair_CASE a
(λnegate v1.
pair.pair_CASE v1
(λR v3.
pair.pair_CASE v3
(λv4 l.
bool.literal_case
(λn.
if n = 0 then id []
else if n = 1 then
list.list_CASE l (id []) (λx l'. id (x :: []))
else if n = arithmetic.BIT2 0 then
list.list_CASE l (id [])
(λx' v19.
list.list_CASE v19 (id (x' :: []))
(λy l''.
id
(mergesort.sort2_tail negate R x'
y)))
else if n = 3 then
list.list_CASE l (id [])
(λx'' v27.
list.list_CASE v27 (id (x'' :: []))
(λy' v31.
list.list_CASE v31
(id
(mergesort.sort2_tail negate R
x'' y'))
(λz l'''.
id
(mergesort.sort3_tail negate
R x'' y' z))))
else
id
(bool.LET
(λlen1.
bool.LET
(λneg.
mergesort.merge_tail neg R
(mergesortN_tail_tupled
(neg, R, arithmetic.DIV2 n,
l))
(mergesortN_tail_tupled
(neg, R,
arithmetic.- n len1,
list.DROP len1 l)) [])
(¬negate)) (arithmetic.DIV2 n)))
v4))))
⊦ ∀P.
(∀negate R l. P negate R 0 l) ∧
(∀negate R x l. P negate R 1 (x :: l)) ∧ (∀negate R. P negate R 1 []) ∧
(∀negate R x y l. P negate R (arithmetic.BIT2 0) (x :: y :: l)) ∧
(∀negate R x. P negate R (arithmetic.BIT2 0) (x :: [])) ∧
(∀negate R. P negate R (arithmetic.BIT2 0) []) ∧
(∀negate R x y z l. P negate R 3 (x :: y :: z :: l)) ∧
(∀negate R x y. P negate R 3 (x :: y :: [])) ∧
(∀negate R x. P negate R 3 (x :: [])) ∧ (∀negate R. P negate R 3 []) ∧
(∀negate R v6 l.
(∀len1 neg.
¬(v6 = 0) ∧ ¬(v6 = 1) ∧ ¬(v6 = arithmetic.BIT2 0) ∧ ¬(v6 = 3) ∧
len1 = arithmetic.DIV2 v6 ∧ (neg ⇔ ¬negate) ⇒
P neg R (arithmetic.DIV2 v6) l) ∧
(∀len1 neg.
¬(v6 = 0) ∧ ¬(v6 = 1) ∧ ¬(v6 = arithmetic.BIT2 0) ∧ ¬(v6 = 3) ∧
len1 = arithmetic.DIV2 v6 ∧ (neg ⇔ ¬negate) ⇒
P neg R (arithmetic.- v6 len1) (list.DROP len1 l)) ⇒
P negate R v6 l) ⇒ ∀negate R n l. P negate R n l
⊦ (∀negate l R. mergesort.mergesortN_tail negate R 0 l = []) ∧
(∀x negate l R.
mergesort.mergesortN_tail negate R 1 (x :: l) = x :: []) ∧
(∀negate R. mergesort.mergesortN_tail negate R 1 [] = []) ∧
(∀y x negate l R.
mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) (x :: y :: l) =
mergesort.sort2_tail negate R x y) ∧
(∀x negate R.
mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) (x :: []) =
x :: []) ∧
(∀negate R.
mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) [] = []) ∧
(∀z y x negate l R.
mergesort.mergesortN_tail negate R 3 (x :: y :: z :: l) =
mergesort.sort3_tail negate R x y z) ∧
(∀y x negate R.
mergesort.mergesortN_tail negate R 3 (x :: y :: []) =
mergesort.sort2_tail negate R x y) ∧
(∀x negate R. mergesort.mergesortN_tail negate R 3 (x :: []) = x :: []) ∧
(∀negate R. mergesort.mergesortN_tail negate R 3 [] = []) ∧
∀v6 negate l R.
mergesort.mergesortN_tail negate R v6 l =
if v6 = 0 then []
else if v6 = 1 then list.list_CASE l [] (λx l'. x :: [])
else if v6 = arithmetic.BIT2 0 then
list.list_CASE l []
(λx' v19.
list.list_CASE v19 (x' :: [])
(λy l''. mergesort.sort2_tail negate R x' y))
else if v6 = 3 then
list.list_CASE l []
(λx'' v27.
list.list_CASE v27 (x'' :: [])
(λy' v31.
list.list_CASE v31 (mergesort.sort2_tail negate R x'' y')
(λz l'''. mergesort.sort3_tail negate R x'' y' z)))
else
bool.LET
(λlen1.
bool.LET
(λneg.
mergesort.merge_tail neg R
(mergesort.mergesortN_tail neg R (arithmetic.DIV2 v6) l)
(mergesort.mergesortN_tail neg R (arithmetic.- v6 len1)
(list.DROP len1 l)) []) (¬negate))
(arithmetic.DIV2 v6)
External Type Operators
- →
- bool
- ind
- Data
- List
- list
- Pair
- ×
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- any
- filter
- head
- last
- length
- map
- reverse
- Pair
- ,
- fst
- snd
- Bool
- Function
- flip
- id
- ∘
- Combinator
- Combinator.s
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.BIT2
- arithmetic.DIV2
- bool
- bool.literal_case
- bool.IN
- bool.LET
- combin
- combin.ASSOC
- combin.COMM
- list
- list.list_CASE
- list.list_size
- list.ALL_DISTINCT
- list.DROP
- list.EL
- list.FOLDR
- list.GENLIST
- list.GENLIST_AUX
- list.LIST_TO_SET
- list.REV
- list.SET_TO_LIST
- list.SNOC
- list.SUM
- list.TAKE
- marker
- marker.:-
- marker.Abbrev
- numeral
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- pair
- pair.##
- pair.pair_CASE
- pair.UNCURRY
- pred_set
- pred_set.count
- pred_set.DELETE
- pred_set.EMPTY
- pred_set.FINITE
- pred_set.INSERT
- pred_set.SUM_IMAGE
- pred_set.UNION
- prim_rec
- prim_rec.measure
- prim_rec.PRE
- relation
- relation.antisymmetric
- relation.equivalence
- relation.inv_image
- relation.total
- relation.EQC
- relation.RC
- relation.RESTRICT
- relation.RTC
- relation.SC
- relation.WFREC
- rich_list
- rich_list.COUNT_LIST
- rich_list.REPLICATE
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- mod
- odd
- suc
- zero
- Natural
- Relation
- irreflexive
- transitive
- transitiveClosure
- wellFounded
Assumptions
⊦ ⊤
⊦ transitive (<)
⊦ wellFounded (<)
⊦ prim_rec.measure = relation.inv_image (<)
⊦ pred_set.count 0 = pred_set.EMPTY
⊦ ∀x. x = x
⊦ ∀t. ⊥ ⇒ t
⊦ ∀n. pred_set.FINITE (pred_set.count n)
⊦ ∀n. 0 ≤ n
⊦ ∀l. pred_set.FINITE (list.LIST_TO_SET l)
⊦ ∀m. wellFounded (prim_rec.measure m)
⊦ ∀R. relation.equivalence (relation.EQC R)
⊦ list.TAKE 0 l = []
⊦ ¬¬p ⇒ p
⊦ ∀x. ¬bool.IN x pred_set.EMPTY
⊦ ∀x. id x = x
⊦ ∀t. t ∨ ¬t
⊦ ∀x. marker.Abbrev x ⇔ x
⊦ ∀n. ¬(n < 0)
⊦ ∀n. 0 < suc n
⊦ (¬) = λt. t ⇒ ⊥
⊦ (∃) = λP. P ((select) P)
⊦ ∀a. ∃x. x = a
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λP. P = λx. ⊤
⊦ ¬(p ⇒ q) ⇒ p
⊦ ∀x. x = x ⇔ ⊤
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀c. arithmetic.- c c = 0
⊦ ∀n. n * 0 = 0
⊦ ∀m. m + 0 = m
⊦ ∀l. reverse (reverse l) = l
⊦ ∀l. l @ [] = l
⊦ flip = λf x y. f y x
⊦ ¬(p ⇒ q) ⇒ ¬q
⊦ ¬(p ∨ q) ⇒ ¬p
⊦ ¬(p ∨ q) ⇒ ¬q
⊦ ∀A. A ⇒ ¬A ⇒ ⊥
⊦ ∀t. ¬t ⇒ t ⇒ ⊥
⊦ ∀t. (t ⇒ ⊥) ⇒ ¬t
⊦ ∀n. rich_list.COUNT_LIST n = list.GENLIST id n
⊦ ∀l. length (reverse l) = length l
⊦ ∀l. list.TAKE (length l) l = l
⊦ ∀s. pred_set.FINITE s ⇒ list.ALL_DISTINCT (list.SET_TO_LIST s)
⊦ Combinator.s = λf g x. f x (g x)
⊦ ∀lab argument. marker.:- lab argument ⇔ argument
⊦ ∀m n. m ≤ m + n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∀) (pair.UNCURRY f) ⇔ (∀) ((∀) ∘ f)
⊦ ∀t. t ⇒ ⊥ ⇔ t ⇔ ⊥
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀n. arithmetic.DIV2 n = n div arithmetic.BIT2 0
⊦ ∀n. suc n = 1 + n
⊦ ∀x. (fst x, snd x) = x
⊦ ∀R. relation.EQC R = relation.RC (transitiveClosure (relation.SC R))
⊦ ∀R. transitive R ⇒ transitiveClosure R = R
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀h t. head (h :: t) = h
⊦ ∀a1 a0. ¬([] = a0 :: a1)
⊦ ∀a1 a0. ¬(a0 :: a1 = [])
⊦ ∀f x. bool.literal_case f x = f x
⊦ ∀f x. bool.LET f x = f x
⊦ ∀P x. P x ⇒ P ((select) P)
⊦ ¬(⊤ ⇔ ⊥) ∧ ¬(⊥ ⇔ ⊤)
⊦ f ∘ (λx. g x) = λx. f (g x)
⊦ flip (λx. f x) y = λx. f x y
⊦ pair.pair_CASE (x, y) f = f x y
⊦ ∀x. ∃q r. x = (q, r)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1
⊦ ∀A B. A ∨ B ⇔ B ∨ A
⊦ ∀m n. m * n = n * m
⊦ ∀m n. m + n = n + m
⊦ ∀R f. transitive R ⇒ transitive (relation.inv_image R f)
⊦ ∀R. irreflexive R ⇔ ∀x. ¬R x x
⊦ ∀R f. wellFounded R ⇒ wellFounded (relation.inv_image R f)
⊦ P (bool.LET f v) = bool.LET (P ∘ f) v
⊦ bool.LET f v x = bool.LET (flip f x) v
⊦ f ∘ pair.UNCURRY g = pair.UNCURRY ((∘) f ∘ g)
⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥
⊦ Combinator.s f (λx. g x) = λx. f x (g x)
⊦ ∀f g. f ∘ g = λx. f (g x)
⊦ ∀m n. m < n ⇔ suc m ≤ n
⊦ ∀m n. m < n ⇒ m < suc n
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. bool.IN m (pred_set.count n) ⇔ m < n
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀L1 L2. list.REV L1 L2 = reverse L1 @ L2
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ flip (pair.UNCURRY f) x = pair.UNCURRY (flip (flip ∘ f) x)
⊦ ∀P. ¬(∀x. P x) ⇔ ∃y. ¬P y
⊦ ∀P. ¬(∃x. P x) ⇔ ∀y. ¬P y
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀x l. list.SNOC x l = l @ x :: []
⊦ ∀m n. ¬(m ≤ n) ⇔ suc n ≤ m
⊦ ∀m n. bool.IN m (list.LIST_TO_SET (rich_list.COUNT_LIST n)) ⇔ m < n
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ ∀n m. suc n ≤ suc m ⇔ n ≤ m
⊦ ∀m n. arithmetic.- m n = 0 ⇔ m ≤ n
⊦ ∀x l. list.SUM (list.SNOC x l) = list.SUM l + x
⊦ ∀n. 0 < n ⇒ ∀k. k div n ≤ k
⊦ ∀l P. filter P (reverse l) = reverse (filter P l)
⊦ pred_set.FINITE s ⇒
pred_set.SUM_IMAGE f s = list.SUM (map f (list.SET_TO_LIST s))
⊦ ∀c l. all (λx. c) l ⇔ l = [] ∨ c
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀f. id ∘ f = f ∧ f ∘ id = f
⊦ ∀R x y. R x y ⇒ transitiveClosure R x y
⊦ ∀f x y. flip f x y = f y x
⊦ ∀m n. m * suc n = m + m * n
⊦ ∀l x.
bool.IN x (list.LIST_TO_SET (reverse l)) ⇔
bool.IN x (list.LIST_TO_SET l)
⊦ ∀l1 l2. length (l1 @ l2) = length l1 + length l2
⊦ ∀l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1
⊦ ∀l1 l2.
list.LIST_TO_SET (l1 @ l2) =
pred_set.UNION (list.LIST_TO_SET l1) (list.LIST_TO_SET l2)
⊦ ∀l1 l2. list.SUM (l1 @ l2) = list.SUM l1 + list.SUM l2
⊦ ∀P l. ¬all P l ⇔ any ((¬) ∘ P) l
⊦ ∀R f. relation.inv_image R f = λx y. R (f x) (f y)
⊦ list.GENLIST f (suc n) = f 0 :: list.GENLIST (f ∘ suc) n
⊦ ∀l. l = [] ∨ ∃h t. l = h :: t
⊦ ∀f g. f = g ⇔ ∀x. f x = g x
⊦ ∀f v. (∀y. y = v ⇒ f y) ⇔ f v
⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a
⊦ ∀f x y. pair.UNCURRY f (x, y) = f x y
⊦ (∨) = λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t
⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ (t1 ⇒ t2) ∧ (t2 ⇒ t1)
⊦ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)
⊦ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m
⊦ bool.LET f v ⇔ (∀) (Combinator.s ((⇒) ∘ (marker.Abbrev ∘ flip (=) v)) f)
⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
⊦ Combinator.s f (pair.UNCURRY g) =
pair.UNCURRY (Combinator.s (Combinator.s ∘ ((∘) f ∘ ,)) g)
⊦ list.LIST_TO_SET [] = pred_set.EMPTY ∧
list.LIST_TO_SET (h :: t) = pred_set.INSERT h (list.LIST_TO_SET t)
⊦ list.GENLIST f 0 = [] ∧ list.GENLIST f n = list.GENLIST_AUX f n []
⊦ (∀l. l @ [] = l) ∧ ∀l. [] @ l = l
⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥
⊦ ∀P l. filter P l = [] ⇔ all (λx. ¬P x) l
⊦ ∀f. combin.COMM f ⇔ ∀x y. f x y = f y x
⊦ ∀R. relation.total R ⇔ ∀x y. R x y ∨ R y x
⊦ ∀R.
relation.RC (transitiveClosure R) = relation.RTC R ∧
transitiveClosure (relation.RC R) = relation.RTC R
⊦ rich_list.COUNT_LIST 0 = [] ∧
∀n. rich_list.COUNT_LIST (suc n) = list.SNOC n (rich_list.COUNT_LIST n)
⊦ ∀P Q. (∀x. P ⇒ Q x) ⇔ P ⇒ ∀y. Q y
⊦ ∀P Q. (∀y. P ∨ Q y) ⇔ P ∨ ∀y. Q y
⊦ ∀Q P. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q
⊦ ∀P Q. (∃y. P ∧ Q y) ⇔ P ∧ ∃y. Q y
⊦ ∀P Q. P ∧ (∀y. Q y) ⇔ ∀y. P ∧ Q y
⊦ ∀P Q. P ∨ (∃y. Q y) ⇔ ∃y. P ∨ Q y
⊦ ∀P Q. (∀x. P x ⇒ Q) ⇔ (∃x. P x) ⇒ Q
⊦ ∀P Q. (∃y. P y ∧ Q) ⇔ (∃x. P x) ∧ Q
⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀y. P y ∧ Q
⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q
⊦ ∀s.
pred_set.FINITE s ⇒
∀x. bool.IN x (list.LIST_TO_SET (list.SET_TO_LIST s)) ⇔ bool.IN x s
⊦ list.EL 0 = head ∧ list.EL (suc n) (l :: ls) = list.EL n ls
⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥
⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3
⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3
⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C
⊦ ∀m n p. arithmetic.- m n ≤ p ⇔ m ≤ n + p
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + p = n + p ⇔ m = n
⊦ ∀m n p. m + p < n + p ⇔ m < n
⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3
⊦ ∀f g n. map f (list.GENLIST g n) = list.GENLIST (f ∘ g) n
⊦ ∀P l. any P l ⇔ ∃e. bool.IN e (list.LIST_TO_SET l) ∧ P e
⊦ ∀s t. s = t ⇔ ∀x. bool.IN x s ⇔ bool.IN x t
⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1 ∧ (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ t1 ∧ t2 ∨ ¬t1 ∧ ¬t2
⊦ ∀n m. arithmetic.- n m = if m < n then numeral.iSUB ⊤ n m else 0
⊦ length [] = 0 ∧ ∀h t. length (h :: t) = suc (length t)
⊦ ∀f g p. pair.## f g p = (f (fst p), g (snd p))
⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n
⊦ ∀R x y. relation.RC R x y ⇔ x = y ∨ R x y
⊦ ∀R x y. relation.SC R x y ⇔ R x y ∨ R y x
⊦ ∀R. relation.equivalence R ⇔ ∀x y. R x y ⇔ R x = R y
⊦ rich_list.COUNT_LIST 0 = [] ∧
∀n. rich_list.COUNT_LIST (suc n) = 0 :: map suc (rich_list.COUNT_LIST n)
⊦ bool.IN x (list.LIST_TO_SET (list.GENLIST f n)) ⇔ ∃m. m < n ∧ x = f m
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)
⊦ ∀m n. ¬(m = n) ⇔ suc m ≤ n ∨ suc n ≤ m
⊦ ∀n d. 0 < n ∧ 1 < d ⇒ n div d < n
⊦ ∀R f x y. relation.inv_image R f x y ⇔ R (f x) (f y)
⊦ list.SUM [] = 0 ∧ ∀h t. list.SUM (h :: t) = h + list.SUM t
⊦ ∀x y s. bool.IN x (pred_set.INSERT y s) ⇔ x = y ∨ bool.IN x s
⊦ ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)
⊦ ∀n r. r < n ⇒ ∀q. (q * n + r) div n = q
⊦ ∀n r. r < n ⇒ ∀q. (q * n + r) mod n = r
⊦ ∀f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2
⊦ ∀P L M. filter P (L @ M) = filter P L @ filter P M
⊦ ∀s t x. bool.IN x (pred_set.UNION s t) ⇔ bool.IN x s ∨ bool.IN x t
⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x
⊦ ∀f b x y. f (if b then x else y) = if b then f x else f y
⊦ ∀f R y z. R y z ⇒ relation.RESTRICT f R z y = f y
⊦ ∀P. (∀n. (∀m. m < n ⇒ P m) ⇒ P n) ⇒ ∀n. P n
⊦ ∀P L x.
bool.IN x (list.LIST_TO_SET (filter P L)) ⇔
P x ∧ bool.IN x (list.LIST_TO_SET L)
⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀y. Q y
⊦ ∀P Q. (∃y. P y ∨ Q y) ⇔ (∃x. P x) ∨ ∃y. Q y
⊦ ∀R. relation.antisymmetric R ⇔ ∀x y. R x y ∧ R y x ⇒ x = y
⊦ ∀l.
list.ALL_DISTINCT l ⇔
∀x. bool.IN x (list.LIST_TO_SET l) ⇒ filter ((=) x) l = x :: []
⊦ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h :: t)) ⇒ ∀l. P l
⊦ reverse [] = [] ∧ ∀h t. reverse (h :: t) = reverse t @ h :: []
⊦ (∀t1 t2. (if ⊤ then t1 else t2) = t1) ∧
∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀m n p. arithmetic.- m n < p ⇔ m < n + p ∧ 0 < p
⊦ ∀l x. bool.IN x (list.LIST_TO_SET l) ⇔ ∃n. n < length l ∧ x = list.EL n l
⊦ ∀s.
pred_set.FINITE s ⇒
(pred_set.SUM_IMAGE f s = 0 ⇔ ∀x. bool.IN x s ⇒ f x = 0)
⊦ ∀f. combin.ASSOC f ⇔ ∀x y z. f x (f y z) = f (f x y) z
⊦ ∀R. transitive R ⇔ ∀x y z. R x y ∧ R y z ⇒ R x z
⊦ (∀x y. R x y ⇒ Q x y) ⇒ transitiveClosure R x y ⇒ transitiveClosure Q x y
⊦ ∀e l1 l2.
bool.IN e (list.LIST_TO_SET (l1 @ l2)) ⇔
bool.IN e (list.LIST_TO_SET l1) ∨ bool.IN e (list.LIST_TO_SET l2)
⊦ (∀x. rich_list.REPLICATE 0 x = []) ∧
∀n x. rich_list.REPLICATE (suc n) x = x :: rich_list.REPLICATE n x
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ ∀f a b.
list.GENLIST f (a + b) =
list.GENLIST f b @ list.GENLIST (λt. f (t + b)) a
⊦ (list.ALL_DISTINCT [] ⇔ ⊤) ∧
∀h t.
list.ALL_DISTINCT (h :: t) ⇔
¬bool.IN h (list.LIST_TO_SET t) ∧ list.ALL_DISTINCT t
⊦ ∀n.
numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n) ∧
numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n) ∧
numeral.iDUB 0 = 0
⊦ (∀f. list.GENLIST f 0 = []) ∧
∀f n. list.GENLIST f (suc n) = list.SNOC (f n) (list.GENLIST f n)
⊦ ∀l f x.
bool.IN x (list.LIST_TO_SET (map f l)) ⇔
∃y. x = f y ∧ bool.IN y (list.LIST_TO_SET l)
⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)
⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)
⊦ ∀f0 f1. ∃fn. fn [] = f0 ∧ ∀a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)
⊦ ∀x y z. 0 < z ⇒ (x < y div z ⇔ (x + 1) * z ≤ y)
⊦ ∀R. wellFounded R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
⊦ s1 = s2 ∧ (∀x. bool.IN x s2 ⇒ f1 x = f2 x) ⇒
pred_set.SUM_IMAGE f1 s1 = pred_set.SUM_IMAGE f2 s2
⊦ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')
⊦ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)
⊦ suc 0 = 1 ∧ (∀n. suc (bit1 n) = arithmetic.BIT2 n) ∧
∀n. suc (arithmetic.BIT2 n) = bit1 (suc n)
⊦ (∀l. [] @ l = l) ∧ ∀l1 l2 h. (h :: l1) @ l2 = h :: l1 @ l2
⊦ ∀n m l.
m ≤ n ⇒
list.TAKE m l @ list.TAKE (arithmetic.- n m) (list.DROP m l) =
list.TAKE n l
⊦ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)
⊦ ∀M R f.
f = relation.WFREC R M ⇒ wellFounded R ⇒
∀x. f x = M (relation.RESTRICT f R x) x
⊦ (∀f. map f [] = []) ∧ ∀f h t. map f (h :: t) = f h :: map f t
⊦ (∀P. all P [] ⇔ ⊤) ∧ ∀P h t. all P (h :: t) ⇔ P h ∧ all P t
⊦ (∀x. last (x :: []) = x) ∧ ∀x y z. last (x :: y :: z) = last (y :: z)
⊦ ∀P P' Q Q'. (Q ⇒ (P ⇔ P')) ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')
⊦ list.ALL_DISTINCT (list.GENLIST f n) ⇔
∀m1 m2. m1 < n ∧ m2 < n ∧ f m1 = f m2 ⇒ m1 = m2
⊦ ∀l1 l2.
list.ALL_DISTINCT (l1 @ l2) ⇔
list.ALL_DISTINCT l1 ∧ list.ALL_DISTINCT l2 ∧
∀e. bool.IN e (list.LIST_TO_SET l1) ⇒ ¬bool.IN e (list.LIST_TO_SET l2)
⊦ (∀v f. list.list_CASE [] v f = v) ∧
∀a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1
⊦ (∀x y. R x y ⇒ f x = f y) ⇒ ∀x y. transitiveClosure R x y ⇒ f x = f y
⊦ (∀x y. P x ∧ R x y ⇒ P y) ⇒ ∀x y. P x ∧ transitiveClosure R x y ⇒ P y
⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)
⊦ (∀f. list.list_size f [] = 0) ∧
∀f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)
⊦ ∀f.
pred_set.SUM_IMAGE f pred_set.EMPTY = 0 ∧
∀e s.
pred_set.FINITE s ⇒
pred_set.SUM_IMAGE f (pred_set.INSERT e s) =
f e + pred_set.SUM_IMAGE f (pred_set.DELETE s e)
⊦ (∀x. bool.IN x (list.LIST_TO_SET []) ⇔ ⊥) ∧
∀x h t.
bool.IN x (list.LIST_TO_SET (h :: t)) ⇔
x = h ∨ bool.IN x (list.LIST_TO_SET t)
⊦ ∀f g M N. M = N ∧ (∀x. x = N ⇒ f x = g x) ⇒ bool.LET f M = bool.LET g N
⊦ (∀P. filter P [] = []) ∧
∀P h t. filter P (h :: t) = if P h then h :: filter P t else filter P t
⊦ (∀f e. list.FOLDR f e [] = e) ∧
∀f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)
⊦ (∀x y. R x y ⇒ Q (f x) (f y)) ∧ transitive Q ⇒
∀x y. transitiveClosure R x y ⇒ Q (f x) (f y)
⊦ ∀t. (⊤ ∧ t ⇔ t) ∧ (t ∧ ⊤ ⇔ t) ∧ (⊥ ∧ t ⇔ ⊥) ∧ (t ∧ ⊥ ⇔ ⊥) ∧ (t ∧ t ⇔ t)
⊦ ∀t. (⊤ ∨ t ⇔ ⊤) ∧ (t ∨ ⊤ ⇔ ⊤) ∧ (⊥ ∨ t ⇔ t) ∧ (t ∨ ⊥ ⇔ t) ∧ (t ∨ t ⇔ t)
⊦ (∀n. list.TAKE n [] = []) ∧
∀n x xs.
list.TAKE n (x :: xs) =
if n = 0 then [] else x :: list.TAKE (arithmetic.- n 1) xs
⊦ ∀t. (⊤ ⇒ t ⇔ t) ∧ (t ⇒ ⊤ ⇔ ⊤) ∧ (⊥ ⇒ t ⇔ ⊤) ∧ (t ⇒ t ⇔ ⊤) ∧ (t ⇒ ⊥ ⇔ ¬t)
⊦ ∀R.
(∀x y. R x y ⇒ transitiveClosure R x y) ∧
∀x y z.
transitiveClosure R x y ∧ transitiveClosure R y z ⇒
transitiveClosure R x z
⊦ (∀l1 l2 l3. l1 @ l2 = l1 @ l3 ⇔ l2 = l3) ∧
∀l1 l2 l3. l2 @ l1 = l3 @ l1 ⇔ l2 = l3
⊦ ∀P Q x x' y y'.
(P ⇔ Q) ∧ (Q ⇒ x = x') ∧ (¬Q ⇒ y = y') ⇒
(if P then x else y) = if Q then x' else y'
⊦ (p ⇔ q ⇔ r) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)
⊦ ∀R P.
(∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ P y z ⇒ P x z) ⇒
∀u v. transitiveClosure R u v ⇒ P u v
⊦ (p ⇔ if q then r else s) ⇔
(p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧
(q ∨ s ∨ ¬p)
⊦ ∀m n.
0 * m = 0 ∧ m * 0 = 0 ∧ 1 * m = m ∧ m * 1 = m ∧ suc m * n = m * n + n ∧
m * suc n = m + m * n
⊦ (∀l1 l2 l1' l2'.
length l1 = length l1' ⇒
(l1 @ l2 = l1' @ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
∀l1 l2 l1' l2'.
length l2 = length l2' ⇒ (l1 @ l2 = l1' @ l2' ⇔ l1 = l1' ∧ l2 = l2')
⊦ ∀n m.
(0 ≤ n ⇔ ⊤) ∧ (bit1 n ≤ 0 ⇔ ⊥) ∧ (arithmetic.BIT2 n ≤ 0 ⇔ ⊥) ∧
(bit1 n ≤ bit1 m ⇔ n ≤ m) ∧ (bit1 n ≤ arithmetic.BIT2 m ⇔ n ≤ m) ∧
(arithmetic.BIT2 n ≤ bit1 m ⇔ ¬(m ≤ n)) ∧
(arithmetic.BIT2 n ≤ arithmetic.BIT2 m ⇔ n ≤ m)
⊦ ∀n m.
(0 < bit1 n ⇔ ⊤) ∧ (0 < arithmetic.BIT2 n ⇔ ⊤) ∧ (n < 0 ⇔ ⊥) ∧
(bit1 n < bit1 m ⇔ n < m) ∧
(arithmetic.BIT2 n < arithmetic.BIT2 m ⇔ n < m) ∧
(bit1 n < arithmetic.BIT2 m ⇔ ¬(m < n)) ∧
(arithmetic.BIT2 n < bit1 m ⇔ n < m)
⊦ ∀n m.
(0 = bit1 n ⇔ ⊥) ∧ (bit1 n = 0 ⇔ ⊥) ∧ (0 = arithmetic.BIT2 n ⇔ ⊥) ∧
(arithmetic.BIT2 n = 0 ⇔ ⊥) ∧ (bit1 n = arithmetic.BIT2 m ⇔ ⊥) ∧
(arithmetic.BIT2 n = bit1 m ⇔ ⊥) ∧ (bit1 n = bit1 m ⇔ n = m) ∧
(arithmetic.BIT2 n = arithmetic.BIT2 m ⇔ n = m)
⊦ ∀b n m.
numeral.iSUB b 0 x = 0 ∧ numeral.iSUB ⊤ n 0 = n ∧
numeral.iSUB ⊥ (bit1 n) 0 = numeral.iDUB n ∧
numeral.iSUB ⊤ (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (bit1 n) (bit1 m) = bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊤ (bit1 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (bit1 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) 0 = bit1 n ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (bit1 m) =
bit1 (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (bit1 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m)
⊦ ∀n m.
numeral.iZ (0 + n) = n ∧ numeral.iZ (n + 0) = n ∧
numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m)) ∧
numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (suc (n + m)) ∧ suc (0 + n) = suc n ∧
suc (n + 0) = suc n ∧ suc (bit1 n + bit1 m) = bit1 (suc (n + m)) ∧
suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (0 + n) = numeral.iiSUC n ∧
numeral.iiSUC (n + 0) = numeral.iiSUC n ∧
numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (numeral.iiSUC (n + m))
⊦ (∀m. 0 + m = m) ∧ (∀m. m + 0 = m) ∧ (∀n m. n + m = numeral.iZ (n + m)) ∧
(∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧ (∀n m. n * m = n * m) ∧
(∀n. arithmetic.- 0 n = 0) ∧ (∀n. arithmetic.- n 0 = n) ∧
(∀n m. arithmetic.- n m = arithmetic.- n m) ∧ (∀n. 0 ↑ bit1 n = 0) ∧
(∀n. 0 ↑ arithmetic.BIT2 n = 0) ∧ (∀n. n ↑ 0 = 1) ∧
(∀n m. n ↑ m = n ↑ m) ∧ suc 0 = 1 ∧ (∀n. suc n = suc n) ∧
prim_rec.PRE 0 = 0 ∧ (∀n. prim_rec.PRE n = prim_rec.PRE n) ∧
(∀n. n = 0 ⇔ n = 0) ∧ (∀n. 0 = n ⇔ n = 0) ∧ (∀n m. n = m ⇔ n = m) ∧
(∀n. n < 0 ⇔ ⊥) ∧ (∀n. 0 < n ⇔ 0 < n) ∧ (∀n m. n < m ⇔ n < m) ∧
(∀n. 0 > n ⇔ ⊥) ∧ (∀n. n > 0 ⇔ 0 < n) ∧ (∀n m. n > m ⇔ m < n) ∧
(∀n. 0 ≤ n ⇔ ⊤) ∧ (∀n. n ≤ 0 ⇔ n ≤ 0) ∧ (∀n m. n ≤ m ⇔ n ≤ m) ∧
(∀n. n ≥ 0 ⇔ ⊤) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧ (∀n m. n ≥ m ⇔ m ≤ n) ∧
(∀n. odd n ⇔ odd n) ∧ (∀n. even n ⇔ even n) ∧ ¬odd 0 ∧ even 0