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