header "Hoare Logics for Mutually Recursive Procedure"
theory PsLang imports Main begin
subsection{* The language *}
typedecl state
typedecl pname
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 pname
| Local "(state => state)" com "(state => state => state)"
("LOCAL _; _; _" [0,0,60] 60)
consts body :: "pname => com"
text{* We generalize from a single procedure to a whole set of
procedures following the ideas of von Oheimb~\cite{Oheimb-FSTTCS99}.
The basic setup is modified only in a few places:
\begin{itemize}
\item We introduce a new basic type @{typ pname} of procedure names.
\item Constant @{term body} is now of type @{typ"pname => com"}.
\item The @{term CALL} command now has an argument of type @{typ pname},
the name of the procedure that is to be called.
\end{itemize}
*}
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"
| Call: "s -body p-> t ==> s -CALL p-> 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 [iff]: "(s -CALL p-> t) = (s -body p-> 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)
inductive
execn :: "state => com => nat => state => bool" ("_/ -_-_->/ _" [50,0,0,50] 50)
where
Do: "t ∈ f s ==> s -Do f-n-> t"
| Semi: "[| s0 -c0-n-> s1; s1 -c1-n-> s2 |] ==> s0 -c0;c1-n-> s2"
| IfTrue: "[| b s; s -c0-n-> t |] ==> s -IF b THEN c0 ELSE c1-n-> t"
| IfFalse: "[| ¬b s; s -c1-n-> t |] ==> s -IF b THEN c0 ELSE c1-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"
| Call: "s -body p-n-> t ==> s -CALL p-Suc n-> t"
| Local: "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 p- 0-> t) = False"
by(blast elim: execn.cases intro:execn.intros)
lemma [iff]: "(s -CALL p-Suc n-> t) = (s -body p-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)
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
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