src/HOL/UNITY/ProgressSets.thy
author haftmann
Mon Sep 21 15:35:15 2009 +0200 (2009-09-21)
changeset 32693 6c6b1ba5e71e
parent 32604 8b3e2bc91a46
child 32960 69916a850301
permissions -rw-r--r--
tuned proofs
paulson@13853
     1
(*  Title:      HOL/UNITY/ProgressSets
paulson@13853
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13853
     3
    Copyright   2003  University of Cambridge
paulson@13853
     4
paulson@13853
     5
Progress Sets.  From 
paulson@13853
     6
paulson@13853
     7
    David Meier and Beverly Sanders,
paulson@13853
     8
    Composing Leads-to Properties
paulson@13853
     9
    Theoretical Computer Science 243:1-2 (2000), 339-361.
paulson@13861
    10
paulson@13861
    11
    David Meier,
paulson@13861
    12
    Progress Properties in Program Refinement and Parallel Composition
paulson@13861
    13
    Swiss Federal Institute of Technology Zurich (1997)
paulson@13853
    14
*)
paulson@13853
    15
paulson@13853
    16
header{*Progress Sets*}
paulson@13853
    17
haftmann@16417
    18
theory ProgressSets imports Transformers begin
paulson@13853
    19
paulson@13866
    20
subsection {*Complete Lattices and the Operator @{term cl}*}
paulson@13866
    21
paulson@13853
    22
constdefs
paulson@13861
    23
  lattice :: "'a set set => bool"
paulson@13861
    24
   --{*Meier calls them closure sets, but they are just complete lattices*}
paulson@13861
    25
   "lattice L ==
paulson@13861
    26
	 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
paulson@13853
    27
paulson@13853
    28
  cl :: "['a set set, 'a set] => 'a set"
paulson@13853
    29
   --{*short for ``closure''*}
paulson@13861
    30
   "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
paulson@13853
    31
paulson@13861
    32
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
paulson@13861
    33
by (force simp add: lattice_def)
paulson@13853
    34
paulson@13861
    35
lemma empty_in_lattice: "lattice L ==> {} \<in> L"
paulson@13861
    36
by (force simp add: lattice_def)
paulson@13853
    37
paulson@13861
    38
lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
paulson@13861
    39
by (simp add: lattice_def)
paulson@13853
    40
paulson@13861
    41
lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
paulson@13861
    42
by (simp add: lattice_def)
paulson@13853
    43
paulson@13861
    44
lemma UN_in_lattice:
paulson@13861
    45
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
haftmann@32139
    46
apply (simp add: UN_eq) 
paulson@13861
    47
apply (blast intro: Union_in_lattice) 
paulson@13853
    48
done
paulson@13853
    49
paulson@13861
    50
lemma INT_in_lattice:
paulson@13861
    51
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
paulson@13853
    52
apply (simp add: INT_eq) 
paulson@13861
    53
apply (blast intro: Inter_in_lattice) 
paulson@13853
    54
done
paulson@13853
    55
paulson@13861
    56
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
paulson@13853
    57
apply (simp only: Un_eq_Union) 
paulson@13861
    58
apply (blast intro: Union_in_lattice) 
paulson@13853
    59
done
paulson@13853
    60
paulson@13861
    61
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
paulson@13853
    62
apply (simp only: Int_eq_Inter) 
paulson@13861
    63
apply (blast intro: Inter_in_lattice) 
paulson@13853
    64
done
paulson@13853
    65
paulson@13861
    66
lemma lattice_stable: "lattice {X. F \<in> stable X}"
paulson@13861
    67
by (simp add: lattice_def stable_def constrains_def, blast)
paulson@13853
    68
paulson@13861
    69
text{*The next three results state that @{term "cl L r"} is the minimal
paulson@13861
    70
 element of @{term L} that includes @{term r}.*}
paulson@13861
    71
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
paulson@13861
    72
apply (simp add: lattice_def cl_def)
paulson@13853
    73
apply (erule conjE)  
paulson@13853
    74
apply (drule spec, erule mp, blast) 
paulson@13853
    75
done
paulson@13853
    76
paulson@13861
    77
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
paulson@13853
    78
by (force simp add: cl_def)
paulson@13853
    79
paulson@13853
    80
text{*The next three lemmas constitute assertion (4.61)*}
paulson@13861
    81
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
paulson@13861
    82
by (simp add: cl_def, blast)
paulson@13861
    83
paulson@13861
    84
lemma subset_cl: "r \<subseteq> cl L r"
paulson@13861
    85
by (simp add: cl_def, blast)
paulson@13861
    86
paulson@13874
    87
text{*A reformulation of @{thm subset_cl}*}
paulson@13874
    88
lemma clI: "x \<in> r ==> x \<in> cl L r"
paulson@13874
    89
by (simp add: cl_def, blast)
paulson@13874
    90
paulson@13874
    91
text{*A reformulation of @{thm cl_least}*}
paulson@13874
    92
lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
paulson@13874
    93
by (force simp add: cl_def)
paulson@13874
    94
paulson@13861
    95
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
paulson@13853
    96
by (simp add: cl_def, blast)
paulson@13853
    97
paulson@13861
    98
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
paulson@13861
    99
apply (rule equalityI) 
paulson@13861
   100
 prefer 2 
paulson@13861
   101
  apply (simp add: cl_def, blast)
paulson@13861
   102
apply (rule cl_least)
paulson@13861
   103
 apply (blast intro: Un_in_lattice cl_in_lattice)
paulson@13861
   104
apply (blast intro: subset_cl [THEN subsetD])  
paulson@13861
   105
done
paulson@13853
   106
paulson@13861
   107
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
paulson@13853
   108
apply (rule equalityI) 
paulson@13866
   109
 prefer 2 apply (simp add: cl_def, blast)
paulson@13853
   110
apply (rule cl_least)
paulson@13861
   111
 apply (blast intro: UN_in_lattice cl_in_lattice)
paulson@13853
   112
apply (blast intro: subset_cl [THEN subsetD])  
paulson@13853
   113
done
paulson@13853
   114
paulson@13874
   115
lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s"
paulson@13874
   116
by (simp add: cl_def, blast)
paulson@13874
   117
paulson@13861
   118
lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
paulson@13853
   119
by (simp add: cl_def, blast)
paulson@13853
   120
paulson@13861
   121
lemma cl_ident: "r\<in>L ==> cl L r = r" 
paulson@13853
   122
by (force simp add: cl_def)
paulson@13853
   123
paulson@13874
   124
lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
paulson@13874
   125
by (simp add: cl_ident empty_in_lattice)
paulson@13874
   126
paulson@13874
   127
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
paulson@13874
   128
by (simp add: cl_ident UNIV_in_lattice)
paulson@13874
   129
paulson@13853
   130
text{*Assertion (4.62)*}
paulson@13861
   131
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
paulson@13853
   132
apply (rule iffI) 
paulson@13853
   133
 apply (erule subst)
paulson@13861
   134
 apply (erule cl_in_lattice)  
paulson@13853
   135
apply (erule cl_ident) 
paulson@13853
   136
done
paulson@13853
   137
paulson@13861
   138
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 
paulson@13861
   139
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
paulson@13861
   140
paulson@13861
   141
paulson@13866
   142
subsection {*Progress Sets and the Main Lemma*}
paulson@13888
   143
text{*A progress set satisfies certain closure conditions and is a 
paulson@13888
   144
simple way of including the set @{term "wens_set F B"}.*}
paulson@13866
   145
paulson@13861
   146
constdefs 
paulson@13861
   147
  closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
paulson@13861
   148
   "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
paulson@13861
   149
                              T \<inter> (B \<union> wp act M) \<in> L"
paulson@13861
   150
paulson@13861
   151
  progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
paulson@13861
   152
   "progress_set F T B ==
paulson@13870
   153
      {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
paulson@13861
   154
paulson@13861
   155
lemma closedD:
paulson@13861
   156
   "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
paulson@14150
   157
    ==> T \<inter> (B \<union> wp act M) \<in> L" 
paulson@13861
   158
by (simp add: closed_def) 
paulson@13861
   159
paulson@13866
   160
text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
paulson@13866
   161
and @{term m} by @{term X}. *}
paulson@13866
   162
paulson@13866
   163
text{*Part of the proof of the claim at the bottom of page 97.  It's
paulson@13866
   164
proved separately because the argument requires a generalization over
paulson@13866
   165
all @{term "act \<in> Acts F"}.*}
paulson@13861
   166
lemma lattice_awp_lemma:
paulson@13866
   167
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13866
   168
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
paulson@13861
   169
      and latt: "lattice C"
paulson@13866
   170
      and TC:   "T \<in> C"
paulson@13866
   171
      and BC:   "B \<in> C"
paulson@13866
   172
      and clos: "closed F T B C"
paulson@13866
   173
    shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
paulson@13861
   174
apply (simp del: INT_simps add: awp_def INT_extend_simps) 
paulson@13861
   175
apply (rule INT_in_lattice [OF latt]) 
paulson@13861
   176
apply (erule closedD [OF clos]) 
paulson@13866
   177
apply (simp add: subset_trans [OF BsubX Un_upper1]) 
paulson@13866
   178
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
paulson@13874
   179
 prefer 2 apply (blast intro: TC clD) 
paulson@13861
   180
apply (erule ssubst) 
paulson@13866
   181
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
paulson@13861
   182
done
paulson@13861
   183
paulson@13866
   184
text{*Remainder of the proof of the claim at the bottom of page 97.*}
paulson@13861
   185
lemma lattice_lemma:
paulson@13866
   186
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13866
   187
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
paulson@13861
   188
      and act:  "act \<in> Acts F"
paulson@13861
   189
      and latt: "lattice C"
paulson@13866
   190
      and TC:   "T \<in> C"
paulson@13866
   191
      and BC:   "B \<in> C"
paulson@13866
   192
      and clos: "closed F T B C"
paulson@13866
   193
    shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
paulson@13866
   194
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
paulson@13866
   195
 prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
paulson@13861
   196
apply (drule Int_in_lattice
paulson@13866
   197
              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
paulson@13861
   198
                    latt])
paulson@13861
   199
apply (subgoal_tac
paulson@13866
   200
	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
paulson@13866
   201
	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
paulson@13861
   202
 prefer 2 apply blast 
paulson@13861
   203
apply simp  
paulson@13866
   204
apply (drule Un_in_lattice [OF _ TXC latt])  
paulson@13861
   205
apply (subgoal_tac
paulson@13866
   206
	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
paulson@13866
   207
	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
paulson@13866
   208
 apply simp 
paulson@13866
   209
apply (blast intro: BsubX [THEN subsetD]) 
paulson@13861
   210
done
paulson@13861
   211
paulson@13861
   212
paulson@13866
   213
text{*Induction step for the main lemma*}
paulson@13861
   214
lemma progress_induction_step:
paulson@13866
   215
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13861
   216
      and act:  "act \<in> Acts F"
paulson@13866
   217
      and Xwens: "X \<in> wens_set F B"
paulson@13861
   218
      and latt: "lattice C"
paulson@13866
   219
      and  TC:  "T \<in> C"
paulson@13866
   220
      and  BC:  "B \<in> C"
paulson@13866
   221
      and clos: "closed F T B C"
paulson@13861
   222
      and Fstable: "F \<in> stable T"
paulson@13866
   223
  shows "T \<inter> wens F act X \<in> C"
paulson@13861
   224
proof -
paulson@13866
   225
  from Xwens have BsubX: "B \<subseteq> X"
paulson@13866
   226
    by (rule wens_set_imp_subset) 
paulson@13866
   227
  let ?r = "wens F act X"
paulson@13866
   228
  have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
paulson@13866
   229
    by (simp add: wens_unfold [symmetric])
paulson@13866
   230
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
paulson@13866
   231
    by blast
paulson@13866
   232
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
paulson@13866
   233
    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
paulson@13866
   234
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
paulson@13866
   235
    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
paulson@13866
   236
  then have "cl C (T\<inter>?r) \<subseteq> 
paulson@13866
   237
             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
paulson@13866
   238
    by (rule cl_mono) 
paulson@13866
   239
  then have "cl C (T\<inter>?r) \<subseteq> 
paulson@13866
   240
             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
paulson@13866
   241
    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
paulson@13866
   242
  then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
paulson@13866
   243
    by blast
paulson@13866
   244
  then have "cl C (T\<inter>?r) \<subseteq> ?r"
paulson@13866
   245
    by (blast intro!: subset_wens) 
paulson@13866
   246
  then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
haftmann@32693
   247
    by (simp add: cl_ident TC
paulson@13866
   248
                  subset_trans [OF cl_mono [OF Int_lower1]]) 
paulson@13866
   249
  show ?thesis
paulson@13866
   250
    by (rule cl_subset_in_lattice [OF cl_subset latt]) 
paulson@13861
   251
qed
paulson@13861
   252
paulson@13888
   253
text{*Proved on page 96 of Meier's thesis.  The special case when
paulson@13888
   254
   @{term "T=UNIV"} states that every progress set for the program @{term F}
paulson@13888
   255
   and set @{term B} includes the set @{term "wens_set F B"}.*}
paulson@13861
   256
lemma progress_set_lemma:
paulson@13870
   257
     "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
paulson@13861
   258
apply (simp add: progress_set_def, clarify) 
paulson@13861
   259
apply (erule wens_set.induct) 
paulson@13861
   260
  txt{*Base*}
paulson@13861
   261
  apply (simp add: Int_in_lattice) 
paulson@13861
   262
 txt{*The difficult @{term wens} case*}
paulson@13861
   263
 apply (simp add: progress_induction_step) 
paulson@13861
   264
txt{*Disjunctive case*}
paulson@13861
   265
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
paulson@13861
   266
 apply (simp add: Int_Union) 
paulson@13861
   267
apply (blast intro: UN_in_lattice) 
paulson@13861
   268
done
paulson@13861
   269
paulson@13866
   270
paulson@13866
   271
subsection {*The Progress Set Union Theorem*}
paulson@13866
   272
paulson@13866
   273
lemma closed_mono:
paulson@13866
   274
  assumes BB':  "B \<subseteq> B'"
paulson@13866
   275
      and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
paulson@13866
   276
      and B'C:  "B' \<in> C"
paulson@13866
   277
      and TC:   "T \<in> C"
paulson@13866
   278
      and latt: "lattice C"
paulson@13866
   279
  shows "T \<inter> (B' \<union> wp act M) \<in> C"
paulson@13866
   280
proof -
paulson@13866
   281
  from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
paulson@13866
   282
    by (simp add: Int_Un_distrib)
paulson@13866
   283
  then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
paulson@13866
   284
    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
paulson@13866
   285
  show ?thesis
paulson@13866
   286
    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
paulson@13866
   287
        blast intro: BB' [THEN subsetD]) 
paulson@13866
   288
qed
paulson@13866
   289
paulson@13866
   290
paulson@13866
   291
lemma progress_set_mono:
paulson@13866
   292
    assumes BB':  "B \<subseteq> B'"
paulson@13866
   293
    shows
paulson@13866
   294
     "[| B' \<in> C;  C \<in> progress_set F T B|] 
paulson@13866
   295
      ==> C \<in> progress_set F T B'"
paulson@13866
   296
by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
paulson@13866
   297
                 subset_trans [OF BB']) 
paulson@13866
   298
paulson@13866
   299
theorem progress_set_Union:
paulson@13874
   300
  assumes leadsTo: "F \<in> A leadsTo B'"
paulson@13874
   301
      and prog: "C \<in> progress_set F T B"
paulson@13870
   302
      and Fstable: "F \<in> stable T"
paulson@13866
   303
      and BB':  "B \<subseteq> B'"
paulson@13866
   304
      and B'C:  "B' \<in> C"
paulson@13866
   305
      and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
paulson@13866
   306
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
paulson@13870
   307
apply (insert prog Fstable) 
paulson@13866
   308
apply (rule leadsTo_Join [OF leadsTo]) 
paulson@13866
   309
  apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
paulson@13866
   310
apply (simp add: awp_iff_constrains)
paulson@13866
   311
apply (drule progress_set_mono [OF BB' B'C]) 
paulson@13866
   312
apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
paulson@13866
   313
                    BB' [THEN subsetD]) 
paulson@13866
   314
done
paulson@13866
   315
paulson@13870
   316
paulson@13870
   317
subsection {*Some Progress Sets*}
paulson@13870
   318
paulson@13870
   319
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
paulson@13870
   320
by (simp add: progress_set_def lattice_def closed_def)
paulson@13870
   321
paulson@13874
   322
paulson@13874
   323
paulson@13885
   324
subsubsection {*Lattices and Relations*}
paulson@13874
   325
text{*From Meier's thesis, section 4.5.3*}
paulson@13874
   326
paulson@13874
   327
constdefs
paulson@13874
   328
  relcl :: "'a set set => ('a * 'a) set"
paulson@13885
   329
    -- {*Derived relation from a lattice*}
paulson@13874
   330
    "relcl L == {(x,y). y \<in> cl L {x}}"
paulson@13885
   331
  
paulson@13885
   332
  latticeof :: "('a * 'a) set => 'a set set"
paulson@13885
   333
    -- {*Derived lattice from a relation: the set of upwards-closed sets*}
paulson@13885
   334
    "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
paulson@13885
   335
paulson@13874
   336
paulson@13874
   337
lemma relcl_refl: "(a,a) \<in> relcl L"
paulson@13874
   338
by (simp add: relcl_def subset_cl [THEN subsetD])
paulson@13874
   339
paulson@13874
   340
lemma relcl_trans:
paulson@13874
   341
     "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
paulson@13874
   342
apply (simp add: relcl_def)
paulson@13874
   343
apply (blast intro: clD cl_in_lattice)
paulson@13874
   344
done
paulson@13874
   345
nipkow@30198
   346
lemma refl_relcl: "lattice L ==> refl (relcl L)"
nipkow@30198
   347
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
paulson@13874
   348
paulson@13874
   349
lemma trans_relcl: "lattice L ==> trans (relcl L)"
paulson@13874
   350
by (blast intro: relcl_trans transI)
paulson@13874
   351
paulson@13885
   352
lemma lattice_latticeof: "lattice (latticeof r)"
paulson@13885
   353
by (auto simp add: lattice_def latticeof_def)
paulson@13885
   354
paulson@13885
   355
lemma lattice_singletonI:
paulson@13885
   356
     "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L"
paulson@13885
   357
apply (cut_tac UN_singleton [of X]) 
paulson@13885
   358
apply (erule subst) 
paulson@13885
   359
apply (simp only: UN_in_lattice) 
paulson@13885
   360
done
paulson@13885
   361
paulson@13885
   362
text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
paulson@13885
   363
lemma cl_latticeof:
nipkow@30198
   364
     "[|refl r; trans r|] 
paulson@13885
   365
      ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
paulson@13885
   366
apply (rule equalityI) 
paulson@13885
   367
 apply (rule cl_least) 
paulson@13885
   368
  apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
nipkow@30198
   369
 apply (simp add: latticeof_def refl_on_def, blast)
paulson@13885
   370
apply (simp add: latticeof_def, clarify)
paulson@13885
   371
apply (unfold cl_def, blast) 
paulson@13885
   372
done
paulson@13885
   373
paulson@13885
   374
text{*Related to (4.71).*}
paulson@13874
   375
lemma cl_eq_Collect_relcl:
paulson@13874
   376
     "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 
paulson@13885
   377
apply (cut_tac UN_singleton [of X]) 
paulson@13885
   378
apply (erule subst) 
paulson@13874
   379
apply (force simp only: relcl_def cl_UN)
paulson@13874
   380
done
paulson@13874
   381
paulson@13885
   382
text{*Meier's theorem of section 4.5.3*}
paulson@13885
   383
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
paulson@13885
   384
apply (rule equalityI) 
paulson@13885
   385
 prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 
paulson@13885
   386
apply (rename_tac X)
paulson@13885
   387
apply (rule cl_subset_in_lattice)   
paulson@13885
   388
 prefer 2 apply assumption
paulson@13885
   389
apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
paulson@13885
   390
apply (drule equalityD1)   
paulson@13885
   391
apply (rule subset_trans) 
paulson@13885
   392
 prefer 2 apply assumption
paulson@13885
   393
apply (thin_tac "?U \<subseteq> X") 
paulson@13885
   394
apply (cut_tac A=X in UN_singleton) 
paulson@13885
   395
apply (erule subst) 
paulson@13885
   396
apply (simp only: cl_UN lattice_latticeof 
paulson@13885
   397
                  cl_latticeof [OF refl_relcl trans_relcl]) 
paulson@13885
   398
apply (simp add: relcl_def) 
paulson@13885
   399
done
paulson@13885
   400
paulson@13885
   401
theorem relcl_latticeof_eq:
nipkow@30198
   402
     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
berghofe@23767
   403
by (simp add: relcl_def cl_latticeof)
paulson@13885
   404
paulson@13874
   405
paulson@13874
   406
subsubsection {*Decoupling Theorems*}
paulson@13874
   407
paulson@13874
   408
constdefs
paulson@13874
   409
  decoupled :: "['a program, 'a program] => bool"
paulson@13874
   410
   "decoupled F G ==
paulson@13874
   411
	\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
paulson@13874
   412
paulson@13874
   413
paulson@13874
   414
text{*Rao's Decoupling Theorem*}
paulson@13874
   415
lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
paulson@13874
   416
by (simp add: stable_def constrains_def, blast) 
paulson@13874
   417
paulson@13874
   418
theorem decoupling:
paulson@13874
   419
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13874
   420
      and Gstable: "G \<in> stable B"
paulson@13874
   421
      and dec:     "decoupled F G"
paulson@13874
   422
  shows "F\<squnion>G \<in> A leadsTo B"
paulson@13874
   423
proof -
paulson@13874
   424
  have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B"
paulson@13874
   425
    by (simp add: progress_set_def lattice_stable Gstable closed_def
paulson@13874
   426
                  stable_Un [OF Gstable] dec [unfolded decoupled_def]) 
paulson@13874
   427
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
paulson@13874
   428
    by (rule progress_set_Union [OF leadsTo prog],
paulson@13874
   429
        simp_all add: Gstable stableco)
paulson@13874
   430
  thus ?thesis by simp
paulson@13874
   431
qed
paulson@13874
   432
paulson@13874
   433
paulson@13874
   434
text{*Rao's Weak Decoupling Theorem*}
paulson@13874
   435
theorem weak_decoupling:
paulson@13874
   436
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13874
   437
      and stable: "F\<squnion>G \<in> stable B"
paulson@13874
   438
      and dec:     "decoupled F (F\<squnion>G)"
paulson@13874
   439
  shows "F\<squnion>G \<in> A leadsTo B"
paulson@13874
   440
proof -
paulson@13874
   441
  have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" 
paulson@13874
   442
    by (simp del: Join_stable
paulson@13874
   443
             add: progress_set_def lattice_stable stable closed_def
paulson@13874
   444
                  stable_Un [OF stable] dec [unfolded decoupled_def])
paulson@13874
   445
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
paulson@13874
   446
    by (rule progress_set_Union [OF leadsTo prog],
paulson@13874
   447
        simp_all del: Join_stable add: stable,
paulson@13874
   448
        simp add: stableco) 
paulson@13874
   449
  thus ?thesis by simp
paulson@13874
   450
qed
paulson@13874
   451
paulson@13874
   452
text{*The ``Decoupling via @{term G'} Union Theorem''*}
paulson@13874
   453
theorem decoupling_via_aux:
paulson@13874
   454
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13874
   455
      and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
paulson@13874
   456
      and GG':  "G \<le> G'"  
paulson@13874
   457
               --{*Beware!  This is the converse of the refinement relation!*}
paulson@13874
   458
  shows "F\<squnion>G \<in> A leadsTo B"
paulson@13874
   459
proof -
paulson@13874
   460
  from prog have stable: "G' \<in> stable B"
paulson@13874
   461
    by (simp add: progress_set_def)
paulson@13874
   462
  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
paulson@13874
   463
    by (rule progress_set_Union [OF leadsTo prog],
paulson@13874
   464
        simp_all add: stable stableco component_stable [OF GG'])
paulson@13874
   465
  thus ?thesis by simp
paulson@13874
   466
qed
paulson@13874
   467
paulson@13874
   468
paulson@13874
   469
subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
paulson@13874
   470
paulson@13888
   471
subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
paulson@13874
   472
constdefs 
paulson@13874
   473
  commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
paulson@13874
   474
   "commutes F T B L ==
paulson@13874
   475
       \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 
paulson@13874
   476
           cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
paulson@13874
   477
paulson@13874
   478
paulson@13888
   479
text{*From Meier's thesis, section 4.5.6*}
paulson@13885
   480
lemma commutativity1_lemma:
paulson@13874
   481
  assumes commutes: "commutes F T B L" 
paulson@13874
   482
      and lattice:  "lattice L"
paulson@13874
   483
      and BL: "B \<in> L"
paulson@13874
   484
      and TL: "T \<in> L"
paulson@13874
   485
  shows "closed F T B L"
paulson@13874
   486
apply (simp add: closed_def, clarify)
paulson@13874
   487
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
haftmann@32693
   488
apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
paulson@13874
   489
                 cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
paulson@13874
   490
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
paulson@13874
   491
 prefer 2 
paulson@15102
   492
 apply (cut_tac commutes, simp add: commutes_def) 
paulson@13874
   493
apply (erule subset_trans) 
paulson@13874
   494
apply (simp add: cl_ident)
paulson@13874
   495
apply (blast intro: rev_subsetD [OF _ wp_mono]) 
paulson@13874
   496
done
paulson@13874
   497
paulson@13888
   498
text{*Version packaged with @{thm progress_set_Union}*}
paulson@13885
   499
lemma commutativity1:
paulson@13885
   500
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13885
   501
      and lattice:  "lattice L"
paulson@13885
   502
      and BL: "B \<in> L"
paulson@13885
   503
      and TL: "T \<in> L"
paulson@13885
   504
      and Fstable: "F \<in> stable T"
paulson@13885
   505
      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
paulson@13885
   506
      and commutes: "commutes F T B L" 
paulson@13885
   507
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
paulson@13885
   508
by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
paulson@13885
   509
    simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) 
paulson@13885
   510
paulson@13885
   511
paulson@13885
   512
paulson@13874
   513
text{*Possibly move to Relation.thy, after @{term single_valued}*}
paulson@13874
   514
constdefs
paulson@13874
   515
  funof :: "[('a*'b)set, 'a] => 'b"
paulson@13874
   516
   "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
paulson@13874
   517
paulson@13874
   518
lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"
paulson@13874
   519
by (simp add: funof_def single_valued_def, blast)
paulson@13874
   520
paulson@13874
   521
lemma funof_Pair_in:
paulson@13874
   522
     "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
paulson@13874
   523
by (force simp add: funof_eq) 
paulson@13874
   524
paulson@13874
   525
lemma funof_in:
paulson@13874
   526
     "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 
paulson@13874
   527
by (force simp add: funof_eq)
paulson@13874
   528
 
paulson@13874
   529
lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A"
paulson@13874
   530
by (force simp add: in_wp_iff funof_eq)
paulson@13874
   531
paulson@13874
   532
paulson@13874
   533
subsubsection{*Commutativity of Functions and Relation*}
paulson@13874
   534
text{*Thesis, page 109*}
paulson@13874
   535
haftmann@32604
   536
(*FIXME: this proof is still an ungodly mess*)
paulson@13888
   537
text{*From Meier's thesis, section 4.5.6*}
paulson@13885
   538
lemma commutativity2_lemma:
paulson@13874
   539
  assumes dcommutes: 
paulson@13874
   540
        "\<forall>act \<in> Acts F. 
paulson@13874
   541
         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
paulson@13874
   542
                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
paulson@13874
   543
      and determ: "!!act. act \<in> Acts F ==> single_valued act"
paulson@13874
   544
      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
paulson@13874
   545
      and lattice:  "lattice L"
paulson@13874
   546
      and BL: "B \<in> L"
paulson@13874
   547
      and TL: "T \<in> L"
paulson@13874
   548
      and Fstable: "F \<in> stable T"
paulson@13874
   549
  shows  "commutes F T B L"
haftmann@32604
   550
apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
haftmann@32604
   551
proof -
haftmann@32604
   552
  fix M and act and t
haftmann@32604
   553
  assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
haftmann@32604
   554
  then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
haftmann@32604
   555
    by (force simp add: cl_eq_Collect_relcl [OF lattice])
haftmann@32604
   556
  then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
haftmann@32604
   557
    by blast
haftmann@32604
   558
  then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
haftmann@32604
   559
    apply (intro ballI impI) 
haftmann@32604
   560
    apply (subst cl_ident [symmetric], assumption)
haftmann@32604
   561
    apply (simp add: relcl_def)  
haftmann@32604
   562
    apply (blast intro: cl_mono [THEN [2] rev_subsetD])
haftmann@32604
   563
    done
haftmann@32604
   564
  with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
haftmann@32604
   565
    by (force intro!: funof_in 
haftmann@32604
   566
      simp add: wp_def stable_def constrains_def determ total)
haftmann@32604
   567
  with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
haftmann@32604
   568
    by (intro dcommutes [rule_format]) assumption+ 
haftmann@32604
   569
  with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
haftmann@32604
   570
    by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
haftmann@32604
   571
  with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
haftmann@32604
   572
    by (blast intro: funof_imp_wp determ) 
haftmann@32604
   573
  with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
haftmann@32604
   574
    by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
haftmann@32604
   575
  then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
haftmann@32604
   576
    by simp
haftmann@32604
   577
qed
haftmann@32604
   578
  
paulson@13888
   579
text{*Version packaged with @{thm progress_set_Union}*}
paulson@13885
   580
lemma commutativity2:
paulson@13885
   581
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13885
   582
      and dcommutes: 
paulson@13885
   583
        "\<forall>act \<in> Acts F. 
paulson@13885
   584
         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
paulson@13885
   585
                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
paulson@13885
   586
      and determ: "!!act. act \<in> Acts F ==> single_valued act"
paulson@13885
   587
      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
paulson@13885
   588
      and lattice:  "lattice L"
paulson@13885
   589
      and BL: "B \<in> L"
paulson@13885
   590
      and TL: "T \<in> L"
paulson@13885
   591
      and Fstable: "F \<in> stable T"
paulson@13885
   592
      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
paulson@13885
   593
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
paulson@13885
   594
apply (rule commutativity1 [OF leadsTo lattice]) 
paulson@13885
   595
apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
paulson@13885
   596
                     lattice BL TL Fstable)
paulson@13885
   597
done
paulson@13885
   598
paulson@13885
   599
paulson@13888
   600
subsection {*Monotonicity*}
paulson@14150
   601
text{*From Meier's thesis, section 4.5.7, page 110*}
paulson@13888
   602
(*to be continued?*)
paulson@13888
   603
paulson@13853
   604
end