# HG changeset patch
# User paulson
# Date 925723124 -7200
# Node ID de4acf4449fa6d23e9be9fca256767cd1c4c0855
# Parent  c09997086ca7e7e410dbbedc66d698aa90357fe0
renamed state variables

diff -r c09997086ca7 -r de4acf4449fa src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Mon May 03 11:18:11 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Mon May 03 11:18:44 1999 +0200
@@ -9,12 +9,12 @@
 (*split_all_tac causes a big blow-up*)
 claset_ref() := claset() delSWrapper record_split_name;
 
-Addsimps [Mprg_def RS def_prg_Init];
-program_defs_ref := [Mprg_def];
+Addsimps [Mutex_def RS def_prg_Init];
+program_defs_ref := [Mutex_def];
 
 Addsimps (map simp_of_act
-	  [cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
-	   cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def]);
+	  [U0_def, U1_def, U2_def, U3_def, U4_def, 
+	   V0_def, V1_def, V2_def, V3_def, V4_def]);
 
 Addsimps (map simp_of_set
 	  [invariantU_def, invariantV_def, bad_invariantU_def]);
@@ -22,13 +22,13 @@
 (*Simplification for records*)
 Addsimps (thms"state.update_defs");
 
-Goal "Mprg : Invariant invariantU";
+Goal "Mutex : Invariant invariantU";
 by (rtac InvariantI 1);
 by (constrains_tac 2);
 by Auto_tac;
 qed "invariantU";
 
-Goal "Mprg : Invariant invariantV";
+Goal "Mutex : Invariant invariantV";
 by (rtac InvariantI 1);
 by (constrains_tac 2);
 by Auto_tac;
@@ -38,14 +38,14 @@
 
 
 (*The safety property: mutual exclusion*)
-Goal "(reachable Mprg) Int {s. MM s = #3 & NN s = #3} = {}";
+Goal "(reachable Mutex) Int {s. m s = #3 & n s = #3} = {}";
 by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
 by Auto_tac;
 qed "mutual_exclusion";
 
 
-(*The bad invariant FAILS in cmd1V*)
-Goal "Mprg : Invariant bad_invariantU";
+(*The bad invariant FAILS in V1*)
+Goal "Mutex : Invariant bad_invariantU";
 by (rtac InvariantI 1);
 by (constrains_tac 2);
 by (Force_tac 1);
@@ -58,13 +58,13 @@
 by (full_simp_tac (simpset_of Int.thy) 1);
 by (asm_full_simp_tac (simpset() addsimps int_simps) 1);
 (*Resulting state: n=1, p=false, m=4, u=false.  
-  Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
+  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
   violating the invariant!*)
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
 
 
-Goal "(#1 <= m & m <= #3) = (m = #1 | m = #2 | m = #3)";
+Goal "(#1 <= i & i <= #3) = (i = #1 | i = #2 | i = #3)";
 by (auto_tac (claset(),
 	      simpset_of Int.thy addsimps
 	        [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, 
@@ -74,44 +74,44 @@
 
 (*** Progress for U ***)
 
-Goalw [Unless_def] "Mprg : {s. MM s=#2} Unless {s. MM s=#3}";
+Goalw [Unless_def] "Mutex : {s. m s=#2} Unless {s. m s=#3}";
 by (constrains_tac 1);
 qed "U_F0";
 
-Goal "Mprg : {s. MM s=#1} LeadsTo {s. PP s = VV s & MM s = #2}";
-by (ensures_tac "cmd1U" 1);
+Goal "Mutex : {s. m s=#1} LeadsTo {s. p s = v s & m s = #2}";
+by (ensures_tac "U1" 1);
 qed "U_F1";
 
-Goal "Mprg : {s. ~ PP s & MM s = #2} LeadsTo {s. MM s = #3}";
+Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}";
 by (cut_facts_tac [invariantU] 1);
-by (ensures_tac "cmd2U" 1);
+by (ensures_tac "U2" 1);
 qed "U_F2";
 
-Goal "Mprg : {s. MM s = #3} LeadsTo {s. PP s}";
-by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1);
-by (ensures_tac "cmd4U" 2);
-by (ensures_tac "cmd3U" 1);
+Goal "Mutex : {s. m s = #3} LeadsTo {s. p s}";
+by (res_inst_tac [("B", "{s. m s = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "U4" 2);
+by (ensures_tac "U3" 1);
 qed "U_F3";
 
-Goal "Mprg : {s. MM s = #2} LeadsTo {s. PP s}";
+Goal "Mutex : {s. m s = #2} LeadsTo {s. p s}";
 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val U_lemma2 = result();
 
-Goal "Mprg : {s. MM s = #1} LeadsTo {s. PP s}";
+Goal "Mutex : {s. m s = #1} LeadsTo {s. p s}";
 by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val U_lemma1 = result();
 
-Goal "Mprg : {s. #1 <= MM s & MM s <= #3} LeadsTo {s. PP s}";
+Goal "Mutex : {s. #1 <= m s & m s <= #3} LeadsTo {s. p s}";
 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
 				  U_lemma1, U_lemma2, U_F3] ) 1);
 val U_lemma123 = result();
 
 (*Misra's F4*)
-Goal "Mprg : {s. UU s} LeadsTo {s. PP s}";
+Goal "Mutex : {s. u s} LeadsTo {s. p s}";
 by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
 by Auto_tac;
 qed "u_Leadsto_p";
@@ -120,45 +120,45 @@
 (*** Progress for V ***)
 
 
-Goalw [Unless_def] "Mprg : {s. NN s=#2} Unless {s. NN s=#3}";
+Goalw [Unless_def] "Mutex : {s. n s=#2} Unless {s. n s=#3}";
 by (constrains_tac 1);
 qed "V_F0";
 
-Goal "Mprg : {s. NN s=#1} LeadsTo {s. PP s = (~ UU s) & NN s = #2}";
-by (ensures_tac "cmd1V" 1);
+Goal "Mutex : {s. n s=#1} LeadsTo {s. p s = (~ u s) & n s = #2}";
+by (ensures_tac "V1" 1);
 qed "V_F1";
 
-Goal "Mprg : {s. PP s & NN s = #2} LeadsTo {s. NN s = #3}";
+Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}";
 by (cut_facts_tac [invariantV] 1);
-by (ensures_tac "cmd2V" 1);
+by (ensures_tac "V2" 1);
 qed "V_F2";
 
-Goal "Mprg : {s. NN s = #3} LeadsTo {s. ~ PP s}";
-by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1);
-by (ensures_tac "cmd4V" 2);
-by (ensures_tac "cmd3V" 1);
+Goal "Mutex : {s. n s = #3} LeadsTo {s. ~ p s}";
+by (res_inst_tac [("B", "{s. n s = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "V4" 2);
+by (ensures_tac "V3" 1);
 qed "V_F3";
 
-Goal "Mprg : {s. NN s = #2} LeadsTo {s. ~ PP s}";
+Goal "Mutex : {s. n s = #2} LeadsTo {s. ~ p s}";
 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val V_lemma2 = result();
 
-Goal "Mprg : {s. NN s = #1} LeadsTo {s. ~ PP s}";
+Goal "Mutex : {s. n s = #1} LeadsTo {s. ~ p s}";
 by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val V_lemma1 = result();
 
-Goal "Mprg : {s. #1 <= NN s & NN s <= #3} LeadsTo {s. ~ PP s}";
+Goal "Mutex : {s. #1 <= n s & n s <= #3} LeadsTo {s. ~ p s}";
 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
 				  V_lemma1, V_lemma2, V_F3] ) 1);
 val V_lemma123 = result();
 
 
 (*Misra's F4*)
-Goal "Mprg : {s. VV s} LeadsTo {s. ~ PP s}";
+Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
 by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
 by Auto_tac;
 qed "v_Leadsto_not_p";
@@ -167,7 +167,7 @@
 (** Absence of starvation **)
 
 (*Misra's F6*)
-Goal "Mprg : {s. MM s = #1} LeadsTo {s. MM s = #3}";
+Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac U_F2 2);
@@ -181,7 +181,7 @@
 
 
 (*The same for V*)
-Goal "Mprg : {s. NN s = #1} LeadsTo {s. NN s = #3}";
+Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac V_F2 2);
diff -r c09997086ca7 -r de4acf4449fa src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Mon May 03 11:18:11 1999 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Mon May 03 11:18:44 1999 +0200
@@ -9,68 +9,69 @@
 Mutex = SubstAx +
 
 record state =
-  PP :: bool
-  MM :: int
-  NN :: int
-  UU :: bool
-  VV :: bool
+  p :: bool
+  m :: int
+  n :: int
+  u :: bool
+  v :: bool
+
+types command = "(state*state) set"
 
 constdefs
   
   (** The program for process U **)
   
-  cmd0U :: "(state*state) set"
-    "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}"
+  U0 :: command
+    "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
 
-  cmd1U :: "(state*state) set"
-    "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}"
+  U1 :: command
+    "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
 
-  cmd2U :: "(state*state) set"
-    "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}"
+  U2 :: command
+    "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
 
-  cmd3U :: "(state*state) set"
-    "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}"
+  U3 :: command
+    "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
 
-  cmd4U :: "(state*state) set"
-    "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}"
+  U4 :: command
+    "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
 
   (** The program for process V **)
   
-  cmd0V :: "(state*state) set"
-    "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}"
+  V0 :: command
+    "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
 
-  cmd1V :: "(state*state) set"
-    "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}"
+  V1 :: command
+    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
 
-  cmd2V :: "(state*state) set"
-    "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}"
+  V2 :: command
+    "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
 
-  cmd3V :: "(state*state) set"
-    "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}"
+  V3 :: command
+    "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
 
-  cmd4V :: "(state*state) set"
-    "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}"
+  V4 :: command
+    "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
 
-  Mprg :: state program
-    "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
-			 {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
-			  cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})"
+  Mutex :: state program
+    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
+		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4})"
 
 
   (** The correct invariants **)
 
-  invariantU :: "state set"
-    "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
-		       (MM s = #3 --> ~ PP s)}"
+  invariantU :: state set
+    "invariantU == {s. (u s = (#1 <= m s & m s <= #3)) &
+		       (m s = #3 --> ~ p s)}"
 
-  invariantV :: "state set"
-    "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) &
-		       (NN s = #3 --> PP s)}"
+  invariantV :: state set
+    "invariantV == {s. (v s = (#1 <= n s & n s <= #3)) &
+		       (n s = #3 --> p s)}"
 
   (** The faulty invariant (for U alone) **)
 
-  bad_invariantU :: "state set"
-    "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
-		           (#3 <= MM s & MM s <= #4 --> ~ PP s)}"
+  bad_invariantU :: state set
+    "bad_invariantU == {s. (u s = (#1 <= m s & m s <= #3)) &
+		           (#3 <= m s & m s <= #4 --> ~ p s)}"
 
 end