Package machine-code-hoare-logic-state: Machine code Hoare logic state

Information

name	machine-code-hoare-logic-state
version	1.1
description	Machine code Hoare logic state
author	HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
license	MIT
checksum	1fe8601cb8e52309802622dfbb3a26bbe4248a0e
requires	base hol-base hol-words machine-code-hoare-logic
show	Data.Bool Data.List Data.Option Data.Pair Function HOL4 Number.Natural Relation

Files

Package tarball machine-code-hoare-logic-state-1.1.tgz
Theory source file machine-code-hoare-logic-state.thy (included in the package tarball)

Defined Constants

HOL4
- state
  - state.FRAME_STATE
  - state.NEXT_REL
  - state.SELECT_STATE
  - state.STATE
- temporal_state
  - temporal_state.TEMPORAL_NEXT

Theorems

⊦ relation.PreOrder (=)

⊦ ∀x. set_sep.SEP_EQ x = pred_set.INSERT x pred_set.EMPTY

⊦ ∀m. state.STATE m = state.SELECT_STATE m pred_set.UNIV

⊦ ∀x c q. temporal_state.TEMPORAL_NEXT x set_sep.SEP_F c q

⊦ ∀m d. state.FRAME_STATE m d = state.SELECT_STATE m (pred_set.COMPL d)

⊦ ∀next. state.NEXT_REL (=) next = λs t. next s = some t

⊦ ∀f x.
pred_set.BIGUNION
(pred_set.IMAGE f (pred_set.INSERT x pred_set.EMPTY)) = f x

⊦ ∀instr c.
    prog.CODE_POOL instr c =
    pred_set.INSERT (pred_set.BIGUNION (pred_set.IMAGE instr c))
      pred_set.EMPTY

⊦ ∀m x s. set_sep.emp (state.SELECT_STATE m x s) ⇔ x = pred_set.EMPTY

⊦ ∀m d s. state.SELECT_STATE m d s = set_sep.fun2set (m s, d)

⊦ (∀p. set_sep.STAR p (set_sep.cond ⊤) = p) ∧
∀p. set_sep.STAR (set_sep.cond ⊤) p = p

⊦ q = pred_set.UNION p₁ p₂ ∧ pred_set.DISJOINT p₁ p₂ ⇒
set_sep.STAR (set_sep.SEP_EQ p₁) (set_sep.SEP_EQ p₂) = set_sep.SEP_EQ q

⊦ ∀f x y.
    pred_set.BIGUNION
      (pred_set.IMAGE f
         (pred_set.INSERT x (pred_set.INSERT y pred_set.EMPTY))) =
    pred_set.UNION (f x) (f y)

⊦ ∀m x y s t. state.FRAME_STATE m x s = state.FRAME_STATE m y t ⇒ x = y

⊦ ∀r next s t. state.NEXT_REL r next s t ⇔ ∃u. r s u ∧ next u = some t

⊦ ∀x p c q.
    temporal_state.TEMPORAL_NEXT x p c q ⇒
    ∀r.
      temporal_state.TEMPORAL_NEXT x (set_sep.STAR p r) c
        (set_sep.STAR q r)

⊦ ∀x p c q g.
temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c q ⇔
g ⇒ temporal_state.TEMPORAL_NEXT x p c q

⊦ ∀a b c.
    pred_set.DISJOINT a b ⇒
    set_sep.STAR (pred_set.INSERT (pred_set.UNION a b) pred_set.EMPTY) c =
    set_sep.STAR
      (set_sep.STAR (pred_set.INSERT a pred_set.EMPTY)
         (pred_set.INSERT b pred_set.EMPTY)) c

⊦ ∀x p c q g.
    temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c q ⇒
    temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c
      (set_sep.STAR q (set_sep.cond g))

⊦ ∀m s u v.
set_sep.SPLIT (state.STATE m s) (u, v) ⇔
∃y. u = state.SELECT_STATE m y s ∧ v = state.FRAME_STATE m y s

⊦ ∀x p c q.
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) p)
      pred_set.EMPTY
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) q) ⇔
    temporal_state.TEMPORAL_NEXT x p c q

⊦ ∀to_set next instr less avoid p c q.
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid) p c q ⇔
    temporal.TEMPORAL (to_set, next, instr, (=), const ⊥) c
      (temporal.T_IMPLIES (temporal.NOW p)
         (temporal.NEXT (temporal.NOW q)))

⊦ ∀to_set next instr less avoid p c q.
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid)
      (set_sep.STAR p (prog.CODE_POOL instr c)) pred_set.EMPTY
      (set_sep.STAR q (prog.CODE_POOL instr c)) ⇔
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid) p c q

⊦ ∀cd m p s x.
    set_sep.STAR (pred_set.INSERT cd pred_set.EMPTY) p
      (state.SELECT_STATE m x s) ⇔
    (∀c d. bool.IN (c, d) cd ⇒ m s c = d) ∧
    pred_set.SUBSET (pred_set.IMAGE fst cd) x ∧
    p (state.SELECT_STATE m (pred_set.DIFF x (pred_set.IMAGE fst cd)) s)

⊦ ∀m f u r.
    (∀b s a w. ¬(b = f a) ⇒ m (u s a w) b = m (r s) b) ⇒
    ∀a w s x.
      bool.IN (f a) x ⇒
      state.FRAME_STATE m x (u s a w) = state.FRAME_STATE m x (r s)

⊦ ∀m next instr p q.
    prog.SPEC (state.STATE m, next, instr, (=), const ⊥) p pred_set.EMPTY
      q ⇔
    ∀y s seq.
      p (state.SELECT_STATE m y s) ∧ prog.rel_sequence next seq s ⇒
      ∃k.
        q (state.SELECT_STATE m y (seq k)) ∧
        state.FRAME_STATE m y s = state.FRAME_STATE m y (seq k)

⊦ ∀m next instr less avoid p q.
    temporal_state.TEMPORAL_NEXT (state.STATE m, next, instr, less, avoid)
      p pred_set.EMPTY q ⇔
    ∀state y seq.
      p (state.SELECT_STATE m y (seq 0)) ∧
      prog.rel_sequence next seq state ⇒
      q (state.SELECT_STATE m y (seq 1)) ∧
      state.FRAME_STATE m y (seq 0) = state.FRAME_STATE m y (seq 1)

⊦ ∀m next instr c p q.
    (∀y s.
       set_sep.STAR p (prog.CODE_POOL instr c) (state.SELECT_STATE m y s) ⇒
       ∃v.
         next s = some v ∧
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y v) ∧
         state.FRAME_STATE m y s = state.FRAME_STATE m y v) ⇒
    prog.SPEC (state.STATE m, state.NEXT_REL (=) next, instr, (=), const ⊥)
      p c q

⊦ ∀m next instr less avoid c p q.
    (∀y s.
       set_sep.STAR p (prog.CODE_POOL instr c) (state.SELECT_STATE m y s) ⇒
       ∃v.
         next s = some v ∧
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y v) ∧
         state.FRAME_STATE m y s = state.FRAME_STATE m y v) ⇒
    temporal_state.TEMPORAL_NEXT
      (state.STATE m, state.NEXT_REL (=) next, instr, less, avoid) p c q

⊦ ∀m next instr r p q.
    prog.SPEC (state.STATE m, next, instr, r, const ⊥) p pred_set.EMPTY q ⇔
    ∀y s t₁ seq.
      p (state.SELECT_STATE m y t₁) ∧ r t₁ s ∧
      prog.rel_sequence next seq s ⇒
      ∃k t₂.
        q (state.SELECT_STATE m y t₂) ∧ r t₂ (seq k) ∧
        state.FRAME_STATE m y t₁ = state.FRAME_STATE m y t₂

⊦ ∀x prefix postfix p c q m i a l₁ l₂.
    length l₂ = length l₁ ∧
    prog.SPEC x (set_sep.STAR p (set_sep.SEP_ARRAY m i a l₁)) c
      (set_sep.STAR q (set_sep.SEP_ARRAY m i a l₂)) ⇒
    prog.SPEC x
      (set_sep.STAR p
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l₁) @ postfix))) c
      (set_sep.STAR q
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l₂) @ postfix)))

⊦ ∀x prefix postfix p c q m i a l₁ l₂.
    length l₂ = length l₁ ∧
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR p (set_sep.SEP_ARRAY m i a l₁)) c
      (set_sep.STAR q (set_sep.SEP_ARRAY m i a l₂)) ⇒
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR p
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l₁) @ postfix))) c
      (set_sep.STAR q
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l₂) @ postfix)))

⊦ ∀y x single_c map_c.
    (∀c d.
       single_c c d =
       pred_set.INSERT (pred_set.INSERT (x c, y d) pred_set.EMPTY)
         pred_set.EMPTY) ⇒
    (∀a b. x a = x b ⇔ a = b) ∧
    (∀df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc. (pred_set.BIGUNION (single_c c (f c)), bool.IN c df))))
         pred_set.EMPTY) ⇒
    ∀f df c d.
      bool.IN c df ⇒
      set_sep.STAR (single_c c d) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

⊦ ∀y x single_c map_c.
    (∀c d.
       single_c c d =
       pred_set.INSERT (pred_set.INSERT (x c, y d) pred_set.EMPTY)
         pred_set.EMPTY) ⇒
    (∀a b. x a = x b ⇔ a = b) ∧
    (∀df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc.
                  (pred_set.BIGUNION (single_c c (some (f c))),
                   bool.IN c df)))) pred_set.EMPTY) ⇒
    ∀f df c d.
      bool.IN c df ⇒
      set_sep.STAR (single_c c (some d)) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

⊦ ∀r m next instr c p q.
    relation.PreOrder r ⇒
    (∀y s t₁.
       set_sep.STAR p (prog.CODE_POOL instr c)
         (state.SELECT_STATE m y t₁) ∧ r t₁ s ⇒
       ∃v t₂.
         set_sep.STAR p (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y s) ∧ next s = some v ∧
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y t₂) ∧ r t₂ v ∧
         state.FRAME_STATE m y t₁ = state.FRAME_STATE m y t₂) ⇒
    prog.SPEC (state.STATE m, state.NEXT_REL r next, instr, r, const ⊥) p c
      q

⊦ ∀P n x y single_c map_c.
    (∀c d.
       single_c c d =
       pred_set.INSERT
         (list.LIST_TO_SET (list.GENLIST (λi. (x c i, y d i)) n))
         pred_set.EMPTY) ⇒
    (∀a b i j.
       P a ∧ P b ∧ i < n ∧ j < n ⇒ (x a i = x b j ⇔ a = b ∧ i = j)) ∧
    (∀df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc.
                  (pred_set.BIGUNION (single_c c (f c)),
                   bool.IN c df ∧ P c)))) pred_set.EMPTY) ⇒
    ∀f df c d.
      bool.IN c df ∧ P c ⇒
      set_sep.STAR (single_c c d) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

External Type Operators

→
bool
Data
- List
  - list
- Option
  - option
- Pair
  - ×
HOL4
- fcp
  - fcp.cart
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - length
- Option
  - some
- Pair
  - ,
  - fst
  - snd
Function
- const
- id
HOL4
- arithmetic
  - arithmetic.-
  - arithmetic.BIT2
- bool
  - bool.IN
  - bool.LET
- combin
  - combin.UPDATE
- list
  - list.GENLIST
  - list.GENLIST_AUX
  - list.LIST_TO_SET
- numeral
  - numeral.iSUB
  - numeral.iZ
- pair
  - pair.UNCURRY
- pred_set
  - pred_set.BIGUNION
  - pred_set.COMPL
  - pred_set.DELETE
  - pred_set.DIFF
  - pred_set.DISJOINT
  - pred_set.EMPTY
  - pred_set.GSPEC
  - pred_set.IMAGE
  - pred_set.INSERT
  - pred_set.INTER
  - pred_set.SUBSET
  - pred_set.UNION
  - pred_set.UNIV
- prim_rec
  - prim_rec.PRE
- prog
  - prog.rel_sequence
  - prog.CODE_POOL
  - prog.RUN
  - prog.SEP_REFINE
  - prog.SPEC
- relation
  - relation.PreOrder
- set_sep
  - set_sep.cond
  - set_sep.emp
  - set_sep.fun2set
  - set_sep.SEP_ARRAY
  - set_sep.SEP_DISJ
  - set_sep.SEP_EQ
  - set_sep.SEP_EXISTS
  - set_sep.SEP_F
  - set_sep.SPLIT
  - set_sep.STAR
- temporal
  - temporal.NEXT
  - temporal.NOW
  - temporal.TEMPORAL
  - temporal.T_IMPLIES
- words
  - words.n2w
  - words.word_2comp
  - words.word_add
  - words.word_mul
  - words.word_sub
Number
- Natural
  - *
  - +
  - <
  - ≤
  - >
  - ≥
  - ↑
  - bit1
  - even
  - odd
  - suc
  - zero
Relation
- reflexive
- transitive

Assumptions

⊦ ⊤

⊦ pred_set.BIGUNION pred_set.EMPTY = pred_set.EMPTY

⊦ ∀x. x = x

⊦ ∀x. bool.IN x pred_set.UNIV

⊦ ∀t. ⊥ ⇒ t

⊦ ∀n. 0 ≤ n

⊦ bool.IN = λx f. f x

⊦ ¬¬p ⇒ p

⊦ ∀x. ¬bool.IN x pred_set.EMPTY

⊦ ∀x. id x = x

⊦ ∀s. set_sep.SEP_F s ⇔ ⊥

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λt. t ⇒ ⊥

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

⊦ set_sep.emp = λs. s = pred_set.EMPTY

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

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

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

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. x = x ⇔ ⊤

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀f. pred_set.IMAGE f pred_set.EMPTY = pred_set.EMPTY

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ¬(p ∨ q) ⇒ ¬p

⊦ ¬(p ∨ q) ⇒ ¬q

⊦ ∀A. A ⇒ ¬A ⇒ ⊥

⊦ ∀t. ¬t ⇒ t ⇒ ⊥

⊦ ∀x. pred_set.BIGUNION (pred_set.INSERT x pred_set.EMPTY) = x

⊦ ∀x y. const x y = x

⊦ ∀x. set_sep.SEP_EQ x = λs. s = 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)

⊦ ∀R. reflexive R ⇔ ∀x. R x x

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

⊦ ∀R. relation.PreOrder R ⇔ reflexive R ∧ transitive R

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

⊦ ∀A B. A ∨ B ⇔ B ∨ A

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

⊦ ∀v w. words.word_add v w = words.word_add w v

⊦ ∀v w. words.word_mul v w = words.word_mul w v

⊦ ∀x y. set_sep.STAR x y = set_sep.STAR y x

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

⊦ ∀w.
words.word_2comp w = words.word_mul (words.word_2comp (words.n2w 1)) w

⊦ ∀x y. pred_set.INSERT y pred_set.EMPTY x ⇔ x = y

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

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

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

⊦ ∀v w. words.word_sub v w = words.word_add v (words.word_2comp w)

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

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

⊦ ∀x. prog.RUN x p q ⇔ prog.SPEC x p pred_set.EMPTY q

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

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

⊦ ∀x s. bool.IN x (pred_set.COMPL s) ⇔ ¬bool.IN x s

⊦ ∀s t. pred_set.DISJOINT s t ⇔ pred_set.INTER s t = pred_set.EMPTY

⊦ ∀s P.
pred_set.BIGUNION (pred_set.INSERT s P) =
pred_set.UNION s (pred_set.BIGUNION P)

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

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

⊦ ∀f v. (∀x. x = v ⇒ f x) ⇔ f v

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

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

⊦ ∀instr c.
prog.CODE_POOL instr c =
λs. s = pred_set.BIGUNION (pred_set.IMAGE instr c)

⊦ ∀p f seq. temporal.NOW p f seq ⇔ f p (seq 0)

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

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

⊦ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m

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

⊦ 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 []

⊦ (∀s. pred_set.UNION pred_set.EMPTY s = s) ∧
∀s. pred_set.UNION s pred_set.EMPTY = s

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

⊦ ∀P Q. (∀x. P ∨ Q x) ⇔ P ∨ ∀x. Q x

⊦ ∀Q P. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q

⊦ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x

⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q

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

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

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

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

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

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

⊦ ∀s t. s = t ⇔ ∀x. bool.IN x s ⇔ bool.IN x t

⊦ ∀s t. pred_set.SUBSET s t ⇔ ∀x. bool.IN x s ⇒ bool.IN x t

⊦ ∀v w x.
words.word_add v (words.word_add w x) =
words.word_add (words.word_add v w) x

⊦ ∀f v. bool.IN v (pred_set.GSPEC f) ⇔ ∃x. (v, ⊤) = f x

⊦ ∀p q r.
set_sep.STAR p (set_sep.STAR q r) = set_sep.STAR (set_sep.STAR p q) r

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

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

⊦ ∀n m. arithmetic.- n m = if m < n then numeral.iSUB ⊤ n m else 0

⊦ (∀w. words.word_add w (words.n2w 0) = w) ∧
∀w. words.word_add (words.n2w 0) w = w

⊦ ∀x sos.
bool.IN x (pred_set.BIGUNION sos) ⇔ ∃s. bool.IN x s ∧ bool.IN s sos

⊦ ∀f x s.
pred_set.IMAGE f (pred_set.INSERT x s) =
pred_set.INSERT (f x) (pred_set.IMAGE f s)

⊦ 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

⊦ ∀p f seq. temporal.NEXT p f seq = p f (λn. seq (n + 1))

⊦ ∀x y s. bool.IN x (pred_set.INSERT y s) ⇔ x = y ∨ bool.IN x s

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

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

⊦ ∀s t x. bool.IN x (pred_set.INTER s t) ⇔ bool.IN x s ∧ bool.IN x t

⊦ ∀s t x. bool.IN x (pred_set.UNION s t) ⇔ bool.IN x s ∨ bool.IN x t

⊦ ∀f d.
set_sep.fun2set (f, d) = pred_set.GSPEC (λa. ((a, f a), bool.IN a d))

⊦ ∀v w x.
words.word_mul (words.word_add v w) x =
words.word_add (words.word_mul v x) (words.word_mul w 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

⊦ ∀s x y. bool.IN x (pred_set.DELETE s y) ⇔ bool.IN x s ∧ ¬(x = y)

⊦ ∀s t x. bool.IN x (pred_set.DIFF s t) ⇔ bool.IN x s ∧ ¬bool.IN x t

⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

⊦ ∀p s t.
set_sep.STAR (set_sep.SEP_EQ t) p s ⇔
p (pred_set.DIFF s t) ∧ pred_set.SUBSET t s

⊦ ∀f a b c. combin.UPDATE a b f c = if a = c then b else f c

⊦ ∀p q f seq. temporal.T_IMPLIES p q f seq ⇔ p f seq ⇒ q f seq

⊦ ∀s u v.
set_sep.SPLIT s (u, v) ⇔ pred_set.UNION u v = s ∧ pred_set.DISJOINT u v

⊦ ∀y s f. bool.IN y (pred_set.IMAGE f s) ⇔ ∃x. y = f x ∧ bool.IN x s

⊦ ∀R. transitive R ⇔ ∀x y z. R x y ∧ R y z ⇒ R x z

⊦ ∀p less to_set state.
prog.SEP_REFINE p less to_set state ⇔ ∃s. less s state ∧ p (to_set s)

⊦ ∀p q. set_sep.STAR p q = λs. ∃u v. set_sep.SPLIT s (u, v) ∧ p u ∧ q v

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

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

⊦ ∀x p c q.
prog.SPEC x p c q ⇒
∀r. prog.SPEC x (set_sep.STAR p r) c (set_sep.STAR q r)

⊦ ∀a y h dh.
bool.IN (a, y) (set_sep.fun2set (h, dh)) ⇔ h a = y ∧ bool.IN a dh

⊦ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')

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

⊦ ∀A B. (¬(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 ⇔ t)

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

⊦ ∀x p c q.
    prog.SPEC x (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) p)
      pred_set.EMPTY
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) q) ⇔
    prog.SPEC x p c q

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

⊦ ∀s t u.
    (pred_set.DISJOINT (pred_set.UNION s t) u ⇔
     pred_set.DISJOINT s u ∧ pred_set.DISJOINT t u) ∧
    (pred_set.DISJOINT u (pred_set.UNION s t) ⇔
     pred_set.DISJOINT s u ∧ pred_set.DISJOINT t u)

⊦ ∀xs ys p i a.
    set_sep.SEP_ARRAY p i a (xs @ ys) =
    set_sep.STAR (set_sep.SEP_ARRAY p i a xs)
      (set_sep.SEP_ARRAY p i
         (words.word_add a (words.word_mul (words.n2w (length xs)) i)) ys)

⊦ ∀R seq state.
    prog.rel_sequence R seq state ⇔
    seq 0 = state ∧
    ∀n.
      if (∃x. R (seq n) x) then R (seq n) (seq (suc n))
      else seq (suc n) = seq n

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

⊦ (∀m n.
     words.word_add (words.word_2comp (words.n2w m))
       (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m + n))) ∧
  ∀m n.
    words.word_add (words.n2w m) (words.word_2comp (words.n2w n)) =
    if n ≤ m then words.n2w (arithmetic.- m n)
    else words.word_2comp (words.n2w (arithmetic.- n m))

⊦ ∀P Q.
((∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q) ∧ ((∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q) ∧
(Q ∧ (∃x. P x) ⇔ ∃x. Q ∧ P x)

⊦ (p ⇔ if q then r else s) ⇔
(p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧
(q ∨ s ∨ ¬p)

⊦ ∀f.
(∀x y z. f x (f y z) = f (f x y) z) ⇒ (∀x y. f x y = f y x) ⇒
∀x y z. f x (f y z) = f y (f x z)

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

⊦ ∀to_set next instr less allow c exp.
    temporal.TEMPORAL (to_set, next, instr, less, allow) c exp ⇔
    ∀state seq r.
      prog.rel_sequence next seq state ⇒
      bool.LET (λf. exp f seq)
        (λp state.
           prog.SEP_REFINE
             (set_sep.STAR (set_sep.STAR p (prog.CODE_POOL instr c)) r)
             less to_set state ∨ allow state)

⊦ (∀f l. list.GENLIST_AUX f 0 l = l) ∧
  (∀f n l.
     list.GENLIST_AUX f (bit1 n) l =
     list.GENLIST_AUX f (arithmetic.- (bit1 n) 1)
       (f (arithmetic.- (bit1 n) 1) :: l)) ∧
  ∀f n l.
    list.GENLIST_AUX f (arithmetic.BIT2 n) l =
    list.GENLIST_AUX f (bit1 n) (f (bit1 n) :: l)

⊦ ∀to_set next instr less allow p q.
    prog.RUN (to_set, next, instr, less, allow) p q ⇔
    ∀state r.
      prog.SEP_REFINE (set_sep.STAR p r) less to_set state ∨ allow state ⇒
      ∀seq.
        prog.rel_sequence next seq state ⇒
        ∃i.
          prog.SEP_REFINE (set_sep.STAR q r) less to_set (seq i) ∨
          allow (seq i)

⊦ ∀v w.
    words.word_mul (words.n2w 0) v = words.n2w 0 ∧
    words.word_mul v (words.n2w 0) = words.n2w 0 ∧
    words.word_mul (words.n2w 1) v = v ∧
    words.word_mul v (words.n2w 1) = v ∧
    words.word_mul (words.word_add v (words.n2w 1)) w =
    words.word_add (words.word_mul v w) w ∧
    words.word_mul v (words.word_add w (words.n2w 1)) =
    words.word_add v (words.word_mul v w)

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

⊦ ∀p q t c c'.
    set_sep.STAR (set_sep.SEP_EXISTS (λv. p v)) q =
    set_sep.SEP_EXISTS (λv. set_sep.STAR (p v) q) ∧
    set_sep.STAR q (set_sep.SEP_EXISTS (λv. p v)) =
    set_sep.SEP_EXISTS (λv. set_sep.STAR q (p v)) ∧
    set_sep.SEP_DISJ (set_sep.SEP_EXISTS (λv. p v)) q =
    set_sep.SEP_EXISTS (λv. set_sep.SEP_DISJ (p v) q) ∧
    set_sep.SEP_DISJ q (set_sep.SEP_EXISTS (λv. p v)) =
    set_sep.SEP_EXISTS (λv. set_sep.SEP_DISJ q (p v)) ∧
    set_sep.SEP_EXISTS (λv. q) = q ∧
    set_sep.SEP_EXISTS (λv. set_sep.STAR (p v) (set_sep.cond (v = x))) =
    p x ∧ set_sep.SEP_DISJ q set_sep.SEP_F = q ∧
    set_sep.SEP_DISJ set_sep.SEP_F q = q ∧
    set_sep.STAR set_sep.SEP_F q = set_sep.SEP_F ∧
    set_sep.STAR q set_sep.SEP_F = set_sep.SEP_F ∧
    set_sep.SEP_DISJ r r = r ∧
    set_sep.STAR q (set_sep.SEP_DISJ r t) =
    set_sep.SEP_DISJ (set_sep.STAR q r) (set_sep.STAR q t) ∧
    set_sep.STAR (set_sep.SEP_DISJ r t) q =
    set_sep.SEP_DISJ (set_sep.STAR r q) (set_sep.STAR t q) ∧
    set_sep.SEP_DISJ (set_sep.cond c) (set_sep.cond c') =
    set_sep.cond (c ∨ c') ∧
    set_sep.STAR (set_sep.cond c) (set_sep.cond c') =
    set_sep.cond (c ∧ c') ∧ set_sep.cond ⊤ = set_sep.emp ∧
    set_sep.cond ⊥ = set_sep.SEP_F ∧ set_sep.STAR set_sep.emp q = q ∧
    set_sep.STAR q set_sep.emp = q

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