Constrains, Stable, Invariant...more of the substitution axiom, but Union
authorpaulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 53131861a564d7e2
parent 5312 b380921982b9
child 5314 c061e6f9d546
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Common.thy
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Common.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Common.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -11,25 +11,21 @@
     1.4  *)
     1.5  
     1.6  (*Misra's property CMT4: t exceeds no common meeting time*)
     1.7 -Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
     1.8 -\     ==> stable acts (atMost n)";
     1.9 -by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
    1.10 +Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
    1.11 +\     ==> Stable prg (atMost n)";
    1.12 +by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    1.13  by (asm_full_simp_tac
    1.14 -    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
    1.15 -			 constrains_def, le_max_iff_disj]) 1);
    1.16 -by (Clarify_tac 1);
    1.17 -by (dtac bspec 1);
    1.18 -by (assume_tac 1);
    1.19 -by (blast_tac (claset() addSEs [subsetCE]
    1.20 -			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    1.21 +    (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
    1.22 +			 le_max_iff_disj]) 1);
    1.23 +by (etac Constrains_weaken_R 1);
    1.24 +by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    1.25  qed "common_stable";
    1.26  
    1.27 -Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
    1.28 -\     ==> invariant (|Init={0}, Acts=acts|) (atMost n)";
    1.29 -by (rtac invariantI 1);
    1.30 -by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
    1.31 -by (simp_tac (simpset() addsimps [atMost_def]) 1);
    1.32 -qed "common_invariant";
    1.33 +Goal "[| Init prg <= atMost n;  \
    1.34 +\        ALL m. Constrains prg {m} (maxfg m); n: common |] \
    1.35 +\     ==> Invariant prg (atMost n)";
    1.36 +by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
    1.37 +qed "common_Invariant";
    1.38  
    1.39  
    1.40  (*** Some programs that implement the safety property above ***)
    1.41 @@ -71,23 +67,23 @@
    1.42  
    1.43  Addsimps [atMost_Int_atLeast];
    1.44  
    1.45 -Goal "[| ALL m. constrains acts {m} (maxfg m); \
    1.46 -\               ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
    1.47 -\               n: common;  id: acts |]  \
    1.48 -\            ==> leadsTo acts (atMost n) common";
    1.49 -by (rtac leadsTo_weaken_R 1);
    1.50 -by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    1.51 +Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    1.52 +\               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
    1.53 +\               n: common;  id: Acts prg |]  \
    1.54 +\            ==> LeadsTo prg (atMost n) common";
    1.55 +by (rtac LeadsTo_weaken_R 1);
    1.56 +by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    1.57  by (ALLGOALS Asm_simp_tac);
    1.58  by (rtac subset_refl 2);
    1.59 -by (blast_tac (claset() addDs [psp_stable2] 
    1.60 -                        addIs [common_stable, leadsTo_weaken_R]) 1);
    1.61 +by (blast_tac (claset() addDs [PSP_stable2] 
    1.62 +                        addIs [common_stable, LeadsTo_weaken_R]) 1);
    1.63  val lemma = result();
    1.64  
    1.65  (*The "ALL m: Compl common" form echoes CMT6.*)
    1.66 -Goal "[| ALL m. constrains acts {m} (maxfg m); \
    1.67 -\               ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
    1.68 -\               n: common;  id: acts |]  \
    1.69 -\            ==> leadsTo acts (atMost (LEAST n. n: common)) common";
    1.70 +Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    1.71 +\               ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
    1.72 +\               n: common;  id: Acts prg |]  \
    1.73 +\            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
    1.74  by (rtac lemma 1);
    1.75  by (ALLGOALS Asm_simp_tac);
    1.76  by (etac LeastI 2);
     2.1 --- a/src/HOL/UNITY/Common.thy	Thu Aug 13 17:44:50 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Common.thy	Thu Aug 13 18:06:40 1998 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
     2.5  *)
     2.6  
     2.7 -Common = WFair + Traces +
     2.8 +Common = SubstAx +
     2.9  
    2.10  consts
    2.11    ftime,gtime :: nat=>nat
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Constrains.ML	Thu Aug 13 18:06:40 1998 +0200
     3.3 @@ -0,0 +1,262 @@
     3.4 +(*  Title:      HOL/UNITY/Constrains
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1998  University of Cambridge
     3.8 +
     3.9 +Safety relations: restricted to the set of reachable states.
    3.10 +*)
    3.11 +
    3.12 +
    3.13 +
    3.14 +(**MOVE TO EQUALITIES.ML**)
    3.15 +
    3.16 +Goal "(A Un B <= C) = (A <= C & B <= C)";
    3.17 +by (Blast_tac 1);
    3.18 +qed "Un_subset_iff";
    3.19 +
    3.20 +Goal "(C <= A Int B) = (C <= A & C <= B)";
    3.21 +by (Blast_tac 1);
    3.22 +qed "Int_subset_iff";
    3.23 +
    3.24 +
    3.25 +(*** Constrains ***)
    3.26 +
    3.27 +(*constrains (Acts prg) B B'
    3.28 +  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
    3.29 +bind_thm ("constrains_reachable_Int",
    3.30 +	  subset_refl RS
    3.31 +	  rewrite_rule [stable_def] stable_reachable RS 
    3.32 +	  constrains_Int);
    3.33 +
    3.34 +Goalw [Constrains_def]
    3.35 +    "constrains (Acts prg) A A' ==> Constrains prg A A'";
    3.36 +by (etac constrains_reachable_Int 1);
    3.37 +qed "constrains_imp_Constrains";
    3.38 +
    3.39 +val prems = Goal
    3.40 +    "(!!act s s'. [| act: Acts prg;  (s,s') : act;  s: A |] ==> s': A') \
    3.41 +\    ==> Constrains prg A A'";
    3.42 +by (rtac constrains_imp_Constrains 1);
    3.43 +by (blast_tac (claset() addIs (constrainsI::prems)) 1);
    3.44 +qed "ConstrainsI";
    3.45 +
    3.46 +Goalw [Constrains_def, constrains_def] "Constrains prg {} B";
    3.47 +by (Blast_tac 1);
    3.48 +qed "Constrains_empty";
    3.49 +
    3.50 +Goal "Constrains prg A UNIV";
    3.51 +by (blast_tac (claset() addIs [ConstrainsI]) 1);
    3.52 +qed "Constrains_UNIV";
    3.53 +AddIffs [Constrains_empty, Constrains_UNIV];
    3.54 +
    3.55 +
    3.56 +Goalw [Constrains_def]
    3.57 +    "[| Constrains prg A A'; A'<=B' |] ==> Constrains prg A B'";
    3.58 +by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
    3.59 +qed "Constrains_weaken_R";
    3.60 +
    3.61 +Goalw [Constrains_def]
    3.62 +    "[| Constrains prg A A'; B<=A |] ==> Constrains prg B A'";
    3.63 +by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
    3.64 +qed "Constrains_weaken_L";
    3.65 +
    3.66 +Goalw [Constrains_def]
    3.67 +   "[| Constrains prg A A'; B<=A; A'<=B' |] ==> Constrains prg B B'";
    3.68 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    3.69 +qed "Constrains_weaken";
    3.70 +
    3.71 +(** Union **)
    3.72 +
    3.73 +Goalw [Constrains_def]
    3.74 +    "[| Constrains prg A A'; Constrains prg B B' |]   \
    3.75 +\    ==> Constrains prg (A Un B) (A' Un B')";
    3.76 +by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
    3.77 +qed "Constrains_Un";
    3.78 +
    3.79 +Goalw [Constrains_def]
    3.80 +    "ALL i:I. Constrains prg (A i) (A' i) \
    3.81 +\    ==> Constrains prg (UN i:I. A i) (UN i:I. A' i)";
    3.82 +by (dtac ball_constrains_UN 1);
    3.83 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    3.84 +qed "ball_Constrains_UN";
    3.85 +
    3.86 +(** Intersection **)
    3.87 +
    3.88 +Goalw [Constrains_def]
    3.89 +    "[| Constrains prg A A'; Constrains prg B B' |]   \
    3.90 +\    ==> Constrains prg (A Int B) (A' Int B')";
    3.91 +by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
    3.92 +qed "Constrains_Int";
    3.93 +
    3.94 +Goalw [Constrains_def]
    3.95 +    "[| ALL i:I. Constrains prg (A i) (A' i) |]   \
    3.96 +\    ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
    3.97 +by (dtac ball_constrains_INT 1);
    3.98 +by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
    3.99 +qed "ball_Constrains_INT";
   3.100 +
   3.101 +Goalw [Constrains_def]
   3.102 +     "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
   3.103 +by (dtac constrains_imp_subset 1);
   3.104 +by (assume_tac 1);
   3.105 +by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
   3.106 +qed "Constrains_imp_subset";
   3.107 +
   3.108 +Goalw [Constrains_def]
   3.109 +    "[| id: Acts prg; Constrains prg A B; Constrains prg B C |]   \
   3.110 +\    ==> Constrains prg A C";
   3.111 +by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
   3.112 +qed "Constrains_trans";
   3.113 +
   3.114 +
   3.115 +(*** Stable ***)
   3.116 +
   3.117 +Goal "Stable prg A = stable (Acts prg) (reachable prg Int A)";
   3.118 +by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
   3.119 +qed "Stable_eq_stable";
   3.120 +
   3.121 +Goalw [Stable_def] "Constrains prg A A ==> Stable prg A";
   3.122 +by (assume_tac 1);
   3.123 +qed "StableI";
   3.124 +
   3.125 +Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
   3.126 +by (assume_tac 1);
   3.127 +qed "StableD";
   3.128 +
   3.129 +Goalw [Stable_def]
   3.130 +    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
   3.131 +by (blast_tac (claset() addIs [Constrains_Un]) 1);
   3.132 +qed "Stable_Un";
   3.133 +
   3.134 +Goalw [Stable_def]
   3.135 +    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Int A')";
   3.136 +by (blast_tac (claset() addIs [Constrains_Int]) 1);
   3.137 +qed "Stable_Int";
   3.138 +
   3.139 +Goalw [Stable_def]
   3.140 +    "[| Stable prg C; Constrains prg A (C Un A') |]   \
   3.141 +\    ==> Constrains prg (C Un A) (C Un A')";
   3.142 +by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
   3.143 +qed "Stable_Constrains_Un";
   3.144 +
   3.145 +Goalw [Stable_def]
   3.146 +    "[| Stable prg C; Constrains prg (C Int A) A' |]   \
   3.147 +\    ==> Constrains prg (C Int A) (C Int A')";
   3.148 +by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
   3.149 +qed "Stable_Constrains_Int";
   3.150 +
   3.151 +Goalw [Stable_def]
   3.152 +    "(ALL i:I. Stable prg (A i)) ==> Stable prg (INT i:I. A i)";
   3.153 +by (etac ball_Constrains_INT 1);
   3.154 +qed "ball_Stable_INT";
   3.155 +
   3.156 +Goal "Stable prg (reachable prg)";
   3.157 +by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
   3.158 +qed "Stable_reachable";
   3.159 +
   3.160 +
   3.161 +
   3.162 +(*** The Elimination Theorem.  The "free" m has become universally quantified!
   3.163 +     Should the premise be !!m instead of ALL m ?  Would make it harder to use
   3.164 +     in forward proof. ***)
   3.165 +
   3.166 +Goalw [Constrains_def, constrains_def]
   3.167 +    "[| ALL m. Constrains prg {s. s x = m} (B m) |] \
   3.168 +\    ==> Constrains prg {s. s x : M} (UN m:M. B m)";
   3.169 +by (Blast_tac 1);
   3.170 +qed "Elimination";
   3.171 +
   3.172 +(*As above, but for the trivial case of a one-variable state, in which the
   3.173 +  state is identified with its one variable.*)
   3.174 +Goalw [Constrains_def, constrains_def]
   3.175 +    "(ALL m. Constrains prg {m} (B m)) ==> Constrains prg M (UN m:M. B m)";
   3.176 +by (Blast_tac 1);
   3.177 +qed "Elimination_sing";
   3.178 +
   3.179 +Goalw [Constrains_def, constrains_def]
   3.180 +   "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
   3.181 +\   ==> Constrains prg A (A' Un B')";
   3.182 +by (Blast_tac 1);
   3.183 +qed "Constrains_cancel";
   3.184 +
   3.185 +
   3.186 +(*** Specialized laws for handling Invariants ***)
   3.187 +
   3.188 +(** Natural deduction rules for "Invariant prg A" **)
   3.189 +
   3.190 +Goal "[| Init prg<=A;  Stable prg A |] ==> Invariant prg A";
   3.191 +by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
   3.192 +qed "InvariantI";
   3.193 +
   3.194 +Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
   3.195 +by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
   3.196 +qed "InvariantD";
   3.197 +
   3.198 +bind_thm ("InvariantE", InvariantD RS conjE);
   3.199 +
   3.200 +
   3.201 +(*The set of all reachable states is an Invariant...*)
   3.202 +Goal "Invariant prg (reachable prg)";
   3.203 +by (simp_tac (simpset() addsimps [Invariant_def]) 1);
   3.204 +by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
   3.205 +qed "Invariant_reachable";
   3.206 +
   3.207 +(*...in fact the strongest Invariant!*)
   3.208 +Goal "Invariant prg A ==> reachable prg <= A";
   3.209 +by (full_simp_tac 
   3.210 +    (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
   3.211 +			 Invariant_def]) 1);
   3.212 +by (rtac subsetI 1);
   3.213 +by (etac reachable.induct 1);
   3.214 +by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   3.215 +qed "Invariant_includes_reachable";
   3.216 +
   3.217 +
   3.218 +Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
   3.219 +by (dtac Invariant_includes_reachable 1);
   3.220 +by (Blast_tac 1);
   3.221 +qed "reachable_Int_INV";
   3.222 +
   3.223 +Goal "[| Invariant prg INV;  Constrains prg (INV Int A) A' |]   \
   3.224 +\     ==> Constrains prg A A'";
   3.225 +by (asm_full_simp_tac
   3.226 +    (simpset() addsimps [Constrains_def, reachable_Int_INV,
   3.227 +			 Int_assoc RS sym]) 1);
   3.228 +qed "Invariant_ConstrainsI";
   3.229 +
   3.230 +bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
   3.231 +
   3.232 +Goal "[| Invariant prg INV;  Constrains prg A A' |]   \
   3.233 +\     ==> Constrains prg A (INV Int A')";
   3.234 +by (asm_full_simp_tac
   3.235 +    (simpset() addsimps [Constrains_def, reachable_Int_INV,
   3.236 +			 Int_assoc RS sym]) 1);
   3.237 +qed "Invariant_ConstrainsD";
   3.238 +
   3.239 +bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
   3.240 +
   3.241 +
   3.242 +
   3.243 +(** Conjoining Invariants **)
   3.244 +
   3.245 +Goal "[| Invariant prg A;  Invariant prg B |] ==> Invariant prg (A Int B)";
   3.246 +by (auto_tac (claset(),
   3.247 +	      simpset() addsimps [Invariant_def, Stable_Int]));
   3.248 +qed "Invariant_Int";
   3.249 +
   3.250 +(*Delete the nearest invariance assumption (which will be the second one
   3.251 +  used by Invariant_Int) *)
   3.252 +val Invariant_thin =
   3.253 +    read_instantiate_sg (sign_of thy)
   3.254 +                [("V", "Invariant ?Prg ?A")] thin_rl;
   3.255 +
   3.256 +(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   3.257 +val Invariant_Int_tac = dtac Invariant_Int THEN' 
   3.258 +                        assume_tac THEN'
   3.259 +			etac Invariant_thin;
   3.260 +
   3.261 +(*Combines two invariance THEOREMS into one.*)
   3.262 +val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
   3.263 +
   3.264 +
   3.265 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/Constrains.thy	Thu Aug 13 18:06:40 1998 +0200
     4.3 @@ -0,0 +1,28 @@
     4.4 +(*  Title:      HOL/UNITY/Constrains
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1998  University of Cambridge
     4.8 +
     4.9 +Safety relations: restricted to the set of reachable states.
    4.10 +*)
    4.11 +
    4.12 +Constrains = UNITY + Traces + 
    4.13 +
    4.14 +constdefs
    4.15 +
    4.16 +  Constrains :: "['a program, 'a set, 'a set] => bool"
    4.17 +    "Constrains prg A B == 
    4.18 +		 constrains (Acts prg)
    4.19 +                            (reachable prg  Int  A)
    4.20 +  		            (reachable prg  Int  B)"
    4.21 +
    4.22 +  Stable     :: "'a program => 'a set => bool"
    4.23 +    "Stable prg A == Constrains prg A A"
    4.24 +
    4.25 +  Unless :: "['a program, 'a set, 'a set] => bool"
    4.26 +    "Unless prg A B == Constrains prg (A-B) (A Un B)"
    4.27 +
    4.28 +  Invariant :: "['a program, 'a set] => bool"
    4.29 +  "Invariant prg A == (Init prg) <= A & Stable prg A"
    4.30 +
    4.31 +end
     5.1 --- a/src/HOL/UNITY/Handshake.ML	Thu Aug 13 17:44:50 1998 +0200
     5.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Aug 13 18:06:40 1998 +0200
     5.3 @@ -22,40 +22,40 @@
     5.4  AddIffs [id_in_Acts];
     5.5  
     5.6  
     5.7 -Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
     5.8 -by (rtac invariantI 1);
     5.9 -by (force_tac (claset(), 
    5.10 -	       simpset() addsimps [Join_def]) 1);
    5.11 -by (auto_tac (claset(), simpset() addsimps [stable_Join]));
    5.12 +Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
    5.13 +by (rtac InvariantI 1);
    5.14 +by (Force_tac 1);
    5.15 +by (rtac (constrains_imp_Constrains RS StableI) 1);
    5.16 +by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
    5.17  by (constrains_tac [prgG_def,cmdG_def] 2);
    5.18  by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
    5.19  by (constrains_tac [prgF_def,cmdF_def] 1);
    5.20  qed "invFG";
    5.21  
    5.22  Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
    5.23 -br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    5.24 +by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    5.25  by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    5.26  by (constrains_tac [prgF_def,cmdF_def] 1);
    5.27  qed "lemma2_1";
    5.28  
    5.29  Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
    5.30 -br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    5.31 +by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    5.32  by (constrains_tac [prgG_def,cmdG_def] 2);
    5.33  by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    5.34  qed "lemma2_2";
    5.35  
    5.36  
    5.37  Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
    5.38 -br LeadsTo_weaken_R 1;
    5.39 +by (rtac LeadsTo_weaken_R 1);
    5.40  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    5.41      GreaterThan_bounded_induct 1);
    5.42  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    5.43  by (trans_tac 2);
    5.44  (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
    5.45 -br LeadsTo_Diff 1;
    5.46 -br lemma2_2 2;
    5.47 -br LeadsTo_Trans 1;
    5.48 -br lemma2_2 2;
    5.49 -br (lemma2_1 RS LeadsTo_weaken_L) 1;
    5.50 +by (rtac LeadsTo_Diff 1);
    5.51 +by (rtac lemma2_2 2);
    5.52 +by (rtac LeadsTo_Trans 1);
    5.53 +by (rtac lemma2_2 2);
    5.54 +by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
    5.55  by Auto_tac;
    5.56  qed "progress";
     6.1 --- a/src/HOL/UNITY/Lift.ML	Thu Aug 13 17:44:50 1998 +0200
     6.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Aug 13 18:06:40 1998 +0200
     6.3 @@ -44,34 +44,36 @@
     6.4  qed "less_imp_le_pred";
     6.5  
     6.6  
     6.7 -Goalw [Lprg_def] "invariant Lprg open_stop";
     6.8 -by (rtac invariantI 1);
     6.9 +Goalw [Lprg_def] "Invariant Lprg open_stop";
    6.10 +by (rtac InvariantI 1);
    6.11  by (Force_tac 1);
    6.12  by (constrains_tac (cmd_defs@always_defs) 1);
    6.13  qed "open_stop";
    6.14  
    6.15 -Goalw [Lprg_def] "invariant Lprg stop_floor";
    6.16 -by (rtac invariantI 1);
    6.17 +Goalw [Lprg_def] "Invariant Lprg stop_floor";
    6.18 +by (rtac InvariantI 1);
    6.19  by (Force_tac 1);
    6.20  by (constrains_tac (cmd_defs@always_defs) 1);
    6.21  qed "stop_floor";
    6.22  
    6.23 -(*Should not have to prove open_stop concurrently!!*)
    6.24 -Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
    6.25 -by (rtac invariantI 1);
    6.26 +(*This one needs open_stop, which was proved above*)
    6.27 +Goal "Invariant Lprg open_move";
    6.28 +by (rtac InvariantI 1);
    6.29 +br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
    6.30 +bw Lprg_def;
    6.31  by (Force_tac 1);
    6.32  by (constrains_tac (cmd_defs@always_defs) 1);
    6.33  qed "open_move";
    6.34  
    6.35 -Goalw [Lprg_def] "invariant Lprg moving_up";
    6.36 -by (rtac invariantI 1);
    6.37 +Goalw [Lprg_def] "Invariant Lprg moving_up";
    6.38 +by (rtac InvariantI 1);
    6.39  by (Force_tac 1);
    6.40  by (constrains_tac (cmd_defs@always_defs) 1);
    6.41  by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
    6.42  qed "moving_up";
    6.43  
    6.44 -Goalw [Lprg_def] "invariant Lprg moving_down";
    6.45 -by (rtac invariantI 1);
    6.46 +Goalw [Lprg_def] "Invariant Lprg moving_down";
    6.47 +by (rtac InvariantI 1);
    6.48  by (Force_tac 1);
    6.49  by (constrains_tac (cmd_defs@always_defs) 1);
    6.50  by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
    6.51 @@ -82,8 +84,8 @@
    6.52  
    6.53  xxxxxxxxxxxxxxxx;
    6.54  
    6.55 -Goalw [Lprg_def] "invariant Lprg bounded";
    6.56 -by (rtac invariantI 1);
    6.57 +Goalw [Lprg_def] "Invariant Lprg bounded";
    6.58 +by (rtac InvariantI 1);
    6.59  by (Force_tac 1);
    6.60  by (constrains_tac (cmd_defs@always_defs) 1);
    6.61  by (ALLGOALS
    6.62 @@ -94,8 +96,8 @@
    6.63  by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
    6.64  qed "bounded";
    6.65  
    6.66 -Goalw [Lprg_def] "invariant Lprg invariantV";
    6.67 -by (rtac invariantI 1);
    6.68 +Goalw [Lprg_def] "Invariant Lprg invariantV";
    6.69 +by (rtac InvariantI 1);
    6.70  by (constrains_tac cmd_defs 2);
    6.71  by Auto_tac;
    6.72  qed "invariantV";
    6.73 @@ -122,7 +124,7 @@
    6.74  
    6.75  Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    6.76  by (cut_facts_tac [invariantUV] 1);
    6.77 -bw Lprg_def;
    6.78 +by (rewtac Lprg_def);
    6.79  by (ensures_tac cmd_defs "cmd2U" 1);
    6.80  qed "U_F2";
    6.81  
     7.1 --- a/src/HOL/UNITY/Mutex.ML	Thu Aug 13 17:44:50 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Aug 13 18:06:40 1998 +0200
     7.3 @@ -26,34 +26,35 @@
     7.4  
     7.5  Addsimps update_defs;
     7.6  
     7.7 -
     7.8  Addsimps [invariantU_def, invariantV_def];
     7.9  
    7.10  
    7.11 -Goalw [Mprg_def] "invariant Mprg invariantU";
    7.12 -by (rtac invariantI 1);
    7.13 +Goalw [Mprg_def] "Invariant Mprg invariantU";
    7.14 +by (rtac InvariantI 1);
    7.15  by (constrains_tac cmd_defs 2);
    7.16  by Auto_tac;
    7.17  qed "invariantU";
    7.18  
    7.19 -Goalw [Mprg_def] "invariant Mprg invariantV";
    7.20 -by (rtac invariantI 1);
    7.21 +Goalw [Mprg_def] "Invariant Mprg invariantV";
    7.22 +by (rtac InvariantI 1);
    7.23  by (constrains_tac cmd_defs 2);
    7.24  by Auto_tac;
    7.25  qed "invariantV";
    7.26  
    7.27 -val invariantUV = invariant_Int_rule [invariantU, invariantV];
    7.28 +val invariantUV = Invariant_Int_rule [invariantU, invariantV];
    7.29  
    7.30  
    7.31  (*The safety property: mutual exclusion*)
    7.32  Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
    7.33 -by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
    7.34 +by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
    7.35  by Auto_tac;
    7.36  qed "mutual_exclusion";
    7.37  
    7.38  
    7.39  (*The bad invariant FAILS in cmd1V*)
    7.40 -Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU";
    7.41 +Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
    7.42 +by (rtac InvariantI 1);
    7.43 +by (Force_tac 1);
    7.44  by (constrains_tac cmd_defs 1);
    7.45  by (REPEAT (trans_tac 1));
    7.46  by (safe_tac (claset() addSEs [le_SucE]));
    7.47 @@ -67,7 +68,7 @@
    7.48  
    7.49  (*** Progress for U ***)
    7.50  
    7.51 -Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}";
    7.52 +Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
    7.53  by (constrains_tac cmd_defs 1);
    7.54  qed "U_F0";
    7.55  
    7.56 @@ -77,13 +78,12 @@
    7.57  
    7.58  Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    7.59  by (cut_facts_tac [invariantUV] 1);
    7.60 -bw Mprg_def;
    7.61 +by (rewtac Mprg_def);
    7.62  by (ensures_tac cmd_defs "cmd2U" 1);
    7.63  qed "U_F2";
    7.64  
    7.65  Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
    7.66 -by (rtac leadsTo_imp_LeadsTo 1); 
    7.67 -by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
    7.68 +by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
    7.69  by (ensures_tac cmd_defs "cmd4U" 2);
    7.70  by (ensures_tac cmd_defs "cmd3U" 1);
    7.71  qed "U_F3";
    7.72 @@ -109,15 +109,15 @@
    7.73  
    7.74  (*Misra's F4*)
    7.75  Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
    7.76 -by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
    7.77 +by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
    7.78  by Auto_tac;
    7.79 -qed "u_leadsto_p";
    7.80 +qed "u_Leadsto_p";
    7.81  
    7.82  
    7.83  (*** Progress for V ***)
    7.84  
    7.85  
    7.86 -Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}";
    7.87 +Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
    7.88  by (constrains_tac cmd_defs 1);
    7.89  qed "V_F0";
    7.90  
    7.91 @@ -131,8 +131,7 @@
    7.92  qed "V_F2";
    7.93  
    7.94  Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
    7.95 -by (rtac leadsTo_imp_LeadsTo 1); 
    7.96 -by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
    7.97 +by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
    7.98  by (ensures_tac cmd_defs "cmd4V" 2);
    7.99  by (ensures_tac cmd_defs "cmd3V" 1);
   7.100  qed "V_F3";
   7.101 @@ -159,9 +158,9 @@
   7.102  
   7.103  (*Misra's F4*)
   7.104  Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
   7.105 -by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
   7.106 +by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   7.107  by Auto_tac;
   7.108 -qed "v_leadsto_not_p";
   7.109 +qed "v_Leadsto_not_p";
   7.110  
   7.111  
   7.112  (** Absence of starvation **)
   7.113 @@ -174,10 +173,10 @@
   7.114  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   7.115  by (stac Un_commute 1);
   7.116  by (rtac LeadsTo_Un_duplicate 1);
   7.117 -by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
   7.118 +by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
   7.119  by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   7.120  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   7.121 -qed "m1_leadsto_3";
   7.122 +qed "m1_Leadsto_3";
   7.123  
   7.124  
   7.125  (*The same for V*)
   7.126 @@ -188,7 +187,7 @@
   7.127  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   7.128  by (stac Un_commute 1);
   7.129  by (rtac LeadsTo_Un_duplicate 1);
   7.130 -by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   7.131 +by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless  RSN(2, LeadsTo_cancel2)) 1);
   7.132  by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   7.133  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   7.134 -qed "n1_leadsto_3";
   7.135 +qed "n1_Leadsto_3";
     8.1 --- a/src/HOL/UNITY/Reach.ML	Thu Aug 13 17:44:50 1998 +0200
     8.2 +++ b/src/HOL/UNITY/Reach.ML	Thu Aug 13 18:06:40 1998 +0200
     8.3 @@ -31,8 +31,8 @@
     8.4  
     8.5  Addsimps [reach_invariant_def];
     8.6  
     8.7 -Goalw [Rprg_def] "invariant Rprg reach_invariant";
     8.8 -by (rtac invariantI 1);
     8.9 +Goalw [Rprg_def] "Invariant Rprg reach_invariant";
    8.10 +by (rtac InvariantI 1);
    8.11  by Auto_tac;  (*for the initial state; proof of stability remains*)
    8.12  by (constrains_tac [Rprg_def, asgt_def] 1);
    8.13  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    8.14 @@ -117,38 +117,31 @@
    8.15  	      simpset() addsimps [fun_upd_idem]));
    8.16  qed "metric_le";
    8.17  
    8.18 -Goal "(u,v): edges ==> \
    8.19 -\              ensures (Acts Rprg) ((metric-``{m}) Int {s. s u & ~ s v})  \
    8.20 -\                            (metric-``(lessThan m))";
    8.21 -by (ensures_tac [Rprg_def, asgt_def] "asgt u v" 1);
    8.22 -by (cut_facts_tac [metric_le] 1);
    8.23 -by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
    8.24 -qed "edges_ensures";
    8.25 -
    8.26 -Goal "leadsTo (Acts Rprg) ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
    8.27 +Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
    8.28  by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
    8.29 -by (rtac leadsTo_UN 1);
    8.30 -by (split_all_tac 1);
    8.31 -by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
    8.32 -qed "leadsTo_Diff_fixedpoint";
    8.33 +by (rtac LeadsTo_UN 1);
    8.34 +by Auto_tac;
    8.35 +by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
    8.36 +by (cut_facts_tac [metric_le RS le_imp_less_or_eq] 1);
    8.37 +by (Fast_tac 1);
    8.38 +qed "LeadsTo_Diff_fixedpoint";
    8.39  
    8.40 -Goal "leadsTo (Acts Rprg) (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
    8.41 -by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
    8.42 -by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
    8.43 -qed "leadsTo_Un_fixedpoint";
    8.44 +Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
    8.45 +by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
    8.46 +by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
    8.47 +qed "LeadsTo_Un_fixedpoint";
    8.48  
    8.49  
    8.50  (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
    8.51 -Goal "leadsTo (Acts Rprg) UNIV fixedpoint";
    8.52 -by (rtac lessThan_induct 1);
    8.53 +Goal "LeadsTo Rprg UNIV fixedpoint";
    8.54 +by (rtac LessThan_induct 1);
    8.55  by Auto_tac;
    8.56 -by (rtac leadsTo_Un_fixedpoint 1);
    8.57 -qed "leadsTo_fixedpoint";
    8.58 +by (rtac LeadsTo_Un_fixedpoint 1);
    8.59 +qed "LeadsTo_fixedpoint";
    8.60  
    8.61  Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
    8.62  by (stac (fixedpoint_invariant_correct RS sym) 1);
    8.63 -by (rtac ([reach_invariant,
    8.64 -	   leadsTo_fixedpoint RS leadsTo_imp_LeadsTo] 
    8.65 -	  MRS invariant_LeadsTo_weaken) 1); 
    8.66 +by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
    8.67 +	  MRS Invariant_LeadsTo_weaken) 1); 
    8.68  by Auto_tac;
    8.69  qed "LeadsTo_correct";
     9.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 17:44:50 1998 +0200
     9.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 18:06:40 1998 +0200
     9.3 @@ -7,32 +7,22 @@
     9.4  *)
     9.5  
     9.6  
     9.7 -(*constrains (Acts prg) B B'
     9.8 -  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
     9.9 -bind_thm ("constrains_reachable",
    9.10 -	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
    9.11 -
    9.12  
    9.13  (*** Specialized laws for handling invariants ***)
    9.14  
    9.15 -Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
    9.16 -bd invariant_includes_reachable 1;
    9.17 -by (Blast_tac 1);
    9.18 -qed "reachable_Int_INV";
    9.19 -
    9.20 -Goal "[| invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
    9.21 +Goal "[| Invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
    9.22  \     ==> LeadsTo prg A A'";
    9.23  by (asm_full_simp_tac
    9.24      (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    9.25  			 Int_assoc RS sym]) 1);
    9.26 -qed "invariant_LeadsToI";
    9.27 +qed "Invariant_LeadsToI";
    9.28  
    9.29 -Goal "[| invariant prg INV;  LeadsTo prg A A' |]   \
    9.30 +Goal "[| Invariant prg INV;  LeadsTo prg A A' |]   \
    9.31  \     ==> LeadsTo prg A (INV Int A')";
    9.32  by (asm_full_simp_tac
    9.33      (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    9.34  			 Int_assoc RS sym]) 1);
    9.35 -qed "invariant_LeadsToD";
    9.36 +qed "Invariant_LeadsToD";
    9.37  
    9.38  
    9.39  (*** Introduction rules: Basis, Trans, Union ***)
    9.40 @@ -42,9 +32,6 @@
    9.41  by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
    9.42  qed "leadsTo_imp_LeadsTo";
    9.43  
    9.44 -(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
    9.45 -bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
    9.46 -
    9.47  Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] ==> LeadsTo prg A C";
    9.48  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    9.49  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    9.50 @@ -138,33 +125,37 @@
    9.51  qed "LeadsTo_weaken";
    9.52  
    9.53  
    9.54 -(** More rules using the premise "invariant prg" **)
    9.55 +(** More rules using the premise "Invariant prg" **)
    9.56  
    9.57 -Goal "[| invariant prg INV;      \
    9.58 -\        constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
    9.59 +Goalw [LeadsTo_def, Constrains_def]
    9.60 +     "[| Constrains prg (A-A') (A Un A'); transient  (Acts prg) (A-A') |]   \
    9.61 +\     ==> LeadsTo prg A A'";
    9.62 +by (rtac (ensuresI RS leadsTo_Basis) 1);
    9.63 +by (blast_tac (claset() addIs [transient_strengthen]) 2);
    9.64 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    9.65 +qed "LeadsTo_Basis";
    9.66 +
    9.67 +Goal "[| Invariant prg INV;      \
    9.68 +\        Constrains prg (INV Int (A-A')) (A Un A'); \
    9.69  \        transient  (Acts prg) (INV Int (A-A')) |]   \
    9.70  \ ==> LeadsTo prg A A'";
    9.71 -br invariant_LeadsToI 1;
    9.72 -ba 1;
    9.73 -by (rtac (ensuresI RS LeadsTo_Basis) 1);
    9.74 -by (ALLGOALS 
    9.75 -    (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym, 
    9.76 -					Diff_Int_distrib RS sym])));
    9.77 -be invariantE 1;
    9.78 -by (blast_tac (claset() addSDs [stable_constrains_Int]
    9.79 -			addIs [constrains_weaken]) 1);
    9.80 -qed "invariant_LeadsTo_Basis";
    9.81 +by (rtac Invariant_LeadsToI 1);
    9.82 +by (assume_tac 1);
    9.83 +by (rtac LeadsTo_Basis 1);
    9.84 +by (blast_tac (claset() addIs [transient_strengthen]) 2);
    9.85 +by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
    9.86 +qed "Invariant_LeadsTo_Basis";
    9.87  
    9.88 -Goal "[| invariant prg INV;      \
    9.89 +Goal "[| Invariant prg INV;      \
    9.90  \        LeadsTo prg A A'; id: Acts prg;   \
    9.91  \        INV Int B  <= A;  INV Int A' <= B' |] \
    9.92  \     ==> LeadsTo prg B B'";
    9.93 -br invariant_LeadsToI 1;
    9.94 -ba 1;
    9.95 -bd invariant_LeadsToD 1;
    9.96 -ba 1;
    9.97 +by (rtac Invariant_LeadsToI 1);
    9.98 +by (assume_tac 1);
    9.99 +by (dtac Invariant_LeadsToD 1);
   9.100 +by (assume_tac 1);
   9.101  by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
   9.102 -qed "invariant_LeadsTo_weaken";
   9.103 +qed "Invariant_LeadsTo_weaken";
   9.104  
   9.105  
   9.106  (*Set difference: maybe combine with leadsTo_weaken_L??
   9.107 @@ -250,43 +241,39 @@
   9.108  (** PSP: Progress-Safety-Progress **)
   9.109  
   9.110  (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
   9.111 -Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   9.112 -\     ==> LeadsTo prg (A Int B) (A' Int B)";
   9.113 -by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, 
   9.114 -					   psp_stable]) 1);
   9.115 +Goal
   9.116 +  "[| LeadsTo prg A A';  Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
   9.117 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
   9.118 +by (dtac psp_stable 1);
   9.119 +by (assume_tac 1);
   9.120 +by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
   9.121  qed "PSP_stable";
   9.122  
   9.123 -Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   9.124 +Goal "[| LeadsTo prg A A'; Stable prg B |] \
   9.125  \     ==> LeadsTo prg (B Int A) (B Int A')";
   9.126  by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
   9.127  qed "PSP_stable2";
   9.128  
   9.129 -
   9.130 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   9.131 +Goalw [LeadsTo_def, Constrains_def]
   9.132 +     "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   9.133  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
   9.134 -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   9.135 -by (dtac psp 1);
   9.136 -by (etac constrains_reachable 1);
   9.137 -by (etac leadsTo_weaken 2);
   9.138 -by (ALLGOALS Blast_tac);
   9.139 +by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
   9.140  qed "PSP";
   9.141  
   9.142 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   9.143 +Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   9.144  \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
   9.145  by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
   9.146  qed "PSP2";
   9.147  
   9.148 -Goalw [unless_def]
   9.149 -   "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
   9.150 +Goalw [Unless_def]
   9.151 +     "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
   9.152  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
   9.153  by (dtac PSP 1);
   9.154  by (assume_tac 1);
   9.155 -by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   9.156 -by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   9.157 -by (etac LeadsTo_Diff 2);
   9.158 -by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
   9.159 -by Auto_tac;
   9.160 -qed "PSP_unless";
   9.161 +by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
   9.162 +			       subset_imp_LeadsTo]) 2);
   9.163 +by (assume_tac 1);
   9.164 +qed "PSP_Unless";
   9.165  
   9.166  
   9.167  (*** Induction rules ***)
   9.168 @@ -294,7 +281,7 @@
   9.169  (** Meta or object quantifier ????? **)
   9.170  Goal "[| wf r;     \
   9.171  \        ALL m. LeadsTo prg (A Int f-``{m})                     \
   9.172 -\                                 ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   9.173 +\                           ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   9.174  \        id: Acts prg |] \
   9.175  \     ==> LeadsTo prg A B";
   9.176  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   9.177 @@ -353,49 +340,42 @@
   9.178  
   9.179  (*** Completion: Binary and General Finite versions ***)
   9.180  
   9.181 -Goal "[| LeadsTo prg A A';  stable (Acts prg) A';   \
   9.182 -\        LeadsTo prg B B';  stable (Acts prg) B';  id: Acts prg |] \
   9.183 +Goal "[| LeadsTo prg A A';  Stable prg A';   \
   9.184 +\        LeadsTo prg B B';  Stable prg B';  id: Acts prg |] \
   9.185  \     ==> LeadsTo prg (A Int B) (A' Int B')";
   9.186 -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   9.187 -by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
   9.188 -                        addSIs [stable_Int, stable_reachable]) 1);
   9.189 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
   9.190 +by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
   9.191  qed "Stable_completion";
   9.192  
   9.193  
   9.194 -Goal "[| finite I;  id: Acts prg |]                     \
   9.195 +Goal "[| finite I;  id: Acts prg |]      \
   9.196  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
   9.197 -\         (ALL i:I. stable (Acts prg) (A' i)) -->         \
   9.198 +\         (ALL i:I. Stable prg (A' i)) -->         \
   9.199  \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
   9.200  by (etac finite_induct 1);
   9.201  by (Asm_simp_tac 1);
   9.202 -by (asm_simp_tac 
   9.203 -    (simpset() addsimps [Stable_completion, stable_def, 
   9.204 -			 ball_constrains_INT]) 1);
   9.205 +by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
   9.206  qed_spec_mp "Finite_stable_completion";
   9.207  
   9.208  
   9.209 -Goal "[| LeadsTo prg A (A' Un C);  constrains (Acts prg) A' (A' Un C); \
   9.210 -\        LeadsTo prg B (B' Un C);  constrains (Acts prg) B' (B' Un C); \
   9.211 +Goal "[| LeadsTo prg A (A' Un C);  Constrains prg A' (A' Un C); \
   9.212 +\        LeadsTo prg B (B' Un C);  Constrains prg B' (B' Un C); \
   9.213  \        id: Acts prg |] \
   9.214  \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
   9.215 -by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
   9.216 -by (dtac completion 1);
   9.217 -by (assume_tac 2);
   9.218 -by (ALLGOALS 
   9.219 -    (asm_simp_tac 
   9.220 -     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
   9.221 -by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   9.222 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
   9.223 +				       Int_Un_distrib]) 1);
   9.224 +by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
   9.225  qed "Completion";
   9.226  
   9.227  
   9.228  Goal "[| finite I;  id: Acts prg |] \
   9.229  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) -->  \
   9.230 -\         (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
   9.231 +\         (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
   9.232  \         LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
   9.233  by (etac finite_induct 1);
   9.234  by (ALLGOALS Asm_simp_tac);
   9.235  by (Clarify_tac 1);
   9.236 -by (dtac ball_constrains_INT 1);
   9.237 +by (dtac ball_Constrains_INT 1);
   9.238  by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
   9.239  qed "Finite_completion";
   9.240  
   9.241 @@ -408,22 +388,22 @@
   9.242  (*proves "constrains" properties when the program is specified*)
   9.243  fun constrains_tac (main_def::cmd_defs) = 
   9.244     SELECT_GOAL
   9.245 -      (EVERY [TRY (rtac stableI 1),
   9.246 +      (EVERY [REPEAT (resolve_tac [StableI, stableI,
   9.247 +				   constrains_imp_Constrains] 1),
   9.248  	      rtac constrainsI 1,
   9.249  	      full_simp_tac (simpset() addsimps [main_def]) 1,
   9.250 -	      REPEAT_FIRST (eresolve_tac [disjE]),
   9.251 +	      REPEAT_FIRST (etac disjE ),
   9.252  	      rewrite_goals_tac cmd_defs,
   9.253  	      ALLGOALS (SELECT_GOAL Auto_tac)]);
   9.254  
   9.255  
   9.256 -(*proves "ensures" properties when the program is specified*)
   9.257 +(*proves "ensures/leadsTo" properties when the program is specified*)
   9.258  fun ensures_tac (main_def::cmd_defs) sact = 
   9.259      SELECT_GOAL
   9.260 -      (EVERY [REPEAT (invariant_Int_tac 1),
   9.261 -	      etac invariant_LeadsTo_Basis 1 
   9.262 +      (EVERY [REPEAT (Invariant_Int_tac 1),
   9.263 +	      etac Invariant_LeadsTo_Basis 1 
   9.264  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   9.265 -		  REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, 
   9.266 -				    ensuresI] 1),
   9.267 +		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
   9.268  	      res_inst_tac [("act", sact)] transient_mem 2,
   9.269  	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
   9.270  	      simp_tac (simpset() addsimps [main_def]) 2,
    10.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 13 17:44:50 1998 +0200
    10.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 13 18:06:40 1998 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  LeadsTo relation: restricted to the set of reachable states.
    10.5  *)
    10.6  
    10.7 -SubstAx = WFair + Traces + 
    10.8 +SubstAx = WFair + Constrains + 
    10.9  
   10.10  constdefs
   10.11  
    11.1 --- a/src/HOL/UNITY/Traces.ML	Thu Aug 13 17:44:50 1998 +0200
    11.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Aug 13 18:06:40 1998 +0200
    11.3 @@ -16,59 +16,7 @@
    11.4  by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
    11.5  qed "reachable_equiv_traces";
    11.6  
    11.7 -Goal "stable (Acts prg) (reachable prg)";
    11.8 +Goal "acts <= Acts prg ==> stable acts (reachable prg)";
    11.9  by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
   11.10  qed "stable_reachable";
   11.11  
   11.12 -(*The set of all reachable states is an invariant...*)
   11.13 -Goal "invariant prg (reachable prg)";
   11.14 -by (simp_tac (simpset() addsimps [invariant_def]) 1);
   11.15 -by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
   11.16 -qed "invariant_reachable";
   11.17 -
   11.18 -(*...in fact the strongest invariant!*)
   11.19 -Goal "invariant prg A ==> reachable prg <= A";
   11.20 -by (full_simp_tac 
   11.21 -    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
   11.22 -by (rtac subsetI 1);
   11.23 -by (etac reachable.induct 1);
   11.24 -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   11.25 -qed "invariant_includes_reachable";
   11.26 -
   11.27 -
   11.28 -(** Natural deduction rules for "invariant prg A" **)
   11.29 -
   11.30 -Goal "[| (Init prg)<=A;  stable (Acts prg) A |] ==> invariant prg A";
   11.31 -by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
   11.32 -qed "invariantI";
   11.33 -
   11.34 -Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
   11.35 -by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
   11.36 -qed "invariantD";
   11.37 -
   11.38 -bind_thm ("invariantE", invariantD RS conjE);
   11.39 -
   11.40 -
   11.41 -(** Conjoining invariants **)
   11.42 -
   11.43 -Goal "[| invariant prg A;  invariant prg B |] \
   11.44 -\     ==> invariant prg (A Int B)";
   11.45 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1);
   11.46 -by Auto_tac;
   11.47 -qed "invariant_Int";
   11.48 -
   11.49 -(*Delete the nearest invariance assumption (which will be the second one
   11.50 -  used by invariant_Int) *)
   11.51 -val invariant_thin =
   11.52 -    read_instantiate_sg (sign_of thy)
   11.53 -                [("V", "invariant ?Prg ?A")] thin_rl;
   11.54 -
   11.55 -(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   11.56 -val invariant_Int_tac = dtac invariant_Int THEN' 
   11.57 -                        assume_tac THEN'
   11.58 -			etac invariant_thin;
   11.59 -
   11.60 -(*Combines two invariance THEOREMS into one.*)
   11.61 -val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int);
   11.62 -
   11.63 -
    12.1 --- a/src/HOL/UNITY/Traces.thy	Thu Aug 13 17:44:50 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Traces.thy	Thu Aug 13 18:06:40 1998 +0200
    12.3 @@ -38,8 +38,4 @@
    12.4      Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
    12.5  	   ==> s' : reachable prg"
    12.6  
    12.7 -constdefs
    12.8 -  invariant :: "['a program, 'a set] => bool"
    12.9 -  "invariant prg A == (Init prg) <= A & stable (Acts prg) A"
   12.10 -
   12.11  end
    13.1 --- a/src/HOL/UNITY/UNITY.ML	Thu Aug 13 17:44:50 1998 +0200
    13.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Aug 13 18:06:40 1998 +0200
    13.3 @@ -21,8 +21,7 @@
    13.4  qed "constrainsI";
    13.5  
    13.6  Goalw [constrains_def]
    13.7 -    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] \
    13.8 -\            ==> s': A'";
    13.9 +    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] ==> s': A'";
   13.10  by (Blast_tac 1);
   13.11  qed "constrainsD";
   13.12  
   13.13 @@ -90,8 +89,7 @@
   13.14  by (Blast_tac 1);
   13.15  qed "all_constrains_INT";
   13.16  
   13.17 -Goalw [constrains_def]
   13.18 -    "[| constrains acts A A'; id: acts |] ==> A<=A'";
   13.19 +Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
   13.20  by (Blast_tac 1);
   13.21  qed "constrains_imp_subset";
   13.22  
   13.23 @@ -104,25 +102,21 @@
   13.24  
   13.25  (*** stable ***)
   13.26  
   13.27 -Goalw [stable_def]
   13.28 -    "constrains acts A A ==> stable acts A";
   13.29 +Goalw [stable_def] "constrains acts A A ==> stable acts A";
   13.30  by (assume_tac 1);
   13.31  qed "stableI";
   13.32  
   13.33 -Goalw [stable_def]
   13.34 -    "stable acts A ==> constrains acts A A";
   13.35 +Goalw [stable_def] "stable acts A ==> constrains acts A A";
   13.36  by (assume_tac 1);
   13.37  qed "stableD";
   13.38  
   13.39  Goalw [stable_def]
   13.40 -    "[| stable acts A; stable acts A' |]   \
   13.41 -\    ==> stable acts (A Un A')";
   13.42 +    "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
   13.43  by (blast_tac (claset() addIs [constrains_Un]) 1);
   13.44  qed "stable_Un";
   13.45  
   13.46  Goalw [stable_def]
   13.47 -    "[| stable acts A; stable acts A' |]   \
   13.48 -\    ==> stable acts (A Int A')";
   13.49 +    "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
   13.50  by (blast_tac (claset() addIs [constrains_Int]) 1);
   13.51  qed "stable_Int";
   13.52  
   13.53 @@ -144,15 +138,15 @@
   13.54    in forward proof.*)
   13.55  Goalw [constrains_def]
   13.56      "[| ALL m. constrains acts {s. s x = m} (B m) |] \
   13.57 -\    ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
   13.58 +\    ==> constrains acts {s. s x : M} (UN m:M. B m)";
   13.59  by (Blast_tac 1);
   13.60  qed "elimination";
   13.61  
   13.62 +
   13.63  (*As above, but for the trivial case of a one-variable state, in which the
   13.64    state is identified with its one variable.*)
   13.65  Goalw [constrains_def]
   13.66 -    "[| ALL m. constrains acts {m} (B m) |] \
   13.67 -\    ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
   13.68 +    "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
   13.69  by (Blast_tac 1);
   13.70  qed "elimination_sing";
   13.71  
    14.1 --- a/src/HOL/UNITY/Union.ML	Thu Aug 13 17:44:50 1998 +0200
    14.2 +++ b/src/HOL/UNITY/Union.ML	Thu Aug 13 18:06:40 1998 +0200
    14.3 @@ -11,133 +11,35 @@
    14.4      Maybe Join instead of Un, and JOIN for UNION
    14.5  *)
    14.6  
    14.7 -(*** Safety: constrains, stable, FP ***)
    14.8 -
    14.9 -Goalw [constrains_def]
   14.10 -    "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
   14.11 -by (Blast_tac 1);
   14.12 -qed "constrains_UN";
   14.13 -
   14.14 -Goalw [constrains_def]
   14.15 -    "constrains (actsF Un actsG) A B =  \
   14.16 -\    (constrains actsF A B & constrains actsG A B)";
   14.17 -by (simp_tac (simpset() addsimps [ball_Un]) 1);
   14.18 -qed "constrains_Un";
   14.19 -
   14.20 -(*Provable by constrains_Un and constrains_weaken, but why bother?*)
   14.21 -Goalw [constrains_def]
   14.22 -     "[| constrains actsF A A';  constrains actsG B B' |] \
   14.23 -\     ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
   14.24 -by (Blast_tac 1);
   14.25 -qed "constrains_Un_weaken";
   14.26  
   14.27 -Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
   14.28 -by (simp_tac (simpset() addsimps [constrains_UN]) 1);
   14.29 -qed "stable_UN";
   14.30 -
   14.31 -Goalw [stable_def]
   14.32 -    "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
   14.33 -by (simp_tac (simpset() addsimps [constrains_Un]) 1);
   14.34 -qed "stable_Un";
   14.35 +Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
   14.36 +by (simp_tac (simpset() addsimps [Join_def]) 1);
   14.37 +qed "Init_Join";
   14.38  
   14.39 -Goal "stable (Acts (Join prgF prgG)) A = \
   14.40 -\     (stable (Acts prgF) A & stable (Acts prgG) A)";
   14.41 -by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
   14.42 -qed "stable_Join";
   14.43 -
   14.44 -Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
   14.45 -by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
   14.46 -qed "FP_UN";
   14.47 -
   14.48 -
   14.49 -(*** Progress: transient, ensures ***)
   14.50 -
   14.51 -Goalw [transient_def]
   14.52 -    "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
   14.53 -by (Simp_tac 1);
   14.54 -qed "transient_UN";
   14.55 +Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
   14.56 +by (simp_tac (simpset() addsimps [Join_def]) 1);
   14.57 +qed "Acts_Join";
   14.58  
   14.59 -Goalw [ensures_def,transient_def]
   14.60 -    "ensures (UN i:I. acts i) A B = \
   14.61 -\    ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
   14.62 -\     (EX i:I. ensures (acts i) A B))";
   14.63 -by (simp_tac (simpset() addsimps [constrains_UN]) 1);
   14.64 -by Auto_tac;
   14.65 -qed "ensures_UN";
   14.66 -
   14.67 -(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
   14.68 -Goal "ensures (actsF Un actsG) A B =     \
   14.69 -\     (constrains actsF (A-B) (A Un B) & \
   14.70 -\      constrains actsG (A-B) (A Un B) & \
   14.71 -\      (ensures actsF A B | ensures actsG A B))";
   14.72 -by (simp_tac (simpset() addcongs [conj_cong]
   14.73 -			addsimps [ensures_UN, Un_eq_UN,
   14.74 -				  all_bool_eq, ex_bool_eq]) 1);
   14.75 -qed "ensures_Un";
   14.76 -
   14.77 -(*Or a longer proof via constrains_imp_subset*)
   14.78 -Goalw [stable_def, constrains_def]
   14.79 -     "[| stable actsF A;  constrains actsG A A';  id: actsG |] \
   14.80 -\     ==> constrains (actsF Un actsG) A A'";
   14.81 -by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
   14.82 -by (Blast_tac 1);
   14.83 -qed "stable_constrains_Un";
   14.84 +Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
   14.85 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   14.86 +qed "Init_JN";
   14.87  
   14.88 -Goalw [Join_def]
   14.89 -      "[| stable (Acts prgF) A;  invariant prgG A |]     \
   14.90 -\      ==> invariant (Join prgF prgG) A";
   14.91 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
   14.92 -by (Blast_tac 1);
   14.93 -qed "stable_Join_invariant";
   14.94 -
   14.95 -Goal "[| stable actsF A;  ensures actsG A B |]     \
   14.96 -\     ==> ensures (actsF Un actsG) A B";
   14.97 -by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
   14.98 -by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
   14.99 -by (etac constrains_weaken 1);
  14.100 -by Auto_tac;
  14.101 -qed "ensures_stable_Un1";
  14.102 +Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
  14.103 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
  14.104 +qed "Acts_JN";
  14.105  
  14.106 -Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
  14.107 -\     ==> ensures (Acts (Join prgF prgG)) A B";
  14.108 -by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
  14.109 -qed "ensures_stable_Join1";
  14.110 -
  14.111 -(*As above, but exchanging the roles of F and G*)
  14.112 -Goal "[| ensures actsF A B;  stable actsG A |]     \
  14.113 -\     ==> ensures (actsF Un actsG) A B";
  14.114 -by (stac Un_commute 1);
  14.115 -by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
  14.116 -qed "ensures_stable_Un2";
  14.117 -
  14.118 -Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
  14.119 -\     ==> ensures (Acts (Join prgF prgG)) A B";
  14.120 -by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
  14.121 -qed "ensures_stable_Join2";
  14.122 -
  14.123 +Addsimps [Init_Join, Init_JN];
  14.124  
  14.125  (** Theoretical issues **)
  14.126  
  14.127 -Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
  14.128 -by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
  14.129 +Goal "Join prgF prgG = Join prgG prgF";
  14.130 +by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
  14.131  qed "Join_commute";
  14.132  
  14.133 -Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
  14.134 -by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
  14.135 +Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
  14.136 +by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
  14.137  qed "Join_assoc";
  14.138  
  14.139 -(**NOT PROVABLE because no "surjective pairing" for records
  14.140 -Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
  14.141 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
  14.142 -qed "Join_Null";
  14.143 -*)
  14.144 -
  14.145 -(**NOT PROVABLE because no "surjective pairing" for records
  14.146 -Goalw [Join_def] "Join prgF prgF = prgF";
  14.147 -auto();
  14.148 -qed "Join_absorb";
  14.149 -*)
  14.150 -
  14.151  
  14.152  (*
  14.153  val field_defs = thms"program.field_defs";
  14.154 @@ -149,3 +51,124 @@
  14.155  val update_convs = thms"program.update_convs";
  14.156  val simps = thms"program.simps";
  14.157  *)
  14.158 +
  14.159 +
  14.160 +(**NOT PROVABLE because no "surjective pairing" for records
  14.161 +Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
  14.162 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
  14.163 +qed "Join_Null";
  14.164 +*)
  14.165 +
  14.166 +(**NOT PROVABLE because no "surjective pairing" for records
  14.167 +Goalw [Join_def] "Join prgF prgF = prgF";
  14.168 +by Auto_tac;
  14.169 +qed "Join_absorb";
  14.170 +*)
  14.171 +
  14.172 +
  14.173 +
  14.174 +(*** Safety: constrains, stable, FP ***)
  14.175 +
  14.176 +Goalw [constrains_def, JOIN_def]
  14.177 +    "constrains (Acts (JN i:I. prg i)) A B = \
  14.178 +\    (ALL i:I. constrains (Acts (prg i)) A B)";
  14.179 +by Auto_tac;
  14.180 +qed "constrains_JN";
  14.181 +
  14.182 +(**FAILS, I think; see 5.4.1, Substitution Axiom.
  14.183 +Goalw [Constrains_def]
  14.184 +    "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
  14.185 +by (simp_tac (simpset() addsimps [constrains_JN]) 1);
  14.186 +by (Blast_tac 1);
  14.187 +qed "Constrains_JN";
  14.188 +**)
  14.189 +
  14.190 +Goalw [constrains_def, Join_def]
  14.191 +    "constrains (Acts (Join prgF prgG)) A B =  \
  14.192 +\    (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
  14.193 +by (simp_tac (simpset() addsimps [ball_Un]) 1);
  14.194 +qed "constrains_Join";
  14.195 +
  14.196 +Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
  14.197 +\     ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
  14.198 +by (simp_tac (simpset() addsimps [constrains_Join]) 1);
  14.199 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
  14.200 +qed "constrains_Join_weaken";
  14.201 +
  14.202 +Goalw [stable_def] 
  14.203 +    "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
  14.204 +by (simp_tac (simpset() addsimps [constrains_JN]) 1);
  14.205 +qed "stable_JN";
  14.206 +
  14.207 +Goal "stable (Acts (Join prgF prgG)) A = \
  14.208 +\     (stable (Acts prgF) A & stable (Acts prgG) A)";
  14.209 +by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  14.210 +qed "stable_Join";
  14.211 +
  14.212 +Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
  14.213 +by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
  14.214 +qed "FP_JN";
  14.215 +
  14.216 +
  14.217 +(*** Progress: transient, ensures ***)
  14.218 +
  14.219 +Goalw [transient_def, JOIN_def]
  14.220 +   "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
  14.221 +by (Simp_tac 1);
  14.222 +qed "transient_JN";
  14.223 +
  14.224 +Goalw [transient_def, Join_def]
  14.225 +   "transient (Acts (Join prgF prgG)) A = \
  14.226 +\   (transient (Acts prgF) A | transient (Acts prgG) A)";
  14.227 +by (simp_tac (simpset() addsimps [bex_Un]) 1);
  14.228 +qed "transient_Join";
  14.229 +
  14.230 +Goalw [ensures_def]
  14.231 +    "ensures (Acts (JN i:I. prg i)) A B = \
  14.232 +\    ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
  14.233 +\     (EX i:I. ensures (Acts (prg i)) A B))";
  14.234 +by (auto_tac (claset(),
  14.235 +	      simpset() addsimps [constrains_JN, transient_JN]));
  14.236 +qed "ensures_JN";
  14.237 +
  14.238 +Goalw [ensures_def]
  14.239 +     "ensures (Acts (Join prgF prgG)) A B =     \
  14.240 +\     (constrains (Acts prgF) (A-B) (A Un B) & \
  14.241 +\      constrains (Acts prgG) (A-B) (A Un B) & \
  14.242 +\      (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
  14.243 +by (auto_tac (claset(),
  14.244 +	      simpset() addsimps [constrains_Join, transient_Join]));
  14.245 +qed "ensures_Join";
  14.246 +
  14.247 +Goalw [stable_def, constrains_def, Join_def]
  14.248 +    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  id: Acts prgG |] \
  14.249 +\    ==> constrains (Acts (Join prgF prgG)) A A'";
  14.250 +by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
  14.251 +by (Blast_tac 1);
  14.252 +qed "stable_constrains_Join";
  14.253 +
  14.254 +(*Premises cannot use Invariant because  Stable prgF A  is weaker than
  14.255 +  stable (Acts prgG) A *)
  14.256 +Goal  "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
  14.257 +\      ==> Invariant (Join prgF prgG) A";
  14.258 +by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
  14.259 +				  stable_Join]) 1);
  14.260 +by (force_tac(claset() addIs [stable_reachable, stable_Int],
  14.261 +	      simpset() addsimps [Acts_Join]) 1);
  14.262 +qed "stable_Join_Invariant";
  14.263 +
  14.264 +Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
  14.265 +\     ==> ensures (Acts (Join prgF prgG)) A B";
  14.266 +by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
  14.267 +by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
  14.268 +by (etac constrains_weaken 1);
  14.269 +by Auto_tac;
  14.270 +qed "ensures_stable_Join1";
  14.271 +
  14.272 +(*As above, but exchanging the roles of F and G*)
  14.273 +Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
  14.274 +\     ==> ensures (Acts (Join prgF prgG)) A B";
  14.275 +by (stac Join_commute 1);
  14.276 +by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
  14.277 +qed "ensures_stable_Join2";
  14.278 +
    15.1 --- a/src/HOL/UNITY/Union.thy	Thu Aug 13 17:44:50 1998 +0200
    15.2 +++ b/src/HOL/UNITY/Union.thy	Thu Aug 13 18:06:40 1998 +0200
    15.3 @@ -11,6 +11,9 @@
    15.4  Union = SubstAx + FP +
    15.5  
    15.6  constdefs
    15.7 +   JOIN  :: ['a set, 'a => 'b program] => 'b program
    15.8 +    "JOIN I prg == (|Init = INT i:I. Init (prg i),
    15.9 +	           Acts = UN  i:I. Acts (prg i)|)"
   15.10  
   15.11     Join :: ['a program, 'a program] => 'a program
   15.12      "Join prgF prgG == (|Init = Init prgF Int Init prgG,
   15.13 @@ -19,4 +22,10 @@
   15.14     Null :: 'a program
   15.15      "Null == (|Init = UNIV, Acts = {id}|)"
   15.16  
   15.17 +syntax
   15.18 +  "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
   15.19 +
   15.20 +translations
   15.21 +  "JN x:A. B"   == "JOIN A (%x. B)"
   15.22 +
   15.23  end