src/HOL/UNITY/Mutex.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5320 79b326bceafb
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     1 (*  Title:      HOL/UNITY/Mutex
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
     7 *)
     8 
     9 (*split_all_tac causes a big blow-up*)
    10 claset_ref() := claset() delSWrapper "split_all_tac";
    11 
    12 val cmd_defs = [Mprg_def, 
    13 		cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
    14 		cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
    15 
    16 Goalw [Mprg_def] "id : Acts Mprg";
    17 by (Simp_tac 1);
    18 qed "id_in_Acts";
    19 AddIffs [id_in_Acts];
    20 
    21 
    22 (*Simplification for records*)
    23 val select_defs = thms"state.select_defs"
    24 and update_defs = thms"state.update_defs"
    25 and dest_defs   = thms"state.dest_defs";
    26 
    27 Addsimps update_defs;
    28 
    29 Addsimps [invariantU_def, invariantV_def];
    30 
    31 
    32 Goalw [Mprg_def] "Invariant Mprg invariantU";
    33 by (rtac InvariantI 1);
    34 by (constrains_tac cmd_defs 2);
    35 by Auto_tac;
    36 qed "invariantU";
    37 
    38 Goalw [Mprg_def] "Invariant Mprg invariantV";
    39 by (rtac InvariantI 1);
    40 by (constrains_tac cmd_defs 2);
    41 by Auto_tac;
    42 qed "invariantV";
    43 
    44 val invariantUV = Invariant_Int_rule [invariantU, invariantV];
    45 
    46 
    47 (*The safety property: mutual exclusion*)
    48 Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
    49 by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
    50 by Auto_tac;
    51 qed "mutual_exclusion";
    52 
    53 
    54 (*The bad invariant FAILS in cmd1V*)
    55 Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
    56 by (rtac InvariantI 1);
    57 by (Force_tac 1);
    58 by (constrains_tac cmd_defs 1);
    59 by (REPEAT (trans_tac 1));
    60 by (safe_tac (claset() addSEs [le_SucE]));
    61 by (Asm_full_simp_tac 1);
    62 (*Resulting state: n=1, p=false, m=4, u=false.  
    63   Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
    64   violating the invariant!*)
    65 (*Check that subgoals remain: proof failed.*)
    66 getgoal 1;  
    67 
    68 
    69 (*** Progress for U ***)
    70 
    71 Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
    72 by (constrains_tac cmd_defs 1);
    73 qed "U_F0";
    74 
    75 Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
    76 by (ensures_tac cmd_defs "cmd1U" 1);
    77 qed "U_F1";
    78 
    79 Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    80 by (cut_facts_tac [invariantUV] 1);
    81 by (rewtac Mprg_def);
    82 by (ensures_tac cmd_defs "cmd2U" 1);
    83 qed "U_F2";
    84 
    85 Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
    86 by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
    87 by (ensures_tac cmd_defs "cmd4U" 2);
    88 by (ensures_tac cmd_defs "cmd3U" 1);
    89 qed "U_F3";
    90 
    91 Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
    92 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
    93 	  MRS LeadsTo_Diff) 1);
    94 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
    95 by (auto_tac (claset() addSEs [less_SucE], simpset()));
    96 val U_lemma2 = result();
    97 
    98 Goal "LeadsTo Mprg {s. MM s = 1} {s. PP s}";
    99 by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
   100 by (Blast_tac 1);
   101 val U_lemma1 = result();
   102 
   103 Goal "LeadsTo Mprg {s. 1 <= MM s & MM s <= 3} {s. PP s}";
   104 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   105 	                addcongs [rev_conj_cong]) 1);
   106 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   107 				  U_lemma1, U_lemma2, U_F3] ) 1);
   108 val U_lemma123 = result();
   109 
   110 (*Misra's F4*)
   111 Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
   112 by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   113 by Auto_tac;
   114 qed "u_Leadsto_p";
   115 
   116 
   117 (*** Progress for V ***)
   118 
   119 
   120 Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
   121 by (constrains_tac cmd_defs 1);
   122 qed "V_F0";
   123 
   124 Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
   125 by (ensures_tac cmd_defs "cmd1V" 1);
   126 qed "V_F1";
   127 
   128 Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
   129 by (cut_facts_tac [invariantUV] 1);
   130 by (ensures_tac cmd_defs "cmd2V" 1);
   131 qed "V_F2";
   132 
   133 Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
   134 by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
   135 by (ensures_tac cmd_defs "cmd4V" 2);
   136 by (ensures_tac cmd_defs "cmd3V" 1);
   137 qed "V_F3";
   138 
   139 Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
   140 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   141 	  MRS LeadsTo_Diff) 1);
   142 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   143 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   144 val V_lemma2 = result();
   145 
   146 Goal "LeadsTo Mprg {s. NN s = 1} {s. ~ PP s}";
   147 by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
   148 by (Blast_tac 1);
   149 val V_lemma1 = result();
   150 
   151 Goal "LeadsTo Mprg {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
   152 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   153 	                addcongs [rev_conj_cong]) 1);
   154 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   155 				  V_lemma1, V_lemma2, V_F3] ) 1);
   156 val V_lemma123 = result();
   157 
   158 
   159 (*Misra's F4*)
   160 Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
   161 by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   162 by Auto_tac;
   163 qed "v_Leadsto_not_p";
   164 
   165 
   166 (** Absence of starvation **)
   167 
   168 (*Misra's F6*)
   169 Goal "LeadsTo Mprg {s. MM s = 1} {s. MM s = 3}";
   170 by (rtac LeadsTo_Un_duplicate 1);
   171 by (rtac LeadsTo_cancel2 1);
   172 by (rtac U_F2 2);
   173 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   174 by (stac Un_commute 1);
   175 by (rtac LeadsTo_Un_duplicate 1);
   176 by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
   177 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   178 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   179 qed "m1_Leadsto_3";
   180 
   181 
   182 (*The same for V*)
   183 Goal "LeadsTo Mprg {s. NN s = 1} {s. NN s = 3}";
   184 by (rtac LeadsTo_Un_duplicate 1);
   185 by (rtac LeadsTo_cancel2 1);
   186 by (rtac V_F2 2);
   187 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   188 by (stac Un_commute 1);
   189 by (rtac LeadsTo_Un_duplicate 1);
   190 by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless  RSN(2, LeadsTo_cancel2)) 1);
   191 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   192 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   193 qed "n1_Leadsto_3";