--- a/src/ZF/UNITY/Mutex.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/Mutex.thy Mon Mar 28 16:19:56 2005 +0200
@@ -1,17 +1,26 @@
-(* Title: ZF/UNITY/Mutex.thy
- ID: $Id$
+(* 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: an ill-tyed expressions reduce to the empty set.
*)
-Mutex = SubstAx +
+header{*Mutual Exclusion*}
+
+theory Mutex
+imports SubstAx
+begin
+
+text{*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: an ill-tyed expressions reduce to the empty set.
+*}
+
consts
- p, m, n, u, v :: i
+ p :: i
+ m :: i
+ n :: i
+ u :: i
+ v :: i
translations
"p" == "Var([0])"
@@ -20,12 +29,12 @@
"u" == "Var([0,1])"
"v" == "Var([1,0])"
-rules (** Type declarations **)
- p_type "type_of(p)=bool & default_val(p)=0"
- m_type "type_of(m)=int & default_val(m)=#0"
- n_type "type_of(n)=int & default_val(n)=#0"
- u_type "type_of(u)=bool & default_val(u)=0"
- v_type "type_of(v)=bool & default_val(v)=0"
+axioms --{** Type declarations **}
+ p_type: "type_of(p)=bool & default_val(p)=0"
+ m_type: "type_of(m)=int & default_val(m)=#0"
+ n_type: "type_of(n)=int & default_val(n)=#0"
+ u_type: "type_of(u)=bool & default_val(u)=0"
+ v_type: "type_of(v)=bool & default_val(v)=0"
constdefs
(** The program for process U **)
@@ -82,4 +91,256 @@
"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]
+
+lemma u_value_type: "s \<in> state ==>s`u \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = u in apply_type, auto)
+done
+
+lemma v_value_type: "s \<in> state ==> s`v \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = v in apply_type, auto)
+done
+
+lemma p_value_type: "s \<in> state ==> s`p \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = p in apply_type, auto)
+done
+
+lemma m_value_type: "s \<in> state ==> s`m \<in> int"
+apply (unfold state_def)
+apply (drule_tac a = m in apply_type, auto)
+done
+
+lemma n_value_type: "s \<in> state ==>s`n \<in> int"
+apply (unfold state_def)
+apply (drule_tac a = n in apply_type, auto)
+done
+
+declare p_value_type [simp] u_value_type [simp] v_value_type [simp]
+ m_value_type [simp] n_value_type [simp]
+
+declare p_value_type [TC] u_value_type [TC] v_value_type [TC]
+ m_value_type [TC] n_value_type [TC]
+
+
+
+text{*Mutex is a program*}
+
+lemma Mutex_in_program [simp,TC]: "Mutex \<in> program"
+by (simp add: Mutex_def)
+
+
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
+ "for proving safety properties"
+
+
+declare Mutex_def [THEN def_prg_Init, simp]
+ML
+{*
+program_defs_ref := [thm"Mutex_def"]
+*}
+
+declare U0_def [THEN def_act_simp, simp]
+declare U1_def [THEN def_act_simp, simp]
+declare U2_def [THEN def_act_simp, simp]
+declare U3_def [THEN def_act_simp, simp]
+declare U4_def [THEN def_act_simp, simp]
+
+declare V0_def [THEN def_act_simp, simp]
+declare V1_def [THEN def_act_simp, simp]
+declare V2_def [THEN def_act_simp, simp]
+declare V3_def [THEN def_act_simp, simp]
+declare V4_def [THEN def_act_simp, simp]
+
+declare U0_def [THEN def_set_simp, simp]
+declare U1_def [THEN def_set_simp, simp]
+declare U2_def [THEN def_set_simp, simp]
+declare U3_def [THEN def_set_simp, simp]
+declare U4_def [THEN def_set_simp, simp]
+
+declare V0_def [THEN def_set_simp, simp]
+declare V1_def [THEN def_set_simp, simp]
+declare V2_def [THEN def_set_simp, simp]
+declare V3_def [THEN def_set_simp, simp]
+declare V4_def [THEN def_set_simp, simp]
+
+declare IU_def [THEN def_set_simp, simp]
+declare IV_def [THEN def_set_simp, simp]
+declare bad_IU_def [THEN def_set_simp, simp]
+
+lemma IU: "Mutex \<in> Always(IU)"
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, constrains, auto)
+done
+
+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 \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
+apply (rule Always_weaken)
+apply (rule Always_Int_I [OF IU IV], auto)
+done
+
+(*The bad invariant FAILS in V1*)
+
+lemma less_lemma: "[| x$<#1; #3 $<= x |] ==> P"
+apply (drule_tac j = "#1" and k = "#3" in zless_zle_trans)
+apply (drule_tac [2] j = x in zle_zless_trans, auto)
+done
+
+lemma "Mutex \<in> Always(bad_IU)"
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, constrains, auto)
+apply (subgoal_tac "#1 $<= #3")
+apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
+apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
+apply auto
+(*Resulting state: n=1, p=false, m=4, u=false.
+ Execution of V1 (the command of process v guarded by n=1) sets p:=true,
+ violating the invariant!*)
+oops
+
+
+
+(*** 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, constrains)
+
+lemma U_F1:
+ "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
+by (unfold Mutex_def, ensures_tac U1)
+
+lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
+apply (cut_tac IU)
+apply (unfold Mutex_def, ensures_tac U2)
+done
+
+lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
+apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
+ apply (unfold Mutex_def)
+ apply (ensures_tac U3)
+apply (ensures_tac U4)
+done
+
+
+lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}"
+apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
+ Int_lower2 [THEN subset_imp_LeadsTo]])
+apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
+apply (auto dest!: p_value_type simp add: bool_def)
+done
+
+lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}"
+by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
+
+lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"
+apply auto
+apply (auto simp add: neq_iff_zless)
+apply (drule_tac [4] j = "#3" and i = i in zle_zless_trans)
+apply (drule_tac [2] j = i and i = "#1" in zle_zless_trans)
+apply (drule_tac j = i and i = "#1" in zle_zless_trans, auto)
+apply (rule zle_anti_sym)
+apply (simp_all (no_asm_simp) add: zless_add1_iff_zle [THEN iff_sym])
+done
+
+
+lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}"
+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 \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}"
+by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
+
+
+(*** 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, constrains)
+
+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")
+
+lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
+apply (cut_tac IV)
+apply (unfold Mutex_def, ensures_tac "V2")
+done
+
+lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
+apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
+ apply (unfold Mutex_def)
+ apply (ensures_tac V3)
+apply (ensures_tac V4)
+done
+
+lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
+apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
+ Int_lower2 [THEN subset_imp_LeadsTo]])
+apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
+apply (auto dest!: p_value_type simp add: bool_def)
+done
+
+lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}"
+by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
+
+lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}"
+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 \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}"
+by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
+
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}"
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+apply (rule_tac [2] U_F2)
+apply (simp add: Collect_conj_eq)
+apply (subst Un_commute)
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+ apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
+apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
+apply (auto dest!: v_value_type simp add: bool_def)
+done
+
+
+(*The same for V*)
+lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}"
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+apply (rule_tac [2] V_F2)
+apply (simp add: Collect_conj_eq)
+apply (subst Un_commute)
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+ apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0])
+apply (rule V_F1 [THEN LeadsTo_weaken_R], auto)
+apply (auto dest!: u_value_type simp add: bool_def)
+done
+
end
\ No newline at end of file