Theory DivLogic

section "A Hoare logic for diverging programs"

theory DivLogic
  imports WhileLang StdLogic CoinductiveLemmas
begin

definition ignores_output :: "(val  state  bool)  bool" where
  "ignores_output H  i s out1 out2. H i (s,out1) = H i (s,out2)"

inductive pohjola where
  p_seq_d: "pohjola P p (D::val llist  bool)  pohjola P (Seq p q) D"
| p_seq_h: "hoare P p M  pohjola M q D  pohjola P (Seq p q) D"
| p_if: "pohjola (λs. P s   guard x s) p D 
   pohjola (λs. P s  ~guard x s) q D  pohjola P (If x p q) D"
| (* proving that a non-terminating loop diverges *)
  p_while1: "(s. P s 
         (H ev.
           guard x s  H 0 s  ignores_output H 
           D (flat (LCons (output_of s) (inf_llist ev))) 
           (i. hoare (λs. H i s  output_of s = []) p
                     (λs. H (i+1) s  output_of s = ev i  guard x s)))) 
    pohjola P (While x p) D"
| (* proving that the ith execution of the body of a loop causes
     something within the body to diverge *)
  p_while2: "(s. P s  guard x s)  wfP R 
   (s0. hoare (λs. P s  b s  s = s0) p (λs. P s  R s s0)) 
    pohjola (λs. P s  ~b s) p D  pohjola P (While x p) D"
| p_const: "pohjola (λs. False) p D"
| p_case: "pohjola (λs. P s  b s) p D  pohjola (λs. P s  ~b s) p D  pohjola P p D"
| p_weaken: "(s. P s  P' s)  pohjola P' p D'  (s. D' s  D s)  pohjola P p D"
print_theorems

(* -- semantics -- *)

definition pohjola_sem where
  "pohjola_sem P p D 
    s. P s  (l. diverges s p l  D l)"

end