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