Theory QuantK_Hoare
section ‹Quantitative Hoare Logic (big-O style)›
theory QuantK_Hoare
imports Big_StepT Complex_Main "HOL-Library.Extended_Nat"
begin
abbreviation "eq a b == (And (Not (Less a b)) (Not (Less b a)))"
type_synonym lvname = string
type_synonym assn = "state ⇒ bool"
type_synonym qassn = "state ⇒ enat"
text ‹The support of an assn2›
abbreviation state_subst :: "state ⇒ aexp ⇒ vname ⇒ state"
(‹_[_'/_]› [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
fun emb :: "bool ⇒ enat" (‹↑›) where
"emb False = ∞"
| "emb True = 0"
subsection "Definition of Validity"
definition hoare2o_valid :: "qassn ⇒ com ⇒ qassn ⇒ bool"
(‹⊨⇩2⇩'' {(1_)}/ (_)/ {(1_)}› 50) where
"⊨⇩2⇩' {P} c {Q} ⟷ (∃k>0. (∀s. P s < ∞ ⟶ (∃t p. ((c,s) ⇒ p ⇓ t) ∧ enat k * P s ≥ p + enat k * Q t)))"
subsection "Hoare Rules"
inductive
hoareQ :: "qassn ⇒ com ⇒ qassn ⇒ bool" (‹⊢⇩2⇩'' ({(1_)}/ (_)/ {(1_)})› 50)
where
Skip: "⊢⇩2⇩' {%s. eSuc (P s)} SKIP {P}" |
Assign: "⊢⇩2⇩' {λs. eSuc (P (s[a/x]))} x::=a { P }" |
If: "⟦ ⊢⇩2⇩' {λs. P s + ↑( bval b s)} c⇩1 { Q};
⊢⇩2⇩' {λs. P s + ↑(¬ bval b s)} c⇩2 { Q} ⟧
⟹ ⊢⇩2⇩' {λs. eSuc (P s)} IF b THEN c⇩1 ELSE c⇩2 { Q }" |
Seq: "⟦ ⊢⇩2⇩' { P⇩1 } c⇩1 { P⇩2 }; ⊢⇩2⇩' {P⇩2} c⇩2 { P⇩3 }⟧ ⟹ ⊢⇩2⇩' {P⇩1} c⇩1;;c⇩2 {P⇩3}" |
While:
"⟦ ⊢⇩2⇩' { %s. I s + ↑(bval b s) } c { %t. I t + 1 } ⟧
⟹ ⊢⇩2⇩' {λs. I s + 1 } WHILE b DO c {λs. I s + ↑(¬ bval b s) }" |
conseq: "⟦ ⊢⇩2⇩' {P}c{Q} ; ⋀s. P s ≤ enat k * P' s ; ⋀s. enat k * Q' s ≤ Q s; k>0 ⟧ ⟹
⊢⇩2⇩' {P'}c{ Q'}"
text ‹Derived Rules›
lemma const: "⟦ ⊢⇩2⇩' {λs. enat k * P s}c{λs. enat k * Q s}; k>0 ⟧ ⟹
⊢⇩2⇩' {P}c{ Q}"
apply(rule conseq) by auto
inductive
hoareQ' :: "qassn ⇒ com ⇒ qassn ⇒ bool" (‹⊢⇩Z ({(1_)}/ (_)/ {(1_)})› 50)
where
ZSkip: "⊢⇩Z {%s. eSuc (P s)} SKIP {P}" |
ZAssign: "⊢⇩Z {λs. eSuc (P (s[a/x]))} x::=a { P }" |
ZIf: "⟦ ⊢⇩Z {λs. P s + ↑( bval b s)} c⇩1 { Q};
⊢⇩Z {λs. P s + ↑(¬ bval b s)} c⇩2 { Q} ⟧
⟹ ⊢⇩Z {λs. eSuc (P s)} IF b THEN c⇩1 ELSE c⇩2 { Q }" |
ZSeq: "⟦ ⊢⇩Z { P⇩1 } c⇩1 { P⇩2 }; ⊢⇩Z {P⇩2} c⇩2 { P⇩3 }⟧ ⟹ ⊢⇩Z {P⇩1} c⇩1;;c⇩2 {P⇩3}" |
ZWhile:
"⟦ ⊢⇩Z { %s. I s + ↑(bval b s) } c { %t. I t + 1 } ⟧
⟹ ⊢⇩Z {λs. I s + 1 } WHILE b DO c {λs. I s + ↑(¬ bval b s) }" |
Zconseq': "⟦ ⊢⇩Z {P}c{Q} ; ⋀s. P s ≤ P' s ; ⋀s. Q' s ≤ Q s ⟧ ⟹
⊢⇩Z {P'}c{ Q'}" |
Zconst: "⟦ ⊢⇩Z {λs. enat k * P s}c{λs. enat k * Q s}; k>0 ⟧ ⟹
⊢⇩Z {P}c{ Q}"
lemma Zconseq: "⟦ ⊢⇩Z {P}c{Q} ; ⋀s. P s ≤ enat k * P' s ; ⋀s. enat k * Q' s ≤ Q s; k>0 ⟧ ⟹
⊢⇩Z {P'}c{ Q'}"
apply(rule Zconst[of k P' c Q'])
apply(rule Zconseq'[where P=P and Q=Q]) by auto
lemma ZQ: " ⊢⇩Z { P } c { Q } ⟹ ⊢⇩2⇩' { P } c { Q }"
apply(induct rule: hoareQ'.induct)
apply (auto simp: hoareQ.Skip hoareQ.Assign hoareQ.If hoareQ.Seq hoareQ.While)
subgoal using conseq[where k=1] using one_enat_def by auto
subgoal for k P c Q using const by auto
done
lemma QZ: " ⊢⇩2⇩' { P } c { Q } ⟹ ⊢⇩Z { P } c { Q }"
apply(induct rule: hoareQ.induct)
apply (auto simp: ZSkip ZAssign ZIf ZSeq ZWhile )
using Zconseq by blast
lemma QZ_iff: "⊢⇩2⇩' { P } c { Q } ⟷ ⊢⇩Z { P } c { Q }"
using ZQ QZ by metis
subsection "Soundness"
lemma enatSuc0[simp]: "enat (Suc 0) * x = x"
using one_enat_def by auto
theorem hoareQ_sound: "⊢⇩2⇩' {P}c{ Q} ⟹ ⊨⇩2⇩' {P}c{ Q}"
apply(unfold hoare2o_valid_def)
proof( induction rule: hoareQ.induct)
case (Skip P)
show ?case apply(rule exI[where x=1]) apply(auto)
subgoal for s apply(rule exI[where x=s]) apply(rule exI[where x="Suc 0"])
apply safe
apply fast
by (metis add.left_neutral add.right_neutral eSuc_enat iadd_Suc le_iff_add zero_enat_def)
done
next
case (Assign P a x)
show ?case apply(rule exI[where x=1]) apply(auto)
subgoal for s apply(rule exI[where x="s[a/x]"]) apply(rule exI[where x="Suc 0"])
apply safe
apply fast
by (metis add.left_neutral add.right_neutral eSuc_enat iadd_Suc le_iff_add zero_enat_def)
done
next
case (Seq P1 C1 P2 C2 P3)
from Seq(3) obtain k1 where Seq3: "∀s. P1 s < ∞ ⟶ (∃t p. (C1, s) ⇒ p ⇓ t ∧ enat p + enat k1 * P2 t ≤ enat k1 * P1 s)" and 10: "k1>0" by blast
from Seq(4) obtain k2 where Seq4: "∀s. P2 s < ∞ ⟶ (∃t p. (C2, s) ⇒ p ⇓ t ∧ enat p + enat k2 * P3 t ≤ enat k2 * P2 s)" and 20: "k2>0" by blast
let ?k = "lcm k1 k2"
show ?case apply(rule exI[where x="?k"])
proof (safe)
from 10 20 show "lcm k1 k2>0" by (auto simp: lcm_pos_nat)
fix s
assume ninfP1: "P1 s < ∞"
with Seq3 obtain t1 p1 where 1: "(C1, s) ⇒ p1 ⇓ t1" and q1: "enat p1 + k1 * P2 t1 ≤ k1 * P1 s" by blast
with ninfP1 have ninfP2: "P2 t1 < ∞"
using not_le 10 by fastforce
with Seq4 obtain t2 p2 where 2: "(C2, t1) ⇒ p2 ⇓ t2" and q2: "enat p2 + k2 * P3 t2 ≤ k2 * P2 t1" by blast
with ninfP2 have ninfP3: "P3 t2 < ∞"
using not_le 20 by fastforce
then obtain u2 where u2: "P3 t2 = enat u2" by auto
from ninfP2 obtain u1 where u1: "P2 t1 = enat u1" by auto
from ninfP1 obtain u0 where u0: "P1 s = enat u0" by auto
from Big_StepT.Seq[OF 1 2] have 12: "(C1;; C2, s) ⇒ p1 + p2 ⇓ t2" by simp
have i: "(C1;; C2, s) ⇒ p1+p2 ⇓ t2" using 1 and 2 by auto
from 10 20 have p: "k1 div gcd k1 k2 > 0" "k2 div gcd k1 k2 > 0"
by (simp_all add: div_greater_zero_iff)
have za: "?k = (k1 div gcd k1 k2) * k2"
apply(simp only: lcm_nat_def)
by (simp add: dvd_div_mult)
have za2: "?k = (k2 div gcd k1 k2) * k1"
apply(simp only: lcm_nat_def)
by (metis dvd_div_mult gcd_dvd2 mult.commute)
from q1[unfolded u1 u2 u0] have z: "p1 + k1 * u1 ≤ k1 * u0" by auto
from q2[unfolded u1 u2 u0] have y: " p2 + k2 * u2 ≤ k2 * u1" by auto
have "p1+p2 + ?k * u2 ≤ p1 + (k1 div gcd k1 k2)*p2 + ?k * u2 " using p by simp
also have "… ≤ (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*p2 + ?k * u2 " using p by simp
also have "… = (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*(p2 + k2* u2)"
apply(simp only: za) by algebra
also have "… ≤ (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*(k2 * u1)" using y
by (metis add_left_mono distrib_left le_iff_add)
also have "… = (k2 div gcd k1 k2)*p1 + ?k * u1" by(simp only: za)
also have "… = (k2 div gcd k1 k2)*p1 + (k2 div gcd k1 k2) *(k1* u1)" by(simp only: za2)
also have "… ≤ (k2 div gcd k1 k2)*(p1 + k1*u1)"
by (simp add: distrib_left)
also have "… ≤ (k2 div gcd k1 k2)*(k1 * u0)" using z
by fastforce
also have "… ≤ ?k * u0" by(simp only: za2)
finally
have "p1+p2 + ?k * u2 ≤ ?k * u0" .
then have ii: "enat (p1+p2) + ?k * P3 t2 ≤ ?k * P1 s"
unfolding u0 u2 by auto
from i ii show "∃t p. (C1;; C2, s) ⇒ p ⇓ t ∧ enat p + ?k * P3 t ≤ ?k * P1 s " by blast
qed
next
case (If P b c1 Q c2)
from If(3) obtain kT where If3: "∀s. P s + ↑ (bval b s) < ∞ ⟶ (∃t p. (c1, s) ⇒ p ⇓ t ∧ enat p + enat kT * Q t ≤ enat kT * (P s + ↑ (bval b s))) " and T: "kT > 0" by blast
from If(4) obtain kF where If4: "∀s. P s + ↑ (¬ bval b s) < ∞ ⟶ (∃t p. (c2, s) ⇒ p ⇓ t ∧ enat p + enat kF * Q t ≤ enat kF * (P s + ↑ (¬ bval b s)))" and F: "kF > 0" by blast
show ?case apply(rule exI[where x="kT*kF"])
proof (safe)
from T F show "0 < kT * kF" by auto
fix s
assume "eSuc (P s) < ∞"
then have i: "P s < ∞"
using enat_ord_simps(4) by fastforce
then obtain u0 where u0: "P s = enat u0" by auto
show "∃t p. (IF b THEN c1 ELSE c2, s) ⇒ p ⇓ t ∧ enat p + enat (kT * kF) * Q t ≤ enat (kT * kF) * eSuc (P s)"
proof(cases "bval b s")
case True
with i have "P s + emb (bval b s) < ∞" by simp
with If3 obtain p t where 1: "(c1, s) ⇒ p ⇓ t" and q: "enat p + enat kT * Q t ≤ enat kT * (P s + emb (bval b s))" by blast
from Big_StepT.IfTrue[OF True 1] have 2: "(IF b THEN c1 ELSE c2, s) ⇒ p + 1 ⇓ t" by simp
from q have "Q t < ∞" using i T True
using less_irrefl by fastforce
then obtain u1 where u1: "Q t = enat u1" by auto
from q True have q': "p + kT * u1 ≤ kT * u0" unfolding u0 u1 by auto
have "(p+1) + (kT * kF) * u1 ≤ kF*(p+1) + (kT * kF) * u1" using F
by (simp add: mult_eq_if)
also have "… ≤ kF*(p+1 + kT * u1)"
by (simp add: add_mult_distrib2)
also have "… ≤ kF*(1 + kT * u0)"
using q' by auto
also have "… ≤ (kT * kF) * Suc u0" using T by simp
finally
have " (p+1) + (kT * kF) * u1 ≤ (kT * kF) * Suc u0" .
then have 1: "enat (p+1) + enat (kT * kF) * Q t ≤ enat (kT * kF) * eSuc (P s)"
unfolding u1 u0 by (simp add: eSuc_enat)
from 1 2 show ?thesis by metis
next
case False
with i have "P s + emb (~bval b s) < ∞" by simp
with If4 obtain p t where 1: "(c2, s) ⇒ p ⇓ t" and q: "enat p + enat kF * Q t ≤ enat kF * (P s + emb (~bval b s))" by blast
from Big_StepT.IfFalse[OF False 1] have 2: "(IF b THEN c1 ELSE c2, s) ⇒ p + 1 ⇓ t" by simp
from q have "Q t < ∞" using i F False
using less_irrefl by fastforce
then obtain u1 where u1: "Q t = enat u1" by auto
from q False have q': "p + kF * u1 ≤ kF * u0" unfolding u0 u1 by auto
have "(p+1) + (kF * kT) * u1 ≤ kT*(p+1) + (kF * kT) * u1" using T
by (simp add: mult_eq_if)
also have "… ≤ kT*(p+1 + kF * u1)"
by (simp add: add_mult_distrib2)
also have "… ≤ kT*(1 + kF * u0)"
using q' by auto
also have "… ≤ (kF * kT) * Suc u0" using F by simp
finally
have " (p+1) + (kT * kF) * u1 ≤ (kT * kF) * Suc u0"
by (simp add: mult.commute)
then have 1: "enat (p+1) + enat (kT * kF) * Q t ≤ enat (kT * kF) * eSuc (P s)"
unfolding u1 u0 by (simp add: eSuc_enat)
from 1 2 show ?thesis by metis
qed
qed
next
case (conseq P c Q k1 P' Q')
from conseq(5) obtain k where c4: "∀s. P s < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * Q t ≤ enat k * P s)" and 0: "k>0" by blast
show ?case apply(rule exI[where x="k*k1"])
proof (safe)
show "k*k1>0" using 0 conseq(4) by auto
fix s
assume "P' s < ∞"
with conseq(2,4) have "P s < ∞"
using le_less_trans
by (metis enat.distinct(2) enat_ord_simps(4) imult_is_infinity)
with c4 obtain p t where 1: "(c, s) ⇒ p ⇓ t" and 2: "enat p + enat k * Q t ≤ enat k * P s" by blast
have "enat p + enat (k*k1) * Q' t = enat p + enat (k) * ( (enat k1) * Q' t)"
by (metis mult.assoc times_enat_simps(1))
also have "… ≤ enat p + enat (k) * Q t" using conseq(3)
by (metis add_left_mono distrib_left le_iff_add)
also have "… ≤ enat k * P s" using 2 by auto
also have "… ≤ enat (k*k1) * P' s" using conseq(2)
by (metis mult.assoc mult_left_mono not_less not_less_zero times_enat_simps(1))
finally have 2: "enat p + enat (k*k1) * Q' t ≤ enat (k*k1) * P' s"
by auto
from 1 2 show "∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + (k*k1) * Q' t ≤ (k*k1) * P' s" by auto
qed
next
case (While INV b c)
then obtain k where W2: "∀s. INV s + ↑ (bval b s) < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * (INV t + 1) ≤ enat k * (INV s + ↑ (bval b s)))" and g0: "k>0"
by blast
show ?case apply(rule exI[where x=k])
proof (safe)
show "0<k" by fact
fix s
assume ninfINV: "INV s + 1 < ∞"
then have f: "INV s < ∞"
using enat_ord_simps(4) by fastforce
then obtain n where i: "INV s = enat n" using not_infinity_eq
by auto
have "INV s = enat n ⟹ ∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ enat p + enat k * (INV t + emb (¬ bval b t)) ≤ enat k * (INV s + 1)"
proof (induct n arbitrary: s rule: less_induct)
case (less n)
then show ?case
proof (cases "bval b s")
case False
show ?thesis
apply(rule exI[where x="s"])
apply(rule exI[where x="Suc 0"])
apply safe
apply (fact WhileFalse[OF False])
using False
apply (simp add: one_enat_def) using g0
by (metis One_nat_def Suc_ile_eq add.commute add_left_mono distrib_left enat_0_iff(2) mult.right_neutral not_gr_zero one_enat_def)
next
case True
with less(2) W2 have "(∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * (INV t + 1) ≤ enat k * INV s )"
by force
then obtain t p where o: "(c, s) ⇒ p ⇓ t" and q: "enat p + enat k * (INV t + 1) ≤ enat k * INV s " by auto
from o bigstep_progress have p: "p > 0" by blast
from q have pf: "enat k * (INV t + 1) ≤ enat k * INV s"
using dual_order.trans by fastforce
then have "INV t < ∞" using less(2)
using g0 not_le by fastforce
then obtain invt where invt: "INV t = enat invt" by auto
from pf g0 have g: "INV t < INV s"
unfolding less(2) invt
by (metis (full_types) Suc_ile_eq add.commute eSuc_enat enat_ord_simps(1) nat_mult_le_cancel_disj plus_1_eSuc(1) times_enat_simps(1))
then have ninfINVt: "INV t < ∞" using less(2)
using enat_ord_simps(4) by fastforce
then obtain n' where i: "INV t = enat n'" using not_infinity_eq
by auto
with less(2) have ii: "n' < n"
using g by auto
from i ii less(1) obtain t2 p2 where o2: "(WHILE b DO c, t) ⇒ p2 ⇓ t2" and q2: "enat p2 + enat k * (INV t2 + emb (¬ bval b t2)) ≤ enat k * ( INV t + 1)" by blast
have ende: "~ bval b t2"
apply(rule ccontr) apply(simp) using q2 g0 ninfINVt
by (simp add: i one_enat_def)
from WhileTrue[OF True o o2] have "(WHILE b DO c, s) ⇒ 1 + p + p2 ⇓ t2" by simp
from ende q2 have q2': "enat p2 + enat k * INV t2 ≤ enat k * (INV t + 1)" by simp
show ?thesis
apply(rule exI[where x=t2])
apply(rule exI[where x= "1 + p + p2"])
apply(safe)
apply(fact)
using ende apply(simp)
proof -
have "enat (Suc (p + p2)) + enat k * INV t2 = enat (Suc p) + enat p2 + enat k * INV t2" by fastforce
also have "… ≤ enat (Suc p) + enat k * (INV t + 1)" using q2'
by (metis ab_semigroup_add_class.add_ac(1) add_left_mono)
also have "… ≤ 1 + enat k * (INV s)" using q
by (metis (no_types, opaque_lifting) add.commute add_left_mono eSuc_enat iadd_Suc plus_1_eSuc(1))
also have "… ≤ enat k + enat k * (INV s)" using g0
by (simp add: Suc_leI one_enat_def)
also have "… ≤ enat k * (INV s + 1)"
by (simp add: add.commute distrib_left)
finally show "enat (Suc (p + p2)) + enat k * INV t2 ≤ enat k * (INV s + 1)" .
qed
qed
qed
from this[OF i] show "∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ enat p + enat k * (INV t + emb (¬ bval b t)) ≤ enat k * (INV s + 1)" .
qed
qed
lemma conseq':
"⟦ ⊢⇩2⇩' {P} c {Q} ; ∀s. P s ≤ P' s; ∀s. Q' s ≤ Q s ⟧ ⟹ ⊢⇩2⇩' {P'} c {Q'}"
apply(rule conseq[where k=1]) by auto
lemma strengthen_pre:
"⟦ ∀s. P s ≤ P' s; ⊢⇩2⇩' {P} c {Q} ⟧ ⟹ ⊢⇩2⇩' {P'} c {Q}"
apply(rule conseq[where k=1 and Q'=Q and Q=Q]) by auto
lemma weaken_post:
"⟦ ⊢⇩2⇩' {P} c {Q}; ∀s. Q s ≥ Q' s ⟧ ⟹ ⊢⇩2⇩' {P} c {Q'}"
apply(rule conseq[where k=1]) by auto
lemma Assign': "∀s. P s ≥ eSuc ( Q(s[a/x])) ⟹ ⊢⇩2⇩' {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
subsection "Completeness"
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 SKIPnot: "(¬ (SKIP, s) ⇒ p ⇓ t) = (s≠t ∨ p≠Suc 0)" by blast
lemma SKIPp: "(THE p. ∃t. (SKIP, s) ⇒ p ⇓ t) = Suc 0"
apply(rule the_equality)
apply fast
apply auto done
lemma SKIPt: "(THE t. ∃p. (SKIP, s) ⇒ p ⇓ t) = s"
apply(rule the_equality)
apply fast
apply auto done
lemma ASSp: "(THE p. Ex (big_step_t (x ::= e, s) p)) = Suc 0"
apply(rule the_equality)
apply fast
apply auto done
lemma ASSt: "(THE t. ∃p. (x ::= e, s) ⇒ p ⇓ t) = s(x := aval e s)"
apply(rule the_equality)
apply fast
apply auto done
lemma ASSnot: "( ¬ (x ::= e, s) ⇒ p ⇓ t ) = (p≠Suc 0 ∨ t≠s(x := aval e s))"
apply auto done
text‹
The completeness proof proceeds along the same lines as the one for partial
correctness. First we have to strengthen our notion of weakest precondition
to take termination into account:›
definition wpQ :: "com ⇒ qassn ⇒ qassn" (‹wp⇩Q›) where
"wp⇩Q c Q = (λs. (if (∃t p. (c,s) ⇒ p ⇓ t ∧ Q t < ∞) then enat (THE p. ∃t. (c,s) ⇒ p ⇓ t) + Q (THE t. ∃p. (c,s) ⇒ p ⇓ t) else ∞))"
lemma wpQ_skip[simp]: "wp⇩Q SKIP Q = (%s. eSuc (Q s))"
apply(auto intro!: ext simp: wpQ_def)
prefer 2
apply(simp only: SKIPnot)
apply(simp)
apply(simp only: SKIPp SKIPt)
using one_enat_def plus_1_eSuc(1) by auto
lemma wpQ_ass[simp]: "wp⇩Q (x ::= e) Q = (λs. eSuc (Q (s(x := aval e s))))"
by (auto intro!: ext simp: wpQ_def ASSp ASSt ASSnot eSuc_enat)
lemma wpt_Seq[simp]: "wp⇩Q (c⇩1;;c⇩2) Q = wp⇩Q c⇩1 (wp⇩Q c⇩2 Q)"
unfolding wpQ_def
proof (rule, case_tac "∃t p. (c⇩1;; c⇩2, s) ⇒ p ⇓ t ∧ Q t < ∞", goal_cases)
case (1 s)
then obtain u p where ter: "(c⇩1;; c⇩2, s) ⇒ p ⇓ u" and Q: "Q u < ∞" by blast
then obtain t p1 p2 where i: "(c⇩1 , s) ⇒ p1 ⇓ t" and ii: "(c⇩2 , t) ⇒ p2 ⇓ u" and p: "p1 + p2 = p" by blast
from bigstepT_the_state[OF i] have t: "(THE t. ∃p. (c⇩1, s) ⇒ p ⇓ t) = t"
by blast
from bigstepT_the_state[OF ii] have t2: "(THE u. ∃p. (c⇩2, t) ⇒ p ⇓ u) = u"
by blast
from bigstepT_the_cost[OF i] have firstcost: "(THE p. ∃t. (c⇩1, s) ⇒ p ⇓ t) = p1"
by blast
from bigstepT_the_cost[OF ii] have secondcost: "(THE p. ∃u. (c⇩2, t) ⇒ p ⇓ u) = p2"
by blast
have totalcost: "(THE p. Ex (big_step_t (c⇩1;; c⇩2, s) p)) = p1 + p2"
using bigstepT_the_cost[OF ter] p by auto
have totalstate: "(THE t. ∃p. (c⇩1;; c⇩2, s) ⇒ p ⇓ t) = u"
using bigstepT_the_state[OF ter] by auto
have c2: "∃ta p. (c⇩2, t) ⇒ p ⇓ ta ∧ Q ta < ∞"
apply(rule exI[where x= u])
apply(rule exI[where x= p2]) apply safe apply fact+ done
have C: "∃t p. (c⇩1, s) ⇒ p ⇓ t ∧ (if ∃ta p. (c⇩2, t) ⇒ p ⇓ ta ∧ Q ta < ∞ then enat (THE p. Ex (big_step_t (c⇩2, t) p)) + Q (THE ta. ∃p. (c⇩2, t) ⇒ p ⇓ ta) else ∞) < ∞"
apply(rule exI[where x=t])
apply(rule exI[where x=p1])
apply safe
apply fact
apply(simp only: c2 if_True)
using Q bigstepT_the_state ii by auto
show ?case
apply(simp only: 1 if_True t t2 c2 C totalcost totalstate firstcost secondcost) by fastforce
next
case (2 s)
show ?case apply(simp only: 2 if_False)
apply auto using 2
by force
qed
lemma wpQ_If[simp]:
"wp⇩Q (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. eSuc (wp⇩Q (if bval b s then c⇩1 else c⇩2) Q s))"
apply (auto simp: wpQ_def fun_eq_iff)
subgoal for x t p i ta ia xa apply(simp only: IfTrue[THEN bigstepT_the_state])
apply(simp only: IfTrue[THEN bigstepT_the_cost])
apply(simp only: bigstepT_the_cost bigstepT_the_state)
by (simp add: eSuc_enat)
apply(simp only: bigstepT_the_state bigstepT_the_cost) apply force
apply(simp only: bigstepT_the_state bigstepT_the_cost)
proof(goal_cases)
case (1 x t p i ta ia xa)
note f= IfFalse[THEN bigstepT_the_state, of b x c⇩2 xa ta "Suc xa" c⇩1, simplified, OF 1(4) 1(5)]
note f2= IfFalse[THEN bigstepT_the_cost, of b x c⇩2 xa ta "Suc xa" c⇩1, simplified, OF 1(4) 1(5)]
note g= bigstep_det[OF 1(1) 1(5)]
show ?case
apply(simp only: f f2) using 1 g
by (simp add: eSuc_enat)
next
case 2
then
show ?case
apply(simp only: bigstepT_the_state bigstepT_the_cost) apply force done
qed
lemma hoareQ_inf: "⊢⇩2⇩' {%s. ∞} c { Q}"
apply (induction c arbitrary: Q)
apply(auto intro: hoareQ.Skip hoareQ.Assign hoareQ.Seq hoareQ.conseq)
subgoal apply(rule hoareQ.conseq) apply(rule hoareQ.If[where P="%s. ∞"]) by(auto intro: hoareQ.If hoareQ.conseq)
subgoal apply(rule hoareQ.conseq) apply(rule hoareQ.While[where I="%s. ∞"]) apply(rule hoareQ.conseq) by auto
done
lemma assumes b: "bval b s"
shows wpQ_WhileTrue: " wp⇩Q c (wp⇩Q (WHILE b DO c) Q) s + 1 ≤ wp⇩Q (WHILE b DO c) Q s"
proof (cases "∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ Q t < ∞")
case True
then obtain t p where w: "(WHILE b DO c, s) ⇒ p ⇓ t" and q: "Q t < ∞" by blast
from b w obtain p1 p2 t1 where c: "(c, s) ⇒ p1 ⇓ t1" and w': "(WHILE b DO c, t1) ⇒ p2 ⇓ t" and sum: "1 + p1 + p2 = p"
by auto
have g: "∃ta p. (WHILE b DO c, t1) ⇒ p ⇓ ta ∧ Q ta < ∞"
apply(rule exI[where x="t"])
apply(rule exI[where x="p2"])
apply safe apply fact+ done
have h: "∃t p. (c, s) ⇒ p ⇓ t ∧ (if ∃ta p. (WHILE b DO c, t) ⇒ p ⇓ ta ∧ Q ta < ∞ then enat (THE p. Ex (big_step_t (WHILE b DO c, t) p)) + Q (THE ta. ∃p. (WHILE b DO c, t) ⇒ p ⇓ ta) else ∞) < ∞"
apply(rule exI[where x="t1"])
apply(rule exI[where x="p1"])
apply safe apply fact
apply(simp only: g if_True) using bigstepT_the_state bigstepT_the_cost w' q by(auto)
have "wp⇩Q c (wp⇩Q (WHILE b DO c) Q) s + 1 = enat p + Q t"
unfolding wpQ_def apply(simp only: h if_True)
apply(simp only: bigstepT_the_state[OF c] bigstepT_the_cost[OF c] g if_True bigstepT_the_state[OF w'] bigstepT_the_cost[OF w']) using sum
by (metis One_nat_def ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral eSuc_enat plus_1_eSuc(2) plus_enat_simps(1))
also have "… = wp⇩Q (WHILE b DO c) Q s"
unfolding wpQ_def apply(simp only: True if_True)
using bigstepT_the_state bigstepT_the_cost w apply(simp) done
finally show ?thesis by simp
next
case False
have "wp⇩Q (WHILE b DO c) Q s = ∞"
unfolding wpQ_def
apply(simp only: False if_False) done
then show ?thesis by auto
qed
lemma assumes b: "~ bval b s"
shows wpQ_WhileFalse: " Q s + 1 ≤ wp⇩Q (WHILE b DO c) Q s"
proof (cases "∃t p. (WHILE b DO c, s) ⇒ p ⇓ t ∧ Q t < ∞")
case True
with b obtain t p where w: "(WHILE b DO c, s) ⇒ p ⇓ t" and "Q t < ∞" by blast
with b have c: "s=t" "p=Suc 0" by auto
have " wp⇩Q (WHILE b DO c) Q s = Q s + 1"
unfolding wpQ_def apply(simp only: True if_True)
using w c bigstepT_the_cost bigstepT_the_state by(auto simp add: one_enat_def)
then show ?thesis by auto
next
case False
have "wp⇩Q (WHILE b DO c) Q s = ∞"
unfolding wpQ_def
apply(simp only: False if_False) done
then show ?thesis by auto
qed
lemma wpQ_is_pre: "⊢⇩2⇩' {wp⇩Q c Q} c { Q}"
proof (induction c arbitrary: Q)
case SKIP show ?case apply (auto intro: hoareQ.Skip) done
next
case Assign show ?case apply (auto intro:hoareQ.Assign) done
next
case Seq thus ?case by (auto intro:hoareQ.Seq)
next
case (If x1 c1 c2 Q) thus ?case
apply (auto intro!: hoareQ.If )
apply(rule hoareQ.conseq)
apply(auto)
apply(rule hoareQ.conseq)
apply(auto)
done
next
case (While b c)
show ?case
apply(rule conseq[where k=1])
apply(rule hoareQ.While[where I="%s. (if bval b s then wp⇩Q c (wp⇩Q (WHILE b DO c) Q) s else Q s)"])
apply(rule conseq[where k=1])
apply(rule While[of "wp⇩Q (WHILE b DO c) Q"])
apply(case_tac "bval b s")
apply(simp) apply(simp)
subgoal for s
apply(cases "bval b s")
using wpQ_WhileTrue apply simp
using wpQ_WhileFalse apply simp done
apply simp
subgoal for s
apply(cases "bval b s")
using wpQ_WhileTrue apply simp
using wpQ_WhileFalse apply simp done
apply(case_tac "bval b s")
apply(simp) apply(simp)
apply simp done
qed
lemma wpQ_is_pre': "⊢⇩2⇩' {wp⇩Q c (%s. enat k * Q s )} c {(%s. enat k * Q s )}"
using wpQ_is_pre by blast
lemma wpQ_is_weakestprePotential1: "⊨⇩2⇩' {P}c{Q} ⟹ (∃k>0. ∀s. wp⇩Q c (%s. enat k* Q s) s ≤ enat k * P s)"
apply(auto simp: hoare2o_valid_def wpQ_def)
proof (goal_cases)
case (1 k)
show ?case
proof (rule exI[where x=k], safe)
show "0<k" by fact
next
fix s t p i
assume "(c, s) ⇒ p ⇓ t" "enat k * Q t = enat i"
show "enat (↓⇩t (c, s)) + enat k * Q (↓⇩s (c, s)) ≤ enat k * P s"
proof (cases "P s < ∞")
case True
with 1 obtain t p' where i: "(c, s) ⇒ p' ⇓ t" and ii: "enat p' + enat k * Q t ≤ enat k * P s"
by auto
show ?thesis by(simp add: bigstepT_the_state[OF i] bigstepT_the_cost[OF i] ii)
next
case False
then show ?thesis
using 1 by auto
qed
next
fix s
assume "∀t. (∀p. ¬ (c, s) ⇒ p ⇓ t) ∨ enat k * Q t = ∞"
then show "enat k * P s = ∞" using 1 by force
qed
qed
theorem hoareQ_complete: "⊨⇩2⇩' {P}c{Q} ⟹ ⊢⇩2⇩' {P}c{ Q}"
proof -
assume "⊨⇩2⇩' {P}c{Q}"
with wpQ_is_weakestprePotential1 obtain k where "k>0"
and 1: "⋀s. wp⇩Q c (λs. enat k * Q s) s ≤ enat k * P s" by blast
show "⊢⇩2⇩' {P}c{Q}"
apply(rule conseq[OF wpQ_is_pre'])
apply(fact 1)
apply simp by fact
qed
theorem hoareQ_complete': "⊨⇩2⇩' {P}c{Q} ⟹ ⊢⇩2⇩' {P}c{ Q}"
unfolding hoare2o_valid_def
proof -
assume "∃k>0. ∀s. P s < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * Q t ≤ enat k * P s)"
then obtain k where f: "∀s. P s < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * Q t ≤ enat k * P s)" and k: "k>0" by auto
show "⊢⇩2⇩' {P}c{ Q}"
apply(rule conseq[OF wpQ_is_pre', where Q'=Q, simplified, where k1=k and k=k and Q1=Q])
unfolding wpQ_def
subgoal for s
proof(cases "P s < ∞")
case True
with f obtain t p' where i: "(c, s) ⇒ p' ⇓ t" and ii: "enat p' + enat k * Q t ≤ enat k * P s"
by auto
from ii k True have iii: "enat k * Q t < ∞"
using imult_is_infinity by fastforce
have kla: "∃t p. (c, s) ⇒ p ⇓ t ∧ enat k * Q t < ∞"
using iii i by auto
show ?thesis unfolding bigstepT_the_state[OF i]
unfolding bigstepT_the_cost[OF i]
apply(simp only: kla) using ii by simp
next
case False
then show ?thesis using k by auto
qed
subgoal by auto
using k by auto
qed
corollary hoareQ_sound_complete: " ⊢⇩2⇩' {P}c{Q} ⟷ ⊨⇩2⇩' {P}c{ Q}"
by (metis hoareQ_sound hoareQ_complete)
subsection "Example"
lemma fixes X::int assumes "0 < X" shows
Z: "eSuc (enat (nat (2 * X) * nat (2 * X))) ≤ enat (5 * (nat (X * X)))"
proof -
from assms have nn: "0 ≤ X" by auto
from assms have "0 < nat X" by auto
then have "0 < enat (nat X)" by (simp add: zero_enat_def)
then have A: "eSuc 0 ≤ enat (nat X)" using ileI1
by blast
have " (nat X) ≤ (nat (X*X))" using nn nat_mult_distrib by auto
then have D: "enat (nat X) ≤ enat (nat (X*X))" by auto
have C: "(enat (nat (2 * X) * nat (2 * X))) = 4* enat (nat (X * X))"
using nn nat_mult_distrib
by (simp add: numeral_eq_enat)
have "eSuc (enat (nat (2 * X) * nat (2 * X)))
= eSuc 0 + (enat (nat (2 * X) * nat (2 * X)))"
using one_eSuc plus_1_eSuc(1) by auto
also have "… ≤ enat (nat X) + (enat (nat (2 * X) * nat (2 * X)))"
using A add_right_mono by blast
also have "… ≤ enat (nat X) + 4* enat (nat (X * X))" using C by auto
also have "… ≤ enat (nat (X * X)) + 4* enat (nat (X * X))" using D by auto
also have "… = 5* enat (nat (X * X))"
by (metis eSuc_numeral mult_eSuc semiring_norm(5))
also have "… = enat ( 5* nat (X * X))"
by (simp add: numeral_eq_enat)
finally
show ?thesis .
qed
lemma weakenpre: "⟦ ⊢⇩2⇩' {P}c{Q} ; (∀s. P s ≤ P' s) ⟧ ⟹
⊢⇩2⇩' {P'}c{ Q}" using conseq[where Q'=Q and k=1]
by auto
lemma whileDecr: "⊢⇩2⇩' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO (SKIP;; SKIP;; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}"
apply(rule conseq[where k=4])
apply(rule While[where I="%s. enat 4 * (enat (nat (s ''x'')))"])
prefer 2
subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
apply(rule Seq[where P⇩2="wp⇩Q (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 4 * enat (nat (t ''x'')) + 1)"])
apply(simp)
apply(rule Seq[where P⇩2="wp⇩Q (SKIP) (λs. eSuc (enat (4 * nat (s ''x'' - 1)) + 1))"])
apply simp
subgoal apply(rule weakenpre) apply(rule Skip) apply auto
subgoal for s apply(cases "s ''x'' > 0") apply auto
apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
done
subgoal apply simp apply(rule Skip) done
subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp
apply simp
subgoal for s apply(cases "s ''x'' > 0") by auto
by simp
lemma whileDecrIf: "⊢⇩2⇩' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO ( (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP );; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}"
apply(rule conseq[OF While, where k=6 and I1="%s. enat 6 * (enat (nat (s ''x'')))"])
prefer 2
subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
apply(rule Seq[where P⇩2="wp⇩Q (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 6 * enat (nat (t ''x'')) + 1)"])
apply(simp)
apply(rule weakenpre)
apply(rule If[where P="wp⇩Q (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP ) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
subgoal
apply simp
apply(rule Seq[where P⇩2="wp⇩Q (SKIP) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
subgoal apply(rule weakenpre) apply(rule Skip) by auto
subgoal apply(rule weakenpre) apply(rule Skip) by auto
done
subgoal
apply simp
subgoal apply(rule weakenpre) apply(rule Skip) by auto
done
subgoal
apply auto
subgoal for s apply(cases "s ''x'' > 0") apply auto
apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
subgoal for s apply(cases "s ''x'' > 0") apply auto
apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
done
subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp
apply simp
subgoal for s apply(cases "s ''x'' > 0") by auto
by simp
lemma whileDecrIf2: "⊢⇩2⇩' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO ( (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP );; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}"
apply(rule conseq[OF While, where k=6 and I1="%s. enat 6 * (enat (nat (s ''x'')))"])
apply(rule Seq[where P⇩2="wp⇩Q (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 6 * enat (nat (t ''x'')) + 1)"])
apply(simp)
apply(rule weakenpre)
apply(rule If[where P="wp⇩Q (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP ) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
subgoal
apply simp
apply(rule Seq[where P⇩2="wp⇩Q (SKIP) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
subgoal apply(rule weakenpre) apply(rule Skip) by auto
subgoal apply(rule weakenpre) apply(rule Skip) by auto
done
subgoal
apply simp
subgoal apply(rule weakenpre) apply(rule Skip) by auto
done
prefer 2
subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp
subgoal
apply auto
subgoal for s apply(cases "s ''x'' > 0") apply auto
apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
subgoal for s apply(cases "s ''x'' > 0") apply auto
apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
done
subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
subgoal for s apply(cases "s ''x'' > 0") by auto
by simp
end