Package machine-code-hoare-triple: Total correctness machine-code Hoare triple

Information

name	machine-code-hoare-triple
version	1.0
description	Total correctness machine-code Hoare triple
author	HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
license	MIT
checksum	c28e88ba1dbcdb694ad359172be6e1af6da9c58a
requires	base hol-base machine-code-hoare-logic
show	Data.Bool

Files

Package tarball machine-code-hoare-triple-1.0.tgz
Theory source file machine-code-hoare-triple.thy (included in the package tarball)

Defined Constants

HOL4
- triple
  - HOL4.triple.case_sum
  - HOL4.triple.SHORT_TERM_TAILREC
  - HOL4.triple.TERM_TAILREC
  - HOL4.triple.TRIPLE

Theorems

⊦ ∀i c p. HOL4.triple.TRIPLE i p c p

⊦ ∀f.
    HOL4.triple.SHORT_TERM_TAILREC f =
    HOL4.triple.TERM_TAILREC (Function.∘ Data.Sum.destLeft f)
      (Function.∘ Data.Sum.isLeft f) (Function.∘ Data.Sum.destRight f)

⊦ ∀f₁ f₂ x.
HOL4.triple.case_sum f₁ f₂ x =
HOL4.sum.sum_CASE x (λy. f₁ y) (λy'. f₂ y')

⊦ HOL4.triple.TERM_TAILREC f g d x =
if g x then HOL4.triple.TERM_TAILREC f g d (f x) else d x

⊦ (x₁ ⇒ f (g x₂)) ∧ (¬x₁ ⇒ f (g y₂)) ⇒ f (g (if x₁ then x₂ else y₂))

⊦ ∀i p c q c'.
HOL4.triple.TRIPLE i p c q ⇒ HOL4.pred_set.SUBSET c c' ⇒
HOL4.triple.TRIPLE i p c' q

⊦ ∀%%genvar%%₆₄₄ p c m q.
    HOL4.triple.TRIPLE %%genvar%%₆₄₄ m c q ⇒
    HOL4.triple.TRIPLE %%genvar%%₆₄₄ p c m ⇒
    HOL4.triple.TRIPLE %%genvar%%₆₄₄ p c q

⊦ ∀i p c m q.
HOL4.triple.TRIPLE i p c m ∧ HOL4.triple.TRIPLE i m c q ⇒
HOL4.triple.TRIPLE i p c q

⊦ ∀i.
HOL4.triple.TRIPLE i (c₁, pre) code (c₂, post) ⇒
∀c. HOL4.triple.TRIPLE i (c ∧ c₁, pre) code (c ∧ c₂, post)

⊦ ∀M.
    (side ⇒
     HOL4.prog.SPEC (Data.Pair.snd M) (Data.Pair.fst M pre) code
       (Data.Pair.fst M post)) ⇒
    ∀c. HOL4.triple.TRIPLE M (c, pre) code (c ∧ side, post)

⊦ ∀assert model pre code post.
    HOL4.triple.TRIPLE (assert, model) pre code post ⇔
    Data.Pair.fst post ⇒
    Data.Pair.fst pre ∧
    HOL4.prog.SPEC model (assert (Data.Pair.snd pre)) code
      (assert (Data.Pair.snd post))

⊦ ∀f g d x.
    HOL4.triple.TERM_TAILREC f g d x =
    HOL4.bool.LET
      (HOL4.pair.UNCURRY
         (λcond y. (cond ∧ (∃n. ¬g (HOL4.arithmetic.FUNPOW f n x)), y)))
      (d (HOL4.while.WHILE g f x))

⊦ (∀x.
     HOL4.triple.TRIPLE i (pre x) c
       (HOL4.triple.case_sum pre post (f x))) ⇒
  (∀c x state. ¬Data.Pair.fst (post (⊥, x))) ⇒
  ∀x.
    HOL4.triple.TRIPLE i (pre x) c
      (post (HOL4.triple.SHORT_TERM_TAILREC f x))

External Type Operators

→
bool
Data
- Pair
  - Data.Pair.×
- Sum
  - Data.Sum.+
Number
- Natural
  - Number.Natural.natural

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- Pair
  - Data.Pair.,
  - Data.Pair.fst
  - Data.Pair.snd
- Sum
  - Data.Sum.destLeft
  - Data.Sum.destRight
  - Data.Sum.isLeft
  - Data.Sum.left
  - Data.Sum.right
Function
- Function.id
- Function.∘
HOL4
- arithmetic
  - HOL4.arithmetic.FUNPOW
- bool
  - HOL4.bool.LET
- pair
  - HOL4.pair.UNCURRY
- pred_set
  - HOL4.pred_set.SUBSET
  - HOL4.pred_set.UNION
- prog
  - HOL4.prog.SPEC
- sum
  - HOL4.sum.sum_CASE
- while
  - HOL4.while.WHILE
Number
- Natural
  - Number.Natural.suc
  - Number.Natural.zero

Assumptions

⊦ ⊤

⊦ ∀t. ⊥ ⇒ t

⊦ ¬¬p ⇒ p

⊦ ∀x. Function.id x = x

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λt. t ⇒ ⊥

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

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

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

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

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. Data.Sum.destLeft (Data.Sum.left x) = x

⊦ ∀x. x = x ⇔ ⊤

⊦ ∀x. Data.Sum.destRight (Data.Sum.right x) = x

⊦ ∀s. HOL4.pred_set.UNION s s = s

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ¬(p ∨ q) ⇒ ¬p

⊦ ¬(p ∨ q) ⇒ ¬q

⊦ ∀A. A ⇒ ¬A ⇒ ⊥

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

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

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

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

⊦ ∀f x. HOL4.bool.LET f x = f x

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

⊦ ∀x p c. HOL4.prog.SPEC x p c p

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

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

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

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

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

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

⊦ (∀x. Data.Sum.isLeft (Data.Sum.left x)) ∧
∀y. ¬Data.Sum.isLeft (Data.Sum.right y)

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

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

⊦ (∀p. P p) ⇔ ∀p_₁ p_₂. P (p_₁, p_₂)

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

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

⊦ ∀ss. (∃x. ss = Data.Sum.left x) ∨ ∃y. ss = Data.Sum.right y

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

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

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

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

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

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

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

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

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

⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (Number.Natural.suc n)) ⇒ ∀n. P n

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

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

⊦ ∀P g x.
HOL4.while.WHILE P g x = if P x then HOL4.while.WHILE P g (g x) else x

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

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

⊦ ∀x p c q.
HOL4.prog.SPEC x p c q ⇒
∀c'. HOL4.pred_set.SUBSET c c' ⇒ HOL4.prog.SPEC x p c' q

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

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

⊦ (∀x f f₁. HOL4.sum.sum_CASE (Data.Sum.left x) f f₁ = f x) ∧
∀y f f₁. HOL4.sum.sum_CASE (Data.Sum.right y) f f₁ = f₁ y

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

⊦ ∀x p c₁ m c₂ q.
HOL4.prog.SPEC x p c₁ m ∧ HOL4.prog.SPEC x m c₂ q ⇒
HOL4.prog.SPEC x p (HOL4.pred_set.UNION c₁ c₂) q

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

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

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