--- a/src/ZF/UNITY/Mutex.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/UNITY/Mutex.thy Sun Oct 07 21:19:31 2007 +0200
@@ -1,6 +1,12 @@
(* ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+
+Variables' types are introduced globally so that type verification
+reduces to the usual ZF typechecking \<in> an ill-tyed expression will
+reduce to the empty set.
*)
header{*Mutual Exclusion*}
@@ -28,75 +34,61 @@
u_type: "type_of(u)=bool & default_val(u)=0"
v_type: "type_of(v)=bool & default_val(v)=0"
-constdefs
+definition
(** The program for process U **)
- U0 :: i
- "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
+ "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
- U1 :: i
+definition
"U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}"
- U2 :: i
- "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
+definition
+ "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
- U3 :: i
- "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
+definition
+ "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
- U4 :: i
- "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
+definition
+ "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
(** The program for process V **)
- V0 :: i
- "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
+definition
+ "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
- V1 :: i
- "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
+definition
+ "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
- V2 :: i
- "V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}"
+definition
+ "V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}"
- V3 :: i
+definition
"V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"
- V4 :: i
- "V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}"
+definition
+ "V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}"
- Mutex :: i
- "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
+definition
+ "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))"
(** The correct invariants **)
- IU :: i
- "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
+definition
+ "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
& (s`m = #3 --> s`p=0)}"
- IV :: i
- "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
+definition
+ "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
& (s`n = #3 --> s`p=1)}"
(** The faulty invariant (for U alone) **)
- bad_IU :: i
- "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))&
+definition
+ "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))&
(#3 $<= s`m & s`m $<= #4 --> s`p=0)}"
-(* Title: ZF/UNITY/Mutex.ML
- ID: $Id \<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
-
-Variables' types are introduced globally so that type verification
-reduces to the usual ZF typechecking \<in> an ill-tyed expression will
-reduce to the empty set.
-
-*)
-
(** Variables' types **)
declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
@@ -211,7 +203,7 @@
(*** Progress for U ***)
lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
-by (unfold Unless_def Mutex_def, safety)
+by (unfold op_Unless_def Mutex_def, safety)
lemma U_F1:
"Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
@@ -263,7 +255,7 @@
(*** Progress for V ***)
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
-by (unfold Unless_def Mutex_def, safety)
+by (unfold op_Unless_def Mutex_def, safety)
lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
by (unfold Mutex_def, ensures_tac "V1")