src/HOL/UNITY/Guar.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13819 78f5885b76a9
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@7400
     1
(*  Title:      HOL/UNITY/Guar.thy
paulson@7400
     2
    ID:         $Id$
paulson@7400
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7400
     4
    Copyright   1999  University of Cambridge
paulson@7400
     5
ehmety@11190
     6
From Chandy and Sanders, "Reasoning About Program Composition",
ehmety@11190
     7
Technical Report 2000-003, University of Florida, 2000.
ehmety@11190
     8
ehmety@11190
     9
Revised by Sidi Ehmety on January 2001
ehmety@11190
    10
ehmety@11190
    11
Added: Compatibility, weakest guarantees, etc.
ehmety@11190
    12
ehmety@11190
    13
and Weakest existential property,
ehmety@11190
    14
from Charpentier and Chandy "Theorems about Composition",
ehmety@11190
    15
Fifth International Conference on Mathematics of Program, 2000.
ehmety@11190
    16
paulson@7400
    17
*)
paulson@7400
    18
paulson@13798
    19
header{*Guarantees Specifications*}
paulson@13798
    20
paulson@13792
    21
theory Guar = Comp:
paulson@7400
    22
wenzelm@12338
    23
instance program :: (type) order
paulson@13792
    24
  by (intro_classes,
paulson@13792
    25
      (assumption | rule component_refl component_trans component_antisym
paulson@13792
    26
                     program_less_le)+)
paulson@13792
    27
paulson@7400
    28
paulson@7400
    29
constdefs
paulson@7400
    30
paulson@7400
    31
  (*Existential and Universal properties.  I formalize the two-program
paulson@7400
    32
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
paulson@7400
    33
paulson@13792
    34
  ex_prop  :: "'a program set => bool"
paulson@13805
    35
   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
paulson@7400
    36
paulson@13792
    37
  strict_ex_prop  :: "'a program set => bool"
paulson@13805
    38
   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
paulson@7400
    39
paulson@13792
    40
  uv_prop  :: "'a program set => bool"
paulson@13805
    41
   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
paulson@7400
    42
paulson@13792
    43
  strict_uv_prop  :: "'a program set => bool"
paulson@13792
    44
   "strict_uv_prop X == 
paulson@13805
    45
      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
paulson@7400
    46
paulson@13792
    47
  guar :: "['a program set, 'a program set] => 'a program set"
paulson@10064
    48
          (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
paulson@13805
    49
   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
ehmety@11190
    50
  
paulson@7400
    51
ehmety@11190
    52
  (* Weakest guarantees *)
paulson@13792
    53
   wg :: "['a program, 'a program set] =>  'a program set"
paulson@13805
    54
  "wg F Y == Union({X. F \<in> X guarantees Y})"
ehmety@11190
    55
ehmety@11190
    56
   (* Weakest existential property stronger than X *)
ehmety@11190
    57
   wx :: "('a program) set => ('a program)set"
paulson@13805
    58
   "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
ehmety@11190
    59
  
ehmety@11190
    60
  (*Ill-defined programs can arise through "Join"*)
paulson@13792
    61
  welldef :: "'a program set"
paulson@13805
    62
  "welldef == {F. Init F \<noteq> {}}"
ehmety@11190
    63
  
paulson@13792
    64
  refines :: "['a program, 'a program, 'a program set] => bool"
paulson@7400
    65
			("(3_ refines _ wrt _)" [10,10,10] 10)
ehmety@11190
    66
  "G refines F wrt X ==
paulson@13805
    67
     \<forall>H. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X) --> 
paulson@13805
    68
         (G Join H \<in> welldef \<inter> X)"
paulson@7400
    69
paulson@13792
    70
  iso_refines :: "['a program, 'a program, 'a program set] => bool"
ehmety@11190
    71
                              ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
ehmety@11190
    72
  "G iso_refines F wrt X ==
paulson@13805
    73
   F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
paulson@7400
    74
paulson@13792
    75
paulson@13792
    76
lemma OK_insert_iff:
paulson@13792
    77
     "(OK (insert i I) F) = 
paulson@13805
    78
      (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
paulson@13792
    79
by (auto intro: ok_sym simp add: OK_iff_ok)
paulson@13792
    80
paulson@13792
    81
paulson@13792
    82
(*** existential properties ***)
paulson@13798
    83
lemma ex1 [rule_format]: 
paulson@13792
    84
 "[| ex_prop X; finite GG |] ==>  
paulson@13805
    85
     GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
paulson@13792
    86
apply (unfold ex_prop_def)
paulson@13792
    87
apply (erule finite_induct)
paulson@13792
    88
apply (auto simp add: OK_insert_iff Int_insert_left)
paulson@13792
    89
done
paulson@13792
    90
paulson@13792
    91
paulson@13792
    92
lemma ex2: 
paulson@13805
    93
     "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X 
paulson@13792
    94
      ==> ex_prop X"
paulson@13792
    95
apply (unfold ex_prop_def, clarify)
paulson@13792
    96
apply (drule_tac x = "{F,G}" in spec)
paulson@13792
    97
apply (auto dest: ok_sym simp add: OK_iff_ok)
paulson@13792
    98
done
paulson@13792
    99
paulson@13792
   100
paulson@13792
   101
(*Chandy & Sanders take this as a definition*)
paulson@13792
   102
lemma ex_prop_finite:
paulson@13792
   103
     "ex_prop X = 
paulson@13805
   104
      (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
paulson@13792
   105
by (blast intro: ex1 ex2)
paulson@13792
   106
paulson@13792
   107
paulson@13792
   108
(*Their "equivalent definition" given at the end of section 3*)
paulson@13792
   109
lemma ex_prop_equiv: 
paulson@13805
   110
     "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
paulson@13792
   111
apply auto
paulson@13812
   112
apply (unfold ex_prop_def component_of_def, safe, blast) 
paulson@13792
   113
apply blast 
paulson@13792
   114
apply (subst Join_commute) 
paulson@13792
   115
apply (drule ok_sym, blast) 
paulson@13792
   116
done
paulson@13792
   117
paulson@13792
   118
paulson@13792
   119
(*** universal properties ***)
paulson@13792
   120
lemma uv1 [rule_format]: 
paulson@13792
   121
     "[| uv_prop X; finite GG |] 
paulson@13805
   122
      ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
paulson@13792
   123
apply (unfold uv_prop_def)
paulson@13792
   124
apply (erule finite_induct)
paulson@13792
   125
apply (auto simp add: Int_insert_left OK_insert_iff)
paulson@13792
   126
done
paulson@13792
   127
paulson@13792
   128
lemma uv2: 
paulson@13805
   129
     "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
paulson@13792
   130
      ==> uv_prop X"
paulson@13792
   131
apply (unfold uv_prop_def)
paulson@13792
   132
apply (rule conjI)
paulson@13792
   133
 apply (drule_tac x = "{}" in spec)
paulson@13792
   134
 prefer 2
paulson@13792
   135
 apply clarify 
paulson@13792
   136
 apply (drule_tac x = "{F,G}" in spec)
paulson@13792
   137
apply (auto dest: ok_sym simp add: OK_iff_ok)
paulson@13792
   138
done
paulson@13792
   139
paulson@13792
   140
(*Chandy & Sanders take this as a definition*)
paulson@13792
   141
lemma uv_prop_finite:
paulson@13792
   142
     "uv_prop X = 
paulson@13805
   143
      (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
paulson@13792
   144
by (blast intro: uv1 uv2)
paulson@13792
   145
paulson@13792
   146
(*** guarantees ***)
paulson@13792
   147
paulson@13792
   148
lemma guaranteesI:
paulson@13805
   149
     "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)  
paulson@13805
   150
      ==> F \<in> X guarantees Y"
paulson@13792
   151
by (simp add: guar_def component_def)
paulson@13792
   152
paulson@13792
   153
lemma guaranteesD: 
paulson@13805
   154
     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X |]  
paulson@13805
   155
      ==> F Join G \<in> Y"
paulson@13792
   156
by (unfold guar_def component_def, blast)
paulson@13792
   157
paulson@13792
   158
(*This version of guaranteesD matches more easily in the conclusion
paulson@13805
   159
  The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
paulson@13792
   160
lemma component_guaranteesD: 
paulson@13805
   161
     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G |]  
paulson@13805
   162
      ==> H \<in> Y"
paulson@13792
   163
by (unfold guar_def, blast)
paulson@13792
   164
paulson@13792
   165
lemma guarantees_weaken: 
paulson@13805
   166
     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
paulson@13792
   167
by (unfold guar_def, blast)
paulson@13792
   168
paulson@13805
   169
lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
paulson@13792
   170
by (unfold guar_def, blast)
paulson@13792
   171
paulson@13792
   172
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
paulson@13805
   173
lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
paulson@13792
   174
by (unfold guar_def, blast)
paulson@13792
   175
paulson@13792
   176
(*Remark at end of section 4.1 *)
paulson@13792
   177
paulson@13792
   178
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
paulson@13792
   179
apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
paulson@13792
   180
apply safe
paulson@13792
   181
 apply (drule_tac x = x in spec)
paulson@13792
   182
 apply (drule_tac [2] x = x in spec)
paulson@13792
   183
 apply (drule_tac [2] sym)
paulson@13792
   184
apply (auto simp add: component_of_def)
paulson@13792
   185
done
paulson@13792
   186
paulson@13792
   187
lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
paulson@13792
   188
apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
paulson@13792
   189
apply safe
paulson@13792
   190
apply (auto simp add: component_of_def dest: sym)
paulson@13792
   191
done
paulson@13792
   192
paulson@13792
   193
lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
paulson@13792
   194
apply (rule iffI)
paulson@13792
   195
apply (rule ex_prop_imp)
paulson@13792
   196
apply (auto simp add: guarantees_imp) 
paulson@13792
   197
done
paulson@13792
   198
paulson@13792
   199
paulson@13792
   200
(** Distributive laws.  Re-orient to perform miniscoping **)
paulson@13792
   201
paulson@13792
   202
lemma guarantees_UN_left: 
paulson@13805
   203
     "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
paulson@13792
   204
by (unfold guar_def, blast)
paulson@13792
   205
paulson@13792
   206
lemma guarantees_Un_left: 
paulson@13805
   207
     "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
paulson@13792
   208
by (unfold guar_def, blast)
paulson@13792
   209
paulson@13792
   210
lemma guarantees_INT_right: 
paulson@13805
   211
     "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
paulson@13792
   212
by (unfold guar_def, blast)
paulson@13792
   213
paulson@13792
   214
lemma guarantees_Int_right: 
paulson@13805
   215
     "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
paulson@13792
   216
by (unfold guar_def, blast)
paulson@13792
   217
paulson@13792
   218
lemma guarantees_Int_right_I:
paulson@13805
   219
     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
paulson@13805
   220
     ==> F \<in> Z guarantees (X \<inter> Y)"
paulson@13792
   221
by (simp add: guarantees_Int_right)
paulson@13792
   222
paulson@13792
   223
lemma guarantees_INT_right_iff:
paulson@13805
   224
     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
paulson@13792
   225
by (simp add: guarantees_INT_right)
paulson@13792
   226
paulson@13805
   227
lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
paulson@13792
   228
by (unfold guar_def, blast)
paulson@13792
   229
paulson@13792
   230
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
paulson@13792
   231
by (unfold guar_def, blast)
paulson@13792
   232
paulson@13792
   233
(** The following two can be expressed using intersection and subset, which
paulson@13792
   234
    is more faithful to the text but looks cryptic.
paulson@13792
   235
**)
paulson@13792
   236
paulson@13792
   237
lemma combining1: 
paulson@13805
   238
    "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
paulson@13805
   239
     ==> F \<in> (V \<inter> Y) guarantees Z"
paulson@13792
   240
paulson@13792
   241
by (unfold guar_def, blast)
paulson@13792
   242
paulson@13792
   243
lemma combining2: 
paulson@13805
   244
    "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
paulson@13805
   245
     ==> F \<in> V guarantees (X \<union> Z)"
paulson@13792
   246
by (unfold guar_def, blast)
paulson@13792
   247
paulson@13792
   248
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
paulson@13792
   249
    does not suit Isabelle... **)
paulson@13792
   250
paulson@13805
   251
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
paulson@13792
   252
lemma all_guarantees: 
paulson@13805
   253
     "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
paulson@13792
   254
by (unfold guar_def, blast)
paulson@13792
   255
paulson@13805
   256
(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
paulson@13792
   257
lemma ex_guarantees: 
paulson@13805
   258
     "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
paulson@13792
   259
by (unfold guar_def, blast)
paulson@13792
   260
paulson@13792
   261
paulson@13792
   262
(*** Additional guarantees laws, by lcp ***)
paulson@13792
   263
paulson@13792
   264
lemma guarantees_Join_Int: 
paulson@13805
   265
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
paulson@13805
   266
     ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
paulson@13792
   267
apply (unfold guar_def)
paulson@13792
   268
apply (simp (no_asm))
paulson@13792
   269
apply safe
paulson@13792
   270
apply (simp add: Join_assoc)
paulson@13792
   271
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
paulson@13792
   272
apply (simp add: ok_commute)
paulson@13792
   273
apply (simp (no_asm_simp) add: Join_ac)
paulson@13792
   274
done
paulson@13792
   275
paulson@13792
   276
lemma guarantees_Join_Un: 
paulson@13805
   277
    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
paulson@13805
   278
     ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
paulson@13792
   279
apply (unfold guar_def)
paulson@13792
   280
apply (simp (no_asm))
paulson@13792
   281
apply safe
paulson@13792
   282
apply (simp add: Join_assoc)
paulson@13792
   283
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
paulson@13792
   284
apply (simp add: ok_commute)
paulson@13792
   285
apply (simp (no_asm_simp) add: Join_ac)
paulson@13792
   286
done
paulson@13792
   287
paulson@13792
   288
lemma guarantees_JN_INT: 
paulson@13805
   289
     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
paulson@13805
   290
      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
paulson@13792
   291
apply (unfold guar_def, auto)
paulson@13792
   292
apply (drule bspec, assumption)
paulson@13792
   293
apply (rename_tac "i")
paulson@13792
   294
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
paulson@13792
   295
apply (auto intro: OK_imp_ok
paulson@13792
   296
            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
paulson@13792
   297
done
paulson@13792
   298
paulson@13792
   299
lemma guarantees_JN_UN: 
paulson@13805
   300
    "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
paulson@13805
   301
     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
paulson@13792
   302
apply (unfold guar_def, auto)
paulson@13792
   303
apply (drule bspec, assumption)
paulson@13792
   304
apply (rename_tac "i")
paulson@13792
   305
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
paulson@13792
   306
apply (auto intro: OK_imp_ok
paulson@13792
   307
            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
paulson@13792
   308
done
paulson@13792
   309
paulson@13792
   310
paulson@13792
   311
(*** guarantees laws for breaking down the program, by lcp ***)
paulson@13792
   312
paulson@13792
   313
lemma guarantees_Join_I1: 
paulson@13805
   314
     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
paulson@13792
   315
apply (unfold guar_def)
paulson@13792
   316
apply (simp (no_asm))
paulson@13792
   317
apply safe
paulson@13792
   318
apply (simp add: Join_assoc)
paulson@13792
   319
done
paulson@13792
   320
paulson@13792
   321
lemma guarantees_Join_I2:
paulson@13805
   322
     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
paulson@13792
   323
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
paulson@13792
   324
apply (blast intro: guarantees_Join_I1)
paulson@13792
   325
done
paulson@13792
   326
paulson@13792
   327
lemma guarantees_JN_I: 
paulson@13805
   328
     "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
paulson@13805
   329
      ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
paulson@13792
   330
apply (unfold guar_def, clarify)
paulson@13792
   331
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
paulson@13792
   332
apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
paulson@13792
   333
done
paulson@13792
   334
paulson@13792
   335
paulson@13792
   336
(*** well-definedness ***)
paulson@13792
   337
paulson@13805
   338
lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
paulson@13792
   339
by (unfold welldef_def, auto)
paulson@13792
   340
paulson@13805
   341
lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
paulson@13792
   342
by (unfold welldef_def, auto)
paulson@13792
   343
paulson@13792
   344
(*** refinement ***)
paulson@13792
   345
paulson@13792
   346
lemma refines_refl: "F refines F wrt X"
paulson@13792
   347
by (unfold refines_def, blast)
paulson@13792
   348
paulson@13792
   349
paulson@13792
   350
(* Goalw [refines_def]
paulson@13792
   351
     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
paulson@13792
   352
by Auto_tac
paulson@13792
   353
qed "refines_trans"; *)
paulson@13792
   354
paulson@13792
   355
paulson@13792
   356
paulson@13792
   357
lemma strict_ex_refine_lemma: 
paulson@13792
   358
     "strict_ex_prop X  
paulson@13805
   359
      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)  
paulson@13805
   360
              = (F \<in> X --> G \<in> X)"
paulson@13792
   361
by (unfold strict_ex_prop_def, auto)
paulson@13792
   362
paulson@13792
   363
lemma strict_ex_refine_lemma_v: 
paulson@13792
   364
     "strict_ex_prop X  
paulson@13805
   365
      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
paulson@13805
   366
          (F \<in> welldef \<inter> X --> G \<in> X)"
paulson@13792
   367
apply (unfold strict_ex_prop_def, safe)
paulson@13792
   368
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
paulson@13792
   369
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
paulson@13792
   370
done
paulson@13792
   371
paulson@13792
   372
lemma ex_refinement_thm:
paulson@13792
   373
     "[| strict_ex_prop X;   
paulson@13805
   374
         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]  
paulson@13792
   375
      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
paulson@13792
   376
apply (rule_tac x = SKIP in allE, assumption)
paulson@13792
   377
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
paulson@13792
   378
done
paulson@13792
   379
paulson@13792
   380
paulson@13792
   381
lemma strict_uv_refine_lemma: 
paulson@13792
   382
     "strict_uv_prop X ==> 
paulson@13805
   383
      (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
paulson@13792
   384
by (unfold strict_uv_prop_def, blast)
paulson@13792
   385
paulson@13792
   386
lemma strict_uv_refine_lemma_v: 
paulson@13792
   387
     "strict_uv_prop X  
paulson@13805
   388
      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
paulson@13805
   389
          (F \<in> welldef \<inter> X --> G \<in> X)"
paulson@13792
   390
apply (unfold strict_uv_prop_def, safe)
paulson@13792
   391
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
paulson@13792
   392
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
paulson@13792
   393
done
paulson@13792
   394
paulson@13792
   395
lemma uv_refinement_thm:
paulson@13792
   396
     "[| strict_uv_prop X;   
paulson@13805
   397
         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> 
paulson@13805
   398
             G Join H \<in> welldef |]  
paulson@13792
   399
      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
paulson@13792
   400
apply (rule_tac x = SKIP in allE, assumption)
paulson@13792
   401
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
paulson@13792
   402
done
paulson@13792
   403
paulson@13792
   404
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
paulson@13792
   405
lemma guarantees_equiv: 
paulson@13805
   406
    "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
paulson@13792
   407
by (unfold guar_def component_of_def, auto)
paulson@13792
   408
paulson@13805
   409
lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
paulson@13792
   410
by (unfold wg_def, auto)
paulson@13792
   411
paulson@13792
   412
lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
paulson@13792
   413
by (unfold wg_def guar_def, blast)
paulson@13792
   414
paulson@13792
   415
lemma wg_equiv: 
paulson@13805
   416
  "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
paulson@13792
   417
apply (unfold wg_def)
paulson@13792
   418
apply (simp (no_asm) add: guarantees_equiv)
paulson@13792
   419
apply (rule iffI)
paulson@13792
   420
apply (rule_tac [2] x = "{H}" in exI)
paulson@13792
   421
apply (blast+)
paulson@13792
   422
done
paulson@13792
   423
paulson@13792
   424
paulson@13805
   425
lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
paulson@13792
   426
by (simp add: wg_equiv)
paulson@13792
   427
paulson@13792
   428
lemma wg_finite: 
paulson@13805
   429
    "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)  
paulson@13805
   430
          --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
paulson@13792
   431
apply clarify
paulson@13805
   432
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
paulson@13792
   433
apply (drule_tac X = X in component_of_wg, simp)
paulson@13792
   434
apply (simp add: component_of_def)
paulson@13805
   435
apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
paulson@13792
   436
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
paulson@13792
   437
done
paulson@13792
   438
paulson@13805
   439
lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
paulson@13792
   440
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
paulson@13792
   441
apply blast
paulson@13792
   442
done
paulson@13792
   443
paulson@13792
   444
(** From Charpentier and Chandy "Theorems About Composition" **)
paulson@13792
   445
(* Proposition 2 *)
paulson@13792
   446
lemma wx_subset: "(wx X)<=X"
paulson@13792
   447
by (unfold wx_def, auto)
paulson@13792
   448
paulson@13792
   449
lemma wx_ex_prop: "ex_prop (wx X)"
paulson@13792
   450
apply (unfold wx_def)
paulson@13792
   451
apply (simp (no_asm) add: ex_prop_equiv)
paulson@13792
   452
apply safe
paulson@13792
   453
apply blast
paulson@13792
   454
apply auto
paulson@13792
   455
done
paulson@13792
   456
paulson@13805
   457
lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
paulson@13792
   458
by (unfold wx_def, auto)
paulson@13792
   459
paulson@13792
   460
(* Proposition 6 *)
paulson@13805
   461
lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
paulson@13792
   462
apply (unfold ex_prop_def, safe)
paulson@13792
   463
apply (drule_tac x = "G Join Ga" in spec)
paulson@13792
   464
apply (force simp add: ok_Join_iff1 Join_assoc)
paulson@13792
   465
apply (drule_tac x = "F Join Ga" in spec)
paulson@13792
   466
apply (simp (no_asm_use) add: ok_Join_iff1)
paulson@13792
   467
apply safe
paulson@13792
   468
apply (simp (no_asm_simp) add: ok_commute)
paulson@13792
   469
apply (subgoal_tac "F Join G = G Join F")
paulson@13792
   470
apply (simp (no_asm_simp) add: Join_assoc)
paulson@13792
   471
apply (simp (no_asm) add: Join_commute)
paulson@13792
   472
done
paulson@13792
   473
paulson@13792
   474
(* Equivalence with the other definition of wx *)
paulson@13792
   475
paulson@13792
   476
lemma wx_equiv: 
paulson@13792
   477
 "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
paulson@13792
   478
paulson@13792
   479
apply (unfold wx_def, safe)
paulson@13792
   480
apply (simp (no_asm_use) add: ex_prop_def)
paulson@13792
   481
apply (drule_tac x = x in spec)
paulson@13792
   482
apply (drule_tac x = G in spec)
paulson@13792
   483
apply (frule_tac c = "x Join G" in subsetD, safe)
paulson@13792
   484
apply (simp (no_asm))
paulson@13805
   485
apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
paulson@13792
   486
apply (rule_tac [2] wx'_ex_prop)
paulson@13792
   487
apply (rotate_tac 1)
paulson@13792
   488
apply (drule_tac x = SKIP in spec, auto)
paulson@13792
   489
done
paulson@13792
   490
paulson@13792
   491
paulson@13792
   492
(* Propositions 7 to 11 are about this second definition of wx. And
paulson@13792
   493
   they are the same as the ones proved for the first definition of wx by equivalence *)
paulson@13792
   494
   
paulson@13792
   495
(* Proposition 12 *)
paulson@13792
   496
(* Main result of the paper *)
paulson@13792
   497
lemma guarantees_wx_eq: 
paulson@13805
   498
   "(X guarantees Y) = wx(-X \<union> Y)"
paulson@13792
   499
apply (unfold guar_def)
paulson@13792
   500
apply (simp (no_asm) add: wx_equiv)
paulson@13792
   501
done
paulson@13792
   502
paulson@13792
   503
(* {* Corollary, but this result has already been proved elsewhere *}
paulson@13792
   504
 "ex_prop(X guarantees Y)"
paulson@13792
   505
  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
paulson@13792
   506
  qed "guarantees_ex_prop";
paulson@13792
   507
*)
paulson@13792
   508
paulson@13792
   509
(* Rules given in section 7 of Chandy and Sander's
paulson@13792
   510
    Reasoning About Program composition paper *)
paulson@13792
   511
paulson@13792
   512
lemma stable_guarantees_Always:
paulson@13805
   513
     "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
paulson@13792
   514
apply (rule guaranteesI)
paulson@13792
   515
apply (simp (no_asm) add: Join_commute)
paulson@13792
   516
apply (rule stable_Join_Always1)
paulson@13792
   517
apply (simp_all add: invariant_def Join_stable)
paulson@13792
   518
done
paulson@13792
   519
paulson@13792
   520
(* To be moved to WFair.ML *)
paulson@13805
   521
lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
paulson@13792
   522
apply (drule_tac B = "A-B" in constrains_weaken_L)
paulson@13792
   523
apply (drule_tac [2] B = "A-B" in transient_strengthen)
paulson@13792
   524
apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
paulson@13792
   525
apply (blast+)
paulson@13792
   526
done
paulson@13792
   527
paulson@13792
   528
paulson@13792
   529
paulson@13792
   530
lemma constrains_guarantees_leadsTo:
paulson@13805
   531
     "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
paulson@13792
   532
apply (rule guaranteesI)
paulson@13792
   533
apply (rule leadsTo_Basis')
paulson@13792
   534
apply (drule constrains_weaken_R)
paulson@13792
   535
prefer 2 apply assumption
paulson@13792
   536
apply blast
paulson@13792
   537
apply (blast intro: Join_transient_I1)
paulson@13792
   538
done
paulson@13792
   539
paulson@7400
   540
end