working shapshot with "projecting" and "extending"
authorpaulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826c6a8b73b6c2a
parent 7825 1be9b63e7d93
child 7827 c9c615d970db
working shapshot with "projecting" and "extending"
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -71,6 +71,16 @@
     1.4  qed "inv_sysOfAlloc_eq";
     1.5  Addsimps [inv_sysOfAlloc_eq];
     1.6  
     1.7 +
     1.8 +(*SHOULD NOT BE NECESSARY????????????????
     1.9 +Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \
    1.10 +\             allocRel = allocRel z |) = z";
    1.11 +by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.12 +	      simpset()));
    1.13 +qed "allocState_eq";
    1.14 +Addsimps [allocState_eq];
    1.15 +????*)
    1.16 +
    1.17  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.18     state need to be treated symmetrically or done automatically*)
    1.19  Goalw [sysOfClient_def] "inj sysOfClient";
    1.20 @@ -183,15 +193,14 @@
    1.21  AddIffs [Network_component_System, Alloc_component_System];
    1.22  
    1.23  
    1.24 -fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.25 +fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
    1.26  
    1.27 -fun client_export th = good_map_sysOfClient RS export th;
    1.28 +fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
    1.29  
    1.30  (* F : UNIV guarantees Increasing func
    1.31     ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
    1.32  val extend_Client_guar_Increasing =
    1.33 -  client_export extend_guar_Increasing
    1.34 -  |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
    1.35 +  client_export extend_guar_Increasing;
    1.36  
    1.37  (*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
    1.38  Goal "i < Nclients \
    1.39 @@ -221,6 +230,8 @@
    1.40  			       System_Increasing_rel]) 1);
    1.41  qed "System_Increasing_allocRel";
    1.42  
    1.43 +
    1.44 +
    1.45  (*safety (1), step 3*)
    1.46  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
    1.47  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
    1.48 @@ -230,14 +241,14 @@
    1.49  by (rtac Alloc_component_System 3);
    1.50  by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
    1.51  by (rtac (Alloc_Safety RS project_guarantees) 1);
    1.52 +(*1: Increasing precondition*)
    1.53 +br (ballI RS projecting_INT) 1;
    1.54 +by (rtac (alloc_export projecting_Increasing RS projecting_weaken) 1);
    1.55  by Auto_tac;
    1.56 -(*1: Increasing precondition*)
    1.57 -by (stac (alloc_export project_Increasing) 1);
    1.58 -by (force_tac
    1.59 -    (claset(),
    1.60 -     simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
    1.61 +by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
    1.62  (*2: Always postcondition*)
    1.63 -by (dtac (subset_refl RS alloc_export project_Always_D) 1);
    1.64 +by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
    1.65 +by Auto_tac;
    1.66  by (asm_full_simp_tac
    1.67       (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
    1.68  qed "System_sum_bounded";
     2.1 --- a/src/HOL/UNITY/Client.ML	Mon Oct 11 10:52:51 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Client.ML	Mon Oct 11 10:53:39 1999 +0200
     2.3 @@ -114,6 +114,7 @@
     2.4  by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
     2.5  	               addIs [Increasing_localTo_Stable, 
     2.6  			      stable_size_rel_le_giv]) 2);
     2.7 +by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
     2.8  by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
     2.9  	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
    2.10  			      stable_size_ask_le_rel]) 1);
    2.11 @@ -133,7 +134,7 @@
    2.12  	       simpset()) 1);
    2.13  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    2.14  by (Blast_tac 1);
    2.15 -by (auto_tac (claset(), 
    2.16 -	      simpset() addsimps [Always_eq_includes_reachable, giv_meets_ask_def]));
    2.17 -by (ALLGOALS Force_tac);
    2.18 +by (force_tac (claset(), 
    2.19 +	       simpset() addsimps [Always_eq_includes_reachable, 
    2.20 +				  giv_meets_ask_def]) 1);
    2.21  qed "client_correct";
     3.1 --- a/src/HOL/UNITY/Common.ML	Mon Oct 11 10:52:51 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Common.ML	Mon Oct 11 10:53:39 1999 +0200
     3.3 @@ -40,7 +40,6 @@
     3.4  \      : {m} co (maxfg m)";
     3.5  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
     3.6  				  le_max_iff_disj, fasc]) 1);
     3.7 -by (Blast_tac 1);
     3.8  result();
     3.9  
    3.10  (*This one is  t := max (ftime t) (gtime t)*)
    3.11 @@ -48,7 +47,6 @@
    3.12  \      : {m} co (maxfg m)";
    3.13  by (simp_tac 
    3.14      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    3.15 -by (Blast_tac 1);
    3.16  result();
    3.17  
    3.18  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    3.19 @@ -56,7 +54,6 @@
    3.20  \      : {m} co (maxfg m)";
    3.21  by (simp_tac 
    3.22      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    3.23 -by (blast_tac (claset() addIs [Suc_leI]) 1);
    3.24  result();
    3.25  
    3.26  
     4.1 --- a/src/HOL/UNITY/Extend.ML	Mon Oct 11 10:52:51 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Oct 11 10:53:39 1999 +0200
     4.3 @@ -70,12 +70,17 @@
     4.4  by (Blast_tac 1);
     4.5  qed "extend_set_mono";
     4.6  
     4.7 -Goalw [extend_set_def]
     4.8 -     "z : extend_set h A = (f z : A)";
     4.9 +Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
    4.10  by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
    4.11  qed "mem_extend_set_iff";
    4.12  AddIffs [mem_extend_set_iff]; 
    4.13  
    4.14 +Goalw [extend_set_def]
    4.15 +    "(extend_set h A <= extend_set h B) = (A <= B)";
    4.16 +by (Force_tac 1);
    4.17 +qed "extend_set_strict_mono";
    4.18 +AddIffs [extend_set_strict_mono];
    4.19 +
    4.20  Goal "{s. P (f s)} = extend_set h {s. P s}";
    4.21  by Auto_tac;
    4.22  qed "Collect_eq_extend_set";
    4.23 @@ -177,6 +182,12 @@
    4.24  qed "extend_act_inverse";
    4.25  Addsimps [extend_act_inverse];
    4.26  
    4.27 +(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
    4.28 +Goalw [extend_act_def, project_act_def]
    4.29 +     "act' <= extend_act h act ==> project_act C h act' <= act";
    4.30 +by (Force_tac 1);
    4.31 +qed "subset_extend_act_D";
    4.32 +
    4.33  Goal "inj (extend_act h)";
    4.34  by (rtac inj_on_inverseI 1);
    4.35  by (rtac extend_act_inverse 1);
    4.36 @@ -189,11 +200,12 @@
    4.37  qed "extend_act_Image";
    4.38  Addsimps [extend_act_Image];
    4.39  
    4.40 -Goalw [extend_set_def, extend_act_def]
    4.41 -    "(extend_set h A <= extend_set h B) = (A <= B)";
    4.42 -by (Force_tac 1);
    4.43 -qed "extend_set_strict_mono";
    4.44 -Addsimps [extend_set_strict_mono];
    4.45 +Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)";
    4.46 +by Auto_tac;
    4.47 +qed "extend_act_strict_mono";
    4.48 +
    4.49 +AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq];
    4.50 +(*The latter theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)
    4.51  
    4.52  Goalw [extend_set_def, extend_act_def]
    4.53      "Domain (extend_act h act) = extend_set h (Domain act)";
    4.54 @@ -226,6 +238,12 @@
    4.55  
    4.56  Addsimps [extend_act_Id, project_act_Id];
    4.57  
    4.58 +Goal "(extend_act h act = Id) = (act = Id)";
    4.59 +by Auto_tac;
    4.60 +by (rewtac extend_act_def);
    4.61 +by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
    4.62 +qed "extend_act_Id_iff";
    4.63 +
    4.64  Goal "Id : extend_act h `` Acts F";
    4.65  by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
    4.66  	      simpset() addsimps [image_iff]));
    4.67 @@ -326,26 +344,56 @@
    4.68  by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
    4.69  qed "extend_invariant";
    4.70  
    4.71 +(*Converse fails: A and B may differ in their extra variables*)
    4.72 +Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
    4.73 +by (auto_tac (claset(), 
    4.74 +	      simpset() addsimps [constrains_def, project_set_def]));
    4.75 +by (Force_tac 1);
    4.76 +qed "extend_constrains_project_set";
    4.77 +
    4.78  
    4.79  (*** Diff, needed for localTo ***)
    4.80  
    4.81  Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
    4.82  by (auto_tac (claset() addSIs [program_equalityI],
    4.83  	      simpset() addsimps [Diff_def,
    4.84 -				  inj_extend_act RS image_set_diff RS sym]));
    4.85 +				  inj_extend_act RS image_set_diff]));
    4.86  qed "Diff_extend_eq";
    4.87  
    4.88  Goal "(Diff (extend h G) (extend_act h `` acts) \
    4.89  \         : (extend_set h A) co (extend_set h B)) \
    4.90  \     = (Diff G acts : A co B)";
    4.91  by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
    4.92 -qed "Diff_extend_co";
    4.93 +qed "Diff_extend_constrains";
    4.94  
    4.95  Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
    4.96  \     = (Diff G acts : stable A)";
    4.97 -by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1);
    4.98 +by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
    4.99  qed "Diff_extend_stable";
   4.100  
   4.101 +Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
   4.102 +\     ==> Diff G acts : (project_set h A) co (project_set h B)";
   4.103 +by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
   4.104 +					   extend_constrains_project_set]) 1);
   4.105 +qed "Diff_extend_constrains_project_set";
   4.106 +
   4.107 +Goalw [localTo_def]
   4.108 +     "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
   4.109 +by (simp_tac (simpset() addsimps []) 1);
   4.110 +(*A trick to strip both quantifiers*)
   4.111 +by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
   4.112 +by (stac Collect_eq_extend_set 1);
   4.113 +by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
   4.114 +qed "extend_localTo_extend_eq";
   4.115 +
   4.116 +Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
   4.117 +by (simp_tac (simpset() addsimps [Disjoint_def,
   4.118 +				  inj_extend_act RS image_Int RS sym]) 1);
   4.119 +by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
   4.120 +by (blast_tac (claset() addEs [equalityE]) 1);
   4.121 +qed "Disjoint_extend_eq";
   4.122 +Addsimps [Disjoint_extend_eq];
   4.123 +
   4.124  (*** Weak safety primitives: Co, Stable ***)
   4.125  
   4.126  Goal "p : reachable (extend h F) ==> f p : reachable F";
     5.1 --- a/src/HOL/UNITY/Extend.thy	Mon Oct 11 10:52:51 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Extend.thy	Mon Oct 11 10:53:39 1999 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4      "project_set h C == {x. EX y. h(x,y) : C}"
     5.5  
     5.6    extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     5.7 -    "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
     5.8 +    "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
     5.9  
    5.10    (*Argument C allows weak safety laws to be projected*)
    5.11    project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
     6.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 11 10:52:51 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 11 10:53:39 1999 +0200
     6.3 @@ -3,13 +3,10 @@
     6.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5      Copyright   1998  University of Cambridge
     6.6  
     6.7 -THESE PROOFS CAN BE REPLACED BY INVOCATIONS OF RESULTS FROM EXTEND.ML
     6.8 +Arrays of processes.  Many results are instances of those in Extend & Project.
     6.9  *)
    6.10  
    6.11  
    6.12 -val image_eqI' = read_instantiate_sg (sign_of thy)
    6.13 -                     [("x", "?ff(i := ?u)")] image_eqI;
    6.14 -
    6.15  (*** Basic properties ***)
    6.16  
    6.17  (** lift_set and drop_set **)
    6.18 @@ -283,6 +280,13 @@
    6.19  	      simpset() addsimps [invariant_def, lift_prog_stable]));
    6.20  qed "lift_prog_invariant";
    6.21  
    6.22 +Goal "[| lift_prog i F : A co B |] \
    6.23 +\     ==> F : (drop_set i A) co (drop_set i B)";
    6.24 +by (asm_full_simp_tac
    6.25 +    (simpset() addsimps [drop_set_correct, lift_prog_correct, 
    6.26 +			 lift_export extend_constrains_project_set]) 1);
    6.27 +qed "lift_prog_constrains_drop_set";
    6.28 +
    6.29  (*This one looks strange!  Proof probably is by case analysis on i=j.
    6.30    If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
    6.31    premise ensures A<=B.*)
    6.32 @@ -316,14 +320,14 @@
    6.33  by (asm_full_simp_tac
    6.34      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
    6.35  			 lift_set_correct, lift_act_correct, 
    6.36 -			 lift_export Diff_project_co]) 1);
    6.37 -qed "Diff_drop_prog_co";
    6.38 +			 lift_export Diff_project_constrains]) 1);
    6.39 +qed "Diff_drop_prog_constrains";
    6.40  
    6.41  Goalw [stable_def]
    6.42       "[| (UN act:acts. Domain act) <= drop_set i C; \
    6.43  \        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
    6.44  \     ==> Diff (drop_prog C i G) acts : stable A";
    6.45 -by (etac Diff_drop_prog_co 1);
    6.46 +by (etac Diff_drop_prog_constrains 1);
    6.47  by (assume_tac 1);
    6.48  qed "Diff_drop_prog_stable";
    6.49  
    6.50 @@ -487,11 +491,3 @@
    6.51      (simpset() addsimps [lift_set_correct, lift_prog_correct, 
    6.52  			 lift_export extend_guar_Always]) 1);
    6.53  qed "lift_prog_guar_Always";
    6.54 -
    6.55 -(*No analogue of this in Extend.ML!*)
    6.56 -Goal "[| lift_prog i F : A co B |] \
    6.57 -\     ==> F : (drop_set i A) co (drop_set i B)";
    6.58 -by (auto_tac (claset(), 
    6.59 -	      simpset() addsimps [constrains_def, drop_set_def]));
    6.60 -by (force_tac (claset() addSIs [image_eqI'], simpset()) 1);
    6.61 -qed "lift_prog_constrains_drop_set";
     7.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Oct 11 10:52:51 1999 +0200
     7.2 +++ b/src/HOL/UNITY/PPROD.ML	Mon Oct 11 10:53:39 1999 +0200
     7.3 @@ -6,10 +6,13 @@
     7.4  Abstraction over replicated components (PLam)
     7.5  General products of programs (Pi operation)
     7.6  
     7.7 -It is not clear that any of this is good for anything.
     7.8 +Probably some dead wood here!
     7.9  *)
    7.10  
    7.11  
    7.12 +val image_eqI' = read_instantiate_sg (sign_of thy)
    7.13 +                     [("x", "?ff(i := ?u)")] image_eqI;
    7.14 +
    7.15  (*** Basic properties ***)
    7.16  
    7.17  Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
     8.1 --- a/src/HOL/UNITY/Project.ML	Mon Oct 11 10:52:51 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Project.ML	Mon Oct 11 10:53:39 1999 +0200
     8.3 @@ -108,13 +108,95 @@
     8.4  
     8.5  (*For using project_guarantees in particular cases*)
     8.6  Goal "extend h F Join G : extend_set h A co extend_set h B \
     8.7 -\     ==> F Join project UNIV h G : A co B";
     8.8 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
     8.9 +\     ==> F Join project C h G : A co B";
    8.10 +by (asm_full_simp_tac
    8.11 +    (simpset() addsimps [project_constrains, Join_constrains, 
    8.12 +			 extend_constrains]) 1);
    8.13 +by (blast_tac (claset() addIs [constrains_weaken]
    8.14 +			addDs [constrains_imp_subset]) 1);
    8.15 +qed "project_constrains_I";
    8.16 +
    8.17 +(*The UNIV argument is essential*)
    8.18 +Goal "F Join project UNIV h G : A co B \
    8.19 +\     ==> extend h F Join G : extend_set h A co extend_set h B";
    8.20  by (asm_full_simp_tac
    8.21      (simpset() addsimps [project_constrains, Join_constrains, 
    8.22  			 extend_constrains]) 1);
    8.23 -by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
    8.24 -qed "project_constrains_I";
    8.25 +qed "project_constrains_D";
    8.26 +
    8.27 +Goalw [projecting_def]
    8.28 +     "[| ALL i:I. projecting C h F (X' i) (X i) |] \
    8.29 +\     ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
    8.30 +by Auto_tac;
    8.31 +qed "projecting_INT";
    8.32 +
    8.33 +Goalw [projecting_def]
    8.34 +     "[| ALL i:I. projecting C h F (X' i) (X i) |] \
    8.35 +\     ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
    8.36 +by Auto_tac;
    8.37 +qed "projecting_UN";
    8.38 +
    8.39 +Goalw [projecting_def]
    8.40 +     "[| projecting C h F X' X;  U'<=X';  X<=U |] ==> projecting C h F U' U";
    8.41 +by Auto_tac;
    8.42 +qed "projecting_weaken";
    8.43 +
    8.44 +(*Is this the right way to handle the X' argument?*)
    8.45 +Goalw [extending_def]
    8.46 +     "[| ALL i:I. extending C h F (X' i) (Y' i) (Y i) |] \
    8.47 +\     ==> extending C h F (INT i:I. X' i) (INT i:I. Y' i) (INT i:I. Y i)";
    8.48 +by Auto_tac;
    8.49 +qed "extending_INT";
    8.50 +
    8.51 +Goalw [extending_def]
    8.52 +     "[| ALL i:I. extending C h F X' (Y' i) (Y i) |] \
    8.53 +\     ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
    8.54 +by Auto_tac;
    8.55 +qed "extending_UN";
    8.56 +
    8.57 +Goalw [extending_def]
    8.58 +     "[| extending C h F X' Y' Y;  U'<= X';  Y'<=V';  V<=Y |] \
    8.59 +\     ==> extending C h F U' V' V";
    8.60 +by Auto_tac;
    8.61 +qed "extending_weaken";
    8.62 +
    8.63 +Goal "projecting C h F X' UNIV";
    8.64 +by (simp_tac (simpset() addsimps [projecting_def]) 1);
    8.65 +qed "projecting_UNIV";
    8.66 +
    8.67 +Goalw [projecting_def]
    8.68 +     "projecting C h F (extend_set h A co extend_set h B) (A co B)";
    8.69 +by (blast_tac (claset() addIs [project_constrains_I]) 1);
    8.70 +qed "projecting_constrains";
    8.71 +
    8.72 +Goalw [stable_def]
    8.73 +     "projecting C h F (stable (extend_set h A)) (stable A)";
    8.74 +by (rtac projecting_constrains 1);
    8.75 +qed "projecting_stable";
    8.76 +
    8.77 +Goalw [projecting_def]
    8.78 +     "projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)";
    8.79 +by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
    8.80 +qed "projecting_increasing";
    8.81 +
    8.82 +Goal "extending C h F X' UNIV Y";
    8.83 +by (simp_tac (simpset() addsimps [extending_def]) 1);
    8.84 +qed "extending_UNIV";
    8.85 +
    8.86 +Goalw [extending_def]
    8.87 +     "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
    8.88 +by (blast_tac (claset() addIs [project_constrains_D]) 1);
    8.89 +qed "extending_constrains";
    8.90 +
    8.91 +Goalw [stable_def]
    8.92 +     "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
    8.93 +by (rtac extending_constrains 1);
    8.94 +qed "extending_stable";
    8.95 +
    8.96 +Goalw [extending_def]
    8.97 +     "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
    8.98 +by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
    8.99 +qed "extending_increasing";
   8.100  
   8.101  
   8.102  (*** Diff, needed for localTo ***)
   8.103 @@ -139,17 +221,19 @@
   8.104  by (ftac constrains_imp_subset 1);
   8.105  by (Asm_full_simp_tac 1);
   8.106  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   8.107 -qed "Diff_project_co";
   8.108 +qed "Diff_project_constrains";
   8.109  
   8.110  Goalw [stable_def]
   8.111       "[| (UN act:acts. Domain act) <= project_set h C; \
   8.112  \        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
   8.113  \     ==> Diff (project C h G) acts : stable A";
   8.114 -by (etac Diff_project_co 1);
   8.115 +by (etac Diff_project_constrains 1);
   8.116  by (assume_tac 1);
   8.117  qed "Diff_project_stable";
   8.118  
   8.119 -(*Converse appears to fail*)
   8.120 +(*Converse fails: even if the conclusion holds, H could modify (v o f) 
   8.121 +  simultaneously with other variables, and this action would not be 
   8.122 +  superseded by anything in (extend h G) *)
   8.123  Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
   8.124  \     ==> project C h H : func localTo G";
   8.125  by (asm_full_simp_tac 
   8.126 @@ -166,6 +250,11 @@
   8.127      (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
   8.128  qed "project_localTo_I";
   8.129  
   8.130 +Goalw [projecting_def]
   8.131 +     "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
   8.132 +by (blast_tac (claset() addIs [project_localTo_I]) 1);
   8.133 +qed "projecting_localTo";
   8.134 +
   8.135  
   8.136  (** Reachability and project **)
   8.137  
   8.138 @@ -243,7 +332,7 @@
   8.139  	      simpset() addsimps [project_set_def]));
   8.140  qed "project_set_reachable_extend_eq";
   8.141  
   8.142 -
   8.143 +(*Perhaps should replace C by reachable...*)
   8.144  Goalw [Constrains_def]
   8.145       "[| C <= reachable (extend h F Join G);  \
   8.146  \        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   8.147 @@ -274,7 +363,7 @@
   8.148  \        extend h F Join G : Always (extend_set h A) |]   \
   8.149  \     ==> F Join project C h G : Always A";
   8.150  by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
   8.151 -bws [project_set_def, extend_set_def];
   8.152 +by (rewrite_goals_tac [project_set_def, extend_set_def]);
   8.153  by (Blast_tac 1);
   8.154  qed "project_Always_I";
   8.155  
   8.156 @@ -305,6 +394,59 @@
   8.157  				      Collect_eq_extend_set RS sym]) 1);
   8.158  qed "project_Increasing";
   8.159  
   8.160 +(** A lot of redundant theorems: all are proved to facilitate reasoning
   8.161 +    about guarantees. **)
   8.162 +
   8.163 +Goalw [projecting_def]
   8.164 +     "projecting (%G. reachable (extend h F Join G)) h F \
   8.165 +\                (extend_set h A Co extend_set h B) (A Co B)";
   8.166 +by (blast_tac (claset() addIs [project_Constrains_I]) 1);
   8.167 +qed "projecting_Constrains";
   8.168 +
   8.169 +Goalw [Stable_def]
   8.170 +     "projecting (%G. reachable (extend h F Join G)) h F \
   8.171 +\                (Stable (extend_set h A)) (Stable A)";
   8.172 +by (rtac projecting_Constrains 1);
   8.173 +qed "projecting_Stable";
   8.174 +
   8.175 +Goalw [projecting_def]
   8.176 +     "projecting (%G. reachable (extend h F Join G)) h F \
   8.177 +\                (Always (extend_set h A)) (Always A)";
   8.178 +by (blast_tac (claset() addIs [project_Always_I]) 1);
   8.179 +qed "projecting_Always";
   8.180 +
   8.181 +Goalw [projecting_def]
   8.182 +     "projecting (%G. reachable (extend h F Join G)) h F \
   8.183 +\                (Increasing (func o f)) (Increasing func)";
   8.184 +by (blast_tac (claset() addIs [project_Increasing_I]) 1);
   8.185 +qed "projecting_Increasing";
   8.186 +
   8.187 +Goalw [extending_def]
   8.188 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   8.189 +\               (extend_set h A Co extend_set h B) (A Co B)";
   8.190 +by (blast_tac (claset() addIs [project_Constrains_D]) 1);
   8.191 +qed "extending_Constrains";
   8.192 +
   8.193 +Goalw [extending_def]
   8.194 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   8.195 +\               (Stable (extend_set h A)) (Stable A)";
   8.196 +by (blast_tac (claset() addIs [project_Stable_D]) 1);
   8.197 +qed "extending_Stable";
   8.198 +
   8.199 +Goalw [extending_def]
   8.200 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   8.201 +\               (Always (extend_set h A)) (Always A)";
   8.202 +by (blast_tac (claset() addIs [project_Always_D]) 1);
   8.203 +qed "extending_Always";
   8.204 +
   8.205 +val [prem] = 
   8.206 +Goalw [extending_def]
   8.207 +     "(!!G. reachable (extend h F Join G) <= C G)  \
   8.208 +\     ==> extending C h F X' \
   8.209 +\                   (Increasing (func o f)) (Increasing func)";
   8.210 +by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
   8.211 +qed "extending_Increasing";
   8.212 +
   8.213  
   8.214  (** Progress includes safety in the definition of ensures **)
   8.215  
   8.216 @@ -369,9 +511,8 @@
   8.217  by (Blast_tac 1);
   8.218  qed "ensures_extend_set_imp_project_ensures";
   8.219  
   8.220 -(*A super-strong condition: G is not allowed to affect the
   8.221 -  shared variables at all.*)
   8.222 -Goal "[| ALL x. project C h G ~: transient {x};  \
   8.223 +(*A strong condition: F can do anything that project G can.*)
   8.224 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   8.225  \        extend h F Join G : stable C;  \
   8.226  \        F Join project C h G : A ensures B |] \
   8.227  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
   8.228 @@ -387,7 +528,7 @@
   8.229  		       simpset()) 1));
   8.230  qed_spec_mp "Join_project_ensures";
   8.231  
   8.232 -Goal "[| ALL x. project C h G ~: transient {x};  \
   8.233 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   8.234  \        extend h F Join G : stable C;  \
   8.235  \        F Join project C h G : A leadsTo B |] \
   8.236  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   8.237 @@ -400,7 +541,7 @@
   8.238  qed "project_leadsTo_lemma";
   8.239  
   8.240  (*Instance of the previous theorem for STRONG progress*)
   8.241 -Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   8.242 +Goal "[| ALL D. project UNIV h G : transient D --> F : transient D;  \
   8.243  \        F Join project UNIV h G : A leadsTo B |] \
   8.244  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   8.245  by (dtac project_leadsTo_lemma 1);
   8.246 @@ -409,7 +550,7 @@
   8.247  
   8.248  (** Towards the analogous theorem for WEAK progress*)
   8.249  
   8.250 -Goal "[| ALL x. project C h G ~: transient {x};  \
   8.251 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   8.252  \        extend h F Join G : stable C;  \
   8.253  \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   8.254  \     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
   8.255 @@ -421,7 +562,7 @@
   8.256  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
   8.257  val lemma = result();
   8.258  
   8.259 -Goal "[| ALL x. project C h G ~: transient {x};  \
   8.260 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   8.261  \        extend h F Join G : stable C;  \
   8.262  \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   8.263  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   8.264 @@ -430,7 +571,7 @@
   8.265  val lemma2 = result();
   8.266  
   8.267  Goal "[| C = (reachable (extend h F Join G)); \
   8.268 -\        ALL x. project C h G ~: transient {x};  \
   8.269 +\        ALL D. project C h G : transient D --> F : transient D;  \
   8.270  \        F Join project C h G : A LeadsTo B |] \
   8.271  \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   8.272  by (asm_full_simp_tac 
   8.273 @@ -453,13 +594,11 @@
   8.274  
   8.275  Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
   8.276  \    ==> F : X guarantees Y";
   8.277 -by (rtac guaranteesI 1);
   8.278 -by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
   8.279 -by (dtac spec 1);
   8.280 -by (dtac (mp RS mp) 1);
   8.281 -by (Blast_tac 2);
   8.282 -by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
   8.283 -by Auto_tac;
   8.284 +by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
   8.285 +by (dres_inst_tac [("x", "extend h G")] spec 1);
   8.286 +by (asm_full_simp_tac 
   8.287 +    (simpset() delsimps [extend_Join] 
   8.288 +           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
   8.289  qed "extend_guarantees_imp_guarantees";
   8.290  
   8.291  Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
   8.292 @@ -471,17 +610,12 @@
   8.293  
   8.294  (*Weak precondition and postcondition; this is the good one!
   8.295    Not clear that it has a converse [or that we want one!]*)
   8.296 -val [xguary,project,extend] =
   8.297  Goal "[| F : X guarantees Y;  \
   8.298 -\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
   8.299 -\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
   8.300 -\                Disjoint (extend h F) G |] \
   8.301 -\             ==> extend h F Join G : Y' |] \
   8.302 +\        projecting C h F X' X;  extending C h F X' Y' Y |] \
   8.303  \     ==> extend h F : X' guarantees Y'";
   8.304 -by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
   8.305 -by (etac project 1);
   8.306 -by (assume_tac 1);
   8.307 -by (assume_tac 1);
   8.308 +by (rtac guaranteesI 1);
   8.309 +by (auto_tac (claset(), 
   8.310 +        simpset() addsimps [guaranteesD, projecting_def, extending_def]));
   8.311  qed "project_guarantees";
   8.312  
   8.313  (** It seems that neither "guarantees" law can be proved from the other. **)
   8.314 @@ -489,17 +623,20 @@
   8.315  
   8.316  (*** guarantees corollaries ***)
   8.317  
   8.318 +(** Most could be deleted: the required versions are easy to prove **)
   8.319 +
   8.320  Goal "F : UNIV guarantees increasing func \
   8.321 -\     ==> extend h F : UNIV guarantees increasing (func o f)";
   8.322 +\     ==> extend h F : X' guarantees increasing (func o f)";
   8.323  by (etac project_guarantees 1);
   8.324 -by (ALLGOALS
   8.325 -    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
   8.326 +by (rtac extending_increasing 2);
   8.327 +by (rtac projecting_UNIV 1);
   8.328  qed "extend_guar_increasing";
   8.329  
   8.330  Goal "F : UNIV guarantees Increasing func \
   8.331 -\     ==> extend h F : UNIV guarantees Increasing (func o f)";
   8.332 +\     ==> extend h F : X' guarantees Increasing (func o f)";
   8.333  by (etac project_guarantees 1);
   8.334 -by (rtac (subset_UNIV RS project_Increasing_D) 2);
   8.335 +by (rtac extending_Increasing 2);
   8.336 +by (rtac projecting_UNIV 1);
   8.337  by Auto_tac;
   8.338  qed "extend_guar_Increasing";
   8.339  
   8.340 @@ -507,30 +644,42 @@
   8.341  \     ==> extend h F : (v o f) localTo (extend h G)  \
   8.342  \                      guarantees increasing (func o f)";
   8.343  by (etac project_guarantees 1);
   8.344 -(*the "increasing" guarantee*)
   8.345 -by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
   8.346 -by (etac project_localTo_I 1);
   8.347 +by (rtac extending_increasing 2);
   8.348 +by (rtac projecting_localTo 1);
   8.349  qed "extend_localTo_guar_increasing";
   8.350  
   8.351  Goal "F : (v localTo G) guarantees Increasing func  \
   8.352  \     ==> extend h F : (v o f) localTo (extend h G)  \
   8.353  \                      guarantees Increasing (func o f)";
   8.354  by (etac project_guarantees 1);
   8.355 -(*the "Increasing" guarantee*)
   8.356 -by (etac (subset_UNIV RS project_Increasing_D) 2);
   8.357 -by (etac project_localTo_I 1);
   8.358 +by (rtac extending_Increasing 2);
   8.359 +by (rtac projecting_localTo 1);
   8.360 +by Auto_tac;
   8.361  qed "extend_localTo_guar_Increasing";
   8.362  
   8.363  Goal "F : Always A guarantees Always B \
   8.364  \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
   8.365  by (etac project_guarantees 1);
   8.366 -by (etac (subset_refl RS project_Always_D) 2);
   8.367 -by (etac (subset_refl RS project_Always_I) 1);
   8.368 +by (rtac extending_Always 2);
   8.369 +by (rtac projecting_Always 1);
   8.370  qed "extend_guar_Always";
   8.371  
   8.372  
   8.373  (** Guarantees with a leadsTo postcondition **)
   8.374  
   8.375 +(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
   8.376 +Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
   8.377 +\     ==> F : transient D";
   8.378 +by (case_tac "D={}" 1);
   8.379 +by (auto_tac (claset() addIs [transient_strengthen], simpset()));
   8.380 +qed "transient_lemma";
   8.381 +
   8.382 +
   8.383 +(*Previously tried to prove
   8.384 +[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
   8.385 +but it can fail if C removes some parts of an action of G.*)
   8.386 +
   8.387 +
   8.388  Goal "[| G : f localTo extend h F; \
   8.389  \        Disjoint (extend h F) G |] ==> project C h G : stable {x}";
   8.390  by (asm_full_simp_tac
   8.391 @@ -544,31 +693,50 @@
   8.392  				  stable_def, constrains_def]));
   8.393  qed "stable_sing_imp_not_transient";
   8.394  
   8.395 +by (auto_tac (claset(), 
   8.396 +	      simpset() addsimps [FP_def, transient_def,
   8.397 +				  stable_def, constrains_def]));
   8.398 +qed "stable_sing_imp_not_transient";
   8.399 +
   8.400  Goal "[| F Join project UNIV h G : A leadsTo B;    \
   8.401 -\        extend h F Join G : f localTo extend h F; \
   8.402 +\        G : f localTo extend h F; \
   8.403  \        Disjoint (extend h F) G |]  \
   8.404  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   8.405  by (rtac project_UNIV_leadsTo_lemma 1);
   8.406 -by Auto_tac;
   8.407 -by (asm_full_simp_tac
   8.408 -    (simpset() addsimps [Join_localTo, self_localTo,
   8.409 -			 localTo_imp_project_stable, 
   8.410 -			 stable_sing_imp_not_transient]) 1);
   8.411 +by (Clarify_tac 1);
   8.412 +by (rtac transient_lemma 1);
   8.413 +by (auto_tac (claset(), 
   8.414 +	      simpset() addsimps [localTo_imp_project_stable, 
   8.415 +				  stable_sing_imp_not_transient]));
   8.416  qed "project_leadsTo_D";
   8.417  
   8.418 -
   8.419  Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
   8.420 -\         extend h F Join G : f localTo extend h F; \
   8.421 -\         Disjoint (extend h F) G  |]  \
   8.422 +\         G : f localTo extend h F; \
   8.423 +\         Disjoint (extend h F) G |]  \
   8.424  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   8.425 -by (rtac Join_project_LeadsTo 1);
   8.426 -by Auto_tac;
   8.427 -by (asm_full_simp_tac
   8.428 -    (simpset() addsimps [Join_localTo, self_localTo,
   8.429 -			 localTo_imp_project_stable, 
   8.430 -			 stable_sing_imp_not_transient]) 1);
   8.431 +by (rtac (refl RS Join_project_LeadsTo) 1);
   8.432 +by (Clarify_tac 1);
   8.433 +by (rtac transient_lemma 1);
   8.434 +by (auto_tac (claset(), 
   8.435 +	      simpset() addsimps [localTo_imp_project_stable, 
   8.436 +				  stable_sing_imp_not_transient]));
   8.437  qed "project_LeadsTo_D";
   8.438  
   8.439 +Goalw [extending_def]
   8.440 +     "extending (%G. UNIV) h F \
   8.441 +\                (f localTo extend h F) \
   8.442 +\                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
   8.443 +by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
   8.444 +			addIs [project_leadsTo_D]) 1);
   8.445 +qed "extending_leadsTo";
   8.446 +
   8.447 +Goalw [extending_def]
   8.448 +     "extending (%G. reachable (extend h F Join G)) h F \
   8.449 +\                (f localTo extend h F) \
   8.450 +\                (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
   8.451 +by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
   8.452 +			addIs [project_LeadsTo_D]) 1);
   8.453 +qed "extending_LeadsTo";
   8.454  
   8.455  (*STRONG precondition and postcondition*)
   8.456  Goal "F : (A co A') guarantees (B leadsTo B')  \
   8.457 @@ -576,10 +744,9 @@
   8.458  \                   Int (f localTo (extend h F)) \
   8.459  \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
   8.460  by (etac project_guarantees 1);
   8.461 -(*the safety precondition*)
   8.462 -by (fast_tac (claset() addIs [project_constrains_I]) 1);
   8.463 -(*the liveness postcondition*)
   8.464 -by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
   8.465 +by (rtac (extending_leadsTo RS extending_weaken) 2);
   8.466 +by (rtac (projecting_constrains RS projecting_weaken) 1);
   8.467 +by Auto_tac;
   8.468  qed "extend_co_guar_leadsTo";
   8.469  
   8.470  (*WEAK precondition and postcondition*)
   8.471 @@ -588,10 +755,9 @@
   8.472  \                   Int (f localTo (extend h F)) \
   8.473  \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
   8.474  by (etac project_guarantees 1);
   8.475 -(*the safety precondition*)
   8.476 -by (fast_tac (claset() addIs [project_Constrains_I]) 1);
   8.477 -(*the liveness postcondition*)
   8.478 -by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
   8.479 +by (rtac (extending_LeadsTo RS extending_weaken) 2);
   8.480 +by (rtac (projecting_Constrains RS projecting_weaken) 1);
   8.481 +by Auto_tac;
   8.482  qed "extend_Co_guar_LeadsTo";
   8.483  
   8.484  Close_locale "Extend";
     9.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 11 10:52:51 1999 +0200
     9.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 11 10:53:39 1999 +0200
     9.3 @@ -8,4 +8,19 @@
     9.4  Inheritance of GUARANTEES properties under extension
     9.5  *)
     9.6  
     9.7 -Project = Extend
     9.8 +Project = Extend +
     9.9 +
    9.10 +constdefs
    9.11 +  projecting :: "['c program => 'c set, 'a*'b => 'c, 
    9.12 +		  'a program, 'c program set, 'a program set] => bool"
    9.13 +  "projecting C h F X' X ==
    9.14 +     ALL G. extend h F Join G : X' --> F Join project (C G) h G : X"
    9.15 +
    9.16 +  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    9.17 +		 'c program set, 'c program set, 'a program set] => bool"
    9.18 +  "extending C h F X' Y' Y ==
    9.19 +     ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
    9.20 +            Disjoint (extend h F) G
    9.21 +            --> extend h F Join G : Y'"
    9.22 +
    9.23 +end
    10.1 --- a/src/HOL/UNITY/UNITY.ML	Mon Oct 11 10:52:51 1999 +0200
    10.2 +++ b/src/HOL/UNITY/UNITY.ML	Mon Oct 11 10:53:39 1999 +0200
    10.3 @@ -133,10 +133,20 @@
    10.4  by (Blast_tac 1);
    10.5  qed "constrains_empty";
    10.6  
    10.7 +Goalw [constrains_def] "(F : A co {}) = (A={})";
    10.8 +by (Blast_tac 1);
    10.9 +qed "constrains_empty2";
   10.10 +
   10.11 +Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)";
   10.12 +by (Blast_tac 1);
   10.13 +qed "constrains_UNIV";
   10.14 +
   10.15  Goalw [constrains_def] "F : A co UNIV";
   10.16  by (Blast_tac 1);
   10.17 -qed "constrains_UNIV";
   10.18 -AddIffs [constrains_empty, constrains_UNIV];
   10.19 +qed "constrains_UNIV2";
   10.20 +
   10.21 +AddIffs [constrains_empty, constrains_empty2, 
   10.22 +	 constrains_UNIV, constrains_UNIV2];
   10.23  
   10.24  (*monotonic in 2nd argument*)
   10.25  Goalw [constrains_def]
   10.26 @@ -167,6 +177,22 @@
   10.27  by (Blast_tac 1);
   10.28  qed "ball_constrains_UN";
   10.29  
   10.30 +Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)";
   10.31 +by (Blast_tac 1);
   10.32 +qed "constrains_Un_distrib";
   10.33 +
   10.34 +Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)";
   10.35 +by (Blast_tac 1);
   10.36 +qed "constrains_UN_distrib";
   10.37 +
   10.38 +Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)";
   10.39 +by (Blast_tac 1);
   10.40 +qed "constrains_Int_distrib";
   10.41 +
   10.42 +Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)";
   10.43 +by (Blast_tac 1);
   10.44 +qed "constrains_INT_distrib";
   10.45 +
   10.46  (** Intersection **)
   10.47  
   10.48  Goalw [constrains_def]
    11.1 --- a/src/HOL/UNITY/Union.ML	Mon Oct 11 10:52:51 1999 +0200
    11.2 +++ b/src/HOL/UNITY/Union.ML	Mon Oct 11 10:53:39 1999 +0200
    11.3 @@ -307,22 +307,13 @@
    11.4  by Auto_tac;
    11.5  qed "Diff_Disjoint";
    11.6  
    11.7 -Goal "[| G : v localTo F;  Disjoint F G |] \
    11.8 -\     ==> G : stable {s. v s = z}";
    11.9 +Goal "[| G : v localTo F;  Disjoint F G |] ==> G : stable {s. v s = z}";
   11.10  by (asm_full_simp_tac 
   11.11      (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
   11.12  			 stable_def, constrains_def]) 1);
   11.13  by (Blast_tac 1);
   11.14  qed "localTo_imp_stable";
   11.15  
   11.16 -Goal "[| F Join G : v localTo F;  (s,s') : act;  \
   11.17 -\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
   11.18 -by (asm_full_simp_tac 
   11.19 -    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
   11.20 -			 stable_def, constrains_def]) 1);
   11.21 -by (Blast_tac 1);
   11.22 -qed "localTo_imp_equals";
   11.23 -
   11.24  Goalw [localTo_def, stable_def, constrains_def]
   11.25       "v localTo F <= (f o v) localTo F";
   11.26  by (Clarify_tac 1);
   11.27 @@ -350,46 +341,62 @@
   11.28  
   11.29  (*** Higher-level rules involving localTo and Join ***)
   11.30  
   11.31 +Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo F |]  \
   11.32 +\     ==> F Join G : {s. P (v s)} co {s. P' (v s)}";
   11.33 +by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
   11.34 +by (auto_tac (claset(), 
   11.35 +	      simpset() addsimps [localTo_def, stable_def, constrains_def,
   11.36 +				  Diff_def]));
   11.37 +by (case_tac "act: Acts F" 1);
   11.38 +by (Blast_tac 1);
   11.39 +by (dtac bspec 1 THEN rtac Id_in_Acts 1);
   11.40 +by (subgoal_tac "v x = v xa" 1);
   11.41 +by Auto_tac;
   11.42 +qed "constrains_localTo_constrains";
   11.43 +
   11.44 +Goalw [localTo_def, stable_def, constrains_def, Diff_def]
   11.45 +     "[| G : v localTo F;  G : w localTo F |]  \
   11.46 +\     ==> G : (%s. (v s, w s)) localTo F";
   11.47 +by (Blast_tac 1);
   11.48 +qed "localTo_pairfun";
   11.49 +
   11.50  Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
   11.51 -\        F Join G : v localTo F;       \
   11.52 -\        F Join G : w localTo F;       \
   11.53 -\        Disjoint F G |]               \
   11.54 +\        G : v localTo F;       \
   11.55 +\        G : w localTo F |]               \
   11.56  \     ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
   11.57 -by (auto_tac (claset(), simpset() addsimps [constrains_def]));
   11.58 -by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
   11.59 +by (res_inst_tac [("A", "{s. (%(x,y). P x y) (v s, w s)}"),
   11.60 +		  ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")] 
   11.61 +    constrains_weaken 1);
   11.62 +by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
   11.63  by Auto_tac;
   11.64  qed "constrains_localTo_constrains2";
   11.65  
   11.66  Goalw [stable_def]
   11.67       "[| F : stable {s. P (v s) (w s)};   \
   11.68 -\        F Join G : v localTo F;       \
   11.69 -\        F Join G : w localTo F;       \
   11.70 -\        Disjoint F G |]               \
   11.71 +\        G : v localTo F;  G : w localTo F |]               \
   11.72  \     ==> F Join G : stable {s. P (v s) (w s)}";
   11.73  by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
   11.74  qed "stable_localTo_stable2";
   11.75  
   11.76 -
   11.77 -Goal "(UN k. {s. f s = k}) = UNIV";
   11.78 -by (Blast_tac 1);
   11.79 -qed "UN_eq_UNIV";
   11.80 -
   11.81  Goal "[| F : stable {s. v s <= w s};   \
   11.82  \        G : v localTo F;       \
   11.83 -\        F Join G : Increasing w;      \
   11.84 -\        Disjoint F G |]               \
   11.85 +\        F Join G : Increasing w |]               \
   11.86  \     ==> F Join G : Stable {s. v s <= w s}";
   11.87 -by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
   11.88 -by (subgoal_tac "ALL k: UNIV. ?H : ({s. v s = k} Int ?AA) Co ?AA" 1);
   11.89 -by (dtac ball_Constrains_UN 1);
   11.90 -by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
   11.91 -by (rtac ballI 1);
   11.92 -by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
   11.93 -\                           ({s. v s = k} Un {s. v s <= w s})" 1);
   11.94 -by (asm_simp_tac (simpset() addsimps [Join_constrains]) 2);
   11.95 -by (fast_tac (claset() addIs [constrains_weaken] 
   11.96 -                addEs [localTo_imp_stable RS stableD RS constrains_weaken]) 2);
   11.97 -by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
   11.98 -by (etac Constrains_weaken 2);
   11.99 +by (auto_tac (claset(), 
  11.100 +	      simpset() addsimps [stable_def, Stable_def, Increasing_def, 
  11.101 +		    Constrains_def, Join_constrains, all_conj_distrib]));
  11.102 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
  11.103 +(*The G case remains; proved like constrains_localTo_constrains*)
  11.104 +by (auto_tac (claset(), 
  11.105 +	      simpset() addsimps [localTo_def, stable_def, constrains_def,
  11.106 +				  Diff_def]));
  11.107 +by (case_tac "act: Acts F" 1);
  11.108 +by (Blast_tac 1);
  11.109 +by (thin_tac "ALL act:Acts F. ?P act" 1);
  11.110 +by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
  11.111 +by (dres_inst_tac [("x", "v xa")] spec 1 THEN dtac bspec 1 THEN rtac DiffI 1);
  11.112 +by (assume_tac 1);
  11.113 +by (Blast_tac 1);
  11.114 +by (subgoal_tac "v x = v xa" 1);
  11.115  by Auto_tac;
  11.116  qed "Increasing_localTo_Stable";
    12.1 --- a/src/HOL/UNITY/Union.thy	Mon Oct 11 10:52:51 1999 +0200
    12.2 +++ b/src/HOL/UNITY/Union.thy	Mon Oct 11 10:53:39 1999 +0200
    12.3 @@ -29,7 +29,8 @@
    12.4    localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    12.5      "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
    12.6  
    12.7 -  (*Two programs with disjoint actions, except for identity actions *)
    12.8 +  (*Two programs with disjoint actions, except for identity actions.
    12.9 +    It's a weak property but still useful.*)
   12.10    Disjoint :: ['a program, 'a program] => bool
   12.11      "Disjoint F G == Acts F Int Acts G <= {Id}"
   12.12  
    13.1 --- a/src/HOL/UNITY/WFair.ML	Mon Oct 11 10:52:51 1999 +0200
    13.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Oct 11 10:53:39 1999 +0200
    13.3 @@ -31,6 +31,15 @@
    13.4  by (Blast_tac 1);
    13.5  qed "transient_mem";
    13.6  
    13.7 +Goalw [transient_def] "transient UNIV = {}";
    13.8 +by Auto_tac;
    13.9 +qed "transient_UNIV";
   13.10 +
   13.11 +Goalw [transient_def] "transient {} = UNIV";
   13.12 +by Auto_tac;
   13.13 +qed "transient_empty";
   13.14 +Addsimps [transient_UNIV, transient_empty];
   13.15 +
   13.16  
   13.17  (*** ensures ***)
   13.18