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.13 -header{*Progress under Weak Fairness*}
    1.14 +header{*Progress*}
    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.21 +eventually executed.  Ernie Cohen suggested that I instead adopt unconditional
    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.62  inductive "leads F"
    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.70      "A leadsTo B == {F. (A,B) \<in> leads F}"
    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.93 +apply (simp add: all_total_def)
    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.149  by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
   1.150  
   1.151 -(*Useful with cancellation, disjunction*)
   1.152 +text{*Useful with cancellation, disjunction*}
   1.153  lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
   1.154  by (simp add: Un_ac)
   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.158  by (simp add: Un_ac)
   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.162  lemma leadsTo_Union: 
   1.163      "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
   1.164  apply (unfold leadsTo_def)
   1.165 @@ -162,7 +205,7 @@
   1.166  apply (blast intro: leadsTo_Union)
   1.167  done
   1.168  
   1.169 -(*Binary union introduction rule*)
   1.170 +text{*Binary union introduction rule*}
   1.171  lemma leadsTo_Un:
   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.180  lemma leadsTo_induct: 
   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.189  lemma leadsTo_induct_pre_lemma: 
   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.200  apply (blast intro: leadsTo_refl)
   1.201  apply (erule leadsTo_induct)
   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.205  by (blast intro: leadsTo_Trans subset_imp_leadsTo)
   1.206  
   1.207 -(*Distributes over binary unions*)
   1.208 +text{*Distributes over binary unions*}
   1.209  lemma leadsTo_Un_distrib:
   1.210       "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
   1.211  by (blast intro: leadsTo_Un leadsTo_weaken_L)
   1.212 @@ -271,7 +314,7 @@
   1.213  apply (blast intro: leadsTo_Union leadsTo_weaken_R)
   1.214  done
   1.215  
   1.216 -(*Binary union version*)
   1.217 +text{*Binary union version*}
   1.218  lemma leadsTo_Un_Un:
   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.228 -lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}"
   1.229 +text{*The impossibility law*}
   1.230 +lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
   1.231  apply (erule leadsTo_induct_pre)
   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.253  lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
   1.254  apply (unfold wlt_def)
   1.255  apply (blast intro!: leadsTo_Union)
   1.256 @@ -463,17 +505,17 @@
   1.257  apply (blast intro!: leadsTo_Union)
   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.263  by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
   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.268  apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
   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.283  lemma leadsTo_123:
   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.286  apply (erule leadsTo_induct)
   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.292 -apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
   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.299 + apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
   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)
   1.303  apply (auto intro: leadsTo_UN)
   1.304 @@ -502,7 +544,7 @@
   1.305  done
   1.306  
   1.307  
   1.308 -(*Misra's property W5*)
   1.309 +text{*Misra's property W5*}
   1.310  lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
   1.311  proof -
   1.312    from wlt_leadsTo [of F B, THEN leadsTo_123]