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