src/HOL/Isar_Examples/Hoare.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 35417 47ee18b6ae32 child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
     1 (*  Title:      HOL/Isar_Examples/Hoare.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3

     4 A formulation of Hoare logic suitable for Isar.

     5 *)

     6

     7 header {* Hoare Logic *}

     8

     9 theory Hoare

    10 imports Main

    11 uses ("~~/src/HOL/Hoare/hoare_tac.ML")

    12 begin

    13

    14 subsection {* Abstract syntax and semantics *}

    15

    16 text {*

    17  The following abstract syntax and semantics of Hoare Logic over

    18  \texttt{WHILE} programs closely follows the existing tradition in

    19  Isabelle/HOL of formalizing the presentation given in

    20  \cite[\S6]{Winskel:1993}.  See also

    21  \url{http://isabelle.in.tum.de/library/Hoare/} and

    22  \cite{Nipkow:1998:Winskel}.

    23 *}

    24

    25 types

    26   'a bexp = "'a set"

    27   'a assn = "'a set"

    28

    29 datatype 'a com =

    30     Basic "'a => 'a"

    31   | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)

    32   | Cond "'a bexp" "'a com" "'a com"

    33   | While "'a bexp" "'a assn" "'a com"

    34

    35 abbreviation

    36   Skip  ("SKIP") where

    37   "SKIP == Basic id"

    38

    39 types

    40   'a sem = "'a => 'a => bool"

    41

    42 consts

    43   iter :: "nat => 'a bexp => 'a sem => 'a sem"

    44 primrec

    45   "iter 0 b S s s' = (s ~: b & s = s')"

    46   "iter (Suc n) b S s s' =

    47     (s : b & (EX s''. S s s'' & iter n b S s'' s'))"

    48

    49 consts

    50   Sem :: "'a com => 'a sem"

    51 primrec

    52   "Sem (Basic f) s s' = (s' = f s)"

    53   "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"

    54   "Sem (Cond b c1 c2) s s' =

    55     (if s : b then Sem c1 s s' else Sem c2 s s')"

    56   "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"

    57

    58 definition Valid :: "'a bexp => 'a com => 'a bexp => bool" ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) where

    59   "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"

    60

    61 notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)

    62

    63 lemma ValidI [intro?]:

    64     "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"

    65   by (simp add: Valid_def)

    66

    67 lemma ValidD [dest?]:

    68     "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"

    69   by (simp add: Valid_def)

    70

    71

    72 subsection {* Primitive Hoare rules *}

    73

    74 text {*

    75  From the semantics defined above, we derive the standard set of

    76  primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.  Usually,

    77  variant forms of these rules are applied in actual proof, see also

    78  \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.

    79

    80  \medskip The \name{basic} rule represents any kind of atomic access

    81  to the state space.  This subsumes the common rules of \name{skip}

    82  and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.

    83 *}

    84

    85 theorem basic: "|- {s. f s : P} (Basic f) P"

    86 proof

    87   fix s s' assume s: "s : {s. f s : P}"

    88   assume "Sem (Basic f) s s'"

    89   hence "s' = f s" by simp

    90   with s show "s' : P" by simp

    91 qed

    92

    93 text {*

    94  The rules for sequential commands and semantic consequences are

    95  established in a straight forward manner as follows.

    96 *}

    97

    98 theorem seq: "|- P c1 Q ==> |- Q c2 R ==> |- P (c1; c2) R"

    99 proof

   100   assume cmd1: "|- P c1 Q" and cmd2: "|- Q c2 R"

   101   fix s s' assume s: "s : P"

   102   assume "Sem (c1; c2) s s'"

   103   then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"

   104     by auto

   105   from cmd1 sem1 s have "s'' : Q" ..

   106   with cmd2 sem2 show "s' : R" ..

   107 qed

   108

   109 theorem conseq: "P' <= P ==> |- P c Q ==> Q <= Q' ==> |- P' c Q'"

   110 proof

   111   assume P'P: "P' <= P" and QQ': "Q <= Q'"

   112   assume cmd: "|- P c Q"

   113   fix s s' :: 'a

   114   assume sem: "Sem c s s'"

   115   assume "s : P'" with P'P have "s : P" ..

   116   with cmd sem have "s' : Q" ..

   117   with QQ' show "s' : Q'" ..

   118 qed

   119

   120 text {*

   121  The rule for conditional commands is directly reflected by the

   122  corresponding semantics; in the proof we just have to look closely

   123  which cases apply.

   124 *}

   125

   126 theorem cond:

   127   "|- (P Int b) c1 Q ==> |- (P Int -b) c2 Q ==> |- P (Cond b c1 c2) Q"

   128 proof

   129   assume case_b: "|- (P Int b) c1 Q" and case_nb: "|- (P Int -b) c2 Q"

   130   fix s s' assume s: "s : P"

   131   assume sem: "Sem (Cond b c1 c2) s s'"

   132   show "s' : Q"

   133   proof cases

   134     assume b: "s : b"

   135     from case_b show ?thesis

   136     proof

   137       from sem b show "Sem c1 s s'" by simp

   138       from s b show "s : P Int b" by simp

   139     qed

   140   next

   141     assume nb: "s ~: b"

   142     from case_nb show ?thesis

   143     proof

   144       from sem nb show "Sem c2 s s'" by simp

   145       from s nb show "s : P Int -b" by simp

   146     qed

   147   qed

   148 qed

   149

   150 text {*

   151  The \name{while} rule is slightly less trivial --- it is the only one

   152  based on recursion, which is expressed in the semantics by a

   153  Kleene-style least fixed-point construction.  The auxiliary statement

   154  below, which is by induction on the number of iterations is the main

   155  point to be proven; the rest is by routine application of the

   156  semantics of \texttt{WHILE}.

   157 *}

   158

   159 theorem while:

   160   assumes body: "|- (P Int b) c P"

   161   shows "|- P (While b X c) (P Int -b)"

   162 proof

   163   fix s s' assume s: "s : P"

   164   assume "Sem (While b X c) s s'"

   165   then obtain n where "iter n b (Sem c) s s'" by auto

   166   from this and s show "s' : P Int -b"

   167   proof (induct n arbitrary: s)

   168     case 0

   169     thus ?case by auto

   170   next

   171     case (Suc n)

   172     then obtain s'' where b: "s : b" and sem: "Sem c s s''"

   173       and iter: "iter n b (Sem c) s'' s'"

   174       by auto

   175     from Suc and b have "s : P Int b" by simp

   176     with body sem have "s'' : P" ..

   177     with iter show ?case by (rule Suc)

   178   qed

   179 qed

   180

   181

   182 subsection {* Concrete syntax for assertions *}

   183

   184 text {*

   185  We now introduce concrete syntax for describing commands (with

   186  embedded expressions) and assertions. The basic technique is that of

   187  semantic quote-antiquote''.  A \emph{quotation} is a syntactic

   188  entity delimited by an implicit abstraction, say over the state

   189  space.  An \emph{antiquotation} is a marked expression within a

   190  quotation that refers the implicit argument; a typical antiquotation

   191  would select (or even update) components from the state.

   192

   193  We will see some examples later in the concrete rules and

   194  applications.

   195 *}

   196

   197 text {*

   198  The following specification of syntax and translations is for

   199  Isabelle experts only; feel free to ignore it.

   200

   201  While the first part is still a somewhat intelligible specification

   202  of the concrete syntactic representation of our Hoare language, the

   203  actual ML drivers'' is quite involved.  Just note that the we

   204  re-use the basic quote/antiquote translations as already defined in

   205  Isabelle/Pure (see \verb,Syntax.quote_tr, and

   206  \verb,Syntax.quote_tr',).

   207 *}

   208

   209 syntax

   210   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)

   211   "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)

   212   "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"

   213         ("_[_'/\<acute>_]" [1000] 999)

   214   "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)

   215   "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)

   216   "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"

   217         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)

   218   "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"

   219         ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)

   220   "_While"       :: "'a bexp => 'a com => 'a com"

   221         ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)

   222

   223 syntax (xsymbols)

   224   "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)

   225

   226 translations

   227   ".{b}."                   => "CONST Collect .(b)."

   228   "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."

   229   "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."

   230   "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"

   231   "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"

   232   "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"

   233

   234 parse_translation {*

   235   let

   236     fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t

   237       | quote_tr ts = raise TERM ("quote_tr", ts);

   238   in [(@{syntax_const "_quote"}, quote_tr)] end

   239 *}

   240

   241 text {*

   242  As usual in Isabelle syntax translations, the part for printing is

   243  more complicated --- we cannot express parts as macro rules as above.

   244  Don't look here, unless you have to do similar things for yourself.

   245 *}

   246

   247 print_translation {*

   248   let

   249     fun quote_tr' f (t :: ts) =

   250           Term.list_comb (f $Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)   251 | quote_tr' _ _ = raise Match;   252   253 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});   254   255 fun bexp_tr' name ((Const (@{const_syntax Collect}, _)$ t) :: ts) =

   256           quote_tr' (Syntax.const name) (t :: ts)

   257       | bexp_tr' _ _ = raise Match;

   258

   259     fun K_tr' (Abs (_, _, t)) =

   260           if null (loose_bnos t) then t else raise Match

   261       | K_tr' (Abs (_, _, Abs (_, _, t) $Bound 0)) =   262 if null (loose_bnos t) then t else raise Match   263 | K_tr' _ = raise Match;   264   265 fun assign_tr' (Abs (x, _, f$ k $Bound 0) :: ts) =   266 quote_tr' (Syntax.const @{syntax_const "_Assign"}$ Syntax.update_name_tr' f)

   267             (Abs (x, dummyT, K_tr' k) :: ts)

   268       | assign_tr' _ = raise Match;

   269   in

   270    [(@{const_syntax Collect}, assert_tr'),

   271     (@{const_syntax Basic}, assign_tr'),

   272     (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),

   273     (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]

   274   end

   275 *}

   276

   277

   278 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}

   279

   280 text {*

   281  We are now ready to introduce a set of Hoare rules to be used in

   282  single-step structured proofs in Isabelle/Isar.  We refer to the

   283  concrete syntax introduce above.

   284

   285  \medskip Assertions of Hoare Logic may be manipulated in

   286  calculational proofs, with the inclusion expressed in terms of sets

   287  or predicates.  Reversed order is supported as well.

   288 *}

   289

   290 lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"

   291   by (unfold Valid_def) blast

   292 lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"

   293   by (unfold Valid_def) blast

   294

   295 lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"

   296   by (unfold Valid_def) blast

   297 lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"

   298   by (unfold Valid_def) blast

   299

   300 lemma [trans]:

   301     "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"

   302   by (simp add: Valid_def)

   303 lemma [trans]:

   304     "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"

   305   by (simp add: Valid_def)

   306

   307 lemma [trans]:

   308     "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."

   309   by (simp add: Valid_def)

   310 lemma [trans]:

   311     "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."

   312   by (simp add: Valid_def)

   313

   314

   315 text {*

   316  Identity and basic assignments.\footnote{The $\idt{hoare}$ method

   317  introduced in \S\ref{sec:hoare-vcg} is able to provide proper

   318  instances for any number of basic assignments, without producing

   319  additional verification conditions.}

   320 *}

   321

   322 lemma skip [intro?]: "|- P SKIP P"

   323 proof -

   324   have "|- {s. id s : P} SKIP P" by (rule basic)

   325   thus ?thesis by simp

   326 qed

   327

   328 lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"

   329   by (rule basic)

   330

   331 text {*

   332  Note that above formulation of assignment corresponds to our

   333  preferred way to model state spaces, using (extensible) record types

   334  in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field

   335  $x$, Isabelle/HOL provides a functions $x$ (selector) and

   336  $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder

   337  appearing for the latter kind of function: due to concrete syntax

   338  \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due

   339  to the external nature of HOL record fields, we could not even state

   340  a general theorem relating selector and update functions (if this

   341  were required here); this would only work for any particular instance

   342  of record fields introduced so far.}

   343 *}

   344

   345 text {*

   346  Sequential composition --- normalizing with associativity achieves

   347  proper of chunks of code verified separately.

   348 *}

   349

   350 lemmas [trans, intro?] = seq

   351

   352 lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"

   353   by (auto simp add: Valid_def)

   354

   355 text {*

   356  Conditional statements.

   357 *}

   358

   359 lemmas [trans, intro?] = cond

   360

   361 lemma [trans, intro?]:

   362   "|- .{\<acute>P & \<acute>b}. c1 Q

   363       ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q

   364       ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"

   365     by (rule cond) (simp_all add: Valid_def)

   366

   367 text {*

   368  While statements --- with optional invariant.

   369 *}

   370

   371 lemma [intro?]:

   372     "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"

   373   by (rule while)

   374

   375 lemma [intro?]:

   376     "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"

   377   by (rule while)

   378

   379

   380 lemma [intro?]:

   381   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.

   382     ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."

   383   by (simp add: while Collect_conj_eq Collect_neg_eq)

   384

   385 lemma [intro?]:

   386   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.

   387     ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."

   388   by (simp add: while Collect_conj_eq Collect_neg_eq)

   389

   390

   391 subsection {* Verification conditions \label{sec:hoare-vcg} *}

   392

   393 text {*

   394  We now load the \emph{original} ML file for proof scripts and tactic

   395  definition for the Hoare Verification Condition Generator (see

   396  \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we are

   397  concerned here, the result is a proof method \name{hoare}, which may

   398  be applied to a Hoare Logic assertion to extract purely logical

   399  verification conditions.  It is important to note that the method

   400  requires \texttt{WHILE} loops to be fully annotated with invariants

   401  beforehand.  Furthermore, only \emph{concrete} pieces of code are

   402  handled --- the underlying tactic fails ungracefully if supplied with

   403  meta-variables or parameters, for example.

   404 *}

   405

   406 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"

   407   by (auto simp add: Valid_def)

   408

   409 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"

   410   by (auto simp: Valid_def)

   411

   412 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"

   413   by (auto simp: Valid_def)

   414

   415 lemma CondRule:

   416   "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}

   417     \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"

   418   by (auto simp: Valid_def)

   419

   420 lemma iter_aux:

   421   "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>

   422        (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"

   423   apply(induct n)

   424    apply clarsimp

   425    apply (simp (no_asm_use))

   426    apply blast

   427   done

   428

   429 lemma WhileRule:

   430     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"

   431   apply (clarsimp simp: Valid_def)

   432   apply (drule iter_aux)

   433     prefer 2

   434     apply assumption

   435    apply blast

   436   apply blast

   437   done

   438

   439 lemma Compl_Collect: "- Collect b = {x. \<not> b x}"

   440   by blast

   441

   442 lemmas AbortRule = SkipRule  -- "dummy version"

   443

   444 use "~~/src/HOL/Hoare/hoare_tac.ML"

   445

   446 method_setup hoare = {*

   447   Scan.succeed (fn ctxt =>

   448     (SIMPLE_METHOD'

   449        (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}

   450   "verification condition generator for Hoare logic"

   451

   452 end