src/HOL/UNITY/Transformers.thy
author haftmann
Mon Sep 21 15:35:15 2009 +0200 (2009-09-21)
changeset 32693 6c6b1ba5e71e
parent 32587 caa5ada96a00
child 35416 d8d7d1b785af
permissions -rw-r--r--
tuned proofs
paulson@13821
     1
(*  Title:      HOL/UNITY/Transformers
paulson@13821
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13821
     3
    Copyright   2003  University of Cambridge
paulson@13821
     4
paulson@13866
     5
Predicate Transformers.  From 
paulson@13821
     6
paulson@13821
     7
    David Meier and Beverly Sanders,
paulson@13821
     8
    Composing Leads-to Properties
paulson@13821
     9
    Theoretical Computer Science 243:1-2 (2000), 339-361.
paulson@13866
    10
paulson@13866
    11
    David Meier,
paulson@13866
    12
    Progress Properties in Program Refinement and Parallel Composition
paulson@13866
    13
    Swiss Federal Institute of Technology Zurich (1997)
paulson@13821
    14
*)
paulson@13821
    15
paulson@13821
    16
header{*Predicate Transformers*}
paulson@13821
    17
haftmann@16417
    18
theory Transformers imports Comp begin
paulson@13821
    19
paulson@13821
    20
subsection{*Defining the Predicate Transformers @{term wp},
paulson@13821
    21
   @{term awp} and  @{term wens}*}
paulson@13821
    22
paulson@13821
    23
constdefs
paulson@13821
    24
  wp :: "[('a*'a) set, 'a set] => 'a set"  
paulson@13832
    25
    --{*Dijkstra's weakest-precondition operator (for an individual command)*}
paulson@13821
    26
    "wp act B == - (act^-1 `` (-B))"
paulson@13821
    27
paulson@13832
    28
  awp :: "['a program, 'a set] => 'a set"  
paulson@13832
    29
    --{*Dijkstra's weakest-precondition operator (for a program)*}
paulson@13821
    30
    "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
paulson@13821
    31
paulson@13832
    32
  wens :: "['a program, ('a*'a) set, 'a set] => 'a set"  
paulson@13832
    33
    --{*The weakest-ensures transformer*}
paulson@13821
    34
    "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
paulson@13821
    35
paulson@13821
    36
text{*The fundamental theorem for wp*}
paulson@13821
    37
theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
paulson@13821
    38
by (force simp add: wp_def) 
paulson@13821
    39
paulson@13874
    40
text{*This lemma is a good deal more intuitive than the definition!*}
paulson@13874
    41
lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
paulson@13874
    42
by (simp add: wp_def, blast)
paulson@13874
    43
paulson@13821
    44
lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
paulson@13821
    45
by (force simp add: wp_def) 
paulson@13821
    46
paulson@13832
    47
lemma wp_empty [simp]: "wp act {} = - (Domain act)"
paulson@13832
    48
by (force simp add: wp_def)
paulson@13832
    49
paulson@13832
    50
text{*The identity relation is the skip action*}
paulson@13832
    51
lemma wp_Id [simp]: "wp Id B = B"
paulson@13832
    52
by (simp add: wp_def) 
paulson@13832
    53
paulson@13851
    54
lemma wp_totalize_act:
paulson@13851
    55
     "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)"
paulson@13851
    56
by (simp add: wp_def totalize_act_def, blast)
paulson@13851
    57
paulson@13861
    58
lemma awp_subset: "(awp F A \<subseteq> A)"
paulson@13861
    59
by (force simp add: awp_def wp_def)
paulson@13861
    60
paulson@13821
    61
lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
paulson@13821
    62
by (simp add: awp_def wp_def, blast) 
paulson@13821
    63
paulson@13821
    64
text{*The fundamental theorem for awp*}
paulson@13861
    65
theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
paulson@13821
    66
by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
paulson@13821
    67
paulson@13861
    68
lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)"
paulson@13861
    69
by (simp add: awp_iff_constrains stable_def) 
paulson@13861
    70
paulson@13861
    71
lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A"
paulson@13861
    72
apply (rule equalityI [OF awp_subset]) 
paulson@13861
    73
apply (simp add: awp_iff_stable) 
paulson@13861
    74
done
paulson@13821
    75
paulson@13874
    76
lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B"
paulson@13874
    77
by (simp add: wp_def, blast)
paulson@13874
    78
paulson@13821
    79
lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
paulson@13821
    80
by (simp add: awp_def wp_def, blast)
paulson@13821
    81
paulson@13821
    82
lemma wens_unfold:
paulson@13821
    83
     "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
paulson@13821
    84
apply (simp add: wens_def) 
paulson@13821
    85
apply (rule gfp_unfold) 
paulson@13821
    86
apply (simp add: mono_def wp_def awp_def, blast) 
paulson@13821
    87
done
paulson@13821
    88
paulson@13832
    89
lemma wens_Id [simp]: "wens F Id B = B"
haftmann@32587
    90
by (simp add: wens_def gfp_def wp_def awp_def, blast)
paulson@13832
    91
paulson@13821
    92
text{*These two theorems justify the claim that @{term wens} returns the
paulson@13821
    93
weakest assertion satisfying the ensures property*}
paulson@13821
    94
lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
paulson@13821
    95
apply (simp add: wens_def ensures_def transient_def, clarify) 
paulson@13821
    96
apply (rule rev_bexI, assumption) 
paulson@13821
    97
apply (rule gfp_upperbound)
paulson@13821
    98
apply (simp add: constrains_def awp_def wp_def, blast)
paulson@13821
    99
done
paulson@13821
   100
paulson@13821
   101
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
paulson@13821
   102
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
haftmann@32587
   103
              ensures_def transient_def, blast)
paulson@13821
   104
paulson@13821
   105
text{*These two results constitute assertion (4.13) of the thesis*}
paulson@13821
   106
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
paulson@13821
   107
apply (simp add: wens_def wp_def awp_def) 
paulson@13821
   108
apply (rule gfp_mono, blast) 
paulson@13821
   109
done
paulson@13821
   110
paulson@13821
   111
lemma wens_weakening: "B \<subseteq> wens F act B"
haftmann@32587
   112
by (simp add: wens_def gfp_def, blast)
paulson@13821
   113
paulson@13821
   114
text{*Assertion (6), or 4.16 in the thesis*}
paulson@13821
   115
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
paulson@13821
   116
apply (simp add: wens_def wp_def awp_def) 
paulson@13821
   117
apply (rule gfp_upperbound, blast) 
paulson@13821
   118
done
paulson@13821
   119
paulson@13821
   120
text{*Assertion 4.17 in the thesis*}
nipkow@21312
   121
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
haftmann@32587
   122
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
paulson@15102
   123
  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
paulson@15102
   124
      is declared as an iff-rule, then it's almost impossible to prove. 
paulson@15102
   125
      One proof is via @{text meson} after expanding all definitions, but it's
paulson@15102
   126
      slow!*}
paulson@13821
   127
paulson@13821
   128
text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
paulson@13821
   129
hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
paulson@13821
   130
lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
paulson@13821
   131
apply (simp add: stable_def)
paulson@13821
   132
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
paulson@13821
   133
apply (simp add: Un_Int_distrib2 Compl_partition2) 
paulson@13832
   134
apply (erule constrains_weaken, blast) 
haftmann@32693
   135
apply (simp add: wens_weakening)
paulson@13821
   136
done
paulson@13821
   137
paulson@13821
   138
text{*Assertion 4.20 in the thesis.*}
paulson@13821
   139
lemma wens_Int_eq_lemma:
paulson@13821
   140
      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
paulson@13821
   141
       ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
paulson@13821
   142
apply (rule subset_wens) 
paulson@13821
   143
apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
paulson@13821
   144
apply (simp add: wp_def awp_def, blast)
paulson@13821
   145
done
paulson@13821
   146
paulson@13821
   147
text{*Assertion (8): 4.21 in the thesis. Here we indeed require
paulson@13821
   148
      @{term "act \<in> Acts F"}*}
paulson@13821
   149
lemma wens_Int_eq:
paulson@13821
   150
      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
paulson@13821
   151
       ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
paulson@13821
   152
apply (rule equalityI)
haftmann@32693
   153
 apply (simp_all add: Int_lower1) 
paulson@13821
   154
 apply (rule wens_Int_eq_lemma, assumption+) 
paulson@13821
   155
apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
paulson@13821
   156
done
paulson@13821
   157
paulson@13832
   158
paulson@13821
   159
subsection{*Defining the Weakest Ensures Set*}
paulson@13821
   160
berghofe@23767
   161
inductive_set
paulson@13821
   162
  wens_set :: "['a program, 'a set] => 'a set set"
berghofe@23767
   163
  for F :: "'a program" and B :: "'a set"
berghofe@23767
   164
where
paulson@13821
   165
paulson@13821
   166
  Basis: "B \<in> wens_set F B"
paulson@13821
   167
berghofe@23767
   168
| Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
paulson@13821
   169
berghofe@23767
   170
| Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
paulson@13821
   171
paulson@13821
   172
lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
paulson@13821
   173
apply (erule wens_set.induct) 
paulson@13821
   174
  apply (simp add: constrains_def)
paulson@13821
   175
 apply (drule_tac act1=act and A1=X 
paulson@13821
   176
        in constrains_Un [OF Diff_wens_constrains]) 
paulson@13821
   177
 apply (erule constrains_weaken, blast) 
haftmann@32693
   178
 apply (simp add: wens_weakening) 
paulson@13821
   179
apply (rule constrains_weaken) 
paulson@13821
   180
apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
paulson@13821
   181
done
paulson@13821
   182
paulson@13821
   183
lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
paulson@13821
   184
apply (erule wens_set.induct)
paulson@13821
   185
  apply (rule leadsTo_refl)  
paulson@13832
   186
 apply (blast intro: wens_ensures leadsTo_Trans) 
paulson@13821
   187
apply (blast intro: leadsTo_Union) 
paulson@13821
   188
done
paulson@13821
   189
paulson@13821
   190
lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
paulson@13821
   191
apply (erule leadsTo_induct_pre)
paulson@13861
   192
  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) 
paulson@13861
   193
 apply (clarify, drule ensures_weaken_R, assumption)  
paulson@13821
   194
 apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
paulson@13821
   195
apply (case_tac "S={}") 
paulson@13821
   196
 apply (simp, blast intro: wens_set.Basis)
paulson@13821
   197
apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
paulson@13821
   198
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
paulson@13821
   199
apply (blast intro: wens_set.Union) 
paulson@13821
   200
done
paulson@13821
   201
paulson@13821
   202
text{*Assertion (9): 4.27 in the thesis.*}
paulson@13821
   203
lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
paulson@13821
   204
by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
paulson@13821
   205
paulson@13821
   206
text{*This is the result that requires the definition of @{term wens_set} to
paulson@13832
   207
  require @{term W} to be non-empty in the Unio case, for otherwise we should
paulson@13832
   208
  always have @{term "{} \<in> wens_set F B"}.*}
paulson@13821
   209
lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
paulson@13821
   210
apply (erule wens_set.induct) 
paulson@13821
   211
  apply (blast intro: wens_weakening [THEN subsetD])+
paulson@13821
   212
done
paulson@13821
   213
paulson@13821
   214
paulson@13821
   215
subsection{*Properties Involving Program Union*}
paulson@13821
   216
paulson@13821
   217
text{*Assertion (4.30) of thesis, reoriented*}
paulson@13821
   218
lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
paulson@13821
   219
by (simp add: awp_def wp_def, blast)
paulson@13821
   220
paulson@13861
   221
lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
paulson@13821
   222
by (subst wens_unfold, fast) 
paulson@13821
   223
paulson@13821
   224
text{*Assertion (4.31)*}
paulson@13821
   225
lemma subset_wens_Join:
paulson@13821
   226
      "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
paulson@13821
   227
       ==> A \<subseteq> wens (F\<squnion>G) act B"
paulson@13821
   228
apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
paulson@13821
   229
                    wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
paulson@13821
   230
 apply (rule subset_wens) 
haftmann@32693
   231
 apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
paulson@13821
   232
 apply (simp add: awp_def wp_def, blast) 
paulson@13821
   233
apply (insert wens_subset [of F act B], blast) 
paulson@13821
   234
done
paulson@13821
   235
paulson@13821
   236
text{*Assertion (4.32)*}
paulson@13821
   237
lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
paulson@13821
   238
apply (simp add: wens_def) 
paulson@13821
   239
apply (rule gfp_mono)
paulson@13821
   240
apply (auto simp add: awp_Join_eq)  
paulson@13821
   241
done
paulson@13821
   242
paulson@13821
   243
text{*Lemma, because the inductive step is just too messy.*}
paulson@13821
   244
lemma wens_Union_inductive_step:
paulson@13821
   245
  assumes awpF: "T-B \<subseteq> awp F T"
paulson@13821
   246
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
paulson@13821
   247
  shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
paulson@13821
   248
         ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
paulson@13821
   249
             T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
paulson@13821
   250
apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")  
paulson@13821
   251
 prefer 2
paulson@13821
   252
 apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
paulson@13821
   253
apply (rule equalityI) 
paulson@13821
   254
 prefer 2 apply blast
haftmann@32693
   255
apply (simp add: Int_lower1) 
paulson@13821
   256
apply (frule wens_set_imp_subset) 
paulson@13821
   257
apply (subgoal_tac "T-X \<subseteq> awp F T")  
paulson@13821
   258
 prefer 2 apply (blast intro: awpF [THEN subsetD]) 
paulson@13821
   259
apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
paulson@13821
   260
 prefer 2 apply (blast intro!: wens_mono)
paulson@13821
   261
apply (subst wens_Int_eq, assumption+) 
paulson@13861
   262
apply (rule subset_wens_Join [of _ T], simp, blast)
paulson@13821
   263
apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
paulson@13821
   264
 prefer 2
paulson@13821
   265
 apply (subst wens_Int_eq [symmetric], assumption+) 
paulson@13821
   266
 apply (blast intro: wens_weakening [THEN subsetD], simp) 
paulson@13821
   267
apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
paulson@13821
   268
done
paulson@13821
   269
paulson@13832
   270
theorem wens_Union:
paulson@13821
   271
  assumes awpF: "T-B \<subseteq> awp F T"
paulson@13821
   272
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
paulson@13821
   273
      and major: "X \<in> wens_set F B"
paulson@13821
   274
  shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
paulson@13821
   275
apply (rule wens_set.induct [OF major])
paulson@13821
   276
  txt{*Basis: trivial*}
paulson@13821
   277
  apply (blast intro: wens_set.Basis)
paulson@13821
   278
 txt{*Inductive step*}
paulson@13821
   279
 apply clarify 
paulson@13821
   280
 apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
paulson@13821
   281
  apply (force intro: wens_set.Wens)
paulson@13821
   282
 apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
paulson@13821
   283
txt{*Union: by Axiom of Choice*}
paulson@13821
   284
apply (simp add: ball_conj_distrib Bex_def) 
paulson@13821
   285
apply (clarify dest!: bchoice) 
paulson@13821
   286
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
paulson@13821
   287
apply (blast intro: wens_set.Union) 
paulson@13821
   288
done
paulson@13821
   289
paulson@13866
   290
theorem leadsTo_Join:
paulson@13866
   291
  assumes leadsTo: "F \<in> A leadsTo B"
paulson@13866
   292
      and awpF: "T-B \<subseteq> awp F T"
paulson@13832
   293
      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
paulson@13832
   294
  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
paulson@13832
   295
apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
paulson@13832
   296
apply (rule wens_Union [THEN bexE]) 
paulson@13832
   297
   apply (rule awpF) 
paulson@13851
   298
  apply (erule awpG, assumption)
paulson@13832
   299
apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])  
paulson@13832
   300
done
paulson@13832
   301
paulson@13832
   302
paulson@13832
   303
subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
paulson@13832
   304
text{*Thesis Section 4.3.3*}
paulson@13832
   305
paulson@13832
   306
text{*We start by proving laws about single-assignment programs*}
paulson@13832
   307
lemma awp_single_eq [simp]:
paulson@13832
   308
     "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
paulson@13832
   309
by (force simp add: awp_def wp_def) 
paulson@13832
   310
paulson@13832
   311
lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)"
paulson@13832
   312
by (force simp add: wp_def)
paulson@13832
   313
paulson@13832
   314
lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B"
paulson@13832
   315
apply (rule equalityI)
paulson@13832
   316
 apply (force simp add: wp_def single_valued_def) 
paulson@13832
   317
apply (rule wp_Un_subset) 
paulson@13832
   318
done
paulson@13832
   319
paulson@13832
   320
lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)"
paulson@13832
   321
by (force simp add: wp_def)
paulson@13832
   322
paulson@13832
   323
lemma wp_UN_eq:
paulson@13832
   324
     "[|single_valued act; I\<noteq>{}|]
paulson@13832
   325
      ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
paulson@13832
   326
apply (rule equalityI)
paulson@13832
   327
 prefer 2 apply (rule wp_UN_subset) 
paulson@13832
   328
 apply (simp add: wp_def Image_INT_eq) 
paulson@13832
   329
done
paulson@13832
   330
paulson@13832
   331
lemma wens_single_eq:
paulson@13832
   332
     "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
haftmann@32587
   333
by (simp add: wens_def gfp_def wp_def, blast)
paulson@13832
   334
paulson@13832
   335
paulson@13832
   336
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
paulson@13832
   337
paulson@13832
   338
constdefs
paulson@13832
   339
  wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
haftmann@30971
   340
    "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
paulson@13832
   341
paulson@13832
   342
  wens_single :: "[('a*'a) set, 'a set] => 'a set"  
haftmann@30971
   343
    "wens_single act B == \<Union>i. (wp act ^^ i) B"
paulson@13832
   344
paulson@13832
   345
lemma wens_single_Un_eq:
paulson@13832
   346
      "single_valued act
paulson@13832
   347
       ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
paulson@13832
   348
apply (rule equalityI)
haftmann@32693
   349
 apply (simp_all add: Un_upper1) 
paulson@13832
   350
apply (simp add: wens_single_def wp_UN_eq, clarify) 
paulson@13832
   351
apply (rule_tac a="Suc(i)" in UN_I, auto) 
paulson@13832
   352
done
paulson@13832
   353
paulson@13832
   354
lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
paulson@13832
   355
by force
paulson@13832
   356
paulson@13851
   357
lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
paulson@13851
   358
by (simp add: wens_single_finite_def)
paulson@13851
   359
paulson@13832
   360
lemma wens_single_finite_Suc:
paulson@13832
   361
      "single_valued act
paulson@13832
   362
       ==> wens_single_finite act B (Suc k) =
paulson@13851
   363
           wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
paulson@13832
   364
apply (simp add: wens_single_finite_def image_def 
paulson@13832
   365
                 wp_UN_eq [OF _ atMost_nat_nonempty]) 
paulson@13832
   366
apply (force elim!: le_SucE)
paulson@13832
   367
done
paulson@13832
   368
paulson@13832
   369
lemma wens_single_finite_Suc_eq_wens:
paulson@13832
   370
     "single_valued act
paulson@13832
   371
       ==> wens_single_finite act B (Suc k) =
paulson@13832
   372
           wens (mk_program (init, {act}, allowed)) act 
paulson@13832
   373
                (wens_single_finite act B k)"
paulson@13832
   374
by (simp add: wens_single_finite_Suc wens_single_eq) 
paulson@13832
   375
paulson@13851
   376
lemma def_wens_single_finite_Suc_eq_wens:
paulson@13851
   377
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
paulson@13851
   378
       ==> wens_single_finite act B (Suc k) =
paulson@13851
   379
           wens F act (wens_single_finite act B k)"
paulson@13851
   380
by (simp add: wens_single_finite_Suc_eq_wens) 
paulson@13851
   381
paulson@13832
   382
lemma wens_single_finite_Un_eq:
paulson@13832
   383
      "single_valued act
paulson@13832
   384
       ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
paulson@13832
   385
           \<in> range (wens_single_finite act B)"
paulson@13832
   386
by (simp add: wens_single_finite_Suc [symmetric]) 
paulson@13832
   387
paulson@13832
   388
lemma wens_single_eq_Union:
paulson@13832
   389
      "wens_single act B = \<Union>range (wens_single_finite act B)" 
paulson@13832
   390
by (simp add: wens_single_finite_def wens_single_def, blast) 
paulson@13832
   391
paulson@13832
   392
lemma wens_single_finite_eq_Union:
paulson@13832
   393
     "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)"
paulson@13832
   394
apply (auto simp add: wens_single_finite_def) 
paulson@13832
   395
apply (blast intro: le_trans) 
paulson@13832
   396
done
paulson@13832
   397
paulson@13832
   398
lemma wens_single_finite_mono:
paulson@13832
   399
     "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n"
paulson@13832
   400
by (force simp add:  wens_single_finite_eq_Union [of act B n]) 
paulson@13832
   401
paulson@13832
   402
lemma wens_single_finite_subset_wens_single:
paulson@13832
   403
      "wens_single_finite act B k \<subseteq> wens_single act B"
nipkow@15236
   404
by (simp add: wens_single_eq_Union, blast)
paulson@13832
   405
paulson@13832
   406
lemma subset_wens_single_finite:
paulson@13832
   407
      "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
paulson@13832
   408
       ==> \<exists>m. \<Union>W = wens_single_finite act B m"
paulson@13851
   409
apply (induct k)
nipkow@15236
   410
 apply (rule_tac x=0 in exI, simp, blast)
nipkow@15236
   411
apply (auto simp add: atMost_Suc)
nipkow@15236
   412
apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
nipkow@15236
   413
 prefer 2 apply blast
nipkow@15236
   414
apply (drule_tac x="Suc k" in spec)
paulson@13832
   415
apply (erule notE, rule equalityI)
nipkow@15236
   416
 prefer 2 apply blast
nipkow@15236
   417
apply (subst wens_single_finite_eq_Union)
nipkow@15236
   418
apply (simp add: atMost_Suc, blast)
paulson@13832
   419
done
paulson@13832
   420
paulson@13832
   421
text{*lemma for Union case*}
paulson@13832
   422
lemma Union_eq_wens_single:
paulson@13832
   423
      "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
paulson@13832
   424
        W \<subseteq> insert (wens_single act B)
paulson@13832
   425
            (range (wens_single_finite act B))\<rbrakk>
paulson@13832
   426
       \<Longrightarrow> \<Union>W = wens_single act B"
paulson@13832
   427
apply (case_tac "wens_single act B \<in> W")
paulson@13832
   428
 apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
paulson@13832
   429
apply (simp add: wens_single_eq_Union) 
paulson@13851
   430
apply (rule equalityI, blast) 
paulson@13832
   431
apply (simp add: UN_subset_iff, clarify)
paulson@13832
   432
apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")  
paulson@13851
   433
 apply (blast intro: wens_single_finite_mono [THEN subsetD]) 
paulson@13832
   434
apply (drule_tac x=i in spec)
paulson@13832
   435
apply (force simp add: atMost_def)
paulson@13832
   436
done
paulson@13832
   437
paulson@13832
   438
lemma wens_set_subset_single:
paulson@13832
   439
      "single_valued act
paulson@13832
   440
       ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 
paulson@13832
   441
           insert (wens_single act B) (range (wens_single_finite act B))"
paulson@13832
   442
apply (rule subsetI)  
paulson@13832
   443
apply (erule wens_set.induct)
paulson@13832
   444
  txt{*Basis*} 
nipkow@21733
   445
  apply (fastsimp simp add: wens_single_finite_def)
paulson@13832
   446
 txt{*Wens inductive step*}
nipkow@21733
   447
 apply (case_tac "acta = Id", simp)
paulson@13832
   448
 apply (simp add: wens_single_eq)
nipkow@21733
   449
 apply (elim disjE)
paulson@13832
   450
 apply (simp add: wens_single_Un_eq)
paulson@13832
   451
 apply (force simp add: wens_single_finite_Un_eq)
paulson@13832
   452
txt{*Union inductive step*}
paulson@13832
   453
apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
paulson@13832
   454
 apply (blast dest!: subset_wens_single_finite, simp) 
paulson@13832
   455
apply (rule disjI1 [OF Union_eq_wens_single], blast+)
paulson@13832
   456
done
paulson@13832
   457
paulson@13832
   458
lemma wens_single_finite_in_wens_set:
paulson@13832
   459
      "single_valued act \<Longrightarrow>
paulson@13832
   460
         wens_single_finite act B k
paulson@13832
   461
         \<in> wens_set (mk_program (init, {act}, allowed)) B"
paulson@13832
   462
apply (induct_tac k) 
paulson@13832
   463
 apply (simp add: wens_single_finite_def wens_set.Basis)
paulson@13832
   464
apply (simp add: wens_set.Wens
paulson@13832
   465
                 wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 
paulson@13832
   466
done
paulson@13832
   467
paulson@13832
   468
lemma single_subset_wens_set:
paulson@13832
   469
      "single_valued act
paulson@13832
   470
       ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
paulson@13832
   471
           wens_set (mk_program (init, {act}, allowed)) B"
paulson@13832
   472
apply (simp add: wens_single_eq_Union UN_eq) 
paulson@13832
   473
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
paulson@13832
   474
done
paulson@13832
   475
paulson@13832
   476
text{*Theorem (4.29)*}
paulson@13832
   477
theorem wens_set_single_eq:
paulson@13851
   478
     "[|F = mk_program (init, {act}, allowed); single_valued act|]
paulson@13851
   479
      ==> wens_set F B =
paulson@13851
   480
          insert (wens_single act B) (range (wens_single_finite act B))"
paulson@13832
   481
apply (rule equalityI)
paulson@13851
   482
 apply (simp add: wens_set_subset_single) 
paulson@13851
   483
apply (erule ssubst, erule single_subset_wens_set) 
paulson@13832
   484
done
paulson@13832
   485
paulson@13853
   486
text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
paulson@13853
   487
paulson@13866
   488
lemma fp_leadsTo_Join:
paulson@13853
   489
    "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
paulson@13866
   490
apply (rule leadsTo_Join, assumption, blast)
paulson@13866
   491
apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 
paulson@13853
   492
done
paulson@13853
   493
paulson@13821
   494
end