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