Now id:(Acts prg) is implicit
authorpaulson
Tue Sep 29 15:58:47 1998 +0200 (1998-09-29)
changeset 5584aad639e56d4e
parent 5583 d2377657f8ef
child 5585 8fcb0f181ad6
Now id:(Acts prg) is implicit
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Handshake.thy
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Mutex.thy
src/HOL/UNITY/NSP_Bad.thy
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Common.ML	Tue Sep 29 15:58:25 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Common.ML	Tue Sep 29 15:58:47 1998 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  Goal "[| ALL m. Constrains prg {m} (maxfg m); \
     1.6  \               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
     1.7 -\               n: common;  id: Acts prg |]  \
     1.8 +\               n: common |]  \
     1.9  \            ==> LeadsTo prg (atMost n) common";
    1.10  by (rtac LeadsTo_weaken_R 1);
    1.11  by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    1.12 @@ -82,7 +82,7 @@
    1.13  (*The "ALL m: -common" form echoes CMT6.*)
    1.14  Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    1.15  \               ALL m: -common. LeadsTo prg {m} (greaterThan m); \
    1.16 -\               n: common;  id: Acts prg |]  \
    1.17 +\               n: common |]  \
    1.18  \            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
    1.19  by (rtac lemma 1);
    1.20  by (ALLGOALS Asm_simp_tac);
     2.1 --- a/src/HOL/UNITY/Constrains.ML	Tue Sep 29 15:58:25 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Constrains.ML	Tue Sep 29 15:58:47 1998 +0200
     2.3 @@ -89,14 +89,14 @@
     2.4  qed "ball_Constrains_INT";
     2.5  
     2.6  Goalw [Constrains_def]
     2.7 -     "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
     2.8 +     "Constrains prg A A' ==> reachable prg Int A <= A'";
     2.9  by (dtac constrains_imp_subset 1);
    2.10 -by (assume_tac 1);
    2.11 -by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
    2.12 +by (ALLGOALS
    2.13 +    (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
    2.14  qed "Constrains_imp_subset";
    2.15  
    2.16  Goalw [Constrains_def]
    2.17 -    "[| id: Acts prg; Constrains prg A B; Constrains prg B C |]   \
    2.18 +    "[| Constrains prg A B; Constrains prg B C |]   \
    2.19  \    ==> Constrains prg A C";
    2.20  by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
    2.21  qed "Constrains_trans";
    2.22 @@ -167,7 +167,7 @@
    2.23  qed "Elimination_sing";
    2.24  
    2.25  Goalw [Constrains_def, constrains_def]
    2.26 -   "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
    2.27 +   "[| Constrains prg A (A' Un B); Constrains prg B B' |] \
    2.28  \   ==> Constrains prg A (A' Un B')";
    2.29  by (Blast_tac 1);
    2.30  qed "Constrains_cancel";
     3.1 --- a/src/HOL/UNITY/Handshake.ML	Tue Sep 29 15:58:25 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Handshake.ML	Tue Sep 29 15:58:47 1998 +0200
     3.3 @@ -20,11 +20,6 @@
     3.4  Addsimps [simp_of_set invFG_def];
     3.5  
     3.6  
     3.7 -Goalw [Join_def] "id : Acts (Join prgF prgG) ";
     3.8 -by (Simp_tac 1);
     3.9 -qed "id_in_Acts";
    3.10 -AddIffs [id_in_Acts];
    3.11 -
    3.12  Goal "Invariant (Join prgF prgG) invFG";
    3.13  by (rtac InvariantI 1);
    3.14  by (Force_tac 1);
    3.15 @@ -59,6 +54,5 @@
    3.16  by (rtac lemma2_2 2);
    3.17  by (rtac LeadsTo_Trans 1);
    3.18  by (rtac lemma2_2 2);
    3.19 -by (rtac (lemma2_1) 1);
    3.20 -by Auto_tac;
    3.21 +by (rtac lemma2_1 1);
    3.22  qed "progress";
     4.1 --- a/src/HOL/UNITY/Handshake.thy	Tue Sep 29 15:58:25 1998 +0200
     4.2 +++ b/src/HOL/UNITY/Handshake.thy	Tue Sep 29 15:58:47 1998 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  
     4.5    prgF :: "state program"
     4.6      "prgF == (|Init = {s. NF s = 0 & BB s},
     4.7 -	       Acts = {id, cmdF}|)"
     4.8 +	       Acts0 = {cmdF}|)"
     4.9  
    4.10    (*G's program*)
    4.11    cmdG :: "(state*state) set"
    4.12 @@ -30,7 +30,7 @@
    4.13  
    4.14    prgG :: "state program"
    4.15      "prgG == (|Init = {s. NG s = 0 & BB s},
    4.16 -	       Acts = {id, cmdG}|)"
    4.17 +	       Acts0 = {cmdG}|)"
    4.18  
    4.19    (*the joint invariant*)
    4.20    invFG :: "state set"
     5.1 --- a/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:25 1998 +0200
     5.2 +++ b/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:47 1998 +0200
     5.3 @@ -118,8 +118,8 @@
     5.4      (*for the moment, we OMIT button_press*)
     5.5      "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
     5.6  		          ~ open s & req s = {}},
     5.7 -	       Acts = {id, request_act, open_act, close_act,
     5.8 -		       req_up, req_down, move_up, move_down}|)"
     5.9 +	       Acts0 = {request_act, open_act, close_act,
    5.10 +		        req_up, req_down, move_up, move_down}|)"
    5.11  
    5.12  
    5.13    (** Invariants **)
     6.1 --- a/src/HOL/UNITY/Mutex.thy	Tue Sep 29 15:58:25 1998 +0200
     6.2 +++ b/src/HOL/UNITY/Mutex.thy	Tue Sep 29 15:58:47 1998 +0200
     6.3 @@ -63,9 +63,8 @@
     6.4  
     6.5    Mprg :: state program
     6.6      "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0},
     6.7 -	       Acts = {id,
     6.8 -	               cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
     6.9 -	               cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
    6.10 +	       Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
    6.11 +	                cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
    6.12  
    6.13  
    6.14    (** The correct invariants **)
     7.1 --- a/src/HOL/UNITY/NSP_Bad.thy	Tue Sep 29 15:58:25 1998 +0200
     7.2 +++ b/src/HOL/UNITY/NSP_Bad.thy	Tue Sep 29 15:58:47 1998 +0200
     7.3 @@ -55,6 +55,6 @@
     7.4    Nprg :: state program
     7.5      (*Initial trace is empty*)
     7.6      "Nprg == (|Init = {[]},   
     7.7 -	       Acts = {id, Fake, NS1, NS2, NS3}|)"
     7.8 +	       Acts0 = {Fake, NS1, NS2, NS3}|)"
     7.9  
    7.10  end
     8.1 --- a/src/HOL/UNITY/Reach.thy	Tue Sep 29 15:58:25 1998 +0200
     8.2 +++ b/src/HOL/UNITY/Reach.thy	Tue Sep 29 15:58:47 1998 +0200
     8.3 @@ -25,7 +25,7 @@
     8.4  
     8.5    Rprg :: state program
     8.6      "Rprg == (|Init = {%v. v=init},
     8.7 -	       Acts = insert id (UN (u,v): edges. {asgt u v})|)"
     8.8 +	       Acts0 = (UN (u,v): edges. {asgt u v})|)"
     8.9  
    8.10    reach_invariant :: state set
    8.11      "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
     9.1 --- a/src/HOL/UNITY/SubstAx.ML	Tue Sep 29 15:58:25 1998 +0200
     9.2 +++ b/src/HOL/UNITY/SubstAx.ML	Tue Sep 29 15:58:47 1998 +0200
     9.3 @@ -65,7 +65,7 @@
     9.4  
     9.5  (*** Derived rules ***)
     9.6  
     9.7 -Goal "id: Acts prg ==> LeadsTo prg A UNIV";
     9.8 +Goal "LeadsTo prg A UNIV";
     9.9  by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
    9.10  				      Int_lower1 RS subset_imp_leadsTo]) 1);
    9.11  qed "LeadsTo_UNIV";
    9.12 @@ -92,7 +92,7 @@
    9.13  by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
    9.14  qed "LeadsTo_Un";
    9.15  
    9.16 -Goal "[| A <= B;  id: Acts prg |] ==> LeadsTo prg A B";
    9.17 +Goal "[| A <= B |] ==> LeadsTo prg A B";
    9.18  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    9.19  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
    9.20  qed "subset_imp_LeadsTo";
    9.21 @@ -105,20 +105,20 @@
    9.22  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
    9.23  qed_spec_mp "LeadsTo_weaken_R";
    9.24  
    9.25 -Goal "[| LeadsTo prg A A';  B <= A; id: Acts prg |]  \
    9.26 +Goal "[| LeadsTo prg A A';  B <= A |]  \
    9.27  \     ==> LeadsTo prg B A'";
    9.28  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    9.29  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
    9.30  qed_spec_mp "LeadsTo_weaken_L";
    9.31  
    9.32 -Goal "[| LeadsTo prg A A'; id: Acts prg;   \
    9.33 +Goal "[| LeadsTo prg A A';   \
    9.34  \        B  <= A;   A' <= B' |] \
    9.35  \     ==> LeadsTo prg B B'";
    9.36  by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
    9.37  			       LeadsTo_Trans]) 1);
    9.38  qed "LeadsTo_weaken";
    9.39  
    9.40 -Goal "[| reachable prg <= C;  LeadsTo prg A A'; id: Acts prg;   \
    9.41 +Goal "[| reachable prg <= C;  LeadsTo prg A A';   \
    9.42  \        C Int B <= A;   C Int A' <= B' |] \
    9.43  \     ==> LeadsTo prg B B'";
    9.44  by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
    9.45 @@ -127,11 +127,11 @@
    9.46  
    9.47  (** Two theorems for "proof lattices" **)
    9.48  
    9.49 -Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
    9.50 +Goal "[| LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
    9.51  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
    9.52  qed "LeadsTo_Un_post";
    9.53  
    9.54 -Goal "[| id: Acts prg;  LeadsTo prg A B;  LeadsTo prg B C |] \
    9.55 +Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] \
    9.56  \     ==> LeadsTo prg (A Un B) C";
    9.57  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
    9.58  			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
    9.59 @@ -140,21 +140,15 @@
    9.60  
    9.61  (** Distributive laws **)
    9.62  
    9.63 -Goal "id: Acts prg ==> \
    9.64 -\       LeadsTo prg (A Un B) C  =  \
    9.65 -\       (LeadsTo prg A C & LeadsTo prg B C)";
    9.66 +Goal "LeadsTo prg (A Un B) C  = (LeadsTo prg A C & LeadsTo prg B C)";
    9.67  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
    9.68  qed "LeadsTo_Un_distrib";
    9.69  
    9.70 -Goal "id: Acts prg ==> \
    9.71 -\       LeadsTo prg (UN i:I. A i) B  =  \
    9.72 -\       (ALL i : I. LeadsTo prg (A i) B)";
    9.73 +Goal "LeadsTo prg (UN i:I. A i) B  =  (ALL i : I. LeadsTo prg (A i) B)";
    9.74  by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
    9.75  qed "LeadsTo_UN_distrib";
    9.76  
    9.77 -Goal "id: Acts prg ==> \
    9.78 -\       LeadsTo prg (Union S) B  =  \
    9.79 -\       (ALL A : S. LeadsTo prg A B)";
    9.80 +Goal "LeadsTo prg (Union S) B  =  (ALL A : S. LeadsTo prg A B)";
    9.81  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
    9.82  qed "LeadsTo_Union_distrib";
    9.83  
    9.84 @@ -181,7 +175,7 @@
    9.85  qed "Invariant_LeadsTo_Basis";
    9.86  
    9.87  Goal "[| Invariant prg INV;      \
    9.88 -\        LeadsTo prg A A'; id: Acts prg;   \
    9.89 +\        LeadsTo prg A A';   \
    9.90  \        INV Int B  <= A;  INV Int A' <= B' |] \
    9.91  \     ==> LeadsTo prg B B'";
    9.92  by (rtac Invariant_LeadsToI 1);
    9.93 @@ -194,7 +188,7 @@
    9.94  
    9.95  (*Set difference: maybe combine with leadsTo_weaken_L??
    9.96    This is the most useful form of the "disjunction" rule*)
    9.97 -Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
    9.98 +Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C |] \
    9.99  \     ==> LeadsTo prg A C";
   9.100  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
   9.101  qed "LeadsTo_Diff";
   9.102 @@ -236,27 +230,26 @@
   9.103  
   9.104  (** The cancellation law **)
   9.105  
   9.106 -Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \
   9.107 -\        id: Acts prg |]    \
   9.108 +Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B' |]    \
   9.109  \     ==> LeadsTo prg A (A' Un B')";
   9.110  by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
   9.111  			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
   9.112  qed "LeadsTo_cancel2";
   9.113  
   9.114 -Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: Acts prg |] \
   9.115 +Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B' |] \
   9.116  \     ==> LeadsTo prg A (A' Un B')";
   9.117  by (rtac LeadsTo_cancel2 1);
   9.118  by (assume_tac 2);
   9.119  by (ALLGOALS Asm_simp_tac);
   9.120  qed "LeadsTo_cancel_Diff2";
   9.121  
   9.122 -Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: Acts prg |] \
   9.123 +Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B' |] \
   9.124  \     ==> LeadsTo prg A (B' Un A')";
   9.125  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   9.126  by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
   9.127  qed "LeadsTo_cancel1";
   9.128  
   9.129 -Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: Acts prg |] \
   9.130 +Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B' |] \
   9.131  \     ==> LeadsTo prg A (B' Un A')";
   9.132  by (rtac LeadsTo_cancel1 1);
   9.133  by (assume_tac 2);
   9.134 @@ -291,24 +284,23 @@
   9.135  qed "PSP_stable2";
   9.136  
   9.137  Goalw [LeadsTo_def, Constrains_def]
   9.138 -     "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   9.139 +     "[| LeadsTo prg A A'; Constrains prg B B' |] \
   9.140  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
   9.141  by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
   9.142  qed "PSP";
   9.143  
   9.144 -Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   9.145 +Goal "[| LeadsTo prg A A'; Constrains prg B B' |] \
   9.146  \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
   9.147  by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
   9.148  qed "PSP2";
   9.149  
   9.150  Goalw [Unless_def]
   9.151 -     "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
   9.152 +     "[| LeadsTo prg A A'; Unless prg B B' |] \
   9.153  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
   9.154  by (dtac PSP 1);
   9.155  by (assume_tac 1);
   9.156  by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
   9.157 -			       subset_imp_LeadsTo]) 2);
   9.158 -by (assume_tac 1);
   9.159 +			       subset_imp_LeadsTo]) 1);
   9.160  qed "PSP_Unless";
   9.161  
   9.162  
   9.163 @@ -317,20 +309,18 @@
   9.164  (** Meta or object quantifier ????? **)
   9.165  Goal "[| wf r;     \
   9.166  \        ALL m. LeadsTo prg (A Int f-``{m})                     \
   9.167 -\                           ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   9.168 -\        id: Acts prg |] \
   9.169 +\                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   9.170  \     ==> LeadsTo prg A B";
   9.171  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   9.172  by (etac leadsTo_wf_induct 1);
   9.173 -by (assume_tac 2);
   9.174 +by (Simp_tac 2);
   9.175  by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   9.176  qed "LeadsTo_wf_induct";
   9.177  
   9.178  
   9.179  Goal "[| wf r;     \
   9.180  \        ALL m:I. LeadsTo prg (A Int f-``{m})                   \
   9.181 -\                             ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   9.182 -\        id: Acts prg |] \
   9.183 +\                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   9.184  \     ==> LeadsTo prg A ((A - (f-``I)) Un B)";
   9.185  by (etac LeadsTo_wf_induct 1);
   9.186  by Safe_tac;
   9.187 @@ -341,45 +331,37 @@
   9.188  
   9.189  
   9.190  Goal "[| ALL m. LeadsTo prg (A Int f-``{m})                     \
   9.191 -\                           ((A Int f-``(lessThan m)) Un B);   \
   9.192 -\        id: Acts prg |] \
   9.193 +\                           ((A Int f-``(lessThan m)) Un B) |] \
   9.194  \     ==> LeadsTo prg A B";
   9.195  by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
   9.196 -by (assume_tac 2);
   9.197  by (Asm_simp_tac 1);
   9.198  qed "LessThan_induct";
   9.199  
   9.200  (*Integer version.  Could generalize from #0 to any lower bound*)
   9.201 -val [reach, prem, id] =
   9.202 +val [reach, prem] =
   9.203  Goal "[| reachable prg <= {s. #0 <= f s};  \
   9.204  \        !! z. LeadsTo prg (A Int {s. f s = z})                     \
   9.205 -\                           ((A Int {s. f s < z}) Un B);   \
   9.206 -\        id: Acts prg |] \
   9.207 +\                           ((A Int {s. f s < z}) Un B) |] \
   9.208  \     ==> LeadsTo prg A B";
   9.209  by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
   9.210  by (simp_tac (simpset() addsimps [vimage_def]) 1);
   9.211  br ([reach, prem] MRS reachable_LeadsTo_weaken) 1;
   9.212 -by (auto_tac (claset(),
   9.213 -	      simpset() addsimps [id, nat_eq_iff, nat_less_iff]));
   9.214 +by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
   9.215  qed "integ_0_le_induct";
   9.216  
   9.217  Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m})   \
   9.218 -\                                        ((A Int f-``(lessThan m)) Un B);   \
   9.219 -\              id: Acts prg |] \
   9.220 +\                                        ((A Int f-``(lessThan m)) Un B) |] \
   9.221  \           ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
   9.222  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
   9.223  by (rtac (wf_less_than RS Bounded_induct) 1);
   9.224 -by (assume_tac 2);
   9.225  by (Asm_simp_tac 1);
   9.226  qed "LessThan_bounded_induct";
   9.227  
   9.228  Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m})   \
   9.229 -\                              ((A Int f-``(greaterThan m)) Un B);   \
   9.230 -\        id: Acts prg |] \
   9.231 +\                              ((A Int f-``(greaterThan m)) Un B) |] \
   9.232  \     ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
   9.233  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   9.234      (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
   9.235 -by (assume_tac 2);
   9.236  by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
   9.237  by (Clarify_tac 1);
   9.238  by (case_tac "m<l" 1);
   9.239 @@ -391,14 +373,14 @@
   9.240  (*** Completion: Binary and General Finite versions ***)
   9.241  
   9.242  Goal "[| LeadsTo prg A A';  Stable prg A';   \
   9.243 -\        LeadsTo prg B B';  Stable prg B';  id: Acts prg |] \
   9.244 +\        LeadsTo prg B B';  Stable prg B' |] \
   9.245  \     ==> LeadsTo prg (A Int B) (A' Int B')";
   9.246  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
   9.247  by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
   9.248  qed "Stable_completion";
   9.249  
   9.250  
   9.251 -Goal "[| finite I;  id: Acts prg |]      \
   9.252 +Goal "finite I      \
   9.253  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
   9.254  \         (ALL i:I. Stable prg (A' i)) -->         \
   9.255  \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
   9.256 @@ -409,8 +391,7 @@
   9.257  
   9.258  
   9.259  Goal "[| LeadsTo prg A (A' Un C);  Constrains prg A' (A' Un C); \
   9.260 -\        LeadsTo prg B (B' Un C);  Constrains prg B' (B' Un C); \
   9.261 -\        id: Acts prg |] \
   9.262 +\        LeadsTo prg B (B' Un C);  Constrains prg B' (B' Un C) |] \
   9.263  \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
   9.264  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
   9.265  				       Int_Un_distrib]) 1);
   9.266 @@ -418,7 +399,7 @@
   9.267  qed "Completion";
   9.268  
   9.269  
   9.270 -Goal "[| finite I;  id: Acts prg |] \
   9.271 +Goal "[| finite I |] \
   9.272  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) -->  \
   9.273  \         (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
   9.274  \         LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
    10.1 --- a/src/HOL/UNITY/Traces.ML	Tue Sep 29 15:58:25 1998 +0200
    10.2 +++ b/src/HOL/UNITY/Traces.ML	Tue Sep 29 15:58:47 1998 +0200
    10.3 @@ -9,6 +9,13 @@
    10.4  
    10.5  *)
    10.6  
    10.7 +Goal "id: Acts prg";
    10.8 +by (simp_tac (simpset() addsimps [Acts_def]) 1);
    10.9 +qed "id_in_Acts";
   10.10 +AddIffs [id_in_Acts];
   10.11 +
   10.12 +
   10.13 +
   10.14  Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
   10.15  by Safe_tac;
   10.16  by (etac traces.induct 2);
   10.17 @@ -20,11 +27,12 @@
   10.18  by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
   10.19  qed "stable_reachable";
   10.20  
   10.21 -Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
   10.22 +Goalw [Acts_def]
   10.23 +     "(act : Acts(|Init=init, Acts0=acts|)) = (act=id | act : acts)";
   10.24  by Auto_tac;
   10.25  qed "Acts_eq";
   10.26  
   10.27 -Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
   10.28 +Goal "(s : Init(|Init=init, Acts0=acts|)) = (s:init)";
   10.29  by Auto_tac;
   10.30  qed "Init_eq";
   10.31  
   10.32 @@ -34,8 +42,8 @@
   10.33  (*** These three rules allow "lazy" definition expansion ***)
   10.34  
   10.35  val [rew] = goal thy
   10.36 -    "[| prg == (|Init=init, Acts=acts|) |] \
   10.37 -\    ==> Init prg = init & Acts prg = acts";
   10.38 +    "[| prg == (|Init=init, Acts0=acts|) |] \
   10.39 +\    ==> Init prg = init & Acts prg = insert id acts";
   10.40  by (rewtac rew);
   10.41  by Auto_tac;
   10.42  qed "def_prg_simps";
    11.1 --- a/src/HOL/UNITY/Traces.thy	Tue Sep 29 15:58:25 1998 +0200
    11.2 +++ b/src/HOL/UNITY/Traces.thy	Tue Sep 29 15:58:47 1998 +0200
    11.3 @@ -25,8 +25,13 @@
    11.4  
    11.5  
    11.6  record 'a program =
    11.7 -  Init :: 'a set
    11.8 -  Acts :: "('a * 'a)set set"
    11.9 +  Init  :: 'a set
   11.10 +  Acts0 :: "('a * 'a)set set"
   11.11 +
   11.12 +
   11.13 +constdefs
   11.14 +    Acts :: "'a program => ('a * 'a)set set"
   11.15 +    "Acts prg == insert id (Acts0 prg)"
   11.16  
   11.17  
   11.18  consts reachable :: "'a program => 'a set"
    12.1 --- a/src/HOL/UNITY/Union.ML	Tue Sep 29 15:58:25 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Union.ML	Tue Sep 29 15:58:47 1998 +0200
    12.3 @@ -14,19 +14,27 @@
    12.4  qed "Init_Join";
    12.5  
    12.6  Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
    12.7 -by (simp_tac (simpset() addsimps [Join_def]) 1);
    12.8 +by (auto_tac (claset(),
    12.9 +	      simpset() addsimps [Acts_def, Join_def]));
   12.10  qed "Acts_Join";
   12.11  
   12.12  Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
   12.13  by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   12.14  qed "Init_JN";
   12.15  
   12.16 -Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
   12.17 -by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   12.18 +Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))";
   12.19 +by (auto_tac (claset(),
   12.20 +	      simpset() addsimps [Acts_def, JOIN_def]));
   12.21  qed "Acts_JN";
   12.22  
   12.23  Addsimps [Init_Join, Init_JN];
   12.24  
   12.25 +Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)";
   12.26 +by (simp_tac (simpset() addsimps [Acts_def, JOIN_def, Join_def]) 1);
   12.27 +qed "JN_insert";
   12.28 +Addsimps[JN_insert];
   12.29 +
   12.30 +
   12.31  (** Theoretical issues **)
   12.32  
   12.33  Goal "Join prgF prgG = Join prgG prgF";
   12.34 @@ -34,7 +42,7 @@
   12.35  qed "Join_commute";
   12.36  
   12.37  Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
   12.38 -by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
   12.39 +by (simp_tac (simpset() addsimps Un_ac@[Join_def, Acts_def, Int_assoc]) 1);
   12.40  qed "Join_assoc";
   12.41  
   12.42  
   12.43 @@ -50,13 +58,20 @@
   12.44  *)
   12.45  
   12.46  
   12.47 -(**NOT PROVABLE because no "surjective pairing" for records
   12.48 -Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
   12.49 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   12.50 -qed "Join_Null";
   12.51 -*)
   12.52 +
   12.53 +
   12.54  
   12.55  (**NOT PROVABLE because no "surjective pairing" for records
   12.56 +Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF";
   12.57 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   12.58 +qed "Join_SKIP";
   12.59 +
   12.60 +    In order to prove Join_SKIP, we possibly need
   12.61 +    "Acts0 = ... - {id}" in JOIN_def and Join_def.  But then Join_absorb only
   12.62 +    holds if id ~: Acts0(prg).  Or else we need to change 'a program to 
   12.63 +    an abstract type!  Then equality could be made to ignore Acts0.
   12.64 +
   12.65 +NOT PROVABLE because no "surjective pairing" for records
   12.66  Goalw [Join_def] "Join prgF prgF = prgF";
   12.67  by Auto_tac;
   12.68  qed "Join_absorb";
   12.69 @@ -64,10 +79,19 @@
   12.70  
   12.71  
   12.72  
   12.73 +Goal "(JN G:{}. G) = SKIP";
   12.74 +by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
   12.75 +qed "JN_empty";
   12.76 +Addsimps [JN_empty];
   12.77 +
   12.78 +
   12.79 +
   12.80 +
   12.81  (*** Safety: constrains, stable, FP ***)
   12.82  
   12.83  Goalw [constrains_def, JOIN_def]
   12.84 -    "constrains (Acts (JN i:I. prg i)) A B = \
   12.85 +    "I ~= {} ==> \
   12.86 +\    constrains (Acts (JN i:I. prg i)) A B = \
   12.87  \    (ALL i:I. constrains (Acts (prg i)) A B)";
   12.88  by Auto_tac;
   12.89  qed "constrains_JN";
   12.90 @@ -80,10 +104,11 @@
   12.91  qed "Constrains_JN";
   12.92  **)
   12.93  
   12.94 -Goalw [constrains_def, Join_def]
   12.95 -    "constrains (Acts (Join prgF prgG)) A B =  \
   12.96 -\    (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
   12.97 -by (simp_tac (simpset() addsimps [ball_Un]) 1);
   12.98 +Goal "constrains (Acts (Join prgF prgG)) A B =  \
   12.99 +\     (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
  12.100 +by (auto_tac
  12.101 +    (claset(),
  12.102 +     simpset() addsimps [constrains_def, Join_def, Acts_def, ball_Un]));
  12.103  qed "constrains_Join";
  12.104  
  12.105  Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
  12.106 @@ -92,9 +117,9 @@
  12.107  by (blast_tac (claset() addIs [constrains_weaken]) 1);
  12.108  qed "constrains_Join_weaken";
  12.109  
  12.110 -Goalw [stable_def] 
  12.111 -    "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
  12.112 -by (simp_tac (simpset() addsimps [constrains_JN]) 1);
  12.113 +Goal "I ~= {} ==> \
  12.114 +\     stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
  12.115 +by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
  12.116  qed "stable_JN";
  12.117  
  12.118  Goal "stable (Acts (Join prgF prgG)) A = \
  12.119 @@ -102,30 +127,32 @@
  12.120  by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  12.121  qed "stable_Join";
  12.122  
  12.123 -Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
  12.124 -by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
  12.125 +Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
  12.126 +by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
  12.127  qed "FP_JN";
  12.128  
  12.129  
  12.130  (*** Progress: transient, ensures ***)
  12.131  
  12.132 -Goalw [transient_def, JOIN_def]
  12.133 -   "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
  12.134 -by (Simp_tac 1);
  12.135 +Goal "I ~= {} ==> \
  12.136 +\   transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
  12.137 +by (auto_tac (claset(),
  12.138 +	      simpset() addsimps [transient_def, JOIN_def]));
  12.139  qed "transient_JN";
  12.140  
  12.141 -Goalw [transient_def, Join_def]
  12.142 -   "transient (Acts (Join prgF prgG)) A = \
  12.143 -\   (transient (Acts prgF) A | transient (Acts prgG) A)";
  12.144 -by (simp_tac (simpset() addsimps [bex_Un]) 1);
  12.145 +Goal "transient (Acts (Join prgF prgG)) A = \
  12.146 +\     (transient (Acts prgF) A | transient (Acts prgG) A)";
  12.147 +by (auto_tac (claset(),
  12.148 +	      simpset() addsimps [bex_Un, Acts_def, transient_def,
  12.149 +				  Join_def]));
  12.150  qed "transient_Join";
  12.151  
  12.152 -Goalw [ensures_def]
  12.153 -    "ensures (Acts (JN i:I. prg i)) A B = \
  12.154 -\    ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
  12.155 -\     (EX i:I. ensures (Acts (prg i)) A B))";
  12.156 +Goal "I ~= {} ==> \
  12.157 +\     ensures (Acts (JN i:I. prg i)) A B = \
  12.158 +\     ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
  12.159 +\      (EX i:I. ensures (Acts (prg i)) A B))";
  12.160  by (auto_tac (claset(),
  12.161 -	      simpset() addsimps [constrains_JN, transient_JN]));
  12.162 +	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
  12.163  qed "ensures_JN";
  12.164  
  12.165  Goalw [ensures_def]
  12.166 @@ -146,7 +173,7 @@
  12.167  
  12.168  (*Premises cannot use Invariant because  Stable prgF A  is weaker than
  12.169    stable (Acts prgG) A *)
  12.170 -Goal  "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
  12.171 +Goal "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
  12.172  \      ==> Invariant (Join prgF prgG) A";
  12.173  by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
  12.174  				  stable_Join]) 1);
    13.1 --- a/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:25 1998 +0200
    13.2 +++ b/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:47 1998 +0200
    13.3 @@ -12,15 +12,15 @@
    13.4  
    13.5  constdefs
    13.6     JOIN  :: ['a set, 'a => 'b program] => 'b program
    13.7 -    "JOIN I prg == (|Init = INT i:I. Init (prg i),
    13.8 -	           Acts = UN  i:I. Acts (prg i)|)"
    13.9 +    "JOIN I prg == (|Init  = INT i:I. Init (prg i),
   13.10 +	             Acts0 = UN  i:I. Acts (prg i)|)"
   13.11  
   13.12     Join :: ['a program, 'a program] => 'a program
   13.13 -    "Join prgF prgG == (|Init = Init prgF Int Init prgG,
   13.14 -			 Acts = Acts prgF Un Acts prgG|)"
   13.15 +    "Join prgF prgG == (|Init  = Init prgF Int Init prgG,
   13.16 +			 Acts0 = Acts prgF Un Acts prgG|)"
   13.17  
   13.18 -   Null :: 'a program
   13.19 -    "Null == (|Init = UNIV, Acts = {id}|)"
   13.20 +   SKIP :: 'a program
   13.21 +    "SKIP == (|Init = UNIV, Acts0 = {}|)"
   13.22  
   13.23  syntax
   13.24    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)