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')";