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