working version with new theory ELT
authorpaulson
Tue Nov 30 16:54:10 1999 +0100 (1999-11-30)
changeset 8041e3237d8c18d6
parent 8040 23e2a2457c77
child 8042 ecdedff41e67
working version with new theory ELT
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/TimerArray.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Tue Nov 30 16:51:41 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Tue Nov 30 16:54:10 1999 +0100
     1.3 @@ -397,17 +397,21 @@
     1.4  
     1.5  (*Lemma (?).  A LOT of work just to lift "Client_Progress" to the array*)
     1.6  Goal "lift_prog i Client \
     1.7 -\  : Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client)) \
     1.8 -\    guarantees \
     1.9 -\    (INT h. {s. h <=  (giv o sub i) s & \
    1.10 -\                       h pfixGe (ask o sub i) s}  \
    1.11 -\            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
    1.12 +\        :  Increasing (giv o sub i) Int \
    1.13 +\           ((funPair rel ask o sub i) LocalTo (lift_prog i Client)) \
    1.14 +\          guarantees \
    1.15 +\          (INT h. {s. h <=  (giv o sub i) s & \
    1.16 +\                             h pfixGe (ask o sub i) s}  \
    1.17 +\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
    1.18 +\                  {s. tokens h <= (tokens o rel o sub i) s})";
    1.19  by (rtac (Client_Progress RS drop_prog_guarantees) 1);
    1.20 -by (rtac (lift_export extending_LeadsTo RS extending_weaken RS
    1.21 +by (rtac (lift_export extending_LeadsETo RS extending_weaken RS
    1.22  	  extending_INT) 2);
    1.23  by (rtac subset_refl 4);
    1.24 -by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
    1.25 -by (force_tac (claset(), simpset() addsimps [sub_def, lift_prog_correct]) 2);
    1.26 +by (simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
    1.27 +				  sub_def]) 3);
    1.28 +by (force_tac (claset(), 
    1.29 +	       simpset() addsimps [sub_def, lift_prog_correct]) 2);
    1.30  by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
    1.31  by (auto_tac (claset(), simpset() addsimps [o_def]));
    1.32  qed "Client_i_Progress";
    1.33 @@ -415,15 +419,123 @@
    1.34  (*needed??*)
    1.35  Goalw [PLam_def]
    1.36       "(plam x:lessThan Nclients. Client) \
    1.37 -\  : (INT i : lessThan Nclients. \
    1.38 -\          Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client))) \
    1.39 -\    guarantees \
    1.40 -\    (INT i : lessThan Nclients. \
    1.41 -\         INT h. {s. h <=  (giv o sub i) s & \
    1.42 -\                       h pfixGe (ask o sub i) s}  \
    1.43 -\            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
    1.44 -br guarantees_JN_INT 1;
    1.45 -br Client_i_Progress 1;
    1.46 +\        : (INT i : lessThan Nclients. \
    1.47 +\             Increasing (giv o sub i) Int \
    1.48 +\             ((funPair rel ask o sub i) LocalTo (lift_prog i Client))) \
    1.49 +\          guarantees \
    1.50 +\          (INT i : lessThan Nclients. \
    1.51 +\               INT h. {s. h <=  (giv o sub i) s & \
    1.52 +\                             h pfixGe (ask o sub i) s}  \
    1.53 +\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
    1.54 +\                    {s. tokens h <= (tokens o rel o sub i) s})";
    1.55 +by (rtac guarantees_JN_INT 1);
    1.56 +by (rtac Client_i_Progress 1);
    1.57  qed "PLam_Client_Progress";
    1.58  
    1.59  (*progress (2), step 7*)
    1.60 +
    1.61 +
    1.62 +
    1.63 +       [| ALL i:lessThan Nclients.
    1.64 +             G : (sub i o client) LocalTo
    1.65 +                 extend sysOfClient (lift_prog i Client) |]
    1.66 +       ==> G : client LocalTo
    1.67 +               extend sysOfClient (plam i:lessThan Nclients. Client)
    1.68 +
    1.69 +   
    1.70 +   
    1.71 +   
    1.72 +   [| ALL i: I.
    1.73 +	 G : (sub i o client) LocalTo
    1.74 +	     extend sysOfClient (lift_prog i Client) |]
    1.75 +   ==> G : client LocalTo
    1.76 +	   extend sysOfClient (plam x: I. Client)
    1.77 +
    1.78 +
    1.79 +Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
    1.80 +     "[| ALL i. G : (sub i o v) localTo[C] F |] ==> G : v localTo[C] F";
    1.81 +by Auto_tac;
    1.82 +by (case_tac "Restrict C x: Restrict C `` Acts F" 1);
    1.83 +by (blast_tac (claset() addSEs [equalityE]) 1);
    1.84 +by (rtac ext 1);
    1.85 +by (blast_tac (claset() addSDs [bspec]) 1);
    1.86 +qed "all_sub_localTo";
    1.87 +
    1.88 +
    1.89 +
    1.90 + G : (sub i o client) LocalTo extend sysOfClient (plam x: I. Client)
    1.91 +
    1.92 +
    1.93 +xxxxxxxxxxxxxxxx;
    1.94 +
    1.95 +THIS PROOF requires an extra locality specification for Network:
    1.96 +    Network : rel o sub i o client localTo[C] 
    1.97 +                     extend sysOfClient (lift_prog i Client)
    1.98 +and similarly for ask o sub i o client.
    1.99 +
   1.100 +
   1.101 +
   1.102 +Goalw [System_def]
   1.103 + "System : (INT i : lessThan Nclients. \
   1.104 +\         INT h. {s. h <= (giv o sub i o client) s & \
   1.105 +\                         h pfixGe (ask o sub i o client) s}  \
   1.106 +\                LeadsTo[givenBy (funPair rel ask o sub i o client)] \
   1.107 +\                  {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.108 +by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
   1.109 +by (rtac (PLam_Client_Progress RS project_guarantees) 1);
   1.110 +br extending_INT 2;
   1.111 +by (rtac (client_export extending_LeadsETo RS extending_weaken RS extending_INT) 2);
   1.112 +by (rtac subset_refl 4);
   1.113 +by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
   1.114 +by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
   1.115 +			      client_export projecting_Increasing,
   1.116 +			      component_PLam,
   1.117 +			      client_export projecting_LocalTo]) 1);
   1.118 +auto();
   1.119 +
   1.120 +be INT_lower 2;
   1.121 +
   1.122 +br projecting_INT 1;
   1.123 +br projecting_Int 1;
   1.124 +
   1.125 +(*The next step goes wrong: it makes an impossible localTo subgoal*)
   1.126 +(*blast_tac doesn't use HO unification*)
   1.127 +by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
   1.128 +			      client_export projecting_Increasing,
   1.129 +			      component_PLam,
   1.130 +			      client_export projecting_LocalTo]) 1);
   1.131 +by (Clarify_tac 2);
   1.132 +by (asm_simp_tac
   1.133 +    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
   1.134 +			 LocalTo_def, Join_localTo,
   1.135 +			 sysOfClient_in_client_localTo_xl_Client,
   1.136 +			 sysOfAlloc_in_client_localTo_xl_Client 
   1.137 +			  RS localTo_imp_o_localTo,
   1.138 +			 self_localTo]) 2);
   1.139 +by Auto_tac;
   1.140 +
   1.141 +
   1.142 +
   1.143 +OLD PROOF;
   1.144 +by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
   1.145 +by (rtac (guarantees_PLam_I RS project_guarantees) 1);
   1.146 +by (rtac Client_i_Progress 1);
   1.147 +by (Force_tac 1);
   1.148 +by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
   1.149 +by (rtac subset_refl 4);
   1.150 +by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
   1.151 +(*The next step goes wrong: it makes an impossible localTo subgoal*)
   1.152 +(*blast_tac doesn't use HO unification*)
   1.153 +by (fast_tac (claset() addIs [projecting_Int,
   1.154 +			      client_export projecting_Increasing,
   1.155 +			      component_PLam,
   1.156 +			      client_export projecting_LocalTo]) 1);
   1.157 +by (asm_simp_tac
   1.158 +    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
   1.159 +			 LocalTo_def, Join_localTo,
   1.160 +			 sysOfClient_in_client_localTo_xl_Client,
   1.161 +			 sysOfAlloc_in_client_localTo_xl_Client]) 2);
   1.162 +by Auto_tac;
   1.163 +
   1.164 +
   1.165 +
     2.1 --- a/src/HOL/UNITY/Alloc.thy	Tue Nov 30 16:51:41 1999 +0100
     2.2 +++ b/src/HOL/UNITY/Alloc.thy	Tue Nov 30 16:54:10 1999 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4    --but need invariants that values are non-negative
     2.5  *)
     2.6  
     2.7 -Alloc = Follows + Project + PPROD +
     2.8 +Alloc = Follows + PPROD +
     2.9  
    2.10  (*Duplicated from HOL/ex/NatSum.thy.
    2.11    Maybe type should be  [nat=>int, nat] => int**)
    2.12 @@ -84,7 +84,7 @@
    2.13  	 Increasing giv
    2.14  	 guarantees
    2.15  	 (INT h. {s. h <= giv s & h pfixGe ask s}
    2.16 -		 LeadsTo
    2.17 +		 LeadsTo[givenBy (funPair rel ask)]
    2.18  		 {s. tokens h <= (tokens o rel) s})"
    2.19  
    2.20    client_spec :: clientState program set
     3.1 --- a/src/HOL/UNITY/Client.ML	Tue Nov 30 16:51:41 1999 +0100
     3.2 +++ b/src/HOL/UNITY/Client.ML	Tue Nov 30 16:54:10 1999 +0100
     3.3 @@ -89,7 +89,7 @@
     3.4  Goal "Cli_prg Join G   \
     3.5  \       : transient {s. size (giv s) = Suc k &  \
     3.6  \                       size (rel s) = k & ask s ! k <= giv s ! k}";
     3.7 -by (res_inst_tac [("act", "rel_act")] transient_mem 1);
     3.8 +by (res_inst_tac [("act", "rel_act")] transientI 1);
     3.9  by (auto_tac (claset(),
    3.10  	      simpset() addsimps [Domain_def, Cli_prg_def]));
    3.11  qed "transient_lemma";
     4.1 --- a/src/HOL/UNITY/Extend.ML	Tue Nov 30 16:51:41 1999 +0100
     4.2 +++ b/src/HOL/UNITY/Extend.ML	Tue Nov 30 16:54:10 1999 +0100
     4.3 @@ -399,6 +399,11 @@
     4.4  by (Force_tac 1);
     4.5  qed "extend_constrains_project_set";
     4.6  
     4.7 +Goal "extend h F : stable A ==> F : stable (project_set h A)";
     4.8 +by (asm_full_simp_tac
     4.9 +    (simpset() addsimps [stable_def, extend_constrains_project_set]) 1);
    4.10 +qed "extend_stable_project_set";
    4.11 +
    4.12  
    4.13  (*** Diff, needed for localTo ***)
    4.14  
     5.1 --- a/src/HOL/UNITY/Lift_prog.ML	Tue Nov 30 16:51:41 1999 +0100
     5.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Tue Nov 30 16:54:10 1999 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4  Addsimps [Init_lift_prog];
     5.5  
     5.6  Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
     5.7 -by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
     5.8 +by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
     5.9  qed "Acts_lift_prog";
    5.10  Addsimps [Acts_lift_prog];
    5.11  
    5.12 @@ -59,7 +59,7 @@
    5.13  Addsimps [Init_drop_prog];
    5.14  
    5.15  Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
    5.16 -by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
    5.17 +by (auto_tac (claset() addIs [image_eqI], 
    5.18  	      simpset() addsimps [drop_prog_def]));
    5.19  qed "Acts_drop_prog";
    5.20  Addsimps [Acts_drop_prog];
    5.21 @@ -391,6 +391,18 @@
    5.22  
    5.23  (*** guarantees properties ***)
    5.24  
    5.25 +(*The raw version*)
    5.26 +val [xguary,drop_prog,lift_prog] =
    5.27 +Goal "[| F : X guarantees Y;  \
    5.28 +\        !!G. lift_prog i F Join G : X' ==> F Join proj G i G : X;  \
    5.29 +\        !!G. [| F Join proj G i G : Y; lift_prog i F Join G : X' |] \
    5.30 +\             ==> lift_prog i F Join G : Y' |] \
    5.31 +\     ==> lift_prog i F : X' guarantees Y'";
    5.32 +by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
    5.33 +by (etac drop_prog 1);
    5.34 +by (assume_tac 1);
    5.35 +qed "drop_prog_guarantees_raw";
    5.36 +
    5.37  Goal "[| F : X guarantees Y;  \
    5.38  \        projecting C (lift_map i) F X' X;  \
    5.39  \        extending  C (lift_map i) F X' Y' Y |] \
     6.1 --- a/src/HOL/UNITY/Lift_prog.thy	Tue Nov 30 16:51:41 1999 +0100
     6.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Tue Nov 30 16:54:10 1999 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  lift_prog, etc: replication of components
     6.5  *)
     6.6  
     6.7 -Lift_prog = Project +
     6.8 +Lift_prog = ELT +
     6.9  
    6.10  constdefs
    6.11  
     7.1 --- a/src/HOL/UNITY/Project.ML	Tue Nov 30 16:51:41 1999 +0100
     7.2 +++ b/src/HOL/UNITY/Project.ML	Tue Nov 30 16:54:10 1999 +0100
     7.3 @@ -12,7 +12,8 @@
     7.4  
     7.5  (** projection: monotonicity for safety **)
     7.6  
     7.7 -Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
     7.8 +Goal "D <= C ==> \
     7.9 +\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
    7.10  by (auto_tac (claset(), simpset() addsimps [project_act_def]));
    7.11  qed "project_act_mono";
    7.12  
    7.13 @@ -589,7 +590,7 @@
    7.14  \        F Join project h C G : A ensures B |] \
    7.15  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
    7.16  by (auto_tac (claset() addDs [extend_transient RS iffD2] 
    7.17 -                       addIs [transient_strengthen, 
    7.18 +                       addIs [transient_strengthen, project_set_I,
    7.19  			      project_unless RS unlessD, unlessI, 
    7.20  			      project_extend_constrains_I], 
    7.21  	      simpset() addsimps [ensures_def, Join_constrains,
    7.22 @@ -608,7 +609,7 @@
    7.23  by (etac leadsTo_induct 1);
    7.24  by (asm_simp_tac (simpset() delsimps UN_simps
    7.25  		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
    7.26 -by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
    7.27 +by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L, 
    7.28  			       leadsTo_Trans]) 2);
    7.29  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
    7.30  val lemma = result();
    7.31 @@ -673,7 +674,7 @@
    7.32  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
    7.33  by (etac project 1);
    7.34  by (assume_tac 1);
    7.35 -qed "project_guarantees_lemma";
    7.36 +qed "project_guarantees_raw";
    7.37  
    7.38  Goal "[| F : X guarantees Y;  \
    7.39  \        projecting C h F X' X;  extending C h F X' Y' Y |] \
     8.1 --- a/src/HOL/UNITY/SubstAx.ML	Tue Nov 30 16:51:41 1999 +0100
     8.2 +++ b/src/HOL/UNITY/SubstAx.ML	Tue Nov 30 16:54:10 1999 +0100
     8.3 @@ -424,7 +424,7 @@
     8.4  				    ensuresI] 1),
     8.5  	      (*now there are two subgoals: co & transient*)
     8.6  	      simp_tac (simpset() addsimps !program_defs_ref) 2,
     8.7 -	      res_inst_tac [("act", sact)] transient_mem 2,
     8.8 +	      res_inst_tac [("act", sact)] transientI 2,
     8.9                   (*simplify the command's domain*)
    8.10  	      simp_tac (simpset() addsimps [Domain_def]) 3,
    8.11  	      constrains_tac 1,
     9.1 --- a/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:51:41 1999 +0100
     9.2 +++ b/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:54:10 1999 +0100
     9.3 @@ -8,10 +8,8 @@
     9.4  
     9.5  SubstAx = WFair + Constrains + 
     9.6  
     9.7 -consts
     9.8 -   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
     9.9 +constdefs
    9.10 +   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    9.11 +    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
    9.12  
    9.13 -defs
    9.14 -   LeadsTo_def
    9.15 -    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
    9.16  end
    10.1 --- a/src/HOL/UNITY/TimerArray.ML	Tue Nov 30 16:51:41 1999 +0100
    10.2 +++ b/src/HOL/UNITY/TimerArray.ML	Tue Nov 30 16:54:10 1999 +0100
    10.3 @@ -33,6 +33,6 @@
    10.4  by (rtac PLam_leadsTo_Basis 1);
    10.5  by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
    10.6  by (constrains_tac 1);
    10.7 -by (res_inst_tac [("act", "decr")] transient_mem 1);
    10.8 +by (res_inst_tac [("act", "decr")] transientI 1);
    10.9  by (auto_tac (claset(), simpset() addsimps [Timer_def]));
   10.10  qed "TimerArray_leadsTo_zero";
    11.1 --- a/src/HOL/UNITY/Union.ML	Tue Nov 30 16:51:41 1999 +0100
    11.2 +++ b/src/HOL/UNITY/Union.ML	Tue Nov 30 16:54:10 1999 +0100
    11.3 @@ -338,6 +338,11 @@
    11.4  by (Force_tac 1);
    11.5  qed "localTo_imp_o_localTo";
    11.6  
    11.7 +Goal "G : v LocalTo F ==> G : (f o v) LocalTo F";
    11.8 +by (asm_full_simp_tac
    11.9 +    (simpset() addsimps [LocalTo_def, localTo_imp_o_localTo]) 1);
   11.10 +qed "LocalTo_imp_o_LocalTo";
   11.11 +
   11.12  (*NOT USED*)
   11.13  Goalw [LOCALTO_def, stable_def, constrains_def]
   11.14       "(%s. x) localTo[C] F = UNIV";
   11.15 @@ -366,12 +371,17 @@
   11.16  				  Join_left_absorb]) 1);
   11.17  qed "self_Join_LocalTo";
   11.18  
   11.19 +Goalw [LOCALTO_def]
   11.20 +     "[| G : v localTo[C] F;  F<=F' |] ==> G : v localTo[C] F'";
   11.21 +by (Force_tac 1);
   11.22 +qed "localTo_imp_o_localTo";
   11.23 +
   11.24  
   11.25  
   11.26  (*** Higher-level rules involving localTo and Join ***)
   11.27  
   11.28 -Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo[C] F |]  \
   11.29 -\     ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
   11.30 +Goal "[| F : {s. P (v s)} co B;  G : v localTo[C] F |]  \
   11.31 +\     ==> G : C Int {s. P (v s)} co B";
   11.32  by (ftac constrains_imp_subset 1);
   11.33  by (auto_tac (claset(), 
   11.34  	      simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
   11.35 @@ -392,12 +402,11 @@
   11.36  by (Blast_tac 1);
   11.37  qed "localTo_pairfun";
   11.38  
   11.39 -Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
   11.40 +Goal "[| F : {s. P (v s) (w s)} co B;   \
   11.41  \        G : v localTo[C] F;       \
   11.42  \        G : w localTo[C] F |]               \
   11.43 -\     ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
   11.44 -by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
   11.45 -		  ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")] 
   11.46 +\     ==> G : C Int {s. P (v s) (w s)} co B";
   11.47 +by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}")] 
   11.48      constrains_weaken 1);
   11.49  by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
   11.50  by Auto_tac;
    12.1 --- a/src/HOL/UNITY/WFair.ML	Tue Nov 30 16:51:41 1999 +0100
    12.2 +++ b/src/HOL/UNITY/WFair.ML	Tue Nov 30 16:54:10 1999 +0100
    12.3 @@ -29,7 +29,16 @@
    12.4  Goalw [transient_def]
    12.5      "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
    12.6  by (Blast_tac 1);
    12.7 -qed "transient_mem";
    12.8 +qed "transientI";
    12.9 +
   12.10 +val major::prems = 
   12.11 +Goalw [transient_def]
   12.12 +    "[| F : transient A;  \
   12.13 +\       !!act. [| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> P |] \
   12.14 +\    ==> P";
   12.15 +by (rtac (major RS CollectD RS bexE) 1);
   12.16 +by (blast_tac (claset() addIs prems) 1);
   12.17 +qed "transientE";
   12.18  
   12.19  Goalw [transient_def] "transient UNIV = {}";
   12.20  by Auto_tac;
   12.21 @@ -53,27 +62,24 @@
   12.22  by (Blast_tac 1);
   12.23  qed "ensuresD";
   12.24  
   12.25 -(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
   12.26  Goalw [ensures_def]
   12.27      "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
   12.28  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   12.29  qed "ensures_weaken_R";
   12.30  
   12.31 -Goalw [ensures_def, constrains_def, transient_def]
   12.32 -    "F : A ensures UNIV";
   12.33 -by Auto_tac;
   12.34 -qed "ensures_UNIV";
   12.35 -
   12.36 +(*The L-version (precondition strengthening) fails, but we have this*)
   12.37  Goalw [ensures_def]
   12.38 -    "[| F : stable C; \
   12.39 -\       F : (C Int (A - A')) co (A Un A'); \
   12.40 -\       F : transient (C Int (A-A')) |]   \
   12.41 -\   ==> F : (C Int A) ensures (C Int A')";
   12.42 -by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
   12.43 -				      Diff_Int_distrib RS sym,
   12.44 -				      stable_constrains_Int]) 1);
   12.45 +    "[| F : stable C;  F : A ensures B |]   \
   12.46 +\   ==> F : (C Int A) ensures (C Int B)";
   12.47 +by (auto_tac (claset(),
   12.48 +	      simpset() addsimps [ensures_def,
   12.49 +				  Int_Un_distrib RS sym,
   12.50 +				  Diff_Int_distrib RS sym]));
   12.51 +by (blast_tac (claset() addIs [transient_strengthen]) 2);
   12.52 +by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
   12.53  qed "stable_ensures_Int";
   12.54  
   12.55 +(*NEVER USED*)
   12.56  Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
   12.57  by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
   12.58  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   12.59 @@ -96,11 +102,6 @@
   12.60      (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
   12.61  qed "transient_imp_leadsTo";
   12.62  
   12.63 -Goal "F : A leadsTo UNIV";
   12.64 -by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
   12.65 -qed "leadsTo_UNIV";
   12.66 -Addsimps [leadsTo_UNIV];
   12.67 -
   12.68  (*Useful with cancellation, disjunction*)
   12.69  Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
   12.70  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   12.71 @@ -164,6 +165,9 @@
   12.72  bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
   12.73  Addsimps [empty_leadsTo];
   12.74  
   12.75 +bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo);
   12.76 +Addsimps [leadsTo_UNIV];
   12.77 +
   12.78  
   12.79  Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
   12.80  by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
   12.81 @@ -210,22 +214,6 @@
   12.82                          addIs prems) 1);
   12.83  qed "leadsTo_UN_UN";
   12.84  
   12.85 -
   12.86 -(*Version with no index set*)
   12.87 -val prems = goal thy
   12.88 -   "(!! i. F : (A i) leadsTo (A' i)) \
   12.89 -\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
   12.90 -by (blast_tac (claset() addIs [leadsTo_UN_UN] 
   12.91 -                        addIs prems) 1);
   12.92 -qed "leadsTo_UN_UN_noindex";
   12.93 -
   12.94 -(*Version with no index set*)
   12.95 -Goal "ALL i. F : (A i) leadsTo (A' i) \
   12.96 -\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
   12.97 -by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
   12.98 -qed "all_leadsTo_UN_UN";
   12.99 -
  12.100 -
  12.101  (*Binary union version*)
  12.102  Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
  12.103  \     ==> F : (A Un B) leadsTo (A' Un B')";