(* Title: HOL/Isar_Examples/Hoare.thy Author: Makarius A formulation of Hoare logic suitable for Isar. *) section ‹Hoare Logic› theory Hoare imports Main begin subsection ‹Abstract syntax and semantics› text ‹ The following abstract syntax and semantics of Hoare Logic over ▩‹WHILE› programs closely follows the existing tradition in Isabelle/HOL of formalizing the presentation given in @{cite ‹\S6› "Winskel:1993"}. See also 🗀‹~~/src/HOL/Hoare› and @{cite "Nipkow:1998:Winskel"}. › type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" datatype 'a com = Basic "'a ⇒ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) | Cond "'a bexp" "'a com" "'a com" | While "'a bexp" "'a assn" "'a com" abbreviation Skip ("SKIP") where "SKIP ≡ Basic id" type_synonym 'a sem = "'a ⇒ 'a ⇒ bool" primrec iter :: "nat ⇒ 'a bexp ⇒ 'a sem ⇒ 'a sem" where "iter 0 b S s s' ⟷ s ∉ b ∧ s = s'" | "iter (Suc n) b S s s' ⟷ s ∈ b ∧ (∃s''. S s s'' ∧ iter n b S s'' s')" primrec Sem :: "'a com ⇒ 'a sem" where "Sem (Basic f) s s' ⟷ s' = f s" | "Sem (c1; c2) s s' ⟷ (∃s''. Sem c1 s s'' ∧ Sem c2 s'' s')" | "Sem (Cond b c1 c2) s s' ⟷ (if s ∈ b then Sem c1 s s' else Sem c2 s s')" | "Sem (While b x c) s s' ⟷ (∃n. iter n b (Sem c) s s')" definition Valid :: "'a bexp ⇒ 'a com ⇒ 'a bexp ⇒ bool" ("(3⊢ _/ (2_)/ _)" [100, 55, 100] 50) where "⊢ P c Q ⟷ (∀s s'. Sem c s s' ⟶ s ∈ P ⟶ s' ∈ Q)" lemma ValidI [intro?]: "(⋀s s'. Sem c s s' ⟹ s ∈ P ⟹ s' ∈ Q) ⟹ ⊢ P c Q" by (simp add: Valid_def) lemma ValidD [dest?]: "⊢ P c Q ⟹ Sem c s s' ⟹ s ∈ P ⟹ s' ∈ Q" by (simp add: Valid_def) subsection ‹Primitive Hoare rules› text ‹ From the semantics defined above, we derive the standard set of primitive Hoare rules; e.g.\ see @{cite ‹\S6› "Winskel:1993"}. Usually, variant forms of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. ┉ The ‹basic› rule represents any kind of atomic access to the state space. This subsumes the common rules of ‹skip› and ‹assign›, as formulated in \S\ref{sec:hoare-isar}. › theorem basic: "⊢ {s. f s ∈ P} (Basic f) P" proof fix s s' assume s: "s ∈ {s. f s ∈ P}" assume "Sem (Basic f) s s'" then have "s' = f s" by simp with s show "s' ∈ P" by simp qed text ‹ The rules for sequential commands and semantic consequences are established in a straight forward manner as follows. › theorem seq: "⊢ P c1 Q ⟹ ⊢ Q c2 R ⟹ ⊢ P (c1; c2) R" proof assume cmd1: "⊢ P c1 Q" and cmd2: "⊢ Q c2 R" fix s s' assume s: "s ∈ P" assume "Sem (c1; c2) s s'" then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'" by auto from cmd1 sem1 s have "s'' ∈ Q" .. with cmd2 sem2 show "s' ∈ R" .. qed theorem conseq: "P' ⊆ P ⟹ ⊢ P c Q ⟹ Q ⊆ Q' ⟹ ⊢ P' c Q'" proof assume P'P: "P' ⊆ P" and QQ': "Q ⊆ Q'" assume cmd: "⊢ P c Q" fix s s' :: 'a assume sem: "Sem c s s'" assume "s ∈ P'" with P'P have "s ∈ P" .. with cmd sem have "s' ∈ Q" .. with QQ' show "s' ∈ Q'" .. qed text ‹ The rule for conditional commands is directly reflected by the corresponding semantics; in the proof we just have to look closely which cases apply. › theorem cond: assumes case_b: "⊢ (P ∩ b) c1 Q" and case_nb: "⊢ (P ∩ -b) c2 Q" shows "⊢ P (Cond b c1 c2) Q" proof fix s s' assume s: "s ∈ P" assume sem: "Sem (Cond b c1 c2) s s'" show "s' ∈ Q" proof cases assume b: "s ∈ b" from case_b show ?thesis proof from sem b show "Sem c1 s s'" by simp from s b show "s ∈ P ∩ b" by simp qed next assume nb: "s ∉ b" from case_nb show ?thesis proof from sem nb show "Sem c2 s s'" by simp from s nb show "s ∈ P ∩ -b" by simp qed qed qed text ‹ The ‹while› rule is slightly less trivial --- it is the only one based on recursion, which is expressed in the semantics by a Kleene-style least fixed-point construction. The auxiliary statement below, which is by induction on the number of iterations is the main point to be proven; the rest is by routine application of the semantics of ▩‹WHILE›. › theorem while: assumes body: "⊢ (P ∩ b) c P" shows "⊢ P (While b X c) (P ∩ -b)" proof fix s s' assume s: "s ∈ P" assume "Sem (While b X c) s s'" then obtain n where "iter n b (Sem c) s s'" by auto from this and s show "s' ∈ P ∩ -b" proof (induct n arbitrary: s) case 0 then show ?case by auto next case (Suc n) then obtain s'' where b: "s ∈ b" and sem: "Sem c s s''" and iter: "iter n b (Sem c) s'' s'" by auto from Suc and b have "s ∈ P ∩ b" by simp with body sem have "s'' ∈ P" .. with iter show ?case by (rule Suc) qed qed subsection ‹Concrete syntax for assertions› text ‹ We now introduce concrete syntax for describing commands (with embedded expressions) and assertions. The basic technique is that of semantic ``quote-antiquote''. A ∗‹quotation› is a syntactic entity delimited by an implicit abstraction, say over the state space. An ∗‹antiquotation› is a marked expression within a quotation that refers the implicit argument; a typical antiquotation would select (or even update) components from the state. We will see some examples later in the concrete rules and applications. ┉ The following specification of syntax and translations is for Isabelle experts only; feel free to ignore it. While the first part is still a somewhat intelligible specification of the concrete syntactic representation of our Hoare language, the actual ``ML drivers'' is quite involved. Just note that the we re-use the basic quote/antiquote translations as already defined in Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},). › syntax "_quote" :: "'b ⇒ ('a ⇒ 'b)" "_antiquote" :: "('a ⇒ 'b) ⇒ 'b" ("´_" [1000] 1000) "_Subst" :: "'a bexp ⇒ 'b ⇒ idt ⇒ 'a bexp" ("_[_'/´_]" [1000] 999) "_Assert" :: "'a ⇒ 'a set" ("(⦃_⦄)" [0] 1000) "_Assign" :: "idt ⇒ 'b ⇒ 'a com" ("(´_ :=/ _)" [70, 65] 61) "_Cond" :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a com" ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) "_While_inv" :: "'a bexp ⇒ 'a assn ⇒ 'a com ⇒ 'a com" ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) "_While" :: "'a bexp ⇒ 'a com ⇒ 'a com" ("(0WHILE _ //DO _ /OD)" [0, 0] 61) translations "⦃b⦄" ⇀ "CONST Collect (_quote b)" "B [a/´x]" ⇀ "⦃´(_update_name x (λ_. a)) ∈ B⦄" "´x := a" ⇀ "CONST Basic (_quote (´(_update_name x (λ_. a))))" "IF b THEN c1 ELSE c2 FI" ⇀ "CONST Cond ⦃b⦄ c1 c2" "WHILE b INV i DO c OD" ⇀ "CONST While ⦃b⦄ i c" "WHILE b DO c OD" ⇌ "WHILE b INV CONST undefined DO c OD" parse_translation ‹ let fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, K quote_tr)] end › text ‹ As usual in Isabelle syntax translations, the part for printing is more complicated --- we cannot express parts as macro rules as above. Don't look here, unless you have to do similar things for yourself. › print_translation ‹ let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | quote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = quote_tr' (Syntax.const name) (t :: ts) | bexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; in [(@{const_syntax Collect}, K assert_tr'), (@{const_syntax Basic}, K assign_tr'), (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})), (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))] end › subsection ‹Rules for single-step proof \label{sec:hoare-isar}› text ‹ We are now ready to introduce a set of Hoare rules to be used in single-step structured proofs in Isabelle/Isar. We refer to the concrete syntax introduce above. ┉ Assertions of Hoare Logic may be manipulated in calculational proofs, with the inclusion expressed in terms of sets or predicates. Reversed order is supported as well. › lemma [trans]: "⊢ P c Q ⟹ P' ⊆ P ⟹ ⊢ P' c Q" by (unfold Valid_def) blast lemma [trans] : "P' ⊆ P ⟹ ⊢ P c Q ⟹ ⊢ P' c Q" by (unfold Valid_def) blast lemma [trans]: "Q ⊆ Q' ⟹ ⊢ P c Q ⟹ ⊢ P c Q'" by (unfold Valid_def) blast lemma [trans]: "⊢ P c Q ⟹ Q ⊆ Q' ⟹ ⊢ P c Q'" by (unfold Valid_def) blast lemma [trans]: "⊢ ⦃´P⦄ c Q ⟹ (⋀s. P' s ⟶ P s) ⟹ ⊢ ⦃´P'⦄ c Q" by (simp add: Valid_def) lemma [trans]: "(⋀s. P' s ⟶ P s) ⟹ ⊢ ⦃´P⦄ c Q ⟹ ⊢ ⦃´P'⦄ c Q" by (simp add: Valid_def) lemma [trans]: "⊢ P c ⦃´Q⦄ ⟹ (⋀s. Q s ⟶ Q' s) ⟹ ⊢ P c ⦃´Q'⦄" by (simp add: Valid_def) lemma [trans]: "(⋀s. Q s ⟶ Q' s) ⟹ ⊢ P c ⦃´Q⦄ ⟹ ⊢ P c ⦃´Q'⦄" by (simp add: Valid_def) text ‹ Identity and basic assignments.⁋‹The ‹hoare› method introduced in \S\ref{sec:hoare-vcg} is able to provide proper instances for any number of basic assignments, without producing additional verification conditions.› › lemma skip [intro?]: "⊢ P SKIP P" proof - have "⊢ {s. id s ∈ P} SKIP P" by (rule basic) then show ?thesis by simp qed lemma assign: "⊢ P [´a/´x::'a] ´x := ´a P" by (rule basic) text ‹ Note that above formulation of assignment corresponds to our preferred way to model state spaces, using (extensible) record types in HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field ‹x›, Isabelle/HOL provides a functions ‹x› (selector) and ‹x_update› (update). Above, there is only a place-holder appearing for the latter kind of function: due to concrete syntax ‹´x := ´a› also contains ‹x_update›.⁋‹Note that due to the external nature of HOL record fields, we could not even state a general theorem relating selector and update functions (if this were required here); this would only work for any particular instance of record fields introduced so far.› ┉ Sequential composition --- normalizing with associativity achieves proper of chunks of code verified separately. › lemmas [trans, intro?] = seq lemma seq_assoc [simp]: "⊢ P c1;(c2;c3) Q ⟷ ⊢ P (c1;c2);c3 Q" by (auto simp add: Valid_def) text ‹Conditional statements.› lemmas [trans, intro?] = cond lemma [trans, intro?]: "⊢ ⦃´P ∧ ´b⦄ c1 Q ⟹ ⊢ ⦃´P ∧ ¬ ´b⦄ c2 Q ⟹ ⊢ ⦃´P⦄ IF ´b THEN c1 ELSE c2 FI Q" by (rule cond) (simp_all add: Valid_def) text ‹While statements --- with optional invariant.› lemma [intro?]: "⊢ (P ∩ b) c P ⟹ ⊢ P (While b P c) (P ∩ -b)" by (rule while) lemma [intro?]: "⊢ (P ∩ b) c P ⟹ ⊢ P (While b undefined c) (P ∩ -b)" by (rule while) lemma [intro?]: "⊢ ⦃´P ∧ ´b⦄ c ⦃´P⦄ ⟹ ⊢ ⦃´P⦄ WHILE ´b INV ⦃´P⦄ DO c OD ⦃´P ∧ ¬ ´b⦄" by (simp add: while Collect_conj_eq Collect_neg_eq) lemma [intro?]: "⊢ ⦃´P ∧ ´b⦄ c ⦃´P⦄ ⟹ ⊢ ⦃´P⦄ WHILE ´b DO c OD ⦃´P ∧ ¬ ´b⦄" by (simp add: while Collect_conj_eq Collect_neg_eq) subsection ‹Verification conditions \label{sec:hoare-vcg}› text ‹ We now load the ∗‹original› ML file for proof scripts and tactic definition for the Hoare Verification Condition Generator (see 🗀‹~~/src/HOL/Hoare›). As far as we are concerned here, the result is a proof method ‹hoare›, which may be applied to a Hoare Logic assertion to extract purely logical verification conditions. It is important to note that the method requires ▩‹WHILE› loops to be fully annotated with invariants beforehand. Furthermore, only ∗‹concrete› pieces of code are handled --- the underlying tactic fails ungracefully if supplied with meta-variables or parameters, for example. › lemma SkipRule: "p ⊆ q ⟹ Valid p (Basic id) q" by (auto simp add: Valid_def) lemma BasicRule: "p ⊆ {s. f s ∈ q} ⟹ Valid p (Basic f) q" by (auto simp: Valid_def) lemma SeqRule: "Valid P c1 Q ⟹ Valid Q c2 R ⟹ Valid P (c1;c2) R" by (auto simp: Valid_def) lemma CondRule: "p ⊆ {s. (s ∈ b ⟶ s ∈ w) ∧ (s ∉ b ⟶ s ∈ w')} ⟹ Valid w c1 q ⟹ Valid w' c2 q ⟹ Valid p (Cond b c1 c2) q" by (auto simp: Valid_def) lemma iter_aux: "∀s s'. Sem c s s' ⟶ s ∈ I ∧ s ∈ b ⟶ s' ∈ I ⟹ (⋀s s'. s ∈ I ⟹ iter n b (Sem c) s s' ⟹ s' ∈ I ∧ s' ∉ b)" by (induct n) auto lemma WhileRule: "p ⊆ i ⟹ Valid (i ∩ b) c i ⟹ i ∩ (-b) ⊆ q ⟹ Valid p (While b i c) q" apply (clarsimp simp: Valid_def) apply (drule iter_aux) prefer 2 apply assumption apply blast apply blast done lemma Compl_Collect: "- Collect b = {x. ¬ b x}" by blast lemmas AbortRule = SkipRule ― ‹dummy version› ML_file "~~/src/HOL/Hoare/hoare_tac.ML" method_setup hoare = ‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (Hoare.hoare_tac ctxt (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))› "verification condition generator for Hoare logic" end