(* Author: Tobias Nipkow *)
subsubsection
"\nat\-Indexed Invariant"
theory Hoare_Total_EX
imports Hoare
begin
text‹This
is the standard set of rules that you find
in many publications.
The While-rule
is different
from the one
in Concrete Semantics
in that the
invariant
is indexed
by natural numbers
and goes down
by 1
with
every iteration. The completeness
proof is easier but the rule
is harder
to apply in program proofs.
›
definition hoare_tvalid ::
"assn \ com \ assn \ bool"
(
‹⊨🚫t {(1_)}/ (_)/ {(1_)}
› 50)
where
"\\<^sub>t {P}c{Q} \ (\s. P s \ (\t. (c,s) \ t \ Q t))"
inductive
hoaret ::
"assn \ com \ assn \ bool" (
‹⊨🚫t ({(1_)}/ (_)/ {(1_)})
› 50)
where
Skip:
"\\<^sub>t {P} SKIP {P}" |
Assign:
"\\<^sub>t {\s. P(s[a/x])} x::=a {P}" |
Seq:
"\ \\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \ \ \\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |
If:
"\ \\<^sub>t {\s. P s \ bval b s} c\<^sub>1 {Q}; \\<^sub>t {\s. P s \ \ bval b s} c\<^sub>2 {Q} \
==> ⊨🚫t {P}
IF b
THEN c
🚫1 ELSE c
🚫2 {Q}
" |
While:
"\ \n::nat. \\<^sub>t {P (Suc n)} c {P n};
∀n s. P (Suc n) s
⟶ bval b s;
∀s. P 0 s
⟶ ¬ bval b s
]
==> ⊨🚫t {λs.
∃n. P n s} WHILE b DO c {P 0}
" |
conseq:
"\ \s. P' s \ P s; \\<^sub>t {P}c{Q}; \s. Q s \ Q' s \ \
⊨🚫t {P
'}c{Q'}
"
text‹Building
in the consequence rule:
›
lemma strengthen_pre:
"\ \s. P' s \ P s; \\<^sub>t {P} c {Q} \ \ \\<^sub>t {P'} c {Q}"
by (metis conseq)
lemma weaken_post:
"\ \\<^sub>t {P} c {Q}; \s. Q s \ Q' s \ \ \\<^sub>t {P} c {Q'}"
by (metis conseq)
lemma Assign
': "\s. P s \ Q(s[a/x]) \ \\<^sub>t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
text‹The soundness
theorem:
›
theorem hoaret_sound:
"\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}"
proof(unfold hoare_tvalid_def,
induction rule: hoaret.induct)
case (While P c b)
have "P n s \ \t. (WHILE b DO c, s) \ t \ P 0 t" for n s
proof(
induction "n" arbitrary: s)
case 0
thus ?
case using While.hyps(3) WhileFalse
by blast
next
case Suc
thus ?
case by (meson While.IH While.hyps(2) WhileTrue)
qed
thus ?
case by auto
next
case If thus ?
case by auto blast
qed fastforce+
definition wpt ::
"com \ assn \ assn" (
‹wp
🚫t
›)
where
"wp\<^sub>t c Q = (\s. \t. (c,s) \ t \ Q t)"
lemma [simp]:
"wp\<^sub>t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)
lemma [simp]:
"wp\<^sub>t (x ::= e) Q = (\s. Q(s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)
lemma [simp]:
"wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done
lemma [simp]:
"wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
apply(unfold wpt_def)
apply(rule ext)
apply auto
done
text‹Function ‹wpw
› computes the weakest precondition of a While-loop
that
is unfolded a fixed number of times.
›
fun wpw ::
"bexp \ com \ nat \ assn \ assn" where
"wpw b c 0 Q s = (\ bval b s \ Q s)" |
"wpw b c (Suc n) Q s = (bval b s \ (\s'. (c,s) \ s' \ wpw b c n Q s'))"
lemma WHILE_Its:
"(WHILE b DO c,s) \ t \ Q t \ \n. wpw b c n Q s"
proof(
induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse
thus ?
case using wpw.simps(1)
by blast
next
case WhileTrue
thus ?
case using wpw.simps(2)
by blast
qed
lemma wpt_is_pre:
"\\<^sub>t {wp\<^sub>t c Q} c {Q}"
proof (
induction c arbitrary: Q)
case SKIP
show ?
case by (auto intro:hoaret.Skip)
next
case Assign
show ?
case by (auto intro:hoaret.Assign)
next
case Seq
thus ?
case by (auto intro:hoaret.Seq)
next
case If thus ?
case by (auto intro:hoaret.
If hoaret.conseq)
next
case (While b c)
let ?w =
"WHILE b DO c"
have c1:
"\s. wp\<^sub>t ?w Q s \ (\n. wpw b c n Q s)"
unfolding wpt_def
by (metis WHILE_Its)
have c3:
"\s. wpw b c 0 Q s \ Q s" by simp
have w2:
"\n s. wpw b c (Suc n) Q s \ bval b s" by simp
have w3:
"\s. wpw b c 0 Q s \ \ bval b s" by simp
have "\\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n
proof -
have *:
"\s. wpw b c (Suc n) Q s \ (\t. (c, s) \ t \ wpw b c n Q t)" by simp
show ?thesis
by(rule strengthen_pre[OF * While.IH[of
"wpw b c n Q", unfolded wpt_def]])
qed
from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
show ?
case .
qed
theorem hoaret_complete:
"\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done
corollary hoaret_sound_complete:
"\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}"
by (metis hoaret_sound hoaret_complete)
text ‹Two examples:
›
lemma "\\<^sub>t
{λs.
∃n. n = nat(s
''x
'')}
WHILE Less (N 0) (V
''x
'') DO
''x
'' ::= Plus (V
''x
'') (N (-1))
{λs. s
''x
'' ≤ 0}
"
apply(rule weaken_post)
apply(rule While)
apply(rule Assign
')
apply auto
done
lemma "\\<^sub>t
{λs.
∃n. n = nat(s
''x
'')}
WHILE Less (N 0) (V
''x
'')
DO (
''x
'' ::= Plus (V
''x
'') (N (-1));;
(
''y
'' ::= V
''x
'';;
WHILE Less (N 0) (V
''y
'') DO
''y
'' ::= Plus (V
''y
'') (N (-1))))
{λs. s
''x
'' ≤ 0}
"
apply(rule weaken_post)
apply(rule While)
defer
apply auto[3]
apply(rule Seq)
prefer 2
apply(rule Seq)
prefer 2
apply(rule weaken_post)
apply(rule_tac P =
"\m s. n = nat(s ''x'') \ m = nat(s ''y'')" in While)
apply(rule Assign
')
apply auto[4]
apply(rule Assign)
apply(rule Assign
')
apply auto
done
end
