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
```