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