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