# 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```