Package hol-monad: HOL monad theories

Information

name	hol-monad
version	1.0
description	HOL monad theories
author	HOL developers <hol-developers@lists.sourceforge.net>
license	MIT
checksum	8e2fbe142b1e7329eb30674b33010a3ab950547a
requires	base hol-base
show	Data.Bool Data.List Data.Pair Function HOL4 Number.Natural Relation

Files

Package tarball hol-monad-1.0.tgz
Theory source file hol-monad.thy (included in the package tarball)

Defined Constants

HOL4
- errorStateMonad
  - errorStateMonad.mapM
  - errorStateMonad.sequence
  - errorStateMonad.BIND
  - errorStateMonad.ES_APPLY
  - errorStateMonad.ES_CHOICE
  - errorStateMonad.ES_FAIL
  - errorStateMonad.ES_GUARD
  - errorStateMonad.ES_LIFT2
  - errorStateMonad.EXT
  - errorStateMonad.FOR
  - errorStateMonad.FOREACH
  - errorStateMonad.IGNORE_BIND
  - errorStateMonad.JOIN
  - errorStateMonad.MCOMP
  - errorStateMonad.MMAP
  - errorStateMonad.NARROW
  - errorStateMonad.READ
  - errorStateMonad.UNIT
  - errorStateMonad.WIDEN
  - errorStateMonad.WRITE
- state_transformer
  - state_transformer.mapM
  - state_transformer.sequence
  - state_transformer.BIND
  - state_transformer.EXT
  - state_transformer.FOR
  - state_transformer.FOREACH
  - state_transformer.IGNORE_BIND
  - state_transformer.JOIN
  - state_transformer.MCOMP
  - state_transformer.MMAP
  - state_transformer.MWHILE
  - state_transformer.NARROW
  - state_transformer.READ
  - state_transformer.UNIT
  - state_transformer.WIDEN
  - state_transformer.WRITE

Theorems

⊦ state_transformer.UNIT = pair.CURRY id

⊦ errorStateMonad.UNIT = pair.CURRY Data.Option.some

⊦ state_transformer.JOIN = state_transformer.EXT id

⊦ state_transformer.EXT state_transformer.UNIT = id

⊦ state_transformer.MMAP id = id

⊦ errorStateMonad.MMAP id = id

⊦ state_transformer.sequence [] = state_transformer.UNIT []

⊦ errorStateMonad.sequence [] = errorStateMonad.UNIT []

⊦ errorStateMonad.ES_CHOICE errorStateMonad.ES_FAIL xM = xM

⊦ errorStateMonad.ES_CHOICE xM errorStateMonad.ES_FAIL = xM

⊦ errorStateMonad.BIND errorStateMonad.ES_FAIL fM = errorStateMonad.ES_FAIL

⊦ state_transformer.JOIN ∘ state_transformer.UNIT = id

⊦ errorStateMonad.JOIN ∘ errorStateMonad.UNIT = id

⊦ ∀s. errorStateMonad.ES_FAIL s = Data.Option.none

⊦ state_transformer.mapM f [] = state_transformer.UNIT []

⊦ errorStateMonad.mapM f [] = errorStateMonad.UNIT []

⊦ state_transformer.EXT f ∘ state_transformer.UNIT = f

⊦ state_transformer.JOIN ∘ state_transformer.MMAP state_transformer.UNIT =
id

⊦ errorStateMonad.JOIN ∘ errorStateMonad.MMAP errorStateMonad.UNIT = id

⊦ ∀s. pair.UNCURRY state_transformer.UNIT s = s

⊦ ∀k. state_transformer.BIND k state_transformer.UNIT = k

⊦ ∀k. errorStateMonad.BIND k errorStateMonad.UNIT = k

⊦ state_transformer.EXT f =
state_transformer.JOIN ∘ state_transformer.MMAP f

⊦ state_transformer.MMAP f =
state_transformer.EXT (state_transformer.UNIT ∘ f)

⊦ state_transformer.BIND m f = state_transformer.EXT f m

⊦ ∀x. snd ∘ state_transformer.UNIT x = id

⊦ ∀z. state_transformer.JOIN z = state_transformer.BIND z id

⊦ ∀z. errorStateMonad.JOIN z = errorStateMonad.BIND z id

⊦ ∀x. state_transformer.UNIT x = λs. (x, s)

⊦ errorStateMonad.MCOMP g f = errorStateMonad.EXT g ∘ f

⊦ errorStateMonad.ES_APPLY (errorStateMonad.UNIT f) xM =
errorStateMonad.MMAP f xM

⊦ state_transformer.JOIN ∘ state_transformer.MMAP state_transformer.JOIN =
state_transformer.JOIN ∘ state_transformer.JOIN

⊦ errorStateMonad.JOIN ∘ errorStateMonad.MMAP errorStateMonad.JOIN =
errorStateMonad.JOIN ∘ errorStateMonad.JOIN

⊦ ∀x. fst ∘ state_transformer.UNIT x = const x

⊦ ∀f. state_transformer.mapM f = state_transformer.sequence ∘ map f

⊦ ∀f. errorStateMonad.mapM f = errorStateMonad.sequence ∘ map f

⊦ ∀x. errorStateMonad.UNIT x = λs. Data.Option.some (x, s)

⊦ ∀f. state_transformer.WRITE f = λs. (Data.Unit.(), f s)

⊦ ∀f. state_transformer.READ f = λs. (f s, s)

⊦ errorStateMonad.ES_APPLY (errorStateMonad.UNIT f)
(errorStateMonad.UNIT x) = errorStateMonad.UNIT (f x)

⊦ ∀b.
    errorStateMonad.ES_GUARD b =
    if b then errorStateMonad.UNIT Data.Unit.()
    else errorStateMonad.ES_FAIL

⊦ ∀f.
errorStateMonad.MMAP f ∘ errorStateMonad.UNIT =
errorStateMonad.UNIT ∘ f

⊦ ∀f.
state_transformer.MMAP f ∘ state_transformer.UNIT =
state_transformer.UNIT ∘ f

⊦ ∀f.
state_transformer.EXT f ∘ state_transformer.JOIN =
state_transformer.EXT (state_transformer.EXT f)

⊦ ∀f. errorStateMonad.WRITE f = λs. Data.Option.some (Data.Unit.(), f s)

⊦ ∀f. errorStateMonad.READ f = λs. Data.Option.some (f s, s)

⊦ ∀k x. state_transformer.BIND (state_transformer.UNIT x) k = k x

⊦ ∀k x. errorStateMonad.BIND (errorStateMonad.UNIT x) k = k x

⊦ ∀g m. errorStateMonad.EXT g m = errorStateMonad.BIND m g

⊦ state_transformer.MCOMP g f =
pair.CURRY (pair.UNCURRY g ∘ pair.UNCURRY f)

⊦ state_transformer.EXT (state_transformer.MCOMP g f) =
state_transformer.EXT g ∘ state_transformer.EXT f

⊦ ∀f g.
state_transformer.IGNORE_BIND f g = state_transformer.BIND f (λx. g)

⊦ ∀f g. errorStateMonad.IGNORE_BIND f g = errorStateMonad.BIND f (λx. g)

⊦ ∀k m.
state_transformer.BIND k m =
state_transformer.JOIN (state_transformer.MMAP m k)

⊦ ∀g f. state_transformer.BIND g f = pair.UNCURRY f ∘ g

⊦ ∀k m.
errorStateMonad.BIND k m =
errorStateMonad.JOIN (errorStateMonad.MMAP m k)

⊦ ∀f m. state_transformer.EXT f m = pair.UNCURRY f ∘ m

⊦ ∀g f. state_transformer.MCOMP g f = state_transformer.EXT g ∘ f

⊦ errorStateMonad.ES_CHOICE xM (errorStateMonad.ES_CHOICE yM zM) =
errorStateMonad.ES_CHOICE (errorStateMonad.ES_CHOICE xM yM) zM

⊦ errorStateMonad.MCOMP f (errorStateMonad.MCOMP g h) =
errorStateMonad.MCOMP (errorStateMonad.MCOMP f g) h

⊦ state_transformer.MCOMP f (state_transformer.MCOMP g h) =
state_transformer.MCOMP (state_transformer.MCOMP f g) h

⊦ errorStateMonad.MCOMP g errorStateMonad.UNIT = g ∧
errorStateMonad.MCOMP errorStateMonad.UNIT f = f

⊦ errorStateMonad.IGNORE_BIND errorStateMonad.ES_FAIL xM =
  errorStateMonad.ES_FAIL ∧
  errorStateMonad.IGNORE_BIND xM errorStateMonad.ES_FAIL =
  errorStateMonad.ES_FAIL

⊦ state_transformer.MCOMP g state_transformer.UNIT = g ∧
state_transformer.MCOMP state_transformer.UNIT f = f

⊦ ∀f.
errorStateMonad.MMAP f ∘ errorStateMonad.JOIN =
errorStateMonad.JOIN ∘ errorStateMonad.MMAP (errorStateMonad.MMAP f)

⊦ ∀f.
    state_transformer.MMAP f ∘ state_transformer.JOIN =
    state_transformer.JOIN ∘
    state_transformer.MMAP (state_transformer.MMAP f)

⊦ ∀f m.
state_transformer.MMAP f m =
state_transformer.BIND m (state_transformer.UNIT ∘ f)

⊦ ∀f m.
errorStateMonad.MMAP f m =
errorStateMonad.BIND m (errorStateMonad.UNIT ∘ f)

⊦ ∀f g.
errorStateMonad.MMAP (f ∘ g) =
errorStateMonad.MMAP f ∘ errorStateMonad.MMAP g

⊦ ∀f g.
state_transformer.MMAP (f ∘ g) =
state_transformer.MMAP f ∘ state_transformer.MMAP g

⊦ ∀g f.
errorStateMonad.MCOMP g f =
pair.CURRY (option.OPTION_MCOMP (pair.UNCURRY g) (pair.UNCURRY f))

⊦ errorStateMonad.IGNORE_BIND (errorStateMonad.ES_GUARD ⊥) xM =
errorStateMonad.ES_FAIL ∧
errorStateMonad.IGNORE_BIND (errorStateMonad.ES_GUARD ⊤) xM = xM

⊦ state_transformer.MCOMP (state_transformer.UNIT ∘ g)
(state_transformer.UNIT ∘ f) = state_transformer.UNIT ∘ (g ∘ f)

⊦ ∀f g. fst ∘ state_transformer.MMAP f g = f ∘ (fst ∘ g)

⊦ errorStateMonad.BIND (errorStateMonad.ES_GUARD ⊥) fM =
errorStateMonad.ES_FAIL ∧
errorStateMonad.BIND (errorStateMonad.ES_GUARD ⊤) fM = fM Data.Unit.()

⊦ ∀f xM yM.
errorStateMonad.ES_LIFT2 f xM yM =
errorStateMonad.ES_APPLY (errorStateMonad.MMAP f xM) yM

⊦ ∀fM xM.
    errorStateMonad.ES_APPLY fM xM =
    errorStateMonad.BIND fM
      (λf. errorStateMonad.BIND xM (λx. errorStateMonad.UNIT (f x)))

⊦ state_transformer.sequence =
  list.FOLDR
    (λm ms.
       state_transformer.BIND m
         (λx.
            state_transformer.BIND ms
              (λxs. state_transformer.UNIT (x :: xs))))
    (state_transformer.UNIT [])

⊦ errorStateMonad.sequence =
  list.FOLDR
    (λm ms.
       errorStateMonad.BIND m
         (λx.
            errorStateMonad.BIND ms (λxs. errorStateMonad.UNIT (x :: xs))))
    (errorStateMonad.UNIT [])

⊦ ∀f.
    state_transformer.WIDEN f =
    pair.UNCURRY
      (λs₁ s₂. bool.LET (pair.UNCURRY (λr s₃. (r, s₁, s₃))) (f s₂))

⊦ ∀xM yM s.
errorStateMonad.ES_CHOICE xM yM s =
option.option_CASE (xM s) (yM s) (λv₁. Data.Option.some v₁)

⊦ ∀k m n.
state_transformer.BIND k (λa. state_transformer.BIND (m a) n) =
state_transformer.BIND (state_transformer.BIND k m) n

⊦ ∀k m n.
errorStateMonad.BIND k (λa. errorStateMonad.BIND (m a) n) =
errorStateMonad.BIND (errorStateMonad.BIND k m) n

⊦ state_transformer.mapM f (x :: xs) =
  state_transformer.BIND (f x)
    (λy.
       state_transformer.BIND (state_transformer.mapM f xs)
         (λys. state_transformer.UNIT (y :: ys)))

⊦ errorStateMonad.mapM f (x :: xs) =
  errorStateMonad.BIND (f x)
    (λy.
       errorStateMonad.BIND (errorStateMonad.mapM f xs)
         (λys. errorStateMonad.UNIT (y :: ys)))

⊦ ∀v f.
state_transformer.NARROW v f =
λs. bool.LET (pair.UNCURRY (λr s₁. (r, snd s₁))) (f (v, s))

⊦ ∀g b.
    state_transformer.MWHILE g b =
    state_transformer.BIND g
      (λgv.
         if gv then
           state_transformer.IGNORE_BIND b (state_transformer.MWHILE g b)
         else state_transformer.UNIT Data.Unit.())

⊦ ∀f.
    errorStateMonad.WIDEN f =
    pair.UNCURRY
      (λs₁ s₂.
         option.option_CASE (f s₂) Data.Option.none
           (λv. pair.pair_CASE v (λr s₃. Data.Option.some (r, s₁, s₃))))

⊦ ∀g f s₀.
    errorStateMonad.BIND g f s₀ =
    option.option_CASE (g s₀) Data.Option.none
      (λv. pair.pair_CASE v (λb s. f b s))

⊦ ∀v f.
    errorStateMonad.NARROW v f =
    λs.
      option.option_CASE (f (v, s)) Data.Option.none
        (λv. pair.pair_CASE v (λr s₁. Data.Option.some (r, snd s₁)))

⊦ (∀a.
     state_transformer.FOREACH ([], a) =
     state_transformer.UNIT Data.Unit.()) ∧
  ∀t h a.
    state_transformer.FOREACH (h :: t, a) =
    state_transformer.BIND (a h) (λu. state_transformer.FOREACH (t, a))

⊦ (∀a.
     errorStateMonad.FOREACH ([], a) = errorStateMonad.UNIT Data.Unit.()) ∧
  ∀t h a.
    errorStateMonad.FOREACH (h :: t, a) =
    errorStateMonad.BIND (a h) (λu. errorStateMonad.FOREACH (t, a))

⊦ ∀P.
(∀a. P ([], a)) ∧ (∀h t a. P (t, a) ⇒ P (h :: t, a)) ⇒ ∀v v₁. P (v, v₁)

⊦ ∀j i a.
    state_transformer.FOR (i, j, a) =
    if i = j then a i
    else
      state_transformer.BIND (a i)
        (λu.
           state_transformer.FOR
             ((if i < j then i + 1 else arithmetic.- i 1), j, a))

⊦ ∀j i a.
    errorStateMonad.FOR (i, j, a) =
    if i = j then a i
    else
      errorStateMonad.BIND (a i)
        (λu.
           errorStateMonad.FOR
             ((if i < j then i + 1 else arithmetic.- i 1), j, a))

⊦ state_transformer.FOREACH =
  relation.WFREC (select R. wellFounded R ∧ ∀h a t. R (t, a) (h :: t, a))
    (λFOREACH a'.
       pair.pair_CASE a'
         (λv a.
            list.list_CASE v (id (state_transformer.UNIT Data.Unit.()))
              (λh t.
                 id (state_transformer.BIND (a h) (λu. FOREACH (t, a))))))

⊦ errorStateMonad.FOREACH =
  relation.WFREC (select R. wellFounded R ∧ ∀h a t. R (t, a) (h :: t, a))
    (λFOREACH a'.
       pair.pair_CASE a'
         (λv a.
            list.list_CASE v (id (errorStateMonad.UNIT Data.Unit.()))
              (λh t.
                 id (errorStateMonad.BIND (a h) (λu. FOREACH (t, a))))))

⊦ ∀P.
    (∀i j a.
       (¬(i = j) ⇒ P ((if i < j then i + 1 else arithmetic.- i 1), j, a)) ⇒
       P (i, j, a)) ⇒ ∀v v₁ v₂. P (v, v₁, v₂)

⊦ state_transformer.FOR =
  relation.WFREC
    (select R.
       wellFounded R ∧
       ∀a j i.
         ¬(i = j) ⇒
         R ((if i < j then i + 1 else arithmetic.- i 1), j, a) (i, j, a))
    (λFOR a'.
       pair.pair_CASE a'
         (λi v₁.
            pair.pair_CASE v₁
              (λj a.
                 id
                   (if i = j then a i
                    else
                      state_transformer.BIND (a i)
                        (λu.
                           FOR
                             ((if i < j then i + 1 else arithmetic.- i 1),
                              j, a))))))

⊦ errorStateMonad.FOR =
  relation.WFREC
    (select R.
       wellFounded R ∧
       ∀a j i.
         ¬(i = j) ⇒
         R ((if i < j then i + 1 else arithmetic.- i 1), j, a) (i, j, a))
    (λFOR a'.
       pair.pair_CASE a'
         (λi v₁.
            pair.pair_CASE v₁
              (λj a.
                 id
                   (if i = j then a i
                    else
                      errorStateMonad.BIND (a i)
                        (λu.
                           FOR
                             ((if i < j then i + 1 else arithmetic.- i 1),
                              j, a))))))

External Type Operators

→
bool
Data
- List
  - list
- Option
  - Data.Option.option
- Pair
  - ×
- Unit
  - Data.Unit.unit
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - map
- Option
  - Data.Option.none
  - Data.Option.some
- Pair
  - ,
  - fst
  - snd
- Unit
  - Data.Unit.()
Function
- const
- flip
- id
- ∘
- Combinator
  - Combinator.s
HOL4
- arithmetic
  - arithmetic.-
  - arithmetic.BIT2
  - arithmetic.FUNPOW
- bool
  - bool.LET
- list
  - list.list_CASE
  - list.list_size
  - list.FOLDR
- marker
  - marker.Abbrev
- numeral
  - numeral.iZ
  - numeral.iiSUC
- option
  - option.option_CASE
  - option.OPTION_BIND
  - option.OPTION_MCOMP
- pair
  - pair.pair_CASE
  - pair.CURRY
  - pair.UNCURRY
- prim_rec
  - prim_rec.measure
  - prim_rec.PRE
- relation
  - relation.inv_image
  - relation.RESTRICT
  - relation.WFREC
- while
  - while.LEAST
Number
- Natural
  - *
  - +
  - <
  - ≤
  - >
  - ≥
  - ↑
  - bit1
  - even
  - odd
  - suc
  - zero
Relation
- wellFounded

Assumptions

⊦ ⊤

⊦ wellFounded (<)

⊦ prim_rec.measure = relation.inv_image (<)

⊦ ∀t. ⊥ ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀m. wellFounded (prim_rec.measure m)

⊦ ∀x. id x = x

⊦ ∀t. t ∨ ¬t

⊦ ∀x. marker.Abbrev x ⇔ x

⊦ (¬) = λt. t ⇒ ⊥

⊦ (∃) = λP. P ((select) P)

⊦ ∀a. ∃x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λP. P = λx. ⊤

⊦ arithmetic.BIT2 0 = suc 1

⊦ arithmetic.FUNPOW f 0 x = x

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. ¬(Data.Option.none = Data.Option.some x)

⊦ ∀x. x = x ⇔ ⊤

⊦ ∀f. pair.CURRY (pair.UNCURRY f) = f

⊦ ∀f. pair.UNCURRY (pair.CURRY f) = f

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ∀A. A ⇒ ¬A ⇒ ⊥

⊦ ∀t. ¬t ⇒ t ⇒ ⊥

⊦ ∀x y. const x y = x

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t. t ⇒ ⊥ ⇔ t ⇔ ⊥

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀n. suc n = 1 + n

⊦ ∀x. (fst x, snd x) = x

⊦ ∀x y. fst (x, y) = x

⊦ ∀x y. snd (x, y) = y

⊦ ∀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

⊦ ∀n. arithmetic.BIT2 0 * n = n + n

⊦ ∀x. ∃q r. x = (q, r)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀m n. m + n = n + m

⊦ ∀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

⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥

⊦ Combinator.s f (λx. g x) = λx. f x (g x)

⊦ ∀f g. f ∘ g = λx. f (g x)

⊦ ∀A B. A ⇒ B ⇔ ¬A ∨ B

⊦ ∀m n. m < n ⇔ suc m ≤ n

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ ∀m. m = 0 ∨ ∃n. m = suc n

⊦ ∀opt. opt = Data.Option.none ∨ ∃x. opt = Data.Option.some x

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ option.OPTION_MCOMP f (option.OPTION_MCOMP g h) =
option.OPTION_MCOMP (option.OPTION_MCOMP f g) h

⊦ option.OPTION_MCOMP g Data.Option.some = g ∧
option.OPTION_MCOMP Data.Option.some f = f

⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ ∀x y. Data.Option.some x = Data.Option.some y ⇔ x = y

⊦ ∀A B. ¬(A ⇒ B) ⇔ A ∧ ¬B

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀p f. pair.pair_CASE p f = f (fst p) (snd p)

⊦ ∀f v. pair.UNCURRY f v = f (fst v) (snd v)

⊦ ∀m. arithmetic.- 0 m = 0 ∧ arithmetic.- m 0 = m

⊦ ∀f g x. (f ∘ g) x = f (g x)

⊦ ∀f. id ∘ f = f ∧ f ∘ id = f

⊦ ∀f x y. flip f x y = f y x

⊦ ∀R f. relation.inv_image R f = λx y. R (f x) (f y)

⊦ ∀l. l = [] ∨ ∃h t. l = h :: t

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

⊦ ∀f g. (∀x. f x = g x) ⇒ f = g

⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a

⊦ ∀g f m. option.OPTION_MCOMP g f m = option.OPTION_BIND (f m) g

⊦ ∀f x y. pair.UNCURRY f (x, y) = f x y

⊦ ∀f x y. pair.CURRY f x y = f (x, y)

⊦ (∨) = λt₁ t₂. ∀t. (t₁ ⇒ t) ⇒ (t₂ ⇒ t) ⇒ t

⊦ ∀t₁ t₂. (t₁ ⇒ t₂) ⇒ (t₂ ⇒ t₁) ⇒ (t₁ ⇔ t₂)

⊦ ∀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)

⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥

⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥

⊦ ∀t₁ t₂ t₃. t₁ ∧ t₂ ∧ t₃ ⇔ (t₁ ∧ t₂) ∧ t₃

⊦ ∀t₁ t₂ t₃. t₁ ⇒ t₂ ⇒ t₃ ⇔ t₁ ∧ t₂ ⇒ t₃

⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

⊦ ∀m n p. m < arithmetic.- n p ⇔ m + p < n

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

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

⊦ ∀m n p. arithmetic.- (arithmetic.- m n) p = arithmetic.- m (n + p)

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h

⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁ ∧ (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (t₁ ⇔ t₂) ⇔ t₁ ∧ t₂ ∨ ¬t₁ ∧ ¬t₂

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)

⊦ ∀m n. ¬(m = n) ⇔ suc m ≤ n ∨ suc n ≤ m

⊦ ∀m n p. m ≤ n ⇔ suc p * m ≤ suc p * n

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

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

⊦ (∀f. option.OPTION_BIND Data.Option.none f = Data.Option.none) ∧
∀x f. option.OPTION_BIND (Data.Option.some x) f = f x

⊦ ∀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

⊦ (∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁) ∧
∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀m n p. arithmetic.- m n < p ⇔ m < n + p ∧ 0 < p

⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b

⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)

⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)

⊦ ∀R. wellFounded R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

⊦ (∀v f. option.option_CASE Data.Option.none v f = v) ∧
∀x v f. option.option_CASE (Data.Option.some x) v f = f x

⊦ ∀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)

⊦ P (arithmetic.- a b) ⇔ ∀d. (b = a + d ⇒ P 0) ∧ (a = b + d ⇒ P d)

⊦ ∀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 P' Q Q'. (Q ⇒ (P ⇔ P')) ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

⊦ (∀f x. arithmetic.FUNPOW f 0 x = x) ∧
∀f n x. arithmetic.FUNPOW f (suc n) x = arithmetic.FUNPOW f n (f x)

⊦ (∀v f. list.list_CASE [] v f = v) ∧
∀a₀ a₁ v f. list.list_CASE (a₀ :: a₁) v f = f a₀ a₁

⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)

⊦ (∀f. list.list_size f [] = 0) ∧
∀f a₀ a₁. list.list_size f (a₀ :: a₁) = 1 + (f a₀ + list.list_size f a₁)

⊦ ∀Q P.
(∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q (while.LEAST P)

⊦ (∀f e. list.FOLDR f e [] = e) ∧
∀f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)

⊦ ∀t. (⊤ ∧ t ⇔ t) ∧ (t ∧ ⊤ ⇔ t) ∧ (⊥ ∧ t ⇔ ⊥) ∧ (t ∧ ⊥ ⇔ ⊥) ∧ (t ∧ t ⇔ t)

⊦ ∀t. (⊤ ∨ t ⇔ ⊤) ∧ (t ∨ ⊤ ⇔ ⊤) ∧ (⊥ ∨ t ⇔ t) ∧ (t ∨ ⊥ ⇔ t) ∧ (t ∨ t ⇔ t)

⊦ 0 + m = m ∧ m + 0 = m ∧ suc m + n = suc (m + n) ∧ m + suc n = suc (m + n)

⊦ ∀t. (⊤ ⇒ t ⇔ t) ∧ (t ⇒ ⊤ ⇔ ⊤) ∧ (⊥ ⇒ t ⇔ ⊤) ∧ (t ⇒ t ⇔ ⊤) ∧ (t ⇒ ⊥ ⇔ ¬t)

⊦ ∀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)

⊦ ∀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

⊦ ∀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.
    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))

⊦ (∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧ (∀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