Theory "while"

Signature

Definitions

WHILE

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

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

OLEAST_def

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

LEAST_DEF

⊢ ∀P. $LEAST P = WHILE ($~ ∘ P) SUC 0

HOARE_SPEC_DEF

⊢ ∀P C Q. HOARE_SPEC P C Q ⇔ ∀s. P s ⇒ Q (C s)

Theorems

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)

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

OWHILE_WHILE

⊢ (OWHILE G f s = SOME s') ⇒ (WHILE G f s = s')

OWHILE_THM

⊢ OWHILE G f s = if G s then OWHILE G f (f s) else SOME 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

OWHILE_EQ_NONE

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

OWHILE_ENDCOND

⊢ (OWHILE G f s = SOME s') ⇒ ¬G s'

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)

OLEAST_EQ_SOME

⊢ ($OLEAST P = SOME n) ⇔ P n ∧ ∀m. m < n ⇒ ¬P m

OLEAST_EQ_NONE

⊢ ($OLEAST P = NONE) ⇔ ∀n. ¬P n

LESS_LEAST

⊢ ∀P m. m < $LEAST P ⇒ ¬P m

LEAST_T

⊢ (LEAST x. T) = 0

LEAST_LESS_EQ

⊢ (LEAST x. y ≤ x) = y

LEAST_INTRO

⊢ ∀P x. P x ⇒ P ($LEAST P)

LEAST_EXISTS_IMP

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

LEAST_EXISTS

⊢ ∀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_ELIM

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

ITERATION

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

FULL_LEAST_INTRO

⊢ ∀x. P x ⇒ P ($LEAST P) ∧ $LEAST P ≤ x