Theory "while"

Signature

Definitions

WHILE

|- ∀P g x. WHILE P g x = if P x then WHILE P g (g x) else x

HOARE_SPEC_DEF

|- ∀P C Q. HOARE_SPEC P C Q ⇔ ∀s. P s ⇒ Q (C s)

LEAST_DEF

|- ∀P. $LEAST P = WHILE ($~ o P) SUC 0

OLEAST_def

|- ∀P. $OLEAST P = if ∃n. P n then SOME (LEAST n. P n) else NONE

OWHILE_def

|- ∀G f s.
     OWHILE G f s =
     if ∃n. ¬G (FUNPOW f n s) then
       SOME (FUNPOW f (LEAST n. ¬G (FUNPOW f n s)) s)
     else NONE

Theorems

ITERATION

|- ∀P g. ∃f. ∀x. f x = if P x then x else f (g x)

WHILE_INDUCTION

|- ∀B C R.
     WF R ∧ (∀s. B s ⇒ R (C s) s) ⇒ ∀P. (∀s. (B s ⇒ P (C s)) ⇒ P s) ⇒ ∀v. P v

WHILE_RULE

|- ∀R B C.
     WF R ∧ (∀s. B s ⇒ R (C s) s) ⇒
     HOARE_SPEC (λs. P s ∧ B s) C P ⇒
     HOARE_SPEC P (WHILE B C) (λs. P s ∧ ¬B s)

LEAST_INTRO

|- ∀P x. P x ⇒ P ($LEAST P)

LESS_LEAST

|- ∀P m. m < $LEAST P ⇒ ¬P m

FULL_LEAST_INTRO

|- ∀x. P x ⇒ P ($LEAST P) ∧ $LEAST P ≤ x

LEAST_ELIM

|- ∀Q P. (∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q ($LEAST P)

LEAST_EXISTS

|- ∀p. (∃n. p n) ⇔ p ($LEAST p) ∧ ∀n. n < $LEAST p ⇒ ¬p n

LEAST_EXISTS_IMP

|- ∀p. (∃n. p n) ⇒ p ($LEAST p) ∧ ∀n. n < $LEAST p ⇒ ¬p n

LEAST_EQ

|- ((LEAST n. n = x) = x) ∧ ((LEAST n. x = n) = x)

LEAST_T

|- (LEAST x. T) = 0

OLEAST_INTRO

|- ((∀n. ¬P n) ⇒ Q NONE) ∧ (∀n. P n ∧ (∀m. m < n ⇒ ¬P m) ⇒ Q (SOME n)) ⇒
   Q ($OLEAST P)

OLEAST_EQNS

|- ((OLEAST n. n = x) = SOME x) ∧ ((OLEAST n. x = n) = SOME x) ∧
   ((OLEAST n. F) = NONE) ∧ ((OLEAST n. T) = SOME 0)

OWHILE_THM

|- OWHILE G f s = if G s then OWHILE G f (f s) else SOME s

OWHILE_EQ_NONE

|- (OWHILE G f s = NONE) ⇔ ∀n. G (FUNPOW f n s)

OWHILE_ENDCOND

|- (OWHILE G f s = SOME s') ⇒ ¬G s'

OWHILE_WHILE

|- (OWHILE G f s = SOME s') ⇒ (WHILE G f s = s')

OWHILE_INV_IND

|- ∀G f s.
     P s ∧ (∀x. P x ∧ G x ⇒ P (f x)) ⇒ ∀s'. (OWHILE G f s = SOME s') ⇒ P s'

OWHILE_IND

|- ∀P G f.
     (∀s. ¬G s ⇒ P s s) ∧ (∀s1 s2. G s1 ∧ P (f s1) s2 ⇒ P s1 s2) ⇒
     ∀s1 s2. (OWHILE G f s1 = SOME s2) ⇒ P s1 s2