Quelle  Hoare.thy

(*  Title:      HOL/Isar_Examples/Hoare.thy
  Author: Makarius
 
 A formulation of Hoare logic suitable for Isar.
*)

section ‹Hoare Logic›

theory Hoare
  imports "HOL-Hoare.Hoare_Tac"
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 🍋‹‹\S6› in "Winskel:1993"›. See also
  🍋‹~~/src/HOL/Hoare› and 🍋‹"Nipkow:1998:Winskel"›.
 ›

type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
type_synonym 'a var = "'a ==> nat"

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 var" "'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 y 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 🍋‹‹\S6› in "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 Y c) (P ∩ -b)"
proof
  fix s s' assume s: "s ∈ P"
  assume "Sem (While b X Y 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 🪙‹Syntax_Trans.quote_tr›, and 🪙‹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 (λ_. 0) 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 🍋‹_antiquote› t
  | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(🍋‹_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' 🍋‹_antiquote› t, ts)
  | quote_tr' _ _ = raise Match;
 
  val assert_tr' = quote_tr' (Syntax.const 🍋‹_Assert›);
 
  fun bexp_tr' name ((Const (🍋‹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 🍋‹_Assign› $ Syntax_Trans.update_name_tr' f)
  (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
  | assign_tr' _ = raise Match;
  in
  [(🍋‹Collect›, K assert_tr'),
  (🍋‹Basic›, K assign_tr'),
  (🍋‹Cond›, K (bexp_tr' 🍋‹_Cond›)),
  (🍋‹While›, K (bexp_tr' 🍋‹_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 🍋‹"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 V c) (P ∩ -b)"
  by (rule while)

lemma [intro?]: "⊨ (P ∩ b) c P ==> ⊨ P (While b undefined V 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 v c) q"
  apply (clarsimp simp: Valid_def)
  apply (drule iter_aux)
    prefer 2
    apply assumption
   apply blast
  apply blast
  done

declare BasicRule [Hoare_Tac.BasicRule]
  and SkipRule [Hoare_Tac.SkipRule]
  and SeqRule [Hoare_Tac.SeqRule]
  and CondRule [Hoare_Tac.CondRule]
  and WhileRule [Hoare_Tac.WhileRule]

method_setup hoare =
  ‹Scan.succeed (fn ctxt =>
  (SIMPLE_METHOD'
  (Hoare_Tac.hoare_tac ctxt
  (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))›
  "verification condition generator for Hoare logic"

end