src/HOL/Isar_examples/Hoare.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 19363 667b5ea637dd child 20503 503ac4c5ef91 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/Isar_examples/Hoare.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4

     5 A formulation of Hoare logic suitable for Isar.

     6 *)

     7

     8 header {* Hoare Logic *}

     9

    10 theory Hoare imports Main

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

    12

    13 subsection {* Abstract syntax and semantics *}

    14

    15 text {*

    16  The following abstract syntax and semantics of Hoare Logic over

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

    18  Isabelle/HOL of formalizing the presentation given in

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

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

    21  \cite{Nipkow:1998:Winskel}.

    22 *}

    23

    24 types

    25   'a bexp = "'a set"

    26   'a assn = "'a set"

    27

    28 datatype 'a com =

    29     Basic "'a => 'a"

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

    31   | Cond "'a bexp" "'a com" "'a com"

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

    33

    34 abbreviation

    35   Skip  ("SKIP")

    36   "SKIP == Basic id"

    37

    38 types

    39   'a sem = "'a => 'a => bool"

    40

    41 consts

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

    43 primrec

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

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

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

    47

    48 consts

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

    50 primrec

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

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

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

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

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

    56

    57 constdefs

    58   Valid :: "'a bexp => 'a com => 'a bexp => bool"

    59     ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)

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

    61

    62 syntax (xsymbols)

    63   Valid :: "'a bexp => 'a com => 'a bexp => bool"

    64     ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)

    65

    66 lemma ValidI [intro?]:

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

    68   by (simp add: Valid_def)

    69

    70 lemma ValidD [dest?]:

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

    72   by (simp add: Valid_def)

    73

    74

    75 subsection {* Primitive Hoare rules *}

    76

    77 text {*

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

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

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

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

    82

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

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

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

    86 *}

    87

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

    89 proof

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

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

    92   hence "s' = f s" by simp

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

    94 qed

    95

    96 text {*

    97  The rules for sequential commands and semantic consequences are

    98  established in a straight forward manner as follows.

    99 *}

   100

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

   102 proof

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

   104   fix s s' assume s: "s : P"

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

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

   107     by auto

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

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

   110 qed

   111

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

   113 proof

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

   115   assume cmd: "|- P c Q"

   116   fix s s' :: 'a

   117   assume sem: "Sem c s s'"

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

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

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

   121 qed

   122

   123 text {*

   124  The rule for conditional commands is directly reflected by the

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

   126  which cases apply.

   127 *}

   128

   129 theorem cond:

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

   131 proof

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

   133   fix s s' assume s: "s : P"

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

   135   show "s' : Q"

   136   proof cases

   137     assume b: "s : b"

   138     from case_b show ?thesis

   139     proof

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

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

   142     qed

   143   next

   144     assume nb: "s ~: b"

   145     from case_nb show ?thesis

   146     proof

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

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

   149     qed

   150   qed

   151 qed

   152

   153 text {*

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

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

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

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

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

   159  semantics of \texttt{WHILE}.

   160 *}

   161

   162 theorem while:

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

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

   165 proof

   166   fix s s' assume s: "s : P"

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

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

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

   170   proof (induct n fixing: s)

   171     case 0

   172     thus ?case by auto

   173   next

   174     case (Suc n)

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

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

   177       by auto

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

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

   180     with iter show ?case by (rule Suc)

   181   qed

   182 qed

   183

   184

   185 subsection {* Concrete syntax for assertions *}

   186

   187 text {*

   188  We now introduce concrete syntax for describing commands (with

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

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

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

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

   193  quotation that refers the implicit argument; a typical antiquotation

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

   195

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

   197  applications.

   198 *}

   199

   200 text {*

   201  The following specification of syntax and translations is for

   202  Isabelle experts only; feel free to ignore it.

   203

   204  While the first part is still a somewhat intelligible specification

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

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

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

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

   209  \verb,Syntax.quote_tr',).

   210 *}

   211

   212 syntax

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

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

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

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

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

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

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

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

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

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

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

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

   225

   226 syntax (xsymbols)

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

   228

   229 translations

   230   ".{b}."                   => "Collect .(b)."

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

   232   "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."

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

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

   235   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"

   236

   237 parse_translation {*

   238   let

   239     fun quote_tr [t] = Syntax.quote_tr "_antiquote" t

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

   241   in [("_quote", quote_tr)] end

   242 *}

   243

   244 text {*

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

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

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

   248 *}

   249

   250 print_translation {*

   251   let

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

   253           Term.list_comb (f $Syntax.quote_tr' "_antiquote" t, ts)   254 | quote_tr' _ _ = raise Match;   255   256 val assert_tr' = quote_tr' (Syntax.const "_Assert");   257   258 fun bexp_tr' name ((Const ("Collect", _)$ t) :: ts) =

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

   260       | bexp_tr' _ _ = raise Match;

   261

   262     fun upd_tr' (x_upd, T) =

   263       (case try (unsuffix RecordPackage.updateN) x_upd of

   264         SOME x => (x, if T = dummyT then T else Term.domain_type T)

   265       | NONE => raise Match);

   266

   267     fun update_name_tr' (Free x) = Free (upd_tr' x)

   268       | update_name_tr' ((c as Const ("_free", _)) $Free x) =   269 c$ Free (upd_tr' x)

   270       | update_name_tr' (Const x) = Const (upd_tr' x)

   271       | update_name_tr' _ = raise Match;

   272

   273     fun assign_tr' (Abs (x, _, f $t$ Bound 0) :: ts) =

   274           quote_tr' (Syntax.const "_Assign" $update_name_tr' f)   275 (Abs (x, dummyT, t) :: ts)   276 | assign_tr' _ = raise Match;   277 in   278 [("Collect", assert_tr'), ("Basic", assign_tr'),   279 ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]   280 end   281 *}   282   283   284 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}   285   286 text {*   287 We are now ready to introduce a set of Hoare rules to be used in   288 single-step structured proofs in Isabelle/Isar. We refer to the   289 concrete syntax introduce above.   290   291 \medskip Assertions of Hoare Logic may be manipulated in   292 calculational proofs, with the inclusion expressed in terms of sets   293 or predicates. Reversed order is supported as well.   294 *}   295   296 lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"   297 by (unfold Valid_def) blast   298 lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"   299 by (unfold Valid_def) blast   300   301 lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"   302 by (unfold Valid_def) blast   303 lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"   304 by (unfold Valid_def) blast   305   306 lemma [trans]:   307 "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"   308 by (simp add: Valid_def)   309 lemma [trans]:   310 "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"   311 by (simp add: Valid_def)   312   313 lemma [trans]:   314 "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."   315 by (simp add: Valid_def)   316 lemma [trans]:   317 "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."   318 by (simp add: Valid_def)   319   320   321 text {*   322 Identity and basic assignments.\footnote{The$\idt{hoare}$method   323 introduced in \S\ref{sec:hoare-vcg} is able to provide proper   324 instances for any number of basic assignments, without producing   325 additional verification conditions.}   326 *}   327   328 lemma skip [intro?]: "|- P SKIP P"   329 proof -   330 have "|- {s. id s : P} SKIP P" by (rule basic)   331 thus ?thesis by simp   332 qed   333   334 lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"   335 by (rule basic)   336   337 text {*   338 Note that above formulation of assignment corresponds to our   339 preferred way to model state spaces, using (extensible) record types   340 in HOL \cite{Naraschewski-Wenzel:1998:HOOL}. For any record field   341$x$, Isabelle/HOL provides a functions$x$(selector) and   342$\idt{x{\dsh}update}\$ (update).  Above, there is only a place-holder

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

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

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

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

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

   348  of record fields introduced so far.}

   349 *}

   350

   351 text {*

   352  Sequential composition --- normalizing with associativity achieves

   353  proper of chunks of code verified separately.

   354 *}

   355

   356 lemmas [trans, intro?] = seq

   357

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

   359   by (auto simp add: Valid_def)

   360

   361 text {*

   362  Conditional statements.

   363 *}

   364

   365 lemmas [trans, intro?] = cond

   366

   367 lemma [trans, intro?]:

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

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

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

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

   372

   373 text {*

   374  While statements --- with optional invariant.

   375 *}

   376

   377 lemma [intro?]:

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

   379   by (rule while)

   380

   381 lemma [intro?]:

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

   383   by (rule while)

   384

   385

   386 lemma [intro?]:

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

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

   389   by (simp add: while Collect_conj_eq Collect_neg_eq)

   390

   391 lemma [intro?]:

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

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

   394   by (simp add: while Collect_conj_eq Collect_neg_eq)

   395

   396

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

   398

   399 text {*

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

   401  definition for the Hoare Verification Condition Generator (see

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

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

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

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

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

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

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

   409  meta-variables or parameters, for example.

   410 *}

   411

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

   413   by (auto simp add: Valid_def)

   414

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

   416   by (auto simp: Valid_def)

   417

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

   419   by (auto simp: Valid_def)

   420

   421 lemma CondRule:

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

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

   424   by (auto simp: Valid_def)

   425

   426 lemma iter_aux:

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

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

   429   apply(induct n)

   430    apply clarsimp

   431    apply (simp (no_asm_use))

   432    apply blast

   433   done

   434

   435 lemma WhileRule:

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

   437   apply (clarsimp simp: Valid_def)

   438   apply (drule iter_aux)

   439     prefer 2

   440     apply assumption

   441    apply blast

   442   apply blast

   443   done

   444

   445 ML {* val Valid_def = thm "Valid_def" *}

   446 use "~~/src/HOL/Hoare/hoare.ML"

   447

   448 method_setup hoare = {*

   449   Method.no_args

   450     (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}

   451   "verification condition generator for Hoare logic"

   452

   453 end