src/HOL/UNITY/WFair.thy
 changeset 13812 91713a1915ee parent 13805 3786b2fd6808 child 14112 95d51043d2a3
```     1.1 --- a/src/HOL/UNITY/WFair.thy	Sat Feb 08 14:46:22 2003 +0100
1.2 +++ b/src/HOL/UNITY/WFair.thy	Sat Feb 08 16:05:33 2003 +0100
1.3 @@ -3,21 +3,44 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1998  University of Cambridge
1.6
1.7 -Weak Fairness versions of transient, ensures, leadsTo.
1.8 +Conditional Fairness versions of transient, ensures, leadsTo.
1.9
1.10  From Misra, "A Logic for Concurrent Programming", 1994
1.11  *)
1.12
1.15
1.16  theory WFair = UNITY:
1.17
1.18 +text{*The original version of this theory was based on weak fairness.  (Thus,
1.19 +the entire UNITY development embodied this assumption, until February 2003.)
1.20 +Weak fairness states that if a command is enabled continuously, then it is
1.22 +fairness: every command is executed infinitely often.
1.23 +
1.24 +In fact, Misra's paper on "Progress" seems to be ambiguous about the correct
1.25 +interpretation, and says that the two forms of fairness are equivalent.  They
1.26 +differ only on their treatment of partial transitions, which under
1.27 +unconditional fairness behave magically.  That is because if there are partial
1.28 +transitions then there may be no fair executions, making all leads-to
1.29 +properties hold vacuously.
1.30 +
1.31 +Unconditional fairness has some great advantages.  By distinguishing partial
1.32 +transitions from total ones that are the identity on part of their domain, it
1.33 +is more expressive.  Also, by simplifying the definition of the transient
1.34 +property, it simplifies many proofs.  A drawback is that some laws only hold
1.35 +under the assumption that all transitions are total.  The best-known of these
1.36 +is the impossibility law for leads-to.
1.37 +*}
1.38 +
1.39  constdefs
1.40
1.41 -  (*This definition specifies weak fairness.  The rest of the theory
1.42 -    is generic to all forms of fairness.*)
1.43 +  --{*This definition specifies conditional fairness.  The rest of the theory
1.44 +      is generic to all forms of fairness.  To get weak fairness, conjoin
1.45 +      the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies
1.46 +      that the action is enabled over all of @{term A}.*}
1.47    transient :: "'a set => 'a program set"
1.48 -    "transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}"
1.49 +    "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
1.50
1.51    ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
1.52      "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
1.53 @@ -25,8 +48,8 @@
1.54
1.55  consts
1.56
1.57 -  (*LEADS-TO constant for the inductive definition*)
1.58    leads :: "'a program => ('a set * 'a set) set"
1.59 +    --{*LEADS-TO constant for the inductive definition*}
1.60
1.61
1.63 @@ -41,12 +64,12 @@
1.64
1.65  constdefs
1.66
1.67 -  (*visible version of the LEADS-TO relation*)
1.68    leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
1.69 +     --{*visible version of the LEADS-TO relation*}
1.71
1.72 -  (*wlt F B is the largest set that leads to B*)
1.73    wlt :: "['a program, 'a set] => 'a set"
1.74 +     --{*predicate transformer: the largest set that leads to @{term B}*}
1.75      "wlt F B == Union {A. F \<in> A leadsTo B}"
1.76
1.77  syntax (xsymbols)
1.78 @@ -55,9 +78,17 @@
1.79
1.80  subsection{*transient*}
1.81
1.82 +lemma stable_transient:
1.83 +    "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
1.84 +apply (simp add: stable_def constrains_def transient_def, clarify)
1.85 +apply (rule rev_bexI, auto)
1.86 +done
1.87 +
1.88  lemma stable_transient_empty:
1.89 -    "[| F \<in> stable A; F \<in> transient A |] ==> A = {}"
1.90 -by (unfold stable_def constrains_def transient_def, blast)
1.91 +    "[| F \<in> stable A; F \<in> transient A; all_total F |] ==> A = {}"
1.92 +apply (drule stable_transient, assumption)
1.94 +done
1.95
1.96  lemma transient_strengthen:
1.97      "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
1.98 @@ -66,22 +97,34 @@
1.99  done
1.100
1.101  lemma transientI:
1.102 -    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> F \<in> transient A"
1.103 +    "[| act: Acts F;  act``A \<subseteq> -A |] ==> F \<in> transient A"
1.104  by (unfold transient_def, blast)
1.105
1.106  lemma transientE:
1.107      "[| F \<in> transient A;
1.108 -        !!act. [| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> P |]
1.109 +        !!act. [| act: Acts F;  act``A \<subseteq> -A |] ==> P |]
1.110       ==> P"
1.111  by (unfold transient_def, blast)
1.112
1.113 -lemma transient_UNIV [simp]: "transient UNIV = {}"
1.114 -by (unfold transient_def, blast)
1.115 -
1.116  lemma transient_empty [simp]: "transient {} = UNIV"
1.117  by (unfold transient_def, auto)
1.118
1.119
1.120 +text{*This equation recovers the notion of weak fairness.  A totalized
1.121 +      program satisfies a transient assertion just if the original program
1.122 +      contains a suitable action that is also enabled.*}
1.123 +lemma totalize_transient_iff:
1.124 +   "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
1.125 +apply (simp add: totalize_def totalize_act_def transient_def
1.126 +                 Un_Image Un_subset_iff, safe)
1.127 +apply (blast intro!: rev_bexI)+
1.128 +done
1.129 +
1.130 +lemma totalize_transientI:
1.131 +    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |]
1.132 +     ==> totalize F \<in> transient A"
1.133 +by (simp add: totalize_transient_iff, blast)
1.134 +
1.135  subsection{*ensures*}
1.136
1.137  lemma ensuresI:
1.138 @@ -98,7 +141,7 @@
1.139  apply (blast intro: constrains_weaken transient_strengthen)
1.140  done
1.141
1.142 -(*The L-version (precondition strengthening) fails, but we have this*)
1.143 +text{*The L-version (precondition strengthening) fails, but we have this*}
1.144  lemma stable_ensures_Int:
1.145      "[| F \<in> stable C;  F \<in> A ensures B |]
1.146      ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
1.147 @@ -134,7 +177,7 @@
1.148  lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
1.150
1.151 -(*Useful with cancellation, disjunction*)
1.152 +text{*Useful with cancellation, disjunction*}
1.155
1.156 @@ -142,7 +185,7 @@
1.157       "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
1.159
1.160 -(*The Union introduction rule as we should have liked to state it*)
1.161 +text{*The Union introduction rule as we should have liked to state it*}
1.163      "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
1.165 @@ -162,7 +205,7 @@
1.167  done
1.168
1.169 -(*Binary union introduction rule*)
1.170 +text{*Binary union introduction rule*}
1.172       "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
1.173  apply (subst Un_eq_Union)
1.174 @@ -174,7 +217,7 @@
1.175  by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
1.176
1.177
1.178 -(*The INDUCTION rule as we should have liked to state it*)
1.179 +text{*The INDUCTION rule as we should have liked to state it*}
1.181    "[| F \<in> za leadsTo zb;
1.182        !!A B. F \<in> A ensures B ==> P A B;
1.183 @@ -203,16 +246,16 @@
1.184
1.185  (** Variant induction rule: on the preconditions for B **)
1.186
1.187 -(*Lemma is the weak version: can't see how to do it in one step*)
1.188 +text{*Lemma is the weak version: can't see how to do it in one step*}
1.190    "[| F \<in> za leadsTo zb;
1.191        P zb;
1.192        !!A B. [| F \<in> A ensures B;  P B |] ==> P A;
1.193        !!S. \<forall>A \<in> S. P A ==> P (Union S)
1.194     |] ==> P za"
1.195 -(*by induction on this formula*)
1.196 +txt{*by induction on this formula*}
1.197  apply (subgoal_tac "P zb --> P za")
1.198 -(*now solve first subgoal: this formula is sufficient*)
1.199 +txt{*now solve first subgoal: this formula is sufficient*}
1.202  apply (blast+)
1.203 @@ -240,7 +283,7 @@
1.204       "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
1.206
1.207 -(*Distributes over binary unions*)
1.208 +text{*Distributes over binary unions*}
1.210       "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
1.212 @@ -271,7 +314,7 @@
1.214  done
1.215
1.216 -(*Binary union version*)
1.217 +text{*Binary union version*}
1.219       "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]
1.220        ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
1.221 @@ -309,18 +352,17 @@
1.222  done
1.223
1.224
1.225 -
1.226 -(** The impossibility law **)
1.227 -
1.229 +text{*The impossibility law*}
1.230 +lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
1.232 -apply (simp_all add: ensures_def constrains_def transient_def, blast)
1.233 +apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
1.234 +apply (drule bspec, assumption)+
1.235 +apply blast
1.236  done
1.237
1.238 +subsection{*PSP: Progress-Safety-Progress*}
1.239
1.240 -(** PSP: Progress-Safety-Progress **)
1.241 -
1.242 -(*Special case of PSP: Misra's "stable conjunction"*)
1.243 +text{*Special case of PSP: Misra's "stable conjunction"*}
1.244  lemma psp_stable:
1.245     "[| F \<in> A leadsTo A'; F \<in> stable B |]
1.246      ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
1.247 @@ -452,7 +494,7 @@
1.248
1.249  subsection{*wlt*}
1.250
1.251 -(*Misra's property W3*)
1.252 +text{*Misra's property W3*}
1.254  apply (unfold wlt_def)
1.256 @@ -463,17 +505,17 @@
1.258  done
1.259
1.260 -(*Misra's property W2*)
1.261 +text{*Misra's property W2*}
1.262  lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
1.264
1.265 -(*Misra's property W4*)
1.266 +text{*Misra's property W4*}
1.267  lemma wlt_increasing: "B \<subseteq> wlt F B"
1.269  done
1.270
1.271
1.272 -(*Used in the Trans case below*)
1.273 +text{*Used in the Trans case below*}
1.274  lemma lemma1:
1.275     "[| B \<subseteq> A2;
1.276         F \<in> (A1 - B) co (A1 \<union> B);
1.277 @@ -481,18 +523,18 @@
1.278      ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
1.279  by (unfold constrains_def, clarify,  blast)
1.280
1.281 -(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
1.282 +text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
1.284       "F \<in> A leadsTo A'
1.285        ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
1.287 -(*Basis*)
1.288 -apply (blast dest: ensuresD)
1.289 -(*Trans*)
1.290 -apply clarify
1.291 -apply (rule_tac x = "Ba \<union> Bb" in exI)
1.293 -(*Union*)
1.294 +  txt{*Basis*}
1.295 +  apply (blast dest: ensuresD)
1.296 + txt{*Trans*}
1.297 + apply clarify
1.298 + apply (rule_tac x = "Ba \<union> Bb" in exI)
1.300 +txt{*Union*}
1.301  apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
1.302  apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)