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

Information

namemachine-code-hoare-triple
version1.0
descriptionTotal correctness machine-code Hoare triple
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksumc28e88ba1dbcdb694ad359172be6e1af6da9c58a
requiresbase
hol-base
machine-code-hoare-logic
showData.Bool

Files

Defined Constants

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)

f1 f2 x.
    HOL4.triple.case_sum f1 f2 x =
    HOL4.sum.sum_CASE x (λy. f1 y) (λy'. f2 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

(x1 f (g x2)) (¬x1 f (g y2)) f (g (if x1 then x2 else y2))

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%%644 p c m q.
    HOL4.triple.TRIPLE %%genvar%%644 m c q
    HOL4.triple.TRIPLE %%genvar%%644 p c m
    HOL4.triple.TRIPLE %%genvar%%644 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 (c1, pre) code (c2, post)
    c. HOL4.triple.TRIPLE i (c c1, pre) code (c c2, 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

External Constants

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_1 p_2. P (p_1, p_2)

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

() = λt1 t2. t. (t1 t) (t2 t) t

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

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

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

¬(A B) (A ) ¬B

t1 t2 t3. t1 t2 t3 t1 t2 t3

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

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

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 f1. HOL4.sum.sum_CASE (Data.Sum.left x) f f1 = f x)
  y f f1. HOL4.sum.sum_CASE (Data.Sum.right y) f f1 = f1 y

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

x p c1 m c2 q.
    HOL4.prog.SPEC x p c1 m HOL4.prog.SPEC x m c2 q
    HOL4.prog.SPEC x p (HOL4.pred_set.UNION c1 c2) 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)