Theory While

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

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

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

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

⊢ ∀f k x. TAILCALL f k x = case f x of INL cv => k cv | INR tv => tv

⊢ ∀f x. TAILREC f x = case f x of INL z => TAILREC f z | INR y => y

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

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

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

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

⊢ (LEAST n. n = x) = x ∧ (LEAST n. x = n) = x

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

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

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

⊢ (LEAST x. y ≤ x) = y

⊢ (LEAST x. T) = 0

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

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

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

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

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

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

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

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

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

⊢ OWHILE G f s = if G s then OWHILE G f (f s) else SOME s

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

⊢ (∀x y. P x ∧ c x = INL y ⇒ P y) ∧
  (∀x. P x ⇒ ∃R. WFP R x ∧ ∀y z. P y ∧ R꙳ y x ∧ c y = INL z ⇒ R z y) ∧
  (∀x. P x ⇒ f x = TAILCALL c f x) ⇒
  ∀x. P x ⇒ f x = TAILREC c x

⊢ WF R ∧ (∀x y. P x ∧ c x = INL y ⇒ P y) ∧
  (∀x y. P x ∧ c x = INL y ⇒ R y x) ∧ (∀x. P x ⇒ f x = TAILCALL c f x) ⇒
  ∀x. P x ⇒ f x = TAILREC c x

⊢ TAILREC f x = TAILCALL f (TAILREC f) x

⊢ (∃n. ¬P (FUNPOW f n s)) ⇒
  WHILE P f s = FUNPOW f (LEAST n. ¬P (FUNPOW f n s)) s

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

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