src/HOL/IMPP/Hoare.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 60754 02924903a6fd
child 63167 0909deb8059b
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/IMPP/Hoare.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 TUM
     4 *)
     5 
     6 section {* Inductive definition of Hoare logic for partial correctness *}
     7 
     8 theory Hoare
     9 imports Natural
    10 begin
    11 
    12 text {*
    13   Completeness is taken relative to completeness of the underlying logic.
    14 
    15   Two versions of completeness proof: nested single recursion
    16   vs. simultaneous recursion in call rule
    17 *}
    18 
    19 type_synonym 'a assn = "'a => state => bool"
    20 translations
    21   (type) "'a assn" <= (type) "'a => state => bool"
    22 
    23 definition
    24   state_not_singleton :: bool where
    25   "state_not_singleton = (\<exists>s t::state. s ~= t)" (* at least two elements *)
    26 
    27 definition
    28   peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where
    29   "peek_and P p = (%Z s. P Z s & p s)"
    30 
    31 datatype 'a triple =
    32   triple "'a assn"  com  "'a assn"       ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
    33 
    34 definition
    35   triple_valid :: "nat => 'a triple     => bool" ( "|=_:_" [0 , 58] 57) where
    36   "|=n:t = (case t of {P}.c.{Q} =>
    37              !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))"
    38 abbreviation
    39   triples_valid :: "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57) where
    40   "||=n:G == Ball G (triple_valid n)"
    41 
    42 definition
    43   hoare_valids :: "'a triple set => 'a triple set => bool" ("_||=_"  [58, 58] 57) where
    44   "G||=ts = (!n. ||=n:G --> ||=n:ts)"
    45 abbreviation
    46   hoare_valid :: "'a triple set => 'a triple     => bool" ("_|=_"   [58, 58] 57) where
    47   "G |=t == G||={t}"
    48 
    49 (* Most General Triples *)
    50 definition
    51   MGT :: "com => state triple"            ("{=}._.{->}" [60] 58) where
    52   "{=}.c.{->} = {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}"
    53 
    54 inductive
    55   hoare_derivs :: "'a triple set => 'a triple set => bool" ("_||-_"  [58, 58] 57) and
    56   hoare_deriv :: "'a triple set => 'a triple     => bool" ("_|-_"   [58, 58] 57)
    57 where
    58   "G |-t == G||-{t}"
    59 
    60 | empty:    "G||-{}"
    61 | insert: "[| G |-t;  G||-ts |]
    62         ==> G||-insert t ts"
    63 
    64 | asm:      "ts <= G ==>
    65              G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
    66 
    67 | cut:   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
    68 
    69 | weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts"
    70 
    71 | conseq: "!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
    72                                    (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
    73           ==> G|-{P}.c.{Q}"
    74 
    75 
    76 | Skip:  "G|-{P}. SKIP .{P}"
    77 
    78 | Ass:   "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
    79 
    80 | Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
    81       ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
    82 
    83 | Comp:  "[| G|-{P}.c.{Q};
    84              G|-{Q}.d.{R} |]
    85          ==> G|-{P}. (c;;d) .{R}"
    86 
    87 | If:    "[| G|-{P &>        b }.c.{Q};
    88              G|-{P &> (Not o b)}.d.{Q} |]
    89          ==> G|-{P}. IF b THEN c ELSE d .{Q}"
    90 
    91 | Loop:  "G|-{P &> b}.c.{P} ==>
    92           G|-{P}. WHILE b DO c .{P &> (Not o b)}"
    93 
    94 (*
    95   BodyN: "(insert ({P}. BODY pn  .{Q}) G)
    96            |-{P}.  the (body pn) .{Q} ==>
    97           G|-{P}.       BODY pn  .{Q}"
    98 *)
    99 | Body:  "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
   100                ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
   101          ==>  G||-(%p. {P p}.      BODY p  .{Q p})`Procs"
   102 
   103 | Call:     "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
   104          ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
   105              X:=CALL pn(a) .{Q}"
   106 
   107 
   108 section {* Soundness and relative completeness of Hoare rules wrt operational semantics *}
   109 
   110 lemma single_stateE:
   111   "state_not_singleton ==> !t. (!s::state. s = t) --> False"
   112 apply (unfold state_not_singleton_def)
   113 apply clarify
   114 apply (case_tac "ta = t")
   115 apply blast
   116 apply (blast dest: not_sym)
   117 done
   118 
   119 declare peek_and_def [simp]
   120 
   121 
   122 subsection "validity"
   123 
   124 lemma triple_valid_def2:
   125   "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))"
   126 apply (unfold triple_valid_def)
   127 apply auto
   128 done
   129 
   130 lemma Body_triple_valid_0: "|=0:{P}. BODY pn .{Q}"
   131 apply (simp (no_asm) add: triple_valid_def2)
   132 apply clarsimp
   133 done
   134 
   135 (* only ==> direction required *)
   136 lemma Body_triple_valid_Suc: "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}"
   137 apply (simp (no_asm) add: triple_valid_def2)
   138 apply force
   139 done
   140 
   141 lemma triple_valid_Suc [rule_format (no_asm)]: "|=Suc n:t --> |=n:t"
   142 apply (unfold triple_valid_def)
   143 apply (induct_tac t)
   144 apply simp
   145 apply (fast intro: evaln_Suc)
   146 done
   147 
   148 lemma triples_valid_Suc: "||=Suc n:ts ==> ||=n:ts"
   149 apply (fast intro: triple_valid_Suc)
   150 done
   151 
   152 
   153 subsection "derived rules"
   154 
   155 lemma conseq12: "[| G|-{P'}.c.{Q'}; !Z s. P Z s -->
   156                          (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |]
   157        ==> G|-{P}.c.{Q}"
   158 apply (rule hoare_derivs.conseq)
   159 apply blast
   160 done
   161 
   162 lemma conseq1: "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}"
   163 apply (erule conseq12)
   164 apply fast
   165 done
   166 
   167 lemma conseq2: "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}"
   168 apply (erule conseq12)
   169 apply fast
   170 done
   171 
   172 lemma Body1: "[| G Un (%p. {P p}.      BODY p  .{Q p})`Procs
   173           ||- (%p. {P p}. the (body p) .{Q p})`Procs;
   174     pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}"
   175 apply (drule hoare_derivs.Body)
   176 apply (erule hoare_derivs.weaken)
   177 apply fast
   178 done
   179 
   180 lemma BodyN: "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==>
   181   G|-{P}. BODY pn .{Q}"
   182 apply (rule Body1)
   183 apply (rule_tac [2] singletonI)
   184 apply clarsimp
   185 done
   186 
   187 lemma escape: "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}"
   188 apply (rule hoare_derivs.conseq)
   189 apply fast
   190 done
   191 
   192 lemma "constant": "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}"
   193 apply (rule hoare_derivs.conseq)
   194 apply fast
   195 done
   196 
   197 lemma LoopF: "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}"
   198 apply (rule hoare_derivs.Loop [THEN conseq2])
   199 apply  (simp_all (no_asm))
   200 apply (rule hoare_derivs.conseq)
   201 apply fast
   202 done
   203 
   204 (*
   205 Goal "[| G'||-ts; G' <= G |] ==> G||-ts"
   206 by (etac hoare_derivs.cut 1);
   207 by (etac hoare_derivs.asm 1);
   208 qed "thin";
   209 *)
   210 lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
   211 apply (erule hoare_derivs.induct)
   212 apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
   213 apply (rule hoare_derivs.empty)
   214 apply               (erule (1) hoare_derivs.insert)
   215 apply              (fast intro: hoare_derivs.asm)
   216 apply             (fast intro: hoare_derivs.cut)
   217 apply            (fast intro: hoare_derivs.weaken)
   218 apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac @{context} 2 1", clarify, tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI)
   219 prefer 7
   220 apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
   221 apply         (tactic {* ALLGOALS (resolve_tac @{context} ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
   222 done
   223 
   224 lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
   225 apply (rule BodyN)
   226 apply (erule thin)
   227 apply auto
   228 done
   229 
   230 lemma derivs_insertD: "G||-insert t ts ==> G|-t & G||-ts"
   231 apply (fast intro: hoare_derivs.weaken)
   232 done
   233 
   234 lemma finite_pointwise [rule_format (no_asm)]: "[| finite U;
   235   !p. G |-     {P' p}.c0 p.{Q' p}       --> G |-     {P p}.c0 p.{Q p} |] ==>
   236       G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U"
   237 apply (erule finite_induct)
   238 apply simp
   239 apply clarsimp
   240 apply (drule derivs_insertD)
   241 apply (rule hoare_derivs.insert)
   242 apply  auto
   243 done
   244 
   245 
   246 subsection "soundness"
   247 
   248 lemma Loop_sound_lemma:
   249  "G|={P &> b}. c .{P} ==>
   250   G|={P}. WHILE b DO c .{P &> (Not o b)}"
   251 apply (unfold hoare_valids_def)
   252 apply (simp (no_asm_use) add: triple_valid_def2)
   253 apply (rule allI)
   254 apply (subgoal_tac "!d s s'. <d,s> -n-> s' --> d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s') ")
   255 apply  (erule thin_rl, fast)
   256 apply ((rule allI)+, rule impI)
   257 apply (erule evaln.induct)
   258 apply (simp_all (no_asm))
   259 apply fast
   260 apply fast
   261 done
   262 
   263 lemma Body_sound_lemma:
   264    "[| G Un (%pn. {P pn}.      BODY pn  .{Q pn})`Procs
   265          ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==>
   266         G||=(%pn. {P pn}.      BODY pn  .{Q pn})`Procs"
   267 apply (unfold hoare_valids_def)
   268 apply (rule allI)
   269 apply (induct_tac n)
   270 apply  (fast intro: Body_triple_valid_0)
   271 apply clarsimp
   272 apply (drule triples_valid_Suc)
   273 apply (erule (1) notE impE)
   274 apply (simp add: ball_Un)
   275 apply (drule spec, erule impE, erule conjI, assumption)
   276 apply (fast intro!: Body_triple_valid_Suc [THEN iffD1])
   277 done
   278 
   279 lemma hoare_sound: "G||-ts ==> G||=ts"
   280 apply (erule hoare_derivs.induct)
   281 apply              (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW assume_tac @{context}) *})
   282 apply            (unfold hoare_valids_def)
   283 apply            blast
   284 apply           blast
   285 apply          (blast) (* asm *)
   286 apply         (blast) (* cut *)
   287 apply        (blast) (* weaken *)
   288 apply       (tactic {* ALLGOALS (EVERY'
   289   [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs _ _" [],
   290    simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
   291 apply       (simp_all (no_asm_use) add: triple_valid_def2)
   292 apply       (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
   293 apply      (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
   294 prefer 3 apply   (force) (* Call *)
   295 apply  (erule_tac [2] evaln_elim_cases) (* If *)
   296 apply   blast+
   297 done
   298 
   299 
   300 section "completeness"
   301 
   302 (* Both versions *)
   303 
   304 (*unused*)
   305 lemma MGT_alternI: "G|-MGT c ==>
   306   G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}"
   307 apply (unfold MGT_def)
   308 apply (erule conseq12)
   309 apply auto
   310 done
   311 
   312 (* requires com_det *)
   313 lemma MGT_alternD: "state_not_singleton ==>
   314   G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c"
   315 apply (unfold MGT_def)
   316 apply (erule conseq12)
   317 apply auto
   318 apply (case_tac "\<exists>t. <c,s> -c-> t" for s)
   319 apply  (fast elim: com_det)
   320 apply clarsimp
   321 apply (drule single_stateE)
   322 apply blast
   323 done
   324 
   325 lemma MGF_complete:
   326  "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}"
   327 apply (unfold MGT_def)
   328 apply (erule conseq12)
   329 apply (clarsimp simp add: hoare_valids_def eval_eq triple_valid_def2)
   330 done
   331 
   332 declare WTs_elim_cases [elim!]
   333 declare not_None_eq [iff]
   334 (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
   335 lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
   336   !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
   337 apply (induct_tac c)
   338 apply        (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
   339 prefer 7 apply        (fast intro: domI)
   340 apply (erule_tac [6] MGT_alternD)
   341 apply       (unfold MGT_def)
   342 apply       (drule_tac [7] bspec, erule_tac [7] domI)
   343 apply       (rule_tac [7] escape, tactic {* clarsimp_tac @{context} 7 *},
   344   rename_tac [7] "fun" y Z,
   345   rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
   346 apply        (erule_tac [!] thin_rl)
   347 apply (rule hoare_derivs.Skip [THEN conseq2])
   348 apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
   349 apply        (rule_tac [3] escape, tactic {* clarsimp_tac @{context} 3 *},
   350   rename_tac [3] loc "fun" y Z,
   351   rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
   352   erule_tac [3] conseq12)
   353 apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
   354 apply         (tactic {* (resolve_tac @{context} @{thms hoare_derivs.If} THEN_ALL_NEW
   355                 eresolve_tac @{context} @{thms conseq12}) 6 *})
   356 apply          (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
   357 apply           auto
   358 done
   359 
   360 (* Version: nested single recursion *)
   361 
   362 lemma nesting_lemma [rule_format]:
   363   assumes "!!G ts. ts <= G ==> P G ts"
   364     and "!!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn}"
   365     and "!!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}"
   366     and "!!pn. pn : U ==> wt (the (body pn))"
   367   shows "finite U ==> uG = mgt_call`U ==>
   368   !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
   369 apply (induct_tac n)
   370 apply  (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
   371 apply  (subgoal_tac "G = mgt_call ` U")
   372 prefer 2
   373 apply   (simp add: card_seteq)
   374 apply  simp
   375 apply  (erule assms(3-)) (*MGF_lemma1*)
   376 apply (rule ballI)
   377 apply  (rule assms) (*hoare_derivs.asm*)
   378 apply  fast
   379 apply (erule assms(3-)) (*MGF_lemma1*)
   380 apply (rule ballI)
   381 apply (case_tac "mgt_call pn : G")
   382 apply  (rule assms) (*hoare_derivs.asm*)
   383 apply  fast
   384 apply (rule assms(2-)) (*MGT_BodyN*)
   385 apply (drule spec, erule impE, erule_tac [2] impE, drule_tac [3] spec, erule_tac [3] mp)
   386 apply   (erule_tac [3] assms(4-))
   387 apply   fast
   388 apply (drule finite_subset)
   389 apply (erule finite_imageI)
   390 apply (simp (no_asm_simp))
   391 done
   392 
   393 lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>
   394   G|-{=}.BODY pn.{->}"
   395 apply (unfold MGT_def)
   396 apply (rule BodyN)
   397 apply (erule conseq2)
   398 apply force
   399 done
   400 
   401 (* requires BodyN, com_det *)
   402 lemma MGF: "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"
   403 apply (rule_tac P = "%G ts. G||-ts" and U = "dom body" in nesting_lemma)
   404 apply (erule hoare_derivs.asm)
   405 apply (erule MGT_BodyN)
   406 apply (rule_tac [3] finite_dom_body)
   407 apply (erule MGF_lemma1)
   408 prefer 2 apply (assumption)
   409 apply       blast
   410 apply      clarsimp
   411 apply     (erule (1) WT_bodiesD)
   412 apply (rule_tac [3] le_refl)
   413 apply    auto
   414 done
   415 
   416 
   417 (* Version: simultaneous recursion in call rule *)
   418 
   419 (* finiteness not really necessary here *)
   420 lemma MGT_Body: "[| G Un (%pn. {=}.      BODY pn  .{->})`Procs
   421                           ||-(%pn. {=}. the (body pn) .{->})`Procs;
   422   finite Procs |] ==>   G ||-(%pn. {=}.      BODY pn  .{->})`Procs"
   423 apply (unfold MGT_def)
   424 apply (rule hoare_derivs.Body)
   425 apply (erule finite_pointwise)
   426 prefer 2 apply (assumption)
   427 apply clarify
   428 apply (erule conseq2)
   429 apply auto
   430 done
   431 
   432 (* requires empty, insert, com_det *)
   433 lemma MGF_lemma2_simult [rule_format (no_asm)]: "[| state_not_singleton; WT_bodies;
   434   F<=(%pn. {=}.the (body pn).{->})`dom body |] ==>
   435      (%pn. {=}.     BODY pn .{->})`dom body||-F"
   436 apply (frule finite_subset)
   437 apply (rule finite_dom_body [THEN finite_imageI])
   438 apply (rotate_tac 2)
   439 apply (tactic "make_imp_tac @{context} 1")
   440 apply (erule finite_induct)
   441 apply  (clarsimp intro!: hoare_derivs.empty)
   442 apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition)
   443 apply (erule MGF_lemma1)
   444 prefer 2 apply  (fast dest: WT_bodiesD)
   445 apply clarsimp
   446 apply (rule hoare_derivs.asm)
   447 apply (fast intro: domI)
   448 done
   449 
   450 (* requires Body, empty, insert, com_det *)
   451 lemma MGF': "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"
   452 apply (rule MGF_lemma1)
   453 apply assumption
   454 prefer 2 apply (assumption)
   455 apply clarsimp
   456 apply (subgoal_tac "{}||- (%pn. {=}. BODY pn .{->}) `dom body")
   457 apply (erule hoare_derivs.weaken)
   458 apply  (fast intro: domI)
   459 apply (rule finite_dom_body [THEN [2] MGT_Body])
   460 apply (simp (no_asm))
   461 apply (erule (1) MGF_lemma2_simult)
   462 apply (rule subset_refl)
   463 done
   464 
   465 (* requires Body+empty+insert / BodyN, com_det *)
   466 lemmas hoare_complete = MGF' [THEN MGF_complete]
   467 
   468 
   469 subsection "unused derived rules"
   470 
   471 lemma falseE: "G|-{%Z s. False}.c.{Q}"
   472 apply (rule hoare_derivs.conseq)
   473 apply fast
   474 done
   475 
   476 lemma trueI: "G|-{P}.c.{%Z s. True}"
   477 apply (rule hoare_derivs.conseq)
   478 apply (fast intro!: falseE)
   479 done
   480 
   481 lemma disj: "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |]
   482         ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}"
   483 apply (rule hoare_derivs.conseq)
   484 apply (fast elim: conseq12)
   485 done (* analogue conj non-derivable *)
   486 
   487 lemma hoare_SkipI: "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}"
   488 apply (rule conseq12)
   489 apply (rule hoare_derivs.Skip)
   490 apply fast
   491 done
   492 
   493 
   494 subsection "useful derived rules"
   495 
   496 lemma single_asm: "{t}|-t"
   497 apply (rule hoare_derivs.asm)
   498 apply (rule subset_refl)
   499 done
   500 
   501 lemma export_s: "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}"
   502 apply (rule hoare_derivs.conseq)
   503 apply auto
   504 done
   505 
   506 
   507 lemma weak_Local: "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==>
   508     G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}"
   509 apply (rule export_s)
   510 apply (rule hoare_derivs.Local)
   511 apply (erule conseq2)
   512 apply (erule spec)
   513 done
   514 
   515 (*
   516 Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}"
   517 by (induct_tac "c" 1);
   518 by Auto_tac;
   519 by (rtac conseq1 1);
   520 by (rtac hoare_derivs.Skip 1);
   521 force 1;
   522 by (rtac conseq1 1);
   523 by (rtac hoare_derivs.Ass 1);
   524 force 1;
   525 by (defer_tac 1);
   526 ###
   527 by (rtac hoare_derivs.Comp 1);
   528 by (dtac spec 2);
   529 by (dtac spec 2);
   530 by (assume_tac 2);
   531 by (etac conseq1 2);
   532 by (Clarsimp_tac 2);
   533 force 1;
   534 *)
   535 
   536 end