Theory StdLogicCompleteness

```section "Completeness of the standard Hoare logic"

theory StdLogicCompleteness imports StdLogic WhileLangLemmas begin

lemma Hoare_strengthen:
"(⋀s. P s ⟹ P' s) ⟹ hoare P' p Q ⟹ hoare P p Q" using h_weaken by blast

lemma Hoare_strengthen_post:
"(⋀s. Q' s ⟹ Q s) ⟹ hoare P p Q' ⟹ hoare P p Q" using h_weaken by blast

theorem Hoare_While:
assumes h1: "(⋀s. P s ⟹ R s)"
assumes h2: "(⋀s. R s ∧ ¬guard x s ⟹ Q s)"
assumes h3:  "⋀s0. hoare (λs. R s ∧ guard x s ∧ s = s0) p (λs. R s ∧ m s < ((m s0)::nat))"
shows "hoare P (While x p) Q"
apply (rule_tac P'=R and Q'="λs. R s ∧ ¬guard x s" in h_weaken; (simp add: h1 h2)?)
apply (rule h_while[OF h3])
apply (clarsimp simp: wfP_def)
using wf_measure[where f=m, simplified measure_def inv_image_def]
by auto

lemma NRC_lemma:
"star_n (λs t. guard f s ∧ terminates s c t) k0 m t0 ⟹
star_n (λs t. guard f s ∧ terminates s c t) k1 m t1 ⟹
¬guard f t0 ∧ ¬guard f t1 ⟹
t0 = t1 ∧ k0 = k1"
apply (induct k0 arbitrary: k1 m; clarsimp)
apply (case_tac k1; clarsimp)
apply (erule star_n.cases)+
apply clarsimp+
apply (erule star_n.cases)+
apply clarsimp+
apply (case_tac k1; clarsimp)
apply (erule star_n.cases)+
apply clarsimp+
apply (erule star_n.cases)+
apply clarsimp+
apply (rename_tac k1)
apply (drule_tac x=k1 in meta_spec)
apply (erule star_n.cases)
apply clarsimp+
apply (erule star_n.cases)
apply clarsimp+
apply (drule (1) terminates_deterministic)
apply clarsimp
done

lemma Hoare_terminates:
"hoare (λs. ∃t. terminates s c t ∧ Q t) c Q"
proof (induct c arbitrary: Q)
case (Seq c1 c2)
then show ?case
apply (clarsimp simp: terminates_Seq)
apply (rule_tac M="λs. ∃s'. terminates s c2 s' ∧ Q s'" in h_seq)
apply (drule_tac x="λs. ∃s'. terminates s c2 s' ∧ Q s'" in meta_spec)
apply clarsimp
apply (rule Hoare_strengthen[rotated], simp, fastforce)
by fastforce
next
case (If x1 c1 c2)
then show ?case
apply (clarsimp simp: terminates_If)
apply (rule h_if)
by (rule Hoare_strengthen[rotated], fastforce+)+
next
case (While x1 c)
then show ?case
apply (rule_tac m="λs. THE n. ∃t. (star_n (λs t. guard x1 s ∧ terminates s c t) n s t)
∧ ¬guard x1 t"
in Hoare_While)
apply assumption
apply (clarsimp simp: terminates_While terminates_If terminates_Skip)
apply (rename_tac s0)
apply (rule_tac Q'="λs. terminates s0 c s ∧ (∃a b. terminates s (While x1 c) (a, b)
∧ guard x1 s0 ∧ Q (a, b))"
in Hoare_strengthen_post[rotated])
apply (drule_tac x="λs. terminates s0 c s ∧ (∃a b. terminates s (While x1 c) (a, b)
∧ guard x1 s0 ∧ Q (a, b))"
in meta_spec)
apply clarsimp
apply (rule Hoare_strengthen[rotated])
apply assumption
apply clarsimp
apply (subst (asm) (3) terminates_While)
apply (clarsimp simp: terminates_If terminates_Seq)
apply fastforce
apply (rule conjI)
apply fastforce
apply clarsimp
apply (drule_tac p="While x1 c" and f=x1 and c=c in terminates_While_NRC)
apply clarsimp
apply (erule exE)
apply (subst the_equality)
apply (rename_tac ab bb n)
apply (rule_tac x=ab in exI, rule_tac x=bb in exI)
apply (fastforce dest: NRC_lemma)+
apply clarsimp
apply (drule step_n[rotated], simp)
apply (subst the_equality)
apply (fastforce dest: NRC_lemma)+
done
qed (clarsimp simp: terminates_Skip terminates_Assign terminates_Print)+

theorem Hoare_completeness:
"hoare_sem P c Q ⟹ hoare P c Q"
apply (unfold hoare_sem_def)
using h_weaken[OF _ Hoare_terminates] by blast

(* lemmas about properties of hoare *)

lemma hoare_pre_False:
"hoare (λ_. False) prog Q"
apply (rule Hoare_completeness)