Tidied; uses records
authorpaulson
Fri Jul 31 18:46:55 1998 +0200 (1998-07-31)
changeset 5232e5a7cdd07ea5
parent 5231 2a454140ae24
child 5233 3571ff68ceda
Tidied; uses records
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Deadlock.ML
src/HOL/UNITY/FP.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/LessThan.thy
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/Mutex.thy
src/HOL/UNITY/Network.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/Token.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:28 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:55 1998 +0200
     1.3 @@ -8,11 +8,8 @@
     1.4  From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
     1.5  *)
     1.6  
     1.7 -open Channel;
     1.8 -
     1.9  AddIffs [skip];
    1.10  
    1.11 -
    1.12  (*None represents "infinity" while Some represents proper integers*)
    1.13  Goalw [minSet_def] "minSet A = Some x --> x : A";
    1.14  by (Simp_tac 1);
     2.1 --- a/src/HOL/UNITY/Deadlock.ML	Fri Jul 31 18:46:28 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Deadlock.ML	Fri Jul 31 18:46:55 1998 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/UNITY/Traces
     2.5 +(*  Title:      HOL/UNITY/Deadlock
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1998  University of Cambridge
     3.1 --- a/src/HOL/UNITY/FP.ML	Fri Jul 31 18:46:28 1998 +0200
     3.2 +++ b/src/HOL/UNITY/FP.ML	Fri Jul 31 18:46:55 1998 +0200
     3.3 @@ -8,12 +8,6 @@
     3.4  From Misra, "A Logic for Concurrent Programming", 1994
     3.5  *)
     3.6  
     3.7 -Goal "Union(B) Int A = (UN C:B. C Int A)";
     3.8 -by (Blast_tac 1);
     3.9 -qed "Int_Union2";
    3.10 -
    3.11 -open FP;
    3.12 -
    3.13  Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
    3.14  by (stac Int_Union2 1);
    3.15  by (rtac ball_constrains_UN 1);
     4.1 --- a/src/HOL/UNITY/LessThan.ML	Fri Jul 31 18:46:28 1998 +0200
     4.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Jul 31 18:46:55 1998 +0200
     4.3 @@ -7,9 +7,6 @@
     4.4  *)
     4.5  
     4.6  
     4.7 -open LessThan;
     4.8 -
     4.9 -
    4.10  (*** lessThan ***)
    4.11  
    4.12  Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
    4.13 @@ -144,3 +141,55 @@
    4.14  qed "atMost_Int_atLeast";
    4.15  
    4.16  
    4.17 +
    4.18 +
    4.19 +(*** Finally, a few set-theoretic laws...
    4.20 +     CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)
    4.21 +
    4.22 +context Set.thy;
    4.23 +
    4.24 +(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
    4.25 +    be any set including A Int C and contained in A Un C, such as B=A or B=C.
    4.26 +**)
    4.27 +
    4.28 +Goal "[| A Int C <= B; B <= A Un C |] \
    4.29 +\     ==> (A Int B) Un (Compl A Int C) = B Un C";
    4.30 +by (Blast_tac 1);
    4.31 +
    4.32 +Goal "[| A Int C <= B; B <= A Un C |] \
    4.33 +\     ==> (A Un B) Int (Compl A Un C) = B Int C";
    4.34 +by (Blast_tac 1);
    4.35 +
    4.36 +(*The base B=A*)
    4.37 +Goal "A Un (Compl A Int C) = A Un C";
    4.38 +by (Blast_tac 1);
    4.39 +
    4.40 +Goal "A Int (Compl A Un C) = A Int C";
    4.41 +by (Blast_tac 1);
    4.42 +
    4.43 +(*The base B=C*)
    4.44 +Goal "(A Int C) Un (Compl A Int C) = C";
    4.45 +by (Blast_tac 1);
    4.46 +
    4.47 +Goal "(A Un C) Int (Compl A Un C) = C";
    4.48 +by (Blast_tac 1);
    4.49 +
    4.50 +
    4.51 +(** More ad-hoc rules **)
    4.52 +
    4.53 +Goal "A Un B - (A - B) = B";
    4.54 +by (Blast_tac 1);
    4.55 +qed "Un_Diff_Diff";
    4.56 +
    4.57 +Goal "A Int (B - C) Un C = A Int B Un C";
    4.58 +by (Blast_tac 1);
    4.59 +qed "Int_Diff_Un";
    4.60 +
    4.61 +Goal "Union(B) Int A = (UN C:B. C Int A)";
    4.62 +by (Blast_tac 1);
    4.63 +qed "Int_Union2";
    4.64 +
    4.65 +Goal "Union(B) Int A = Union((%C. C Int A)``B)";
    4.66 +by (Blast_tac 1);
    4.67 +qed "Int_Union_Union";
    4.68 +
     5.1 --- a/src/HOL/UNITY/LessThan.thy	Fri Jul 31 18:46:28 1998 +0200
     5.2 +++ b/src/HOL/UNITY/LessThan.thy	Fri Jul 31 18:46:55 1998 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  lessThan, greaterThan, atLeast, atMost
     5.5  *)
     5.6  
     5.7 -LessThan = List +
     5.8 +LessThan = Main +
     5.9  
    5.10  constdefs
    5.11  
     6.1 --- a/src/HOL/UNITY/Mutex.ML	Fri Jul 31 18:46:28 1998 +0200
     6.2 +++ b/src/HOL/UNITY/Mutex.ML	Fri Jul 31 18:46:55 1998 +0200
     6.3 @@ -6,10 +6,12 @@
     6.4  Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
     6.5  *)
     6.6  
     6.7 -open Mutex;
     6.8 +(*split_all_tac causes a big blow-up*)
     6.9 +claset_ref() := claset() delSWrapper "split_all_tac";
    6.10  
    6.11 -val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
    6.12 -		cmd2_def, cmd3_def, cmd4_def];
    6.13 +val cmd_defs = [mutex_def, 
    6.14 +		cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
    6.15 +		cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
    6.16  
    6.17  Goalw [mutex_def] "id : mutex";
    6.18  by (Simp_tac 1);
    6.19 @@ -17,7 +19,16 @@
    6.20  AddIffs [id_in_mutex];
    6.21  
    6.22  
    6.23 -(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
    6.24 +(*Simplification for records*)
    6.25 +val select_defs = thms"state.select_defs"
    6.26 +and update_defs = thms"state.update_defs"
    6.27 +and dest_defs   = thms"state.dest_defs";
    6.28 +
    6.29 +Addsimps update_defs;
    6.30 +
    6.31 +
    6.32 +(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS
    6.33 +     [They have free occurrences of mutex_def and cmd_defs] **)
    6.34  
    6.35  (*proves "constrains" properties when the program is specified*)
    6.36  val constrains_tac = 
    6.37 @@ -32,82 +43,67 @@
    6.38  (*proves "ensures" properties when the program is specified*)
    6.39  fun ensures_tac sact = 
    6.40      SELECT_GOAL
    6.41 -      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
    6.42 +      (EVERY [etac reachable_LeadsTo_Basis 1 
    6.43 +	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    6.44 +		  REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, 
    6.45 +				    ensuresI] 1),
    6.46  	      res_inst_tac [("act", sact)] transient_mem 2,
    6.47 -	      Simp_tac 2,
    6.48 +	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
    6.49 +	      simp_tac (simpset() addsimps [mutex_def]) 2,
    6.50  	      constrains_tac 1,
    6.51  	      rewrite_goals_tac cmd_defs,
    6.52 +	      ALLGOALS Clarify_tac,
    6.53  	      Auto_tac]);
    6.54  
    6.55  
    6.56 -(*The booleans p, u, v are always either 0 or 1*)
    6.57 -Goalw [stable_def, boolVars_def]
    6.58 -    "stable mutex boolVars";
    6.59 +Goalw [stable_def, invariantU_def] "stable mutex invariantU";
    6.60  by (constrains_tac 1);
    6.61 -by (auto_tac (claset() addSEs [less_SucE], simpset()));
    6.62 -qed "stable_boolVars";
    6.63 +qed "stable_invariantU";
    6.64  
    6.65 -Goal "reachable (MInit,mutex) <= boolVars";
    6.66 -by (rtac strongest_invariant 1);
    6.67 -by (rtac stable_boolVars 2);
    6.68 -by (rewrite_goals_tac [MInit_def, boolVars_def]);
    6.69 -by Auto_tac;
    6.70 -qed "reachable_subset_boolVars";
    6.71 -
    6.72 -val reachable_subset_boolVars' = 
    6.73 -    rewrite_rule [boolVars_def] reachable_subset_boolVars;
    6.74 +Goalw [stable_def, invariantV_def] "stable mutex invariantV";
    6.75 +by (constrains_tac 1);
    6.76 +qed "stable_invariantV";
    6.77  
    6.78 -Goalw [stable_def, invariant_def]
    6.79 -    "stable mutex (invariant 0 UU MM)";
    6.80 -by (constrains_tac 1);
    6.81 -qed "stable_invar_0um";
    6.82 +Goalw [MInit_def, invariantU_def] "MInit <= invariantU";
    6.83 +by Auto_tac;
    6.84 +qed "MInit_invariantU";
    6.85  
    6.86 -Goalw [stable_def, invariant_def]
    6.87 -    "stable mutex (invariant 1 VV NN)";
    6.88 -by (constrains_tac 1);
    6.89 -qed "stable_invar_1vn";
    6.90 -
    6.91 -Goalw [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
    6.92 +Goalw [MInit_def, invariantV_def] "MInit <= invariantV";
    6.93  by Auto_tac;
    6.94 -qed "MInit_invar_0um";
    6.95 -
    6.96 -Goalw [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
    6.97 -by Auto_tac;
    6.98 -qed "MInit_invar_1vn";
    6.99 +qed "MInit_invariantV";
   6.100  
   6.101  (*The intersection is an invariant of the system*)
   6.102 -Goal "reachable (MInit,mutex) <= invariant 0 UU MM Int invariant 1 VV NN";
   6.103 +Goal "reachable (MInit,mutex) <= invariantU Int invariantV";
   6.104  by (simp_tac (simpset() addsimps
   6.105  	      [strongest_invariant, Int_greatest, stable_Int, 
   6.106 -	       stable_invar_0um, stable_invar_1vn, 
   6.107 -	       MInit_invar_0um,MInit_invar_1vn]) 1); 
   6.108 +	       stable_invariantU, stable_invariantV, 
   6.109 +	       MInit_invariantU,MInit_invariantV]) 1); 
   6.110  qed "reachable_subset_invariant";
   6.111  
   6.112  val reachable_subset_invariant' = 
   6.113 -    rewrite_rule [invariant_def] reachable_subset_invariant;
   6.114 +    rewrite_rule [invariantU_def, invariantV_def] reachable_subset_invariant;
   6.115  
   6.116  
   6.117  (*The safety property (mutual exclusion) follows from the claimed invar_s*)
   6.118 -Goalw [invariant_def]
   6.119 -    "{s. s MM = 3 & s NN = 3} <= \
   6.120 -\    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
   6.121 +Goalw [invariantU_def, invariantV_def]
   6.122 +    "{s. MM s = 3 & NN s = 3} <= Compl (invariantU Int invariantV)";
   6.123  by Auto_tac;
   6.124  val lemma = result();
   6.125  
   6.126 -Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable (MInit,mutex))";
   6.127 -by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
   6.128 +Goal "{s. MM s = 3 & NN s = 3} <= Compl (reachable (MInit,mutex))";
   6.129 +by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] 
   6.130 +	  MRS subset_trans) 1);
   6.131  qed "mutual_exclusion";
   6.132  
   6.133  
   6.134 -(*The bad invariant FAILS in cmd1v*)
   6.135 -Goalw [stable_def, bad_invariant_def]
   6.136 -    "stable mutex (bad_invariant 0 UU MM)";
   6.137 +(*The bad invariant FAILS in cmd1V*)
   6.138 +Goalw [stable_def, bad_invariantU_def] "stable mutex bad_invariantU";
   6.139  by (constrains_tac 1);
   6.140 -by (trans_tac 1);
   6.141 +by (REPEAT (trans_tac 1));
   6.142  by (safe_tac (claset() addSEs [le_SucE]));
   6.143  by (Asm_full_simp_tac 1);
   6.144  (*Resulting state: n=1, p=false, m=4, u=false.  
   6.145 -  Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
   6.146 +  Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
   6.147    violating the invariant!*)
   6.148  (*Check that subgoals remain: proof failed.*)
   6.149  getgoal 1;  
   6.150 @@ -115,42 +111,40 @@
   6.151  
   6.152  (*** Progress for U ***)
   6.153  
   6.154 -Goalw [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
   6.155 +Goalw [unless_def] "unless mutex {s. MM s=2} {s. MM s=3}";
   6.156  by (constrains_tac 1);
   6.157  qed "U_F0";
   6.158  
   6.159 -Goal "LeadsTo(MInit,mutex) {s. s MM=1} {s. s PP = s VV & s MM = 2}";
   6.160 -by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   6.161 -by (ensures_tac "cmd1u" 1);
   6.162 +Goal "LeadsTo(MInit,mutex) {s. MM s=1} {s. PP s = VV s & MM s = 2}";
   6.163 +by (ensures_tac "cmd1U" 1);
   6.164  qed "U_F1";
   6.165  
   6.166 -Goal "LeadsTo(MInit,mutex) {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
   6.167 +Goal "LeadsTo(MInit,mutex) {s. ~ PP s & MM s = 2} {s. MM s = 3}";
   6.168  by (cut_facts_tac [reachable_subset_invariant'] 1);
   6.169 -by (ensures_tac "cmd2 0 MM" 1);
   6.170 +by (ensures_tac "cmd2U" 1);
   6.171  qed "U_F2";
   6.172  
   6.173 -Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s MM = 3} {s. s PP = 1}";
   6.174 +Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. MM s = 3} {s. PP s}";
   6.175  by (rtac leadsTo_imp_LeadsTo 1); 
   6.176 -by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
   6.177 -by (ensures_tac "cmd4 1 MM" 2);
   6.178 -by (ensures_tac "cmd3 UU MM" 1);
   6.179 +by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
   6.180 +by (ensures_tac "cmd4U" 2);
   6.181 +by (ensures_tac "cmd3U" 1);
   6.182  qed "U_F3";
   6.183  
   6.184 -Goal "LeadsTo(MInit,mutex) {s. s MM = 2} {s. s PP = 1}";
   6.185 +Goal "LeadsTo(MInit,mutex) {s. MM s = 2} {s. PP s}";
   6.186  by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   6.187  	  MRS LeadsTo_Diff) 1);
   6.188  by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   6.189 -by (cut_facts_tac [reachable_subset_boolVars'] 1);
   6.190  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   6.191  val lemma2 = result();
   6.192  
   6.193 -Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s PP = 1}";
   6.194 +Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. PP s}";
   6.195  by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   6.196  by (Blast_tac 1);
   6.197  val lemma1 = result();
   6.198  
   6.199  
   6.200 -Goal "LeadsTo(MInit,mutex) {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
   6.201 +Goal "LeadsTo(MInit,mutex) {s. 1 <= MM s & MM s <= 3} {s. PP s}";
   6.202  by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   6.203  	                addcongs [rev_conj_cong]) 1);
   6.204  by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   6.205 @@ -159,7 +153,7 @@
   6.206  
   6.207  
   6.208  (*Misra's F4*)
   6.209 -Goal "LeadsTo(MInit,mutex) {s. s UU = 1} {s. s PP = 1}";
   6.210 +Goal "LeadsTo(MInit,mutex) {s. UU s} {s. PP s}";
   6.211  by (rtac LeadsTo_weaken_L 1);
   6.212  by (rtac lemma123 1);
   6.213  by (cut_facts_tac [reachable_subset_invariant'] 1);
   6.214 @@ -170,42 +164,40 @@
   6.215  (*** Progress for V ***)
   6.216  
   6.217  
   6.218 -Goalw [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
   6.219 +Goalw [unless_def] "unless mutex {s. NN s=2} {s. NN s=3}";
   6.220  by (constrains_tac 1);
   6.221  qed "V_F0";
   6.222  
   6.223 -Goal "LeadsTo(MInit,mutex) {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
   6.224 -by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   6.225 -by (ensures_tac "cmd1v" 1);
   6.226 +Goal "LeadsTo(MInit,mutex) {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
   6.227 +by (ensures_tac "cmd1V" 1);
   6.228  qed "V_F1";
   6.229  
   6.230 -Goal "LeadsTo(MInit,mutex) {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
   6.231 +Goal "LeadsTo(MInit,mutex) {s. PP s & NN s = 2} {s. NN s = 3}";
   6.232  by (cut_facts_tac [reachable_subset_invariant'] 1);
   6.233 -by (ensures_tac "cmd2 1 NN" 1);
   6.234 +by (ensures_tac "cmd2V" 1);
   6.235  qed "V_F2";
   6.236  
   6.237 -Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s NN = 3} {s. s PP = 0}";
   6.238 +Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. NN s = 3} {s. ~ PP s}";
   6.239  by (rtac leadsTo_imp_LeadsTo 1); 
   6.240 -by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
   6.241 -by (ensures_tac "cmd4 0 NN" 2);
   6.242 -by (ensures_tac "cmd3 VV NN" 1);
   6.243 +by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
   6.244 +by (ensures_tac "cmd4V" 2);
   6.245 +by (ensures_tac "cmd3V" 1);
   6.246  qed "V_F3";
   6.247  
   6.248 -Goal "LeadsTo(MInit,mutex) {s. s NN = 2} {s. s PP = 0}";
   6.249 +Goal "LeadsTo(MInit,mutex) {s. NN s = 2} {s. ~ PP s}";
   6.250  by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   6.251  	  MRS LeadsTo_Diff) 1);
   6.252  by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   6.253 -by (cut_facts_tac [reachable_subset_boolVars'] 1);
   6.254  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   6.255  val lemma2 = result();
   6.256  
   6.257 -Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s PP = 0}";
   6.258 +Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. ~ PP s}";
   6.259  by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   6.260  by (Blast_tac 1);
   6.261  val lemma1 = result();
   6.262  
   6.263  
   6.264 -Goal "LeadsTo(MInit,mutex) {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
   6.265 +Goal "LeadsTo(MInit,mutex) {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
   6.266  by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   6.267  	                addcongs [rev_conj_cong]) 1);
   6.268  by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   6.269 @@ -214,7 +206,7 @@
   6.270  
   6.271  
   6.272  (*Misra's F4*)
   6.273 -Goal "LeadsTo(MInit,mutex) {s. s VV = 1} {s. s PP = 0}";
   6.274 +Goal "LeadsTo(MInit,mutex) {s. VV s} {s. ~ PP s}";
   6.275  by (rtac LeadsTo_weaken_L 1);
   6.276  by (rtac lemma123 1);
   6.277  by (cut_facts_tac [reachable_subset_invariant'] 1);
   6.278 @@ -225,7 +217,7 @@
   6.279  (** Absence of starvation **)
   6.280  
   6.281  (*Misra's F6*)
   6.282 -Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s MM = 3}";
   6.283 +Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. MM s = 3}";
   6.284  by (rtac LeadsTo_Un_duplicate 1);
   6.285  by (rtac LeadsTo_cancel2 1);
   6.286  by (rtac U_F2 2);
   6.287 @@ -234,13 +226,12 @@
   6.288  by (rtac LeadsTo_Un_duplicate 1);
   6.289  by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
   6.290  by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   6.291 -by (cut_facts_tac [reachable_subset_boolVars'] 1);
   6.292  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   6.293  qed "m1_leadsto_3";
   6.294  
   6.295  
   6.296  (*The same for V*)
   6.297 -Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s NN = 3}";
   6.298 +Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. NN s = 3}";
   6.299  by (rtac LeadsTo_Un_duplicate 1);
   6.300  by (rtac LeadsTo_cancel2 1);
   6.301  by (rtac V_F2 2);
   6.302 @@ -249,6 +240,5 @@
   6.303  by (rtac LeadsTo_Un_duplicate 1);
   6.304  by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   6.305  by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   6.306 -by (cut_facts_tac [reachable_subset_boolVars'] 1);
   6.307  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   6.308  qed "n1_leadsto_3";
     7.1 --- a/src/HOL/UNITY/Mutex.thy	Fri Jul 31 18:46:28 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Mutex.thy	Fri Jul 31 18:46:55 1998 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
     7.5  *)
     7.6  
     7.7 -Mutex = Update + UNITY + Traces + SubstAx +
     7.8 +Mutex = UNITY + Traces + SubstAx +
     7.9  
    7.10  (*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
    7.11  syntax
    7.12 @@ -18,57 +18,66 @@
    7.13     "4"  == "Suc 3"
    7.14  
    7.15  
    7.16 -(*program variables*)
    7.17 -datatype pvar = PP | MM | NN | UU | VV
    7.18 -
    7.19 -(*No booleans; instead True=1 and False=0*)
    7.20 -types state = pvar => nat
    7.21 +record state =
    7.22 +  PP :: bool
    7.23 +  MM :: nat
    7.24 +  NN :: nat
    7.25 +  UU :: bool
    7.26 +  VV :: bool
    7.27  
    7.28  constdefs
    7.29 -  cmd0 :: "[pvar,pvar] => (state*state) set"
    7.30 -    "cmd0 u m == {(s,s'). s' = s(u:=1,m:=1) & s m = 0}"
    7.31 +  cmd0U :: "(state*state) set"
    7.32 +    "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}"
    7.33 +
    7.34 +  cmd1U :: "(state*state) set"
    7.35 +    "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}"
    7.36  
    7.37 -  cmd1u :: "(state*state) set"
    7.38 -    "cmd1u == {(s,s'). s' = s(PP:= s VV,MM:=2) & s MM = 1}"
    7.39 +  cmd2U :: "(state*state) set"
    7.40 +    "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}"
    7.41  
    7.42 -  cmd1v :: "(state*state) set"
    7.43 -    "cmd1v == {(s,s'). s' = s(PP:= 1 - s UU,NN:=2) & s NN = 1}"
    7.44 +  cmd3U :: "(state*state) set"
    7.45 +    "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}"
    7.46 +
    7.47 +  cmd4U :: "(state*state) set"
    7.48 +    "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}"
    7.49  
    7.50 -  (*Put pv=0 for u's program and pv=1 for v's program*)
    7.51 -  cmd2 :: "[nat,pvar] => (state*state) set"
    7.52 -    "cmd2 pv m == {(s,s'). s' = s(m:=3) & s PP = pv & s m = 2}"
    7.53 +  cmd0V :: "(state*state) set"
    7.54 +    "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}"
    7.55 +
    7.56 +  cmd1V :: "(state*state) set"
    7.57 +    "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}"
    7.58  
    7.59 -  cmd3 :: "[pvar,pvar] => (state*state) set"
    7.60 -    "cmd3 u m == {(s,s'). s' = s(u:=0,m:=4) & s m = 3}"
    7.61 +  cmd2V :: "(state*state) set"
    7.62 +    "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}"
    7.63  
    7.64 -  (*Put pv=1 for u's program and pv=0 for v's program*)
    7.65 -  cmd4 :: "[nat,pvar] => (state*state) set"
    7.66 -    "cmd4 pv m == {(s,s'). s' = s(PP:=pv,m:=0) & s m = 4}"
    7.67 +  cmd3V :: "(state*state) set"
    7.68 +    "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}"
    7.69 +
    7.70 +  cmd4V :: "(state*state) set"
    7.71 +    "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}"
    7.72  
    7.73    mutex :: "(state*state) set set"
    7.74      "mutex == {id,
    7.75 -	       cmd0 UU MM, cmd0 VV NN,
    7.76 -	       cmd1u, cmd1v,
    7.77 -	       cmd2 0 MM, cmd2 1 NN,
    7.78 -	       cmd3 UU MM, cmd3 VV NN,
    7.79 -	       cmd4 1 MM, cmd4 0 NN}"
    7.80 +	       cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
    7.81 +	       cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}"
    7.82 +
    7.83 +  (** The correct invariants **)
    7.84 +
    7.85 +  invariantU :: "state set"
    7.86 +    "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
    7.87 +		       (MM s = 3 --> ~ PP s)}"
    7.88 +
    7.89 +  invariantV :: "state set"
    7.90 +    "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) &
    7.91 +		       (NN s = 3 --> PP s)}"
    7.92 +
    7.93 +  (** The faulty invariant (for U alone) **)
    7.94 +
    7.95 +  bad_invariantU :: "state set"
    7.96 +    "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
    7.97 +		           (3 <= MM s & MM s <= 4 --> ~ PP s)}"
    7.98  
    7.99    MInit :: "state set"
   7.100 -    "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
   7.101 -
   7.102 -  boolVars :: "state set"
   7.103 -    "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
   7.104 -
   7.105 -  (*Put pv=0 for u's program and pv=1 for v's program*)
   7.106 -  invariant :: "[nat,pvar,pvar] => state set"
   7.107 -    "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
   7.108 -			     (s m = 3 --> s PP = pv)}"
   7.109 -
   7.110 -  bad_invariant :: "[nat,pvar,pvar] => state set"
   7.111 -    "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
   7.112 -			         (3 <= s m & s m <= 4 --> s PP = pv)}"
   7.113 -
   7.114 -
   7.115 -  
   7.116 +    "MInit == {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}"
   7.117  
   7.118  end
     8.1 --- a/src/HOL/UNITY/Network.ML	Fri Jul 31 18:46:28 1998 +0200
     8.2 +++ b/src/HOL/UNITY/Network.ML	Fri Jul 31 18:46:55 1998 +0200
     8.3 @@ -8,8 +8,6 @@
     8.4  From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
     8.5  *)
     8.6  
     8.7 -open Network;
     8.8 -
     8.9  val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
    8.10  Goalw [stable_def]
    8.11     "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
     9.1 --- a/src/HOL/UNITY/Reach.ML	Fri Jul 31 18:46:28 1998 +0200
     9.2 +++ b/src/HOL/UNITY/Reach.ML	Fri Jul 31 18:46:55 1998 +0200
     9.3 @@ -7,8 +7,6 @@
     9.4  	[ this example took only four days!]
     9.5  *)
     9.6  
     9.7 -open Reach;
     9.8 -
     9.9  (*TO SIMPDATA.ML??  FOR CLASET??  *)
    9.10  val major::prems = goal thy 
    9.11      "[| if P then Q else R;    \
    10.1 --- a/src/HOL/UNITY/Reach.thy	Fri Jul 31 18:46:28 1998 +0200
    10.2 +++ b/src/HOL/UNITY/Reach.thy	Fri Jul 31 18:46:55 1998 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
    10.5  *)
    10.6  
    10.7 -Reach = Update + FP + Traces + SubstAx +
    10.8 +Reach = FP + Traces + SubstAx +
    10.9  
   10.10  types   vertex
   10.11          state = "vertex=>bool"
    11.1 --- a/src/HOL/UNITY/SubstAx.ML	Fri Jul 31 18:46:28 1998 +0200
    11.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Jul 31 18:46:55 1998 +0200
    11.3 @@ -8,8 +8,6 @@
    11.4  From Misra, "A Logic for Concurrent Programming", 1994
    11.5  *)
    11.6  
    11.7 -open SubstAx;
    11.8 -
    11.9  (*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
   11.10                                             (reachable(Init,Acts) Int B') *)
   11.11  bind_thm ("constrains_reachable",
   11.12 @@ -24,9 +22,9 @@
   11.13  qed "leadsTo_imp_LeadsTo";
   11.14  
   11.15  Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A'))   \
   11.16 -\                               (A Un A'); \
   11.17 -\               transient  Acts (reachable(Init,Acts) Int (A-A')) |]   \
   11.18 -\           ==> LeadsTo(Init,Acts) A A'";
   11.19 +\                         (A Un A'); \
   11.20 +\         transient  Acts (reachable(Init,Acts) Int (A-A')) |]   \
   11.21 +\     ==> LeadsTo(Init,Acts) A A'";
   11.22  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   11.23  by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
   11.24  by (assume_tac 2);
   11.25 @@ -36,7 +34,7 @@
   11.26  qed "LeadsTo_Basis";
   11.27  
   11.28  Goal "[| LeadsTo(Init,Acts) A B;  LeadsTo(Init,Acts) B C |] \
   11.29 -\            ==> LeadsTo(Init,Acts) A C";
   11.30 +\      ==> LeadsTo(Init,Acts) A C";
   11.31  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   11.32  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
   11.33  qed "LeadsTo_Trans";
   11.34 @@ -75,15 +73,14 @@
   11.35  qed "LeadsTo_UN";
   11.36  
   11.37  (*Binary union introduction rule*)
   11.38 -Goal
   11.39 -  "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
   11.40 +Goal "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
   11.41  by (stac Un_eq_Union 1);
   11.42  by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
   11.43  qed "LeadsTo_Un";
   11.44  
   11.45  
   11.46  Goal "[| reachable(Init,Acts) Int A <= B;  id: Acts |] \
   11.47 -\            ==> LeadsTo(Init,Acts) A B";
   11.48 +\     ==> LeadsTo(Init,Acts) A B";
   11.49  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   11.50  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   11.51  qed "Int_subset_imp_LeadsTo";
   11.52 @@ -97,55 +94,51 @@
   11.53  Addsimps [empty_LeadsTo];
   11.54  
   11.55  Goal "[| reachable(Init,Acts) Int A = {};  id: Acts |] \
   11.56 -\            ==> LeadsTo(Init,Acts) A B";
   11.57 +\     ==> LeadsTo(Init,Acts) A B";
   11.58  by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
   11.59  qed "Int_empty_LeadsTo";
   11.60  
   11.61  
   11.62  Goal "[| LeadsTo(Init,Acts) A A';   \
   11.63 -\                reachable(Init,Acts) Int A' <= B' |] \
   11.64 -\             ==> LeadsTo(Init,Acts) A B'";
   11.65 +\        reachable(Init,Acts) Int A' <= B' |] \
   11.66 +\     ==> LeadsTo(Init,Acts) A B'";
   11.67  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   11.68  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
   11.69  qed_spec_mp "LeadsTo_weaken_R";
   11.70  
   11.71  
   11.72  Goal "[| LeadsTo(Init,Acts) A A'; \
   11.73 -\                reachable(Init,Acts) Int B <= A; id: Acts |]  \
   11.74 -\             ==> LeadsTo(Init,Acts) B A'";
   11.75 +\        reachable(Init,Acts) Int B <= A; id: Acts |]  \
   11.76 +\     ==> LeadsTo(Init,Acts) B A'";
   11.77  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   11.78  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
   11.79  qed_spec_mp "LeadsTo_weaken_L";
   11.80  
   11.81  
   11.82  (*Distributes over binary unions*)
   11.83 -Goal
   11.84 -  "id: Acts ==> \
   11.85 +Goal "id: Acts ==> \
   11.86  \       LeadsTo(Init,Acts) (A Un B) C  =  \
   11.87  \       (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)";
   11.88  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
   11.89  qed "LeadsTo_Un_distrib";
   11.90  
   11.91 -Goal
   11.92 -  "id: Acts ==> \
   11.93 +Goal "id: Acts ==> \
   11.94  \       LeadsTo(Init,Acts) (UN i:I. A i) B  =  \
   11.95  \       (ALL i : I. LeadsTo(Init,Acts) (A i) B)";
   11.96  by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
   11.97  qed "LeadsTo_UN_distrib";
   11.98  
   11.99 -Goal
  11.100 -  "id: Acts ==> \
  11.101 +Goal "id: Acts ==> \
  11.102  \       LeadsTo(Init,Acts) (Union S) B  =  \
  11.103  \       (ALL A : S. LeadsTo(Init,Acts) A B)";
  11.104  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
  11.105  qed "LeadsTo_Union_distrib";
  11.106  
  11.107  
  11.108 -Goal 
  11.109 -   "[| LeadsTo(Init,Acts) A A'; id: Acts;   \
  11.110 -\               reachable(Init,Acts) Int B  <= A;     \
  11.111 -\               reachable(Init,Acts) Int A' <= B' |] \
  11.112 -\           ==> LeadsTo(Init,Acts) B B'";
  11.113 +Goal "[| LeadsTo(Init,Acts) A A'; id: Acts;   \
  11.114 +\        reachable(Init,Acts) Int B  <= A;     \
  11.115 +\        reachable(Init,Acts) Int A' <= B' |] \
  11.116 +\     ==> LeadsTo(Init,Acts) B B'";
  11.117  (*PROOF FAILED: why?*)
  11.118  by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
  11.119  			       LeadsTo_weaken_L]) 1);
  11.120 @@ -153,8 +146,7 @@
  11.121  
  11.122  
  11.123  (*Set difference: maybe combine with leadsTo_weaken_L??*)
  11.124 -Goal
  11.125 -  "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
  11.126 +Goal "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
  11.127  \       ==> LeadsTo(Init,Acts) A C";
  11.128  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
  11.129  qed "LeadsTo_Diff";
  11.130 @@ -181,8 +173,7 @@
  11.131  qed "LeadsTo_UN_UN_noindex";
  11.132  
  11.133  (*Version with no index set*)
  11.134 -Goal
  11.135 -   "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
  11.136 +Goal "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
  11.137  \           ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)";
  11.138  by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
  11.139  qed "all_LeadsTo_UN_UN";
  11.140 @@ -198,31 +189,27 @@
  11.141  
  11.142  (** The cancellation law **)
  11.143  
  11.144 -Goal
  11.145 -   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
  11.146 +Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
  11.147  \              id: Acts |]    \
  11.148  \           ==> LeadsTo(Init,Acts) A (A' Un B')";
  11.149  by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
  11.150  			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
  11.151  qed "LeadsTo_cancel2";
  11.152  
  11.153 -Goal
  11.154 -   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
  11.155 +Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
  11.156  \           ==> LeadsTo(Init,Acts) A (A' Un B')";
  11.157  by (rtac LeadsTo_cancel2 1);
  11.158  by (assume_tac 2);
  11.159  by (ALLGOALS Asm_simp_tac);
  11.160  qed "LeadsTo_cancel_Diff2";
  11.161  
  11.162 -Goal
  11.163 -   "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
  11.164 +Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
  11.165  \           ==> LeadsTo(Init,Acts) A (B' Un A')";
  11.166  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  11.167  by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
  11.168  qed "LeadsTo_cancel1";
  11.169  
  11.170 -Goal
  11.171 -   "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
  11.172 +Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
  11.173  \           ==> LeadsTo(Init,Acts) A (B' Un A')";
  11.174  by (rtac LeadsTo_cancel1 1);
  11.175  by (assume_tac 2);
  11.176 @@ -263,8 +250,7 @@
  11.177  by (ALLGOALS Blast_tac);
  11.178  qed "R_PSP";
  11.179  
  11.180 -Goal
  11.181 -   "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
  11.182 +Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
  11.183  \           ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))";
  11.184  by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
  11.185  qed "R_PSP2";
  11.186 @@ -285,8 +271,7 @@
  11.187  (*** Induction rules ***)
  11.188  
  11.189  (** Meta or object quantifier ????? **)
  11.190 -Goal
  11.191 -   "[| wf r;     \
  11.192 +Goal "[| wf r;     \
  11.193  \              ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
  11.194  \                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  11.195  \              id: Acts |] \
  11.196 @@ -298,12 +283,11 @@
  11.197  qed "LeadsTo_wf_induct";
  11.198  
  11.199  
  11.200 -Goal
  11.201 -   "[| wf r;     \
  11.202 -\              ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m})                   \
  11.203 -\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  11.204 -\              id: Acts |] \
  11.205 -\           ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
  11.206 +Goal "[| wf r;     \
  11.207 +\        ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m})                   \
  11.208 +\                                    ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  11.209 +\        id: Acts |] \
  11.210 +\     ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
  11.211  by (etac LeadsTo_wf_induct 1);
  11.212  by Safe_tac;
  11.213  by (case_tac "m:I" 1);
  11.214 @@ -312,18 +296,16 @@
  11.215  qed "R_bounded_induct";
  11.216  
  11.217  
  11.218 -Goal
  11.219 -   "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
  11.220 +Goal "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
  11.221  \                                  ((A Int f-``(lessThan m)) Un B);   \
  11.222 -\              id: Acts |] \
  11.223 -\           ==> LeadsTo(Init,Acts) A B";
  11.224 +\        id: Acts |] \
  11.225 +\     ==> LeadsTo(Init,Acts) A B";
  11.226  by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
  11.227  by (assume_tac 2);
  11.228  by (Asm_simp_tac 1);
  11.229  qed "R_lessThan_induct";
  11.230  
  11.231 -Goal
  11.232 -   "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
  11.233 +Goal "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
  11.234  \                                        ((A Int f-``(lessThan m)) Un B);   \
  11.235  \              id: Acts |] \
  11.236  \           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atMost l))) Un B)";
  11.237 @@ -333,11 +315,10 @@
  11.238  by (Asm_simp_tac 1);
  11.239  qed "R_lessThan_bounded_induct";
  11.240  
  11.241 -Goal
  11.242 -   "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
  11.243 -\                                    ((A Int f-``(greaterThan m)) Un B);   \
  11.244 -\              id: Acts |] \
  11.245 -\           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
  11.246 +Goal "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
  11.247 +\                              ((A Int f-``(greaterThan m)) Un B);   \
  11.248 +\        id: Acts |] \
  11.249 +\     ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
  11.250  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  11.251      (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
  11.252  by (assume_tac 2);
  11.253 @@ -352,10 +333,9 @@
  11.254  
  11.255  (*** Completion: Binary and General Finite versions ***)
  11.256  
  11.257 -Goal
  11.258 -   "[| LeadsTo(Init,Acts) A A';  stable Acts A';   \
  11.259 -\              LeadsTo(Init,Acts) B B';  stable Acts B';  id: Acts |] \
  11.260 -\           ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
  11.261 +Goal "[| LeadsTo(Init,Acts) A A';  stable Acts A';   \
  11.262 +\        LeadsTo(Init,Acts) B B';  stable Acts B';  id: Acts |] \
  11.263 +\     ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
  11.264  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  11.265  by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
  11.266                          addSIs [stable_Int, stable_reachable]) 1);
  11.267 @@ -363,9 +343,9 @@
  11.268  
  11.269  
  11.270  Goal "[| finite I;  id: Acts |]                     \
  11.271 -\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) -->  \
  11.272 -\               (ALL i:I. stable Acts (A' i)) -->         \
  11.273 -\               LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
  11.274 +\     ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) -->  \
  11.275 +\         (ALL i:I. stable Acts (A' i)) -->         \
  11.276 +\         LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
  11.277  by (etac finite_induct 1);
  11.278  by (Asm_simp_tac 1);
  11.279  by (asm_simp_tac 
  11.280 @@ -374,12 +354,10 @@
  11.281  qed_spec_mp "R_finite_stable_completion";
  11.282  
  11.283  
  11.284 -Goal
  11.285 - "[| LeadsTo(Init,Acts) A (A' Un C);  constrains Acts A' (A' Un C); \
  11.286 -\            LeadsTo(Init,Acts) B (B' Un C);  constrains Acts B' (B' Un C); \
  11.287 -\            id: Acts |] \
  11.288 -\         ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
  11.289 -
  11.290 +Goal "[| LeadsTo(Init,Acts) A (A' Un C);  constrains Acts A' (A' Un C); \
  11.291 +\        LeadsTo(Init,Acts) B (B' Un C);  constrains Acts B' (B' Un C); \
  11.292 +\        id: Acts |] \
  11.293 +\     ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
  11.294  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
  11.295  by (dtac completion 1);
  11.296  by (assume_tac 2);
  11.297 @@ -390,11 +368,10 @@
  11.298  qed "R_completion";
  11.299  
  11.300  
  11.301 -Goal
  11.302 -   "[| finite I;  id: Acts |] \
  11.303 -\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) -->  \
  11.304 -\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
  11.305 -\               LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
  11.306 +Goal "[| finite I;  id: Acts |] \
  11.307 +\     ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) -->  \
  11.308 +\         (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
  11.309 +\         LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
  11.310  by (etac finite_induct 1);
  11.311  by (ALLGOALS Asm_simp_tac);
  11.312  by (Clarify_tac 1);
  11.313 @@ -402,3 +379,29 @@
  11.314  by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
  11.315  qed "R_finite_completion";
  11.316  
  11.317 +
  11.318 +
  11.319 +(*** Specialized laws for handling invariants ***)
  11.320 +
  11.321 +Goalw [transient_def]
  11.322 +    "[| reachable(Init,Acts) <= INV;  transient Acts (INV Int A) |]  \
  11.323 +\    ==> transient Acts (reachable(Init,Acts) Int A)";
  11.324 +by (Clarify_tac 1);
  11.325 +by (rtac bexI 1); 
  11.326 +by (assume_tac 2);
  11.327 +by (Blast_tac 1);
  11.328 +qed "reachable_transient";
  11.329 +
  11.330 +(*Eliminates the set "reachable (Init,Acts)" from the subgoals.  This boosts
  11.331 +  efficiency because the term contains a full copy of the program.*)
  11.332 +Goal "[| reachable (Init,Acts) <= INV;      \
  11.333 +\        constrains Acts (INV Int (A - A')) (A Un A'); \
  11.334 +\        transient  Acts (INV Int (A-A')) |]   \
  11.335 +\     ==> LeadsTo(Init,Acts) A A'";
  11.336 +by (rtac LeadsTo_Basis 1);
  11.337 +by (blast_tac (claset() addSIs [reachable_transient]) 2);
  11.338 +by (rewtac constrains_def);
  11.339 +by (Blast_tac 1);
  11.340 +qed "reachable_LeadsTo_Basis";
  11.341 +
  11.342 +
    12.1 --- a/src/HOL/UNITY/Token.ML	Fri Jul 31 18:46:28 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Token.ML	Fri Jul 31 18:46:55 1998 +0200
    12.3 @@ -8,11 +8,7 @@
    12.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
    12.5  *)
    12.6  
    12.7 -
    12.8 -open Token;
    12.9 -
   12.10 -
   12.11 -val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
   12.12 +val Token_defs = [HasTok_def, H_def, E_def, T_def];
   12.13  
   12.14  AddIffs [N_positive, skip];
   12.15  
   12.16 @@ -20,33 +16,14 @@
   12.17  by Auto_tac;
   12.18  qed "HasToK_partition";
   12.19  
   12.20 -Goalw Token_defs "s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
   12.21 +Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
   12.22  by (Simp_tac 1);
   12.23 -by (exhaust_tac "s (Suc i)" 1);
   12.24 +by (exhaust_tac "proc s i" 1);
   12.25  by Auto_tac;
   12.26  qed "not_E_eq";
   12.27  
   12.28 -(** We should be able to prove WellTyped as a separate Invariant.  Then
   12.29 -    the Invariant rule should let us assume that the initial
   12.30 -    state is reachable, and therefore contained in any Invariant.  Then
   12.31 -    we'd not have to mention WellTyped in the statement of this theorem.
   12.32 -**)
   12.33 -
   12.34 -Goalw [stable_def]
   12.35 -    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
   12.36 -by (rtac (stable_WT RS stable_constrains_Int) 1);
   12.37 -by (cut_facts_tac [TR2,TR4,TR5] 1);
   12.38 -by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
   12.39 -by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
   12.40 -by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   12.41 -by (case_tac "xa : HasTok i" 1);
   12.42 -by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
   12.43 -qed "token_stable";
   12.44 -
   12.45  (*This proof is in the "massaging" style and is much faster! *)
   12.46 -Goalw [stable_def]
   12.47 -    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
   12.48 -by (rtac (stable_WT RS stable_constrains_Int) 1);
   12.49 +Goalw [stable_def] "stable Acts (Compl(E i) Un (HasTok i))";
   12.50  by (rtac constrains_weaken 1);
   12.51  by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
   12.52  by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   12.53 @@ -99,9 +76,8 @@
   12.54  
   12.55  (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   12.56    Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
   12.57 -Goal
   12.58 - "[| i<N; j<N |] ==> \
   12.59 -\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
   12.60 +Goal "[| i<N; j<N |] ==>   \
   12.61 +\     leadsTo Acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
   12.62  by (case_tac "i=j" 1);
   12.63  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   12.64  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   12.65 @@ -111,27 +87,25 @@
   12.66  
   12.67  
   12.68  (*Chapter 4 variant, the one actually used below.*)
   12.69 -Goal
   12.70 - "[| i<N; j<N; i~=j |] ==> \
   12.71 -\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
   12.72 +Goal "[| i<N; j<N; i~=j |]    \
   12.73 +\     ==> leadsTo Acts (HasTok i) {s. (token s, i) : nodeOrder j}";
   12.74  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   12.75  by (Clarify_tac 1);
   12.76  by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
   12.77  qed "TR7_aux";
   12.78  
   12.79 -Goal "({s. Token s < N} Int Token -`` {m}) = \
   12.80 -\         (if m<N then Token -`` {m} else {})";
   12.81 +Goal "({s. token s < N} Int token -`` {m}) = \
   12.82 +\     (if m<N then token -`` {m} else {})";
   12.83  by Auto_tac;
   12.84 -val Token_lemma = result();
   12.85 +val token_lemma = result();
   12.86  
   12.87  
   12.88  (*Misra's TR9: the token reaches an arbitrary node*)
   12.89 -Goal
   12.90 - "j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
   12.91 +Goal "j<N ==> leadsTo Acts {s. token s < N} (HasTok j)";
   12.92  by (rtac leadsTo_weaken_R 1);
   12.93 -by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
   12.94 +by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")]
   12.95       (wf_nodeOrder RS bounded_induct) 1);
   12.96 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
   12.97 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
   12.98  						HasTok_def])));
   12.99  by (Blast_tac 2);
  12.100  by (Clarify_tac 1);
  12.101 @@ -141,10 +115,10 @@
  12.102  qed "leadsTo_j";
  12.103  
  12.104  (*Misra's TR8: a hungry process eventually eats*)
  12.105 -Goal "j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
  12.106 +Goal "j<N ==> leadsTo Acts ({s. token s < N} Int H j) (E j)";
  12.107  by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
  12.108  by (rtac TR6 2);
  12.109  by (rtac leadsTo_weaken_R 1);
  12.110  by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
  12.111  by (ALLGOALS Blast_tac);
  12.112 -qed "Token_progress";
  12.113 +qed "token_progress";
    13.1 --- a/src/HOL/UNITY/Token.thy	Fri Jul 31 18:46:28 1998 +0200
    13.2 +++ b/src/HOL/UNITY/Token.thy	Fri Jul 31 18:46:55 1998 +0200
    13.3 @@ -12,9 +12,11 @@
    13.4  Token = WFair +
    13.5  
    13.6  (*process states*)
    13.7 -datatype pstate = Hungry | Eating | Thinking | Pnum nat
    13.8 +datatype pstate = Hungry | Eating | Thinking
    13.9  
   13.10 -types state = nat => pstate
   13.11 +record state =
   13.12 +  token :: nat
   13.13 +  proc  :: nat => pstate
   13.14  
   13.15  consts
   13.16    N :: nat	(*number of nodes in the ring*)
   13.17 @@ -27,33 +29,21 @@
   13.18    next      :: nat => nat
   13.19      "next i == (Suc i) mod N"
   13.20  
   13.21 -  WellTyped :: state set
   13.22 -    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
   13.23 -
   13.24 -  Token :: state => nat
   13.25 -    "Token s == case s 0 of 
   13.26 -                    Hungry => 0
   13.27 -                  | Eating => 0
   13.28 -                  | Thinking => 0
   13.29 -                  | Pnum i => i"
   13.30 -
   13.31    HasTok :: nat => state set
   13.32 -    "HasTok i == Token -`` {i}"
   13.33 +    "HasTok i == {s. token s = i}"
   13.34  
   13.35    H :: nat => state set
   13.36 -    "H i == {s. s (Suc i) = Hungry}"
   13.37 +    "H i == {s. proc s i = Hungry}"
   13.38  
   13.39    E :: nat => state set
   13.40 -    "E i == {s. s (Suc i) = Eating}"
   13.41 +    "E i == {s. proc s i = Eating}"
   13.42  
   13.43    T :: nat => state set
   13.44 -    "T i == {s. s (Suc i) = Thinking}"
   13.45 +    "T i == {s. proc s i = Thinking}"
   13.46  
   13.47  rules
   13.48    N_positive "0<N"
   13.49  
   13.50 -  stable_WT  "stable Acts WellTyped"
   13.51 -
   13.52    skip "id: Acts"
   13.53  
   13.54    TR2  "constrains Acts (T i) (T i Un H i)"
    14.1 --- a/src/HOL/UNITY/Traces.ML	Fri Jul 31 18:46:28 1998 +0200
    14.2 +++ b/src/HOL/UNITY/Traces.ML	Fri Jul 31 18:46:55 1998 +0200
    14.3 @@ -9,9 +9,6 @@
    14.4  
    14.5  *)
    14.6  
    14.7 -open Traces;
    14.8 -
    14.9 -
   14.10  (****
   14.11  Now simulate the inductive definition (illegal due to paired arguments)
   14.12  
   14.13 @@ -38,7 +35,7 @@
   14.14  \     ==> (s,s'): act --> s' : reachable(Init,Acts)";
   14.15  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
   14.16  by (etac exE 1);
   14.17 -be traces.induct 1;
   14.18 +by (etac traces.induct 1);
   14.19  by (ALLGOALS Asm_simp_tac);
   14.20  by (ALLGOALS (blast_tac (claset() addIs traces.intrs)));
   14.21  qed_spec_mp "reachable_Acts";
   14.22 @@ -54,7 +51,7 @@
   14.23  \  ==> P za";
   14.24  by (cut_facts_tac [major] 1);
   14.25  by Auto_tac;
   14.26 -be traces.induct 1;
   14.27 +by (etac traces.induct 1);
   14.28  by (ALLGOALS (blast_tac (claset() addIs prems)));
   14.29  qed "reachable_induct";
   14.30  
   14.31 @@ -71,7 +68,7 @@
   14.32  Goalw [stable_def, constrains_def]
   14.33      "[| Init<=A;  stable Acts A |] ==> reachable(Init,Acts) <= A";
   14.34  by (rtac subsetI 1);
   14.35 -be reachable.induct 1;
   14.36 +by (etac reachable.induct 1);
   14.37  by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   14.38  qed "strongest_invariant";
   14.39  
    15.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Jul 31 18:46:28 1998 +0200
    15.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Jul 31 18:46:55 1998 +0200
    15.3 @@ -12,49 +12,6 @@
    15.4  HOL_quantifiers := false;
    15.5  
    15.6  
    15.7 -(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
    15.8 -
    15.9 -(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
   15.10 -    be any set including A Int C and contained in A Un C, such as B=A or B=C.
   15.11 -**)
   15.12 -
   15.13 -Goal "[| A Int C <= B; B <= A Un C |] \
   15.14 -\              ==> (A Int B) Un (Compl A Int C) = B Un C";
   15.15 -by (Blast_tac 1);
   15.16 -
   15.17 -Goal "[| A Int C <= B; B <= A Un C |] \
   15.18 -\              ==> (A Un B) Int (Compl A Un C) = B Int C";
   15.19 -by (Blast_tac 1);
   15.20 -
   15.21 -(*The base B=A*)
   15.22 -Goal "A Un (Compl A Int C) = A Un C";
   15.23 -by (Blast_tac 1);
   15.24 -
   15.25 -Goal "A Int (Compl A Un C) = A Int C";
   15.26 -by (Blast_tac 1);
   15.27 -
   15.28 -(*The base B=C*)
   15.29 -Goal "(A Int C) Un (Compl A Int C) = C";
   15.30 -by (Blast_tac 1);
   15.31 -
   15.32 -Goal "(A Un C) Int (Compl A Un C) = C";
   15.33 -by (Blast_tac 1);
   15.34 -
   15.35 -
   15.36 -(** More ad-hoc rules **)
   15.37 -
   15.38 -Goal "A Un B - (A - B) = B";
   15.39 -by (Blast_tac 1);
   15.40 -qed "Un_Diff_Diff";
   15.41 -
   15.42 -Goal "A Int (B - C) Un C = A Int B Un C";
   15.43 -by (Blast_tac 1);
   15.44 -qed "Int_Diff_Un";
   15.45 -
   15.46 -
   15.47 -open UNITY;
   15.48 -
   15.49 -
   15.50  (*** constrains ***)
   15.51  
   15.52  val prems = goalw thy [constrains_def]
    16.1 --- a/src/HOL/UNITY/WFair.ML	Fri Jul 31 18:46:28 1998 +0200
    16.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Jul 31 18:46:55 1998 +0200
    16.3 @@ -8,12 +8,6 @@
    16.4  From Misra, "A Logic for Concurrent Programming", 1994
    16.5  *)
    16.6  
    16.7 -open WFair;
    16.8 -
    16.9 -Goal "Union(B) Int A = Union((%C. C Int A)``B)";
   16.10 -by (Blast_tac 1);
   16.11 -qed "Int_Union_Union";
   16.12 -
   16.13  
   16.14  (*** transient ***)
   16.15  
   16.16 @@ -121,7 +115,7 @@
   16.17  \              ==> P A C; \
   16.18  \     !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
   16.19  \  |] ==> P za zb";
   16.20 -br (major RS leadsto.induct) 1;
   16.21 +by (rtac (major RS leadsto.induct) 1);
   16.22  by (REPEAT (blast_tac (claset() addIs prems) 1));
   16.23  qed "leadsTo_induct";
   16.24