header "Hoare Logics for 1 Procedure"
theory PLang imports Main begin
subsection{* The language *}
typedecl state
type_synonym bexp = "state => bool"
datatype com = Do "(state => state set)"
| Semi com com ("_; _" [60, 60] 10)
| Cond bexp com com ("IF _ THEN _ ELSE _" 60)
| While bexp com ("WHILE _ DO _" 60)
| CALL
| Local "(state => state)" com "(state => state => state)"
("LOCAL _; _; _" [0,0,60] 60)
text{*\noindent There is only one parameterless procedure in the program. Hence
@{term CALL} does not even need to mention the procedure name. There
is no separate syntax for procedure declarations. Instead we declare a HOL
constant that represents the body of the one procedure in the program.*}
consts body :: com
text{*\noindent
As before, command execution is described by transitions
@{text"s -c-> t"}. The only new rule is the one for @{term CALL} ---
it requires no comment:*}
inductive
exec :: "state => com => state => bool" ("_/ -_->/ _" [50,0,50] 50)
where
Do: "t ∈ f s ==> s -Do f-> t"
| Semi: "[| s0 -c1-> s1; s1 -c2-> s2 |]
==> s0 -c1;c2-> s2"
| IfTrue: "[| b s; s -c1-> t |] ==> s -IF b THEN c1 ELSE c2-> t"
| IfFalse: "[| ¬b s; s -c2-> t |] ==> s -IF b THEN c1 ELSE c2-> t"
| WhileFalse: "¬b s ==> s -WHILE b DO c-> s"
| WhileTrue: "[| b s; s -c-> t; t -WHILE b DO c-> u |]
==> s -WHILE b DO c-> u"
| "s -body-> t ==> s -CALL-> t"
| Local: "f s -c-> t ==> s -LOCAL f; c; g-> g s t"
lemma [iff]: "(s -Do f-> t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)
lemma [iff]: "(s -c;d-> u) = (∃t. s -c-> t ∧ t -d-> u)"
by(auto elim: exec.cases intro:exec.intros)
lemma [iff]: "(s -IF b THEN c ELSE d-> t) =
(s -if b s then c else d-> t)"
apply(rule iffI)
apply(auto elim: exec.cases intro:exec.intros)
apply(auto intro:exec.intros split:split_if_asm)
done
lemma unfold_while:
"(s -WHILE b DO c-> u) =
(s -IF b THEN c;WHILE b DO c ELSE Do(λs. {s})-> u)"
by(auto elim: exec.cases intro:exec.intros split:split_if_asm)
lemma [iff]: "(s -CALL-> t) = (s -body-> t)"
by(blast elim: exec.cases intro:exec.intros)
lemma [iff]: "(s -LOCAL f; c; g-> u) = (∃t. f s -c-> t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)
lemma [simp]: "¬b s ==> s -WHILE b DO c-> s"
by(fast intro:exec.intros)
lemma WhileI: "[|b s; s -c-> t; t -WHILE b DO c-> u|] ==> s -WHILE b DO c-> u"
by(fastforce elim:exec.WhileTrue)
text{*This semantics turns out not to be fine-grained
enough. The soundness proof for the Hoare logic below proceeds by
induction on the call depth during execution. To make this work we
define a second semantics \mbox{@{text"s -c-n-> t"}} which expresses that the
execution uses at most @{term n} nested procedure invocations, where
@{term n} is a natural number. The rules are straightforward: @{term
n} is just passed around, except for procedure calls, where it is
decremented: *}
inductive
execn :: "state => com => nat => state => bool" ("_/ -_-_->/ _" [50,0,0,50] 50)
where
"t ∈ f s ==> s -Do f-n-> t"
| "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==> s0 -c1;c2-n-> s2"
| "[| b s; s -c1-n-> t |] ==> s -IF b THEN c1 ELSE c2-n-> t"
| "[| ¬b s; s -c2-n-> t |] ==> s -IF b THEN c1 ELSE c2-n-> t"
| WhileFalse:"¬b s ==> s -WHILE b DO c-n-> s"
| WhileTrue:"[|b s; s -c-n-> t; t -WHILE b DO c-n-> u|] ==> s -WHILE b DO c-n-> u"
| "s -body-n-> t ==> s -CALL-Suc n-> t"
| "f s -c-n-> t ==> s -LOCAL f; c; g-n-> g s t"
lemma [iff]: "(s -Do f-n-> t) = (t ∈ f s)"
by(auto elim: execn.cases intro:execn.intros)
lemma [iff]: "(s -c1;c2-n-> u) = (∃t. s -c1-n-> t ∧ t -c2-n-> u)"
by(best elim: execn.cases intro:execn.intros)
lemma [iff]: "(s -IF b THEN c ELSE d-n-> t) =
(s -if b s then c else d-n-> t)"
apply auto
apply(blast elim: execn.cases intro:execn.intros)+
done
lemma [iff]: "(s -CALL- 0-> t) = False"
by(blast elim: execn.cases intro:execn.intros)
lemma [iff]: "(s -CALL-Suc n-> t) = (s -body-n-> t)"
by(blast elim: execn.cases intro:execn.intros)
lemma [iff]: "(s -LOCAL f; c; g-n-> u) = (∃t. f s -c-n-> t ∧ u = g s t)"
by(auto elim: execn.cases intro:execn.intros)
text{*\noindent By induction on @{prop"s -c-m-> t"} we show
monotonicity w.r.t.\ the call depth:*}
lemma exec_mono[rule_format]: "s -c-m-> t ==> ∀n. m ≤ n --> s -c-n-> t"
apply(erule execn.induct)
apply(blast)
apply(blast)
apply(simp)
apply(simp)
apply(simp add:execn.intros)
apply(blast intro:execn.intros)
apply(clarify)
apply(rename_tac m)
apply(case_tac m)
apply simp
apply simp
apply blast
done
text{*\noindent With the help of this lemma we prove the expected
relationship between the two semantics: *}
lemma exec_iff_execn: "(s -c-> t) = (∃n. s -c-n-> t)"
apply(rule iffI)
apply(erule exec.induct)
apply blast
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply(fastforce intro:exec.intros exec_mono simp add:max_def)
apply fastforce
apply fastforce
apply(blast intro:execn.intros)
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
apply blast
apply blast
apply(erule exE, erule execn.induct)
apply blast
apply blast
apply fastforce
apply fastforce
apply(erule exec.WhileFalse)
apply(blast intro: exec.intros)
apply blast
apply blast
done
lemma while_lemma[rule_format]:
"s -w-n-> t ==> !b c. w = WHILE b DO c ∧ P s ∧
(!s s'. P s ∧ b s ∧ s -c-n-> s' --> P s') --> P t ∧ ¬b t"
apply(erule execn.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done
lemma while_rule:
"[|s -WHILE b DO c-n-> t; P s; !!s s'. [|P s; b s; s -c-n-> s' |] ==> P s'|]
==> P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done
end