src/HOL/UNITY/Mutex.ML
author paulson
Mon, 20 Sep 1999 10:46:16 +0200
changeset 7543 abefbd41bd3e
parent 7403 c318acb88251
child 8355 04d0f732e24e
permissions -rw-r--r--
renamed Always_Int to Always_Int_I
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
     1
(*  Title:      HOL/UNITY/Mutex
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
     9
Addsimps [Mutex_def RS def_prg_Init];
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    10
program_defs_ref := [Mutex_def];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    12
Addsimps (map simp_of_act
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    13
	  [U0_def, U1_def, U2_def, U3_def, U4_def, 
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    14
	   V0_def, V1_def, V2_def, V3_def, V4_def]);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    16
Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    18
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    19
Goal "Mutex : Always IU";
7403
c318acb88251 tidied some proofs
paulson
parents: 7221
diff changeset
    20
by (always_tac 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    21
qed "IU";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    23
Goal "Mutex : Always IV";
7403
c318acb88251 tidied some proofs
paulson
parents: 7221
diff changeset
    24
by (always_tac 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    25
qed "IV";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    26
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    27
(*The safety property: mutual exclusion*)
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    28
Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    29
by (rtac Always_weaken 1);
7543
abefbd41bd3e renamed Always_Int to Always_Int_I
paulson
parents: 7403
diff changeset
    30
by (rtac ([IU, IV] MRS Always_Int_I) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
qed "mutual_exclusion";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    33
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    35
(*The bad invariant FAILS in V1*)
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    36
Goal "Mutex : Always bad_IU";
7403
c318acb88251 tidied some proofs
paulson
parents: 7221
diff changeset
    37
by (always_tac 1);
6615
paulson
parents: 6570
diff changeset
    38
by Auto_tac;
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    39
(*Resulting state: n=1, p=false, m=4, u=false.  
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    40
  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    41
  violating the invariant!*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    42
(*Check that subgoals remain: proof failed.*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
getgoal 1;  
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
6909
21601bc4f3c2 adapted to generic numerals;
wenzelm
parents: 6678
diff changeset
    46
Goal "((#1::int) <= i & i <= #3) = (i = #1 | i = #2 | i = #3)";
6615
paulson
parents: 6570
diff changeset
    47
by (arith_tac 1);
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5426
diff changeset
    48
qed "eq_123";
b29d18d8c4d2 abstype of programs
paulson
parents: 5426
diff changeset
    49
b29d18d8c4d2 abstype of programs
paulson
parents: 5426
diff changeset
    50
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
(*** Progress for U ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    53
Goalw [Unless_def] "Mutex : {s. m s=#2} Unless {s. m s=#3}";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    54
by (constrains_tac 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    55
qed "U_F0";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    56
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    57
Goal "Mutex : {s. m s=#1} LeadsTo {s. p s = v s & m s = #2}";
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    58
by (ensures_tac "U1" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
qed "U_F1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    60
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    61
Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}";
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    62
by (cut_facts_tac [IU] 1);
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    63
by (ensures_tac "U2" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    64
qed "U_F2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    65
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    66
Goal "Mutex : {s. m s = #3} LeadsTo {s. p s}";
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    67
by (res_inst_tac [("B", "{s. m s = #4}")] LeadsTo_Trans 1);
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    68
by (ensures_tac "U4" 2);
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    69
by (ensures_tac "U3" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    70
qed "U_F3";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    71
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    72
Goal "Mutex : {s. m s = #2} LeadsTo {s. p s}";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
    73
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    74
	  MRS LeadsTo_Diff) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    75
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    76
by (auto_tac (claset() addSEs [less_SucE], simpset()));
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    77
val U_lemma2 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    78
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    79
Goal "Mutex : {s. m s = #1} LeadsTo {s. p s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    80
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    81
by (Blast_tac 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    82
val U_lemma1 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    83
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    84
Goal "Mutex : {s. #1 <= m s & m s <= #3} LeadsTo {s. p s}";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5426
diff changeset
    85
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    86
				  U_lemma1, U_lemma2, U_F3] ) 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    87
val U_lemma123 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    88
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    89
(*Misra's F4*)
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    90
Goal "Mutex : {s. u s} LeadsTo {s. p s}";
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
    91
by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    92
by Auto_tac;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    93
qed "u_Leadsto_p";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    94
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    95
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    96
(*** Progress for V ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    97
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    98
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
    99
Goalw [Unless_def] "Mutex : {s. n s=#2} Unless {s. n s=#3}";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   100
by (constrains_tac 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   101
qed "V_F0";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   102
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   103
Goal "Mutex : {s. n s=#1} LeadsTo {s. p s = (~ u s) & n s = #2}";
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   104
by (ensures_tac "V1" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   105
qed "V_F1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   106
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   107
Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}";
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
   108
by (cut_facts_tac [IV] 1);
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   109
by (ensures_tac "V2" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   110
qed "V_F2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   111
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   112
Goal "Mutex : {s. n s = #3} LeadsTo {s. ~ p s}";
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   113
by (res_inst_tac [("B", "{s. n s = #4}")] LeadsTo_Trans 1);
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   114
by (ensures_tac "V4" 2);
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   115
by (ensures_tac "V3" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   116
qed "V_F3";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   117
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   118
Goal "Mutex : {s. n s = #2} LeadsTo {s. ~ p s}";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   119
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   120
	  MRS LeadsTo_Diff) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   121
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   122
by (auto_tac (claset() addSEs [less_SucE], simpset()));
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   123
val V_lemma2 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   124
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   125
Goal "Mutex : {s. n s = #1} LeadsTo {s. ~ p s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   126
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   127
by (Blast_tac 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   128
val V_lemma1 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   129
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   130
Goal "Mutex : {s. #1 <= n s & n s <= #3} LeadsTo {s. ~ p s}";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5426
diff changeset
   131
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   132
				  V_lemma1, V_lemma2, V_F3] ) 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   133
val V_lemma123 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   134
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   135
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   136
(*Misra's F4*)
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   137
Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6565
diff changeset
   138
by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   139
by Auto_tac;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   140
qed "v_Leadsto_not_p";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   141
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   142
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   143
(** Absence of starvation **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   144
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   145
(*Misra's F6*)
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   146
Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}";
6615
paulson
parents: 6570
diff changeset
   147
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   148
by (rtac U_F2 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   149
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   150
by (stac Un_commute 1);
6615
paulson
parents: 6570
diff changeset
   151
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
paulson
parents: 6570
diff changeset
   152
by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   153
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
6615
paulson
parents: 6570
diff changeset
   154
by Auto_tac;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   155
qed "m1_Leadsto_3";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   156
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   157
(*The same for V*)
6565
de4acf4449fa renamed state variables
paulson
parents: 6536
diff changeset
   158
Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}";
6615
paulson
parents: 6570
diff changeset
   159
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   160
by (rtac V_F2 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   161
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   162
by (stac Un_commute 1);
6615
paulson
parents: 6570
diff changeset
   163
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
paulson
parents: 6570
diff changeset
   164
by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   165
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
6615
paulson
parents: 6570
diff changeset
   166
by Auto_tac;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   167
qed "n1_Leadsto_3";