--- a/src/HOL/UNITY/Simple/Mutex.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Mutex.thy Wed Feb 05 13:35:32 2003 +0100
@@ -62,16 +62,16 @@
(** The correct invariants **)
IU :: "state set"
- "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
+ "IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
IV :: "state set"
- "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
+ "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
(** The faulty invariant (for U alone) **)
bad_IU :: "state set"
- "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
- (3 <= m s & m s <= 4 --> ~ p s)}"
+ "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) &
+ (3 \<le> m s & m s \<le> 4 --> ~ p s)}"
declare Mutex_def [THEN def_prg_Init, simp]
@@ -91,26 +91,26 @@
declare IV_def [THEN def_set_simp, simp]
declare bad_IU_def [THEN def_set_simp, simp]
-lemma IU: "Mutex : Always IU"
+lemma IU: "Mutex \<in> Always IU"
apply (rule AlwaysI, force)
apply (unfold Mutex_def, constrains)
done
-lemma IV: "Mutex : Always IV"
+lemma IV: "Mutex \<in> Always IV"
apply (rule AlwaysI, force)
apply (unfold Mutex_def, constrains)
done
(*The safety property: mutual exclusion*)
-lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"
+lemma mutual_exclusion: "Mutex \<in> Always {s. ~ (m s = 3 & n s = 3)}"
apply (rule Always_weaken)
apply (rule Always_Int_I [OF IU IV], auto)
done
(*The bad invariant FAILS in V1*)
-lemma "Mutex : Always bad_IU"
+lemma "Mutex \<in> Always bad_IU"
apply (rule AlwaysI, force)
apply (unfold Mutex_def, constrains, auto)
(*Resulting state: n=1, p=false, m=4, u=false.
@@ -119,90 +119,90 @@
oops
-lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
+lemma eq_123: "((1::int) \<le> i & i \<le> 3) = (i = 1 | i = 2 | i = 3)"
by arith
(*** Progress for U ***)
-lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}"
+lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}"
by (unfold Unless_def Mutex_def, constrains)
-lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
-by (unfold Mutex_def, ensures_tac "U1")
+lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
+by (unfold Mutex_def, ensures_tac U1)
-lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
+lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
apply (cut_tac IU)
apply (unfold Mutex_def, ensures_tac U2)
done
-lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}"
+lemma U_F3: "Mutex \<in> {s. m s = 3} LeadsTo {s. p s}"
apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans)
apply (unfold Mutex_def)
apply (ensures_tac U3)
apply (ensures_tac U4)
done
-lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}"
+lemma U_lemma2: "Mutex \<in> {s. m s = 2} LeadsTo {s. p s}"
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
Int_lower2 [THEN subset_imp_LeadsTo]])
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
done
-lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}"
+lemma U_lemma1: "Mutex \<in> {s. m s = 1} LeadsTo {s. p s}"
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
-lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"
+lemma U_lemma123: "Mutex \<in> {s. 1 \<le> m s & m s \<le> 3} LeadsTo {s. p s}"
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
(*Misra's F4*)
-lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}"
+lemma u_Leadsto_p: "Mutex \<in> {s. u s} LeadsTo {s. p s}"
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
(*** Progress for V ***)
-lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}"
+lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}"
by (unfold Unless_def Mutex_def, constrains)
-lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
+lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
by (unfold Mutex_def, ensures_tac "V1")
-lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"
+lemma V_F2: "Mutex \<in> {s. p s & n s = 2} LeadsTo {s. n s = 3}"
apply (cut_tac IV)
apply (unfold Mutex_def, ensures_tac "V2")
done
-lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"
+lemma V_F3: "Mutex \<in> {s. n s = 3} LeadsTo {s. ~ p s}"
apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans)
apply (unfold Mutex_def)
apply (ensures_tac V3)
apply (ensures_tac V4)
done
-lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"
+lemma V_lemma2: "Mutex \<in> {s. n s = 2} LeadsTo {s. ~ p s}"
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
Int_lower2 [THEN subset_imp_LeadsTo]])
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
done
-lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"
+lemma V_lemma1: "Mutex \<in> {s. n s = 1} LeadsTo {s. ~ p s}"
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
-lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"
+lemma V_lemma123: "Mutex \<in> {s. 1 \<le> n s & n s \<le> 3} LeadsTo {s. ~ p s}"
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
(*Misra's F4*)
-lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}"
+lemma v_Leadsto_not_p: "Mutex \<in> {s. v s} LeadsTo {s. ~ p s}"
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
(** Absence of starvation **)
(*Misra's F6*)
-lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"
+lemma m1_Leadsto_3: "Mutex \<in> {s. m s = 1} LeadsTo {s. m s = 3}"
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
apply (rule_tac [2] U_F2)
apply (simp add: Collect_conj_eq)
@@ -213,7 +213,7 @@
done
(*The same for V*)
-lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"
+lemma n1_Leadsto_3: "Mutex \<in> {s. n s = 1} LeadsTo {s. n s = 3}"
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
apply (rule_tac [2] V_F2)
apply (simp add: Collect_conj_eq)