src/HOL/UNITY/Mutex.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5320 79b326bceafb
     1.1 --- a/src/HOL/UNITY/Mutex.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -26,34 +26,35 @@
     1.4  
     1.5  Addsimps update_defs;
     1.6  
     1.7 -
     1.8  Addsimps [invariantU_def, invariantV_def];
     1.9  
    1.10  
    1.11 -Goalw [Mprg_def] "invariant Mprg invariantU";
    1.12 -by (rtac invariantI 1);
    1.13 +Goalw [Mprg_def] "Invariant Mprg invariantU";
    1.14 +by (rtac InvariantI 1);
    1.15  by (constrains_tac cmd_defs 2);
    1.16  by Auto_tac;
    1.17  qed "invariantU";
    1.18  
    1.19 -Goalw [Mprg_def] "invariant Mprg invariantV";
    1.20 -by (rtac invariantI 1);
    1.21 +Goalw [Mprg_def] "Invariant Mprg invariantV";
    1.22 +by (rtac InvariantI 1);
    1.23  by (constrains_tac cmd_defs 2);
    1.24  by Auto_tac;
    1.25  qed "invariantV";
    1.26  
    1.27 -val invariantUV = invariant_Int_rule [invariantU, invariantV];
    1.28 +val invariantUV = Invariant_Int_rule [invariantU, invariantV];
    1.29  
    1.30  
    1.31  (*The safety property: mutual exclusion*)
    1.32  Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
    1.33 -by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
    1.34 +by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
    1.35  by Auto_tac;
    1.36  qed "mutual_exclusion";
    1.37  
    1.38  
    1.39  (*The bad invariant FAILS in cmd1V*)
    1.40 -Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU";
    1.41 +Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
    1.42 +by (rtac InvariantI 1);
    1.43 +by (Force_tac 1);
    1.44  by (constrains_tac cmd_defs 1);
    1.45  by (REPEAT (trans_tac 1));
    1.46  by (safe_tac (claset() addSEs [le_SucE]));
    1.47 @@ -67,7 +68,7 @@
    1.48  
    1.49  (*** Progress for U ***)
    1.50  
    1.51 -Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}";
    1.52 +Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
    1.53  by (constrains_tac cmd_defs 1);
    1.54  qed "U_F0";
    1.55  
    1.56 @@ -77,13 +78,12 @@
    1.57  
    1.58  Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    1.59  by (cut_facts_tac [invariantUV] 1);
    1.60 -bw Mprg_def;
    1.61 +by (rewtac Mprg_def);
    1.62  by (ensures_tac cmd_defs "cmd2U" 1);
    1.63  qed "U_F2";
    1.64  
    1.65  Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
    1.66 -by (rtac leadsTo_imp_LeadsTo 1); 
    1.67 -by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
    1.68 +by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
    1.69  by (ensures_tac cmd_defs "cmd4U" 2);
    1.70  by (ensures_tac cmd_defs "cmd3U" 1);
    1.71  qed "U_F3";
    1.72 @@ -109,15 +109,15 @@
    1.73  
    1.74  (*Misra's F4*)
    1.75  Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
    1.76 -by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
    1.77 +by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
    1.78  by Auto_tac;
    1.79 -qed "u_leadsto_p";
    1.80 +qed "u_Leadsto_p";
    1.81  
    1.82  
    1.83  (*** Progress for V ***)
    1.84  
    1.85  
    1.86 -Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}";
    1.87 +Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
    1.88  by (constrains_tac cmd_defs 1);
    1.89  qed "V_F0";
    1.90  
    1.91 @@ -131,8 +131,7 @@
    1.92  qed "V_F2";
    1.93  
    1.94  Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
    1.95 -by (rtac leadsTo_imp_LeadsTo 1); 
    1.96 -by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
    1.97 +by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
    1.98  by (ensures_tac cmd_defs "cmd4V" 2);
    1.99  by (ensures_tac cmd_defs "cmd3V" 1);
   1.100  qed "V_F3";
   1.101 @@ -159,9 +158,9 @@
   1.102  
   1.103  (*Misra's F4*)
   1.104  Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
   1.105 -by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
   1.106 +by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   1.107  by Auto_tac;
   1.108 -qed "v_leadsto_not_p";
   1.109 +qed "v_Leadsto_not_p";
   1.110  
   1.111  
   1.112  (** Absence of starvation **)
   1.113 @@ -174,10 +173,10 @@
   1.114  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   1.115  by (stac Un_commute 1);
   1.116  by (rtac LeadsTo_Un_duplicate 1);
   1.117 -by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
   1.118 +by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
   1.119  by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   1.120  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.121 -qed "m1_leadsto_3";
   1.122 +qed "m1_Leadsto_3";
   1.123  
   1.124  
   1.125  (*The same for V*)
   1.126 @@ -188,7 +187,7 @@
   1.127  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   1.128  by (stac Un_commute 1);
   1.129  by (rtac LeadsTo_Un_duplicate 1);
   1.130 -by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   1.131 +by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless  RSN(2, LeadsTo_cancel2)) 1);
   1.132  by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   1.133  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.134 -qed "n1_leadsto_3";
   1.135 +qed "n1_Leadsto_3";