# Theory DivLogicCompleteness

```section "Completeness of Hoare logic for diverging programs"

theory DivLogicCompleteness
imports DivLogic StdLogicCompleteness StdLogicSoundness
begin

declare pohjola.intros[intro, simp]
declare pohjola.intros(7)[simp del]
declare pohjola.intros(7)[rule del]
declare pohjola.intros(6)[rule del]

theorem pohjola_strengthen:
"⟦pohjola P' p D;  ∀s. P s ⟶ P' s⟧ ⟹ pohjola P p D"
by blast

inductive div_at_iteration where
"guard f s ⟹ diverges s c l ⟹ D l ⟹ div_at_iteration 0 s f c D"
| "guard f s ⟹ terminates s c t ⟹ div_at_iteration n t f c D ⟹
div_at_iteration (Suc n) s f c D"
print_theorems

inductive_cases
div_at_0 [elim!]:   "div_at_iteration 0 s f c D" and
div_at_S [elim!]: "div_at_iteration (Suc n) s f c D"
print_theorems

theorem div_at_iteration_11:
"div_at_iteration i s f c D ⟹
div_at_iteration j s f c D ⟹ i = j"
apply (induct arbitrary: j rule: div_at_iteration.induct)
apply (erule div_at_iteration.cases; simp)
apply (erule diverges.cases; clarsimp)
apply (rotate_tac -1)
apply (erule div_at_iteration.cases)
apply (erule diverges.cases, blast)
apply safe
apply (drule (1) terminates_deterministic)
apply clarsimp
done

lemma star_n_While_flatten:
"star_n (λs t. star step (While x p, s) (While x p, t)
∧ terminates s p t ∧ guard x s) i s t
⟹ ∃n'. star_n step n' (While x p, s) (While x p, t) ∧ n' ≥ i"
apply (induct arbitrary: s t rule: nat_less_induct)
apply (rename_tac n s t)
apply (clarsimp simp: star_eq_star_n)
apply (case_tac n; simp)
apply clarsimp
apply (erule star_n.cases; clarsimp)
apply fastforce
apply clarsimp
apply (erule star_n.cases; clarsimp)
apply (rename_tac ac bc n ad bd na)
apply (drule_tac x=n in spec)
apply clarsimp
apply (drule_tac x=ac and y=bc in spec2)
apply (drule_tac x=ad and y=bd in spec2)
apply simp
apply clarsimp
apply (clarsimp simp: terminates star_eq_star_n)
apply (rename_tac n' nb)
apply (thin_tac "star_n _ na _ _")
apply (frule (1) star_n_trans)
apply (rule_tac x="nb + 3 + n'" in exI)
apply fastforce
done

lemma diverges_init_state:
"⟦terminates s c t; diverges t (While g c) l; guard g s⟧ ⟹ diverges s (While g c) l"
apply (simp (no_asm) add: diverges_While diverges_If)
apply clarsimp
apply (rule disjI2)
apply (rule_tac x="fst t" in exI, rule_tac x="snd t" in exI)
by fastforce

lemma diverges_init_state_n:
"⟦star_n (λs t. terminates s c t ∧ guard g s) n s t; diverges t (While g c) l; guard g t⟧
⟹ diverges s (While g c) l"
apply (induct n arbitrary: s t)
apply (erule star_n.cases, clarsimp)
apply (clarsimp simp: terminates)
apply (erule star_n.cases; clarsimp)
apply (rename_tac a b a' b' n a'' b'')
apply (drule_tac x=a' and y=b' in meta_spec2)
apply (drule_tac x=a'' and y=b'' in meta_spec2)
apply clarsimp
apply (frule diverges_init_state; simp?)
done

lemma div_at_i_unwind:
"div_at_iteration i s g c D
⟷ (∃t. star_n (λs t. terminates s c t ∧ guard g s) i s t ∧ guard g t
∧ (∃l. diverges t c l ∧ D l))"
apply (rule iffI)
apply (induct i arbitrary: s)
apply fastforce
apply clarsimp
apply (rename_tac a' b')
apply (drule_tac x=a' and y=b' in meta_spec2)
apply fastforce
apply clarsimp
apply (induct i arbitrary: s)
apply (erule star_n.cases; simp)
apply (rule div_at_iteration.intros(1); simp)
apply (erule star_n.cases; simp)
apply clarsimp
apply (rename_tac l a b a' b' n a'' b'')
apply (rule div_at_iteration.intros(2); simp?)
apply (drule_tac x=a'' and y=b'' in meta_spec2)
apply (drule_tac x=l in meta_spec)
apply (drule_tac x=a' and y=b' in meta_spec2)
apply clarsimp
done

lemma diverging_body_diverges:
"⟦diverges s c l; guard g s⟧ ⟹ diverges s (While g c) l"
done

lemma non_diverging_inf_loop:
"⟦∀i. ¬ div_at_iteration i s g c D; diverges s (While g c) l; D l⟧
⟹ ∀i. ∃t. star_n (λs t. (∃k. star_n step k (While g c, s) (While g c, t))
∧ terminates s c t ∧ guard g s) i s t"
apply clarsimp
apply (case_tac "guard g s"; simp)
apply (erule disjE)
apply (fastforce intro!: div_at_iteration.intros)
apply clarsimp
apply (rule nat.induct)
apply (cases s; blast)
apply clarsimp
apply (rename_tac a b n a' b')
apply (subgoal_tac "guard g (a', b')")
prefer 2
apply (rule ccontr)
apply (frule star_n_While_flatten[simplified star_eq_star_n])
apply clarsimp
apply (subgoal_tac "star_n step (Suc (Suc 0)) (While g c, a', b')
(if guard g (a', b') then Seq c (While g c) else Skip, a', b')")
prefer 2
apply fastforce
apply (drule (1) star_n_trans)
apply (drule (2) diverges_init_state)
apply (clarsimp simp: diverges.simps terminates.simps star_eq_star_n)
apply (insert terminates_or_diverges)
apply (drule_tac x="(a', b')" and y=c in meta_spec2)
apply (erule disjE)
(* terminating case *)
apply clarsimp
apply (rename_tac aa ba)
apply (rule_tac x=aa in exI)
apply (rule_tac x=ba in exI)
apply (rule step_n_rev, simp)
apply clarsimp
apply (clarsimp simp: terminates star_eq_star_n)
apply (rename_tac nb)
apply (drule_tac n=nb in While_body_add3step, simp, fastforce)
(* diverging case *)
apply clarsimp
apply (frule (1) diverging_body_diverges)
apply (frule star_n_conjunct2)
apply (drule (2) diverges_init_state_n)
apply (drule (2) diverges_init_state)
apply (drule (1) diverges_deterministic, simp)
apply (drule star_n_conjunct2)
by blast

lemma While_lemma:
"⟦∀i. ¬ div_at_iteration i s g c D; diverges s (While g c) l; D l⟧
⟹ ∃ts. ts 0 = s ∧ (∀i. guard g (ts i) ∧ terminates (ts i) c (ts (Suc i))
∧ (∃k. star_n step (i+k) (While g c, ts 0) (While g c, ts i)))"
apply (rule_tac x="λi. SOME t. star_n (λs t. terminates s c t) i s t" in exI)
apply (rule context_conjI)
apply (rule some_equality; clarsimp?)
apply (erule star_n.cases; simp)
apply clarsimp
apply (rename_tac i)
apply (drule (2) non_diverging_inf_loop)
apply (rule someI2_ex)
apply (drule_tac x=i in spec, clarsimp)
apply (drule star_n_conjunct2[THEN star_n_conjunct1])
apply fastforce
apply (frule_tac x=i in spec)
apply (elim exE conjE)
apply (frule star_n_conjunct2[THEN star_n_conjunct1])
apply (rename_tac t)
apply (drule NRC_terminates, drule_tac x=t in spec, simp)
apply (drule_tac x="Suc i" in spec)
apply (elim exE conjE)
apply (rename_tac a b)
apply (frule_tac t="(a, b)" in star_n_conjunct2[THEN star_n_conjunct1])
apply (erule star_n_lastE, clarsimp)
apply (rename_tac ad bd ae be k)
apply (frule_tac t="(ad, bd)" in star_n_conjunct2[THEN star_n_conjunct1])
apply (drule NRC_terminates, drule_tac x="(ad, bd)" in spec, clarsimp)
apply (rename_tac b n a' b' a a'' b'' k)
apply (rule conjI)
apply (rule someI2_ex, fastforce)
apply (fastforce simp: NRC_terminates)
apply (drule star_n_While_flatten, clarsimp)
apply (rule_tac x="n' - n" in exI, clarsimp)
done

(* output equality *)

lemma H_for_Nil_output:
"H i (a, b) ⟹ ignores_output H ⟹ H i (a, [])"
using ignores_output_def by blast

lemma output_of_simp[simp]:
"output_of (a, b) = b" by (fastforce simp: output_of_def)

lemma star_n_step_output_extend:
"star_n step n (c, s) (c', t) ⟹
∃new. snd t = snd s @ new ∧
(∀xs.  star_n step n (c, fst s, xs)
(c', fst t, xs @ new)) "
apply (induct n arbitrary: c s t c')
apply (erule star_n.cases; fastforce)
apply clarsimp
apply (erule star_n.cases; simp)
apply clarsimp
apply (rename_tac c a b c' a' b' n c'' a'' b'')
apply (drule_tac x=c' in meta_spec)
apply (drule_tac x=a' and y=b' in meta_spec2)
apply (drule_tac x=a'' and y=b'' in meta_spec2)
apply (drule_tac x=c'' in meta_spec)
apply clarsimp
apply (drule step_output_extend)
apply clarsimp
apply (rotate_tac -1)
apply (rename_tac newa xs)
apply (drule_tac x=xs in spec)
apply (drule_tac x="xs@newa" in spec)
apply clarsimp
done

lemma lappend_initial_output:
"{llist_of out |out.
∃q t. star step (While x p, a, b) (q, t, out)}
=  lappend (llist_of b) ` {llist_of out |out.
∃q t. star step (While x p, a, []) (q, t, out)}"
apply (rule equalityI; clarsimp simp: star_eq_star_n)
apply (drule star_n_step_output_extend)
apply clarsimp
apply (drule_tac x=Nil in spec)
apply clarsimp
apply (metis (mono_tags, lifting) lappend_llist_of_llist_of mem_Collect_eq rev_image_eqI)
apply (drule star_n_step_output_extend)
apply clarsimp
apply (drule_tac x=b in spec)
apply (rename_tac out q t n)
apply (rule_tac x="b@out" in exI)
using lappend_llist_of_llist_of by blast

(***)

lemma ts_accum:
"∀i. prefix (output_of (ts i)) (output_of (ts (Suc i))) ⟹
concat (map (λi. drop (length (output_of (ts i))) (output_of (ts (Suc i)))) [0..<i])
= drop (length (output_of (ts 0))) (output_of (ts i))"
apply (induct i)
apply clarsimp
apply clarsimp
apply (rule injD[where f="λx. output_of (ts 0) @ x"])
apply (metis append_eq_append_conv injI)
apply (frule min_prefix)
apply (rotate_tac -1)
apply (rename_tac i)
apply (frule_tac x=i in spec)
apply (drule prefix_drop_append)
apply (drule_tac x="Suc i" in spec)
apply (drule prefix_drop_append)
apply (simp only: append_assoc[symmetric])
apply (frule_tac x=i in spec)
apply (drule prefix_drop_append)
apply clarsimp
done

theorem Pohjola_diverges:
"pohjola (λs. ∃l. diverges s c l ∧ D l) c D"
proof (induct c)
case (Seq c1 c2)
then show ?case
apply (clarsimp simp: diverges_Seq)
apply (rule_tac b="λs. ∃l. diverges s c1 l ∧ D l" in p_case)
apply (rule pohjola_strengthen[where P="λs. P s ∧ Q s" and P'=Q for P Q]; clarsimp)
apply (rule_tac P'="λs. ∃l. (∃t. terminates s c1 t ∧ diverges t c2 l) ∧ D l"
in pohjola_strengthen[rotated])
apply fastforce
apply (rule_tac M="λs. ∃l. diverges s c2 l ∧ D l" in p_seq_h; clarsimp)
by (rule_tac Q'="λs. ∃l. diverges s c2 l ∧ D l" in h_weaken[OF _ Hoare_terminates]; fastforce)
next
case (If x1 c1 c2)
then show ?case
apply (clarsimp simp: diverges_If)
apply (rule p_if)
apply (erule pohjola_strengthen, clarsimp)
by (erule pohjola_strengthen, clarsimp)
next
case (While x1 c)
then show ?case
apply (rule_tac b="λs. ∃i. div_at_iteration i s x1 c D" in p_case)
apply (rule_tac P'="λs. ∃i. div_at_iteration i s x1 c D" in pohjola_strengthen[rotated])
apply clarsimp
apply (rule_tac R="wf_to_wfP (measure (λs. SOME i. div_at_iteration i s x1 c D))"
and b="λs.¬ div_at_iteration 0 s x1 c D"
in p_while2)
apply clarsimp
apply (erule div_at_iteration.cases; clarsimp)
apply (simp only: wf_to_wfP_def wfP_def)
using wf_measure
apply (metis (no_types, lifting) case_prodE mem_Collect_eq subsetI wf_subset)
apply clarsimp
apply (rule Hoare_completeness)
apply (clarsimp simp: hoare_sem_def wf_to_wfP_def)
apply (case_tac i; clarsimp)
apply (rename_tac a b n a' b')
apply (rule_tac x=a' in exI, rule_tac x=b' in exI, clarsimp)
apply (frule (2) div_at_iteration.intros(2))
apply (rule conjI, fastforce)
apply (rule someI2_ex, fastforce)
apply (drule (1) div_at_iteration_11)
apply (rule someI2, simp)
apply (drule (1) div_at_iteration_11, clarsimp)
apply clarsimp
apply (rule pohjola_strengthen, simp)
apply fastforce
apply (rule p_while1, clarsimp)
apply (drule (2) While_lemma)
apply clarsimp
apply (rule context_conjI)
apply (drule_tac x=0 in spec, clarsimp)
apply (rename_tac ts)
apply (rule_tac x="λi s. fst s = fst (ts i)" in exI)
apply clarsimp
apply (rule context_conjI)
apply (clarsimp simp: ignores_output_def)
apply (rule_tac x="λi. drop (length (output_of (ts i))) (output_of (ts (Suc i)))" in exI)
apply (rule conjI; clarsimp?)
defer
apply (rule Hoare_completeness)
apply (clarsimp simp: hoare_sem_def)
apply (rename_tac i)
apply (frule_tac x=i in spec)
apply (drule_tac x="Suc i" in spec, clarsimp)
apply (intro conjI; (clarsimp simp: output_of_def guard_def; fail)?)
apply (drule terminates_history, clarsimp)
apply (drule_tac x=Nil in spec)
apply (clarsimp simp: split_def output_of_def)
apply (thin_tac "pohjola _ _ _")
apply (clarsimp simp: diverges.simps)
apply (erule back_subst[of D])
apply (simp only: lappend_initial_output[THEN arg_cong[where f=lSup]])
apply (subst lSup_lappend)
apply (rule chainI)
apply clarsimp
apply (meson lprefix_chain_NRC_step' lprefix_llist_of star_eq_star_n)
apply blast
apply (rename_tac a b ts)
apply (rule_tac f="lappend (llist_of b)" in arg_cong)
apply (subst lmap_inf_llist[symmetric])
apply (simp only: flat_inf_llist_lSup)
apply (subst ts_accum)
apply clarsimp
apply (rename_tac i)
apply (drule_tac x=i in spec)
apply safe
apply (meson NRC_step_output_mono star_star_n terminates.cases)
apply (rename_tac a b ts)
apply (rule upper_subset_lSup_eq[OF lprefix_chain_RTC_step])
apply clarsimp
apply (rename_tac i)
apply (drule_tac x=i in spec)
apply clarsimp
apply (drule_tac star_n_step_output_extend, clarsimp simp: star_eq_star_n)
apply (drule_tac x=Nil in spec)
apply clarsimp
apply (metis (mono_tags, opaque_lifting) append_eq_conv_conj output_of_simp prod.exhaust_sel)
apply (clarsimp simp: star_eq_star_n)
apply (rename_tac n)
apply (subgoal_tac "∃i k. star_n step (i + k) (While x1 c, a, b) (While x1 c, ts i)
∧ n < i + k")
apply clarsimp
apply (rename_tac i k)
apply (drule_tac x=i in spec)
apply clarsimp
apply (drule_tac n="i + k" in star_n_step_output_extend)
apply clarsimp
apply (rename_tac new)
apply (drule_tac x=Nil in spec, clarsimp)
apply (rule_tac x="llist_of new" in exI)
apply clarsimp
apply (rule conjI)
apply (metis append_eq_conv_conj output_of_def snd_def)
apply (metis (no_types, lifting) NRC_step_output_mono output_of_simp star_n_step_decompose)