author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63680 6e1e8b5abbfa
child 67443 3abf6a722518
permissions -rw-r--r--
     1 (*  Title:      HOL/Isar_Examples/Hoare.thy
     2     Author:     Makarius
     4 A formulation of Hoare logic suitable for Isar.
     5 *)
     7 section \<open>Hoare Logic\<close>
     9 theory Hoare
    10   imports Main
    11 begin
    13 subsection \<open>Abstract syntax and semantics\<close>
    15 text \<open>
    16   The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
    17   programs closely follows the existing tradition in Isabelle/HOL of
    18   formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
    19   \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
    20 \<close>
    22 type_synonym 'a bexp = "'a set"
    23 type_synonym 'a assn = "'a set"
    25 datatype 'a com =
    26     Basic "'a \<Rightarrow> 'a"
    27   | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
    28   | Cond "'a bexp" "'a com" "'a com"
    29   | While "'a bexp" "'a assn" "'a com"
    31 abbreviation Skip  ("SKIP")
    32   where "SKIP \<equiv> Basic id"
    34 type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    36 primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
    37   where
    38     "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
    39   | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
    41 primrec Sem :: "'a com \<Rightarrow> 'a sem"
    42   where
    43     "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
    44   | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
    45   | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
    46   | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
    48 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    49   where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
    51 lemma ValidI [intro?]: "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
    52   by (simp add: Valid_def)
    54 lemma ValidD [dest?]: "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
    55   by (simp add: Valid_def)
    58 subsection \<open>Primitive Hoare rules\<close>
    60 text \<open>
    61   From the semantics defined above, we derive the standard set of primitive
    62   Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, variant forms
    63   of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar}
    64   and \S\ref{sec:hoare-vcg}.
    66   \<^medskip>
    67   The \<open>basic\<close> rule represents any kind of atomic access to the state space.
    68   This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in
    69   \S\ref{sec:hoare-isar}.
    70 \<close>
    72 theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
    73 proof
    74   fix s s'
    75   assume s: "s \<in> {s. f s \<in> P}"
    76   assume "Sem (Basic f) s s'"
    77   then have "s' = f s" by simp
    78   with s show "s' \<in> P" by simp
    79 qed
    81 text \<open>
    82   The rules for sequential commands and semantic consequences are established
    83   in a straight forward manner as follows.
    84 \<close>
    86 theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
    87 proof
    88   assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
    89   fix s s'
    90   assume s: "s \<in> P"
    91   assume "Sem (c1; c2) s s'"
    92   then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
    93     by auto
    94   from cmd1 sem1 s have "s'' \<in> Q" ..
    95   with cmd2 sem2 show "s' \<in> R" ..
    96 qed
    98 theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
    99 proof
   100   assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
   101   assume cmd: "\<turnstile> P c Q"
   102   fix s s' :: 'a
   103   assume sem: "Sem c s s'"
   104   assume "s : P'" with P'P have "s \<in> P" ..
   105   with cmd sem have "s' \<in> Q" ..
   106   with QQ' show "s' \<in> Q'" ..
   107 qed
   109 text \<open>
   110   The rule for conditional commands is directly reflected by the corresponding
   111   semantics; in the proof we just have to look closely which cases apply.
   112 \<close>
   114 theorem cond:
   115   assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
   116     and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
   117   shows "\<turnstile> P (Cond b c1 c2) Q"
   118 proof
   119   fix s s'
   120   assume s: "s \<in> P"
   121   assume sem: "Sem (Cond b c1 c2) s s'"
   122   show "s' \<in> Q"
   123   proof cases
   124     assume b: "s \<in> b"
   125     from case_b show ?thesis
   126     proof
   127       from sem b show "Sem c1 s s'" by simp
   128       from s b show "s \<in> P \<inter> b" by simp
   129     qed
   130   next
   131     assume nb: "s \<notin> b"
   132     from case_nb show ?thesis
   133     proof
   134       from sem nb show "Sem c2 s s'" by simp
   135       from s nb show "s : P \<inter> -b" by simp
   136     qed
   137   qed
   138 qed
   140 text \<open>
   141   The \<open>while\<close> rule is slightly less trivial --- it is the only one based on
   142   recursion, which is expressed in the semantics by a Kleene-style least
   143   fixed-point construction. The auxiliary statement below, which is by
   144   induction on the number of iterations is the main point to be proven; the
   145   rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.
   146 \<close>
   148 theorem while:
   149   assumes body: "\<turnstile> (P \<inter> b) c P"
   150   shows "\<turnstile> P (While b X c) (P \<inter> -b)"
   151 proof
   152   fix s s' assume s: "s \<in> P"
   153   assume "Sem (While b X c) s s'"
   154   then obtain n where "iter n b (Sem c) s s'" by auto
   155   from this and s show "s' \<in> P \<inter> -b"
   156   proof (induct n arbitrary: s)
   157     case 0
   158     then show ?case by auto
   159   next
   160     case (Suc n)
   161     then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
   162       and iter: "iter n b (Sem c) s'' s'" by auto
   163     from Suc and b have "s \<in> P \<inter> b" by simp
   164     with body sem have "s'' \<in> P" ..
   165     with iter show ?case by (rule Suc)
   166   qed
   167 qed
   170 subsection \<open>Concrete syntax for assertions\<close>
   172 text \<open>
   173   We now introduce concrete syntax for describing commands (with embedded
   174   expressions) and assertions. The basic technique is that of semantic
   175   ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity delimited by an
   176   implicit abstraction, say over the state space. An \<^emph>\<open>antiquotation\<close> is a
   177   marked expression within a quotation that refers the implicit argument; a
   178   typical antiquotation would select (or even update) components from the
   179   state.
   181   We will see some examples later in the concrete rules and applications.
   183   \<^medskip>
   184   The following specification of syntax and translations is for Isabelle
   185   experts only; feel free to ignore it.
   187   While the first part is still a somewhat intelligible specification of the
   188   concrete syntactic representation of our Hoare language, the actual ``ML
   189   drivers'' is quite involved. Just note that the we re-use the basic
   190   quote/antiquote translations as already defined in Isabelle/Pure (see @{ML
   191   Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).
   192 \<close>
   194 syntax
   195   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   196   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"  ("\<acute>_" [1000] 1000)
   197   "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
   198   "_Assert" :: "'a \<Rightarrow> 'a set"  ("(\<lbrace>_\<rbrace>)" [0] 1000)
   199   "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"  ("(\<acute>_ :=/ _)" [70, 65] 61)
   200   "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
   201     ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   202   "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
   203     ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
   204   "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
   206 translations
   207   "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)"
   208   "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
   209   "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
   210   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   211   "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
   212   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
   214 parse_translation \<open>
   215   let
   216     fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
   217       | quote_tr ts = raise TERM ("quote_tr", ts);
   218   in [(@{syntax_const "_quote"}, K quote_tr)] end
   219 \<close>
   221 text \<open>
   222   As usual in Isabelle syntax translations, the part for printing is more
   223   complicated --- we cannot express parts as macro rules as above. Don't look
   224   here, unless you have to do similar things for yourself.
   225 \<close>
   227 print_translation \<open>
   228   let
   229     fun quote_tr' f (t :: ts) =
   230           Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
   231       | quote_tr' _ _ = raise Match;
   233     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   235     fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
   236           quote_tr' (Syntax.const name) (t :: ts)
   237       | bexp_tr' _ _ = raise Match;
   239     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   240           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
   241             (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   242       | assign_tr' _ = raise Match;
   243   in
   244    [(@{const_syntax Collect}, K assert_tr'),
   245     (@{const_syntax Basic}, K assign_tr'),
   246     (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
   247     (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
   248   end
   249 \<close>
   252 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
   254 text \<open>
   255   We are now ready to introduce a set of Hoare rules to be used in single-step
   256   structured proofs in Isabelle/Isar. We refer to the concrete syntax
   257   introduce above.
   259   \<^medskip>
   260   Assertions of Hoare Logic may be manipulated in calculational proofs, with
   261   the inclusion expressed in terms of sets or predicates. Reversed order is
   262   supported as well.
   263 \<close>
   265 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   266   by (unfold Valid_def) blast
   267 lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
   268   by (unfold Valid_def) blast
   270 lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
   271   by (unfold Valid_def) blast
   272 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
   273   by (unfold Valid_def) blast
   275 lemma [trans]:
   276     "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   277   by (simp add: Valid_def)
   278 lemma [trans]:
   279     "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   280   by (simp add: Valid_def)
   282 lemma [trans]:
   283     "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   284   by (simp add: Valid_def)
   285 lemma [trans]:
   286     "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   287   by (simp add: Valid_def)
   290 text \<open>
   291   Identity and basic assignments.\<^footnote>\<open>The \<open>hoare\<close> method introduced in
   292   \S\ref{sec:hoare-vcg} is able to provide proper instances for any number of
   293   basic assignments, without producing additional verification conditions.\<close>
   294 \<close>
   296 lemma skip [intro?]: "\<turnstile> P SKIP P"
   297 proof -
   298   have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
   299   then show ?thesis by simp
   300 qed
   302 lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   303   by (rule basic)
   305 text \<open>
   306   Note that above formulation of assignment corresponds to our preferred way
   307   to model state spaces, using (extensible) record types in HOL @{cite
   308   "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, Isabelle/HOL
   309   provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). Above, there is
   310   only a place-holder appearing for the latter kind of function: due to
   311   concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains \<open>x_update\<close>.\<^footnote>\<open>Note that due to the
   312   external nature of HOL record fields, we could not even state a general
   313   theorem relating selector and update functions (if this were required here);
   314   this would only work for any particular instance of record fields introduced
   315   so far.\<close>
   317   \<^medskip>
   318   Sequential composition --- normalizing with associativity achieves proper of
   319   chunks of code verified separately.
   320 \<close>
   322 lemmas [trans, intro?] = seq
   324 lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
   325   by (auto simp add: Valid_def)
   327 text \<open>Conditional statements.\<close>
   329 lemmas [trans, intro?] = cond
   331 lemma [trans, intro?]:
   332   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
   333       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
   334       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
   335     by (rule cond) (simp_all add: Valid_def)
   337 text \<open>While statements --- with optional invariant.\<close>
   339 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
   340   by (rule while)
   342 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
   343   by (rule while)
   346 lemma [intro?]:
   347   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   348     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   349   by (simp add: while Collect_conj_eq Collect_neg_eq)
   351 lemma [intro?]:
   352   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   353     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   354   by (simp add: while Collect_conj_eq Collect_neg_eq)
   357 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
   359 text \<open>
   360   We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
   361   for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>).
   362   As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which
   363   may be applied to a Hoare Logic assertion to extract purely logical
   364   verification conditions. It is important to note that the method requires
   365   \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand.
   366   Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying
   367   tactic fails ungracefully if supplied with meta-variables or parameters, for
   368   example.
   369 \<close>
   371 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   372   by (auto simp add: Valid_def)
   374 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
   375   by (auto simp: Valid_def)
   377 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
   378   by (auto simp: Valid_def)
   380 lemma CondRule:
   381   "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   382     \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   383   by (auto simp: Valid_def)
   385 lemma iter_aux:
   386   "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
   387        (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
   388   by (induct n) auto
   390 lemma WhileRule:
   391     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
   392   apply (clarsimp simp: Valid_def)
   393   apply (drule iter_aux)
   394     prefer 2
   395     apply assumption
   396    apply blast
   397   apply blast
   398   done
   400 lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
   401   by blast
   403 lemmas AbortRule = SkipRule  \<comment> "dummy version"
   405 ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
   407 method_setup hoare =
   408   \<open>Scan.succeed (fn ctxt =>
   409     (SIMPLE_METHOD'
   410       (Hoare.hoare_tac ctxt
   411         (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\<close>
   412   "verification condition generator for Hoare logic"
   414 end