Theory Nielson_Hoare
theory Nielson_Hoare
imports Big_StepT
begin
section "Nielson Style Hoare Logic with logical variables"
abbreviation "eq a b == (And (Not (Less a b)) (Not (Less b a)))"
type_synonym lvname = string
type_synonym assn2 = "(lvname ⇒ nat) ⇒ state ⇒ bool"
type_synonym tbd = "state ⇒ nat"
subsection ‹The support of an assn2›
definition support :: "assn2 ⇒ string set" where
"support P = {x. ∃l1 l2 s. (∀y. y ≠ x ⟶ l1 y = l2 y) ∧ P l1 s ≠ P l2 s}"
lemma support_and: "support (λl s. P l s ∧ Q l s) ⊆ support P ∪ support Q"
unfolding support_def by blast
lemma support_impl: "support (λl s. P s ⟶ Q l s) ⊆ support Q"
unfolding support_def by blast
lemma support_exist: "support (λl s. ∃ z::nat. Q z l s) ⊆ (UN n. support (Q n))"
unfolding support_def apply(auto)
by blast+
lemma support_all: "support (λl s. ∀z. Q z l s) ⊆ (UN n. support (Q n))"
unfolding support_def apply(auto)
by blast+
lemma support_single: "support (λl s. P (l a) s) ⊆ {a}"
unfolding support_def by fastforce
lemma support_inv: "⋀P. support (λl s. P s) = {}"
unfolding support_def by blast
lemma assn2_lupd: "x ∉ support Q ⟹ Q (l(x:=n)) = Q l"
by(simp add: support_def fun_upd_other fun_eq_iff)
(metis (no_types, lifting) fun_upd_def)
subsection "Validity"
abbreviation state_subst :: "state ⇒ aexp ⇒ vname ⇒ state"
(‹_[_'/_]› [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
definition hoare1_valid :: "assn2 ⇒ com ⇒ tbd ⇒ assn2 ⇒ bool"
(‹⊨⇩1 {(1_)}/ (_)/ { _ ⇓(1_)}› 50) where
"⊨⇩1 {P} c {q ⇓ Q} ⟷ (∃k>0. (∀l s. P l s ⟶ (∃t p. ((c,s) ⇒ p ⇓ t) ∧ p ≤ k * (q s) ∧ Q l t)))"
subsection "Hoare rules"
inductive
hoare1 :: "assn2 ⇒ com ⇒ tbd ⇒ assn2 ⇒ bool" (‹⊢⇩1 ({(1_)}/ (_)/ { _ ⇓ (1_)})› 50)
where
Skip: "⊢⇩1 {P} SKIP { (%s. Suc 0) ⇓ P}" |
Assign: "⊢⇩1 {λl s. P l (s[a/x])} x::=a { (%s. Suc 0) ⇓ P}" |
If: "⟦ ⊢⇩1 {λl s. P l s ∧ bval b s} c⇩1 { e1 ⇓ Q};
⊢⇩1 {λl s. P l s ∧ ¬ bval b s} c⇩2 { e1 ⇓ Q} ⟧
⟹ ⊢⇩1 {P} IF b THEN c⇩1 ELSE c⇩2 { (λs. e1 s + Suc 0 ) ⇓ Q}" |
Seq: "⟦ ⊢⇩1 { (%l s. P⇩1 l s ∧ l x = e2' s ) } c⇩1 { e1 ⇓ (%l s. P⇩2 l s ∧ e2 s ≤ l x )};
⊢⇩1 {P⇩2} c⇩2 { e2 ⇓ P⇩3}; x ∉ support P⇩1; x ∉ support P⇩2;
⋀l s. P⇩1 l s ⟹ e1 s + e2' s ≤ e s⟧
⟹ ⊢⇩1 {P⇩1} c⇩1;;c⇩2 { e ⇓ P⇩3}" |
While:
"⟦ ⊢⇩1 {λl s. P l s ∧ bval b s ∧ e' s = l y} c { e'' ⇓ λl s. P l s ∧ e s ≤ l y};
∀l s. bval b s ∧ P l s ⟶ e s ≥ 1 + e' s + e'' s ;
∀l s. ~ bval b s ∧ P l s ⟶ 1 ≤ e s;
y ∉ support P ⟧
⟹ ⊢⇩1 {P} WHILE b DO c { e ⇓ λl s. P l s ∧ ¬ bval b s}" |
conseq: "⟦ ∃k>0. ∀l s. P' l s ⟶ ( e s ≤ k * (e' s) ∧(∀t. ∃l'. P l' s ∧ ( Q l' t ⟶ Q' l t) ));
⊢⇩1 {P}c{ e ⇓ Q} ⟧ ⟹
⊢⇩1 {P'}c{e' ⇓ Q'}"
text‹Derived Rules:›
lemma conseq_old: "⟦∃k>0. ∀l s. P' l s ⟶ (P l s ∧ ( e' s ≤ k * (e s))); ⊢⇩1 {P}c{ e' ⇓ Q}; ∀l s. Q l s ⟶ Q' l s ⟧ ⟹
⊢⇩1 {P'}c{e ⇓ Q'}"
using conseq apply(metis) done
lemma If2: "⟦ ⊢⇩1 {λl s. P l s ∧ bval b s} c⇩1 { e ⇓ Q}; ⊢⇩1 {λl s. P l s ∧ ¬ bval b s} c⇩2 { e ⇓ Q};
⋀l s. P l s ⟹ e s + 1 = e' s ⟧
⟹ ⊢⇩1 {P} IF b THEN c⇩1 ELSE c⇩2 { e' ⇓ Q}"
apply(rule conseq[OF _ If, where P=P and P'=P]) by(auto)
lemma strengthen_pre:
"⟦ ∀l s. P' l s ⟶ P l s ; ⊢⇩1 {P} c { e ⇓ Q} ⟧ ⟹ ⊢⇩1 {P'} c { e ⇓ Q}"
apply(rule conseq_old[where e'=e and Q=Q and P=P])
by(auto)
lemma weaken_post:
"⟦ ⊢⇩1 {P} c {e ⇓ Q}; ∀l s. Q l s ⟶ Q' l s ⟧ ⟹ ⊢⇩1 {P} c {e ⇓ Q'}"
apply(rule conseq_old[where e'=e and Q=Q and P=P])
by(auto)
lemma ub_cost:
"⟦ (∃k>0. ∀l s. P l s ⟶ e' s ≤ k * (e s)); ⊢⇩1 {P} c {e' ⇓ Q} ⟧ ⟹ ⊢⇩1 {P} c {e ⇓ Q}"
apply(rule conseq_old[where e'=e' and Q=Q and P=P])
by(auto)
lemma Assign': "∀l s. P l s ⟶ Q l (s[a/x]) ⟹ (⊢⇩1 {P} x ::= a { (%s. 1) ⇓ Q})"
using strengthen_pre[OF _ Assign]
by (simp )
subsection "Soundness"
text‹The soundness theorem:›
theorem hoare1_sound: "⊢⇩1 {P}c{e ⇓ Q} ⟹ ⊨⇩1 {P}c{e ⇓ Q}"
apply(unfold hoare1_valid_def)
proof( induction rule: hoare1.induct)
case (Skip P)
show ?case by fastforce
next
case (Assign P a x)
show ?case by fastforce
next
case (Seq P1 x e2' c1 e1 P2 e2 c2 P3 e)
from Seq(6) obtain k where k: "k>0" and S6: "∀l s. P1 l s ∧ l x = e2' s ⟶ (∃t p. (c1, s) ⇒ p ⇓ t ∧ p ≤ k * e1 s ∧ P2 l t ∧ e2 t ≤ l x)" by auto
from Seq(7) obtain k' where k': "k'>0" and S7: "∀l s. P2 l s ⟶ (∃t p. (c2, s) ⇒ p ⇓ t ∧ p ≤ k' * e2 s ∧ P3 l t)" by auto
from k k' have "0 < max k k'" by auto
show ?case
proof (rule exI[where x="max k k'"], safe)
fix l s
have x_supp: "x ∉ support P1" by fact
have x_supp2: "x ∉ support P2" by fact
from S6 have S: "P1 (l(x := e2' s)) s ∧ (l(x := e2' s)) x = e2' s ⟶ (∃t p. (c1, s) ⇒ p ⇓ t ∧ p ≤ k * e1 s ∧ P2 (l(x := e2' s)) t ∧ e2 t ≤ (l(x := e2' s)) x) "
by blast
assume a: "P1 l s"
with Seq(5) have 1: " e1 s + e2' s ≤ e s" by simp
with a S assn2_lupd[OF x_supp] have "(∃t p. (c1, s) ⇒ p ⇓ t ∧ p ≤ k * e1 s ∧ P2 (l(x := e2' s)) t ∧ e2 t ≤ (l(x := e2' s)) x)" by simp
then obtain t p where c1: "(c1, s) ⇒ p ⇓ t" and cost1: " p ≤ k * e1 s" and P2': "P2 (l(x := e2' s)) t" and 31: "e2 t ≤ (l(x := e2' s)) x" by blast
from P2' assn2_lupd[OF x_supp2] have P2: "P2 l t" by auto
from 31 have 3: "e2 t ≤ e2' s" by simp
from S7 P2 have "(∃t' p'. ((c2, t) ⇒ p' ⇓ t') ∧ p' ≤ k' * e2 t ∧ P3 l t')" by blast
then obtain t' p' where c2: "(c2, t) ⇒ p' ⇓ t'" and cost2: " p' ≤ k' * (e2 t)" and P3: "P3 l t'" by blast
from c1 c2 have weg: "(c1;; c2, s) ⇒ p + p' ⇓ t'"
apply (rule Big_StepT.Seq) by simp
from cost1 cost2 3 have " (p+p') ≤ k * (e1 s) + k' * (e2' s)"
by (meson add_mono mult_le_mono2 order_subst1)
also have "… ≤ (max k k') * (e1 s) + (max k k') * (e2' s)"
by (simp add: add_mono)
also have "… ≤ (max k k') * (e1 s + e2' s)"
by (simp add: add_mult_distrib2)
also have "… ≤ (max k k') * (e s)" using 1 by simp
finally
have cost: " (p + p') ≤ (max k k') * (e s)" .
from weg cost P3
have "(c1;; c2, s) ⇒ p+p' ⇓ t' ∧ (p+p') ≤ (max k k') * (e s) ∧ P3 l t'" by blast
then show "(∃t p. (c1;; c2, s) ⇒ p ⇓ t ∧ p ≤ (max k k') * (e s) ∧ P3 l t)" by metis
qed fact
next
case (If P b c1 e Q c2)
from If(3) obtain k1 where k1: "k1>0" and If1: "∀l s. P l s ∧ bval b s ⟶ (∃t p. (c1, s) ⇒ p ⇓ t ∧ p ≤ k1 * e s ∧ Q l t)" by auto
from If(4) obtain k2 where k2: "k2>0" and If2: "∀l s. P l s ∧ ¬ bval b s ⟶ (∃t p. (c2, s) ⇒ p ⇓ t ∧ p ≤ k2 * e s ∧ Q l t)" by auto
let ?k' = "max (k1+1) (k2+1)"
have "?k'>0" by auto
show ?case
proof (rule exI[where x="?k'"], safe)
fix l s
assume P1: "P l s"
show "∃t p. (IF b THEN c1 ELSE c2, s) ⇒ p ⇓ t ∧ p ≤ ?k' * (e s + Suc 0) ∧ Q l t"
proof (cases "bval b s")
case True
with If1 P1 obtain t p where "(c1, s) ⇒ p ⇓ t" "p ≤ k1 * (e s)" "Q l t" by blast
with True have 1: "(IF b THEN c1 ELSE c2, s) ⇒ p+1 ⇓ t" "(p + 1) ≤ (k1+1) * (e s + Suc 0)"
"Q l t"
by auto
have "(k1+1) * (e s + Suc 0) ≤ ?k' * (e s + Suc 0)"
by (simp add: nat_mult_max_left)
with 1 have 2: "p+1 ≤ ?k' * (e s + Suc 0)"
by linarith
from 1 2 show "∃t p. (IF b THEN c1 ELSE c2, s) ⇒ p ⇓ t ∧ p ≤ ?k' * (e s + Suc 0) ∧ Q l t" by metis
next
case False
with If2 P1 obtain t p where "(c2, s) ⇒ p ⇓ t" "p ≤ k2 * (e s)" "Q l t" by blast
with False have 1: "(IF b THEN c1 ELSE c2, s) ⇒ p+1 ⇓ t" "(p + 1) ≤ (k2+1) * ( e s + Suc 0)"
"Q l t"
by auto
have "(k2+1) * (e s + Suc 0) ≤ ?k' * (e s + Suc 0)"
by (simp add: nat_mult_max_left)
with 1 have 2: "p+1 ≤ ?k' * (e s + Suc 0)"
by linarith
from 1 2 show "∃t p. (IF b THEN c1 ELSE c2, s) ⇒ p ⇓ t ∧ p ≤ ?k' * (e s + Suc 0) ∧ Q l t" by metis
qed
qed fact
next
case (conseq P' e e' P Q Q' c)
from conseq(1) obtain k1 where k1: "k1>0" and c1: "∀l s. P' l s ⟶ e s ≤ k1 * e' s ∧ (∀t. ∃l'. P l' s ∧ (Q l' t ⟶ Q' l t))" by auto
then have c1': "⋀l s. P' l s ⟹ e s ≤ k1 * e' s ∧ (∀t. ∃l'. P l' s ∧ (Q l' t ⟶ Q' l t))"
by auto
from conseq(3) obtain k2 where k2: "k2>0" and c2: "∀l s. P l s ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k2 * e s ∧ Q l t)" by auto
then have c2': "⋀l s. P l s ⟹ (∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k2 * e s ∧ Q l t)" by auto
have "k2*k1 > 0" using k1 k2 by auto
show ?case
proof (rule exI[where x="k2*k1"], safe)
fix l s
assume "P' l s"
with c1' have A: "e s ≤ k1 * e' s" and "⋀t. ∃l'. P l' s ∧ (Q l' t ⟶ Q' l t)" by auto
then obtain fl where "⋀t. P (fl t) s" and B: "⋀t. Q (fl t) t ⟶ Q' l t" by metis
with c2' obtain ft fp where i: "⋀t. (c, s) ⇒ (fp t) ⇓ (ft t)" and ii: "⋀t. (fp t) ≤ k2 * e s"
and iii: "⋀t. Q (fl t) (ft t)"
by meson
from i obtain t p where tt: "⋀x. ft x = t" "⋀x. fp x = p" using big_step_t_determ2
by meson
with i have c: "(c, s) ⇒ p ⇓ t" by simp
from tt ii iii have p: "p ≤ k2 * e s" and Q: "⋀x. Q (fl x) t" by auto
have p: "p ≤ k2 * k1 * e' s" using p A
by (metis le_trans mult.assoc mult_le_mono2)
from B Q have q: "Q' l t" by fast
from c p q
show "∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k2 *k1 * e' s ∧ Q' l t"
by blast
qed fact
next
case (While INV b e' y c e'' e)
from While(5) obtain k where W6: "∀l s. INV l s ∧ bval b s ∧ e' s = l y ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k * e'' s ∧ INV l t ∧ e t ≤ l y)" by auto
let ?k' = "k+1"
{
fix n l s
have "⟦ e s = n; INV l s ⟧ ⟹ ∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ p ≤ ?k' * e s ∧ INV l t ∧ ¬ bval b t"
proof(induction "n" arbitrary: l s rule: less_induct)
case (less x)
show ?case
proof (cases "bval b s")
case False
with less(2,3) While(3) have b: "1 ≤ e s" by auto
show ?thesis
apply(rule exI[where x=s])
apply(rule exI[where x=1]) apply safe
subgoal using WhileFalse[OF False] by simp
subgoal using b by auto
subgoal using less by auto
subgoal using False by auto
done
next
case True
with less(2,3) While(2) have bT: "bval b s" and cost1: " 1 + e' s + e'' s ≤ e s" by auto
let ?l' = "l(y := e' s)"
have y_supp: "y ∉ support INV" by fact
from cost1 have Z: "e' s < x" using less(2) by auto
from W6
have "INV ?l' s ∧ bval b s ∧ e' s = ?l' y
⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k * e'' s ∧ INV ?l' t ∧ e t ≤ ?l' y)"
by blast
with less(3) bT
have "(∃t p. ((c, s) ⇒ p ⇓ t) ∧ p ≤ k * e'' s ∧ INV ?l' t ∧ e t ≤ e' s)"
using assn2_lupd[OF y_supp]
by(auto)
then obtain t p where ceff: "(c, s) ⇒ p ⇓ t" and cost2: " p ≤ k * e'' s"
and INVz': "INV ?l' t" and cost3: " e t ≤ e' s"
by blast
from INVz' have INVz: "INV l t" using assn2_lupd[OF y_supp] by auto
have "e t < x" using Z cost3 by auto
with less(1)[OF _ _ INVz, of "e t"] obtain t' p'
where weff: "(WHILE b DO c, t) ⇒ p' ⇓ t'" and cost4: " p' ≤ ?k' * e t" and INV0: "INV l t'"
and nb: "¬ bval b t'"
by fastforce
have "(WHILE b DO c, s) ⇒ 1 + p + p' ⇓ t'"
apply(rule WhileTrue)
apply fact
apply (fact ceff)
apply (fact weff) by simp
moreover
note INV0 nb
moreover
{
have "(1 + p + p') ≤ 1 + k * e'' s + ?k' * e t" using cost2 cost4 by linarith
also have "… ≤ 1 + k * e'' s + ?k' * e' s" using cost3
using add_left_mono mult_le_mono2 by blast
also have "… ≤ ?k'*1 + ?k'* e'' s + ?k' * e' s " by force
also have "… = ?k' * (1+ e' s + e'' s)" by algebra
also have "… ≤ ?k' * e s" using cost1
using mult_le_mono2 by blast
finally have " (1 + p + p') ≤ ?k' * e s" .
}
ultimately
show ?thesis by metis
qed
qed
}
then have erg: "⋀l s. INV l s ⟹ ∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ p ≤ (k + 1) * e s ∧ INV l t ∧ ¬ bval b t" by auto
show ?case apply(rule exI[where x="?k'"]) using erg by fastforce
qed
subsection "Completeness"
definition wp1 :: "com ⇒ assn2 ⇒ assn2" (‹wp⇩1›) where
"wp⇩1 c Q = (λl s. ∃t p. (c,s) ⇒ p ⇓ t ∧ Q l t)"
lemma support_wpt: "support (wp⇩1 c Q) ⊆ support Q"
by(simp add: support_def wp1_def) blast
lemma wp1_terminates: "wp⇩1 c Q l s ⟹ ↓ (c, s)" unfolding wp1_def by auto
lemma wp1_SKIP[simp]: "wp⇩1 SKIP Q = Q" by(auto intro!: ext simp: wp1_def)
lemma wp1_Assign[simp]: "wp⇩1 (x ::= e) Q = (λl s. Q l (s(x := aval e s)))" by(auto intro!: ext simp: wp1_def)
lemma wp1_Seq[simp]: "wp⇩1 (c⇩1;;c⇩2) Q = wp⇩1 c⇩1 (wp⇩1 c⇩2 Q)" by (auto simp: wp1_def fun_eq_iff)
lemma wp1_If[simp]: "wp⇩1 (IF b THEN c⇩1 ELSE c⇩2) Q = (λl s. wp⇩1 (if bval b s then c⇩1 else c⇩2) Q l s)" by (auto simp: wp1_def fun_eq_iff)
definition "prec c E == %s. E (THE t. (∃p. (c,s) ⇒ p ⇓ t))"
lemma wp1_prec_Seq_correct: "wp⇩1 (c1;;c2) Q l s ⟹ ↓⇩t (c1, s) + prec c1 (λs. ↓⇩t (c2, s)) s ≤ ↓⇩t (c1;; c2, s)"
proof -
assume "wp⇩1 (c1;;c2) Q l s"
then have wp: "wp⇩1 c1 (wp⇩1 c2 Q) l s" by simp
then obtain t p where c1_term: "(c1, s) ⇒ p ⇓ t" and "(∃ta p. (c2, t) ⇒ p ⇓ ta ∧ Q l ta)" unfolding wp1_def by blast
then obtain t' p' where c2_term: "(c2, t) ⇒ p' ⇓ t'" and "Q l t'" by blast
have p: "↓⇩t (c1, s) = p" using c1_term bigstepT_the_cost by simp
have "↓⇩t (c2, t) = p'" using c2_term bigstepT_the_cost by simp
have f: "(THE t. ∃p. (c1, s) ⇒ p ⇓ t) = t" using c1_term bigstepT_the_state by simp
have " prec c1 (λs. ↓⇩t (c2, s)) s = p'" unfolding prec_def f using c2_term bigstep_det by blast
then have p': " prec c1 (λs. (THE n. ∃a. (c2, s) ⇒ n ⇓ a)) s
= p'" unfolding prec_def by blast
from wp have "wp⇩1 (c1;;c2) Q l s" by simp
then obtain T P where c12_term: "(c1;;c2, s) ⇒ P ⇓ T" and "Q l T" unfolding wp1_def by blast
have P: "(THE n. (∃a. (c1;;c2, s) ⇒ n ⇓ a)) = P" using c12_term bigstepT_the_cost by simp
from c12_term have Ppp': "P = p + p'"
apply(elim Seq_tE)
using c1_term bigstep_det c2_term by blast
have " (THE n. ∃a. (c1, s) ⇒ n ⇓ a) + prec c1 (λs. (THE n. ∃a. (c2, s) ⇒ n ⇓ a)) s
= p + p'" using p p' by auto
also have "… = P" using Ppp' by auto
also have "… = (THE n. (∃a. (c1;;c2, s) ⇒ n ⇓ a))" using P by auto
finally
show "↓⇩t (c1, s) + prec c1 (λs. ↓⇩t (c2, s)) s ≤ ↓⇩t (c1;; c2, s)"
by simp
qed
abbreviation "new Q ≡ SOME x. x ∉ support Q"
lemma bigstep_det: "(c1, s) ⇒ p1 ⇓ t1 ⟹ (c1, s) ⇒ p ⇓ t ⟹ p1=p ∧ t1=t"
using big_step_t_determ2 by simp
lemma bigstepT_the_cost: "(c, s) ⇒ P ⇓ T ⟹ (THE n. ∃a. (c, s) ⇒ n ⇓ a) = P"
using bigstep_det by blast
lemma bigstepT_the_state: "(c, s) ⇒ P ⇓ T ⟹ (THE a. ∃n. (c, s) ⇒ n ⇓ a) = T"
using bigstep_det by blast
lemma assumes b: "bval b s"
shows wp1WhileTrue': "wp⇩1 (WHILE b DO c) Q l s = wp⇩1 c (wp⇩1 (WHILE b DO c) Q) l s"
proof
assume "wp⇩1 c (wp⇩1 (WHILE b DO c) Q) l s"
from this[unfolded wp1_def]
obtain t s' t' s'' where "(c, s) ⇒ t ⇓ s'" "(WHILE b DO c, s') ⇒ t' ⇓ s''" and Q: "Q l s''" by blast
with b have "(WHILE b DO c, s) ⇒ 1+t+t' ⇓ s''" by auto
with Q show "wp⇩1 (WHILE b DO c) Q l s" unfolding wp1_def by auto
next
assume "wp⇩1 (WHILE b DO c) Q l s"
from this[unfolded wp1_def]
obtain t s'' where "(WHILE b DO c, s) ⇒ t ⇓ s''" and Q: "Q l s''" by blast
with b obtain t1 t2 s' where "(c, s) ⇒ t1 ⇓ s'" "(WHILE b DO c, s') ⇒ t2 ⇓ s''" by auto
with Q show "wp⇩1 c (wp⇩1 (WHILE b DO c) Q) l s " unfolding wp1_def by auto
qed
lemma assumes b: "~ bval b s"
shows wp1WhileFalse': "wp⇩1 (WHILE b DO c) Q l s = Q l s"
proof
assume "wp⇩1 (WHILE b DO c) Q l s"
from this[unfolded wp1_def]
obtain t s' where "(WHILE b DO c, s) ⇒ t ⇓ s'" and Q: "Q l s'" by blast
with b have "s=s'" by auto
with Q show "Q l s" by auto
next
assume "Q l s"
with b show "wp⇩1 (WHILE b DO c) Q l s" unfolding wp1_def by auto
qed
lemma wp1While: "wp⇩1 (WHILE b DO c) Q l s = (if bval b s then wp⇩1 c (wp⇩1 (WHILE b DO c) Q) l s else Q l s)"
apply(cases "bval b s")
using wp1WhileTrue' apply simp
using wp1WhileFalse' apply simp done
lemma wp1_prec2: fixes e::tbd
shows "(wp⇩1 c1 Q l s ∧
l x = prec c1 e s) = wp⇩1 c1 (λl s. Q l s ∧ e s = l x) l s"
by (metis (mono_tags, lifting) Big_StepT.bigstepT_the_state prec_def wp1_def)
lemma wp1_prec: fixes e::tbd
shows "wp⇩1 c1 Q l s ⟹
l x = prec c1 e s ⟹ wp⇩1 c1 (λl s. Q l s ∧ e s = l x) l s"
unfolding wp1_def prec_def apply(auto)
proof -
fix p t
assume "l x = e (THE t. ∃p. (c1, s) ⇒ p ⇓ t)"
assume 2: "Q l t"
assume 1: "(c1, s) ⇒ p ⇓ t "
show "∃t. (∃p. (c1, s) ⇒ p ⇓ t) ∧ Q l t ∧ e t = e (THE t. ∃p. (c1, s) ⇒ p ⇓ t) "
apply(rule exI[where x=t])
apply(safe)
apply(rule exI[where x=p]) using 1 apply simp
apply(fact)
using 1 by(simp add: bigstepT_the_state)
qed
lemma wp1_is_pre: "finite (support Q) ⟹ ⊢⇩1 {wp⇩1 c Q} c { λs. ↓⇩t (c, s) ⇓ Q}"
proof (induction c arbitrary: Q)
case SKIP
have ff: "⋀s n. (∃a. (SKIP, s) ⇒ n ⇓ a) = (n=Suc 0)" by blast
show ?case apply (auto intro:hoare1.Skip simp add: ff) using ff done
next
have gg: "⋀x1 x2 s n. (∃a. (x1 ::= x2, s) ⇒ n ⇓ a) = (n=Suc 0)" by blast
case Assign show ?case apply (auto intro:hoare1.Assign simp add: gg) done
next
case (Seq c1 c2)
let ?x = "new Q"
have "∃x. x ∉ support Q" using Seq.prems infinite_UNIV_listI
using ex_new_if_finite by blast
hence "?x ∉ support Q" by (rule someI_ex)
then have x2: "?x ∉ support (wp⇩1 c2 Q)" using support_wpt by (fast)
then have x12: "?x ∉ support (wp⇩1 (c1;;c2) Q)" apply simp using support_wpt by fast
let ?Q1 = "(λl s. (wp⇩1 c2 Q) l s ∧ ↓⇩t (c2, s) = l ?x)"
have "finite (support ?Q1)" apply(rule rev_finite_subset[OF _ support_and])
apply(rule finite_UnI)
apply(rule rev_finite_subset[OF _ support_wpt]) apply(fact)
apply(rule rev_finite_subset[OF _ support_single]) by simp
then have pre: "⋀u. ⊢⇩1 {wp⇩1 c1 ?Q1 } c1 { λs. ↓⇩t (c1, s) ⇓ ?Q1 }"
using Seq(1) by simp
have A: " ⊢⇩1 {λl s. wp⇩1 (c1;;c2) Q l s ∧ l ?x = (prec c1 (%s. ↓⇩t (c2, s))) s} c1 { λs. ↓⇩t (c1, s) ⇓ λl s. wp⇩1 c2 Q l s ∧ ↓⇩t (c2, s) ≤ l ?x}"
apply(rule conseq_old[OF _ pre ])
by(auto simp add: wp1_prec)
show "⊢⇩1 {wp⇩1 (c1;; c2) Q} c1;; c2 { λs. ↓⇩t (c1;; c2, s) ⇓ Q}"
apply(rule hoare1.Seq[OF A Seq(2)])
using Seq(3) x12 x2 wp1_prec_Seq_correct .
next
case (If b c1 c2)
show ?case apply(simp)
apply(rule If2[where e="%s. if bval b s then ↓⇩t (c1, s) else ↓⇩t (c2, s)"])
apply(simp_all cong:rev_conj_cong)
apply(rule conseq_old[where Q=Q and Q'=Q])
prefer 2
apply(rule If.IH(1)) apply(fact)
apply(simp_all) apply(auto)[1]
apply(rule conseq_old[where Q=Q and Q'=Q])
prefer 2
apply(rule If.IH(2)) apply(fact)
apply(simp_all) apply(auto)[1]
apply (blast intro: If_THE_True wp1_terminates If_THE_False)
done
next
case (While b c)
let ?y = "(new (wp⇩1 (WHILE b DO c) Q))"
have "finite (support (wp⇩1 (WHILE b DO c) Q))"
apply(rule finite_subset[OF support_wpt]) apply fact done
then have "∃x. x ∉ support (wp⇩1 (WHILE b DO c) Q)" using infinite_UNIV_listI
using ex_new_if_finite by blast
hence yQx: "?y ∉ support (wp⇩1 (WHILE b DO c) Q)" by (rule someI_ex)
show ?case
proof (rule conseq_old[OF _ hoare1.While], safe )
show "∃k>0. ∀l s. wp⇩1 (WHILE b DO c) Q l s ⟶ wp⇩1 (WHILE b DO c) Q l s ∧ ↓⇩t (WHILE b DO c, s) ≤ k * ↓⇩t (WHILE b DO c, s)"
apply auto done
next
fix l s
assume "wp⇩1 (WHILE b DO c) Q l s" "¬ bval b s"
then show "Q l s" by (simp add: wp1While)
next
fix l s
assume "wp⇩1 (WHILE b DO c) Q l s"
from this[unfolded wp1_def] obtain t s' where t: "(WHILE b DO c, s) ⇒ t ⇓ s'" and "Q l s'" by blast
then have r: "↓⇩t (WHILE b DO c, s) = t" using Nielson_Hoare.bigstepT_the_cost by auto
assume "¬ bval b s"
with r t have t2: "t=1" by auto
from r t2 show "1 ≤ ↓⇩t (WHILE b DO c, s)" by auto
next
fix l s
assume "wp⇩1 (WHILE b DO c) Q l s"
from this[unfolded wp1_def] obtain t s'' where t: "(WHILE b DO c, s) ⇒ t ⇓ s''" "Q l s''" by blast
then have r: "↓⇩t (WHILE b DO c, s) = t" using Nielson_Hoare.bigstepT_the_cost by auto
assume "bval b s"
with t obtain t1 t2 s' where 1: "(c,s) ⇒ t1 ⇓ s'" and 2: "(WHILE b DO c, s') ⇒ t2 ⇓ s''" and sum: "t=t1+t2+1" and "bval b s" by auto
from 1 have A: "↓⇩t (c,s) = t1" and s': "↓⇩s (c,s) = s'" using Nielson_Hoare.bigstepT_the_cost bigstepT_the_state by auto
from 2 s' have B: "↓⇩t (WHILE b DO c, ↓⇩s(c,s)) = t2" using Nielson_Hoare.bigstepT_the_cost by auto
show "1 + (%s. ↓⇩t (WHILE b DO c, ↓⇩s(c,s))) s + (%s. ↓⇩t (c,s)) s ≤ ↓⇩t (WHILE b DO c, s)"
apply(simp add: r A B sum) done
next
show "⊢⇩1 {λl s. wp⇩1 (WHILE b DO c) Q l s ∧ bval b s ∧ ↓⇩t (WHILE b DO c, ↓⇩s (c, s)) = l ?y} c
{ λs. ↓⇩t (c, s) ⇓ λl s. wp⇩1 (WHILE b DO c) Q l s ∧ ↓⇩t (WHILE b DO c, s) ≤ l ?y}"
apply(rule conseq_old[OF _ While(1), of _ "%l s. wp⇩1 (WHILE b DO c) Q l s ∧ ↓⇩t (WHILE b DO c, s) = l ?y"])
apply(rule exI[where x=1]) apply simp
subgoal apply safe
apply(subst (asm) wp1While) apply simp
proof - fix l s
assume 1: "wp⇩1 c (wp⇩1 (WHILE b DO c) Q) l s"
assume 2: "↓⇩t (WHILE b DO c, ↓⇩s (c, s)) = l ?y"
then have "l ?y = prec c (%s. ↓⇩t (WHILE b DO c, s)) s" unfolding prec_def by auto
with 1 wp1_prec2[of c "(wp⇩1 (WHILE b DO c) Q)" l s _ "(λs. ↓⇩t (WHILE b DO c, s))"]
show "wp⇩1 c (λl s. wp⇩1 (WHILE b DO c) Q l s ∧ ↓⇩t (WHILE b DO c, s) = l ?y) l s" by auto
qed
subgoal apply(rule finite_subset[OF support_and]) apply auto
apply(rule finite_subset[OF support_wpt]) apply fact
apply(rule finite_subset) apply(rule support_single) by auto
apply auto done
next
assume "new (wp⇩1 (WHILE b DO c) Q) ∈ support (wp⇩1 (WHILE b DO c) Q)"
with yQx show "False"
by blast
qed
qed
lemma valid_wp: "⊨⇩1 {P}c{p ⇓ Q} ⟷ (∃k>0. (∀l s. P l s ⟶ (wp⇩1 c Q l s ∧ ((THE n. (∃ t. ((c,s) ⇒ n ⇓ t)))) ≤ k * p s)))"
apply(rule)
apply(auto simp: hoare1_valid_def wp1_def)
subgoal for k apply(rule exI[where x=k]) using bigstepT_the_cost by fast
subgoal for k apply(rule exI[where x=k]) using bigstepT_the_cost by fast
done
theorem hoare1_complete: "finite (support Q) ⟹ ⊨⇩1 {P}c{p ⇓ Q} ⟹ ⊢⇩1 {P}c{p ⇓ Q}"
apply(rule conseq_old[OF _ wp1_is_pre, where Q'=Q and Q=Q, simplified])
by (auto simp: valid_wp)
corollary hoare1_sound_complete: "finite (support Q) ⟹ ⊢⇩1 {P}c{p ⇓ Q} ⟷ ⊨⇩1 {P}c{p ⇓ Q}"
by (metis hoare1_sound hoare1_complete)
end