--- a/src/HOL/UNITY/Alloc.thy Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy Thu Aug 26 11:36:04 1999 +0200
@@ -67,18 +67,18 @@
(*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
client_increasing :: clientState program set
"client_increasing ==
- UNIV guar Increasing ask Int Increasing rel"
+ UNIV guarantees Increasing ask Int Increasing rel"
(*spec (4)*)
client_bounded :: clientState program set
"client_bounded ==
- UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}"
+ UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
(*spec (5)*)
client_progress :: clientState program set
"client_progress ==
Increasing giv
- guar
+ guarantees
(INT h. {s. h <= giv s & h pfixGe ask s}
LeadsTo
{s. tokens h <= (tokens o rel) s})"
@@ -92,14 +92,14 @@
alloc_increasing :: allocState program set
"alloc_increasing ==
UNIV
- guar
+ guarantees
(INT i : lessThan Nclients. Increasing (sub i o allocAsk))"
(*spec (7)*)
alloc_safety :: allocState program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
- guar
+ guarantees
Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
<= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
@@ -116,7 +116,7 @@
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
- guar
+ guarantees
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
@@ -130,21 +130,21 @@
network_ask :: systemState program set
"network_ask == INT i : lessThan Nclients.
Increasing (ask o sub i o client)
- guar
+ guarantees
((sub i o allocAsk) Fols (ask o sub i o client))"
(*spec (9.2)*)
network_giv :: systemState program set
"network_giv == INT i : lessThan Nclients.
Increasing (sub i o allocGiv)
- guar
+ guarantees
((giv o sub i o client) Fols (sub i o allocGiv))"
(*spec (9.3)*)
network_rel :: systemState program set
"network_rel == INT i : lessThan Nclients.
Increasing (rel o sub i o client)
- guar
+ guarantees
((sub i o allocRel) Fols (rel o sub i o client))"
network_spec :: systemState program set
--- a/src/HOL/UNITY/Client.ML Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Thu Aug 26 11:36:04 1999 +0200
@@ -74,7 +74,7 @@
(*Safety property 2: clients return the right number of tokens*)
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \
-\ guar Always {s. rel s <= giv s}";
+\ guarantees Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
by (rtac AlwaysI 1);
by (Force_tac 1);
@@ -101,7 +101,7 @@
Goal "Cli_prg : \
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
-\ guar Always ({s. size (ask s) <= Suc (size (rel s))} Int \
+\ guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
\ {s. size (rel s) <= size (giv s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
@@ -121,7 +121,7 @@
Goal "Cli_prg : \
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
\ Int Always giv_meets_ask) \
-\ guar ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
+\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (rtac Stable_transient_Always_LeadsTo 1);
--- a/src/HOL/UNITY/Comp.ML Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Thu Aug 26 11:36:04 1999 +0200
@@ -11,6 +11,14 @@
(*** component ***)
Goalw [component_def]
+ "H component F | H component G ==> H component (F Join G)";
+by Auto_tac;
+by (res_inst_tac [("x", "G Join Ga")] exI 1);
+by (res_inst_tac [("x", "G Join F")] exI 2);
+by (auto_tac (claset(), simpset() addsimps Join_ac));
+qed "componentI";
+
+Goalw [component_def]
"(F component G) = (Init G <= Init F & Acts F <= Acts G)";
by (force_tac (claset() addSIs [exI, program_equalityI],
simpset() addsimps [Acts_Join]) 1);
@@ -122,73 +130,81 @@
val prems = Goal
"(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \
-\ ==> F : X guar Y";
-by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
+\ ==> F : X guarantees Y";
+by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
by (blast_tac (claset() addIs prems) 1);
qed "guaranteesI";
-Goalw [guarantees_def, component_def]
- "[| F : X guar Y; F Join G : X |] ==> F Join G : Y";
+Goalw [guar_def, component_def]
+ "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y";
by (Blast_tac 1);
qed "guaranteesD";
+(*This version of guaranteesD matches more easily in the conclusion*)
+Goalw [guar_def]
+ "[| F : X guarantees Y; H : X; F component H |] ==> H : Y";
+by (Blast_tac 1);
+qed "component_guaranteesD";
+
(*This equation is more intuitive than the official definition*)
-Goal "(F : X guar Y) = \
+Goal "(F : X guarantees Y) = \
\ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
-by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
+by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
by (Blast_tac 1);
qed "guarantees_eq";
-Goalw [guarantees_def] "[| F: X guar X'; Y <= X; X' <= Y' |] ==> F: Y guar Y'";
+Goalw [guar_def]
+ "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
by (Blast_tac 1);
qed "guarantees_weaken";
-Goalw [guarantees_def] "[| F: X guar Y; F component F' |] ==> F': X guar Y";
+Goalw [guar_def]
+ "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y";
by (blast_tac (claset() addIs [component_trans]) 1);
qed "guarantees_weaken_prog";
-Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
+Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
by (Blast_tac 1);
qed "subset_imp_guarantees_UNIV";
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
+Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
by (Blast_tac 1);
qed "subset_imp_guarantees";
(*Remark at end of section 4.1*)
-Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
+Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
by (blast_tac (claset() addEs [equalityE]) 1);
qed "ex_prop_equiv2";
(** Distributive laws. Re-orient to perform miniscoping **)
-Goalw [guarantees_def]
- "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
+Goalw [guar_def]
+ "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
by (Blast_tac 1);
qed "guarantees_UN_left";
-Goalw [guarantees_def]
- "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
+Goalw [guar_def]
+ "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
by (Blast_tac 1);
qed "guarantees_Un_left";
-Goalw [guarantees_def]
- "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
+Goalw [guar_def]
+ "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
by (Blast_tac 1);
qed "guarantees_INT_right";
-Goalw [guarantees_def]
- "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
+Goalw [guar_def]
+ "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
by (Blast_tac 1);
qed "guarantees_Int_right";
-Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
+Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
by (Blast_tac 1);
qed "shunting";
-Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
+Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
by (Blast_tac 1);
qed "contrapositive";
@@ -196,43 +212,45 @@
is more faithful to the text but looks cryptic.
**)
-Goalw [guarantees_def]
- "[| F : V guar X; F : (X Int Y) guar Z |]\
-\ ==> F : (V Int Y) guar Z";
+Goalw [guar_def]
+ "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
+\ ==> F : (V Int Y) guarantees Z";
by (Blast_tac 1);
qed "combining1";
-Goalw [guarantees_def]
- "[| F : V guar (X Un Y); F : Y guar Z |]\
-\ ==> F : V guar (X Un Z)";
+Goalw [guar_def]
+ "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\
+\ ==> F : V guarantees (X Un Z)";
by (Blast_tac 1);
qed "combining2";
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
does not suit Isabelle... **)
-(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
-Goalw [guarantees_def]
- "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
+(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+Goalw [guar_def]
+ "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
by (Blast_tac 1);
qed "all_guarantees";
-(*Premises should be [| F: X guar Y i; i: I |] *)
-Goalw [guarantees_def]
- "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
+Goalw [guar_def]
+ "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
by (Blast_tac 1);
qed "ex_guarantees";
(*** Additional guarantees laws, by lcp ***)
-Goalw [guarantees_def]
- "[| F: U guar V; G: X guar Y |] ==> F Join G: (U Int X) guar (V Int Y)";
+Goalw [guar_def]
+ "[| F: U guarantees V; G: X guarantees Y |] \
+\ ==> F Join G: (U Int X) guarantees (V Int Y)";
by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
by (Blast_tac 1);
qed "guarantees_Join_Int";
-Goalw [guarantees_def]
- "[| F: U guar V; G: X guar Y |] ==> F Join G: (U Un X) guar (V Un Y)";
+Goalw [guar_def]
+ "[| F: U guarantees V; G: X guarantees Y |] \
+\ ==> F Join G: (U Un X) guarantees (V Un Y)";
by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
by (Blast_tac 1);
qed "guarantees_Join_Un";
@@ -242,16 +260,16 @@
by (Blast_tac 1);
qed "JN_component_iff";
-Goalw [guarantees_def]
- "[| ALL i:I. F i : X i guar Y i |] \
-\ ==> (JOIN I F) : (INTER I X) guar (INTER I Y)";
+Goalw [guar_def]
+ "[| ALL i:I. F i : X i guarantees Y i |] \
+\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
by (Blast_tac 1);
bind_thm ("guarantees_JN_INT", ballI RS result());
-Goalw [guarantees_def]
- "[| ALL i:I. F i : X i guar Y i |] \
-\ ==> (JOIN I F) : (UNION I X) guar (UNION I Y)";
+Goalw [guar_def]
+ "[| ALL i:I. F i : X i guarantees Y i |] \
+\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
by (Blast_tac 1);
bind_thm ("guarantees_JN_UN", ballI RS result());
@@ -259,14 +277,14 @@
(*** guarantees laws for breaking down the program, by lcp ***)
-Goalw [guarantees_def]
- "F: X guar Y | G: X guar Y ==> F Join G: X guar Y";
+Goalw [guar_def]
+ "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
by (Blast_tac 1);
qed "guarantees_Join_I";
-Goalw [guarantees_def]
- "[| i : I; F i: X guar Y |] ==> (JN i:I. (F i)) : X guar Y";
+Goalw [guar_def]
+ "[| i : I; F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
by (Blast_tac 1);
qed "guarantees_JN_I";
--- a/src/HOL/UNITY/Lift_prog.ML Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Thu Aug 26 11:36:04 1999 +0200
@@ -346,13 +346,13 @@
by (etac reachable_lift_prog_Join_D 1);
qed "reachable_lift_prog_Join_subset";
-Goal "F Join drop_prog i G : Stable A \
-\ ==> lift_prog i F Join G : Stable (lift_set i A)";
-by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def]) 1);
+Goalw [Constrains_def]
+ "F Join drop_prog i G : A Co B \
+\ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
by (subgoal_tac
"lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \
\ lift_set i A \
-\ co lift_set i A" 1);
+\ co lift_set i B" 1);
by (asm_full_simp_tac
(simpset() addsimps [lift_set_Int RS sym,
lift_prog_constrains,
@@ -360,6 +360,12 @@
drop_prog_lift_prog_Join]) 2);
by (blast_tac (claset() addIs [constrains_weaken,
reachable_lift_prog_Join_D]) 1);
+qed "lift_prog_Join_Constrains";
+
+Goal "F Join drop_prog i G : Stable A \
+\ ==> lift_prog i F Join G : Stable (lift_set i A)";
+by (asm_full_simp_tac (simpset() addsimps [Stable_def,
+ lift_prog_Join_Constrains]) 1);
qed "lift_prog_Join_Stable";
@@ -369,8 +375,8 @@
(*Strong precondition and postcondition; doesn't seem very useful.
Probably can be strengthened to an equivalance.*)
-Goal "F : X guar Y \
-\ ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)";
+Goal "F : X guarantees Y \
+\ ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
@@ -378,10 +384,10 @@
(*Weak precondition and postcondition; this is the good one!*)
val [xguary,drop_prog,lift_prog] =
-Goal "[| F : X guar Y; \
+Goal "[| F : X guarantees Y; \
\ !!H. H : XX ==> drop_prog i H : X; \
\ !!G. F Join drop_prog i G : Y ==> lift_prog i F Join G : YY |] \
-\ ==> lift_prog i F : XX guar YY";
+\ ==> lift_prog i F : XX guarantees YY";
by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
by (dtac drop_prog 1);
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
@@ -421,8 +427,8 @@
(*** guarantees corollaries ***)
Goalw [increasing_def]
- "F : UNIV guar increasing f \
-\ ==> lift_prog i F : UNIV guar increasing (f o sub i)";
+ "F : UNIV guarantees increasing f \
+\ ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 1);
@@ -432,8 +438,8 @@
qed "lift_prog_guar_increasing";
Goalw [Increasing_def]
- "F : UNIV guar Increasing f \
-\ ==> lift_prog i F : UNIV guar Increasing (f o sub i)";
+ "F : UNIV guarantees Increasing f \
+\ ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 1);
@@ -441,9 +447,9 @@
qed "lift_prog_guar_Increasing";
Goalw [localTo_def, increasing_def]
- "F : (f localTo F) guar increasing f \
+ "F : (f localTo F) guarantees increasing f \
\ ==> lift_prog i F : (f o sub i) localTo (lift_prog i F) \
-\ guar increasing (f o sub i)";
+\ guarantees increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 2);
@@ -458,9 +464,9 @@
qed "lift_prog_localTo_guar_increasing";
Goalw [localTo_def, Increasing_def]
- "F : (f localTo F) guar Increasing f \
+ "F : (f localTo F) guarantees Increasing f \
\ ==> lift_prog i F : (f o sub i) localTo (lift_prog i F) \
-\ guar Increasing (f o sub i)";
+\ guarantees Increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 2);
--- a/src/HOL/UNITY/PPROD.ML Thu Aug 26 11:34:17 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Thu Aug 26 11:36:04 1999 +0200
@@ -263,20 +263,21 @@
(*** guarantees properties ***)
Goalw [PLam_def]
- "[| i : I; lift_prog i (F i): X guar Y |] ==> (PLam I F) : X guar Y";
+ "[| i : I; lift_prog i (F i): X guarantees Y |] \
+\ ==> (PLam I F) : X guarantees Y";
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
qed "guarantees_PLam_I";
Goalw [PLam_def]
- "[| ALL i:I. F i : X guar Y |] \
+ "[| ALL i:I. F i : X guarantees Y |] \
\ ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
-\ guar (INT i: I. lift_prog i `` Y)";
+\ guarantees (INT i: I. lift_prog i `` Y)";
by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
bind_thm ("guarantees_PLam_INT", ballI RS result());
Goalw [PLam_def]
- "[| ALL i:I. F i : X guar Y |] \
+ "[| ALL i:I. F i : X guarantees Y |] \
\ ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
-\ guar (UN i: I. lift_prog i `` Y)";
+\ guarantees (UN i: I. lift_prog i `` Y)";
by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
bind_thm ("guarantees_PLam_UN", ballI RS result());