src/HOL/UNITY/ProgressSets.thy
author paulson
Tue Mar 18 18:07:06 2003 +0100 (2003-03-18)
changeset 13870 cf947d1ec5ff
parent 13866 b42d7983a822
child 13874 0da2141606c6
permissions -rw-r--r--
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.

Deleted Ring, Module from GroupTheory

Minor UNITY changes
paulson@13853
     1
(*  Title:      HOL/UNITY/ProgressSets
paulson@13853
     2
    ID:         $Id$
paulson@13853
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13853
     4
    Copyright   2003  University of Cambridge
paulson@13853
     5
paulson@13853
     6
Progress Sets.  From 
paulson@13853
     7
paulson@13853
     8
    David Meier and Beverly Sanders,
paulson@13853
     9
    Composing Leads-to Properties
paulson@13853
    10
    Theoretical Computer Science 243:1-2 (2000), 339-361.
paulson@13861
    11
paulson@13861
    12
    David Meier,
paulson@13861
    13
    Progress Properties in Program Refinement and Parallel Composition
paulson@13861
    14
    Swiss Federal Institute of Technology Zurich (1997)
paulson@13853
    15
*)
paulson@13853
    16
paulson@13853
    17
header{*Progress Sets*}
paulson@13853
    18
paulson@13853
    19
theory ProgressSets = Transformers:
paulson@13853
    20
paulson@13866
    21
subsection {*Complete Lattices and the Operator @{term cl}*}
paulson@13866
    22
paulson@13853
    23
constdefs
paulson@13861
    24
  lattice :: "'a set set => bool"
paulson@13861
    25
   --{*Meier calls them closure sets, but they are just complete lattices*}
paulson@13861
    26
   "lattice L ==
paulson@13861
    27
	 (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
paulson@13853
    28
paulson@13853
    29
  cl :: "['a set set, 'a set] => 'a set"
paulson@13853
    30
   --{*short for ``closure''*}
paulson@13861
    31
   "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
paulson@13853
    32
paulson@13861
    33
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
paulson@13861
    34
by (force simp add: lattice_def)
paulson@13853
    35
paulson@13861
    36
lemma empty_in_lattice: "lattice L ==> {} \<in> L"
paulson@13861
    37
by (force simp add: lattice_def)
paulson@13853
    38
paulson@13861
    39
lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L"
paulson@13861
    40
by (simp add: lattice_def)
paulson@13853
    41
paulson@13861
    42
lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L"
paulson@13861
    43
by (simp add: lattice_def)
paulson@13853
    44
paulson@13861
    45
lemma UN_in_lattice:
paulson@13861
    46
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
paulson@13853
    47
apply (simp add: Set.UN_eq) 
paulson@13861
    48
apply (blast intro: Union_in_lattice) 
paulson@13853
    49
done
paulson@13853
    50
paulson@13861
    51
lemma INT_in_lattice:
paulson@13861
    52
     "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
paulson@13853
    53
apply (simp add: INT_eq) 
paulson@13861
    54
apply (blast intro: Inter_in_lattice) 
paulson@13853
    55
done
paulson@13853
    56
paulson@13861
    57
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
paulson@13853
    58
apply (simp only: Un_eq_Union) 
paulson@13861
    59
apply (blast intro: Union_in_lattice) 
paulson@13853
    60
done
paulson@13853
    61
paulson@13861
    62
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
paulson@13853
    63
apply (simp only: Int_eq_Inter) 
paulson@13861
    64
apply (blast intro: Inter_in_lattice) 
paulson@13853
    65
done
paulson@13853
    66
paulson@13861
    67
lemma lattice_stable: "lattice {X. F \<in> stable X}"
paulson@13861
    68
by (simp add: lattice_def stable_def constrains_def, blast)
paulson@13853
    69
paulson@13861
    70
text{*The next three results state that @{term "cl L r"} is the minimal
paulson@13861
    71
 element of @{term L} that includes @{term r}.*}
paulson@13861
    72
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
paulson@13861
    73
apply (simp add: lattice_def cl_def)
paulson@13853
    74
apply (erule conjE)  
paulson@13853
    75
apply (drule spec, erule mp, blast) 
paulson@13853
    76
done
paulson@13853
    77
paulson@13861
    78
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
paulson@13853
    79
by (force simp add: cl_def)
paulson@13853
    80
paulson@13853
    81
text{*The next three lemmas constitute assertion (4.61)*}
paulson@13861
    82
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
paulson@13861
    83
by (simp add: cl_def, blast)
paulson@13861
    84
paulson@13861
    85
lemma subset_cl: "r \<subseteq> cl L r"
paulson@13861
    86
by (simp add: cl_def, blast)
paulson@13861
    87
paulson@13861
    88
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
paulson@13853
    89
by (simp add: cl_def, blast)
paulson@13853
    90
paulson@13861
    91
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
paulson@13861
    92
apply (rule equalityI) 
paulson@13861
    93
 prefer 2 
paulson@13861
    94
  apply (simp add: cl_def, blast)
paulson@13861
    95
apply (rule cl_least)
paulson@13861
    96
 apply (blast intro: Un_in_lattice cl_in_lattice)
paulson@13861
    97
apply (blast intro: subset_cl [THEN subsetD])  
paulson@13861
    98
done
paulson@13853
    99
paulson@13861
   100
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
paulson@13853
   101
apply (rule equalityI) 
paulson@13866
   102
 prefer 2 apply (simp add: cl_def, blast)
paulson@13853
   103
apply (rule cl_least)
paulson@13861
   104
 apply (blast intro: UN_in_lattice cl_in_lattice)
paulson@13853
   105
apply (blast intro: subset_cl [THEN subsetD])  
paulson@13853
   106
done
paulson@13853
   107
paulson@13861
   108
lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
paulson@13853
   109
by (simp add: cl_def, blast)
paulson@13853
   110
paulson@13861
   111
lemma cl_ident: "r\<in>L ==> cl L r = r" 
paulson@13853
   112
by (force simp add: cl_def)
paulson@13853
   113
paulson@13853
   114
text{*Assertion (4.62)*}
paulson@13861
   115
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
paulson@13853
   116
apply (rule iffI) 
paulson@13853
   117
 apply (erule subst)
paulson@13861
   118
 apply (erule cl_in_lattice)  
paulson@13853
   119
apply (erule cl_ident) 
paulson@13853
   120
done
paulson@13853
   121
paulson@13861
   122
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" 
paulson@13861
   123
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
paulson@13861
   124
paulson@13861
   125
paulson@13866
   126
subsection {*Progress Sets and the Main Lemma*}
paulson@13866
   127
paulson@13861
   128
constdefs 
paulson@13861
   129
  closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
paulson@13861
   130
   "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
paulson@13861
   131
                              T \<inter> (B \<union> wp act M) \<in> L"
paulson@13861
   132
paulson@13861
   133
  progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
paulson@13861
   134
   "progress_set F T B ==
paulson@13870
   135
      {L. lattice L & B \<in> L & T \<in> L & closed F T B L}"
paulson@13861
   136
paulson@13861
   137
lemma closedD:
paulson@13861
   138
   "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
paulson@13861
   139
    ==> T \<inter> (B \<union> wp act M) \<in> L"
paulson@13861
   140
by (simp add: closed_def) 
paulson@13861
   141
paulson@13866
   142
text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
paulson@13866
   143
and @{term m} by @{term X}. *}
paulson@13866
   144
paulson@13866
   145
text{*Part of the proof of the claim at the bottom of page 97.  It's
paulson@13866
   146
proved separately because the argument requires a generalization over
paulson@13866
   147
all @{term "act \<in> Acts F"}.*}
paulson@13861
   148
lemma lattice_awp_lemma:
paulson@13866
   149
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13866
   150
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
paulson@13861
   151
      and latt: "lattice C"
paulson@13866
   152
      and TC:   "T \<in> C"
paulson@13866
   153
      and BC:   "B \<in> C"
paulson@13866
   154
      and clos: "closed F T B C"
paulson@13866
   155
    shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
paulson@13861
   156
apply (simp del: INT_simps add: awp_def INT_extend_simps) 
paulson@13861
   157
apply (rule INT_in_lattice [OF latt]) 
paulson@13861
   158
apply (erule closedD [OF clos]) 
paulson@13866
   159
apply (simp add: subset_trans [OF BsubX Un_upper1]) 
paulson@13866
   160
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
paulson@13866
   161
 prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least]) 
paulson@13861
   162
apply (erule ssubst) 
paulson@13866
   163
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
paulson@13861
   164
done
paulson@13861
   165
paulson@13866
   166
text{*Remainder of the proof of the claim at the bottom of page 97.*}
paulson@13861
   167
lemma lattice_lemma:
paulson@13866
   168
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13866
   169
      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
paulson@13861
   170
      and act:  "act \<in> Acts F"
paulson@13861
   171
      and latt: "lattice C"
paulson@13866
   172
      and TC:   "T \<in> C"
paulson@13866
   173
      and BC:   "B \<in> C"
paulson@13866
   174
      and clos: "closed F T B C"
paulson@13866
   175
    shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
paulson@13866
   176
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
paulson@13866
   177
 prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
paulson@13861
   178
apply (drule Int_in_lattice
paulson@13866
   179
              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
paulson@13861
   180
                    latt])
paulson@13861
   181
apply (subgoal_tac
paulson@13866
   182
	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
paulson@13866
   183
	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
paulson@13861
   184
 prefer 2 apply blast 
paulson@13861
   185
apply simp  
paulson@13866
   186
apply (drule Un_in_lattice [OF _ TXC latt])  
paulson@13861
   187
apply (subgoal_tac
paulson@13866
   188
	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
paulson@13866
   189
	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
paulson@13866
   190
 apply simp 
paulson@13866
   191
apply (blast intro: BsubX [THEN subsetD]) 
paulson@13861
   192
done
paulson@13861
   193
paulson@13861
   194
paulson@13866
   195
text{*Induction step for the main lemma*}
paulson@13861
   196
lemma progress_induction_step:
paulson@13866
   197
  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
paulson@13861
   198
      and act:  "act \<in> Acts F"
paulson@13866
   199
      and Xwens: "X \<in> wens_set F B"
paulson@13861
   200
      and latt: "lattice C"
paulson@13866
   201
      and  TC:  "T \<in> C"
paulson@13866
   202
      and  BC:  "B \<in> C"
paulson@13866
   203
      and clos: "closed F T B C"
paulson@13861
   204
      and Fstable: "F \<in> stable T"
paulson@13866
   205
  shows "T \<inter> wens F act X \<in> C"
paulson@13861
   206
proof -
paulson@13866
   207
  from Xwens have BsubX: "B \<subseteq> X"
paulson@13866
   208
    by (rule wens_set_imp_subset) 
paulson@13866
   209
  let ?r = "wens F act X"
paulson@13866
   210
  have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
paulson@13866
   211
    by (simp add: wens_unfold [symmetric])
paulson@13866
   212
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
paulson@13866
   213
    by blast
paulson@13866
   214
  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
paulson@13866
   215
    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
paulson@13866
   216
  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
   217
    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
paulson@13866
   218
  then have "cl C (T\<inter>?r) \<subseteq> 
paulson@13866
   219
             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
paulson@13866
   220
    by (rule cl_mono) 
paulson@13866
   221
  then have "cl C (T\<inter>?r) \<subseteq> 
paulson@13866
   222
             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
paulson@13866
   223
    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
paulson@13866
   224
  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
   225
    by blast
paulson@13866
   226
  then have "cl C (T\<inter>?r) \<subseteq> ?r"
paulson@13866
   227
    by (blast intro!: subset_wens) 
paulson@13866
   228
  then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
paulson@13866
   229
    by (simp add: Int_subset_iff cl_ident TC
paulson@13866
   230
                  subset_trans [OF cl_mono [OF Int_lower1]]) 
paulson@13866
   231
  show ?thesis
paulson@13866
   232
    by (rule cl_subset_in_lattice [OF cl_subset latt]) 
paulson@13861
   233
qed
paulson@13861
   234
paulson@13866
   235
text{*The Lemma proved on page 96*}
paulson@13861
   236
lemma progress_set_lemma:
paulson@13870
   237
     "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
paulson@13861
   238
apply (simp add: progress_set_def, clarify) 
paulson@13861
   239
apply (erule wens_set.induct) 
paulson@13861
   240
  txt{*Base*}
paulson@13861
   241
  apply (simp add: Int_in_lattice) 
paulson@13861
   242
 txt{*The difficult @{term wens} case*}
paulson@13861
   243
 apply (simp add: progress_induction_step) 
paulson@13861
   244
txt{*Disjunctive case*}
paulson@13861
   245
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
paulson@13861
   246
 apply (simp add: Int_Union) 
paulson@13861
   247
apply (blast intro: UN_in_lattice) 
paulson@13861
   248
done
paulson@13861
   249
paulson@13866
   250
paulson@13866
   251
subsection {*The Progress Set Union Theorem*}
paulson@13866
   252
paulson@13866
   253
lemma closed_mono:
paulson@13866
   254
  assumes BB':  "B \<subseteq> B'"
paulson@13866
   255
      and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
paulson@13866
   256
      and B'C:  "B' \<in> C"
paulson@13866
   257
      and TC:   "T \<in> C"
paulson@13866
   258
      and latt: "lattice C"
paulson@13866
   259
  shows "T \<inter> (B' \<union> wp act M) \<in> C"
paulson@13866
   260
proof -
paulson@13866
   261
  from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
paulson@13866
   262
    by (simp add: Int_Un_distrib)
paulson@13866
   263
  then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
paulson@13866
   264
    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
paulson@13866
   265
  show ?thesis
paulson@13866
   266
    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
paulson@13866
   267
        blast intro: BB' [THEN subsetD]) 
paulson@13866
   268
qed
paulson@13866
   269
paulson@13866
   270
paulson@13866
   271
lemma progress_set_mono:
paulson@13866
   272
    assumes BB':  "B \<subseteq> B'"
paulson@13866
   273
    shows
paulson@13866
   274
     "[| B' \<in> C;  C \<in> progress_set F T B|] 
paulson@13866
   275
      ==> C \<in> progress_set F T B'"
paulson@13866
   276
by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
paulson@13866
   277
                 subset_trans [OF BB']) 
paulson@13866
   278
paulson@13866
   279
theorem progress_set_Union:
paulson@13866
   280
  assumes prog: "C \<in> progress_set F T B"
paulson@13870
   281
      and Fstable: "F \<in> stable T"
paulson@13866
   282
      and BB':  "B \<subseteq> B'"
paulson@13866
   283
      and B'C:  "B' \<in> C"
paulson@13866
   284
      and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
paulson@13866
   285
      and leadsTo: "F \<in> A leadsTo B'"
paulson@13866
   286
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
paulson@13870
   287
apply (insert prog Fstable) 
paulson@13866
   288
apply (rule leadsTo_Join [OF leadsTo]) 
paulson@13866
   289
  apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
paulson@13866
   290
apply (simp add: awp_iff_constrains)
paulson@13866
   291
apply (drule progress_set_mono [OF BB' B'C]) 
paulson@13866
   292
apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
paulson@13866
   293
                    BB' [THEN subsetD]) 
paulson@13866
   294
done
paulson@13866
   295
paulson@13870
   296
paulson@13870
   297
subsection {*Some Progress Sets*}
paulson@13870
   298
paulson@13870
   299
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
paulson@13870
   300
by (simp add: progress_set_def lattice_def closed_def)
paulson@13870
   301
paulson@13853
   302
end