--- a/src/HOL/UNITY/Alloc.ML Wed Oct 13 12:04:11 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Wed Oct 13 12:05:25 1999 +0200
@@ -5,11 +5,13 @@
Specification of Chandy and Charpentier's Allocator
-STOP USING o (COMPOSITION), since function application is naturally associative
+Stop using o (composition)?
guarantees_PLam_I looks wrong: refers to lift_prog
*)
+(*Eliminating the "o" operator gives associativity for free*)
+val o_simp = simplify (simpset() addsimps [o_def]);
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
by (induct_tac "n" 1);
@@ -86,7 +88,8 @@
Goalw [sysOfClient_def] "inj sysOfClient";
by (rtac injI 1);
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
- addSWrapper record_split_wrapper, simpset()));
+ addSWrapper record_split_wrapper,
+ simpset()));
qed "inj_sysOfClient";
Goalw [sysOfClient_def] "surj sysOfClient";
@@ -197,11 +200,6 @@
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
-(* F : UNIV guarantees Increasing func
- ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
-val extend_Client_guar_Increasing =
- client_export extend_guar_Increasing;
-
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
Goal "i < Nclients \
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
@@ -209,13 +207,26 @@
by (auto_tac (claset(), simpset() addsimps [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 Auto_tac;
+qed "System_Increasing_allocGiv";
-(*** Proof of the safety property (1) ***)
+
-(*safety (1), step 1*)
+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);
+by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
+by Auto_tac;
+qed "System_Increasing_ask";
+
Goalw [System_def]
"i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2
+by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2
RS guaranteesD) 1);
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
(*gets Client_Increasing_rel from simpset*)
@@ -223,6 +234,40 @@
qed "System_Increasing_rel";
+(** Follows consequences.
+ The "Always (INT ...) formulation expresses the general safety property
+ and allows it to be combined using Always_Int_rule below. **)
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
+by (auto_tac (claset(),
+ simpset() delsimps [o_apply]
+ addsimps [Always_INT_distrib, Follows_Bounded,
+ Network_Giv RS component_guaranteesD,
+ extend_Alloc_Increasing_allocGiv RS component_guaranteesD]));
+qed "Always_giv_le_allocGiv";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
+by (auto_tac (claset(),
+ simpset() delsimps [o_apply]
+ addsimps [Always_INT_distrib, Follows_Bounded,
+ [Network_Ask, System_Increasing_ask] MRS component_guaranteesD]));
+qed "Always_allocAsk_le_ask";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
+by (auto_tac (claset(),
+ simpset() delsimps [o_apply]
+ addsimps [Always_INT_distrib, Follows_Bounded,
+ [Network_Rel, System_Increasing_rel] MRS component_guaranteesD]));
+qed "Always_allocRel_le_rel";
+
+
+(*** Proof of the safety property (1) ***)
+
+(*safety (1), step 1 is System_Increasing_rel*)
+
(*safety (1), step 2*)
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
by (rtac Follows_Increasing1 1);
@@ -242,8 +287,8 @@
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
by (rtac (Alloc_Safety RS project_guarantees) 1);
(*1: Increasing precondition*)
-br (ballI RS projecting_INT) 1;
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken) 1);
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS
+ projecting_INT) 1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
(*2: Always postcondition*)
@@ -253,43 +298,27 @@
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
qed "System_sum_bounded";
-(*safety (1), step 4*)
+(** Follows reasoning **)
+
Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o giv o sub i o client) s \
\ <= (tokens o sub i o allocGiv) s})";
-by (auto_tac (claset(),
- simpset() delsimps [o_apply]
- addsimps [Always_INT_distrib]));
-by (rtac Follows_Bounded 1);
-by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1);
-by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1);
-by (simp_tac (HOL_ss addsimps [o_assoc]) 1);
-by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD,
- extend_Alloc_Increasing_allocGiv RS component_guaranteesD]) 1);
-qed "System_Always_giv_le_allocGiv";
+by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
+by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
+qed "Always_tokens_giv_le_allocGiv";
-
-(*safety (1), step 5*)
Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o sub i o allocRel) s \
\ <= (tokens o rel o sub i o client) s})";
-by (auto_tac (claset(),
- simpset() delsimps [o_apply]
- addsimps [Always_INT_distrib]));
-by (rtac Follows_Bounded 1);
-by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1);
-by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1);
-by (simp_tac (HOL_ss addsimps [o_assoc]) 1);
-by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
- System_Increasing_rel]) 1);
-qed "System_Always_allocRel_le_rel";
+by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
+by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
+qed "Always_tokens_allocRel_le_rel";
-
-(*safety (1), step 6*)
+(*safety (1), step 4 (final result!) *)
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
\ <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
-by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv,
- System_Always_allocRel_le_rel] RS Always_weaken) 1);
+by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv,
+ Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
by Auto_tac;
by (rtac (sum_mono RS order_trans) 1);
by (dtac order_trans 2);
@@ -305,33 +334,92 @@
(*we begin with proofs identical to System_Increasing_rel and
System_Increasing_allocRel: tactics needed!*)
-(*progress (2), step 1*)
-Goalw [System_def]
- "i < Nclients ==> System : Increasing (ask o sub i o client)";
-by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2
- RS guaranteesD) 1);
-by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
-by Auto_tac;
-qed "System_Increasing_ask";
+(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*)
-(*progress (2), step 2*)
+(*progress (2), step 2; see also System_Increasing_allocRel*)
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
by (rtac Follows_Increasing1 1);
by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
System_Increasing_ask]) 1);
qed "System_Increasing_allocAsk";
+val Client_i_Bounded =
+ [Client_Bounded, projecting_UNIV, lift_export extending_Always]
+ MRS drop_prog_guarantees;
+
+val UNIV_guar_Always =
+ [asm_rl, projecting_UNIV, extending_Always]
+ MRS project_guarantees;
+
+
(*progress (2), step 3*)
-(*All this trouble just to lift "Client_Bounded" through two extemd ops*)
+(*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 (lift_prog_guar_Always RS
- guarantees_PLam_I RS client_export extend_guar_Always RS
+by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS
guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
-by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1);
+by (rtac Client_i_Bounded 1);
by (auto_tac(claset(),
- simpset() addsimps [Collect_eq_lift_set RS sym,
+ simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
client_export Collect_eq_extend_set RS sym]));
-qed "System_Bounded";
+qed "System_Bounded_ask";
+
+(*progress (2), step 4*)
+Goal "System : Always {s. ALL i : lessThan Nclients. \
+\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+by (auto_tac (claset(),
+ simpset() addsimps [Collect_ball_eq, Always_INT_distrib]));
+by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
+ RS Always_weaken) 1);
+by (auto_tac(claset() addDs [set_mono], simpset()));
+qed "System_Bounded_allocAsk";
+
+(*progress (2), step 5*)
+
+Goal "i < Nclients ==> System : Increasing (giv o sub i o client)";
+by (rtac Follows_Increasing1 1);
+by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD,
+ System_Increasing_allocGiv]) 1);
+qed "System_Increasing_giv";
+
+(*progress (2), step 6*)
+
+(*A LOT of work just to lift "Client_Progress" to the array*)
+Goal "lift_prog i Client \
+\ : Increasing (giv o sub i) Int ((%z. z i) localTo (lift_prog i Client)) \
+\ guarantees \
+\ (INT h. {s. h <= (giv o sub i) s & \
+\ h pfixGe (ask o sub i) s} \
+\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
+br (Client_Progress RS drop_prog_guarantees) 1;
+br (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
+br subset_refl 4;
+by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
+by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2);
+by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
+by (auto_tac (claset(), simpset() addsimps [o_def]));
+qed "Client_i_Progress";
+
+Goalw [System_def]
+ "i < Nclients \
+\ ==> System : (INT h. {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s} \
+\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
+br (guarantees_PLam_I RS project_guarantees) 1;
+br Client_i_Progress 1;
+by (Force_tac 1);
+br (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
+br subset_refl 4;
+by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+br projecting_Int 1;
+br (client_export projecting_Increasing) 1;
+br (client_export projecting_localTo) 1;
+
+by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
+
+by (rtac (client_export ) 1);
+
+Client_Progress;
--- a/src/HOL/UNITY/Project.ML Wed Oct 13 12:04:11 1999 +0200
+++ b/src/HOL/UNITY/Project.ML Wed Oct 13 12:05:25 1999 +0200
@@ -124,16 +124,30 @@
extend_constrains]) 1);
qed "project_constrains_D";
+(** "projecting" and union/intersection **)
+
Goalw [projecting_def]
- "[| ALL i:I. projecting C h F (X' i) (X i) |] \
+ "[| projecting C h F XA' XA; projecting C h F XB' XB |] \
+\ ==> projecting C h F (XA' Int XB') (XA Int XB)";
+by (Blast_tac 1);
+qed "projecting_Int";
+
+Goalw [projecting_def]
+ "[| projecting C h F XA' XA; projecting C h F XB' XB |] \
+\ ==> projecting C h F (XA' Un XB') (XA Un XB)";
+by (Blast_tac 1);
+qed "projecting_Un";
+
+val [prem] = Goalw [projecting_def]
+ "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
-by Auto_tac;
+by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "projecting_INT";
-Goalw [projecting_def]
- "[| ALL i:I. projecting C h F (X' i) (X i) |] \
+val [prem] = Goalw [projecting_def]
+ "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
-by Auto_tac;
+by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "projecting_UN";
Goalw [projecting_def]
@@ -141,17 +155,30 @@
by Auto_tac;
qed "projecting_weaken";
-(*Is this the right way to handle the X' argument?*)
+Goalw [extending_def]
+ "[| extending C h F X' YA' YA; extending C h F X' YB' YB |] \
+\ ==> extending C h F X' (YA' Int YB') (YA Int YB)";
+by (Blast_tac 1);
+qed "extending_Int";
+
Goalw [extending_def]
- "[| ALL i:I. extending C h F (X' i) (Y' i) (Y i) |] \
-\ ==> extending C h F (INT i:I. X' i) (INT i:I. Y' i) (INT i:I. Y i)";
-by Auto_tac;
+ "[| extending C h F X' YA' YA; extending C h F X' YB' YB |] \
+\ ==> extending C h F X' (YA' Un YB') (YA Un YB)";
+by (Blast_tac 1);
+qed "extending_Un";
+
+(*This is the right way to handle the X' argument. Having (INT i:I. X' i)
+ would strengthen the premise.*)
+val [prem] = Goalw [extending_def]
+ "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
+\ ==> extending C h F X' (INT i:I. Y' i) (INT i:I. Y i)";
+by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "extending_INT";
-Goalw [extending_def]
- "[| ALL i:I. extending C h F X' (Y' i) (Y i) |] \
+val [prem] = Goalw [extending_def]
+ "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
\ ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
-by Auto_tac;
+by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "extending_UN";
Goalw [extending_def]
@@ -203,6 +230,13 @@
(*Opposite direction fails because Diff in the extended state may remove
fewer actions, i.e. those that affect other state variables.*)
+
+Goal "Diff (project C h G) (project_act C h `` acts) <= \
+\ project C h (Diff G acts)";
+by (auto_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def,
+ UN_subset_iff]));
+qed "Diff_project_project_component_project_Diff";
+
Goal "(UN act:acts. Domain act) <= project_set h C \
\ ==> Diff (project C h G) acts <= \
\ project C h (Diff G (extend_act h `` acts))";
@@ -610,6 +644,21 @@
(*Weak precondition and postcondition; this is the good one!
Not clear that it has a converse [or that we want one!]*)
+
+(*The raw version*)
+val [xguary,project,extend] =
+Goal "[| F : X guarantees Y; \
+\ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \
+\ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
+\ Disjoint (extend h F) G |] \
+\ ==> extend h F Join G : Y' |] \
+\ ==> extend h F : X' guarantees Y'";
+by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
+by (etac project 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "project_guarantees_lemma";
+
Goal "[| F : X guarantees Y; \
\ projecting C h F X' X; extending C h F X' Y' Y |] \
\ ==> extend h F : X' guarantees Y'";
@@ -618,7 +667,7 @@
simpset() addsimps [guaranteesD, projecting_def, extending_def]));
qed "project_guarantees";
-(** It seems that neither "guarantees" law can be proved from the other. **)
+(*It seems that neither "guarantees" law can be proved from the other.*)
(*** guarantees corollaries ***)
@@ -732,8 +781,8 @@
Goalw [extending_def]
"extending (%G. reachable (extend h F Join G)) h F \
-\ (f localTo extend h F) \
-\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
+\ (f localTo extend h F) \
+\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
addIs [project_LeadsTo_D]) 1);
qed "extending_LeadsTo";