src/HOL/Isar_Examples/Hoare.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 48891 c0eafbd55de3 child 51717 9e7d1c139569 permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     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 begin

    12

    13 subsection {* Abstract syntax and semantics *}

    14

    15 text {* The following abstract syntax and semantics of Hoare Logic

    16   over \texttt{WHILE} programs closely follows the existing tradition

    17   in Isabelle/HOL of formalizing the presentation given in

    18   \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and

    19   \cite{Nipkow:1998:Winskel}. *}

    20

    21 type_synonym 'a bexp = "'a set"

    22 type_synonym 'a assn = "'a set"

    23

    24 datatype 'a com =

    25     Basic "'a => 'a"

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

    27   | Cond "'a bexp" "'a com" "'a com"

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

    29

    30 abbreviation Skip  ("SKIP")

    31   where "SKIP == Basic id"

    32

    33 type_synonym 'a sem = "'a => 'a => bool"

    34

    35 primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"

    36 where

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

    38 | "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"

    39

    40 primrec Sem :: "'a com => 'a sem"

    41 where

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

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

    44 | "Sem (Cond b c1 c2) s s' =

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

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

    47

    48 definition Valid :: "'a bexp => 'a com => 'a bexp => bool"

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

    50   where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"

    51

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

    53

    54 lemma ValidI [intro?]:

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

    56   by (simp add: Valid_def)

    57

    58 lemma ValidD [dest?]:

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

    60   by (simp add: Valid_def)

    61

    62

    63 subsection {* Primitive Hoare rules *}

    64

    65 text {* From the semantics defined above, we derive the standard set

    66   of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.

    67   Usually, variant forms of these rules are applied in actual proof,

    68   see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.

    69

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

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

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

    73

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

    75 proof

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

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

    78   then have "s' = f s" by simp

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

    80 qed

    81

    82 text {*

    83  The rules for sequential commands and semantic consequences are

    84  established in a straight forward manner as follows.

    85 *}

    86

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

    88 proof

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

    90   fix s s' assume s: "s : 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'' : Q" ..

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

    96 qed

    97

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

    99 proof

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

   101   assume cmd: "|- P c Q"

   102   fix s s' :: 'a

   103   assume sem: "Sem c s s'"

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

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

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

   107 qed

   108

   109 text {* The rule for conditional commands is directly reflected by the

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

   111   which cases apply. *}

   112

   113 theorem cond:

   114   assumes case_b: "|- (P Int b) c1 Q"

   115     and case_nb: "|- (P Int -b) c2 Q"

   116   shows "|- P (Cond b c1 c2) Q"

   117 proof

   118   fix s s' assume s: "s : P"

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

   120   show "s' : Q"

   121   proof cases

   122     assume b: "s : b"

   123     from case_b show ?thesis

   124     proof

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

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

   127     qed

   128   next

   129     assume nb: "s ~: b"

   130     from case_nb show ?thesis

   131     proof

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

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

   134     qed

   135   qed

   136 qed

   137

   138 text {* The @{text while} rule is slightly less trivial --- it is the

   139   only one based on recursion, which is expressed in the semantics by

   140   a Kleene-style least fixed-point construction.  The auxiliary

   141   statement below, which is by induction on the number of iterations

   142   is the main point to be proven; the rest is by routine application

   143   of the semantics of \texttt{WHILE}. *}

   144

   145 theorem while:

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

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

   148 proof

   149   fix s s' assume s: "s : P"

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

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

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

   153   proof (induct n arbitrary: s)

   154     case 0

   155     then show ?case by auto

   156   next

   157     case (Suc n)

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

   159       and iter: "iter n b (Sem c) s'' s'" by auto

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

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

   162     with iter show ?case by (rule Suc)

   163   qed

   164 qed

   165

   166

   167 subsection {* Concrete syntax for assertions *}

   168

   169 text {* We now introduce concrete syntax for describing commands (with

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

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

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

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

   174   quotation that refers the implicit argument; a typical antiquotation

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

   176

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

   178   applications. *}

   179

   180 text {* The following specification of syntax and translations is for

   181   Isabelle experts only; feel free to ignore it.

   182

   183   While the first part is still a somewhat intelligible specification

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

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

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

   187   Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and

   188   @{ML Syntax_Trans.quote_tr'},). *}

   189

   190 syntax

   191   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)"  1000)

   192   "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_"  1000)

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

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

   195   "_Assert"      :: "'a => 'a set"           ("(.{_}.)"  1000)

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

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

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

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

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

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

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

   203

   204 syntax (xsymbols)

   205   "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)"  1000)

   206

   207 translations

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

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

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

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

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

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

   214

   215 parse_translation {*

   216   let

   217     fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t

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

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

   220 *}

   221

   222 text {* As usual in Isabelle syntax translations, the part for

   223   printing is more complicated --- we cannot express parts as macro

   224   rules as above.  Don't look here, unless you have to do similar

   225   things for yourself. *}

   226

   227 print_translation {*

   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;   232   233 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});   234   235 fun bexp_tr' name ((Const (@{const_syntax Collect}, _)$ t) :: ts) =

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

   237       | bexp_tr' _ _ = raise Match;

   238

   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}, assert_tr'),   245 (@{const_syntax Basic}, assign_tr'),   246 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),   247 (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]   248 end   249 *}   250   251   252 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}   253   254 text {* We are now ready to introduce a set of Hoare rules to be used   255 in single-step structured proofs in Isabelle/Isar. We refer to the   256 concrete syntax introduce above.   257   258 \medskip Assertions of Hoare Logic may be manipulated in   259 calculational proofs, with the inclusion expressed in terms of sets   260 or predicates. Reversed order is supported as well. *}   261   262 lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"   263 by (unfold Valid_def) blast   264 lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"   265 by (unfold Valid_def) blast   266   267 lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"   268 by (unfold Valid_def) blast   269 lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"   270 by (unfold Valid_def) blast   271   272 lemma [trans]:   273 "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"   274 by (simp add: Valid_def)   275 lemma [trans]:   276 "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"   277 by (simp add: Valid_def)   278   279 lemma [trans]:   280 "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."   281 by (simp add: Valid_def)   282 lemma [trans]:   283 "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."   284 by (simp add: Valid_def)   285   286   287 text {* Identity and basic assignments.\footnote{The$\idt{hoare}$  288 method introduced in \S\ref{sec:hoare-vcg} is able to provide proper   289 instances for any number of basic assignments, without producing   290 additional verification conditions.} *}   291   292 lemma skip [intro?]: "|- P SKIP P"   293 proof -   294 have "|- {s. id s : P} SKIP P" by (rule basic)   295 then show ?thesis by simp   296 qed   297   298 lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"   299 by (rule basic)   300   301 text {* Note that above formulation of assignment corresponds to our   302 preferred way to model state spaces, using (extensible) record types   303 in HOL \cite{Naraschewski-Wenzel:1998:HOOL}. For any record field   304$x$, Isabelle/HOL provides a functions$x$(selector) and   305$\idt{x{\dsh}update}\$ (update).  Above, there is only a place-holder

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

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

   308   due to the external nature of HOL record fields, we could not even

   309   state a general theorem relating selector and update functions (if

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

   311   instance of record fields introduced so far.} *}

   312

   313 text {* Sequential composition --- normalizing with associativity

   314   achieves proper of chunks of code verified separately. *}

   315

   316 lemmas [trans, intro?] = seq

   317

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

   319   by (auto simp add: Valid_def)

   320

   321 text {* Conditional statements. *}

   322

   323 lemmas [trans, intro?] = cond

   324

   325 lemma [trans, intro?]:

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

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

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

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

   330

   331 text {* While statements --- with optional invariant. *}

   332

   333 lemma [intro?]:

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

   335   by (rule while)

   336

   337 lemma [intro?]:

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

   339   by (rule while)

   340

   341

   342 lemma [intro?]:

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

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

   345   by (simp add: while Collect_conj_eq Collect_neg_eq)

   346

   347 lemma [intro?]:

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

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

   350   by (simp add: while Collect_conj_eq Collect_neg_eq)

   351

   352

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

   354

   355 text {* We now load the \emph{original} ML file for proof scripts and

   356   tactic definition for the Hoare Verification Condition Generator

   357   (see @{file "~~/src/HOL/Hoare/"}).  As far as we

   358   are concerned here, the result is a proof method \name{hoare}, which

   359   may be applied to a Hoare Logic assertion to extract purely logical

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

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

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

   363   handled --- the underlying tactic fails ungracefully if supplied

   364   with meta-variables or parameters, for example. *}

   365

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

   367   by (auto simp add: Valid_def)

   368

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

   370   by (auto simp: Valid_def)

   371

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

   373   by (auto simp: Valid_def)

   374

   375 lemma CondRule:

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

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

   378   by (auto simp: Valid_def)

   379

   380 lemma iter_aux:

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

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

   383   apply(induct n)

   384    apply clarsimp

   385    apply (simp (no_asm_use))

   386    apply blast

   387   done

   388

   389 lemma WhileRule:

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

   391   apply (clarsimp simp: Valid_def)

   392   apply (drule iter_aux)

   393     prefer 2

   394     apply assumption

   395    apply blast

   396   apply blast

   397   done

   398

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

   400   by blast

   401

   402 lemmas AbortRule = SkipRule  -- "dummy version"

   403

   404 ML_file "~~/src/HOL/Hoare/hoare_tac.ML"

   405

   406 method_setup hoare = {*

   407   Scan.succeed (fn ctxt =>

   408     (SIMPLE_METHOD'

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

   410   "verification condition generator for Hoare logic"

   411

   412 end