Theory "while"

Parents     arithmetic

Signature

Constant Type
WHILE :('a -> bool) -> ('a -> 'a) -> 'a -> 'a
LEAST :(num -> bool) -> num
HOARE_SPEC :('a -> bool) -> ('a -> 'b) -> ('b -> bool) -> bool

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

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