src/HOL/UNITY/Simple/Mutex.thy
changeset 13785 e2fcd88be55d
parent 11868 56db9f3a6b3e
child 13806 fd40c9d9076b
     1.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Thu Jan 23 10:30:14 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Fri Jan 24 14:06:49 2003 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
     1.5  *)
     1.6  
     1.7 -Mutex = SubstAx +
     1.8 +theory Mutex = UNITY_Main:
     1.9  
    1.10  record state =
    1.11    p :: bool
    1.12 @@ -53,7 +53,7 @@
    1.13    V4 :: command
    1.14      "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
    1.15  
    1.16 -  Mutex :: state program
    1.17 +  Mutex :: "state program"
    1.18      "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
    1.19  		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    1.20  			  UNIV)"
    1.21 @@ -61,16 +61,166 @@
    1.22  
    1.23    (** The correct invariants **)
    1.24  
    1.25 -  IU :: state set
    1.26 +  IU :: "state set"
    1.27      "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
    1.28  
    1.29 -  IV :: state set
    1.30 +  IV :: "state set"
    1.31      "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
    1.32  
    1.33    (** The faulty invariant (for U alone) **)
    1.34  
    1.35 -  bad_IU :: state set
    1.36 +  bad_IU :: "state set"
    1.37      "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
    1.38  	           (3 <= m s & m s <= 4 --> ~ p s)}"
    1.39  
    1.40 +
    1.41 +declare Mutex_def [THEN def_prg_Init, simp]
    1.42 +
    1.43 +declare U0_def [THEN def_act_simp, simp]
    1.44 +declare U1_def [THEN def_act_simp, simp]
    1.45 +declare U2_def [THEN def_act_simp, simp]
    1.46 +declare U3_def [THEN def_act_simp, simp]
    1.47 +declare U4_def [THEN def_act_simp, simp]
    1.48 +declare V0_def [THEN def_act_simp, simp]
    1.49 +declare V1_def [THEN def_act_simp, simp]
    1.50 +declare V2_def [THEN def_act_simp, simp]
    1.51 +declare V3_def [THEN def_act_simp, simp]
    1.52 +declare V4_def [THEN def_act_simp, simp]
    1.53 +
    1.54 +declare IU_def [THEN def_set_simp, simp]
    1.55 +declare IV_def [THEN def_set_simp, simp]
    1.56 +declare bad_IU_def [THEN def_set_simp, simp]
    1.57 +
    1.58 +lemma IU: "Mutex : Always IU"
    1.59 +apply (rule AlwaysI, force) 
    1.60 +apply (unfold Mutex_def, constrains) 
    1.61 +done
    1.62 +
    1.63 +
    1.64 +lemma IV: "Mutex : Always IV"
    1.65 +apply (rule AlwaysI, force) 
    1.66 +apply (unfold Mutex_def, constrains)
    1.67 +done
    1.68 +
    1.69 +(*The safety property: mutual exclusion*)
    1.70 +lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"
    1.71 +apply (rule Always_weaken) 
    1.72 +apply (rule Always_Int_I [OF IU IV], auto)
    1.73 +done
    1.74 +
    1.75 +
    1.76 +(*The bad invariant FAILS in V1*)
    1.77 +lemma "Mutex : Always bad_IU"
    1.78 +apply (rule AlwaysI, force) 
    1.79 +apply (unfold Mutex_def, constrains, auto)
    1.80 +(*Resulting state: n=1, p=false, m=4, u=false.  
    1.81 +  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
    1.82 +  violating the invariant!*)
    1.83 +oops
    1.84 +
    1.85 +
    1.86 +lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
    1.87 +by arith
    1.88 +
    1.89 +
    1.90 +(*** Progress for U ***)
    1.91 +
    1.92 +lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}"
    1.93 +by (unfold Unless_def Mutex_def, constrains)
    1.94 +
    1.95 +lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
    1.96 +by (unfold Mutex_def, ensures_tac "U1")
    1.97 +
    1.98 +lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
    1.99 +apply (cut_tac IU)
   1.100 +apply (unfold Mutex_def, ensures_tac U2)
   1.101 +done
   1.102 +
   1.103 +lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}"
   1.104 +apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans)
   1.105 + apply (unfold Mutex_def)
   1.106 + apply (ensures_tac U3)
   1.107 +apply (ensures_tac U4)
   1.108 +done
   1.109 +
   1.110 +lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}"
   1.111 +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
   1.112 +                             Int_lower2 [THEN subset_imp_LeadsTo]])
   1.113 +apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
   1.114 +done
   1.115 +
   1.116 +lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}"
   1.117 +by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
   1.118 +
   1.119 +lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"
   1.120 +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
   1.121 +
   1.122 +(*Misra's F4*)
   1.123 +lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}"
   1.124 +by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
   1.125 +
   1.126 +
   1.127 +(*** Progress for V ***)
   1.128 +
   1.129 +
   1.130 +lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}"
   1.131 +by (unfold Unless_def Mutex_def, constrains)
   1.132 +
   1.133 +lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
   1.134 +by (unfold Mutex_def, ensures_tac "V1")
   1.135 +
   1.136 +lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"
   1.137 +apply (cut_tac IV)
   1.138 +apply (unfold Mutex_def, ensures_tac "V2")
   1.139 +done
   1.140 +
   1.141 +lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"
   1.142 +apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans)
   1.143 + apply (unfold Mutex_def)
   1.144 + apply (ensures_tac V3)
   1.145 +apply (ensures_tac V4)
   1.146 +done
   1.147 +
   1.148 +lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"
   1.149 +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
   1.150 +                             Int_lower2 [THEN subset_imp_LeadsTo]])
   1.151 +apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) 
   1.152 +done
   1.153 +
   1.154 +lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"
   1.155 +by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
   1.156 +
   1.157 +lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"
   1.158 +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
   1.159 +
   1.160 +
   1.161 +(*Misra's F4*)
   1.162 +lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}"
   1.163 +by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
   1.164 +
   1.165 +
   1.166 +(** Absence of starvation **)
   1.167 +
   1.168 +(*Misra's F6*)
   1.169 +lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"
   1.170 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
   1.171 +apply (rule_tac [2] U_F2)
   1.172 +apply (simp add: Collect_conj_eq)
   1.173 +apply (subst Un_commute)
   1.174 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
   1.175 + apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
   1.176 +apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
   1.177 +done
   1.178 +
   1.179 +(*The same for V*)
   1.180 +lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"
   1.181 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
   1.182 +apply (rule_tac [2] V_F2)
   1.183 +apply (simp add: Collect_conj_eq)
   1.184 +apply (subst Un_commute)
   1.185 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
   1.186 + apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0])
   1.187 +apply (rule V_F1 [THEN LeadsTo_weaken_R], auto)
   1.188 +done
   1.189 +
   1.190  end