--- a/src/HOL/UNITY/Alloc.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML Wed Dec 08 13:53:29 1999 +0100
@@ -123,19 +123,20 @@
rewrite_rule [client_spec_def, client_increasing_def,
client_bounded_def, client_progress_def] Client;
-Goal "Client : UNIV guarantees Increasing ask";
+Goal "Client : UNIV guarantees[funPair rel ask] Increasing ask";
by (cut_facts_tac [Client_Spec] 1);
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
qed "Client_Increasing_ask";
-Goal "Client : UNIV guarantees Increasing rel";
+Goal "Client : UNIV guarantees[funPair rel ask] Increasing rel";
by (cut_facts_tac [Client_Spec] 1);
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
qed "Client_Increasing_rel";
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
-Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
+Goal "Client : UNIV guarantees[ask] \
+\ Always {s. ALL elt : set (ask s). elt <= NbT}";
by (cut_facts_tac [Client_Spec] 1);
by Auto_tac;
qed "Client_Bounded";
@@ -161,7 +162,8 @@
rewrite_rule [alloc_spec_def, alloc_increasing_def,
alloc_safety_def, alloc_progress_def] Alloc;
-Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
+Goal "i < Nclients \
+\ ==> Alloc : UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
by (cut_facts_tac [Alloc_Spec] 1);
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
qed "Alloc_Increasing";
@@ -192,7 +194,8 @@
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
Goal "i < Nclients \
-\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
+\ ==> extend sysOfAlloc Alloc : \
+\ UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
by (auto_tac (claset(), simpset() addsimps [o_def]));
qed "extend_Alloc_Increasing_allocGiv";
@@ -324,7 +327,6 @@
(** Lemmas about localTo **)
Goal "extend sysOfAlloc F : client localTo[C] extend sysOfClient G";
-by (rtac localTo_UNIV_imp_localTo 1);
by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def,
stable_def, constrains_def,
image_eq_UN, extend_act_def,
@@ -332,12 +334,11 @@
by (Force_tac 1);
qed "sysOfAlloc_in_client_localTo_xl_Client";
-Goal "extend sysOfClient (plam i:I. F) : \
+??Goal "extend sysOfClient (plam i:I. F) : \
\ (sub i o client) localTo[C] extend sysOfClient (lift_prog i F)";
-by (rtac localTo_UNIV_imp_localTo 1);
by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN
(2, extend_localTo_extend_I))) 1);
-by (rtac PLam_sub_localTo 1);
+by (rtac ??PLam_sub_localTo 1);
qed "sysOfClient_in_client_localTo_xl_Client";
@@ -398,7 +399,7 @@
(*Lemma (?). A LOT of work just to lift "Client_Progress" to the array*)
Goal "lift_prog i Client \
\ : Increasing (giv o sub i) Int \
-\ ((funPair rel ask o sub i) LocalTo (lift_prog i Client)) \
+\ ((funPair rel ask o sub i) localTo (lift_prog i Client)) \
\ guarantees \
\ (INT h. {s. h <= (giv o sub i) s & \
\ h pfixGe (ask o sub i) s} \
@@ -421,7 +422,7 @@
"(plam x:lessThan Nclients. Client) \
\ : (INT i : lessThan Nclients. \
\ Increasing (giv o sub i) Int \
-\ ((funPair rel ask o sub i) LocalTo (lift_prog i Client))) \
+\ ((funPair rel ask o sub i) localTo (lift_prog i Client))) \
\ guarantees \
\ (INT i : lessThan Nclients. \
\ INT h. {s. h <= (giv o sub i) s & \
@@ -432,23 +433,39 @@
by (rtac Client_i_Progress 1);
qed "PLam_Client_Progress";
+(*because it IS NOT CLEAR that localTo is good for anything: no laws*)
+Goal "(plam x:lessThan Nclients. Client) \
+\ : (INT i : lessThan Nclients. \
+\ Increasing (giv o sub i) Int \
+\ ((funPair rel ask o sub i) localTo[UNIV] (lift_prog i Client))) \
+\ guarantees \
+\ (INT i : lessThan Nclients. \
+\ 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 (blast_tac (claset() addIs [PLam_Client_Progress RS guarantees_weaken,
+ localTo_imp_localTo]) 1);
+qed "PLam_Client_Progress_localTo";
+
(*progress (2), step 7*)
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
[| ALL i:lessThan Nclients.
- G : (sub i o client) LocalTo
+ G : (sub i o client) localTo
extend sysOfClient (lift_prog i Client) |]
- ==> G : client LocalTo
+ ==> G : client localTo
extend sysOfClient (plam i:lessThan Nclients. Client)
[| ALL i: I.
- G : (sub i o client) LocalTo
+ G : (sub i o client) localTo
extend sysOfClient (lift_prog i Client) |]
- ==> G : client LocalTo
+ ==> G : client localTo
extend sysOfClient (plam x: I. Client)
@@ -463,16 +480,31 @@
- G : (sub i o client) LocalTo extend sysOfClient (plam x: I. Client)
+ G : (sub i o client) localTo extend sysOfClient (plam x: I. Client)
xxxxxxxxxxxxxxxx;
-THIS PROOF requires an extra locality specification for Network:
- Network : rel o sub i o client localTo[C]
- extend sysOfClient (lift_prog i Client)
-and similarly for ask o sub i o client.
+NEW AXIOM NEEDED??
+i < Nclients
+ ==> System
+ : (funPair rel ask o sub i o client) localTo
+ extend sysOfClient (lift_prog i Client)
+
+Goal "[| G : v localTo[C] (lift_prog i (F i)); i: I |] \
+\ ==> G : v localTo[C] (PLam I F)";
+by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains],
+ simpset()));
+qed "localTo_component";
+
+Goalw [LOCALTO_def, localTo_def, stable_def]
+ "[| G : v localTo (lift_prog i (F i)); i: I |] \
+\ ==> G : v localTo (PLam I F)";
+by (subgoal_tac "reachable ((PLam I F) Join G) <= reachable ((lift_prog i (F i)) Join G)" 1);
+by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains],
+ simpset()));
+qed "localTo_component";
Goalw [System_def]
@@ -483,31 +515,41 @@
\ {s. tokens h <= (tokens o rel o sub i o client) s})";
by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
by (rtac (PLam_Client_Progress RS project_guarantees) 1);
-br extending_INT 2;
+by (rtac extending_INT 2);
by (rtac (client_export extending_LeadsETo RS extending_weaken RS extending_INT) 2);
by (rtac subset_refl 4);
by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+
+by (rtac projecting_INT 1);
+by (rtac projecting_Int 1);
+by (rtac (client_export projecting_Increasing) 1);
+
by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
client_export projecting_Increasing,
component_PLam,
- client_export projecting_LocalTo]) 1);
-auto();
+ client_export projecting_localTo]) 1);
+by Auto_tac;
+by (fold_tac [System_def]);
+by (etac System_Increasing_giv 2);
+
-be INT_lower 2;
+by (rtac localTo_component 1);
-br projecting_INT 1;
-br projecting_Int 1;
+by (etac INT_lower 2);
+
+by (rtac projecting_INT 1);
+by (rtac projecting_Int 1);
(*The next step goes wrong: it makes an impossible localTo subgoal*)
(*blast_tac doesn't use HO unification*)
by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
client_export projecting_Increasing,
component_PLam,
- client_export projecting_LocalTo]) 1);
+ client_export projecting_localTo]) 1);
by (Clarify_tac 2);
by (asm_simp_tac
(simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
- LocalTo_def, Join_localTo,
+ localTo_def, Join_localTo,
sysOfClient_in_client_localTo_xl_Client,
sysOfAlloc_in_client_localTo_xl_Client
RS localTo_imp_o_localTo,
@@ -516,6 +558,7 @@
+
OLD PROOF;
by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
by (rtac (guarantees_PLam_I RS project_guarantees) 1);
@@ -529,10 +572,10 @@
by (fast_tac (claset() addIs [projecting_Int,
client_export projecting_Increasing,
component_PLam,
- client_export projecting_LocalTo]) 1);
+ client_export projecting_localTo]) 1);
by (asm_simp_tac
(simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
- LocalTo_def, Join_localTo,
+ localTo_def, Join_localTo,
sysOfClient_in_client_localTo_xl_Client,
sysOfAlloc_in_client_localTo_xl_Client]) 2);
by Auto_tac;
--- a/src/HOL/UNITY/Alloc.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy Wed Dec 08 13:53:29 1999 +0100
@@ -32,15 +32,17 @@
Nclients :: nat (*Number of clients*)
+(** State definitions. OUTPUT variables are locals **)
+
record clientState =
giv :: nat list (*client's INPUT history: tokens GRANTED*)
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
record allocState =
- allocGiv :: nat => nat list (*allocator's local copy of "giv" for i*)
- allocAsk :: nat => nat list (*allocator's local copy of "ask" for i*)
- allocRel :: nat => nat list (*allocator's local copy of "rel" for i*)
+ allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*)
+ allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*)
+ allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*)
record systemState = allocState +
client :: nat => clientState (*states of all clients*)
@@ -68,21 +70,23 @@
(** Client specification (required) ***)
- (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
+ (*spec (3)*)
client_increasing :: clientState program set
"client_increasing ==
- UNIV guarantees Increasing ask Int Increasing rel"
+ UNIV guarantees[funPair rel ask]
+ Increasing ask Int Increasing rel"
(*spec (4)*)
client_bounded :: clientState program set
"client_bounded ==
- UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
+ UNIV guarantees[ask]
+ Always {s. ALL elt : set (ask s). elt <= NbT}"
(*spec (5)*)
client_progress :: clientState program set
"client_progress ==
Increasing giv
- guarantees
+ 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})"
@@ -92,18 +96,18 @@
(** Allocator specification (required) ***)
- (*spec (6) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
+ (*spec (6)*)
alloc_increasing :: allocState program set
"alloc_increasing ==
UNIV
- guarantees
+ guarantees[allocGiv]
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
alloc_safety :: allocState program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
- guarantees
+ 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}"
@@ -120,7 +124,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})
- guarantees
+ guarantees[allocGiv]
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
@@ -134,21 +138,21 @@
network_ask :: systemState program set
"network_ask == INT i : lessThan Nclients.
Increasing (ask o sub i o client)
- guarantees
+ guarantees[allocAsk]
((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)
- guarantees
+ guarantees[giv o sub i o client]
((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)
- guarantees
+ guarantees[allocRel]
((sub i o allocRel) Fols (rel o sub i o client))"
network_spec :: systemState program set
--- a/src/HOL/UNITY/Client.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Client.ML Wed Dec 08 13:53:29 1999 +0100
@@ -73,13 +73,11 @@
program_defs_ref := [];
(*Safety property 2: clients return the right number of tokens*)
-Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg)) \
-\ guarantees Always {s. rel s <= giv s}";
+Goal "Cli_prg : Increasing giv guarantees[rel] Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
by (rtac AlwaysI 1);
by (Force_tac 1);
-by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
-by (blast_tac (claset() addIs [Increasing_localTo_Stable,
+by (blast_tac (claset() addIs [Increasing_preserves_Stable,
stable_rel_le_giv]) 1);
qed "ok_guar_rel_prefix_giv";
@@ -101,30 +99,29 @@
val Increasing_length = mono_length RS mono_Increasing_o;
Goal "Cli_prg : \
-\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \
-\ guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
-\ {s. size (rel s) <= size (giv s)})";
+\ Increasing giv guarantees[funPair rel ask] \
+\ 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);
by (dtac (impOfSubs (rewrite_o Increasing_length)) 1);
by (rtac AlwaysI 1);
by (Force_tac 1);
by (rtac Stable_Int 1);
-by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
-by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
- addIs [Increasing_localTo_Stable,
+by (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
+ addIs [Increasing_preserves_Stable,
stable_size_rel_le_giv]) 2);
-by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
-by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
- addIs [stable_localTo_stable2 RS stable_imp_Stable,
- stable_size_ask_le_rel]) 1);
+by (res_inst_tac [("v1", "ask"), ("w1", "rel")]
+ (stable_localTo_stable2 RS stable_imp_Stable) 1);
+by (ALLGOALS
+ (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
+ addIs [stable_size_ask_le_rel])));
val lemma1 = result();
Goal "Cli_prg : \
-\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \
-\ Int Always giv_meets_ask) \
-\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
+\ Increasing giv Int Always giv_meets_ask \
+\ guarantees[funPair rel ask] \
+\ ({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);
@@ -133,7 +130,7 @@
impOfSubs Increasing_Stable_less],
simpset()) 1);
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
-by (Blast_tac 1);
+by Auto_tac;
by (force_tac (claset(),
simpset() addsimps [Always_eq_includes_reachable,
giv_meets_ask_def]) 1);
--- a/src/HOL/UNITY/Comp.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Comp.ML Wed Dec 08 13:53:29 1999 +0100
@@ -74,11 +74,6 @@
by (blast_tac (claset() addSIs [program_equalityI]) 1);
qed "component_antisym";
-Goalw [component_def]
- "F <= H = (EX G. F Join G = H & Disjoint UNIV F G)";
-by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
-qed "component_eq";
-
Goal "((F Join G) <= H) = (F <= H & G <= H)";
by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (Blast_tac 1);
@@ -92,16 +87,86 @@
(*Used in Guar.thy to show that programs are partially ordered*)
bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
-Goal "F' <= F ==> Diff C G (Acts F) <= Diff C G (Acts F')";
-by (auto_tac (claset(), simpset() addsimps [Diff_def, component_eq_subset]));
-qed "Diff_anti_mono";
+
+(*** preserves ***)
+
+Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
+by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
+by (Blast_tac 1);
+qed "Join_preserves";
+
+Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
+by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1);
+by (Blast_tac 1);
+qed "JN_preserves";
+
+Goal "preserves (funPair v w) = preserves v Int preserves w";
+by (auto_tac (claset(),
+ simpset() addsimps [funPair_def, preserves_def,
+ stable_def, constrains_def]));
+by (Blast_tac 1);
+qed "preserves_funPair";
+
+(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
+AddIffs [preserves_funPair RS eqset_imp_iff];
+
+
+Goal "(funPair f g) o h = funPair (f o h) (g o h)";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "funPair_o_distrib";
+
+Goal "preserves v <= preserves (w o v)";
+by (force_tac (claset(),
+ simpset() addsimps [preserves_def,
+ stable_def, constrains_def]) 1);
+qed "subset_preserves_o";
-(*The LocalTo analogue fails unless
- reachable (F Join G) <= reachable (F' Join G),
- e.g. if the initial condition of F is stronger than that of F'*)
-Goalw [LOCALTO_def, stable_def]
- "[| G : v localTo[C] F'; F' <= F |] ==> G : v localTo[C] F";
-by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains],
- simpset()));
-qed "localTo_component";
+Goal "preserves v <= stable {s. P (v s)}";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def,
+ stable_def, constrains_def]));
+by (rename_tac "s' s" 1);
+by (subgoal_tac "v s = v s'" 1);
+by (ALLGOALS Force_tac);
+qed "preserves_subset_stable";
+
+Goal "preserves id <= stable A";
+by (force_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
+qed "preserves_id_subset_stable";
+
+
+(** Some lemmas used only in Client.ML **)
+Goal "[| F : stable {s. P (v s) (w s)}; \
+\ G : preserves v; G : preserves w |] \
+\ ==> F Join G : stable {s. P (v s) (w s)}";
+by (asm_simp_tac (simpset() addsimps [Join_stable]) 1);
+by (subgoal_tac "G: preserves (funPair v w)" 1);
+by (Asm_simp_tac 2);
+by (dres_inst_tac [("P1", "split ?Q")]
+ (impOfSubs preserves_subset_stable) 1);
+by (auto_tac (claset(), simpset() addsimps [funPair_def]));
+qed "stable_localTo_stable2";
+
+Goal "[| F : stable {s. v s <= w s}; G : preserves v; \
+\ F Join G : Increasing w |] \
+\ ==> F Join G : Stable {s. v s <= w s}";
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def, Stable_def, Increasing_def,
+ Constrains_def, Join_constrains, all_conj_distrib]));
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+(*The G case remains*)
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
+by (case_tac "act: Acts F" 1);
+by (Blast_tac 1);
+(*We have a G-action, so delete assumptions about F-actions*)
+by (thin_tac "ALL act:Acts F. ?P act" 1);
+by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
+by (subgoal_tac "v x = v xa" 1);
+by (Blast_tac 2);
+by Auto_tac;
+by (etac order_trans 1);
+by (Blast_tac 1);
+qed "Increasing_preserves_Stable";
--- a/src/HOL/UNITY/Comp.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Comp.thy Wed Dec 08 13:53:29 1999 +0100
@@ -19,4 +19,11 @@
strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)"
+constdefs
+ preserves :: "('a=>'b) => 'a program set"
+ "preserves v == INT z. stable {s. v s = z}"
+
+ funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
+ "funPair f g == %x. (f x, g x)"
+
end
--- a/src/HOL/UNITY/ELT.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/ELT.ML Wed Dec 08 13:53:29 1999 +0100
@@ -6,6 +6,11 @@
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);
@@ -51,9 +56,12 @@
givenBy_imp_eq_Collect]) 1);
qed "givenBy_eq_eq_Collect";
-Goal "(funPair f g) o h = funPair (f o h) (g o h)";
-by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
-qed "funPair_o_distrib";
+(*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";
(** Standard leadsTo rules **)
@@ -301,7 +309,7 @@
(*** Special properties involving the parameter [CC] ***)
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
-Goal "[| F: (A leadsTo[givenBy v] B); F Join G : v localTo[C] F; \
+Goal "[| F: (A leadsTo[givenBy v] B); G : preserves v; \
\ F Join G : stable C |] \
\ ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
by (etac leadsETo_induct 1);
@@ -311,30 +319,17 @@
leadsETo_Trans]) 2);
by (rtac leadsETo_Basis 1);
by (auto_tac (claset(),
- simpset() addsimps [Int_Diff, ensures_def, stable_def,
- givenBy_eq_Collect,
- Join_localTo,
+ simpset() addsimps [Int_Diff, ensures_def,
+ givenBy_eq_Collect, Join_stable,
Join_constrains, Join_transient]));
by (blast_tac (claset() addIs [transient_strengthen]) 3);
-by (blast_tac (claset() addDs [constrains_localTo_constrains]
+by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
+by (rewtac stable_def);
+by (blast_tac (claset() addSEs [equalityE]
addIs [constrains_Int RS constrains_weaken]) 2);
-by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
-qed "gen_leadsETo_localTo_imp_Join_leadsETo";
-
-(*USED???
- Could replace this proof by instantiation of the one above with C=UNIV*)
-Goal "[| F: (A leadsTo[givenBy v] B); F Join G : v localTo[UNIV] F |] \
-\ ==> F Join G : (A leadsTo[givenBy v] B)";
-by (etac leadsETo_induct 1);
-by (blast_tac (claset() addIs [leadsETo_Union]) 3);
-by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
-by (rtac leadsETo_Basis 1);
-by (auto_tac (claset(),
- simpset() addsimps [ensures_def, givenBy_eq_Collect,
- Join_localTo,
- Join_constrains, Join_transient]));
-by (force_tac (claset() addDs [constrains_localTo_constrains], simpset()) 1);
-qed "leadsETo_localTo_imp_Join_leadsETo";
+by (blast_tac (claset() addSEs [equalityE]
+ addIs [constrains_Int RS constrains_weaken]) 1);
+qed "gen_leadsETo_imp_Join_leadsETo";
(*useful??*)
Goal "[| F Join G : (A leadsTo[CC] B); ALL C:CC. G : stable C |] \
@@ -382,85 +377,54 @@
extend_set_Diff_distrib RS sym]) 1);
qed "leadsETo_imp_extend_leadsETo";
-(*NOW OBSOLETE: SEE BELOW !! Generalizes the version proved in Project.ML*)
-Goalw [LOCALTO_def, transient_def, Diff_def]
- "[| G : (v o f) localTo[C] extend h F; project h C G : transient D; \
-\ D : givenBy v |] \
-\ ==> F : transient D";
-by (auto_tac (claset(),
- simpset() addsimps [givenBy_eq_Collect]));
-by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
-by Auto_tac;
-by (rtac bexI 1);
-by (assume_tac 2);
-by (Blast_tac 1);
-by (case_tac "{s. P (v s)} = {}" 1);
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, constrains_def]));
-by (subgoal_tac
- "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
-by (blast_tac (claset() addSDs [bspec]) 2);
-by (thin_tac "ALL z. ?P z" 1);
-by (subgoal_tac "project_act h (Restrict C act) ^^ {s. P (v s)} <= {s. P (v s)}" 1);
-by (Clarify_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
-by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
-by (blast_tac (claset() addSDs [subsetD]) 1);
-qed "localTo_project_transient_transient";
-
-
+(*NEEDED?? THEN 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() addIs [project_set_I],
simpset()));
qed "Int_extend_set_lemma";
+(*NEEDED?? THEN 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, project_set_def]) 1);
by (Blast_tac 1);
qed "project_constrains_project_set";
+(*NEEDED?? THEN 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";
-(*!! Generalizes the version proved in Project.ML*)
-Goalw [LOCALTO_def, transient_def, Diff_def]
- "[| G : (v o f) localTo[C] extend h F; \
-\ project h C G : transient (C' Int D); \
-\ project h C G : stable C'; \
-\ D : givenBy v; (C' Int D) <= D |] \
-\ ==> F : transient (C' Int D)";
-by (auto_tac (claset(),
- simpset() addsimps [givenBy_eq_Collect]));
-by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
-by Auto_tac;
-by (rtac bexI 1);
+
+
+(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
+Goal "[| G : preserves (v o f); project h C G : transient D; \
+\ D : givenBy v |] ==> D={}";
+by (rtac stable_transient_empty 1);
by (assume_tac 2);
-by (Blast_tac 1);
-by (case_tac "(C' Int {s. P (v s)}) = {}" 1);
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, constrains_def]));
-by (subgoal_tac
- "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
-by (blast_tac (claset() addSDs [bspec]) 2);
-by (thin_tac "ALL z. ?P z" 1);
-by (subgoal_tac "project_act h (Restrict C act) ^^ (C' Int {s. P (v s)}) <= (C' Int {s. P (v s)})" 1);
-by (Clarify_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
-by (thin_tac "(C' Int {s. P (v s)}) <= Domain ?A" 2);
-by (thin_tac "?A <= -C' Un ?B" 2);
-by (rtac conjI 2);
-by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 3);
-by (Blast_tac 2);
-by (blast_tac (claset() addSDs [subsetD]) 1);
-qed "localTo_project_transient_transient";
+(*If addIs then PROOF FAILED at depth 2*)
+by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable,
+ 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*)
-Goal "[| project h C G : transient (project_set h C Int (A-B)) --> \
-\ F : transient (project_set h C Int (A-B)); \
+Goal "[| project h C G ~: transient (project_set h C Int (A-B)) | \
+\ project_set h C Int (A - B) = {}; \
\ extend h F Join G : stable C; \
\ F Join project h C G : (project_set h C Int A) ensures B |] \
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
@@ -470,8 +434,8 @@
qed "Join_project_ensures_strong";
Goal "[| extend h F Join G : stable C; \
-\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
-\ G : (v o f) localTo[C] extend h F |] \
+\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\ G : preserves (v o f) |] \
\ ==> extend h F Join G : \
\ (C Int extend_set h (project_set h C Int A)) \
\ leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
@@ -486,8 +450,8 @@
by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma,
extend_set_Diff_distrib RS sym]) 2);
by (rtac Join_project_ensures_strong 1);
-by (auto_tac (claset() addIs [localTo_project_transient_transient,
- project_stable_project_set],
+by (auto_tac (claset() addDs [preserves_o_project_transient_empty]
+ addIs [project_stable_project_set],
simpset() addsimps [Int_left_absorb, Join_stable]));
by (asm_simp_tac
(simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
@@ -496,33 +460,36 @@
val lemma = result();
Goal "[| extend h F Join G : stable C; \
-\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
-\ G : (v o f) localTo[C] extend h F |] \
+\ F Join project h C G : \
+\ (project_set h C Int A) \
+\ leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\ G : preserves (v o f) |] \
\ ==> extend h F Join G : (C Int extend_set h A) \
\ leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
by (rtac (lemma RS leadsETo_weaken) 1);
by (auto_tac (claset() addIs [project_set_I], simpset()));
qed "project_leadsETo_lemma";
-Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B; \
-\ G : (v o f) localTo[UNIV] extend h F |] \
+Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B; \
+\ G : preserves (v o f) |] \
\ ==> extend h F Join G : (extend_set h A) \
\ leadsTo[givenBy (v o f)] (extend_set h B)";
by (rtac (make_elim project_leadsETo_lemma) 1);
+by (stac stable_UNIV 1);
by Auto_tac;
by (etac leadsETo_givenBy 1);
by (rtac extend_set_givenBy_subset 1);
qed "project_leadsETo_D";
Goal "[| F Join project h (reachable (extend h F Join G)) G \
-\ : A LeadsTo[givenBy v] B; \
-\ G : (v o f) LocalTo extend h F |] \
+\ : A LeadsTo[givenBy v] B; \
+\ G : preserves (v o f) |] \
\ ==> extend h F Join G : \
\ (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
by (rtac (make_elim (subset_refl RS stable_reachable RS
project_leadsETo_lemma)) 1);
by (auto_tac (claset(),
- simpset() addsimps [LeadsETo_def, LocalTo_def]));
+ simpset() addsimps [LeadsETo_def]));
by (asm_full_simp_tac
(simpset() addsimps [project_set_reachable_extend_eq RS sym]) 1);
by (etac (impOfSubs leadsETo_mono) 1);
@@ -530,24 +497,18 @@
qed "project_LeadsETo_D";
Goalw [extending_def]
- "extending (%G. UNIV) h F \
-\ ((v o f) localTo[UNIV] extend h F) \
+ "extending (v o f) (%G. UNIV) h F \
\ (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
\ (A leadsTo[givenBy v] B)";
-by (auto_tac (claset(),
- simpset() addsimps [project_leadsETo_D, Join_localTo]));
+by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
qed "extending_leadsETo";
Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F \
-\ ((v o f) LocalTo extend h F) \
+ "extending (v o f) (%G. reachable (extend h F Join G)) h F \
\ (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
\ (A LeadsTo[givenBy v] B)";
-
-by (force_tac (claset() addIs [project_LeadsETo_D],
- simpset()addsimps [LocalTo_def, Join_assoc RS sym,
- Join_localTo]) 1);
+by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
qed "extending_LeadsETo";
--- a/src/HOL/UNITY/ELT.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/ELT.thy Wed Dec 08 13:53:29 1999 +0100
@@ -32,9 +32,6 @@
givenBy :: "['a => 'b] => 'a set set"
"givenBy f == range (%B. f-`` B)"
- funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
- "funPair f g == %x. (f x, g x)"
-
(*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 Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML Wed Dec 08 13:53:29 1999 +0100
@@ -159,7 +159,7 @@
(*** More laws ***)
(*Because A and B could differ on the "other" part of the state,
- cannot generalize result to
+ cannot generalize to
project_set h (A Int B) = project_set h A Int project_set h B
*)
Goalw [project_set_def]
@@ -167,6 +167,11 @@
by Auto_tac;
qed "project_set_extend_set_Int";
+Goalw [project_set_def]
+ "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
+by Auto_tac;
+qed "project_set_Int_subset";
+
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B";
by Auto_tac;
qed "extend_set_Un_distrib";
@@ -207,6 +212,11 @@
qed "extend_act_D";
Goalw [extend_act_def, project_act_def, project_set_def]
+ "project_act h (extend_act h act) = act";
+by (Blast_tac 1);
+qed "project_act_extend_act";
+
+Goalw [extend_act_def, project_act_def, project_set_def]
"project_act h (Restrict C (extend_act h act)) = \
\ Restrict (project_set h C) act";
by (Blast_tac 1);
@@ -405,97 +415,6 @@
qed "extend_stable_project_set";
-(*** Diff, needed for localTo ***)
-
-Goal "Restrict (extend_set h C) (extend_act h act) = \
-\ extend_act h (Restrict C act)";
-by (auto_tac (claset(),
- simpset() addsimps [split_extended_all]));
-by (auto_tac (claset(),
- simpset() addsimps [extend_act_def]));
-qed "Restrict_extend_set";
-
-Goalw [Diff_def]
- "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
-\ extend h (Diff C G acts)";
-by (rtac program_equalityI 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
-by (simp_tac (simpset() addsimps [image_eq_UN,
- Restrict_extend_set]) 1);
-qed "Diff_extend_eq";
-
-(*Opposite inclusion fails; this inclusion's more general than that of
- Diff_extend_eq*)
-Goal "Diff (project_set h C) G acts \
-\ <= project h C (Diff C (extend h G) (extend_act h `` acts))";
-by (simp_tac
- (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
- image_image, image_Diff_image_eq,
- Restrict_extend_act_eq_Restrict_project_act,
- vimage_image_eq]) 1);
-by (blast_tac (claset() addSEs [equalityE])1);
-qed "Diff_project_set_component";
-
-Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
-\ : (extend_set h A) co (extend_set h B)) \
-\ = (Diff C G acts : A co B)";
-by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
-qed "Diff_extend_constrains";
-
-Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
-\ : stable (extend_set h A)) \
-\ = (Diff C G acts : stable A)";
-by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
-qed "Diff_extend_stable";
-
-(*UNUSED!!*)
-Goal "Diff (extend_set h C) (extend h G) (extend_act h `` acts) : A co B \
-\ ==> Diff C G acts : (project_set h A) co (project_set h B)";
-by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq,
- extend_constrains_project_set]) 1);
-qed "Diff_extend_constrains_project_set";
-
-Goalw [LOCALTO_def]
- "(extend h F : (v o f) localTo[extend_set h C] extend h H) = \
-\ (F : v localTo[C] H)";
-by (Simp_tac 1);
-(*A trick to strip both quantifiers*)
-by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
-by (stac Collect_eq_extend_set 1);
-by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
-qed "extend_localTo_extend_eq";
-
-Goal "[| F : v localTo[C] H; C' <= extend_set h C |] \
-\ ==> extend h F : (v o f) localTo[C'] extend h H";
-by (blast_tac (claset() addDs [extend_localTo_extend_eq RS iffD2,
- impOfSubs localTo_anti_mono]) 1);
-qed "extend_localTo_extend_I";
-
-(*USED?? opposite inclusion fails*)
-Goal "Restrict C (extend_act h act) <= \
-\ extend_act h (Restrict (project_set h C) act)";
-by (auto_tac (claset(),
- simpset() addsimps [split_extended_all]));
-by (auto_tac (claset(),
- simpset() addsimps [extend_act_def, project_set_def]));
-qed "Restrict_extend_set_subset";
-
-
-Goal "(extend_act h `` Acts F) - {Id} = extend_act h `` (Acts F - {Id})";
-by (stac (extend_act_Id RS sym) 1);
-by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
-qed "extend_act_image_Id_eq";
-
-Goal "Disjoint C (extend h F) (extend h G) = Disjoint (project_set h C) F G";
-by (simp_tac
- (simpset() addsimps [Disjoint_def, disjoint_iff_not_equal,
- image_Diff_image_eq,
- Restrict_extend_act_eq_Restrict_project_act,
- extend_act_Id_iff, vimage_def]) 1);
-qed "Disjoint_extend_eq";
-Addsimps [Disjoint_extend_eq];
-
(*** Weak safety primitives: Co, Stable ***)
Goal "p : reachable (extend h F) ==> f p : reachable F";
--- a/src/HOL/UNITY/Guar.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Guar.ML Wed Dec 08 13:53:29 1999 +0100
@@ -65,82 +65,79 @@
(*** guarantees ***)
val prems = Goal
- "(!!G. [| F Join G : X; Disjoint UNIV F G |] ==> F Join G : Y) \
-\ ==> F : X guarantees Y";
-by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
+ "(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \
+\ ==> F : X guarantees[v] Y";
+by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
by (blast_tac (claset() addIs prems) 1);
qed "guaranteesI";
Goalw [guar_def, component_def]
- "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y";
+ "[| F : X guarantees[v] Y; G : preserves v; 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 <= H |] ==> H : Y";
+ "[| F : X guarantees[v] Y; H : X; H = F Join G; G : preserves v |] \
+\ ==> H : Y";
by (Blast_tac 1);
qed "component_guaranteesD";
-(*This equation is more intuitive than the official definition*)
-Goal "(F : X guarantees Y) = \
-\ (ALL G. F Join G : X & Disjoint UNIV F G --> F Join G : Y)";
-by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
-by (Blast_tac 1);
-qed "guarantees_eq";
-
Goalw [guar_def]
- "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
+ "[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'";
by (Blast_tac 1);
qed "guarantees_weaken";
Goalw [guar_def]
- "[| F: X guarantees Y; F <= F' |] ==> F': X guarantees Y";
-by (blast_tac (claset() addIs [component_trans]) 1);
-qed "guarantees_weaken_prog";
+ "[| F: X guarantees[v] Y; preserves w <= preserves v |] \
+\ ==> F: X guarantees[w] Y";
+by (Blast_tac 1);
+qed "guarantees_weaken_var";
-Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
+Goalw [guar_def] "X <= Y ==> X guarantees[v] Y = UNIV";
by (Blast_tac 1);
qed "subset_imp_guarantees_UNIV";
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
+Goalw [guar_def] "X <= Y ==> F : X guarantees[v] Y";
by (Blast_tac 1);
qed "subset_imp_guarantees";
-(*Remark at end of section 4.1*)
-Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
+(*Remark at end of section 4.1
+Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] 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 [guar_def]
- "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
+ "(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)";
by (Blast_tac 1);
qed "guarantees_UN_left";
Goalw [guar_def]
- "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
+ "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
by (Blast_tac 1);
qed "guarantees_Un_left";
Goalw [guar_def]
- "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
+ "X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)";
by (Blast_tac 1);
qed "guarantees_INT_right";
Goalw [guar_def]
- "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
+ "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
by (Blast_tac 1);
qed "guarantees_Int_right";
-Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
+Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))";
by (Blast_tac 1);
qed "shunting";
-Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
+Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X";
by (Blast_tac 1);
qed "contrapositive";
@@ -149,78 +146,108 @@
**)
Goalw [guar_def]
- "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
-\ ==> F : (V Int Y) guarantees Z";
+ "[| F : V guarantees[v] X; F : (X Int Y) guarantees[v] Z |]\
+\ ==> F : (V Int Y) guarantees[v] Z";
by (Blast_tac 1);
qed "combining1";
Goalw [guar_def]
- "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\
-\ ==> F : V guarantees (X Un Z)";
+ "[| F : V guarantees[v] (X Un Y); F : Y guarantees[v] Z |]\
+\ ==> F : V guarantees[v] (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 guarantees Y i) *)
+(*Premise should be (!!i. i: I ==> F: X guarantees[v] Y i) *)
Goalw [guar_def]
- "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
+ "ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)";
by (Blast_tac 1);
qed "all_guarantees";
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F: X guarantees[v] Y i; i: I |] *)
Goalw [guar_def]
- "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
+ "EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)";
by (Blast_tac 1);
qed "ex_guarantees";
(*** Additional guarantees laws, by lcp ***)
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);
+ "[| F: U guarantees[v] V; G: X guarantees[v] Y; \
+\ F : preserves v; G : preserves v |] \
+\ ==> F Join G: (U Int X) guarantees[v] (V Int Y)";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
+by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
+by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1);
+by (asm_simp_tac (simpset() addsimps Join_ac) 1);
qed "guarantees_Join_Int";
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);
+ "[| F: U guarantees[v] V; G: X guarantees[v] Y; \
+\ F : preserves v; G : preserves v |] \
+\ ==> F Join G: (U Un X) guarantees[v] (V Un Y)";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
+by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
+by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1);
+by (asm_simp_tac (simpset() addsimps Join_ac) 1);
qed "guarantees_Join_Un";
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());
+ "[| ALL i:I. F i : X i guarantees[v] Y i; \
+\ ALL i:I. F i : preserves v |] \
+\ ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
+by Auto_tac;
+by (ball_tac 1);
+by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb,
+ Join_preserves, JN_preserves]) 1);
+qed "guarantees_JN_INT";
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());
+ "[| ALL i:I. F i : X i guarantees[v] Y i; \
+\ ALL i:I. F i : preserves v |] \
+\ ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)";
+by Auto_tac;
+by (ball_tac 1);
+by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
+by (auto_tac
+ (claset(),
+ simpset() addsimps [Join_assoc RS sym, JN_absorb,
+ Join_preserves, JN_preserves]));
+qed "guarantees_JN_UN";
-(*** guarantees laws for breaking down the program, by lcp ***)
+(*** guarantees[v] laws for breaking down the program, by lcp ***)
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";
+ "[| F: X guarantees[v] Y; G: preserves v |] \
+\ ==> F Join G: X guarantees[v] Y";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
+qed "guarantees_Join_I1";
-bind_thm ("guarantees_Join_I1", disjI1 RS guarantees_Join_I);
-bind_thm ("guarantees_Join_I2", disjI2 RS guarantees_Join_I);
+Goal "[| G: X guarantees[v] Y; F: preserves v |] \
+\ ==> F Join G: X guarantees[v] Y";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
+qed "guarantees_Join_I2";
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);
+ "[| i : I; F i: X guarantees[v] Y; \
+\ ALL j:I. i~=j --> F j : preserves v |] \
+\ ==> (JN i:I. (F i)) : X guarantees[v] Y";
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
+by (auto_tac (claset(),
+ simpset() addsimps [JN_Join_diff, Join_assoc RS sym,
+ Join_preserves, JN_preserves]));
qed "guarantees_JN_I";
--- a/src/HOL/UNITY/Guar.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Guar.thy Wed Dec 08 13:53:29 1999 +0100
@@ -35,9 +35,11 @@
welldef :: 'a program set
"welldef == {F. Init F ~= {}}"
- guar :: ['a program set, 'a program set] => 'a program set
- (infixl "guarantees" 55) (*higher than membership, lower than Co*)
- "X guarantees Y == {F. ALL H. F <= H --> H:X --> H:Y}"
+ guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
+ ("(_/ guarantees[_]/ _)" [55,0,55] 55)
+ (*higher than membership, lower than Co*)
+ "X guarantees[v] Y == {F. ALL G. G : preserves v --> F Join G : X -->
+ F Join G : Y}"
refines :: ['a program, 'a program, 'a program set] => bool
("(3_ refines _ wrt _)" [10,10,10] 10)
--- a/src/HOL/UNITY/Lift_prog.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Wed Dec 08 13:53:29 1999 +0100
@@ -85,6 +85,11 @@
qed "sub_vimage";
Addsimps [sub_vimage];
+(*For tidying the result of "export"*)
+Goal "v o (%z. z i) = v o sub i";
+by (simp_tac (simpset() addsimps [sub_def]) 1);
+qed "fold_o_sub";
+
(*** lift_prog and the lattice operations ***)
@@ -115,7 +120,9 @@
by Auto_tac;
qed "good_map_lift_map";
-fun lift_export th = good_map_lift_map RS export th;
+fun lift_export th =
+ good_map_lift_map RS export th
+ |> simplify (simpset() addsimps [fold_o_sub]);;
Goal "fst (inv (lift_map i) g) = g i";
by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
@@ -293,23 +300,6 @@
qed "drop_prog_stable";
-(*** Diff, needed for localTo ***)
-
-Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
-\ ==> Diff (drop_set i C) (drop_prog i C G) acts : A co B";
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_correct, drop_prog_correct,
- lift_set_correct, lift_act_correct,
- lift_export Diff_project_constrains]) 1);
-qed "Diff_drop_prog_constrains";
-
-Goalw [stable_def]
- "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |] \
-\ ==> Diff (drop_set i C) (drop_prog i C G) acts : stable A";
-by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
-qed "Diff_drop_prog_stable";
-
-
(*** Weak safety primitives: Co, Stable ***)
(** Reachability **)
@@ -391,24 +381,33 @@
(*** guarantees properties ***)
+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);
+qed "drop_prog_preserves_I";
+
(*The raw version*)
val [xguary,drop_prog,lift_prog] =
-Goal "[| F : X guarantees Y; \
-\ !!G. lift_prog i F Join G : X' ==> F Join proj G i G : X; \
-\ !!G. [| F Join proj G i G : Y; lift_prog i F Join G : X' |] \
+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' |] \
\ ==> lift_prog i F Join G : Y' |] \
-\ ==> lift_prog i F : X' guarantees 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);
qed "drop_prog_guarantees_raw";
-Goal "[| F : X guarantees Y; \
-\ projecting C (lift_map i) F X' X; \
-\ extending C (lift_map i) F X' Y' Y |] \
-\ ==> lift_prog i F : X' guarantees Y'";
-by (asm_simp_tac
- (simpset() addsimps [lift_prog_correct, project_guarantees]) 1);
+Goal "[| F : X guarantees[v] Y; \
+\ projecting C (lift_map i) F X' X; \
+\ extending w C (lift_map i) F Y' Y; \
+\ preserves w <= preserves (v o sub i) |] \
+\ ==> 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);
qed "drop_prog_guarantees";
@@ -431,35 +430,21 @@
(*** guarantees corollaries ***)
-Goal "F : UNIV guarantees increasing f \
-\ ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
+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 (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_guar_increasing";
-Goal "F : UNIV guarantees Increasing f \
-\ ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
+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 (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_guar_Increasing";
-Goal "F : (v localTo[UNIV] G) guarantees increasing func \
-\ ==> lift_prog i F : (v o sub i) localTo[UNIV] (lift_prog i G) \
-\ guarantees increasing (func o sub i)";
-by (dtac (lift_export extend_localTo_guar_increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_localTo_guar_increasing";
-
-Goal "[| F : (v LocalTo H) guarantees Increasing func; H <= F |] \
-\ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H) \
-\ guarantees Increasing (func o sub i)";
-by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
-by (auto_tac (claset(),
- simpset() addsimps [lift_prog_correct, o_def]));
-qed "lift_prog_LocalTo_guar_Increasing";
-
-Goal "F : Always A guarantees Always B \
-\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
+Goal "F : Always A guarantees[v] Always B \
+\ ==> lift_prog i F : \
+\ 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);
--- a/src/HOL/UNITY/PPROD.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/PPROD.ML Wed Dec 08 13:53:29 1999 +0100
@@ -126,15 +126,6 @@
qed "const_PLam_invariant";
-(** localTo **)
-
-Goal "(PLam I F) : (sub i) localTo[C] lift_prog i (F i)";
-by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def,
- stable_def, constrains_def]) 1);
-by (Force_tac 1);
-qed "PLam_sub_localTo";
-
-
(** Reachability **)
Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)";
@@ -286,7 +277,8 @@
(*** guarantees properties ***)
Goalw [PLam_def]
- "[| lift_prog i (F i): X guarantees Y; i : I |] \
-\ ==> (PLam I F) : X guarantees Y";
+ "[| lift_prog i (F i): X guarantees[v] Y; i : I; \
+\ ALL j:I. i~=j --> lift_prog j (F j) : preserves v |] \
+\ ==> (PLam I F) : X guarantees[v] Y";
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
qed "guarantees_PLam_I";
--- a/src/HOL/UNITY/Project.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Project.ML Wed Dec 08 13:53:29 1999 +0100
@@ -6,6 +6,8 @@
Projections of state sets (also of actions and programs)
Inheritance of GUARANTEES properties under extension
+
+POSSIBLY CAN DELETE Restrict_image_Diff
*)
Open_locale "Extend";
@@ -157,34 +159,31 @@
qed "projecting_weaken";
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)";
+ "[| extending v C h F YA' YA; extending v C h F YB' YB |] \
+\ ==> extending v C h F (YA' Int YB') (YA Int YB)";
by (Blast_tac 1);
qed "extending_Int";
Goalw [extending_def]
- "[| 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)";
+ "[| extending v C h F YA' YA; extending v C h F YB' YB |] \
+\ ==> extending v C h F (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)";
+ "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
+\ ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)";
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "extending_INT";
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)";
+ "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
+\ ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
qed "extending_UN";
Goalw [extending_def]
- "[| extending C h F X' Y' Y; U'<= X'; Y'<=V'; V<=Y |] \
-\ ==> extending C h F U' V' V";
+ "[| extending v C h F Y' Y; Y'<=V'; V<=Y |] ==> extending v C h F V' V";
by Auto_tac;
qed "extending_weaken";
@@ -207,133 +206,38 @@
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
qed "projecting_increasing";
-Goal "extending C h F X' UNIV Y";
+Goal "extending v C h F UNIV Y";
by (simp_tac (simpset() addsimps [extending_def]) 1);
qed "extending_UNIV";
Goalw [extending_def]
- "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
+ "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
by (blast_tac (claset() addIs [project_constrains_D]) 1);
qed "extending_constrains";
Goalw [stable_def]
- "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
+ "extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
by (rtac extending_constrains 1);
qed "extending_stable";
Goalw [extending_def]
- "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
+ "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
qed "extending_increasing";
-
-(*** Diff, needed for localTo ***)
-
-(*Opposite direction fails because Diff in the extended state may remove
- fewer actions, i.e. those that affect other state variables.*)
-
+(*UNUSED*)
Goalw [project_set_def, project_act_def]
"Restrict (project_set h C) (project_act h (Restrict C act)) = \
\ project_act h (Restrict C act)";
by (Blast_tac 1);
qed "Restrict_project_act";
+(*UNUSED*)
Goalw [project_set_def, project_act_def]
"project_act h (Restrict C Id) = Restrict (project_set h C) Id";
by (Blast_tac 1);
qed "project_act_Restrict_Id";
-Goal
- "Diff(project_set h C)(project h C G)(project_act h `` Restrict C `` acts) \
-\ <= project h C (Diff C G acts)";
-by (simp_tac
- (simpset() addsimps [component_eq_subset, Diff_def,
- project_act_Restrict_Id, Restrict_image_Diff]) 1);
-by (force_tac (claset() delrules [equalityI],
- simpset() addsimps [Restrict_project_act, image_eq_UN]) 1);
-qed "Diff_project_project_component_project_Diff";
-
-Goal "Diff (project_set h C) (project h C G) acts <= \
-\ project h C (Diff C G (extend_act h `` acts))";
-by (rtac component_trans 1);
-by (rtac Diff_project_project_component_project_Diff 2);
-by (simp_tac
- (simpset() addsimps [component_eq_subset, Diff_def,
- Restrict_project_act, project_act_Restrict_Id,
- image_eq_UN, Restrict_image_Diff]) 1);
-qed "Diff_project_component_project_Diff";
-
-Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
-\ ==> Diff (project_set h C) (project h C G) acts : A co B";
-by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
-by (rtac (project_constrains RS iffD2) 1);
-by (ftac constrains_imp_subset 1);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "Diff_project_constrains";
-
-Goalw [stable_def]
- "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
-\ ==> Diff (project_set h C) (project h C G) acts : stable A";
-by (etac Diff_project_constrains 1);
-qed "Diff_project_stable";
-
-(** Some results for Diff, extend and project_set **)
-
-Goal "Diff C (extend h G) (extend_act h `` acts) \
-\ : (extend_set h A) co (extend_set h B) \
-\ ==> Diff (project_set h C) G acts : A co B";
-by (rtac (Diff_project_set_component RS component_constrains) 1);
-by (ftac constrains_imp_subset 1);
-by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "Diff_project_set_constrains_I";
-
-Goalw [stable_def]
- "Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \
-\ ==> Diff (project_set h C) G acts : stable A";
-by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1);
-qed "Diff_project_set_stable_I";
-
-Goalw [LOCALTO_def]
- "extend h F : (v o f) localTo[C] extend h H \
-\ ==> F : v localTo[project_set h C] H";
-by Auto_tac;
-by (rtac Diff_project_set_stable_I 1);
-by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
-qed "localTo_project_set_I";
-
-(*Converse fails: even if the conclusion holds, H could modify (v o f)
- simultaneously with other variables, and this action would not be
- superseded by anything in (extend h G) *)
-Goal "H : (v o f) localTo[C] extend h G \
-\ ==> project h C H : v localTo[project_set h C] G";
-by (asm_full_simp_tac
- (simpset() addsimps [LOCALTO_def,
- project_extend_Join RS sym,
- Diff_project_stable,
- Collect_eq_extend_set RS sym]) 1);
-qed "project_localTo_lemma";
-
-Goal "extend h F Join G : (v o f) localTo[C] extend h H \
-\ ==> F Join project h C G : v localTo[project_set h C] H";
-by (asm_full_simp_tac
- (simpset() addsimps [Join_localTo, localTo_project_set_I,
- project_localTo_lemma]) 1);
-qed "gen_project_localTo_I";
-
-Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
-\ ==> F Join project h UNIV G : v localTo[UNIV] H";
-by (dtac gen_project_localTo_I 1);
-by (Asm_full_simp_tac 1);
-qed "project_localTo_I";
-
-Goalw [projecting_def]
- "projecting (%G. UNIV) h F \
-\ ((v o f) localTo[UNIV] extend h H) (v localTo[UNIV] H)";
-by (blast_tac (claset() addIs [project_localTo_I]) 1);
-qed "projecting_localTo";
-
(** Reachability and project **)
@@ -352,7 +256,8 @@
qed "reachable_imp_reachable_project";
(*The extra generality in the first premise allows guarantees with STRONG
- preconditions (localTo) and WEAK postconditions.*)
+ preconditions (localT) and WEAK postconditions.*)
+(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
Goalw [Constrains_def]
"[| reachable (extend h F Join G) <= C; \
\ F Join project h C G : A Co B |] \
@@ -479,15 +384,6 @@
Collect_eq_extend_set RS sym]) 1);
qed "project_Increasing";
-Goal "[| H <= F; extend h F Join G : (v o f) LocalTo extend h H |] \
-\ ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
-by (asm_full_simp_tac
- (simpset() delsimps [extend_Join]
- addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
- gen_project_localTo_I, extend_Join RS sym,
- Join_assoc RS sym, Join_absorb1]) 1);
-qed "project_LocalTo_I";
-
(** A lot of redundant theorems: all are proved to facilitate reasoning
about guarantees. **)
@@ -515,35 +411,28 @@
by (blast_tac (claset() addIs [project_Increasing_I]) 1);
qed "projecting_Increasing";
-Goalw [projecting_def]
- "H <= F ==> projecting (%G. reachable (extend h F Join G)) h F \
-\ ((v o f) LocalTo extend h H) (v LocalTo H)";
-by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
-qed "projecting_LocalTo";
-
Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F X' \
-\ (extend_set h A Co extend_set h B) (A Co B)";
+ "extending v (%G. reachable (extend h F Join G)) h F \
+\ (extend_set h A Co extend_set h B) (A Co B)";
by (blast_tac (claset() addIs [project_Constrains_D]) 1);
qed "extending_Constrains";
Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F X' \
-\ (Stable (extend_set h A)) (Stable A)";
+ "extending v (%G. reachable (extend h F Join G)) h F \
+\ (Stable (extend_set h A)) (Stable A)";
by (blast_tac (claset() addIs [project_Stable_D]) 1);
qed "extending_Stable";
Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F X' \
-\ (Always (extend_set h A)) (Always A)";
+ "extending v (%G. reachable (extend h F Join G)) h F \
+\ (Always (extend_set h A)) (Always A)";
by (blast_tac (claset() addIs [project_Always_D]) 1);
qed "extending_Always";
val [prem] =
Goalw [extending_def]
"(!!G. reachable (extend h F Join G) <= C G) \
-\ ==> extending C h F X' \
-\ (Increasing (func o f)) (Increasing func)";
+\ ==> extending v C h F (Increasing (func o f)) (Increasing func)";
by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
qed "extending_Increasing";
@@ -585,10 +474,12 @@
by (Blast_tac 1);
qed "ensures_extend_set_imp_project_ensures";
-Goal "[| project h C G : transient (A-B) --> F : transient (A-B); \
+Goal "[| project h C G ~: transient (A-B) | A<=B; \
\ extend h F Join G : stable C; \
\ F Join project h C G : A ensures B |] \
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
+by (etac disjE 1);
+by (blast_tac (claset() addIs [subset_imp_ensures]) 2);
by (auto_tac (claset() addDs [extend_transient RS iffD2]
addIs [transient_strengthen, project_set_I,
project_unless RS unlessD, unlessI,
@@ -601,7 +492,7 @@
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
-Goal "[| ALL D. project h C G : transient D --> F : transient D; \
+Goal "[| ALL D. project h C G : transient D --> D={}; \
\ extend h F Join G : stable C; \
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : \
@@ -614,7 +505,7 @@
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
val lemma = result();
-Goal "[| ALL D. project h C G : transient D --> F : transient D; \
+Goal "[| ALL D. project h C G : transient D --> D={}; \
\ extend h F Join G : stable C; \
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
@@ -623,7 +514,7 @@
qed "project_leadsTo_lemma";
Goal "[| C = (reachable (extend h F Join G)); \
-\ ALL D. project h C G : transient D --> F : transient D; \
+\ ALL D. project h C G : transient D --> D={}; \
\ F Join project h C G : A LeadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (asm_full_simp_tac
@@ -632,30 +523,52 @@
qed "Join_project_LeadsTo";
+
(*** GUARANTEES and EXTEND ***)
+(** 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";
+
(** Strong precondition and postcondition; doesn't seem very useful. **)
-Goal "F : X guarantees Y ==> \
-\ extend h F : (extend h `` X) guarantees (extend h `` Y)";
+Goal "F : X guarantees[v] Y ==> \
+\ extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
-by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS
- extend_Join_eq_extend_D,
+by (blast_tac (claset() addIs [project_preserves_I]
+ addDs [project_set_UNIV RS equalityD2 RS
+ extend_Join_eq_extend_D,
guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
-Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
-\ ==> F : X guarantees Y";
-by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
+Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
+\ ==> F : X guarantees[v] Y";
+by (auto_tac (claset(), simpset() addsimps [guar_def]));
by (dres_inst_tac [("x", "extend h G")] spec 1);
by (asm_full_simp_tac
(simpset() delsimps [extend_Join]
- addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
+ addsimps [extend_Join RS sym, extend_preserves,
+ inj_extend RS inj_image_mem_iff]) 1);
qed "extend_guarantees_imp_guarantees";
-Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
-\ (F : X guarantees Y)";
+Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
+\ (F : X guarantees[v] Y)";
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
extend_guarantees_imp_guarantees]) 1);
qed "extend_guarantees_eq";
@@ -666,151 +579,116 @@
(*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' |] \
+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' |] \
\ ==> extend h F Join G : Y' |] \
-\ ==> extend h F : X' guarantees 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);
qed "project_guarantees_raw";
-Goal "[| F : X guarantees Y; \
-\ projecting C h F X' X; extending C h F X' Y' Y |] \
-\ ==> extend h F : X' guarantees Y'";
+Goal "[| F : X guarantees[v] Y; \
+\ projecting C h F X' X; extending w C h F Y' Y; \
+\ preserves w <= preserves (v o f) |] \
+\ ==> extend h F : X' guarantees[w] Y'";
by (rtac guaranteesI 1);
by (auto_tac (claset(),
- simpset() addsimps [guaranteesD, projecting_def, extending_def]));
+ simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
+ extending_def]));
qed "project_guarantees";
+
(*It seems that neither "guarantees" law can be proved from the other.*)
(*** guarantees corollaries ***)
-(** Most could be deleted: the required versions are easy to prove **)
+(** Some could be deleted: the required versions are easy to prove **)
-Goal "F : UNIV guarantees increasing func \
-\ ==> extend h F : X' guarantees increasing (func o f)";
+Goal "F : UNIV guarantees[v] increasing func \
+\ ==> extend h F : X' guarantees[v o f] increasing (func o f)";
by (etac project_guarantees 1);
by (rtac extending_increasing 2);
by (rtac projecting_UNIV 1);
+by Auto_tac;
qed "extend_guar_increasing";
-Goal "F : UNIV guarantees Increasing func \
-\ ==> extend h F : X' guarantees Increasing (func o f)";
+Goal "F : UNIV guarantees[v] Increasing func \
+\ ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
by (etac project_guarantees 1);
by (rtac extending_Increasing 2);
by (rtac projecting_UNIV 1);
by Auto_tac;
qed "extend_guar_Increasing";
-Goal "F : (v localTo[UNIV] G) guarantees increasing func \
-\ ==> extend h F : (v o f) localTo[UNIV] (extend h G) \
-\ guarantees increasing (func o f)";
-by (etac project_guarantees 1);
-by (rtac extending_increasing 2);
-by (rtac projecting_localTo 1);
-qed "extend_localTo_guar_increasing";
-
-Goal "[| F : (v LocalTo H) guarantees Increasing func; H <= F |] \
-\ ==> extend h F : (v o f) LocalTo (extend h H) \
-\ guarantees Increasing (func o f)";
-by (etac project_guarantees 1);
-by (rtac extending_Increasing 2);
-by (rtac projecting_LocalTo 1);
-by Auto_tac;
-qed "extend_LocalTo_guar_Increasing";
-
-Goal "F : Always A guarantees Always B \
-\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
+Goal "F : Always A guarantees[v] Always B \
+\ ==> extend h F : Always(extend_set h A) guarantees[v o f] \
+\ Always(extend_set h B)";
by (etac project_guarantees 1);
by (rtac extending_Always 2);
by (rtac projecting_Always 1);
+by Auto_tac;
qed "extend_guar_Always";
+Goal "[| G : preserves f; project h C G : transient D |] ==> D={}";
+by (rtac stable_transient_empty 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [project_preserves_id_I,
+ impOfSubs preserves_id_subset_stable]) 1);
+qed "preserves_project_transient_empty";
+
(** Guarantees with a leadsTo postcondition **)
-Goalw [LOCALTO_def, transient_def, Diff_def]
- "[| G : f localTo[C] extend h F; project h C G : transient D |] \
-\ ==> F : transient D";
-by Auto_tac;
-by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
-by Auto_tac;
-by (rtac bexI 1);
-by (assume_tac 2);
-by (Blast_tac 1);
-by (case_tac "D={}" 1);
-by (Blast_tac 1);
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, constrains_def]));
-by (subgoal_tac "ALL z. Restrict C act ^^ {s. f s = z} <= {s. f s = z}" 1);
-by (blast_tac (claset() addSDs [bspec]) 2);
-by (thin_tac "ALL z. ?P z" 1);
-by (subgoal_tac "project_act h (Restrict C act) ^^ D <= D" 1);
-by (Clarify_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
-by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
-by (blast_tac (claset() addSDs [subsetD]) 1);
-qed "localTo_project_transient_transient";
-
Goal "[| F Join project h UNIV G : A leadsTo B; \
-\ G : f localTo[UNIV] extend h F |] \
+\ G : preserves f |] \
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset(),
- simpset() addsimps [localTo_UNIV_imp_localTo RS
- localTo_project_transient_transient]));
+by (auto_tac (claset() addDs [preserves_project_transient_empty],
+ simpset()));
qed "project_leadsTo_D";
Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
-\ G : f LocalTo extend h F |] \
+\ G : preserves f |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (rtac (refl RS Join_project_LeadsTo) 1);
-by (auto_tac (claset(),
- simpset() addsimps [LocalTo_def,
- localTo_project_transient_transient]));
+by (auto_tac (claset() addDs [preserves_project_transient_empty],
+ simpset()));
qed "project_LeadsTo_D";
Goalw [extending_def]
- "extending (%G. UNIV) h F \
-\ (f localTo[UNIV] 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);
+ "extending f (%G. UNIV) h F \
+\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
+by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
qed "extending_leadsTo";
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)";
-by (force_tac (claset() addIs [project_LeadsTo_D],
- simpset()addsimps [LocalTo_def, Join_assoc RS sym,
- Join_localTo]) 1);
+ "extending f (%G. reachable (extend h F Join G)) h F \
+\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
+by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
qed "extending_LeadsTo";
(*STRONG precondition and postcondition*)
-Goal "F : (A co A') guarantees (B leadsTo B') \
-\ ==> extend h F : ((extend_set h A) co (extend_set h A')) \
-\ Int (f localTo[UNIV] (extend h F)) \
-\ guarantees ((extend_set h B) leadsTo (extend_set h B'))";
+Goal "F : (A co A') guarantees[v] (B leadsTo B') \
+\ ==> extend h F : (extend_set h A co extend_set h A') \
+\ guarantees[f] (extend_set h B leadsTo extend_set h B')";
by (etac project_guarantees 1);
-by (rtac (extending_leadsTo RS extending_weaken) 2);
-by (rtac (projecting_constrains RS projecting_weaken) 1);
-by Auto_tac;
+by (rtac subset_preserves_o 3);
+by (rtac extending_leadsTo 2);
+by (rtac projecting_constrains 1);
qed "extend_co_guar_leadsTo";
(*WEAK precondition and postcondition*)
-Goal "F : (A Co A') guarantees (B LeadsTo B') \
-\ ==> extend h F : ((extend_set h A) Co (extend_set h A')) \
-\ Int (f LocalTo (extend h F)) \
-\ guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
+Goal "F : (A Co A') guarantees[v] (B LeadsTo B') \
+\ ==> extend h F : (extend_set h A Co extend_set h A') \
+\ guarantees[f] (extend_set h B LeadsTo extend_set h B')";
by (etac project_guarantees 1);
-by (rtac (extending_LeadsTo RS extending_weaken) 2);
-by (rtac (projecting_Constrains RS projecting_weaken) 1);
-by Auto_tac;
+by (rtac subset_preserves_o 3);
+by (rtac extending_LeadsTo 2);
+by (rtac projecting_Constrains 1);
qed "extend_Co_guar_LeadsTo";
Close_locale "Extend";
--- a/src/HOL/UNITY/Project.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Project.thy Wed Dec 08 13:53:29 1999 +0100
@@ -16,10 +16,10 @@
"projecting C h F X' X ==
ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
- extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
- 'c program set, 'c program set, 'a program set] => bool"
- "extending C h F X' Y' Y ==
- ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
+ extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program,
+ 'c program set, 'a program set] => bool"
+ "extending v C h F Y' Y ==
+ ALL G. G : preserves v --> F Join project h (C G) G : Y
--> extend h F Join G : Y'"
end
--- a/src/HOL/UNITY/Union.ML Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Union.ML Wed Dec 08 13:53:29 1999 +0100
@@ -159,6 +159,12 @@
by Auto_tac;
qed "JN_Join_miniscope";
+(*Used to prove guarantees_JN_I*)
+Goalw [JOIN_def, Join_def] "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "JN_Join_diff";
+
(*** Safety: co, stable, FP ***)
@@ -192,9 +198,9 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "JN_constrains_weaken";
-Goal "i : I ==> \
-\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
-by (asm_simp_tac (simpset() addsimps [stable_def, JN_constrains]) 1);
+Goal "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
+by (asm_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
qed "JN_stable";
Goal "[| ALL i:I. F i : invariant A; i : I |] \
@@ -220,7 +226,7 @@
by (Blast_tac 1);
qed "invariant_JoinI";
-Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
+Goal "FP (JN i:I. F i) = (INT i:I. FP (F i))";
by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1);
qed "FP_JN";
@@ -286,156 +292,3 @@
qed "stable_Join_ensures2";
-(** Diff and localTo **)
-
-Goalw [Diff_def] "F Join (Diff UNIV G (Acts F)) = F Join G";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "Join_Diff2";
-
-Goalw [Diff_def]
- "Diff C (F Join G) (Acts H) = (Diff C F (Acts H)) Join (Diff C G (Acts H))";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "Diff_Join_distrib";
-
-Goalw [Diff_def] "Diff C F (Acts F) = mk_program(Init F, {})";
-by Auto_tac;
-qed "Diff_self_eq";
-
-Goalw [Diff_def, Disjoint_def] "Disjoint C F (Diff C G (Acts F))";
-by (force_tac (claset(),
- simpset() addsimps [Restrict_imageI,
- sym RSN (2,Restrict_imageI)]) 1);
-qed "Diff_Disjoint";
-
-Goalw [Disjoint_def]
- "[| A <= B; Disjoint A F G |] ==> Disjoint B F G";
-by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
-qed "Disjoint_mono";
-
-(*** localTo ***)
-
-Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
- "A <= B ==> v localTo[B] F <= v localTo[A] F";
-by Auto_tac;
-by (dres_inst_tac [("x", "v xc")] spec 1);
-by (dres_inst_tac [("x", "Restrict B xa")] bspec 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
-qed "localTo_anti_mono";
-
-bind_thm ("localTo_UNIV_imp_localTo",
- impOfSubs (subset_UNIV RS localTo_anti_mono));
-
-Goalw [LocalTo_def]
- "G : v localTo[UNIV] F ==> G : v LocalTo F";
-by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
-qed "localTo_imp_LocalTo";
-
-Goalw [LOCALTO_def, stable_def, constrains_def]
- "G : v localTo[C] F ==> G : (f o v) localTo[C] F";
-by (Force_tac 1);
-qed "localTo_imp_o_localTo";
-
-Goal "G : v LocalTo F ==> G : (f o v) LocalTo F";
-by (asm_full_simp_tac
- (simpset() addsimps [LocalTo_def, localTo_imp_o_localTo]) 1);
-qed "LocalTo_imp_o_LocalTo";
-
-(*NOT USED*)
-Goalw [LOCALTO_def, stable_def, constrains_def]
- "(%s. x) localTo[C] F = UNIV";
-by (Blast_tac 1);
-qed "triv_localTo_eq_UNIV";
-
-Goal "(F Join G : v localTo[C] H) = \
-\ (F : v localTo[C] H & G : v localTo[C] H)";
-by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
- stable_def, Join_constrains]) 1);
-by (Blast_tac 1);
-qed "Join_localTo";
-
-Goal "F : v localTo[C] F";
-by (simp_tac
- (simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
- Diff_self_eq]) 1);
-qed "self_localTo";
-
-Goal "(F Join G : v localTo[C] F) = (G : v localTo[C] F)";
-by (simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
-qed "self_Join_localTo";
-
-Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)";
-by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def,
- Join_left_absorb]) 1);
-qed "self_Join_LocalTo";
-
-
-(*** Higher-level rules involving localTo and Join ***)
-
-Goal "[| F : {s. P (v s)} co B; G : v localTo[C] F |] \
-\ ==> G : C Int {s. P (v s)} co B";
-by (ftac constrains_imp_subset 1);
-by (auto_tac (claset(),
- simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
- Diff_def]));
-by (case_tac "Restrict C act: Restrict C `` Acts F" 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-by (subgoal_tac "v x = v xa" 1);
-by (Force_tac 1);
-by (thin_tac "ALL act: ?A. ?P act" 1);
-by (dtac spec 1);
-by (dres_inst_tac [("x", "Restrict C act")] bspec 1);
-by Auto_tac;
-qed "constrains_localTo_constrains";
-
-Goalw [LOCALTO_def, stable_def, constrains_def, Diff_def]
- "[| G : v localTo[C] F; G : w localTo[C] F |] \
-\ ==> G : (%s. (v s, w s)) localTo[C] F";
-by (Blast_tac 1);
-qed "localTo_pairfun";
-
-Goal "[| F : {s. P (v s) (w s)} co B; \
-\ G : v localTo[C] F; \
-\ G : w localTo[C] F |] \
-\ ==> G : C Int {s. P (v s) (w s)} co B";
-by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}")]
- constrains_weaken 1);
-by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
-by Auto_tac;
-qed "constrains_localTo_constrains2";
-
-(*Used just once, in Client.ML. Having F in the conclusion is silly.*)
-Goalw [stable_def]
- "[| F : stable {s. P (v s) (w s)}; \
-\ G : v localTo[UNIV] F; G : w localTo[UNIV] F |] \
-\ ==> F Join G : stable {s. P (v s) (w s)}";
-by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
-by (blast_tac (claset() addIs [constrains_localTo_constrains2 RS
- constrains_weaken]) 1);
-qed "stable_localTo_stable2";
-
-(*Used just in Client.ML. Generalize to arbitrary C?*)
-Goal "[| F : stable {s. v s <= w s}; \
-\ G : v localTo[UNIV] F; \
-\ F Join G : Increasing w |] \
-\ ==> F Join G : Stable {s. v s <= w s}";
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, Stable_def, Increasing_def,
- Constrains_def, Join_constrains, all_conj_distrib]));
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-(*The G case remains; proved like constrains_localTo_constrains*)
-by (auto_tac (claset(),
- simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
- Diff_def]));
-by (case_tac "act: Acts F" 1);
-by (Blast_tac 1);
-by (thin_tac "ALL act:Acts F. ?P act" 1);
-by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
-by (dres_inst_tac [("x", "v xa")] spec 1 THEN dtac bspec 1 THEN rtac DiffI 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (subgoal_tac "v x = v xa" 1);
-by Auto_tac;
-qed "Increasing_localTo_Stable";
--- a/src/HOL/UNITY/Union.thy Wed Dec 08 13:52:36 1999 +0100
+++ b/src/HOL/UNITY/Union.thy Wed Dec 08 13:53:29 1999 +0100
@@ -6,10 +6,6 @@
Unions of programs
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
-
-Do we need a Meet operator? (Aka Intersection)
-
-CAN PROBABLY DELETE the "Disjoint" predicate
*)
Union = SubstAx + FP +
@@ -24,26 +20,6 @@
SKIP :: 'a program
"SKIP == mk_program (UNIV, {})"
- Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
- "Diff C G acts ==
- mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
-
- (*The set of systems that regard "v" as local to F*)
- LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
- ("(_/ localTo[_]/ _)" [80,0,80] 80)
- "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
-
- (*The weak version of localTo, considering only G's reachable states*)
- LocalTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
- "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}"
-
- (*Two programs with disjoint actions, except for identity actions.
- It's a weak property but still useful.*)
- Disjoint :: ['a set, 'a program, 'a program] => bool
- "Disjoint C F G ==
- (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
- <= {}"
-
syntax
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)