working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.
--- a/src/HOL/UNITY/Alloc.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML Thu Jan 13 17:30:23 2000 +0100
@@ -23,10 +23,12 @@
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
qed "sub_fold";
-(*Splits up an intersection: like CONJUNCTS in the HOL system*)
-fun list_of_Int th = (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
- handle THM _ => (list_of_Int (th RS INT_D))
- handle THM _ => [th];
+(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
+fun list_of_Int th =
+ (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
+ handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+ handle THM _ => (list_of_Int (th RS INT_D))
+ handle THM _ => [th];
(*useful??*)
val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
@@ -75,17 +77,6 @@
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
qed "mono_tokens";
-(*Generalized version allowing different clients*)
-Goal "[| Alloc : alloc_spec; \
-\ Client : (lessThan Nclients) funcset client_spec; \
-\ Network : network_spec |] \
-\ ==> (extend sysOfAlloc Alloc) \
-\ Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
-\ Join Network : system_spec";
-
-Goal "System : system_spec";
-
-
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
by (rtac injI 1);
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
@@ -206,15 +197,7 @@
AddIffs [Network_preserves_allocGiv];
-
-Goal "i < Nclients ==> Network : preserves (ask o sub i o client) & \
-\ Network : preserves (rel o sub i o client)";
-by (rtac (Network_preserves_rel_ask RS revcut_rl) 1);
-by (auto_tac (claset(),
- simpset() addsimps [funPair_o_distrib]));
-qed "Network_preserves_rel_conj_ask";
-
-Addsimps [Network_preserves_rel_conj_ask];
+Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
(*Alloc : <unfolded specification> *)
@@ -222,31 +205,41 @@
rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
alloc_progress_def, alloc_preserves_def] Alloc;
-val [Alloc_Increasing, Alloc_Safety,
+val [Alloc_Increasing_0, Alloc_Safety,
Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
+(*Strip off the INT in the guarantees postcondition*)
+val Alloc_Increasing = normalize Alloc_Increasing_0;
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
-(*extend sysOfAlloc G : preserves client
- alloc_export isn't needed!*)
-bind_thm ("extend_sysOfAlloc_preserves_client",
- inj_sysOfAlloc RS export inj_extend_preserves
- |> simplify (simpset()));
+AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
+
+(** Components lemmas **)
-AddIffs [extend_sysOfAlloc_preserves_client];
+(*Alternative is to say that System = Network Join F such that F preserves
+ certain state variables*)
+Goal "(extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
+\ (Network Join Alloc) = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Client_component_System";
-Goal "extend sysOfAlloc Alloc : preserves allocRel & \
-\ extend sysOfAlloc Alloc : preserves allocAsk";
-by (cut_facts_tac [Alloc_preserves] 1);
-by (auto_tac (claset() addSDs [alloc_export extend_preserves RS iffD2],
- simpset() addsimps [o_def]));
-qed "extend_sysOfAlloc_preserves_Rel_Ask";
+Goal "Network Join \
+\ ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join Alloc) \
+\ = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Network_component_System";
-AddIffs [extend_sysOfAlloc_preserves_Rel_Ask RS conjunct1,
- extend_sysOfAlloc_preserves_Rel_Ask RS conjunct2];
+Goal "Alloc Join \
+\ ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
+\ Network) = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Alloc_component_System";
+
+AddIffs [Client_component_System, Network_component_System,
+ Alloc_component_System];
(** These preservation laws should be generated automatically **)
@@ -282,68 +275,28 @@
AddIffs [extend_sysOfClient_preserves_o_client];
-(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing
- (the form changes slightly, though, removing the INT) *)
-Goal "i < Nclients \
-\ ==> extend sysOfAlloc Alloc : \
-\ UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
-(* Alternative is something like
-by (dtac (Alloc_Increasing RS (guarantees_INT_right_iff RS iffD1)
- RS lessThanBspec RS alloc_export extend_guar_Increasing) 1);
-*)
-by (cut_facts_tac [Alloc_Increasing] 1);
-by (auto_tac (claset() addSDs [alloc_export extend_guar_Increasing],
- simpset() addsimps [guarantees_INT_right_iff, o_def]));
-qed "extend_Alloc_Increasing_allocGiv";
-
-
Goalw [System_def]
"i < Nclients ==> System : Increasing (sub i o allocGiv)";
-by (rtac (extend_Alloc_Increasing_allocGiv RS
- guarantees_Join_I1 RS guaranteesD) 1);
+by (rtac (Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
by Auto_tac;
qed "System_Increasing_allocGiv";
-Goalw [System_def]
- "i < Nclients ==> System : Increasing (ask o sub i o client)";
-by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2
- RS guaranteesD) 1);
+Goal "i < Nclients ==> System : Increasing (ask o sub i o client)";
+by (rtac ([client_export extend_guar_Increasing,
+ Client_component_System] MRS component_guaranteesD) 1);
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
-by (auto_tac (claset(),
- simpset() addsimps [Network_preserves_rel_ask]));
+by Auto_tac;
qed "System_Increasing_ask";
-Goalw [System_def]
- "i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2
- RS guaranteesD) 1);
+Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
+by (rtac ([client_export extend_guar_Increasing,
+ Client_component_System] MRS component_guaranteesD) 1);
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
(*gets Client_Increasing_rel from simpset*)
-by (auto_tac (claset(),
- simpset() addsimps [Network_preserves_rel_ask]));
+by Auto_tac;
qed "System_Increasing_rel";
-(** Components lemmas **)
-
-(*Alternative is to say that System = Network Join F such that F preserves
- certain state variables*)
-Goal "Network Join \
-\ ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
-\ (extend sysOfAlloc Alloc)) \
-\ = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Network_component_System";
-
-Goal "(extend sysOfAlloc Alloc) Join \
-\ ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
-\ Network) \
-\ = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Alloc_component_System";
-
-AddIffs [Network_component_System, Alloc_component_System];
-
(** Follows consequences.
The "Always (INT ...) formulation expresses the general safety property
and allows it to be combined using Always_Int_rule below. **)
@@ -365,7 +318,7 @@
Goal
"i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD,
- extend_Alloc_Increasing_allocGiv RS component_guaranteesD],
+ Alloc_Increasing RS component_guaranteesD],
simpset()));
qed "System_Follows_allocGiv";
@@ -399,28 +352,10 @@
by (etac (System_Follows_rel RS Follows_Increasing1) 1);
qed "System_Increasing_allocRel";
-(*NEED AUTOMATIC PROPAGATION of Alloc_Safety. The text is identical.*)
-Goal "extend sysOfAlloc Alloc : \
-\ (INT i : lessThan Nclients. Increasing (sub i o allocRel)) \
-\ guarantees[allocGiv] \
-\ Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
-\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
-by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
-(*2: Always postcondition*)
-by (rtac (alloc_export extending_Always RS extending_weaken_L) 2);
-(*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L RS
- projecting_INT) 1);
-by (auto_tac (claset(),
- simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
- o_def]));
-qed "extend_Alloc_Safety";
-
(*safety (1), step 3*)
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
-by (rtac (extend_Alloc_Safety RS component_guaranteesD) 1);
-by (rtac Alloc_component_System 2);
+by (rtac ([Alloc_Safety, Alloc_component_System] MRS component_guaranteesD) 1);
(*preserves*)
by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
@@ -484,12 +419,12 @@
(*progress (2), step 3*)
(*All this trouble just to lift "Client_Bounded" through two extend ops*)
-Goalw [System_def]
- "i < Nclients \
-\ ==> System : Always \
-\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
-by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS
- guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
+Goal "i < Nclients \
+\ ==> System : Always \
+\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+br Always_weaken 1;
+by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
+ Client_component_System] MRS component_guaranteesD) 1);
by (rtac Client_i_Bounded 1);
by (auto_tac(claset(),
simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
@@ -516,48 +451,126 @@
simpset()));
qed "System_Increasing_giv";
-(*Lemma. A LOT of work just to lift "Client_Progress" to the array*)
+(** A LOT of work just to lift "Client_Progress" to the array **)
+
+(*stability lemma for G*)
+Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
+ "[| ALL z. G : stable \
+\ (reachable (lift_prog i Client Join G) Int \
+\ {s. z <= (giv o sub i) s}); \
+\ G : preserves (rel o sub i); G : preserves (ask o sub i) |] \
+\ ==> G : stable \
+\ (reachable (lift_prog i Client Join G) Int \
+\ {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} - \
+\ {s. tokens h <= tokens ((rel o sub i) s)})";
+auto();
+by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
+by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
+by (REPEAT_FIRST ball_tac);
+auto();
+qed "G_stable_lift_prog";
+
Goal "lift_prog i Client \
\ : Increasing (giv o sub i) \
\ guarantees[funPair rel ask o sub i] \
\ (INT h. {s. h <= (giv o sub i) s & \
\ h pfixGe (ask o sub i) s} \
-\ LeadsTo[givenBy (funPair rel ask o sub i)] \
-\ {s. tokens h <= (tokens o rel o sub i) s})";
-by (rtac (Client_Progress RS drop_prog_guarantees) 1);
-by (rtac (lift_export extending_LeadsETo RS extending_weaken_L RS
- extending_INT) 2);
-by (asm_simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
- sub_def, o_def]) 2);
-by (rtac (lift_export projecting_Increasing) 1);
-by (auto_tac (claset(), simpset() addsimps [o_def]));
+\ Ensures {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
+br (lift_export (subset_refl RS project_Increasing_I)) 1;
+by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
+br INT_I 1;
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
+br (lift_export project_Ensures_D) 1;
+by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct,
+ drop_prog_correct]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [all_conj_distrib,
+ Increasing_def, Stable_eq_stable, Join_stable,
+ lift_set_correct RS sym,
+ Collect_eq_lift_set RS sym,
+ lift_prog_correct RS sym]) 1);
+by (Clarify_tac 1);
+bd G_stable_lift_prog 1;
+by (auto_tac (claset(),
+ simpset() addsimps [o_apply]));
qed "Client_i_Progress";
+Goal "i < Nclients \
+\ ==> (plam x: lessThan Nclients. Client) \
+\ : Increasing (giv o sub i) \
+\ guarantees[funPair rel ask o sub i] \
+\ (INT h. {s. h <= (giv o sub i) s & \
+\ h pfixGe (ask o sub i) s} \
+\ Ensures {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac guarantees_PLam_I 1);
+br Client_i_Progress 1;
+by Auto_tac;
+val lemma2 = result();
+
+(*another stability lemma for G*)
+Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
+ "[| ALL z. G : stable \
+\ (reachable (extend sysOfClient \
+\ (plam x:lessThan Nclients. Client) Join G) Int \
+\ {s. z <= (giv o sub i o client) s}); \
+\ G : preserves (rel o sub i o client); \
+\ G : preserves (ask o sub i o client) |] \
+\ ==> G : stable \
+\ (reachable (extend sysOfClient \
+\ (plam x:lessThan Nclients. Client) Join G) Int \
+\ {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s} - \
+\ {s. tokens h <= tokens ((rel o sub i o client) s)})";
+auto();
+by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
+by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
+by (REPEAT_FIRST ball_tac);
+auto();
+qed "G_stable_sysOfClient";
+
+Goal "i < Nclients \
+\ ==> extend sysOfClient (plam x: lessThan Nclients. Client) \
+\ : Increasing (giv o sub i o client) \
+\ guarantees[funPair rel ask o sub i o client] \
+\ (INT h. {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s} \
+\ Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
+ba 1;
+br (client_export (subset_refl RS project_Increasing_I)) 1;
+by (Simp_tac 1);
+br INT_I 1;
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
+br (client_export project_Ensures_D) 1;
+by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [all_conj_distrib,
+ Increasing_def, Stable_eq_stable, Join_stable,
+ Collect_eq_extend_set RS sym]) 1);
+by (Clarify_tac 1);
+bd G_stable_sysOfClient 1;
+by (auto_tac (claset(),
+ simpset() addsimps [o_apply,
+ client_export Collect_eq_extend_set RS sym]));
+qed "sysOfClient_i_Progress";
+
+
(*progress (2), step 7*)
-Goalw [System_def]
+Goal
"System : (INT i : lessThan Nclients. \
\ INT h. {s. h <= (giv o sub i o client) s & \
\ h pfixGe (ask o sub i o client) s} \
-\ LeadsTo[givenBy (funPair rel ask o sub i o client)] \
-\ {s. tokens h <= (tokens o rel o sub i o client) s})";
-by (stac INT_iff 1);
-by (rtac ballI 1);
+\ Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac INT_I 1);
(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
-by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
-by (rtac (Client_i_Progress RS
- (guarantees_PLam_I RS client_export project_guarantees)) 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addIs [projecting_Int,
- component_PLam,
- client_export projecting_Increasing]) 1);
+by (rtac ([sysOfClient_i_Progress,
+ Client_component_System] MRS component_guaranteesD) 1);
by (asm_full_simp_tac
- (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv]) 5);
-by (rtac (client_export extending_LeadsETo RS extending_weaken_L RS
- extending_INT) 1);
-by (auto_tac (claset(),
- simpset() addsimps [o_apply,
- client_export Collect_eq_extend_set RS sym]));
+ (simpset() addsimps [System_Increasing_giv]) 2);
+auto();
qed "System_Client_Progress";
val lemma =
@@ -583,11 +596,7 @@
val lemma3 = result();
-(*NOT GOOD ENOUGH. Needs givenBy restriction
- (funPair allocGiv (funPair allocAsk allocRel))
- in LeadsTo! But System_Client_Progress has the wrong restriction (below)
-*)
-(*progress (2), step 8*)
+(*progress (2), step 8: Client i's "release" action is visible system-wide*)
Goal "i < Nclients \
\ ==> System : {s. h <= (sub i o allocGiv) s & \
\ h pfixGe (sub i o allocAsk) s} \
@@ -597,75 +606,20 @@
Follows_LeadsTo) 2);
by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
by (rtac LeadsTo_Trans 1);
-by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
-(*Here we have givenBy (funPair rel ask o sub i o client)]
- when we need givenBy (funPair allocRel allocAsk) ?? *)
by (cut_facts_tac [System_Client_Progress] 2);
-by (Force_tac 2);
+by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
by (etac lemma3 1);
-qed "System_Alloc_Progress";
-
-(*NEED AUTOMATIC PROPAGATION of Alloc_Progress. The text is identical
- except in the LeadsTo precondition.*)
-Goal "extend sysOfAlloc Alloc : \
-\ (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
-\ Increasing (sub i o allocRel)) \
-\ Int \
-\ Always {s. ALL i : lessThan Nclients. \
-\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT} \
-\ Int \
-\ (INT i : lessThan Nclients. \
-\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \
-\ LeadsTo[givenBy (funPair allocGiv (funPair allocAsk allocRel))] \
-\ {s. tokens h <= (tokens o sub i o allocRel)s}) \
-\ guarantees[allocGiv] \
-\ (INT i : lessThan Nclients. \
-\ INT h. {s. h <= (sub i o allocAsk) s} \
- \ LeadsTo[givenBy allocGiv] \
-\ {s. h pfixLe (sub i o allocGiv) s})";
-by (rtac (Alloc_Progress RS alloc_export project_guarantees) 1);
-(*preserves*)
-by (simp_tac (simpset() addsimps [o_def]) 3);
-(*2: LeadsTo postcondition*)
-by (rtac (extending_INT RS extending_INT) 2);
-by (rtac (alloc_export extending_LeadsETo RS extending_weaken) 2);
-by (rtac subset_refl 3);
-by (simp_tac (simpset() addsimps [o_def]) 3);
-by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
- o_def]) 2);
-(*1: Complex precondition*)
-by (rtac (projecting_Int RS projecting_INT RS projecting_Int RS
- projecting_Int) 1);
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-by (rtac (alloc_export projecting_Always RS projecting_weaken_L) 1);
-by (asm_simp_tac
- (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym, o_def]) 1);
-(*LeadsTo precondition*)
-by (rtac (projecting_INT RS projecting_INT) 1);
-by (rtac (alloc_export projecting_LeadsTo RS projecting_weaken_L) 1);
-by (auto_tac (claset(),
- simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
- o_def]));
-by (auto_tac (claset() addSIs [givenByI]
- addEs [LeadsETo_weaken, givenByD]
- addSWrapper record_split_wrapper,
- simpset() addsimps [funPair_def]));
-qed "extend_Alloc_Progress";
+qed "System_Alloc_Client_Progress";
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
(*progress (2), step 9*)
Goal
"System : (INT i : lessThan Nclients. \
\ INT h. {s. h <= (sub i o allocAsk) s} \
-\ LeadsTo[givenBy allocGiv] \
-\ {s. h pfixLe (sub i o allocGiv) s})";
-by (rtac (extend_Alloc_Progress RS component_guaranteesD) 1);
-by (rtac Alloc_component_System 2);
+\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
+by (rtac ([Alloc_Progress, Alloc_component_System]
+ MRS component_guaranteesD) 1);
(*preserves*)
by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
(*the guarantees precondition*)
@@ -673,8 +627,50 @@
simpset() addsimps [System_Increasing_allocRel,
System_Increasing_allocAsk]));
by (rtac System_Bounded_allocAsk 1);
-by (rtac System_Alloc_Progress 1);
+by (etac System_Alloc_Progress 1);
+qed "System_Alloc_Progress";
+
+
+
+(*Ultimate goal*)
+Goal "System : system_spec";
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+
+(*progress (2), step 10*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (ask o sub i o client) s} \
+\ LeadsTo {s. h pfixLe (giv o sub i o client) s})";
+by (Clarify_tac 1);
+by (rtac LeadsTo_Trans 1);
+by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
+by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
+
+prefix_imp_pfixLe
+
-by (rtac Alloc_component_System 3);
-by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
-by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
+System_Follows_ask
+
+by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS
+ Follows_LeadsTo) 2);
+
+by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
+by (rtac LeadsTo_Trans 1);
+by (cut_facts_tac [System_Client_Progress] 2);
+by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
+by (etac lemma3 1);
+
+by (rtac ([Alloc_Progress, Alloc_component_System]
+ MRS component_guaranteesD) 1);
+(*preserves*)
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+(*the guarantees precondition*)
+by (auto_tac (claset(),
+ simpset() addsimps [System_Increasing_allocRel,
+ System_Increasing_allocAsk]));
+by (rtac System_Bounded_allocAsk 1);
+by (etac System_Alloc_Progress 1);
+qed "System_Alloc_Progress";
+
--- a/src/HOL/UNITY/Alloc.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Alloc.thy Thu Jan 13 17:30:23 2000 +0100
@@ -88,8 +88,7 @@
Increasing giv
guarantees[funPair rel ask]
(INT h. {s. h <= giv s & h pfixGe ask s}
- LeadsTo[givenBy (funPair rel ask)]
- {s. tokens h <= (tokens o rel) s})"
+ Ensures {s. tokens h <= (tokens o rel) s})"
(*spec: preserves part*)
client_preserves :: clientState program set
@@ -101,15 +100,18 @@
(** Allocator specification (required) ***)
+ (*Specified over the systemState, not the allocState, since then the
+ leads-to properties could not be transferred to extend sysOfAlloc Alloc*)
+
(*spec (6)*)
- alloc_increasing :: allocState program set
+ alloc_increasing :: systemState program set
"alloc_increasing ==
UNIV
guarantees[allocGiv]
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
- alloc_safety :: allocState program set
+ alloc_safety :: systemState program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees[allocGiv]
@@ -117,7 +119,7 @@
<= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
(*spec (8)*)
- alloc_progress :: allocState program set
+ alloc_progress :: systemState program set
"alloc_progress ==
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
Increasing (sub i o allocRel))
@@ -132,14 +134,14 @@
guarantees[allocGiv]
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocAsk) s}
- LeadsTo[givenBy allocGiv]
+ LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
(*spec: preserves part*)
- alloc_preserves :: allocState program set
- "alloc_preserves == preserves (funPair allocRel allocAsk)"
+ alloc_preserves :: systemState program set
+ "alloc_preserves == preserves (funPair client (funPair allocRel allocAsk))"
- alloc_spec :: allocState program set
+ alloc_spec :: systemState program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_preserves"
@@ -190,7 +192,7 @@
locale System =
fixes
- Alloc :: allocState program
+ Alloc :: systemState program
Client :: clientState program
Network :: systemState program
System :: systemState program
@@ -202,9 +204,6 @@
defines
System_def
- "System == (extend sysOfAlloc Alloc)
- Join
- (extend sysOfClient (plam x: lessThan Nclients. Client))
- Join
- Network"
+ "System == Alloc Join Network Join
+ (extend sysOfClient (plam x: lessThan Nclients. Client))"
end
--- a/src/HOL/UNITY/Comp.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML Thu Jan 13 17:30:23 2000 +0100
@@ -172,3 +172,75 @@
by (etac order_trans 1);
by (Blast_tac 1);
qed "Increasing_preserves_Stable";
+
+
+(*** givenBy ***)
+
+Goalw [givenBy_def] "givenBy id = UNIV";
+by Auto_tac;
+qed "givenBy_id";
+Addsimps [givenBy_id];
+
+Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
+by Safe_tac;
+by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by Auto_tac;
+qed "givenBy_eq_all";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "givenBy_eq_Collect";
+
+val prems =
+Goal "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v";
+by (stac givenBy_eq_all 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "givenByI";
+
+Goalw [givenBy_def] "[| A: givenBy v; x:A; v x = v y |] ==> y: A";
+by Auto_tac;
+qed "givenByD";
+
+Goal "{} : givenBy v";
+by (blast_tac (claset() addSIs [givenByI]) 1);
+qed "empty_mem_givenBy";
+
+AddIffs [empty_mem_givenBy];
+
+Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "givenBy_imp_eq_Collect";
+
+Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
+by (Best_tac 1);
+qed "Collect_mem_givenBy";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (blast_tac (claset() addIs [Collect_mem_givenBy,
+ givenBy_imp_eq_Collect]) 1);
+qed "givenBy_eq_eq_Collect";
+
+(*preserving v preserves properties given by v*)
+Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
+by (force_tac (claset(),
+ simpset() addsimps [impOfSubs preserves_subset_stable,
+ givenBy_eq_Collect]) 1);
+qed "preserves_givenBy_imp_stable";
+
+Goal "givenBy (w o v) <= givenBy v";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_subset";
+
+Goal "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
+by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
+qed "givenBy_DiffI";
--- a/src/HOL/UNITY/Comp.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Comp.thy Thu Jan 13 17:30:23 2000 +0100
@@ -26,4 +26,8 @@
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
"funPair f g == %x. (f x, g x)"
+ (*the set of all sets determined by f alone*)
+ givenBy :: "['a => 'b] => 'a set set"
+ "givenBy f == range (%B. f-`` B)"
+
end
--- a/src/HOL/UNITY/ELT.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML Thu Jan 13 17:30:23 2000 +0100
@@ -6,69 +6,6 @@
leadsTo strengthened with a specification of the allowable sets transient parts
*)
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
-by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
-by Auto_tac;
-qed "givenBy_eq_all";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "givenBy_eq_Collect";
-
-val prems =
-Goal "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v";
-by (stac givenBy_eq_all 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "givenByI";
-
-Goalw [givenBy_def] "[| A: givenBy v; x:A; v x = v y |] ==> y: A";
-by Auto_tac;
-qed "givenByD";
-
-Goal "{} : givenBy v";
-by (blast_tac (claset() addSIs [givenByI]) 1);
-qed "empty_mem_givenBy";
-
-AddIffs [empty_mem_givenBy];
-
-Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "givenBy_imp_eq_Collect";
-
-Goalw [givenBy_def] "EX P. A = {s. P(v s)} ==> A: givenBy v";
-by (Best_tac 1);
-qed "eq_Collect_imp_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [eq_Collect_imp_givenBy,
- givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(),
- simpset() addsimps [impOfSubs preserves_subset_stable,
- givenBy_eq_Collect]) 1);
-qed "preserves_givenBy_imp_stable";
-
-Goal "givenBy (w o v) <= givenBy v";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_subset";
-
-
(** Standard leadsTo rules **)
Goalw [leadsETo_def]
@@ -81,6 +18,7 @@
by (blast_tac (claset() addIs [elt.Trans]) 1);
qed "leadsETo_Trans";
+
(*Useful with cancellation, disjunction*)
Goal "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
@@ -126,6 +64,11 @@
by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
qed "leadsETo_mono";
+Goal "[| F : A leadsTo[CC] B; F : B leadsTo[DD] C |] \
+\ ==> F : A leadsTo[CC Un DD] C";
+by (blast_tac (claset() addIs [impOfSubs leadsETo_mono, leadsETo_Trans]) 1);
+qed "leadsETo_Trans_Un";
+
val prems = Goalw [leadsETo_def]
"(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
@@ -154,6 +97,7 @@
Addsimps [empty_leadsETo];
+
(** Weakening laws **)
Goal "[| F : A leadsTo[CC] A'; A'<=B' |] ==> F : A leadsTo[CC] B'";
@@ -478,22 +422,6 @@
Open_locale "Extend";
-Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_eq_extend_set";
-
-Goal "givenBy f = range (extend_set h)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_eq_extend_set";
-
-Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "extend_set_givenBy_I";
-
-
Goal "F : A leadsTo[CC] B \
\ ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
\ (extend_set h B)";
@@ -505,24 +433,6 @@
extend_set_Diff_distrib RS sym]) 1);
qed "leadsETo_imp_extend_leadsETo";
-(*MOVE to Extend.ML?*)
-Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
-by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
-qed "Int_extend_set_lemma";
-
-(*MOVE to extend.ML??*)
-Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
-by (full_simp_tac (simpset() addsimps [constrains_def, project_def,
- project_act_def]) 1);
-by (Blast_tac 1);
-qed "project_constrains_project_set";
-
-(*MOVE to extend.ML??*)
-Goal "G : stable C ==> project h C G : stable (project_set h C)";
-by (asm_full_simp_tac (simpset() addsimps [stable_def,
- project_constrains_project_set]) 1);
-qed "project_stable_project_set";
-
(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
@@ -535,18 +445,6 @@
project_preserves_I]) 1);
result();
-(*GENERALIZES the version proved in Project.ML*)
-Goal "[| G : preserves (v o f); \
-\ project h C G : transient (C' Int D); \
-\ project h C G : stable C'; D : givenBy v |] \
-\ ==> C' Int D = {}";
-by (rtac stable_transient_empty 1);
-by (assume_tac 2);
-(*If addIs then PROOF FAILED at depth 3*)
-by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
- project_preserves_I]) 1);
-qed "preserves_o_project_transient_empty";
-
(*This version's stronger in the "ensures" precondition
BUT there's no ensures_weaken_L*)
--- a/src/HOL/UNITY/ELT.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/ELT.thy Thu Jan 13 17:30:23 2000 +0100
@@ -4,6 +4,22 @@
Copyright 1999 University of Cambridge
leadsTo strengthened with a specification of the allowable sets transient parts
+
+TRY INSTEAD (to get rid of the {} and to gain strong induction)
+
+ elt :: "['a set set, 'a program, 'a set] => ('a set) set"
+
+inductive "elt CC F B"
+ intrs
+
+ Weaken "A <= B ==> A : elt CC F B"
+
+ ETrans "[| F : A ensures A'; A-A' : CC; A' : elt CC F B |]
+ ==> A : elt CC F B"
+
+ Union "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
+
+ monos Pow_mono
*)
ELT = Project +
@@ -28,10 +44,6 @@
constdefs
- (*the set of all sets determined by f alone*)
- givenBy :: "['a => 'b] => 'a set set"
- "givenBy f == range (%B. f-`` B)"
-
(*visible version of the LEADS-TO relation*)
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
--- a/src/HOL/UNITY/Extend.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML Thu Jan 13 17:30:23 2000 +0100
@@ -327,6 +327,7 @@
by (rtac program_equalityI 1);
by Auto_tac;
qed "extend_SKIP";
+Addsimps [export extend_SKIP];
Goal "project_set h UNIV = UNIV";
by Auto_tac;
@@ -456,6 +457,24 @@
qed "extend_Always";
+(** Further lemmas **)
+
+Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
+qed "Int_extend_set_lemma";
+
+Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
+by (full_simp_tac (simpset() addsimps [constrains_def, project_def,
+ project_act_def]) 1);
+by (Blast_tac 1);
+qed "project_constrains_project_set";
+
+Goal "G : stable C ==> project h C G : stable (project_set h C)";
+by (asm_full_simp_tac (simpset() addsimps [stable_def,
+ project_constrains_project_set]) 1);
+qed "project_stable_project_set";
+
+
(*** Progress: transient, ensures ***)
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
@@ -550,6 +569,24 @@
qed "extend_LeadsTo";
+(*** givenBy: USEFUL??? ***)
+
+Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_eq_extend_set";
+
+Goal "givenBy f = range (extend_set h)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_eq_extend_set";
+
+Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
+
Close_locale "Extend";
(*Close_locale should do this!
--- a/src/HOL/UNITY/Follows.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Follows.thy Thu Jan 13 17:30:23 2000 +0100
@@ -9,7 +9,7 @@
progress part: g cannot do anything silly.
*)
-Follows = ELT +
+Follows = Project +
constdefs
--- a/src/HOL/UNITY/Guar.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Guar.ML Thu Jan 13 17:30:23 2000 +0100
@@ -80,7 +80,7 @@
(*This version of guaranteesD matches more easily in the conclusion
The major premise can no longer be F<=H since we need to reason about G*)
Goalw [guar_def]
- "[| F : X guarantees[v] Y; H : X; F Join G = H; G : preserves v |] \
+ "[| F : X guarantees[v] Y; F Join G = H; H : X; G : preserves v |] \
\ ==> H : Y";
by (Blast_tac 1);
qed "component_guaranteesD";
--- a/src/HOL/UNITY/Lift_prog.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Thu Jan 13 17:30:23 2000 +0100
@@ -120,7 +120,7 @@
by Auto_tac;
qed "good_map_lift_map";
-fun lift_export th =
+fun lift_export0 th =
good_map_lift_map RS export th
|> simplify (simpset() addsimps [fold_o_sub]);;
@@ -133,7 +133,7 @@
Goal "lift_set i A = extend_set (lift_map i) A";
by (auto_tac (claset(),
- simpset() addsimps [lift_export mem_extend_set_iff]));
+ simpset() addsimps [lift_export0 mem_extend_set_iff]));
qed "lift_set_correct";
Goalw [drop_set_def, project_set_def, lift_map_def]
@@ -148,7 +148,7 @@
Goal "lift_act i = extend_act (lift_map i)";
by (rtac ext 1);
by Auto_tac;
-by (forward_tac [lift_export extend_act_D] 2);
+by (forward_tac [lift_export0 extend_act_D] 2);
by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
by (rtac bexI 1);
@@ -168,7 +168,7 @@
by (rtac (program_equalityI RS ext) 1);
by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
by (simp_tac (simpset()
- addsimps [lift_export Acts_extend,
+ addsimps [lift_export0 Acts_extend,
lift_act_correct]) 1);
qed "lift_prog_correct";
@@ -212,7 +212,7 @@
Goal "lift_set i UNIV = UNIV";
by (simp_tac
- (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
+ (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
qed "lift_set_UNIV_eq";
Addsimps [lift_set_UNIV_eq];
@@ -220,7 +220,7 @@
Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, drop_act_correct,
- lift_act_correct, lift_export extend_act_inverse]) 1);
+ lift_act_correct, lift_export0 extend_act_inverse]) 1);
qed "lift_act_inverse";
Addsimps [lift_act_inverse];
*)
@@ -228,13 +228,13 @@
Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, drop_prog_correct,
- lift_prog_correct, lift_export extend_inverse]) 1);
+ lift_prog_correct, lift_export0 extend_inverse]) 1);
qed "lift_prog_inverse";
Addsimps [lift_prog_inverse];
Goal "inj (lift_prog i)";
by (simp_tac
- (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
+ (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
qed "inj_lift_prog";
@@ -242,7 +242,7 @@
Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
- lift_export extend_act_Image]) 1);
+ lift_export0 extend_act_Image]) 1);
qed "lift_act_Image";
Addsimps [lift_act_Image];
@@ -272,7 +272,7 @@
\ ==> F : (drop_set i A) co (drop_set i B)";
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, lift_prog_correct,
- lift_export extend_constrains_project_set]) 1);
+ lift_export0 extend_constrains_project_set]) 1);
qed "lift_prog_constrains_drop_set";
(*This one looks strange! Proof probably is by case analysis on i=j.
@@ -292,7 +292,7 @@
\ (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
by (simp_tac
(simpset() addsimps [drop_prog_correct,
- lift_set_correct, lift_export project_constrains]) 1);
+ lift_set_correct, lift_export0 project_constrains]) 1);
qed "drop_prog_constrains";
Goal "(drop_prog i UNIV F : stable A) = (F : stable (lift_set i A))";
@@ -307,14 +307,14 @@
Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
by (simp_tac
(simpset() addsimps [lift_prog_correct, lift_set_correct,
- lift_export reachable_extend_eq]) 1);
+ lift_export0 reachable_extend_eq]) 1);
qed "reachable_lift_prog";
Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \
\ (F : A Co B)";
by (simp_tac
(simpset() addsimps [lift_prog_correct, lift_set_correct,
- lift_export extend_Constrains]) 1);
+ lift_export0 extend_Constrains]) 1);
qed "lift_prog_Constrains";
Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
@@ -326,7 +326,7 @@
\ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
by (asm_full_simp_tac
(simpset() addsimps [lift_prog_correct, drop_prog_correct,
- lift_set_correct, lift_export project_Constrains_D]) 1);
+ lift_set_correct, lift_export0 project_Constrains_D]) 1);
qed "drop_prog_Constrains_D";
Goalw [Stable_def]
@@ -341,7 +341,7 @@
\ ==> lift_prog i F Join G : Always (lift_set i A)";
by (asm_full_simp_tac
(simpset() addsimps [lift_prog_correct, drop_prog_correct,
- lift_set_correct, lift_export project_Always_D]) 1);
+ lift_set_correct, lift_export0 project_Always_D]) 1);
qed "drop_prog_Always_D";
Goalw [Increasing_def]
@@ -359,7 +359,7 @@
\ ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
by (asm_full_simp_tac
(simpset() addsimps [lift_prog_correct, drop_prog_correct,
- drop_set_correct, lift_export project_extend_Join]) 1);
+ drop_set_correct, lift_export0 project_extend_Join]) 1);
qed "drop_prog_lift_prog_Join";
@@ -367,7 +367,7 @@
Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
- lift_export extend_transient]) 1);
+ lift_export0 extend_transient]) 1);
qed "lift_prog_transient";
Goal "(lift_prog i F : transient (lift_set j A)) = \
@@ -384,7 +384,7 @@
Goal "lift_prog i F : preserves (v o sub j) = \
\ (if i=j then F : preserves v else True)";
by (simp_tac (simpset() addsimps [lift_prog_correct,
- lift_export extend_preserves]) 1);
+ lift_export0 extend_preserves]) 1);
by (auto_tac (claset(),
simpset() addsimps [preserves_def, extend_def, extend_act_def,
stable_def, constrains_def, lift_map_def]));
@@ -395,20 +395,21 @@
Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
by (asm_simp_tac
(simpset() addsimps [drop_prog_correct, fold_o_sub,
- lift_export project_preserves_I]) 1);
+ lift_export0 project_preserves_I]) 1);
qed "drop_prog_preserves_I";
(*The raw version*)
val [xguary,drop_prog,lift_prog] =
Goal "[| F : X guarantees[v] Y; \
-\ !!G. lift_prog i F Join G : X' ==> F Join drop_prog i C G : X; \
-\ !!G. [| F Join drop_prog i C G : Y; lift_prog i F Join G : X' |] \
+\ !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X; \
+\ !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
+\ G : preserves (v o sub i) |] \
\ ==> lift_prog i F Join G : Y' |] \
\ ==> lift_prog i F : X' guarantees[v o sub i] Y'";
by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
by (etac drop_prog_preserves_I 1);
by (etac drop_prog 1);
-by (assume_tac 1);
+by Auto_tac;
qed "drop_prog_guarantees_raw";
Goal "[| F : X guarantees[v] Y; \
@@ -418,7 +419,7 @@
\ ==> lift_prog i F : X' guarantees[w] Y'";
by (asm_simp_tac
(simpset() addsimps [lift_prog_correct, fold_o_sub,
- lift_export project_guarantees]) 1);
+ lift_export0 project_guarantees]) 1);
qed "drop_prog_guarantees";
@@ -443,13 +444,13 @@
Goal "F : UNIV guarantees[v] increasing func \
\ ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
-by (dtac (lift_export extend_guar_increasing) 1);
+by (dtac (lift_export0 extend_guar_increasing) 1);
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_guar_increasing";
Goal "F : UNIV guarantees[v] Increasing func \
\ ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
-by (dtac (lift_export extend_guar_Increasing) 1);
+by (dtac (lift_export0 extend_guar_Increasing) 1);
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_guar_Increasing";
@@ -458,5 +459,16 @@
\ Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
by (asm_simp_tac
(simpset() addsimps [lift_set_correct, lift_prog_correct,
- lift_export extend_guar_Always]) 1);
+ lift_export0 extend_guar_Always]) 1);
qed "lift_prog_guar_Always";
+
+(*version for outside use*)
+fun lift_export th =
+ good_map_lift_map RS export th
+ |> simplify
+ (simpset() addsimps [fold_o_sub,
+ drop_set_correct RS sym,
+ lift_set_correct RS sym,
+ drop_prog_correct RS sym,
+ lift_prog_correct RS sym]);;
+
--- a/src/HOL/UNITY/Lift_prog.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Thu Jan 13 17:30:23 2000 +0100
@@ -6,7 +6,7 @@
lift_prog, etc: replication of components
*)
-Lift_prog = ELT +
+Lift_prog = Project +
constdefs
--- a/src/HOL/UNITY/Project.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Project.ML Thu Jan 13 17:30:23 2000 +0100
@@ -10,6 +10,12 @@
POSSIBLY CAN DELETE Restrict_image_Diff
*)
+(*EQUALITIES.ML*)
+ Goal "(A <= -A) = (A = {})";
+ by (Blast_tac 1);
+ qed "subset_Compl_self_eq";
+
+
Open_locale "Extend";
(** projection: monotonicity for safety **)
@@ -137,7 +143,34 @@
extend_constrains]) 1);
qed "project_constrains_D";
-(** "projecting" and union/intersection (no converses) **)
+
+(*** preserves ***)
+
+Goal "G : preserves (v o f) ==> project h C G : preserves v";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, project_stable_I,
+ Collect_eq_extend_set RS sym]));
+qed "project_preserves_I";
+
+(*to preserve f is to preserve the whole original state*)
+Goal "G : preserves f ==> project h C G : preserves id";
+by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
+qed "project_preserves_id_I";
+
+Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, extend_stable RS sym,
+ Collect_eq_extend_set RS sym]));
+qed "extend_preserves";
+
+Goal "inj h ==> (extend h G : preserves g)";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, extend_def, extend_act_def,
+ stable_def, constrains_def, g_def]));
+qed "inj_extend_preserves";
+
+
+(*** "projecting" and union/intersection (no converses) ***)
Goalw [projecting_def]
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \
@@ -446,7 +479,7 @@
qed "extending_Increasing";
-(*** leadsETo in the precondition ***)
+(*** leadsETo in the precondition (??) ***)
(** transient **)
@@ -533,7 +566,8 @@
Join_stable, Join_transient]));
qed_spec_mp "Join_project_ensures";
-(** Lemma useful for both STRONG and WEAK progress*)
+(** Lemma useful for both STRONG and WEAK progress, but the transient
+ condition's very strong **)
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
@@ -568,32 +602,91 @@
qed "Join_project_LeadsTo";
-(*** GUARANTEES and EXTEND ***)
+(*** Towards project_Ensures_D ***)
+
+
-(** preserves **)
+Goalw [project_set_def, extend_set_def, project_act_def]
+ "act ^^ (C Int extend_set h A) <= B \
+\ ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
+\ <= project_set h B";
+by (Blast_tac 1);
+qed "act_subset_imp_project_act_subset";
+
-Goal "G : preserves (v o f) ==> project h C G : preserves v";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, project_stable_I,
- Collect_eq_extend_set RS sym]));
-qed "project_preserves_I";
+Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \
+\ project h C G : transient (project_set h C Int A - B) |] \
+\ ==> G : transient (C Int extend_set h A - extend_set h B)";
+by (case_tac "C Int extend_set h A <= extend_set h B" 1);
+by (asm_simp_tac (simpset() addsimps [Diff_eq_empty_iff RS iffD2]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [transient_def, subset_Compl_self_eq,
+ Domain_project_act, split_extended_all]));
+by (Blast_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def, constrains_def]));
+by (ball_tac 1);
+by (thin_tac "ALL act: Acts G. ?P act" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Int_Diff,
+ extend_set_Diff_distrib RS sym]));
+bd act_subset_imp_project_act_subset 1;
+by (subgoal_tac
+ "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
+bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
+(*using Int_greatest actually slows the next step!*)
+by (Blast_tac 2);
+by (force_tac (claset(),
+ simpset() addsimps [split_extended_all]) 1);
+qed "stable_project_transient";
+
-(*to preserve f is to preserve the whole original state*)
-Goal "G : preserves f ==> project h C G : preserves id";
-by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
-qed "project_preserves_id_I";
+Goal "[| G : stable C; project h C G : (project_set h C Int A) unless B |] \
+\ ==> G : (C Int extend_set h A) unless (extend_set h B)";
+by (auto_tac
+ (claset() addDs [stable_constrains_Int]
+ addIs [constrains_weaken],
+ simpset() addsimps [unless_def, project_constrains, Diff_eq,
+ Int_assoc, Int_extend_set_lemma]));
+qed_spec_mp "project_unless2";
-Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_stable RS sym,
- Collect_eq_extend_set RS sym]));
-qed "extend_preserves";
+Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \
+\ F Join project h C G : (project_set h C Int A) ensures B; \
+\ extend h F Join G : stable C |] \
+\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
+(*unless*)
+by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2]
+ addIs [project_extend_constrains_I],
+ simpset() addsimps [ensures_def, Join_constrains,
+ Join_stable]));
+(*transient*)
+by (auto_tac (claset(), simpset() addsimps [Join_transient]));
+by (blast_tac (claset() addIs [stable_project_transient]) 2);
+by (force_tac (claset() addSEs [extend_transient RS iffD2 RS
+ transient_strengthen],
+ simpset() addsimps [Join_transient, split_extended_all]) 1);
+qed "project_ensures_D_lemma";
-Goal "inj h ==> (extend h G : preserves g)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_def, extend_act_def,
- stable_def, constrains_def, g_def]));
-qed "inj_extend_preserves";
+Goal "[| F Join project h UNIV G : A ensures B; \
+\ G : stable (extend_set h A - extend_set h B) |] \
+\ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
+br (project_ensures_D_lemma RS revcut_rl) 1;
+by (stac stable_UNIV 3);
+auto();
+qed "project_ensures_D";
+
+Goalw [Ensures_def]
+ "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B; \
+\ G : stable (reachable (extend h F Join G) Int extend_set h A - \
+\ extend_set h B) |] \
+\ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
+br (project_ensures_D_lemma RS revcut_rl) 1;
+by (auto_tac (claset(),
+ simpset() addsimps [project_set_reachable_extend_eq RS sym]));
+qed "project_Ensures_D";
+
+
+(*** GUARANTEES and EXTEND ***)
(** Strong precondition and postcondition; doesn't seem very useful. **)
@@ -630,14 +723,15 @@
(*The raw version*)
val [xguary,project,extend] =
Goal "[| F : X guarantees[v] Y; \
-\ !!G. extend h F Join G : X' ==> F Join project h C G : X; \
-\ !!G. [| F Join project h C G : Y; extend h F Join G : X' |] \
+\ !!G. extend h F Join G : X' ==> F Join project h (C G) G : X; \
+\ !!G. [| F Join project h (C G) G : Y; extend h F Join G : X'; \
+\ G : preserves (v o f) |] \
\ ==> extend h F Join G : Y' |] \
\ ==> extend h F : X' guarantees[v o f] Y'";
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
by (etac project_preserves_I 1);
by (etac project 1);
-by (assume_tac 1);
+by Auto_tac;
qed "project_guarantees_raw";
Goal "[| F : X guarantees[v] Y; \
--- a/src/HOL/UNITY/SubstAx.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Thu Jan 13 17:30:23 2000 +0100
@@ -157,24 +157,28 @@
(** More rules using the premise "Always INV" **)
-Goal "[| F : (A-A') Co (A Un A'); F : transient (A-A') |] \
-\ ==> F : A LeadsTo A'";
+Goal "F : A Ensures B ==> F : A LeadsTo B";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
-by (rtac (ensuresI RS leadsTo_Basis) 1);
-by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
+ (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
qed "LeadsTo_Basis";
+Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \
+\ ==> F : A Ensures B";
+by (asm_full_simp_tac
+ (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
+ transient_strengthen]) 1);
+qed "EnsuresI";
+
Goal "[| F : Always INV; \
\ F : (INV Int (A-A')) Co (A Un A'); \
\ F : transient (INV Int (A-A')) |] \
\ ==> F : A LeadsTo A'";
by (rtac Always_LeadsToI 1);
by (assume_tac 1);
-by (rtac LeadsTo_Basis 1);
-by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [Always_ConstrainsD RS Constrains_weaken]) 1);
+by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
+ Always_ConstrainsD RS Constrains_weaken,
+ transient_strengthen]) 1);
qed "Always_LeadsTo_Basis";
(*Set difference: maybe combine with leadsTo_weaken_L??
@@ -420,7 +424,7 @@
etac Always_LeadsTo_Basis 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
- ensuresI] 1),
+ EnsuresI, ensuresI] 1),
(*now there are two subgoals: co & transient*)
simp_tac (simpset() addsimps !program_defs_ref) 2,
res_inst_tac [("act", sact)] transientI 2,
--- a/src/HOL/UNITY/SubstAx.thy Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Thu Jan 13 17:30:23 2000 +0100
@@ -9,6 +9,9 @@
SubstAx = WFair + Constrains +
constdefs
+ Ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
+ "A Ensures B == {F. F : (reachable F Int A) ensures B}"
+
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
"A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
--- a/src/HOL/UNITY/Union.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Union.ML Thu Jan 13 17:30:23 2000 +0100
@@ -181,6 +181,10 @@
simpset() addsimps [constrains_def, Join_def]));
qed "Join_constrains";
+Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)";
+by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
+qed "Join_unless";
+
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F Join G) could be much bigger than reachable F, reachable G
*)
--- a/src/HOL/UNITY/WFair.ML Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML Thu Jan 13 17:30:23 2000 +0100
@@ -79,12 +79,15 @@
by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
qed "stable_ensures_Int";
-(*NEVER USED*)
Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B";
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
qed "stable_transient_ensures";
+Goal "(A ensures B) = (A unless B) Int transient (A-B)";
+by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1);
+qed "ensures_eq";
+
(*** leadsTo ***)