made many specification operators infix
authorpaulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536281d44905cab
parent 6535 880f31a62784
child 6537 b1288c5e599c
made many specification operators infix
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Channel.thy
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Deadlock.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/Network.ML
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Token.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/Channel.ML	Wed Apr 28 13:36:31 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Thu Apr 29 10:51:58 1999 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed_spec_mp "minSet_nonempty";
     1.6  
     1.7 -Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
     1.8 +Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
     1.9  by (rtac leadsTo_weaken 1);
    1.10  by (rtac ([UC2, UC1] MRS psp) 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12 @@ -36,7 +36,7 @@
    1.13  
    1.14  
    1.15  (*The induction*)
    1.16 -Goal "F : leadsTo (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
    1.17 +Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))";
    1.18  by (rtac leadsTo_weaken_R 1);
    1.19  by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
    1.20       greaterThan_bounded_induct 1);
    1.21 @@ -52,7 +52,7 @@
    1.22  val lemma = result();
    1.23  
    1.24  
    1.25 -Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {s. y ~: s}";
    1.26 +Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
    1.27  by (rtac (lemma RS leadsTo_weaken_R) 1);
    1.28  by (Clarify_tac 1);
    1.29  by (forward_tac [minSet_nonempty] 1);
     2.1 --- a/src/HOL/UNITY/Channel.thy	Wed Apr 28 13:36:31 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Channel.thy	Thu Apr 29 10:51:58 1999 +0200
     2.3 @@ -21,10 +21,10 @@
     2.4  
     2.5  rules
     2.6  
     2.7 -  UC1  "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
     2.8 +  UC1  "F : (minSet -`` {Some x}) co (minSet -`` (Some``atLeast x))"
     2.9  
    2.10 -  (*  UC1  "F : constrains {s. minSet s = x} {s. x <= minSet s}"  *)
    2.11 +  (*  UC1  "F : {s. minSet s = x} co {s. x <= minSet s}"  *)
    2.12  
    2.13 -  UC2  "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
    2.14 +  UC2  "F : (minSet -`` {Some x}) leadsTo {s. x ~: s}"
    2.15  
    2.16  end
     3.1 --- a/src/HOL/UNITY/Client.ML	Wed Apr 28 13:36:31 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Client.ML	Thu Apr 29 10:51:58 1999 +0200
     3.3 @@ -124,8 +124,7 @@
     3.4  Goal "Cli_prg : \
     3.5  \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
     3.6  \                 Int Invariant giv_meets_ask) \
     3.7 -\      guarantees (LeadsTo {s. k < size (giv s)}    \
     3.8 -\                          {s. k < size (rel s)})";
     3.9 +\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
    3.10  by (rtac guaranteesI 1);
    3.11  by (Clarify_tac 1);
    3.12  by (rtac Stable_transient_reachable_LeadsTo 1);
     4.1 --- a/src/HOL/UNITY/Common.ML	Wed Apr 28 13:36:31 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Common.ML	Thu Apr 29 10:51:58 1999 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  *)
     4.5  
     4.6  (*Misra's property CMT4: t exceeds no common meeting time*)
     4.7 -Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
     4.8 +Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \
     4.9  \     ==> F : Stable (atMost n)";
    4.10  by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    4.11  by (asm_full_simp_tac
    4.12 @@ -22,7 +22,7 @@
    4.13  qed "common_stable";
    4.14  
    4.15  Goal "[| Init F <= atMost n;  \
    4.16 -\        ALL m. F : Constrains {m} (maxfg m); n: common |] \
    4.17 +\        ALL m. F : {m} Co (maxfg m); n: common |] \
    4.18  \     ==> F : Invariant (atMost n)";
    4.19  by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
    4.20  qed "common_Invariant";
    4.21 @@ -30,14 +30,14 @@
    4.22  
    4.23  (*** Some programs that implement the safety property above ***)
    4.24  
    4.25 -Goal "SKIP : constrains {m} (maxfg m)";
    4.26 +Goal "SKIP : {m} co (maxfg m)";
    4.27  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    4.28  				  fasc]) 1);
    4.29  result();
    4.30  
    4.31  (*This one is  t := ftime t || t := gtime t*)
    4.32  Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
    4.33 -\      : constrains {m} (maxfg m)";
    4.34 +\      : {m} co (maxfg m)";
    4.35  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    4.36  				  le_max_iff_disj, fasc]) 1);
    4.37  by (Blast_tac 1);
    4.38 @@ -45,7 +45,7 @@
    4.39  
    4.40  (*This one is  t := max (ftime t) (gtime t)*)
    4.41  Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
    4.42 -\      : constrains {m} (maxfg m)";
    4.43 +\      : {m} co (maxfg m)";
    4.44  by (simp_tac 
    4.45      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    4.46  by (Blast_tac 1);
    4.47 @@ -53,7 +53,7 @@
    4.48  
    4.49  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    4.50  Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    4.51 -\      : constrains {m} (maxfg m)";
    4.52 +\      : {m} co (maxfg m)";
    4.53  by (simp_tac 
    4.54      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    4.55  by (blast_tac (claset() addIs [Suc_leI]) 1);
    4.56 @@ -68,10 +68,10 @@
    4.57  
    4.58  Addsimps [atMost_Int_atLeast];
    4.59  
    4.60 -Goal "[| ALL m. F : Constrains {m} (maxfg m); \
    4.61 -\               ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
    4.62 +Goal "[| ALL m. F : {m} Co (maxfg m); \
    4.63 +\               ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
    4.64  \               n: common |]  \
    4.65 -\     ==> F : LeadsTo (atMost n) common";
    4.66 +\     ==> F : (atMost n) LeadsTo common";
    4.67  by (rtac LeadsTo_weaken_R 1);
    4.68  by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    4.69  by (ALLGOALS Asm_simp_tac);
    4.70 @@ -81,10 +81,10 @@
    4.71  val lemma = result();
    4.72  
    4.73  (*The "ALL m: -common" form echoes CMT6.*)
    4.74 -Goal "[| ALL m. F : Constrains {m} (maxfg m); \
    4.75 -\               ALL m: -common. F : LeadsTo {m} (greaterThan m); \
    4.76 +Goal "[| ALL m. F : {m} Co (maxfg m); \
    4.77 +\               ALL m: -common. F : {m} LeadsTo (greaterThan m); \
    4.78  \               n: common |]  \
    4.79 -\            ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
    4.80 +\            ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
    4.81  by (rtac lemma 1);
    4.82  by (ALLGOALS Asm_simp_tac);
    4.83  by (etac LeastI 2);
     5.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Apr 28 13:36:31 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Constrains.ML	Thu Apr 29 10:51:58 1999 +0200
     5.3 @@ -41,18 +41,17 @@
     5.4  qed "invariant_includes_reachable";
     5.5  
     5.6  
     5.7 -(*** Constrains ***)
     5.8 +(*** Co ***)
     5.9  
    5.10 -overload_1st_set "Constrains.Constrains";
    5.11 +overload_1st_set "Constrains.op Co";
    5.12  
    5.13 -(*F : constrains B B'
    5.14 -  ==> F : constrains (reachable F Int B) (reachable F Int B')*)
    5.15 +(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
    5.16  bind_thm ("constrains_reachable_Int",
    5.17  	  subset_refl RS
    5.18  	  rewrite_rule [stable_def] stable_reachable RS 
    5.19  	  constrains_Int);
    5.20  
    5.21 -Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'";
    5.22 +Goalw [Constrains_def] "F : A co A' ==> F : A Co A'";
    5.23  by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
    5.24  qed "constrains_imp_Constrains";
    5.25  
    5.26 @@ -62,46 +61,46 @@
    5.27  
    5.28  val prems = Goal
    5.29      "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
    5.30 -\    ==> F : Constrains A A'";
    5.31 +\    ==> F : A Co A'";
    5.32  by (rtac constrains_imp_Constrains 1);
    5.33  by (blast_tac (claset() addIs (constrainsI::prems)) 1);
    5.34  qed "ConstrainsI";
    5.35  
    5.36 -Goalw [Constrains_def, constrains_def] "F : Constrains {} B";
    5.37 +Goalw [Constrains_def, constrains_def] "F : {} Co B";
    5.38  by (Blast_tac 1);
    5.39  qed "Constrains_empty";
    5.40  
    5.41 -Goal "F : Constrains A UNIV";
    5.42 +Goal "F : A Co UNIV";
    5.43  by (blast_tac (claset() addIs [ConstrainsI]) 1);
    5.44  qed "Constrains_UNIV";
    5.45  AddIffs [Constrains_empty, Constrains_UNIV];
    5.46  
    5.47  
    5.48  Goalw [Constrains_def]
    5.49 -    "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'";
    5.50 +    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
    5.51  by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
    5.52  qed "Constrains_weaken_R";
    5.53  
    5.54  Goalw [Constrains_def]
    5.55 -    "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'";
    5.56 +    "[| F : A Co A'; B<=A |] ==> F : B Co A'";
    5.57  by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
    5.58  qed "Constrains_weaken_L";
    5.59  
    5.60  Goalw [Constrains_def]
    5.61 -   "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'";
    5.62 +   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
    5.63  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    5.64  qed "Constrains_weaken";
    5.65  
    5.66  (** Union **)
    5.67  
    5.68  Goalw [Constrains_def]
    5.69 -    "[| F : Constrains A A'; F : Constrains B B' |]   \
    5.70 -\    ==> F : Constrains (A Un B) (A' Un B')";
    5.71 +    "[| F : A Co A'; F : B Co B' |]   \
    5.72 +\    ==> F : (A Un B) Co (A' Un B')";
    5.73  by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
    5.74  qed "Constrains_Un";
    5.75  
    5.76 -Goal "ALL i:I. F : Constrains (A i) (A' i) \
    5.77 -\     ==> F : Constrains (UN i:I. A i) (UN i:I. A' i)";
    5.78 +Goal "ALL i:I. F : (A i) Co (A' i) \
    5.79 +\     ==> F : (UN i:I. A i) Co (UN i:I. A' i)";
    5.80  by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
    5.81  by (dtac ball_constrains_UN 1);
    5.82  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    5.83 @@ -110,20 +109,20 @@
    5.84  (** Intersection **)
    5.85  
    5.86  Goalw [Constrains_def]
    5.87 -    "[| F : Constrains A A'; F : Constrains B B' |]   \
    5.88 -\    ==> F : Constrains (A Int B) (A' Int B')";
    5.89 +    "[| F : A Co A'; F : B Co B' |]   \
    5.90 +\    ==> F : (A Int B) Co (A' Int B')";
    5.91  by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
    5.92  qed "Constrains_Int";
    5.93  
    5.94 -Goal "ALL i:I. F : Constrains (A i) (A' i)   \
    5.95 -\     ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)";
    5.96 +Goal "ALL i:I. F : (A i) Co (A' i)   \
    5.97 +\     ==> F : (INT i:I. A i) Co (INT i:I. A' i)";
    5.98  by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
    5.99  by (dtac ball_constrains_INT 1);
   5.100  by (dtac constrains_reachable_Int 1);
   5.101  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   5.102  qed "ball_Constrains_INT";
   5.103  
   5.104 -Goal "F : Constrains A A' ==> reachable F Int A <= A'";
   5.105 +Goal "F : A Co A' ==> reachable F Int A <= A'";
   5.106  by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
   5.107  by (dtac constrains_imp_subset 1);
   5.108  by (ALLGOALS
   5.109 @@ -131,14 +130,14 @@
   5.110  qed "Constrains_imp_subset";
   5.111  
   5.112  Goalw [Constrains_def]
   5.113 -    "[| F : Constrains A B; F : Constrains B C |]   \
   5.114 -\    ==> F : Constrains A C";
   5.115 +    "[| F : A Co B; F : B Co C |]   \
   5.116 +\    ==> F : A Co C";
   5.117  by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
   5.118  qed "Constrains_trans";
   5.119  
   5.120  Goalw [Constrains_def, constrains_def]
   5.121 -   "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
   5.122 -\   ==> F : Constrains A (A' Un B')";
   5.123 +   "[| F : A Co (A' Un B); F : B Co B' |] \
   5.124 +\   ==> F : A Co (A' Un B')";
   5.125  by (Clarify_tac 1);
   5.126  by (Blast_tac 1);
   5.127  qed "Constrains_cancel";
   5.128 @@ -150,11 +149,11 @@
   5.129  by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
   5.130  qed "Stable_eq_stable";
   5.131  
   5.132 -Goalw [Stable_def] "F : Constrains A A ==> F : Stable A";
   5.133 +Goalw [Stable_def] "F : A Co A ==> F : Stable A";
   5.134  by (assume_tac 1);
   5.135  qed "StableI";
   5.136  
   5.137 -Goalw [Stable_def] "F : Stable A ==> F : Constrains A A";
   5.138 +Goalw [Stable_def] "F : Stable A ==> F : A Co A";
   5.139  by (assume_tac 1);
   5.140  qed "StableD";
   5.141  
   5.142 @@ -169,14 +168,14 @@
   5.143  qed "Stable_Int";
   5.144  
   5.145  Goalw [Stable_def]
   5.146 -    "[| F : Stable C; F : Constrains A (C Un A') |]   \
   5.147 -\    ==> F : Constrains (C Un A) (C Un A')";
   5.148 +    "[| F : Stable C; F : A Co (C Un A') |]   \
   5.149 +\    ==> F : (C Un A) Co (C Un A')";
   5.150  by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
   5.151  qed "Stable_Constrains_Un";
   5.152  
   5.153  Goalw [Stable_def]
   5.154 -    "[| F : Stable C; F : Constrains (C Int A) A' |]   \
   5.155 -\    ==> F : Constrains (C Int A) (C Int A')";
   5.156 +    "[| F : Stable C; F : (C Int A) Co A' |]   \
   5.157 +\    ==> F : (C Int A) Co (C Int A')";
   5.158  by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
   5.159  qed "Stable_Constrains_Int";
   5.160  
   5.161 @@ -222,15 +221,15 @@
   5.162       in forward proof. ***)
   5.163  
   5.164  Goalw [Constrains_def, constrains_def]
   5.165 -    "[| ALL m. F : Constrains {s. s x = m} (B m) |] \
   5.166 -\    ==> F : Constrains {s. s x : M} (UN m:M. B m)";
   5.167 +    "[| ALL m. F : {s. s x = m} Co (B m) |] \
   5.168 +\    ==> F : {s. s x : M} Co (UN m:M. B m)";
   5.169  by (Blast_tac 1);
   5.170  qed "Elimination";
   5.171  
   5.172  (*As above, but for the trivial case of a one-variable state, in which the
   5.173    state is identified with its one variable.*)
   5.174  Goalw [Constrains_def, constrains_def]
   5.175 -    "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)";
   5.176 +    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)";
   5.177  by (Blast_tac 1);
   5.178  qed "Elimination_sing";
   5.179  
   5.180 @@ -286,21 +285,21 @@
   5.181  qed "Invariant_eq_UN_invariant";
   5.182  
   5.183  
   5.184 -(*** "Constrains" rules involving Invariant ***)
   5.185 +(*** "Co" rules involving Invariant ***)
   5.186  
   5.187 -Goal "[| F : Invariant INV;  F : Constrains (INV Int A) A' |]   \
   5.188 -\     ==> F : Constrains A A'";
   5.189 +Goal "[| F : Invariant INV;  F : (INV Int A) Co A' |]   \
   5.190 +\     ==> F : A Co A'";
   5.191  by (asm_full_simp_tac
   5.192      (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
   5.193  			 Constrains_def, Int_assoc RS sym]) 1);
   5.194  qed "Invariant_ConstrainsI";
   5.195  
   5.196 -(* [| F : Invariant INV; F : Constrains (INV Int A) A |]
   5.197 +(* [| F : Invariant INV; F : (INV Int A) Co A |]
   5.198     ==> F : Stable A *)
   5.199  bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
   5.200  
   5.201 -Goal "[| F : Invariant INV;  F : Constrains A A' |]   \
   5.202 -\     ==> F : Constrains A (INV Int A')";
   5.203 +Goal "[| F : Invariant INV;  F : A Co A' |]   \
   5.204 +\     ==> F : A Co (INV Int A')";
   5.205  by (asm_full_simp_tac
   5.206      (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
   5.207  			 Constrains_def, Int_assoc RS sym]) 1);
   5.208 @@ -334,7 +333,7 @@
   5.209  (*To allow expansion of the program's definition when appropriate*)
   5.210  val program_defs_ref = ref ([] : thm list);
   5.211  
   5.212 -(*proves "constrains" properties when the program is specified*)
   5.213 +(*proves "co" properties when the program is specified*)
   5.214  fun constrains_tac i = 
   5.215     SELECT_GOAL
   5.216        (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
     6.1 --- a/src/HOL/UNITY/Constrains.thy	Wed Apr 28 13:36:31 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Constrains.thy	Thu Apr 29 10:51:58 1999 +0200
     6.3 @@ -31,17 +31,20 @@
     6.4      Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
     6.5  	   ==> s' : reachable F"
     6.6  
     6.7 +consts
     6.8 +  Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
     6.9 +
    6.10 +defs
    6.11 +  Constrains_def
    6.12 +    "A Co B == {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
    6.13 +
    6.14 +  Unless_def
    6.15 +    "A Unless B == (A-B) Co (A Un B)"
    6.16 +
    6.17  constdefs
    6.18  
    6.19 -  Constrains :: "['a set, 'a set] => 'a program set"
    6.20 -    "Constrains A B == {F. F : constrains (reachable F  Int  A)
    6.21 -  		                          (reachable F  Int  B)}"
    6.22 -
    6.23    Stable     :: "'a set => 'a program set"
    6.24 -    "Stable A == Constrains A A"
    6.25 -
    6.26 -  Unless :: "['a set, 'a set] => 'a program set"
    6.27 -    "Unless A B == Constrains (A-B) (A Un B)"
    6.28 +    "Stable A == A Co A"
    6.29  
    6.30    Invariant :: "'a set => 'a program set"
    6.31      "Invariant A == {F. Init F <= A} Int Stable A"
     7.1 --- a/src/HOL/UNITY/Deadlock.ML	Wed Apr 28 13:36:31 1999 +0200
     7.2 +++ b/src/HOL/UNITY/Deadlock.ML	Thu Apr 29 10:51:58 1999 +0200
     7.3 @@ -9,7 +9,7 @@
     7.4  
     7.5  (*Trivial, two-process case*)
     7.6  Goalw [constrains_def, stable_def]
     7.7 -    "[| F : constrains (A Int B) A;  F : constrains (B Int A) B |] \
     7.8 +    "[| F : (A Int B) co A;  F : (B Int A) co B |] \
     7.9  \    ==> F : stable (A Int B)";
    7.10  by (Blast_tac 1);
    7.11  result();
    7.12 @@ -69,9 +69,9 @@
    7.13  
    7.14  (*The final deadlock example*)
    7.15  val [zeroprem, allprem] = goalw thy [stable_def]
    7.16 -    "[| F : constrains (A 0 Int A (Suc n)) (A 0);  \
    7.17 -\       ALL i: atMost n. F : constrains (A(Suc i) Int A i) \
    7.18 -\                                         (-A i Un A(Suc i)) |] \
    7.19 +    "[| F : (A 0 Int A (Suc n)) co (A 0);  \
    7.20 +\       ALL i: atMost n. F : (A(Suc i) Int A i) co \
    7.21 +\                            (-A i Un A(Suc i)) |] \
    7.22  \    ==> F : stable (INT i: atMost (Suc n). A i)";
    7.23  
    7.24  by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
     8.1 --- a/src/HOL/UNITY/Extend.ML	Wed Apr 28 13:36:31 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Extend.ML	Thu Apr 29 10:51:58 1999 +0200
     8.3 @@ -172,10 +172,10 @@
     8.4  Addsimps [extend_Join];
     8.5  
     8.6  
     8.7 -(*** Safety: constrains, stable ***)
     8.8 +(*** Safety: co, stable ***)
     8.9  
    8.10 -Goal "(extend h F : constrains (extend_set h A) (extend_set h B)) = \
    8.11 -\     (F : constrains A B)";
    8.12 +Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
    8.13 +\     (F : A co B)";
    8.14  by (simp_tac (simpset() addsimps [constrains_def]) 1);
    8.15  qed "extend_constrains";
    8.16  
    8.17 @@ -187,7 +187,7 @@
    8.18  by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
    8.19  qed "extend_invariant";
    8.20  
    8.21 -(** Substitution Axiom versions: Constrains, Stable **)
    8.22 +(** Substitution Axiom versions: Co, Stable **)
    8.23  
    8.24  Goal "p : reachable (extend h F) ==> f p : reachable F";
    8.25  by (etac reachable.induct 1);
    8.26 @@ -212,8 +212,8 @@
    8.27  			 simpset())));
    8.28  qed "reachable_extend_eq";
    8.29  
    8.30 -Goal "(extend h F : Constrains (extend_set h A) (extend_set h B)) =  \
    8.31 -\     (F : Constrains A B)";
    8.32 +Goal "(extend h F : (extend_set h A) Co (extend_set h B)) =  \
    8.33 +\     (F : A Co B)";
    8.34  by (simp_tac
    8.35      (simpset() addsimps [Constrains_def, reachable_extend_eq, 
    8.36  			 extend_constrains, extend_set_Int_distrib RS sym]) 1);
    8.37 @@ -232,16 +232,16 @@
    8.38  				  Domain_extend_act]));
    8.39  qed "extend_transient";
    8.40  
    8.41 -Goal "(extend h F : ensures (extend_set h A) (extend_set h B)) = \
    8.42 -\     (F : ensures A B)";
    8.43 +Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \
    8.44 +\     (F : A ensures B)";
    8.45  by (simp_tac
    8.46      (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
    8.47  			 extend_set_Un_distrib RS sym, 
    8.48  			 extend_set_Diff_distrib RS sym]) 1);
    8.49  qed "extend_ensures";
    8.50  
    8.51 -Goal "F : leadsTo A B \
    8.52 -\     ==> extend h F : leadsTo (extend_set h A) (extend_set h B)";
    8.53 +Goal "F : A leadsTo B \
    8.54 +\     ==> extend h F : (extend_set h A) leadsTo (extend_set h B)";
    8.55  by (etac leadsTo_induct 1);
    8.56  by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
    8.57  by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
    8.58 @@ -272,7 +272,7 @@
    8.59  by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1);
    8.60  qed "extend_transient_slice";
    8.61  
    8.62 -Goal "extend h F : ensures A B ==> F : ensures (slice A y) (f `` B)";
    8.63 +Goal "extend h F : A ensures B ==> F : (slice A y) ensures (f `` B)";
    8.64  by (full_simp_tac
    8.65      (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
    8.66  			 image_Un RS sym,
    8.67 @@ -292,14 +292,14 @@
    8.68  	       simpset() addsimps [slice_def]) 1);
    8.69  qed "extend_ensures_slice";
    8.70  
    8.71 -Goal "ALL y. F : leadsTo (slice B y) CU ==> F : leadsTo (f `` B) CU";
    8.72 +Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (f `` B) leadsTo CU";
    8.73  by (simp_tac (simpset() addsimps [image_is_UN_slice]) 1);
    8.74  by (blast_tac (claset() addIs [leadsTo_UN]) 1);
    8.75  qed "leadsTo_slice_image";
    8.76  
    8.77  
    8.78 -Goal "extend h F : leadsTo AU BU \
    8.79 -\     ==> ALL y. F : leadsTo (slice AU y) (f `` BU)";
    8.80 +Goal "extend h F : AU leadsTo BU \
    8.81 +\     ==> ALL y. F : (slice AU y) leadsTo (f `` BU)";
    8.82  by (etac leadsTo_induct 1);
    8.83  by (full_simp_tac (simpset() addsimps [slice_Union]) 3);
    8.84  by (blast_tac (claset() addIs [leadsTo_UN]) 3);
    8.85 @@ -307,16 +307,16 @@
    8.86  by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1);
    8.87  qed_spec_mp "extend_leadsTo_slice";
    8.88  
    8.89 -Goal "(extend h F : leadsTo (extend_set h A) (extend_set h B)) = \
    8.90 -\     (F : leadsTo A B)";
    8.91 +Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \
    8.92 +\     (F : A leadsTo B)";
    8.93  by Safe_tac;
    8.94  by (etac leadsTo_imp_extend_leadsTo 2);
    8.95  by (dtac extend_leadsTo_slice 1);
    8.96  by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
    8.97  qed "extend_leadsto_eq";
    8.98  
    8.99 -Goal "(extend h F : LeadsTo (extend_set h A) (extend_set h B)) =  \
   8.100 -\     (F : LeadsTo A B)";
   8.101 +Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =  \
   8.102 +\     (F : A LeadsTo B)";
   8.103  by (simp_tac
   8.104      (simpset() addsimps [LeadsTo_def, reachable_extend_eq, 
   8.105  			 extend_leadsto_eq, extend_set_Int_distrib RS sym]) 1);
     9.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Apr 28 13:36:31 1999 +0200
     9.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Apr 29 10:51:58 1999 +0200
     9.3 @@ -31,7 +31,7 @@
     9.4  by (constrains_tac 1);
     9.5  qed "invFG";
     9.6  
     9.7 -Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
     9.8 +Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
     9.9  \                          ({s. NF s = k} Int {s. BB s})";
    9.10  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    9.11  by (ensures_tac "cmdG" 2);
    9.12 @@ -39,7 +39,7 @@
    9.13  by Auto_tac;
    9.14  qed "lemma2_1";
    9.15  
    9.16 -Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    9.17 +Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
    9.18  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    9.19  by (constrains_tac 2);
    9.20  by (ensures_tac "cmdF" 1);
    9.21 @@ -47,12 +47,12 @@
    9.22  qed "lemma2_2";
    9.23  
    9.24  
    9.25 -Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}";
    9.26 +Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
    9.27  by (rtac LeadsTo_weaken_R 1);
    9.28  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    9.29      GreaterThan_bounded_induct 1);
    9.30  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    9.31 -(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*)
    9.32 +(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    9.33  by (rtac LeadsTo_Diff 1);
    9.34  by (rtac lemma2_2 2);
    9.35  by (rtac LeadsTo_Trans 1);
    10.1 --- a/src/HOL/UNITY/Lift.ML	Wed Apr 28 13:36:31 1999 +0200
    10.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Apr 29 10:51:58 1999 +0200
    10.3 @@ -55,7 +55,7 @@
    10.4  
    10.5  
    10.6  val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
    10.7 -(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
    10.8 +(* [| Lprg : B LeadsTo C; Lprg : A LeadsTo B |] ==> Lprg : (A Un B) LeadsTo C *)
    10.9  
   10.10  
   10.11  (*Simplification for records*)
   10.12 @@ -126,24 +126,24 @@
   10.13  
   10.14  (** Lift_1 **)
   10.15  
   10.16 -Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
   10.17 +Goal "Lprg : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
   10.18  by (cut_facts_tac [stop_floor] 1);
   10.19  by (ensures_tac "open_act" 1);
   10.20  qed "E_thm01";  (*lem_lift_1_5*)
   10.21  
   10.22 -Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
   10.23 +Goal "Lprg : (Req n Int stopped - atFloor n) LeadsTo \
   10.24  \                    (Req n Int opened - atFloor n)";
   10.25  by (cut_facts_tac [stop_floor] 1);
   10.26  by (ensures_tac "open_act" 1);
   10.27  qed "E_thm02";  (*lem_lift_1_1*)
   10.28  
   10.29 -Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
   10.30 +Goal "Lprg : (Req n Int opened - atFloor n) LeadsTo \
   10.31  \                    (Req n Int closed - (atFloor n - queueing))";
   10.32  by (ensures_tac "close_act" 1);
   10.33  qed "E_thm03";  (*lem_lift_1_2*)
   10.34  
   10.35 -Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
   10.36 -\                    (opened Int atFloor n)";
   10.37 +Goal "Lprg : (Req n Int closed Int (atFloor n - queueing))  \
   10.38 +\            LeadsTo (opened Int atFloor n)";
   10.39  by (ensures_tac "open_act" 1);
   10.40  qed "E_thm04";  (*lem_lift_1_7*)
   10.41  
   10.42 @@ -166,16 +166,16 @@
   10.43  (*lem_lift_2_0 
   10.44    NOT an ensures property, but a mere inclusion;
   10.45    don't know why script lift_2.uni says ENSURES*)
   10.46 -Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
   10.47 -\                    ((closed Int goingup Int Req n)  Un \
   10.48 +Goal "Lprg : (Req n Int closed - (atFloor n - queueing))   \
   10.49 +\            LeadsTo ((closed Int goingup Int Req n)  Un \
   10.50  \                     (closed Int goingdown Int Req n))";
   10.51  by (rtac subset_imp_LeadsTo 1);
   10.52  by (auto_tac (claset() addSEs [int_neqE], simpset()));
   10.53  qed "E_thm05c";
   10.54  
   10.55  (*lift_2*)
   10.56 -Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
   10.57 -\                    (moving Int Req n)";
   10.58 +Goal "Lprg : (Req n Int closed - (atFloor n - queueing))   \
   10.59 +\            LeadsTo (moving Int Req n)";
   10.60  by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   10.61  by (ensures_tac "req_down" 2);
   10.62  by (ensures_tac "req_up" 1);
   10.63 @@ -188,9 +188,9 @@
   10.64  
   10.65  (*lem_lift_4_1 *)
   10.66  Goal "#0 < N ==> \
   10.67 -\     Lprg : LeadsTo \
   10.68 -\              (moving Int Req n Int {s. metric n s = N} Int \
   10.69 -\               {s. floor s ~: req s} Int {s. up s})   \
   10.70 +\     Lprg : (moving Int Req n Int {s. metric n s = N} Int \
   10.71 +\             {s. floor s ~: req s} Int {s. up s})   \
   10.72 +\            LeadsTo \
   10.73  \              (moving Int Req n Int {s. metric n s < N})";
   10.74  by (cut_facts_tac [moving_up] 1);
   10.75  by (ensures_tac "move_up" 1);
   10.76 @@ -208,10 +208,9 @@
   10.77  
   10.78  (*lem_lift_4_3 *)
   10.79  Goal "#0 < N ==> \
   10.80 -\     Lprg : LeadsTo \
   10.81 -\              (moving Int Req n Int {s. metric n s = N} Int \
   10.82 -\               {s. floor s ~: req s} - {s. up s})   \
   10.83 -\              (moving Int Req n Int {s. metric n s < N})";
   10.84 +\     Lprg : (moving Int Req n Int {s. metric n s = N} Int \
   10.85 +\             {s. floor s ~: req s} - {s. up s})   \
   10.86 +\            LeadsTo (moving Int Req n Int {s. metric n s < N})";
   10.87  by (cut_facts_tac [moving_down] 1);
   10.88  by (ensures_tac "move_down" 1);
   10.89  by Safe_tac;
   10.90 @@ -224,8 +223,8 @@
   10.91  qed "E_thm12b";
   10.92  
   10.93  (*lift_4*)
   10.94 -Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
   10.95 -\                           {s. floor s ~: req s})     \
   10.96 +Goal "#0<N ==> Lprg : (moving Int Req n Int {s. metric n s = N} Int \
   10.97 +\                           {s. floor s ~: req s}) LeadsTo     \
   10.98  \                          (moving Int Req n Int {s. metric n s < N})";
   10.99  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  10.100  by (etac E_thm12b 3);
  10.101 @@ -238,7 +237,7 @@
  10.102  
  10.103  (*lem_lift_5_3*)
  10.104  Goal "#0<N   \
  10.105 -\     ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
  10.106 +\     ==> Lprg : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
  10.107  \                      (moving Int Req n Int {s. metric n s < N})";
  10.108  by (cut_facts_tac [bounded] 1);
  10.109  by (ensures_tac "req_up" 1);
  10.110 @@ -250,7 +249,7 @@
  10.111  
  10.112  (*lem_lift_5_1 has ~goingup instead of goingdown*)
  10.113  Goal "#0<N ==>   \
  10.114 -\     Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
  10.115 +\     Lprg : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
  10.116  \                  (moving Int Req n Int {s. metric n s < N})";
  10.117  by (cut_facts_tac [bounded] 1);
  10.118  by (ensures_tac "req_down" 1);
  10.119 @@ -272,7 +271,7 @@
  10.120  
  10.121  
  10.122  (*lift_5*)
  10.123 -Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N})   \
  10.124 +Goal "#0<N ==> Lprg : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
  10.125  \                          (moving Int Req n Int {s. metric n s < N})";
  10.126  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  10.127  by (etac E_thm16b 3);
  10.128 @@ -295,7 +294,7 @@
  10.129  
  10.130  
  10.131  (*lem_lift_3_1*)
  10.132 -Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0})   \
  10.133 +Goal "Lprg : (moving Int Req n Int {s. metric n s = #0}) LeadsTo   \
  10.134  \                  (stopped Int atFloor n)";
  10.135  by (cut_facts_tac [bounded] 1);
  10.136  by (ensures_tac "request_act" 1);
  10.137 @@ -303,27 +302,26 @@
  10.138  qed "E_thm11";
  10.139  
  10.140  (*lem_lift_3_5*)
  10.141 -Goal "Lprg : LeadsTo \
  10.142 -\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
  10.143 -\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
  10.144 +Goal
  10.145 +  "Lprg : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
  10.146 +\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
  10.147  by (ensures_tac "request_act" 1);
  10.148  by (auto_tac (claset(), simpset() addsimps metric_simps));
  10.149  qed "E_thm13";
  10.150  
  10.151  (*lem_lift_3_6*)
  10.152  Goal "#0 < N ==> \
  10.153 -\     Lprg : LeadsTo \
  10.154 +\     Lprg : \
  10.155  \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
  10.156 -\       (opened Int Req n Int {s. metric n s = N})";
  10.157 +\       LeadsTo (opened Int Req n Int {s. metric n s = N})";
  10.158  by (ensures_tac "open_act" 1);
  10.159  by (REPEAT_FIRST (eresolve_tac mov_metrics));
  10.160  by (auto_tac (claset(), simpset() addsimps metric_simps));
  10.161  qed "E_thm14";
  10.162  
  10.163  (*lem_lift_3_7*)
  10.164 -Goal "Lprg : LeadsTo \
  10.165 -\       (opened Int Req n Int {s. metric n s = N})  \
  10.166 -\       (closed Int Req n Int {s. metric n s = N})";
  10.167 +Goal "Lprg : (opened Int Req n Int {s. metric n s = N})  \
  10.168 +\            LeadsTo (closed Int Req n Int {s. metric n s = N})";
  10.169  by (ensures_tac "close_act" 1);
  10.170  by (auto_tac (claset(), simpset() addsimps metric_simps));
  10.171  qed "E_thm15";
  10.172 @@ -332,9 +330,9 @@
  10.173  (** the final steps **)
  10.174  
  10.175  Goal "#0 < N ==> \
  10.176 -\     Lprg : LeadsTo \
  10.177 +\     Lprg : \
  10.178  \       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
  10.179 -\       (moving Int Req n Int {s. metric n s < N})";
  10.180 +\       LeadsTo (moving Int Req n Int {s. metric n s < N})";
  10.181  by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
  10.182  	                addIs [LeadsTo_Trans]) 1);
  10.183  qed "lift_3_Req";
  10.184 @@ -353,7 +351,7 @@
  10.185  
  10.186  val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
  10.187  
  10.188 -Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
  10.189 +Goal "Lprg : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
  10.190  by (rtac (reach_nonneg RS integ_0_le_induct) 1);
  10.191  by (case_tac "#0 < z" 1);
  10.192  (*If z <= #0 then actually z = #0*)
  10.193 @@ -367,7 +365,7 @@
  10.194  qed "lift_3";
  10.195  
  10.196  
  10.197 -Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
  10.198 +Goal "Lprg : (Req n) LeadsTo (opened Int atFloor n)";
  10.199  by (rtac LeadsTo_Trans 1);
  10.200  by (rtac (E_thm04 RS LeadsTo_Un) 2);
  10.201  by (rtac LeadsTo_Un_post 2);
    11.1 --- a/src/HOL/UNITY/Mutex.ML	Wed Apr 28 13:36:31 1999 +0200
    11.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Apr 29 10:51:58 1999 +0200
    11.3 @@ -74,44 +74,44 @@
    11.4  
    11.5  (*** Progress for U ***)
    11.6  
    11.7 -Goalw [Unless_def] "Mprg : Unless {s. MM s=#2} {s. MM s=#3}";
    11.8 +Goalw [Unless_def] "Mprg : {s. MM s=#2} Unless {s. MM s=#3}";
    11.9  by (constrains_tac 1);
   11.10  qed "U_F0";
   11.11  
   11.12 -Goal "Mprg : LeadsTo {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
   11.13 +Goal "Mprg : {s. MM s=#1} LeadsTo {s. PP s = VV s & MM s = #2}";
   11.14  by (ensures_tac "cmd1U" 1);
   11.15  qed "U_F1";
   11.16  
   11.17 -Goal "Mprg : LeadsTo {s. ~ PP s & MM s = #2} {s. MM s = #3}";
   11.18 +Goal "Mprg : {s. ~ PP s & MM s = #2} LeadsTo {s. MM s = #3}";
   11.19  by (cut_facts_tac [invariantU] 1);
   11.20  by (ensures_tac "cmd2U" 1);
   11.21  qed "U_F2";
   11.22  
   11.23 -Goal "Mprg : LeadsTo {s. MM s = #3} {s. PP s}";
   11.24 +Goal "Mprg : {s. MM s = #3} LeadsTo {s. PP s}";
   11.25  by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1);
   11.26  by (ensures_tac "cmd4U" 2);
   11.27  by (ensures_tac "cmd3U" 1);
   11.28  qed "U_F3";
   11.29  
   11.30 -Goal "Mprg : LeadsTo {s. MM s = #2} {s. PP s}";
   11.31 +Goal "Mprg : {s. MM s = #2} LeadsTo {s. PP s}";
   11.32  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   11.33  	  MRS LeadsTo_Diff) 1);
   11.34  by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   11.35  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   11.36  val U_lemma2 = result();
   11.37  
   11.38 -Goal "Mprg : LeadsTo {s. MM s = #1} {s. PP s}";
   11.39 +Goal "Mprg : {s. MM s = #1} LeadsTo {s. PP s}";
   11.40  by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
   11.41  by (Blast_tac 1);
   11.42  val U_lemma1 = result();
   11.43  
   11.44 -Goal "Mprg : LeadsTo {s. #1 <= MM s & MM s <= #3} {s. PP s}";
   11.45 +Goal "Mprg : {s. #1 <= MM s & MM s <= #3} LeadsTo {s. PP s}";
   11.46  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
   11.47  				  U_lemma1, U_lemma2, U_F3] ) 1);
   11.48  val U_lemma123 = result();
   11.49  
   11.50  (*Misra's F4*)
   11.51 -Goal "Mprg : LeadsTo {s. UU s} {s. PP s}";
   11.52 +Goal "Mprg : {s. UU s} LeadsTo {s. PP s}";
   11.53  by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   11.54  by Auto_tac;
   11.55  qed "u_Leadsto_p";
   11.56 @@ -120,45 +120,45 @@
   11.57  (*** Progress for V ***)
   11.58  
   11.59  
   11.60 -Goalw [Unless_def] "Mprg : Unless {s. NN s=#2} {s. NN s=#3}";
   11.61 +Goalw [Unless_def] "Mprg : {s. NN s=#2} Unless {s. NN s=#3}";
   11.62  by (constrains_tac 1);
   11.63  qed "V_F0";
   11.64  
   11.65 -Goal "Mprg : LeadsTo {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
   11.66 +Goal "Mprg : {s. NN s=#1} LeadsTo {s. PP s = (~ UU s) & NN s = #2}";
   11.67  by (ensures_tac "cmd1V" 1);
   11.68  qed "V_F1";
   11.69  
   11.70 -Goal "Mprg : LeadsTo {s. PP s & NN s = #2} {s. NN s = #3}";
   11.71 +Goal "Mprg : {s. PP s & NN s = #2} LeadsTo {s. NN s = #3}";
   11.72  by (cut_facts_tac [invariantV] 1);
   11.73  by (ensures_tac "cmd2V" 1);
   11.74  qed "V_F2";
   11.75  
   11.76 -Goal "Mprg : LeadsTo {s. NN s = #3} {s. ~ PP s}";
   11.77 +Goal "Mprg : {s. NN s = #3} LeadsTo {s. ~ PP s}";
   11.78  by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1);
   11.79  by (ensures_tac "cmd4V" 2);
   11.80  by (ensures_tac "cmd3V" 1);
   11.81  qed "V_F3";
   11.82  
   11.83 -Goal "Mprg : LeadsTo {s. NN s = #2} {s. ~ PP s}";
   11.84 +Goal "Mprg : {s. NN s = #2} LeadsTo {s. ~ PP s}";
   11.85  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   11.86  	  MRS LeadsTo_Diff) 1);
   11.87  by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   11.88  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   11.89  val V_lemma2 = result();
   11.90  
   11.91 -Goal "Mprg : LeadsTo {s. NN s = #1} {s. ~ PP s}";
   11.92 +Goal "Mprg : {s. NN s = #1} LeadsTo {s. ~ PP s}";
   11.93  by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
   11.94  by (Blast_tac 1);
   11.95  val V_lemma1 = result();
   11.96  
   11.97 -Goal "Mprg : LeadsTo {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
   11.98 +Goal "Mprg : {s. #1 <= NN s & NN s <= #3} LeadsTo {s. ~ PP s}";
   11.99  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
  11.100  				  V_lemma1, V_lemma2, V_F3] ) 1);
  11.101  val V_lemma123 = result();
  11.102  
  11.103  
  11.104  (*Misra's F4*)
  11.105 -Goal "Mprg : LeadsTo {s. VV s} {s. ~ PP s}";
  11.106 +Goal "Mprg : {s. VV s} LeadsTo {s. ~ PP s}";
  11.107  by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
  11.108  by Auto_tac;
  11.109  qed "v_Leadsto_not_p";
  11.110 @@ -167,7 +167,7 @@
  11.111  (** Absence of starvation **)
  11.112  
  11.113  (*Misra's F6*)
  11.114 -Goal "Mprg : LeadsTo {s. MM s = #1} {s. MM s = #3}";
  11.115 +Goal "Mprg : {s. MM s = #1} LeadsTo {s. MM s = #3}";
  11.116  by (rtac LeadsTo_Un_duplicate 1);
  11.117  by (rtac LeadsTo_cancel2 1);
  11.118  by (rtac U_F2 2);
  11.119 @@ -181,7 +181,7 @@
  11.120  
  11.121  
  11.122  (*The same for V*)
  11.123 -Goal "Mprg : LeadsTo {s. NN s = #1} {s. NN s = #3}";
  11.124 +Goal "Mprg : {s. NN s = #1} LeadsTo {s. NN s = #3}";
  11.125  by (rtac LeadsTo_Un_duplicate 1);
  11.126  by (rtac LeadsTo_cancel2 1);
  11.127  by (rtac V_F2 2);
    12.1 --- a/src/HOL/UNITY/Network.ML	Wed Apr 28 13:36:31 1999 +0200
    12.2 +++ b/src/HOL/UNITY/Network.ML	Thu Apr 29 10:51:58 1999 +0200
    12.3 @@ -14,9 +14,9 @@
    12.4  \      !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
    12.5  \      !! m proc. F : stable {s. m <= s(proc,Sent)};  \
    12.6  \      !! n proc. F : stable {s. n <= s(proc,Rcvd)};  \
    12.7 -\      !! m proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
    12.8 +\      !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
    12.9  \                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
   12.10 -\      !! n proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
   12.11 +\      !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
   12.12  \                                 {s. s(proc,Sent) = n} \
   12.13  \   |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
   12.14  \                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
    13.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Apr 28 13:36:31 1999 +0200
    13.2 +++ b/src/HOL/UNITY/PPROD.ML	Thu Apr 29 10:51:58 1999 +0200
    13.3 @@ -68,12 +68,12 @@
    13.4  qed "component_PPROD";
    13.5  
    13.6  
    13.7 -(*** Safety: constrains, stable, invariant ***)
    13.8 +(*** Safety: co, stable, invariant ***)
    13.9  
   13.10  (** 1st formulation of lifting **)
   13.11  
   13.12 -Goal "(lift_prog i F : constrains (lift_set i A) (lift_set i B))  =  \
   13.13 -\     (F : constrains A B)";
   13.14 +Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
   13.15 +\     (F : A co B)";
   13.16  by (auto_tac (claset(), 
   13.17  	      simpset() addsimps [constrains_def, Acts_lift_prog]));
   13.18  by (Blast_tac 2);
   13.19 @@ -85,16 +85,16 @@
   13.20  qed "lift_prog_stable_eq";
   13.21  
   13.22  (*This one looks strange!  Proof probably is by case analysis on i=j.*)
   13.23 -Goal "F i : constrains A B  \
   13.24 -\     ==> lift_prog j (F j) : constrains (lift_set i A) (lift_set i B)";
   13.25 +Goal "F i : A co B  \
   13.26 +\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
   13.27  by (auto_tac (claset(), 
   13.28  	      simpset() addsimps [constrains_def, Acts_lift_prog]));
   13.29  by (REPEAT (Blast_tac 1));
   13.30  qed "constrains_imp_lift_prog_constrains";
   13.31  
   13.32  Goal "i : I ==>  \
   13.33 -\     (PPROD I F : constrains (lift_set i A) (lift_set i B))  =  \
   13.34 -\     (F i : constrains A B)";
   13.35 +\     (PPROD I F : (lift_set i A) co (lift_set i B))  =  \
   13.36 +\     (F i : A co B)";
   13.37  by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1);
   13.38  by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, 
   13.39  			       constrains_imp_lift_prog_constrains]) 1);
   13.40 @@ -107,8 +107,8 @@
   13.41  
   13.42  (** 2nd formulation of lifting **)
   13.43  
   13.44 -Goal "[| lift_prog i F : constrains AA BB |] \
   13.45 -\     ==> F : constrains (Applyall AA i) (Applyall BB i)";
   13.46 +Goal "[| lift_prog i F : AA co BB |] \
   13.47 +\     ==> F : (Applyall AA i) co (Applyall BB i)";
   13.48  by (auto_tac (claset(), 
   13.49  	      simpset() addsimps [Applyall_def, constrains_def, 
   13.50  				  Acts_lift_prog]));
   13.51 @@ -116,8 +116,8 @@
   13.52  	       simpset()) 1);
   13.53  qed "lift_prog_constrains_projection";
   13.54  
   13.55 -Goal "[| PPROD I F : constrains AA BB;  i: I |] \
   13.56 -\     ==> F i : constrains (Applyall AA i) (Applyall BB i)";
   13.57 +Goal "[| PPROD I F : AA co BB;  i: I |] \
   13.58 +\     ==> F i : (Applyall AA i) co (Applyall BB i)";
   13.59  by (rtac lift_prog_constrains_projection 1);
   13.60  (*rotate this assumption to be last*)
   13.61  by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1);
   13.62 @@ -163,7 +163,7 @@
   13.63  qed "PFUN_invariant";
   13.64  
   13.65  
   13.66 -(*** Substitution Axiom versions: Constrains, Stable ***)
   13.67 +(*** Substitution Axiom versions: Co, Stable ***)
   13.68  
   13.69  (** Reachability **)
   13.70  
   13.71 @@ -225,10 +225,10 @@
   13.72  qed "reachable_PPROD_eq";
   13.73  
   13.74  
   13.75 -(** Constrains **)
   13.76 +(** Co **)
   13.77  
   13.78 -Goal "[| F i : Constrains A B;  i: I;  finite I |]  \
   13.79 -\     ==> PPROD I F : Constrains (lift_set i A) (lift_set i B)";
   13.80 +Goal "[| F i : A Co B;  i: I;  finite I |]  \
   13.81 +\     ==> PPROD I F : (lift_set i A) Co (lift_set i B)";
   13.82  by (auto_tac
   13.83      (claset(),
   13.84       simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
   13.85 @@ -245,11 +245,11 @@
   13.86  	       simpset() addsimps [Applyall_def, lift_set_def]) 1);
   13.87  qed "Applyall_Int_depend";
   13.88  
   13.89 -(*Again, we need the f0 premise because otherwise Constrains holds trivially
   13.90 +(*Again, we need the f0 premise because otherwise holds Co trivially
   13.91    for PPROD I F.*)
   13.92 -Goal "[| PPROD I F : Constrains (lift_set i A) (lift_set i B);  \
   13.93 +Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B);  \
   13.94  \        i: I;  finite I;  f0: Init (PPROD I F) |]  \
   13.95 -\     ==> F i : Constrains A B";
   13.96 +\     ==> F i : A Co B";
   13.97  by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
   13.98  by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
   13.99  by (blast_tac (claset() addIs [reachable.Init]) 2);
  13.100 @@ -261,8 +261,8 @@
  13.101  
  13.102  
  13.103  Goal "[| i: I;  finite I;  f0: Init (PPROD I F) |]  \
  13.104 -\     ==> (PPROD I F : Constrains (lift_set i A) (lift_set i B)) =  \
  13.105 -\         (F i : Constrains A B)";
  13.106 +\     ==> (PPROD I F : (lift_set i A) Co (lift_set i B)) =  \
  13.107 +\         (F i : A Co B)";
  13.108  by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, 
  13.109  			       PPROD_Constrains_imp_Constrains]) 1);
  13.110  qed "PPROD_Constrains";
  13.111 @@ -281,9 +281,9 @@
  13.112  by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1);
  13.113  qed "Applyall_Int";
  13.114  
  13.115 -Goal "[| (PPI x:I. F) : Constrains (lift_set i A) (lift_set i B);  \
  13.116 +Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B);  \
  13.117  \        i: I;  finite I |]  \
  13.118 -\     ==> F : Constrains A B";
  13.119 +\     ==> F : A Co B";
  13.120  by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
  13.121  by (dtac PPROD_constrains_projection 1);
  13.122  by (assume_tac 1);
  13.123 @@ -293,8 +293,8 @@
  13.124  qed "PFUN_Constrains_imp_Constrains";
  13.125  
  13.126  Goal "[| i: I;  finite I |]  \
  13.127 -\     ==> ((PPI x:I. F) : Constrains (lift_set i A) (lift_set i B)) =  \
  13.128 -\         (F : Constrains A B)";
  13.129 +\     ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
  13.130 +\         (F : A Co B)";
  13.131  by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, 
  13.132  			       PFUN_Constrains_imp_Constrains]) 1);
  13.133  qed "PFUN_Constrains";
    14.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Apr 28 13:36:31 1999 +0200
    14.2 +++ b/src/HOL/UNITY/ROOT.ML	Thu Apr 29 10:51:58 1999 +0200
    14.3 @@ -13,7 +13,6 @@
    14.4  add_path "../Lex";	(*to find Prefix.thy*)
    14.5  
    14.6  time_use_thy"UNITY";
    14.7 -
    14.8  time_use_thy "Deadlock";
    14.9  time_use_thy "WFair";
   14.10  time_use_thy "Common";
    15.1 --- a/src/HOL/UNITY/Reach.ML	Wed Apr 28 13:36:31 1999 +0200
    15.2 +++ b/src/HOL/UNITY/Reach.ML	Thu Apr 29 10:51:58 1999 +0200
    15.3 @@ -109,7 +109,7 @@
    15.4  	      simpset() addsimps [fun_upd_idem]));
    15.5  qed "metric_le";
    15.6  
    15.7 -Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
    15.8 +Goal "Rprg : ((metric-``{m}) - fixedpoint) LeadsTo (metric-``(lessThan m))";
    15.9  by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
   15.10  by (rtac LeadsTo_UN 1);
   15.11  by Auto_tac;
   15.12 @@ -121,7 +121,7 @@
   15.13  	      simpset()));
   15.14  qed "LeadsTo_Diff_fixedpoint";
   15.15  
   15.16 -Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
   15.17 +Goal "Rprg : (metric-``{m}) LeadsTo (metric-``(lessThan m) Un fixedpoint)";
   15.18  by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
   15.19  	   subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
   15.20  by Auto_tac;
   15.21 @@ -129,13 +129,13 @@
   15.22  
   15.23  
   15.24  (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
   15.25 -Goal "Rprg : LeadsTo UNIV fixedpoint";
   15.26 +Goal "Rprg : UNIV LeadsTo fixedpoint";
   15.27  by (rtac LessThan_induct 1);
   15.28  by Auto_tac;
   15.29  by (rtac LeadsTo_Un_fixedpoint 1);
   15.30  qed "LeadsTo_fixedpoint";
   15.31  
   15.32 -Goal "Rprg : LeadsTo UNIV { %v. (init, v) : edges^* }";
   15.33 +Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
   15.34  by (stac (fixedpoint_invariant_correct RS sym) 1);
   15.35  by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
   15.36  	  MRS Invariant_LeadsTo_weaken) 1); 
    16.1 --- a/src/HOL/UNITY/SubstAx.ML	Wed Apr 28 13:36:31 1999 +0200
    16.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Apr 29 10:51:58 1999 +0200
    16.3 @@ -6,21 +6,21 @@
    16.4  LeadsTo relation, restricted to the set of reachable states.
    16.5  *)
    16.6  
    16.7 -overload_1st_set "SubstAx.LeadsTo";
    16.8 +overload_1st_set "SubstAx.op LeadsTo";
    16.9  
   16.10  
   16.11  (*** Specialized laws for handling invariants ***)
   16.12  
   16.13  (** Conjoining a safety property **)
   16.14  
   16.15 -Goal "[| reachable F <= C;  F : LeadsTo (C Int A) A' |]   \
   16.16 -\     ==> F : LeadsTo A A'";
   16.17 +Goal "[| reachable F <= C;  F : (C Int A) LeadsTo A' |]   \
   16.18 +\     ==> F : A LeadsTo A'";
   16.19  by (asm_full_simp_tac
   16.20      (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
   16.21  qed "reachable_LeadsToI";
   16.22  
   16.23 -Goal "[| reachable F <= C;  F : LeadsTo A A' |]   \
   16.24 -\     ==> F : LeadsTo A (C Int A')";
   16.25 +Goal "[| reachable F <= C;  F : A LeadsTo A' |]   \
   16.26 +\     ==> F : A LeadsTo (C Int A')";
   16.27  by (asm_full_simp_tac
   16.28      (simpset() addsimps [LeadsTo_def, Int_absorb2,
   16.29  			 Int_assoc RS sym]) 1);
   16.30 @@ -29,11 +29,11 @@
   16.31  
   16.32  (** Conjoining an invariant **)
   16.33  
   16.34 -(* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *)
   16.35 +(* [| Invariant F C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
   16.36  bind_thm ("Invariant_LeadsToI", 
   16.37  	  Invariant_includes_reachable RS reachable_LeadsToI);
   16.38  
   16.39 -(* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *)
   16.40 +(* [| Invariant F C; F : A LeadsTo A' |] ==> F : A LeadsTo (C Int A') *)
   16.41  bind_thm ("Invariant_LeadsToD", 
   16.42  	  Invariant_includes_reachable RS reachable_LeadsToD);
   16.43  
   16.44 @@ -42,18 +42,18 @@
   16.45  
   16.46  (*** Introduction rules: Basis, Trans, Union ***)
   16.47  
   16.48 -Goal "F : leadsTo A B ==> F : LeadsTo A B";
   16.49 +Goal "F : A leadsTo B ==> F : A LeadsTo B";
   16.50  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   16.51  by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
   16.52  qed "leadsTo_imp_LeadsTo";
   16.53  
   16.54 -Goal "[| F : LeadsTo A B;  F : LeadsTo B C |] ==> F : LeadsTo A C";
   16.55 +Goal "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C";
   16.56  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   16.57  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
   16.58  qed "LeadsTo_Trans";
   16.59  
   16.60  val prems = Goalw [LeadsTo_def]
   16.61 -     "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B";
   16.62 +     "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B";
   16.63  by (Simp_tac 1);
   16.64  by (stac Int_Union 1);
   16.65  by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
   16.66 @@ -62,34 +62,34 @@
   16.67  
   16.68  (*** Derived rules ***)
   16.69  
   16.70 -Goal "F : LeadsTo A UNIV";
   16.71 +Goal "F : A LeadsTo UNIV";
   16.72  by (asm_simp_tac 
   16.73      (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1);
   16.74  qed "LeadsTo_UNIV";
   16.75  Addsimps [LeadsTo_UNIV];
   16.76  
   16.77  (*Useful with cancellation, disjunction*)
   16.78 -Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'";
   16.79 +Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'";
   16.80  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   16.81  qed "LeadsTo_Un_duplicate";
   16.82  
   16.83 -Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo A (A' Un C)";
   16.84 +Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)";
   16.85  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   16.86  qed "LeadsTo_Un_duplicate2";
   16.87  
   16.88  val prems = 
   16.89 -Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B";
   16.90 +Goal "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B";
   16.91  by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
   16.92  by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
   16.93  qed "LeadsTo_UN";
   16.94  
   16.95  (*Binary union introduction rule*)
   16.96 -Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (A Un B) C";
   16.97 +Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C";
   16.98  by (stac Un_eq_Union 1);
   16.99  by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
  16.100  qed "LeadsTo_Un";
  16.101  
  16.102 -Goal "A <= B ==> F : LeadsTo A B";
  16.103 +Goal "A <= B ==> F : A LeadsTo B";
  16.104  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  16.105  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  16.106  qed "subset_imp_LeadsTo";
  16.107 @@ -97,39 +97,39 @@
  16.108  bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
  16.109  Addsimps [empty_LeadsTo];
  16.110  
  16.111 -Goal "[| F : LeadsTo A A';  A' <= B' |] ==> F : LeadsTo A B'";
  16.112 +Goal "[| F : A LeadsTo A';  A' <= B' |] ==> F : A LeadsTo B'";
  16.113  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  16.114  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
  16.115  qed_spec_mp "LeadsTo_weaken_R";
  16.116  
  16.117 -Goal "[| F : LeadsTo A A';  B <= A |]  \
  16.118 -\     ==> F : LeadsTo B A'";
  16.119 +Goal "[| F : A LeadsTo A';  B <= A |]  \
  16.120 +\     ==> F : B LeadsTo A'";
  16.121  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  16.122  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
  16.123  qed_spec_mp "LeadsTo_weaken_L";
  16.124  
  16.125 -Goal "[| F : LeadsTo A A';   \
  16.126 +Goal "[| F : A LeadsTo A';   \
  16.127  \        B  <= A;   A' <= B' |] \
  16.128 -\     ==> F : LeadsTo B B'";
  16.129 +\     ==> F : B LeadsTo B'";
  16.130  by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
  16.131  			       LeadsTo_Trans]) 1);
  16.132  qed "LeadsTo_weaken";
  16.133  
  16.134 -Goal "[| reachable F <= C;  F : LeadsTo A A';   \
  16.135 +Goal "[| reachable F <= C;  F : A LeadsTo A';   \
  16.136  \        C Int B <= A;   C Int A' <= B' |] \
  16.137 -\     ==> F : LeadsTo B B'";
  16.138 +\     ==> F : B LeadsTo B'";
  16.139  by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
  16.140                          addIs [reachable_LeadsToD]) 1);
  16.141  qed "reachable_LeadsTo_weaken";
  16.142  
  16.143  (** Two theorems for "proof lattices" **)
  16.144  
  16.145 -Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B";
  16.146 +Goal "[| F : A LeadsTo B |] ==> F : (A Un B) LeadsTo B";
  16.147  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
  16.148  qed "LeadsTo_Un_post";
  16.149  
  16.150 -Goal "[| F : LeadsTo A B;  F : LeadsTo B C |] \
  16.151 -\     ==> F : LeadsTo (A Un B) C";
  16.152 +Goal "[| F : A LeadsTo B;  F : B LeadsTo C |] \
  16.153 +\     ==> F : (A Un B) LeadsTo C";
  16.154  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
  16.155  			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
  16.156  qed "LeadsTo_Trans_Un";
  16.157 @@ -137,23 +137,23 @@
  16.158  
  16.159  (** Distributive laws **)
  16.160  
  16.161 -Goal "(F : LeadsTo (A Un B) C)  = (F : LeadsTo A C & F : LeadsTo B C)";
  16.162 +Goal "(F : (A Un B) LeadsTo C)  = (F : A LeadsTo C & F : B LeadsTo C)";
  16.163  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
  16.164  qed "LeadsTo_Un_distrib";
  16.165  
  16.166 -Goal "(F : LeadsTo (UN i:I. A i) B)  =  (ALL i : I. F : LeadsTo (A i) B)";
  16.167 +Goal "(F : (UN i:I. A i) LeadsTo B)  =  (ALL i : I. F : (A i) LeadsTo B)";
  16.168  by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
  16.169  qed "LeadsTo_UN_distrib";
  16.170  
  16.171 -Goal "(F : LeadsTo (Union S) B)  =  (ALL A : S. F : LeadsTo A B)";
  16.172 +Goal "(F : (Union S) LeadsTo B)  =  (ALL A : S. F : A LeadsTo B)";
  16.173  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
  16.174  qed "LeadsTo_Union_distrib";
  16.175  
  16.176  
  16.177  (** More rules using the premise "Invariant F" **)
  16.178  
  16.179 -Goal "[| F : Constrains (A-A') (A Un A');  F : transient (A-A') |]   \
  16.180 -\     ==> F : LeadsTo A A'";
  16.181 +Goal "[| F : (A-A') Co (A Un A');  F : transient (A-A') |]   \
  16.182 +\     ==> F : A LeadsTo A'";
  16.183  by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1);
  16.184  by (rtac (ensuresI RS leadsTo_Basis) 1);
  16.185  by (blast_tac (claset() addIs [transient_strengthen]) 2);
  16.186 @@ -161,9 +161,9 @@
  16.187  qed "LeadsTo_Basis";
  16.188  
  16.189  Goal "[| F : Invariant INV;      \
  16.190 -\        F : Constrains (INV Int (A-A')) (A Un A'); \
  16.191 +\        F : (INV Int (A-A')) Co (A Un A'); \
  16.192  \        F : transient (INV Int (A-A')) |]   \
  16.193 -\ ==> F : LeadsTo A A'";
  16.194 +\ ==> F : A LeadsTo A'";
  16.195  by (rtac Invariant_LeadsToI 1);
  16.196  by (assume_tac 1);
  16.197  by (rtac LeadsTo_Basis 1);
  16.198 @@ -172,8 +172,8 @@
  16.199  qed "Invariant_LeadsTo_Basis";
  16.200  
  16.201  Goal "[| F : Invariant INV;      \
  16.202 -\        F : LeadsTo A A';  INV Int B  <= A;  INV Int A' <= B' |] \
  16.203 -\     ==> F : LeadsTo B B'";
  16.204 +\        F : A LeadsTo A';  INV Int B  <= A;  INV Int A' <= B' |] \
  16.205 +\     ==> F : B LeadsTo B'";
  16.206  by (REPEAT (ares_tac [Invariant_includes_reachable, 
  16.207  		      reachable_LeadsTo_weaken] 1));
  16.208  qed "Invariant_LeadsTo_weaken";
  16.209 @@ -181,15 +181,15 @@
  16.210  
  16.211  (*Set difference: maybe combine with leadsTo_weaken_L??
  16.212    This is the most useful form of the "disjunction" rule*)
  16.213 -Goal "[| F : LeadsTo (A-B) C;  F : LeadsTo (A Int B) C |] \
  16.214 -\     ==> F : LeadsTo A C";
  16.215 +Goal "[| F : (A-B) LeadsTo C;  F : (A Int B) LeadsTo C |] \
  16.216 +\     ==> F : A LeadsTo C";
  16.217  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
  16.218  qed "LeadsTo_Diff";
  16.219  
  16.220  
  16.221  val prems = 
  16.222 -Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
  16.223 -\     ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)";
  16.224 +Goal "(!! i. i:I ==> F : (A i) LeadsTo (A' i)) \
  16.225 +\     ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)";
  16.226  by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
  16.227  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
  16.228                          addIs prems) 1);
  16.229 @@ -198,22 +198,22 @@
  16.230  
  16.231  (*Version with no index set*)
  16.232  val prems = 
  16.233 -Goal "(!! i. F : LeadsTo (A i) (A' i)) \
  16.234 -\     ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
  16.235 +Goal "(!! i. F : (A i) LeadsTo (A' i)) \
  16.236 +\     ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
  16.237  by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
  16.238                          addIs prems) 1);
  16.239  qed "LeadsTo_UN_UN_noindex";
  16.240  
  16.241  (*Version with no index set*)
  16.242 -Goal "ALL i. F : LeadsTo (A i) (A' i) \
  16.243 -\     ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
  16.244 +Goal "ALL i. F : (A i) LeadsTo (A' i) \
  16.245 +\     ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
  16.246  by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
  16.247  qed "all_LeadsTo_UN_UN";
  16.248  
  16.249  
  16.250  (*Binary union version*)
  16.251 -Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \
  16.252 -\           ==> F : LeadsTo (A Un B) (A' Un B')";
  16.253 +Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \
  16.254 +\           ==> F : (A Un B) LeadsTo (A' Un B')";
  16.255  by (blast_tac (claset() addIs [LeadsTo_Un, 
  16.256  			       LeadsTo_weaken_R]) 1);
  16.257  qed "LeadsTo_Un_Un";
  16.258 @@ -221,27 +221,27 @@
  16.259  
  16.260  (** The cancellation law **)
  16.261  
  16.262 -Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |]    \
  16.263 -\     ==> F : LeadsTo A (A' Un B')";
  16.264 +Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]    \
  16.265 +\     ==> F : A LeadsTo (A' Un B')";
  16.266  by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
  16.267  			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
  16.268  qed "LeadsTo_cancel2";
  16.269  
  16.270 -Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \
  16.271 -\     ==> F : LeadsTo A (A' Un B')";
  16.272 +Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \
  16.273 +\     ==> F : A LeadsTo (A' Un B')";
  16.274  by (rtac LeadsTo_cancel2 1);
  16.275  by (assume_tac 2);
  16.276  by (ALLGOALS Asm_simp_tac);
  16.277  qed "LeadsTo_cancel_Diff2";
  16.278  
  16.279 -Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \
  16.280 -\     ==> F : LeadsTo A (B' Un A')";
  16.281 +Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \
  16.282 +\     ==> F : A LeadsTo (B' Un A')";
  16.283  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  16.284  by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
  16.285  qed "LeadsTo_cancel1";
  16.286  
  16.287 -Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \
  16.288 -\     ==> F : LeadsTo A (B' Un A')";
  16.289 +Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \
  16.290 +\     ==> F : A LeadsTo (B' Un A')";
  16.291  by (rtac LeadsTo_cancel1 1);
  16.292  by (assume_tac 2);
  16.293  by (ALLGOALS Asm_simp_tac);
  16.294 @@ -251,7 +251,7 @@
  16.295  (** The impossibility law **)
  16.296  
  16.297  (*The set "A" may be non-empty, but it contains no reachable states*)
  16.298 -Goal "F : LeadsTo A {} ==> reachable F Int A = {}";
  16.299 +Goal "F : A LeadsTo {} ==> reachable F Int A = {}";
  16.300  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  16.301  by (etac leadsTo_empty 1);
  16.302  qed "LeadsTo_empty";
  16.303 @@ -260,33 +260,33 @@
  16.304  (** PSP: Progress-Safety-Progress **)
  16.305  
  16.306  (*Special case of PSP: Misra's "stable conjunction"*)
  16.307 -Goal "[| F : LeadsTo A A';  F : Stable B |] \
  16.308 -\     ==> F : LeadsTo (A Int B) (A' Int B)";
  16.309 +Goal "[| F : A LeadsTo A';  F : Stable B |] \
  16.310 +\     ==> F : (A Int B) LeadsTo (A' Int B)";
  16.311  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
  16.312  by (dtac psp_stable 1);
  16.313  by (assume_tac 1);
  16.314  by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
  16.315  qed "PSP_stable";
  16.316  
  16.317 -Goal "[| F : LeadsTo A A'; F : Stable B |] \
  16.318 -\     ==> F : LeadsTo (B Int A) (B Int A')";
  16.319 +Goal "[| F : A LeadsTo A'; F : Stable B |] \
  16.320 +\     ==> F : (B Int A) LeadsTo (B Int A')";
  16.321  by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
  16.322  qed "PSP_stable2";
  16.323  
  16.324  Goalw [LeadsTo_def, Constrains_def]
  16.325 -     "[| F : LeadsTo A A'; F : Constrains B B' |] \
  16.326 -\     ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))";
  16.327 +     "[| F : A LeadsTo A'; F : B Co B' |] \
  16.328 +\     ==> F : (A Int B) LeadsTo ((A' Int B) Un (B' - B))";
  16.329  by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
  16.330  qed "PSP";
  16.331  
  16.332 -Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \
  16.333 -\     ==> F : LeadsTo (B Int A) ((B Int A') Un (B' - B))";
  16.334 +Goal "[| F : A LeadsTo A'; F : B Co B' |] \
  16.335 +\     ==> F : (B Int A) LeadsTo ((B Int A') Un (B' - B))";
  16.336  by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
  16.337  qed "PSP2";
  16.338  
  16.339  Goalw [Unless_def]
  16.340 -     "[| F : LeadsTo A A'; F : Unless B B' |] \
  16.341 -\     ==> F : LeadsTo (A Int B) ((A' Int B) Un B')";
  16.342 +     "[| F : A LeadsTo A'; F : B Unless B' |] \
  16.343 +\     ==> F : (A Int B) LeadsTo ((A' Int B) Un B')";
  16.344  by (dtac PSP 1);
  16.345  by (assume_tac 1);
  16.346  by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
  16.347 @@ -295,7 +295,7 @@
  16.348  
  16.349  
  16.350  Goal "[| F : Stable A;  F : transient C;  \
  16.351 -\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
  16.352 +\        reachable F <= (-A Un B Un C) |] ==> F : A LeadsTo B";
  16.353  by (etac reachable_LeadsTo_weaken 1);
  16.354  by (rtac LeadsTo_Diff 1);
  16.355  by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
  16.356 @@ -307,9 +307,9 @@
  16.357  
  16.358  (** Meta or object quantifier ????? **)
  16.359  Goal "[| wf r;     \
  16.360 -\        ALL m. F : LeadsTo (A Int f-``{m})                     \
  16.361 +\        ALL m. F : (A Int f-``{m}) LeadsTo                     \
  16.362  \                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  16.363 -\     ==> F : LeadsTo A B";
  16.364 +\     ==> F : A LeadsTo B";
  16.365  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  16.366  by (etac leadsTo_wf_induct 1);
  16.367  by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
  16.368 @@ -317,9 +317,9 @@
  16.369  
  16.370  
  16.371  Goal "[| wf r;     \
  16.372 -\        ALL m:I. F : LeadsTo (A Int f-``{m})                   \
  16.373 +\        ALL m:I. F : (A Int f-``{m}) LeadsTo                   \
  16.374  \                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  16.375 -\     ==> F : LeadsTo A ((A - (f-``I)) Un B)";
  16.376 +\     ==> F : A LeadsTo ((A - (f-``I)) Un B)";
  16.377  by (etac LeadsTo_wf_induct 1);
  16.378  by Safe_tac;
  16.379  by (case_tac "m:I" 1);
  16.380 @@ -328,9 +328,9 @@
  16.381  qed "Bounded_induct";
  16.382  
  16.383  
  16.384 -Goal "[| ALL m. F : LeadsTo (A Int f-``{m})                     \
  16.385 +Goal "[| ALL m. F : (A Int f-``{m}) LeadsTo                     \
  16.386  \                           ((A Int f-``(lessThan m)) Un B) |] \
  16.387 -\     ==> F : LeadsTo A B";
  16.388 +\     ==> F : A LeadsTo B";
  16.389  by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
  16.390  by (Asm_simp_tac 1);
  16.391  qed "LessThan_induct";
  16.392 @@ -338,26 +338,26 @@
  16.393  (*Integer version.  Could generalize from #0 to any lower bound*)
  16.394  val [reach, prem] =
  16.395  Goal "[| reachable F <= {s. #0 <= f s};  \
  16.396 -\        !! z. F : LeadsTo (A Int {s. f s = z})                     \
  16.397 +\        !! z. F : (A Int {s. f s = z}) LeadsTo                     \
  16.398  \                           ((A Int {s. f s < z}) Un B) |] \
  16.399 -\     ==> F : LeadsTo A B";
  16.400 +\     ==> F : A LeadsTo B";
  16.401  by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
  16.402  by (simp_tac (simpset() addsimps [vimage_def]) 1);
  16.403  by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1);
  16.404  by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
  16.405  qed "integ_0_le_induct";
  16.406  
  16.407 -Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m})   \
  16.408 +Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo   \
  16.409  \                                        ((A Int f-``(lessThan m)) Un B) |] \
  16.410 -\           ==> F : LeadsTo A ((A Int (f-``(atMost l))) Un B)";
  16.411 +\           ==> F : A LeadsTo ((A Int (f-``(atMost l))) Un B)";
  16.412  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  16.413  by (rtac (wf_less_than RS Bounded_induct) 1);
  16.414  by (Asm_simp_tac 1);
  16.415  qed "LessThan_bounded_induct";
  16.416  
  16.417 -Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m})   \
  16.418 +Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo   \
  16.419  \                              ((A Int f-``(greaterThan m)) Un B) |] \
  16.420 -\     ==> F : LeadsTo A ((A Int (f-``(atLeast l))) Un B)";
  16.421 +\     ==> F : A LeadsTo ((A Int (f-``(atLeast l))) Un B)";
  16.422  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  16.423      (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
  16.424  by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  16.425 @@ -370,27 +370,27 @@
  16.426  
  16.427  (*** Completion: Binary and General Finite versions ***)
  16.428  
  16.429 -Goal "[| F : LeadsTo A A';  F : Stable A';   \
  16.430 -\        F : LeadsTo B B';  F : Stable B' |] \
  16.431 -\     ==> F : LeadsTo (A Int B) (A' Int B')";
  16.432 +Goal "[| F : A LeadsTo A';  F : Stable A';   \
  16.433 +\        F : B LeadsTo B';  F : Stable B' |] \
  16.434 +\     ==> F : (A Int B) LeadsTo (A' Int B')";
  16.435  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
  16.436  by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
  16.437  qed "Stable_completion";
  16.438  
  16.439  
  16.440  Goal "finite I      \
  16.441 -\     ==> (ALL i:I. F : LeadsTo (A i) (A' i)) -->  \
  16.442 +\     ==> (ALL i:I. F : (A i) LeadsTo (A' i)) -->  \
  16.443  \         (ALL i:I. F : Stable (A' i)) -->         \
  16.444 -\         F : LeadsTo (INT i:I. A i) (INT i:I. A' i)";
  16.445 +\         F : (INT i:I. A i) LeadsTo (INT i:I. A' i)";
  16.446  by (etac finite_induct 1);
  16.447  by (Asm_simp_tac 1);
  16.448  by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
  16.449  qed_spec_mp "Finite_stable_completion";
  16.450  
  16.451  
  16.452 -Goal "[| F : LeadsTo A (A' Un C);  F : Constrains A' (A' Un C); \
  16.453 -\        F : LeadsTo B (B' Un C);  F : Constrains B' (B' Un C) |] \
  16.454 -\     ==> F : LeadsTo (A Int B) ((A' Int B') Un C)";
  16.455 +Goal "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C); \
  16.456 +\        F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |] \
  16.457 +\     ==> F : (A Int B) LeadsTo ((A' Int B') Un C)";
  16.458  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
  16.459  				       Int_Un_distrib]) 1);
  16.460  by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
  16.461 @@ -398,9 +398,9 @@
  16.462  
  16.463  
  16.464  Goal "[| finite I |] \
  16.465 -\     ==> (ALL i:I. F : LeadsTo (A i) (A' i Un C)) -->  \
  16.466 -\         (ALL i:I. F : Constrains (A' i) (A' i Un C)) --> \
  16.467 -\         F : LeadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
  16.468 +\     ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->  \
  16.469 +\         (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
  16.470 +\         F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
  16.471  by (etac finite_induct 1);
  16.472  by (ALLGOALS Asm_simp_tac);
  16.473  by (Clarify_tac 1);
  16.474 @@ -416,7 +416,7 @@
  16.475  	      etac Invariant_LeadsTo_Basis 1 
  16.476  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
  16.477  		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
  16.478 -	      (*now there are two subgoals: constrains & transient*)
  16.479 +	      (*now there are two subgoals: co & transient*)
  16.480  	      simp_tac (simpset() addsimps !program_defs_ref) 2,
  16.481  	      res_inst_tac [("act", sact)] transient_mem 2,
  16.482                   (*simplify the command's domain*)
    17.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Apr 28 13:36:31 1999 +0200
    17.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Apr 29 10:51:58 1999 +0200
    17.3 @@ -3,14 +3,16 @@
    17.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.5      Copyright   1998  University of Cambridge
    17.6  
    17.7 -LeadsTo relation: restricted to the set of reachable states.
    17.8 +Weak LeadsTo relation (restricted to the set of reachable states)
    17.9  *)
   17.10  
   17.11  SubstAx = WFair + Constrains + 
   17.12  
   17.13 -constdefs
   17.14 +consts
   17.15 +   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
   17.16  
   17.17 -   LeadsTo :: "['a set, 'a set] => 'a program set"
   17.18 -    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
   17.19 -	   	                    (reachable F  Int  B)}"
   17.20 +defs
   17.21 +   LeadsTo_def
   17.22 +    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
   17.23 +	   	            (reachable F  Int  B)}"
   17.24  end
    18.1 --- a/src/HOL/UNITY/Token.ML	Wed Apr 28 13:36:31 1999 +0200
    18.2 +++ b/src/HOL/UNITY/Token.ML	Thu Apr 29 10:51:58 1999 +0200
    18.3 @@ -67,7 +67,7 @@
    18.4  (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
    18.5    Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
    18.6  Goal "[| i<N; j<N |] ==>   \
    18.7 -\     F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
    18.8 +\     F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
    18.9  by (case_tac "i=j" 1);
   18.10  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   18.11  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   18.12 @@ -78,7 +78,7 @@
   18.13  
   18.14  (*Chapter 4 variant, the one actually used below.*)
   18.15  Goal "[| i<N; j<N; i~=j |]    \
   18.16 -\     ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}";
   18.17 +\     ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
   18.18  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   18.19  by (Clarify_tac 1);
   18.20  by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
   18.21 @@ -91,7 +91,7 @@
   18.22  
   18.23  
   18.24  (*Misra's TR9: the token reaches an arbitrary node*)
   18.25 -Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
   18.26 +Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
   18.27  by (rtac leadsTo_weaken_R 1);
   18.28  by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
   18.29       (wf_nodeOrder RS bounded_induct) 1);
   18.30 @@ -105,7 +105,7 @@
   18.31  qed "leadsTo_j";
   18.32  
   18.33  (*Misra's TR8: a hungry process eventually eats*)
   18.34 -Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)";
   18.35 +Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
   18.36  by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
   18.37  by (rtac TR6 2);
   18.38  by (rtac leadsTo_weaken_R 1);
    19.1 --- a/src/HOL/UNITY/Token.thy	Wed Apr 28 13:36:31 1999 +0200
    19.2 +++ b/src/HOL/UNITY/Token.thy	Thu Apr 29 10:51:58 1999 +0200
    19.3 @@ -43,17 +43,17 @@
    19.4    assumes
    19.5      N_positive "0<N"
    19.6  
    19.7 -    TR2  "F : constrains (T i) (T i Un H i)"
    19.8 +    TR2  "F : (T i) co (T i Un H i)"
    19.9  
   19.10 -    TR3  "F : constrains (H i) (H i Un E i)"
   19.11 +    TR3  "F : (H i) co (H i Un E i)"
   19.12  
   19.13 -    TR4  "F : constrains (H i - HasTok i) (H i)"
   19.14 +    TR4  "F : (H i - HasTok i) co (H i)"
   19.15  
   19.16 -    TR5  "F : constrains (HasTok i) (HasTok i Un -(E i))"
   19.17 +    TR5  "F : (HasTok i) co (HasTok i Un -(E i))"
   19.18  
   19.19 -    TR6  "F : leadsTo (H i Int HasTok i) (E i)"
   19.20 +    TR6  "F : (H i Int HasTok i) leadsTo (E i)"
   19.21  
   19.22 -    TR7  "F : leadsTo (HasTok i) (HasTok (next i))"
   19.23 +    TR7  "F : (HasTok i) leadsTo (HasTok (next i))"
   19.24  
   19.25    defines
   19.26      nodeOrder_def
    20.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Apr 28 13:36:31 1999 +0200
    20.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Apr 29 10:51:58 1999 +0200
    20.3 @@ -111,92 +111,91 @@
    20.4  fun simp_of_set def = def RS def_set_simp;
    20.5  
    20.6  
    20.7 -(*** constrains ***)
    20.8 +(*** co ***)
    20.9  
   20.10 -overload_1st_set "UNITY.constrains";
   20.11 +overload_1st_set "UNITY.op co";
   20.12  overload_1st_set "UNITY.stable";
   20.13  overload_1st_set "UNITY.unless";
   20.14  
   20.15  val prems = Goalw [constrains_def]
   20.16      "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
   20.17 -\    ==> F : constrains A A'";
   20.18 +\    ==> F : A co A'";
   20.19  by (blast_tac (claset() addIs prems) 1);
   20.20  qed "constrainsI";
   20.21  
   20.22  Goalw [constrains_def]
   20.23 -    "[| F : constrains A A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
   20.24 +    "[| F : A co A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
   20.25  by (Blast_tac 1);
   20.26  qed "constrainsD";
   20.27  
   20.28 -Goalw [constrains_def] "F : constrains {} B";
   20.29 +Goalw [constrains_def] "F : {} co B";
   20.30  by (Blast_tac 1);
   20.31  qed "constrains_empty";
   20.32  
   20.33 -Goalw [constrains_def] "F : constrains A UNIV";
   20.34 +Goalw [constrains_def] "F : A co UNIV";
   20.35  by (Blast_tac 1);
   20.36  qed "constrains_UNIV";
   20.37  AddIffs [constrains_empty, constrains_UNIV];
   20.38  
   20.39  (*monotonic in 2nd argument*)
   20.40  Goalw [constrains_def]
   20.41 -    "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
   20.42 +    "[| F : A co A'; A'<=B' |] ==> F : A co B'";
   20.43  by (Blast_tac 1);
   20.44  qed "constrains_weaken_R";
   20.45  
   20.46  (*anti-monotonic in 1st argument*)
   20.47  Goalw [constrains_def]
   20.48 -    "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
   20.49 +    "[| F : A co A'; B<=A |] ==> F : B co A'";
   20.50  by (Blast_tac 1);
   20.51  qed "constrains_weaken_L";
   20.52  
   20.53  Goalw [constrains_def]
   20.54 -   "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
   20.55 +   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
   20.56  by (Blast_tac 1);
   20.57  qed "constrains_weaken";
   20.58  
   20.59  (** Union **)
   20.60  
   20.61  Goalw [constrains_def]
   20.62 -    "[| F : constrains A A'; F : constrains B B' |]   \
   20.63 -\    ==> F : constrains (A Un B) (A' Un B')";
   20.64 +    "[| F : A co A'; F : B co B' |]   \
   20.65 +\    ==> F : (A Un B) co (A' Un B')";
   20.66  by (Blast_tac 1);
   20.67  qed "constrains_Un";
   20.68  
   20.69  Goalw [constrains_def]
   20.70 -    "ALL i:I. F : constrains (A i) (A' i) \
   20.71 -\    ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
   20.72 +    "ALL i:I. F : (A i) co (A' i) \
   20.73 +\    ==> F : (UN i:I. A i) co (UN i:I. A' i)";
   20.74  by (Blast_tac 1);
   20.75  qed "ball_constrains_UN";
   20.76  
   20.77  (** Intersection **)
   20.78  
   20.79  Goalw [constrains_def]
   20.80 -    "[| F : constrains A A'; F : constrains B B' |]   \
   20.81 -\    ==> F : constrains (A Int B) (A' Int B')";
   20.82 +    "[| F : A co A'; F : B co B' |]   \
   20.83 +\    ==> F : (A Int B) co (A' Int B')";
   20.84  by (Blast_tac 1);
   20.85  qed "constrains_Int";
   20.86  
   20.87  Goalw [constrains_def]
   20.88 -    "ALL i:I. F : constrains (A i) (A' i) \
   20.89 -\    ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
   20.90 +    "ALL i:I. F : (A i) co (A' i) \
   20.91 +\    ==> F : (INT i:I. A i) co (INT i:I. A' i)";
   20.92  by (Blast_tac 1);
   20.93  qed "ball_constrains_INT";
   20.94  
   20.95 -Goalw [constrains_def] "F : constrains A A' ==> A <= A'";
   20.96 +Goalw [constrains_def] "F : A co A' ==> A <= A'";
   20.97  by Auto_tac;
   20.98  qed "constrains_imp_subset";
   20.99  
  20.100 -(*The reasoning is by subsets since "constrains" refers to single actions
  20.101 +(*The reasoning is by subsets since "co" refers to single actions
  20.102    only.  So this rule isn't that useful.*)
  20.103  Goalw [constrains_def]
  20.104 -    "[| F : constrains A B; F : constrains B C |]   \
  20.105 -\    ==> F : constrains A C";
  20.106 +    "[| F : A co B; F : B co C |] ==> F : A co C";
  20.107  by (Blast_tac 1);
  20.108  qed "constrains_trans";
  20.109  
  20.110  Goalw [constrains_def]
  20.111 -   "[| F : constrains A (A' Un B); F : constrains B B' |] \
  20.112 -\   ==> F : constrains A (A' Un B')";
  20.113 +   "[| F : A co (A' Un B); F : B co B' |] \
  20.114 +\   ==> F : A co (A' Un B')";
  20.115  by (Clarify_tac 1);
  20.116  by (Blast_tac 1);
  20.117  qed "constrains_cancel";
  20.118 @@ -204,11 +203,11 @@
  20.119  
  20.120  (*** stable ***)
  20.121  
  20.122 -Goalw [stable_def] "F : constrains A A ==> F : stable A";
  20.123 +Goalw [stable_def] "F : A co A ==> F : stable A";
  20.124  by (assume_tac 1);
  20.125  qed "stableI";
  20.126  
  20.127 -Goalw [stable_def] "F : stable A ==> F : constrains A A";
  20.128 +Goalw [stable_def] "F : stable A ==> F : A co A";
  20.129  by (assume_tac 1);
  20.130  qed "stableD";
  20.131  
  20.132 @@ -237,18 +236,18 @@
  20.133  qed "ball_stable_INT";
  20.134  
  20.135  Goalw [stable_def, constrains_def]
  20.136 -    "[| F : stable C; F : constrains A (C Un A') |]   \
  20.137 -\    ==> F : constrains (C Un A) (C Un A')";
  20.138 +    "[| F : stable C; F : A co (C Un A') |]   \
  20.139 +\    ==> F : (C Un A) co (C Un A')";
  20.140  by (Blast_tac 1);
  20.141  qed "stable_constrains_Un";
  20.142  
  20.143  Goalw [stable_def, constrains_def]
  20.144 -    "[| F : stable C; F : constrains (C Int A) A' |]   \
  20.145 -\    ==> F : constrains (C Int A) (C Int A')";
  20.146 +    "[| F : stable C; F :  (C Int A) co  A' |]   \
  20.147 +\    ==> F : (C Int A) co (C Int A')";
  20.148  by (Blast_tac 1);
  20.149  qed "stable_constrains_Int";
  20.150  
  20.151 -(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
  20.152 +(*[| F : stable C; F :  co (C Int A) A |] ==> F : stable (C Int A)*)
  20.153  bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
  20.154  
  20.155  
  20.156 @@ -284,15 +283,15 @@
  20.157      in forward proof. **)
  20.158  
  20.159  Goalw [constrains_def]
  20.160 -    "[| ALL m. F : constrains {s. s x = m} (B m) |] \
  20.161 -\    ==> F : constrains {s. s x : M} (UN m:M. B m)";
  20.162 +    "[| ALL m:M. F : {s. s x = m} co (B m) |] \
  20.163 +\    ==> F : {s. s x : M} co (UN m:M. B m)";
  20.164  by (Blast_tac 1);
  20.165  qed "elimination";
  20.166  
  20.167  (*As above, but for the trivial case of a one-variable state, in which the
  20.168    state is identified with its one variable.*)
  20.169  Goalw [constrains_def]
  20.170 -    "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
  20.171 +    "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)";
  20.172  by (Blast_tac 1);
  20.173  qed "elimination_sing";
  20.174  
  20.175 @@ -301,11 +300,11 @@
  20.176  (*** Theoretical Results from Section 6 ***)
  20.177  
  20.178  Goalw [constrains_def, strongest_rhs_def]
  20.179 -    "F : constrains A (strongest_rhs F A )";
  20.180 +    "F : A co (strongest_rhs F A )";
  20.181  by (Blast_tac 1);
  20.182  qed "constrains_strongest_rhs";
  20.183  
  20.184  Goalw [constrains_def, strongest_rhs_def]
  20.185 -    "F : constrains A B ==> strongest_rhs F A <= B";
  20.186 +    "F : A co B ==> strongest_rhs F A <= B";
  20.187  by (Blast_tac 1);
  20.188  qed "strongest_rhs_is_strongest";
    21.1 --- a/src/HOL/UNITY/UNITY.thy	Wed Apr 28 13:36:31 1999 +0200
    21.2 +++ b/src/HOL/UNITY/UNITY.thy	Thu Apr 29 10:51:58 1999 +0200
    21.3 @@ -14,6 +14,9 @@
    21.4  typedef (Program)
    21.5    'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    21.6  
    21.7 +consts
    21.8 +  co, unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
    21.9 +
   21.10  constdefs
   21.11      mk_program :: "('a set * ('a * 'a)set set) => 'a program"
   21.12      "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
   21.13 @@ -24,17 +27,11 @@
   21.14    Acts :: "'a program => ('a * 'a)set set"
   21.15      "Acts F == (%(init, acts). acts) (Rep_Program F)"
   21.16  
   21.17 -  constrains :: "['a set, 'a set] => 'a program set"
   21.18 -    "constrains A B == {F. ALL act: Acts F. act^^A <= B}"
   21.19 -
   21.20    stable     :: "'a set => 'a program set"
   21.21 -    "stable A == constrains A A"
   21.22 +    "stable A == A co A"
   21.23  
   21.24    strongest_rhs :: "['a program, 'a set] => 'a set"
   21.25 -    "strongest_rhs F A == Inter {B. F : constrains A B}"
   21.26 -
   21.27 -  unless :: "['a set, 'a set] => 'a program set"
   21.28 -    "unless A B == constrains (A-B) (A Un B)"
   21.29 +    "strongest_rhs F A == Inter {B. F : A co B}"
   21.30  
   21.31    invariant :: "'a set => 'a program set"
   21.32      "invariant A == {F. Init F <= A} Int stable A"
   21.33 @@ -43,4 +40,10 @@
   21.34    increasing :: "['a => 'b::{ord}] => 'a program set"
   21.35      "increasing f == INT z. stable {s. z <= f s}"
   21.36  
   21.37 +
   21.38 +defs
   21.39 +  constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
   21.40 +
   21.41 +  unless_def     "A unless B == (A-B) co (A Un B)"
   21.42 +
   21.43  end
    22.1 --- a/src/HOL/UNITY/Union.ML	Wed Apr 28 13:36:31 1999 +0200
    22.2 +++ b/src/HOL/UNITY/Union.ML	Thu Apr 29 10:51:58 1999 +0200
    22.3 @@ -137,24 +137,24 @@
    22.4  qed "JN_Join_distrib";
    22.5  
    22.6  
    22.7 -(*** Safety: constrains, stable, FP ***)
    22.8 +(*** Safety: co, stable, FP ***)
    22.9  
   22.10  Goalw [constrains_def, JOIN_def]
   22.11      "i : I ==> \
   22.12 -\    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
   22.13 +\    (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
   22.14  by (Simp_tac 1);
   22.15  by (Blast_tac 1);
   22.16  qed "constrains_JN";
   22.17  
   22.18 -Goal "F Join G : constrains A B =  \
   22.19 -\     (F : constrains A B & G : constrains A B)";
   22.20 +Goal "F Join G : A co B =  \
   22.21 +\     (F : A co B & G : A co B)";
   22.22  by (auto_tac
   22.23      (claset(),
   22.24       simpset() addsimps [constrains_def, Join_def]));
   22.25  qed "constrains_Join";
   22.26  
   22.27 -Goal "[| i : I;  ALL i:I. F i : constrains A B |] \
   22.28 -\     ==> (JN i:I. F i) : constrains A B";
   22.29 +Goal "[| i : I;  ALL i:I. F i : A co B |] \
   22.30 +\     ==> (JN i:I. F i) : A co B";
   22.31  by (full_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
   22.32  by (Blast_tac 1);
   22.33  qed "constrains_imp_JN_constrains";
   22.34 @@ -164,12 +164,12 @@
   22.35         reachable F and reachable G
   22.36  
   22.37      Goalw [Constrains_def]
   22.38 -	"(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
   22.39 +	"(JN i:I. F i) : A Co B = (ALL i:I. F i : A Co B)";
   22.40      by (simp_tac (simpset() addsimps [constrains_JN]) 1);
   22.41      by (Blast_tac 1);
   22.42      qed "Constrains_JN";
   22.43  
   22.44 -    Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
   22.45 +    Goal "F Join G : A Co B = (F Co A B & G Co A B)";
   22.46      by (auto_tac
   22.47  	(claset(),
   22.48  	 simpset() addsimps [Constrains_def, constrains_Join]));
   22.49 @@ -177,8 +177,8 @@
   22.50      **)
   22.51  
   22.52  
   22.53 -Goal "[| F : constrains A A';  G : constrains B B' |] \
   22.54 -\     ==> F Join G : constrains (A Int B) (A' Un B')";
   22.55 +Goal "[| F : A co A';  G : B co B' |] \
   22.56 +\     ==> F Join G : (A Int B) co (A' Un B')";
   22.57  by (simp_tac (simpset() addsimps [constrains_Join]) 1);
   22.58  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   22.59  qed "constrains_Join_weaken";
   22.60 @@ -226,25 +226,25 @@
   22.61  qed "transient_Join";
   22.62  
   22.63  Goal "i : I ==> \
   22.64 -\     (JN i:I. F i) : ensures A B = \
   22.65 -\     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
   22.66 -\      (EX i:I. F i : ensures A B))";
   22.67 +\     (JN i:I. F i) : A ensures B = \
   22.68 +\     ((ALL i:I. F i : (A-B) co (A Un B)) & \
   22.69 +\      (EX i:I. F i : A ensures B))";
   22.70  by (auto_tac (claset(),
   22.71  	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
   22.72  qed "ensures_JN";
   22.73  
   22.74  Goalw [ensures_def]
   22.75 -     "F Join G : ensures A B =     \
   22.76 -\     (F : constrains (A-B) (A Un B) & \
   22.77 -\      G : constrains (A-B) (A Un B) & \
   22.78 -\      (F : ensures A B | G : ensures A B))";
   22.79 +     "F Join G : A ensures B =     \
   22.80 +\     (F : (A-B) co (A Un B) & \
   22.81 +\      G : (A-B) co (A Un B) & \
   22.82 +\      (F : A ensures B | G : A ensures B))";
   22.83  by (auto_tac (claset(),
   22.84  	      simpset() addsimps [constrains_Join, transient_Join]));
   22.85  qed "ensures_Join";
   22.86  
   22.87  Goalw [stable_def, constrains_def, Join_def]
   22.88 -    "[| F : stable A;  G : constrains A A' |] \
   22.89 -\    ==> F Join G : constrains A A'";
   22.90 +    "[| F : stable A;  G : A co A' |] \
   22.91 +\    ==> F Join G : A co A'";
   22.92  by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
   22.93  by (Blast_tac 1);
   22.94  qed "stable_constrains_Join";
   22.95 @@ -258,7 +258,7 @@
   22.96  	      simpset() addsimps [Acts_Join]) 1);
   22.97  qed "stable_Join_Invariant";
   22.98  
   22.99 -Goal "[| F : stable A;  G : ensures A B |] ==> F Join G : ensures A B";
  22.100 +Goal "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B";
  22.101  by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
  22.102  by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
  22.103  by (etac constrains_weaken 1);
  22.104 @@ -266,7 +266,7 @@
  22.105  qed "ensures_stable_Join1";
  22.106  
  22.107  (*As above, but exchanging the roles of F and G*)
  22.108 -Goal "[| F : ensures A B;  G : stable A |] ==> F Join G : ensures A B";
  22.109 +Goal "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B";
  22.110  by (stac Join_commute 1);
  22.111  by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
  22.112  qed "ensures_stable_Join2";
  22.113 @@ -308,11 +308,11 @@
  22.114  
  22.115  (*** Higher-level rules involving localTo and Join ***)
  22.116  
  22.117 -Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)};   \
  22.118 +Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
  22.119  \        F Join G : v localTo F;       \
  22.120  \        F Join G : w localTo F;       \
  22.121  \        Disjoint F G |]               \
  22.122 -\     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
  22.123 +\     ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
  22.124  by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
  22.125  by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
  22.126  by Auto_tac;
  22.127 @@ -339,11 +339,11 @@
  22.128  \     ==> F Join G : Stable {s. v s <= w s}";
  22.129  by (safe_tac (claset() addSDs [localTo_imp_stable]));
  22.130  by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
  22.131 -by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
  22.132 +by (subgoal_tac "ALL k: UNIV. ?H : ({s. v s = k} Int ?AA) Co ?AA" 1);
  22.133  by (dtac ball_Constrains_UN 1);
  22.134  by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
  22.135  by (rtac ballI 1);
  22.136 -by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
  22.137 +by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
  22.138  \                                      ({s. v s = k} Un {s. v s <= w s})" 1);
  22.139  by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
  22.140  by (blast_tac (claset() addIs [constrains_weaken]) 2);
    23.1 --- a/src/HOL/UNITY/WFair.ML	Wed Apr 28 13:36:31 1999 +0200
    23.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Apr 29 10:51:58 1999 +0200
    23.3 @@ -11,7 +11,7 @@
    23.4  
    23.5  overload_1st_set "WFair.transient";
    23.6  overload_1st_set "WFair.ensures";
    23.7 -overload_1st_set "WFair.leadsTo";
    23.8 +overload_1st_set "WFair.op leadsTo";
    23.9  
   23.10  (*** transient ***)
   23.11  
   23.12 @@ -35,38 +35,38 @@
   23.13  (*** ensures ***)
   23.14  
   23.15  Goalw [ensures_def]
   23.16 -    "[| F : constrains (A-B) (A Un B); F : transient (A-B) |] \
   23.17 -\    ==> F : ensures A B";
   23.18 +    "[| F : (A-B) co (A Un B); F : transient (A-B) |] \
   23.19 +\    ==> F : A ensures B";
   23.20  by (Blast_tac 1);
   23.21  qed "ensuresI";
   23.22  
   23.23  Goalw [ensures_def]
   23.24 -    "F : ensures A B ==> F : constrains (A-B) (A Un B) & F : transient (A-B)";
   23.25 +    "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
   23.26  by (Blast_tac 1);
   23.27  qed "ensuresD";
   23.28  
   23.29  (*The L-version (precondition strengthening) doesn't hold for ENSURES*)
   23.30  Goalw [ensures_def]
   23.31 -    "[| F : ensures A A'; A'<=B' |] ==> F : ensures A B'";
   23.32 +    "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
   23.33  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   23.34  qed "ensures_weaken_R";
   23.35  
   23.36  Goalw [ensures_def, constrains_def, transient_def]
   23.37 -    "F : ensures A UNIV";
   23.38 +    "F : A ensures UNIV";
   23.39  by Auto_tac;
   23.40  qed "ensures_UNIV";
   23.41  
   23.42  Goalw [ensures_def]
   23.43      "[| F : stable C; \
   23.44 -\       F : constrains (C Int (A - A')) (A Un A'); \
   23.45 +\       F : (C Int (A - A')) co (A Un A'); \
   23.46  \       F : transient (C Int (A-A')) |]   \
   23.47 -\   ==> F : ensures (C Int A) (C Int A')";
   23.48 +\   ==> F : (C Int A) ensures (C Int A')";
   23.49  by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
   23.50  				      Diff_Int_distrib RS sym,
   23.51  				      stable_constrains_Int]) 1);
   23.52  qed "stable_ensures_Int";
   23.53  
   23.54 -Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : ensures A B";
   23.55 +Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
   23.56  by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
   23.57  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   23.58  qed "stable_transient_ensures";
   23.59 @@ -74,55 +74,55 @@
   23.60  
   23.61  (*** leadsTo ***)
   23.62  
   23.63 -Goalw [leadsTo_def] "F : ensures A B ==> F : leadsTo A B";
   23.64 +Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
   23.65  by (blast_tac (claset() addIs [leadsto.Basis]) 1);
   23.66  qed "leadsTo_Basis";
   23.67  
   23.68  Goalw [leadsTo_def]
   23.69 -     "[| F : leadsTo A B;  F : leadsTo B C |] ==> F : leadsTo A C";
   23.70 +     "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C";
   23.71  by (blast_tac (claset() addIs [leadsto.Trans]) 1);
   23.72  qed "leadsTo_Trans";
   23.73  
   23.74 -Goal "F : transient A ==> F : leadsTo A (-A)";
   23.75 +Goal "F : transient A ==> F : A leadsTo (-A)";
   23.76  by (asm_simp_tac 
   23.77      (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
   23.78  qed "transient_imp_leadsTo";
   23.79  
   23.80 -Goal "F : leadsTo A UNIV";
   23.81 +Goal "F : A leadsTo UNIV";
   23.82  by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
   23.83  qed "leadsTo_UNIV";
   23.84  Addsimps [leadsTo_UNIV];
   23.85  
   23.86  (*Useful with cancellation, disjunction*)
   23.87 -Goal "F : leadsTo A (A' Un A') ==> F : leadsTo A A'";
   23.88 +Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
   23.89  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   23.90  qed "leadsTo_Un_duplicate";
   23.91  
   23.92 -Goal "F : leadsTo A (A' Un C Un C) ==> F : leadsTo A (A' Un C)";
   23.93 +Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)";
   23.94  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   23.95  qed "leadsTo_Un_duplicate2";
   23.96  
   23.97  (*The Union introduction rule as we should have liked to state it*)
   23.98  val prems = Goalw [leadsTo_def]
   23.99 -    "(!!A. A : S ==> F : leadsTo A B) ==> F : leadsTo (Union S) B";
  23.100 +    "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
  23.101  by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
  23.102  qed "leadsTo_Union";
  23.103  
  23.104  val prems = Goalw [leadsTo_def]
  23.105 -    "(!!A. A : S ==> F : leadsTo (A Int C) B) \
  23.106 -\    ==> F : leadsTo (Union S Int C) B";
  23.107 +    "(!!A. A : S ==> F : (A Int C) leadsTo B) \
  23.108 +\    ==> F : (Union S Int C) leadsTo B";
  23.109  by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
  23.110  by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
  23.111  qed "leadsTo_Union_Int";
  23.112  
  23.113  val prems = Goal
  23.114 -    "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (UN i:I. A i) B";
  23.115 +    "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B";
  23.116  by (stac (Union_image_eq RS sym) 1);
  23.117  by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
  23.118  qed "leadsTo_UN";
  23.119  
  23.120  (*Binary union introduction rule*)
  23.121 -Goal "[| F : leadsTo A C; F : leadsTo B C |] ==> F : leadsTo (A Un B) C";
  23.122 +Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C";
  23.123  by (stac Un_eq_Union 1);
  23.124  by (blast_tac (claset() addIs [leadsTo_Union]) 1);
  23.125  qed "leadsTo_Un";
  23.126 @@ -130,18 +130,18 @@
  23.127  
  23.128  (*The INDUCTION rule as we should have liked to state it*)
  23.129  val major::prems = Goalw [leadsTo_def]
  23.130 -  "[| F : leadsTo za zb;  \
  23.131 -\     !!A B. F : ensures A B ==> P A B; \
  23.132 -\     !!A B C. [| F : leadsTo A B; P A B; F : leadsTo B C; P B C |] \
  23.133 +  "[| F : za leadsTo zb;  \
  23.134 +\     !!A B. F : A ensures B ==> P A B; \
  23.135 +\     !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \
  23.136  \              ==> P A C; \
  23.137 -\     !!B S. ALL A:S. F : leadsTo A B & P A B ==> P (Union S) B \
  23.138 +\     !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
  23.139  \  |] ==> P za zb";
  23.140  by (rtac (major RS CollectD RS leadsto.induct) 1);
  23.141  by (REPEAT (blast_tac (claset() addIs prems) 1));
  23.142  qed "leadsTo_induct";
  23.143  
  23.144  
  23.145 -Goal "A<=B ==> F : leadsTo A B";
  23.146 +Goal "A<=B ==> F : A leadsTo B";
  23.147  by (rtac leadsTo_Basis 1);
  23.148  by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  23.149  by (Blast_tac 1);
  23.150 @@ -151,36 +151,36 @@
  23.151  Addsimps [empty_leadsTo];
  23.152  
  23.153  
  23.154 -Goal "[| F : leadsTo A A'; A'<=B' |] ==> F : leadsTo A B'";
  23.155 +Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
  23.156  by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
  23.157  qed "leadsTo_weaken_R";
  23.158  
  23.159 -Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'";
  23.160 +Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
  23.161  by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
  23.162  qed_spec_mp "leadsTo_weaken_L";
  23.163  
  23.164  (*Distributes over binary unions*)
  23.165 -Goal "F : leadsTo (A Un B) C  =  (F : leadsTo A C & F : leadsTo B C)";
  23.166 +Goal "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)";
  23.167  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
  23.168  qed "leadsTo_Un_distrib";
  23.169  
  23.170 -Goal "F : leadsTo (UN i:I. A i) B  =  (ALL i : I. F : leadsTo (A i) B)";
  23.171 +Goal "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)";
  23.172  by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
  23.173  qed "leadsTo_UN_distrib";
  23.174  
  23.175 -Goal "F : leadsTo (Union S) B  =  (ALL A : S. F : leadsTo A B)";
  23.176 +Goal "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)";
  23.177  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
  23.178  qed "leadsTo_Union_distrib";
  23.179  
  23.180  
  23.181 -Goal "[| F : leadsTo A A'; B<=A; A'<=B' |] ==> F : leadsTo B B'";
  23.182 +Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'";
  23.183  by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
  23.184  			       leadsTo_Trans]) 1);
  23.185  qed "leadsTo_weaken";
  23.186  
  23.187  
  23.188  (*Set difference: maybe combine with leadsTo_weaken_L??*)
  23.189 -Goal "[| F : leadsTo (A-B) C; F : leadsTo B C |]   ==> F : leadsTo A C";
  23.190 +Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
  23.191  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
  23.192  qed "leadsTo_Diff";
  23.193  
  23.194 @@ -189,8 +189,8 @@
  23.195      see ball_constrains_UN in UNITY.ML***)
  23.196  
  23.197  val prems = goal thy
  23.198 -   "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \
  23.199 -\   ==> F : leadsTo (UN i:I. A i) (UN i:I. A' i)";
  23.200 +   "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
  23.201 +\   ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
  23.202  by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
  23.203  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
  23.204                          addIs prems) 1);
  23.205 @@ -199,21 +199,21 @@
  23.206  
  23.207  (*Version with no index set*)
  23.208  val prems = goal thy
  23.209 -   "(!! i. F : leadsTo (A i) (A' i)) \
  23.210 -\   ==> F : leadsTo (UN i. A i) (UN i. A' i)";
  23.211 +   "(!! i. F : (A i) leadsTo (A' i)) \
  23.212 +\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
  23.213  by (blast_tac (claset() addIs [leadsTo_UN_UN] 
  23.214                          addIs prems) 1);
  23.215  qed "leadsTo_UN_UN_noindex";
  23.216  
  23.217  (*Version with no index set*)
  23.218 -Goal "ALL i. F : leadsTo (A i) (A' i) \
  23.219 -\   ==> F : leadsTo (UN i. A i) (UN i. A' i)";
  23.220 +Goal "ALL i. F : (A i) leadsTo (A' i) \
  23.221 +\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
  23.222  by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
  23.223  qed "all_leadsTo_UN_UN";
  23.224  
  23.225  
  23.226  (*Binary union version*)
  23.227 -Goal "[| F : leadsTo A A'; F : leadsTo B B' |]     ==> F : leadsTo (A Un B) (A' Un B')";
  23.228 +Goal "[| F : A leadsTo A'; F : B leadsTo B' |]     ==> F : (A Un B) leadsTo (A' Un B')";
  23.229  by (blast_tac (claset() addIs [leadsTo_Un, 
  23.230  			       leadsTo_weaken_R]) 1);
  23.231  qed "leadsTo_Un_Un";
  23.232 @@ -221,27 +221,27 @@
  23.233  
  23.234  (** The cancellation law **)
  23.235  
  23.236 -Goal "[| F : leadsTo A (A' Un B); F : leadsTo B B' |] \
  23.237 -\   ==> F : leadsTo A (A' Un B')";
  23.238 +Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
  23.239 +\   ==> F : A leadsTo (A' Un B')";
  23.240  by (blast_tac (claset() addIs [leadsTo_Un_Un, 
  23.241  			       subset_imp_leadsTo, leadsTo_Trans]) 1);
  23.242  qed "leadsTo_cancel2";
  23.243  
  23.244 -Goal "[| F : leadsTo A (A' Un B); F : leadsTo (B-A') B' |] \
  23.245 -\   ==> F : leadsTo A (A' Un B')";
  23.246 +Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
  23.247 +\   ==> F : A leadsTo (A' Un B')";
  23.248  by (rtac leadsTo_cancel2 1);
  23.249  by (assume_tac 2);
  23.250  by (ALLGOALS Asm_simp_tac);
  23.251  qed "leadsTo_cancel_Diff2";
  23.252  
  23.253 -Goal "[| F : leadsTo A (B Un A'); F : leadsTo B B' |] \
  23.254 -\   ==> F : leadsTo A (B' Un A')";
  23.255 +Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
  23.256 +\   ==> F : A leadsTo (B' Un A')";
  23.257  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  23.258  by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
  23.259  qed "leadsTo_cancel1";
  23.260  
  23.261 -Goal "[| F : leadsTo A (B Un A'); F : leadsTo (B-A') B' |] \
  23.262 -\   ==> F : leadsTo A (B' Un A')";
  23.263 +Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
  23.264 +\   ==> F : A leadsTo (B' Un A')";
  23.265  by (rtac leadsTo_cancel1 1);
  23.266  by (assume_tac 2);
  23.267  by (ALLGOALS Asm_simp_tac);
  23.268 @@ -251,14 +251,14 @@
  23.269  
  23.270  (** The impossibility law **)
  23.271  
  23.272 -Goal "F : leadsTo A B ==> B={} --> A={}";
  23.273 +Goal "F : A leadsTo B ==> B={} --> A={}";
  23.274  by (etac leadsTo_induct 1);
  23.275  by (ALLGOALS Asm_simp_tac);
  23.276  by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  23.277  by (Blast_tac 1);
  23.278  val lemma = result() RS mp;
  23.279  
  23.280 -Goal "F : leadsTo A {} ==> A={}";
  23.281 +Goal "F : A leadsTo {} ==> A={}";
  23.282  by (blast_tac (claset() addSIs [lemma]) 1);
  23.283  qed "leadsTo_empty";
  23.284  
  23.285 @@ -267,8 +267,8 @@
  23.286  
  23.287  (*Special case of PSP: Misra's "stable conjunction"*)
  23.288  Goalw [stable_def]
  23.289 -   "[| F : leadsTo A A'; F : stable B |] \
  23.290 -\   ==> F : leadsTo (A Int B) (A' Int B)";
  23.291 +   "[| F : A leadsTo A'; F : stable B |] \
  23.292 +\   ==> F : (A Int B) leadsTo (A' Int B)";
  23.293  by (etac leadsTo_induct 1);
  23.294  by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
  23.295  by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  23.296 @@ -279,19 +279,19 @@
  23.297  by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
  23.298  qed "psp_stable";
  23.299  
  23.300 -Goal "[| F : leadsTo A A'; F : stable B |] \
  23.301 -\   ==> F : leadsTo (B Int A) (B Int A')";
  23.302 +Goal "[| F : A leadsTo A'; F : stable B |] \
  23.303 +\   ==> F : (B Int A) leadsTo (B Int A')";
  23.304  by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
  23.305  qed "psp_stable2";
  23.306  
  23.307  Goalw [ensures_def, constrains_def]
  23.308 -   "[| F : ensures A A'; F : constrains B B' |] \
  23.309 -\   ==> F : ensures (A Int B) ((A' Int B) Un (B' - B))";
  23.310 +   "[| F : A ensures A'; F : B co B' |] \
  23.311 +\   ==> F : (A Int B) ensures ((A' Int B) Un (B' - B))";
  23.312  by (blast_tac (claset() addIs [transient_strengthen]) 1);
  23.313  qed "psp_ensures";
  23.314  
  23.315 -Goal "[| F : leadsTo A A'; F : constrains B B' |] \
  23.316 -\     ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))";
  23.317 +Goal "[| F : A leadsTo A'; F : B co B' |] \
  23.318 +\     ==> F : (A Int B) leadsTo ((A' Int B) Un (B' - B))";
  23.319  by (etac leadsTo_induct 1);
  23.320  by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
  23.321  (*Transitivity case has a delicate argument involving "cancellation"*)
  23.322 @@ -302,15 +302,15 @@
  23.323  by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
  23.324  qed "psp";
  23.325  
  23.326 -Goal "[| F : leadsTo A A'; F : constrains B B' |] \
  23.327 -\   ==> F : leadsTo (B Int A) ((B Int A') Un (B' - B))";
  23.328 +Goal "[| F : A leadsTo A'; F : B co B' |] \
  23.329 +\   ==> F : (B Int A) leadsTo ((B Int A') Un (B' - B))";
  23.330  by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
  23.331  qed "psp2";
  23.332  
  23.333  
  23.334  Goalw [unless_def]
  23.335 -   "[| F : leadsTo A A';  F : unless B B' |] \
  23.336 -\   ==> F : leadsTo (A Int B) ((A' Int B) Un B')";
  23.337 +   "[| F : A leadsTo A';  F : B unless B' |] \
  23.338 +\   ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
  23.339  by (dtac psp 1);
  23.340  by (assume_tac 1);
  23.341  by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1);
  23.342 @@ -325,11 +325,11 @@
  23.343  (** The most general rule: r is any wf relation; f is any variant function **)
  23.344  
  23.345  Goal "[| wf r;     \
  23.346 -\        ALL m. F : leadsTo (A Int f-``{m})                     \
  23.347 +\        ALL m. F : (A Int f-``{m}) leadsTo                     \
  23.348  \                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  23.349 -\     ==> F : leadsTo (A Int f-``{m}) B";
  23.350 +\     ==> F : (A Int f-``{m}) leadsTo B";
  23.351  by (eres_inst_tac [("a","m")] wf_induct 1);
  23.352 -by (subgoal_tac "F : leadsTo (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
  23.353 +by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
  23.354  by (stac vimage_eq_UN 2);
  23.355  by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
  23.356  by (blast_tac (claset() addIs [leadsTo_UN]) 2);
  23.357 @@ -339,9 +339,9 @@
  23.358  
  23.359  (** Meta or object quantifier ????? **)
  23.360  Goal "[| wf r;     \
  23.361 -\        ALL m. F : leadsTo (A Int f-``{m})                     \
  23.362 +\        ALL m. F : (A Int f-``{m}) leadsTo                     \
  23.363  \                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  23.364 -\     ==> F : leadsTo A B";
  23.365 +\     ==> F : A leadsTo B";
  23.366  by (res_inst_tac [("t", "A")] subst 1);
  23.367  by (rtac leadsTo_UN 2);
  23.368  by (etac lemma 2);
  23.369 @@ -351,9 +351,9 @@
  23.370  
  23.371  
  23.372  Goal "[| wf r;     \
  23.373 -\        ALL m:I. F : leadsTo (A Int f-``{m})                   \
  23.374 +\        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
  23.375  \                              ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  23.376 -\     ==> F : leadsTo A ((A - (f-``I)) Un B)";
  23.377 +\     ==> F : A leadsTo ((A - (f-``I)) Un B)";
  23.378  by (etac leadsTo_wf_induct 1);
  23.379  by Safe_tac;
  23.380  by (case_tac "m:I" 1);
  23.381 @@ -362,26 +362,26 @@
  23.382  qed "bounded_induct";
  23.383  
  23.384  
  23.385 -(*Alternative proof is via the lemma F : leadsTo (A Int f-``(lessThan m)) B*)
  23.386 -Goal "[| ALL m. F : leadsTo (A Int f-``{m})                     \
  23.387 +(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
  23.388 +Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
  23.389  \                            ((A Int f-``(lessThan m)) Un B) |] \
  23.390 -\     ==> F : leadsTo A B";
  23.391 +\     ==> F : A leadsTo B";
  23.392  by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
  23.393  by (Asm_simp_tac 1);
  23.394  qed "lessThan_induct";
  23.395  
  23.396 -Goal "[| ALL m:(greaterThan l). F : leadsTo (A Int f-``{m})   \
  23.397 +Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) leadsTo   \
  23.398  \                                  ((A Int f-``(lessThan m)) Un B) |] \
  23.399 -\     ==> F : leadsTo A ((A Int (f-``(atMost l))) Un B)";
  23.400 +\     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
  23.401  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
  23.402  			       Compl_greaterThan RS sym]) 1);
  23.403  by (rtac (wf_less_than RS bounded_induct) 1);
  23.404  by (Asm_simp_tac 1);
  23.405  qed "lessThan_bounded_induct";
  23.406  
  23.407 -Goal "[| ALL m:(lessThan l). F : leadsTo (A Int f-``{m})   \
  23.408 +Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) leadsTo   \
  23.409  \                              ((A Int f-``(greaterThan m)) Un B) |] \
  23.410 -\     ==> F : leadsTo A ((A Int (f-``(atLeast l))) Un B)";
  23.411 +\     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
  23.412  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  23.413      (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
  23.414  by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  23.415 @@ -396,16 +396,16 @@
  23.416  (*** wlt ****)
  23.417  
  23.418  (*Misra's property W3*)
  23.419 -Goalw [wlt_def] "F : leadsTo (wlt F B) B";
  23.420 +Goalw [wlt_def] "F : (wlt F B) leadsTo B";
  23.421  by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  23.422  qed "wlt_leadsTo";
  23.423  
  23.424 -Goalw [wlt_def] "F : leadsTo A B ==> A <= wlt F B";
  23.425 +Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B";
  23.426  by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  23.427  qed "leadsTo_subset";
  23.428  
  23.429  (*Misra's property W2*)
  23.430 -Goal "F : leadsTo A B = (A <= wlt F B)";
  23.431 +Goal "F : A leadsTo B = (A <= wlt F B)";
  23.432  by (blast_tac (claset() addSIs [leadsTo_subset, 
  23.433  				wlt_leadsTo RS leadsTo_weaken_L]) 1);
  23.434  qed "leadsTo_eq_subset_wlt";
  23.435 @@ -420,17 +420,17 @@
  23.436  (*Used in the Trans case below*)
  23.437  Goalw [constrains_def]
  23.438     "[| B <= A2;  \
  23.439 -\      F : constrains (A1 - B) (A1 Un B); \
  23.440 -\      F : constrains (A2 - C) (A2 Un C) |] \
  23.441 -\   ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
  23.442 +\      F : (A1 - B) co (A1 Un B); \
  23.443 +\      F : (A2 - C) co (A2 Un C) |] \
  23.444 +\   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
  23.445  by (Clarify_tac 1);
  23.446  by (Blast_tac 1);
  23.447  val lemma1 = result();
  23.448  
  23.449  
  23.450  (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
  23.451 -Goal "F : leadsTo A A' ==> \
  23.452 -\     EX B. A<=B & F : leadsTo B A' & F : constrains (B-A') (B Un A')";
  23.453 +Goal "F : A leadsTo A' ==> \
  23.454 +\     EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
  23.455  by (etac leadsTo_induct 1);
  23.456  (*Basis*)
  23.457  by (blast_tac (claset() addIs [leadsTo_Basis]
  23.458 @@ -449,7 +449,7 @@
  23.459  
  23.460  
  23.461  (*Misra's property W5*)
  23.462 -Goal "F : constrains (wlt F B - B) (wlt F B)";
  23.463 +Goal "F : (wlt F B - B) co (wlt F B)";
  23.464  by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
  23.465  by (Clarify_tac 1);
  23.466  by (subgoal_tac "Ba = wlt F B" 1);
  23.467 @@ -461,29 +461,29 @@
  23.468  
  23.469  (*** Completion: Binary and General Finite versions ***)
  23.470  
  23.471 -Goal "[| F : leadsTo A A';  F : stable A';   \
  23.472 -\        F : leadsTo B B';  F : stable B' |] \
  23.473 -\   ==> F : leadsTo (A Int B) (A' Int B')";
  23.474 +Goal "[| F : A leadsTo A';  F : stable A';   \
  23.475 +\        F : B leadsTo B';  F : stable B' |] \
  23.476 +\   ==> F : (A Int B) leadsTo (A' Int B')";
  23.477  by (subgoal_tac "F : stable (wlt F B')" 1);
  23.478  by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
  23.479  by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
  23.480  	   rtac wlt_constrains_wlt 2,
  23.481  	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
  23.482  	   Blast_tac 2]);
  23.483 -by (subgoal_tac "F : leadsTo (A Int wlt F B') (A' Int wlt F B')" 1);
  23.484 +by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1);
  23.485  by (blast_tac (claset() addIs [psp_stable]) 2);
  23.486 -by (subgoal_tac "F : leadsTo (A' Int wlt F B') (A' Int B')" 1);
  23.487 +by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1);
  23.488  by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
  23.489 -by (subgoal_tac "F : leadsTo (A Int B) (A Int wlt F B')" 1);
  23.490 +by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1);
  23.491  by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
  23.492  			       subset_imp_leadsTo]) 2);
  23.493  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
  23.494  qed "stable_completion";
  23.495  
  23.496  
  23.497 -Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i)) -->  \
  23.498 +Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) -->  \
  23.499  \                  (ALL i:I. F : stable (A' i)) -->         \
  23.500 -\                  F : leadsTo (INT i:I. A i) (INT i:I. A' i)";
  23.501 +\                  F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
  23.502  by (etac finite_induct 1);
  23.503  by (Asm_simp_tac 1);
  23.504  by (asm_simp_tac 
  23.505 @@ -493,20 +493,20 @@
  23.506  
  23.507  
  23.508  Goal "[| W = wlt F (B' Un C);     \
  23.509 -\      F : leadsTo A (A' Un C);  F : constrains A' (A' Un C);   \
  23.510 -\      F : leadsTo B (B' Un C);  F : constrains B' (B' Un C) |] \
  23.511 -\   ==> F : leadsTo (A Int B) ((A' Int B') Un C)";
  23.512 -by (subgoal_tac "F : constrains (W-C) (W Un B' Un C)" 1);
  23.513 +\      F : A leadsTo (A' Un C);  F : A' co (A' Un C);   \
  23.514 +\      F : B leadsTo (B' Un C);  F : B' co (B' Un C) |] \
  23.515 +\   ==> F : (A Int B) leadsTo ((A' Int B') Un C)";
  23.516 +by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
  23.517  by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
  23.518  			       MRS constrains_Un RS constrains_weaken]) 2);
  23.519 -by (subgoal_tac "F : constrains (W-C) W" 1);
  23.520 +by (subgoal_tac "F : (W-C) co W" 1);
  23.521  by (asm_full_simp_tac 
  23.522      (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
  23.523 -by (subgoal_tac "F : leadsTo (A Int W - C) (A' Int W Un C)" 1);
  23.524 +by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
  23.525  by (simp_tac (simpset() addsimps [Int_Diff]) 2);
  23.526  by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
  23.527  (** LEVEL 7 **)
  23.528 -by (subgoal_tac "F : leadsTo (A' Int W Un C) (A' Int B' Un C)" 1);
  23.529 +by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
  23.530  by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
  23.531                                 psp2 RS leadsTo_weaken_R, 
  23.532  			       subset_refl RS subset_imp_leadsTo, 
  23.533 @@ -520,9 +520,9 @@
  23.534  bind_thm("completion", refl RS result());
  23.535  
  23.536  
  23.537 -Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i Un C)) -->  \
  23.538 -\                  (ALL i:I. F : constrains (A' i) (A' i Un C)) --> \
  23.539 -\                  F : leadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
  23.540 +Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->  \
  23.541 +\                  (ALL i:I. F : (A' i) co (A' i Un C)) --> \
  23.542 +\                  F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
  23.543  by (etac finite_induct 1);
  23.544  by (ALLGOALS Asm_simp_tac);
  23.545  by (Clarify_tac 1);
    24.1 --- a/src/HOL/UNITY/WFair.thy	Wed Apr 28 13:36:31 1999 +0200
    24.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Apr 29 10:51:58 1999 +0200
    24.3 @@ -17,16 +17,22 @@
    24.4    transient :: "'a set => 'a program set"
    24.5      "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
    24.6  
    24.7 -  ensures :: "['a set, 'a set] => 'a program set"
    24.8 -    "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
    24.9 +
   24.10 +consts
   24.11 +
   24.12 +  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
   24.13  
   24.14 +  (*LEADS-TO constant for the inductive definition*)
   24.15 +  leadsto :: "'a program => ('a set * 'a set) set"
   24.16  
   24.17 -consts leadsto :: "'a program => ('a set * 'a set) set"
   24.18 +  (*visible version of the LEADS-TO relation*)
   24.19 +  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
   24.20 +
   24.21    
   24.22  inductive "leadsto F"
   24.23    intrs 
   24.24  
   24.25 -    Basis  "F : ensures A B ==> (A,B) : leadsto F"
   24.26 +    Basis  "F : A ensures B ==> (A,B) : leadsto F"
   24.27  
   24.28      Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
   24.29  	   ==> (A,C) : leadsto F"
   24.30 @@ -40,12 +46,15 @@
   24.31  
   24.32  
   24.33    
   24.34 -constdefs (*visible version of the relation*)
   24.35 -  leadsTo :: "['a set, 'a set] => 'a program set"
   24.36 -    "leadsTo A B == {F. (A,B) : leadsto F}"
   24.37 +defs
   24.38 +  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
   24.39 +
   24.40 +  leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
   24.41 +
   24.42 +constdefs
   24.43    
   24.44    (*wlt F B is the largest set that leads to B*)
   24.45    wlt :: "['a program, 'a set] => 'a set"
   24.46 -    "wlt F B == Union {A. F: leadsTo A B}"
   24.47 +    "wlt F B == Union {A. F: A leadsTo B}"
   24.48  
   24.49  end