added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
--- a/src/HOL/UNITY/Alloc.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Sat Sep 23 16:02:01 2000 +0200
@@ -9,7 +9,8 @@
(*Perhaps equalities.ML shouldn't add this in the first place!*)
Delsimps [image_Collect];
-AddIs [impOfSubs subset_preserves_o];
+AddIs [impOfSubs subset_preserves_o];
+Addsimps [impOfSubs subset_preserves_o];
Addsimps [funPair_o_distrib];
Addsimps [Always_INT_distrib];
Delsimps [o_apply];
@@ -23,7 +24,7 @@
rename_image_Constrains, rename_image_Stable,
rename_image_Increasing, rename_image_Always,
rename_image_leadsTo, rename_image_LeadsTo,
- rename_preserves,
+ rename_preserves, rename_image_preserves, lift_image_preserves,
bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
@@ -31,6 +32,7 @@
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
handle THM _ => (list_of_Int (th RS INT_D))
+ handle THM _ => (list_of_Int (th RS bspec))
handle THM _ => [th];
(*Used just once, for Alloc_Increasing*)
@@ -196,7 +198,32 @@
qed "allocRel_o_sysOfClient_eq";
Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
+Goal "allocGiv o inv sysOfAlloc = allocGiv";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocGiv_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq);
+Goal "allocAsk o inv sysOfAlloc = allocAsk";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocAsk_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq);
+
+Goal "allocRel o inv sysOfAlloc = allocRel";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocRel_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq);
+
+Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \
+\ rel o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
+qed "rel_inv_client_map_drop_map";
+Addsimps (make_o_equivs rel_inv_client_map_drop_map);
+
+Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \
+\ ask o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
+qed "ask_inv_client_map_drop_map";
+Addsimps (make_o_equivs ask_inv_client_map_drop_map);
(**
Open_locale "System";
@@ -206,55 +233,63 @@
val Network = thm "Network";
val System_def = thm "System_def";
-(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
- exporting it from the locale*)
+CANNOT use bind_thm: it puts the theorem into standard form, in effect
+ exporting it from the locale
**)
AddIffs [finite_lessThan];
(*Client : <unfolded specification> *)
-val Client_Spec =
- rewrite_rule [client_spec_def, client_increasing_def,
- client_bounded_def, client_progress_def,
- client_preserves_def] Client;
+val client_spec_simps =
+ [client_spec_def, client_increasing_def, client_bounded_def,
+ client_progress_def, client_allowed_acts_def, client_preserves_def,
+ guarantees_Int_right];
val [Client_Increasing_ask, Client_Increasing_rel,
- Client_Bounded, Client_Progress, Client_preserves_giv,
- Client_preserves_dummy] =
- Client_Spec
- |> simplify (simpset() addsimps [guarantees_Int_right])
- |> list_of_Int;
+ Client_Bounded, Client_Progress, Client_AllowedActs,
+ Client_preserves_giv, Client_preserves_dummy] =
+ Client |> simplify (simpset() addsimps client_spec_simps)
+ |> list_of_Int;
AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
Client_preserves_giv, Client_preserves_dummy];
(*Network : <unfolded specification> *)
-val Network_Spec =
- rewrite_rule [network_spec_def, network_ask_def, network_giv_def,
- network_rel_def, network_preserves_def] Network;
+val network_spec_simps =
+ [network_spec_def, network_ask_def, network_giv_def,
+ network_rel_def, network_allowed_acts_def, network_preserves_def,
+ ball_conj_distrib];
-val [Network_Ask, Network_Giv, Network_Rel,
- Network_preserves_allocGiv, Network_preserves_rel_ask] =
- list_of_Int Network_Spec;
+val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
+ Network_preserves_allocGiv, Network_preserves_rel,
+ Network_preserves_ask] =
+ Network |> simplify (simpset() addsimps network_spec_simps)
+ |> list_of_Int;
AddIffs [Network_preserves_allocGiv];
-Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
+Addsimps [Network_preserves_rel, Network_preserves_ask];
+Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
(*Alloc : <unfolded specification> *)
-val Alloc_Spec =
- rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
- alloc_progress_def, alloc_preserves_def] Alloc;
+val alloc_spec_simps =
+ [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
+ alloc_progress_def, alloc_allowed_acts_def,
+ alloc_preserves_def];
-val [Alloc_Increasing_0, Alloc_Safety,
- Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
+val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
+ Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
+ Alloc_preserves_dummy] =
+ Alloc |> simplify (simpset() addsimps alloc_spec_simps)
+ |> list_of_Int;
(*Strip off the INT in the guarantees postcondition*)
val Alloc_Increasing = normalize Alloc_Increasing_0;
-AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
+AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
+ Alloc_preserves_dummy];
(** Components lemmas [MUST BE AUTOMATED] **)
@@ -283,9 +318,37 @@
(** These preservation laws should be generated automatically **)
-AddIs [impOfSubs subset_preserves_o];
-Addsimps [impOfSubs subset_preserves_o];
+Goal "Allowed Client = preserves rel Int preserves ask";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Client_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Client_Allowed";
+Addsimps [Client_Allowed];
+
+Goal "Allowed Network = \
+\ preserves allocRel Int \
+\ (INT i: lessThan Nclients. preserves(giv o sub i o client))";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Network_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Network_Allowed";
+Addsimps [Network_Allowed];
+Goal "Allowed Alloc = preserves allocGiv";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Alloc_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Alloc_Allowed";
+Addsimps [Alloc_Allowed];
+
+Goal "OK I (%i. lift i (rename client_map Client))";
+by (rtac OK_lift_I 1);
+by Auto_tac;
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));
+qed "OK_lift_rename_Client";
+Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*
(*The proofs of rename_Client_Increasing, rename_Client_Bounded and
rename_Client_Progress are similar. All require copying out the original
@@ -321,23 +384,62 @@
asm_simp_tac
(simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
-
+
(*Lifting Client_Increasing to systemState*)
Goal "i : I \
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
-\ UNIV \
-\ guarantees[(funPair rel ask) o sub i o client] \
-\ Increasing (ask o sub i o client) Int \
-\ Increasing (rel o sub i o client)";
+\ UNIV guarantees \
+\ Increasing (ask o sub i o client) Int \
+\ Increasing (rel o sub i o client)";
by rename_client_map_tac;
qed "rename_Client_Increasing";
+Goal "[| F : preserves w; i ~= j |] \
+\ ==> F : preserves (sub i o fst o lift_map j o funPair v w)";
+by (auto_tac (claset(),
+ simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def]));
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (auto_tac (claset(), simpset() addsimps [o_def]));
+qed "preserves_sub_fst_lift_map";
+
+Goal "[| i < Nclients; j < Nclients |] \
+\ ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)";
+by (case_tac "i=j" 1);
+by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1);
+by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1);
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1);
+qed "client_preserves_giv_oo_client_map";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\ ok Network";
+by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed,
+ client_preserves_giv_oo_client_map]));
+qed "rename_sysOfClient_ok_Network";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\ ok rename sysOfAlloc Alloc";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfClient_ok_Alloc";
+
+Goal "rename sysOfAlloc Alloc ok Network";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfAlloc_ok_Network";
+
+AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc,
+ rename_sysOfAlloc_ok_Network];
+
+(*The "ok" laws, re-oriented*)
+AddIffs [rename_sysOfClient_ok_Network RS ok_sym,
+ rename_sysOfClient_ok_Alloc RS ok_sym,
+ rename_sysOfAlloc_ok_Network RS ok_sym];
+
Goal "i < Nclients \
\ ==> System : Increasing (ask o sub i o client) Int \
\ Increasing (rel o sub i o client)";
by (rtac ([rename_Client_Increasing,
Client_component_System] MRS component_guaranteesD) 1);
-by Auto_tac;
+by Auto_tac;
qed "System_Increasing";
bind_thm ("rename_guarantees_sysOfAlloc_I",
@@ -476,9 +578,8 @@
(*progress (2), step 3: lifting "Client_Bounded" to systemState*)
Goal "i : I \
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
-\ UNIV \
-\ guarantees[ask o sub i o client] \
-\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+\ UNIV guarantees \
+\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
by rename_client_map_tac;
qed "rename_Client_Bounded";
@@ -514,7 +615,7 @@
Goal "i: I \
\ ==> rename sysOfClient (plam x: I. rename client_map Client) \
\ : Increasing (giv o sub i o client) \
-\ guarantees[funPair rel ask o sub i o client] \
+\ guarantees \
\ (INT h. {s. h <= (giv o sub i o client) s & \
\ h pfixGe (ask o sub i o client) s} \
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
@@ -616,3 +717,28 @@
qed "System_correct";
+(** Some lemmas no longer used **)
+
+Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
+\ (funPair giv (funPair ask rel))";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));
+qed "non_dummy_eq_o_funPair";
+
+Goal "(preserves non_dummy) = \
+\ (preserves rel Int preserves ask Int preserves giv)";
+by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1);
+by Auto_tac;
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
+by (auto_tac (claset(), simpset() addsimps [o_def]));
+qed "preserves_non_dummy_eq";
+
+(*Could go to Extend.ML*)
+Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
+by (rtac fst_inv_equalityI 1);
+by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1);
+qed "bij_fst_inv_inv_eq";
--- a/src/HOL/UNITY/Alloc.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Sat Sep 23 16:02:01 2000 +0200
@@ -70,45 +70,47 @@
(*spec (3)*)
client_increasing :: 'a clientState_d program set
"client_increasing ==
- UNIV guarantees[funPair rel ask]
- Increasing ask Int Increasing rel"
+ UNIV guarantees Increasing ask Int Increasing rel"
(*spec (4)*)
client_bounded :: 'a clientState_d program set
"client_bounded ==
- UNIV guarantees[ask]
- Always {s. ALL elt : set (ask s). elt <= NbT}"
+ UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
(*spec (5)*)
client_progress :: 'a clientState_d program set
"client_progress ==
- Increasing giv
- guarantees[funPair rel ask]
+ Increasing giv guarantees
(INT h. {s. h <= giv s & h pfixGe ask s}
LeadsTo {s. tokens h <= (tokens o rel) s})"
(*spec: preserves part*)
- client_preserves :: 'a clientState_d program set
- "client_preserves == preserves (funPair giv clientState_d.dummy)"
+ client_preserves :: 'a clientState_d program set
+ "client_preserves == preserves giv Int preserves clientState_d.dummy"
+
+ (*environmental constraints*)
+ client_allowed_acts :: 'a clientState_d program set
+ "client_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves (funPair rel ask)) Acts)}"
client_spec :: 'a clientState_d program set
"client_spec == client_increasing Int client_bounded Int client_progress
- Int client_preserves"
+ Int client_allowed_acts Int client_preserves"
(** Allocator specification (required) ***)
(*spec (6)*)
alloc_increasing :: 'a allocState_d program set
"alloc_increasing ==
- UNIV
- guarantees[allocGiv]
+ UNIV guarantees
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
alloc_safety :: 'a allocState_d program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
- guarantees[allocGiv]
+ guarantees
Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
<= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
@@ -125,7 +127,7 @@
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[allocGiv]
+ guarantees
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocAsk) s}
LeadsTo
@@ -139,46 +141,62 @@
looked at.*)
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_d program set
- "alloc_preserves == preserves (funPair allocRel
- (funPair allocAsk allocState_d.dummy))"
+ alloc_preserves :: 'a allocState_d program set
+ "alloc_preserves == preserves allocRel Int preserves allocAsk Int
+ preserves allocState_d.dummy"
+ (*environmental constraints*)
+ alloc_allowed_acts :: 'a allocState_d program set
+ "alloc_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves allocGiv) Acts)}"
+
alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
- alloc_preserves"
+ alloc_allowed_acts Int alloc_preserves"
(** Network specification ***)
(*spec (9.1)*)
network_ask :: 'a systemState program set
"network_ask == INT i : lessThan Nclients.
- Increasing (ask o sub i o client)
- guarantees[allocAsk]
+ Increasing (ask o sub i o client) guarantees
((sub i o allocAsk) Fols (ask o sub i o client))"
(*spec (9.2)*)
network_giv :: 'a systemState program set
"network_giv == INT i : lessThan Nclients.
Increasing (sub i o allocGiv)
- guarantees[giv o sub i o client]
+ guarantees
((giv o sub i o client) Fols (sub i o allocGiv))"
(*spec (9.3)*)
network_rel :: 'a systemState program set
"network_rel == INT i : lessThan Nclients.
Increasing (rel o sub i o client)
- guarantees[allocRel]
+ guarantees
((sub i o allocRel) Fols (rel o sub i o client))"
(*spec: preserves part*)
- network_preserves :: 'a systemState program set
- "network_preserves == preserves allocGiv Int
- (INT i : lessThan Nclients.
- preserves (funPair rel ask o sub i o client))"
+ network_preserves :: 'a systemState program set
+ "network_preserves ==
+ preserves allocGiv Int
+ (INT i : lessThan Nclients. preserves (rel o sub i o client) Int
+ preserves (ask o sub i o client))"
+ (*environmental constraints*)
+ network_allowed_acts :: 'a systemState program set
+ "network_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id
+ (UNION (preserves allocRel Int
+ (INT i: lessThan Nclients. preserves(giv o sub i o client)))
+ Acts)}"
+
network_spec :: 'a systemState program set
"network_spec == network_ask Int network_giv Int
- network_rel Int network_preserves"
+ network_rel Int network_allowed_acts Int
+ network_preserves"
(** State mappings **)
--- a/src/HOL/UNITY/AllocImpl.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.ML Sat Sep 23 16:02:01 2000 +0200
@@ -11,21 +11,38 @@
Addsimps [Always_INT_distrib];
Delsimps [o_apply];
-(*Make a locale for M: merge_spec and G: preserves (funPair merge.Out iOut)?*)
+Open_locale "Merge";
+
+val Merge = thm "Merge_spec";
+
+Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
+by (cut_facts_tac [Merge] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [merge_spec_def, merge_allowed_acts_def,
+ Allowed_def, safety_prop_Acts_iff]));
+qed "Merge_Allowed";
-Goalw [merge_spec_def,merge_eqOut_def]
- "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
-\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
-by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
+\ M : Allowed G)";
+by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));
+qed "M_ok_iff";
+AddIffs [M_ok_iff];
+
+Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
+\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD],
+ simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1);
qed "Merge_Always_Out_eq_iOut";
-Goalw [merge_spec_def,merge_bounded_def]
- "[| M: merge_spec; G: preserves merge.iOut |] \
-\ ==> M Join G : Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
-by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
+\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD],
+ simpset() addsimps [merge_spec_def, merge_bounded_def]) 1);
qed "Merge_Bounded";
-Goal "[| M : merge_spec; G : preserves (funPair merge.Out iOut) |] \
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
\ ==> M Join G : Always \
\ {s. setsum (%i. bag_of (sublist (merge.Out s) \
\ {k. k < length (iOut s) & iOut s ! k = i})) \
@@ -45,35 +62,44 @@
by (asm_simp_tac (simpset() addsimps [o_def]) 1);
qed "Merge_Bag_Follows_lemma";
-Goal "M : merge_spec \
-\ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
-\ guarantees[funPair merge.Out merge.iOut] \
-\ (bag_of o merge.Out) Fols \
-\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
-\ (lessThan Nclients))";
+Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
+\ guarantees \
+\ (bag_of o merge.Out) Fols \
+\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
+\ (lessThan Nclients))";
by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
-by Auto_tac;
+by Auto_tac;
by (rtac Follows_setsum 1);
+by (cut_facts_tac [Merge] 1);
by (auto_tac (claset(),
- simpset() addsimps [merge_spec_def,merge_follows_def, o_def]));
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
- addDs [guaranteesD]) 1);
+ simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
+by (dtac guaranteesD 1);
+by (best_tac
+ (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;
qed "Merge_Bag_Follows";
+Close_locale "Merge";
+
(** Distributor **)
-
-Goalw [distr_follows_def]
- "D : distr_follows \
-\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
-\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\ guarantees[distr.Out] \
-\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
+
+Open_locale "Distrib";
+
+val Distrib = thm "Distrib_spec";
+
+
+Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
+\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
+\ guarantees \
+\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
+by (cut_facts_tac [Distrib] 1);
+by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
+by (Clarify_tac 1);
by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
addDs [guaranteesD]) 1);
qed "Distr_Increasing_Out";
-
Goal "[| G : preserves distr.Out; \
\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
\ ==> D Join G : Always \
@@ -94,26 +120,37 @@
by (Asm_simp_tac 1);
qed "Distr_Bag_Follows_lemma";
+Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
+by (cut_facts_tac [Distrib] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [distr_spec_def, distr_allowed_acts_def,
+ Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
+qed "D_ok_iff";
+AddIffs [D_ok_iff];
-Goal "D : distr_follows \
-\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
+Goal
+ "D : Increasing distr.In Int Increasing distr.iIn Int \
\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\ guarantees[distr.Out] \
+\ guarantees \
\ (INT i : lessThan Nclients. \
\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
\ Fols \
\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
by (rtac guaranteesI 1);
-by (Clarify_tac 1);
+by (Clarify_tac 1);
by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;
+by Auto_tac;
by (rtac Follows_setsum 1);
+by (cut_facts_tac [Distrib] 1);
by (auto_tac (claset(),
- simpset() addsimps [distr_follows_def, o_def]));
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
- addDs [guaranteesD]) 1);
+ simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
+by (dtac guaranteesD 1);
+by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;
qed "Distr_Bag_Follows";
+Close_locale "Distrib";
+
Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \
\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
--- a/src/HOL/UNITY/AllocImpl.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy Sat Sep 23 16:02:01 2000 +0200
@@ -58,38 +58,43 @@
(*spec (10)*)
merge_increasing :: ('a,'b) merge_d program set
"merge_increasing ==
- UNIV guarantees[funPair merge.Out merge.iOut]
- (Increasing merge.Out) Int (Increasing merge.iOut)"
+ UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
(*spec (11)*)
merge_eqOut :: ('a,'b) merge_d program set
"merge_eqOut ==
- UNIV guarantees[funPair merge.Out merge.iOut]
+ UNIV guarantees
Always {s. length (merge.Out s) = length (merge.iOut s)}"
(*spec (12)*)
merge_bounded :: ('a,'b) merge_d program set
"merge_bounded ==
- UNIV guarantees[merge.iOut]
+ UNIV guarantees
Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
(*spec (13)*)
merge_follows :: ('a,'b) merge_d program set
"merge_follows ==
(INT i : lessThan Nclients. Increasing (sub i o merge.In))
- guarantees[funPair merge.Out merge.iOut]
+ guarantees
(INT i : lessThan Nclients.
(%s. sublist (merge.Out s)
{k. k < size(merge.iOut s) & merge.iOut s! k = i})
Fols (sub i o merge.In))"
(*spec: preserves part*)
- merge_preserves :: ('a,'b) merge_d program set
- "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
+ merge_preserves :: ('a,'b) merge_d program set
+ "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
+
+ (*environmental constraints*)
+ merge_allowed_acts :: ('a,'b) merge_d program set
+ "merge_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
merge_spec :: ('a,'b) merge_d program set
"merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
- merge_follows Int merge_preserves"
+ merge_follows Int merge_allowed_acts Int merge_preserves"
(** Distributor specification (the number of outputs is Nclients) ***)
@@ -98,24 +103,30 @@
"distr_follows ==
Increasing distr.In Int Increasing distr.iIn Int
Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
- guarantees[distr.Out]
+ guarantees
(INT i : lessThan Nclients.
(sub i o distr.Out) Fols
(%s. sublist (distr.In s)
{k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
+ distr_allowed_acts :: ('a,'b) distr_d program set
+ "distr_allowed_acts ==
+ {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
+
+ distr_spec :: ('a,'b) distr_d program set
+ "distr_spec == distr_follows Int distr_allowed_acts"
(** Single-client allocator specification (required) ***)
(*spec (18)*)
alloc_increasing :: 'a allocState_d program set
- "alloc_increasing == UNIV guarantees[giv] Increasing giv"
+ "alloc_increasing == UNIV guarantees Increasing giv"
(*spec (19)*)
alloc_safety :: 'a allocState_d program set
"alloc_safety ==
Increasing rel
- guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
+ guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
(*spec (20)*)
alloc_progress :: 'a allocState_d program set
@@ -126,86 +137,88 @@
(INT h. {s. h <= giv s & h pfixGe (ask s)}
LeadsTo
{s. tokens h <= tokens (rel s)})
- guarantees[giv]
- (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+ guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_d program set
- "alloc_preserves == preserves (funPair rel
- (funPair ask allocState_d.dummy))"
+ alloc_preserves :: 'a allocState_d program set
+ "alloc_preserves == preserves rel Int
+ preserves ask Int
+ preserves allocState_d.dummy"
+
+ (*environmental constraints*)
+ alloc_allowed_acts :: 'a allocState_d program set
+ "alloc_allowed_acts ==
+ {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
+
alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
- alloc_preserves"
+ alloc_allowed_acts Int alloc_preserves"
+
+locale Merge =
+ fixes
+ M :: ('a,'b::order) merge_d program
+ assumes
+ Merge_spec "M : merge_spec"
+
+locale Distrib =
+ fixes
+ D :: ('a,'b::order) distr_d program
+ assumes
+ Distrib_spec "D : distr_spec"
+
(****
- (** Network specification ***)
+# (** Network specification ***)
- (*spec (9.1)*)
- network_ask :: 'a systemState program set
- "network_ask == INT i : lessThan Nclients.
- Increasing (ask o sub i o client)
- guarantees[ask]
- (ask Fols (ask o sub i o client))"
+# (*spec (9.1)*)
+# network_ask :: 'a systemState program set
+# "network_ask == INT i : lessThan Nclients.
+# Increasing (ask o sub i o client)
+# guarantees[ask]
+# (ask Fols (ask o sub i o client))"
- (*spec (9.2)*)
- network_giv :: 'a systemState program set
- "network_giv == INT i : lessThan Nclients.
- Increasing giv
- guarantees[giv o sub i o client]
- ((giv o sub i o client) Fols giv )"
+# (*spec (9.2)*)
+# network_giv :: 'a systemState program set
+# "network_giv == INT i : lessThan Nclients.
+# Increasing giv
+# guarantees[giv o sub i o client]
+# ((giv o sub i o client) Fols giv )"
- (*spec (9.3)*)
- network_rel :: 'a systemState program set
- "network_rel == INT i : lessThan Nclients.
- Increasing (rel o sub i o client)
- guarantees[rel]
- (rel Fols (rel o sub i o client))"
+# (*spec (9.3)*)
+# network_rel :: 'a systemState program set
+# "network_rel == INT i : lessThan Nclients.
+# Increasing (rel o sub i o client)
+# guarantees[rel]
+# (rel Fols (rel o sub i o client))"
- (*spec: preserves part*)
- network_preserves :: 'a systemState program set
- "network_preserves == preserves giv Int
- (INT i : lessThan Nclients.
- preserves (funPair rel ask o sub i o client))"
+# (*spec: preserves part*)
+# network_preserves :: 'a systemState program set
+# "network_preserves == preserves giv Int
+# (INT i : lessThan Nclients.
+# preserves (funPair rel ask o sub i o client))"
- network_spec :: 'a systemState program set
- "network_spec == network_ask Int network_giv Int
- network_rel Int network_preserves"
+# network_spec :: 'a systemState program set
+# "network_spec == network_ask Int network_giv Int
+# network_rel Int network_preserves"
- (** State mappings **)
- sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
- "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
- in (| giv = giv s,
- ask = ask s,
- rel = rel s,
- client = cl,
- dummy = xtr|)"
+# (** State mappings **)
+# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
+# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
+# in (| giv = giv s,
+# ask = ask s,
+# rel = rel s,
+# client = cl,
+# dummy = xtr|)"
- sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
- "sysOfClient == %(cl,al). (| giv = giv al,
- ask = ask al,
- rel = rel al,
- client = cl,
- systemState.dummy = allocState_d.dummy al|)"
+# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
+# "sysOfClient == %(cl,al). (| giv = giv al,
+# ask = ask al,
+# rel = rel al,
+# client = cl,
+# systemState.dummy = allocState_d.dummy al|)"
****)
-consts
- Alloc :: 'a allocState_d program
- Merge :: ('a,'b) merge_d program
-
-(*
- Network :: 'a systemState program
- System :: 'a systemState program
- *)
-
-rules
- Alloc "Alloc : alloc_spec"
- Merge "Merge : merge_spec"
-
-(** Network "Network : network_spec"**)
-
-
-
end
--- a/src/HOL/UNITY/Client.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Client.ML Sat Sep 23 16:02:01 2000 +0200
@@ -6,15 +6,23 @@
Distributed Resource Management System: the Client
*)
-Addsimps [Client_def RS def_prg_Init];
+Addsimps [Client_def RS def_prg_Init,
+ Client_def RS def_prg_AllowedActs];
program_defs_ref := [Client_def];
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
+Goal "(Client ok G) = \
+\ (G : preserves rel & G : preserves ask & G : preserves tok &\
+\ Client : Allowed G)";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));
+qed "Client_ok_iff";
+AddIffs [Client_ok_iff];
+
(*Safety property 1: ask, rel are increasing*)
-Goal "Client: UNIV guarantees[funPair rel ask] \
-\ Increasing ask Int Increasing rel";
+Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
by (auto_tac
(claset() addSIs [increasing_imp_Increasing],
simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
@@ -23,7 +31,6 @@
by Auto_tac;
qed "increasing_ask_rel";
-
Addsimps [nth_append, append_one_prefix];
@@ -31,10 +38,11 @@
With no Substitution Axiom, we must prove the two invariants
simultaneously.
*)
-Goal "G : preserves (funPair ask tok) \
+Goal "Client ok G \
\ ==> Client Join G : \
\ Always ({s. tok s <= NbT} Int \
\ {s. ALL elt : set (ask s). elt <= NbT})";
+by Auto_tac;
by (rtac (invariantI RS stable_Join_Always2) 1);
by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
addSIs [stable_Int]) 3);
@@ -45,8 +53,7 @@
(*export version, with no mention of tok in the postcondition, but
unfortunately tok must be declared local.*)
-Goal "Client: UNIV guarantees[funPair ask tok] \
-\ Always {s. ALL elt : set (ask s). elt <= NbT}";
+Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
by (rtac guaranteesI 1);
by (etac (ask_bounded_lemma RS Always_weaken) 1);
by (rtac Int_lower2 1);
@@ -83,7 +90,7 @@
qed "transient_lemma";
-Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
\ LeadsTo {s. k < rel s & rel s <= giv s & \
\ h <= giv s & h pfixGe ask s}";
@@ -105,7 +112,7 @@
qed "induct_lemma";
-Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \
\ LeadsTo {s. h <= rel s}";
by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
@@ -120,7 +127,7 @@
qed "rel_progress_lemma";
-Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \
\ LeadsTo {s. h <= rel s}";
by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
@@ -133,7 +140,7 @@
(*Progress property: all tokens that are given will be released*)
Goal "Client : \
-\ Increasing giv guarantees[funPair rel ask] \
+\ Increasing giv guarantees \
\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
@@ -158,7 +165,7 @@
qed "stable_size_rel_le_giv";
(*clients return the right number of tokens*)
-Goal "Client : Increasing giv guarantees[rel] Always {s. rel s <= giv s}";
+Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
by (rtac AlwaysI 1);
by (Force_tac 1);
--- a/src/HOL/UNITY/Client.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Client.thy Sat Sep 23 16:02:01 2000 +0200
@@ -48,9 +48,12 @@
(s' = s (|ask := ask s @ [tok s]|))}"
Client :: 'a state_d program
- "Client == mk_program ({s. tok s : atMost NbT &
- giv s = [] & ask s = [] & rel s = []},
- {rel_act, tok_act, ask_act})"
+ "Client ==
+ mk_program ({s. tok s : atMost NbT &
+ giv s = [] & ask s = [] & rel s = []},
+ {rel_act, tok_act, ask_act},
+ UN G: preserves rel Int preserves ask Int preserves tok.
+ Acts G)"
(*Maybe want a special theory section to declare such maps*)
non_dummy :: 'a state_d => state
--- a/src/HOL/UNITY/Common.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Common.ML Sat Sep 23 16:02:01 2000 +0200
@@ -36,21 +36,22 @@
result();
(*This one is t := ftime t || t := gtime t*)
-Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
+Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
\ : {m} co (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
le_max_iff_disj, fasc]) 1);
result();
(*This one is t := max (ftime t) (gtime t)*)
-Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
+Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
result();
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
-Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
+Goal "mk_program \
+\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \
\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
--- a/src/HOL/UNITY/Common.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Common.thy Sat Sep 23 16:02:01 2000 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-Common = Union +
+Common = SubstAx +
consts
ftime,gtime :: nat=>nat
--- a/src/HOL/UNITY/Comp.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Comp.ML Sat Sep 23 16:02:01 2000 +0200
@@ -19,7 +19,8 @@
qed "componentI";
Goalw [component_def]
- "(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
+ "(F <= G) = \
+\ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)";
by (force_tac (claset() addSIs [exI, program_equalityI],
simpset()) 1);
qed "component_eq_subset";
@@ -110,7 +111,11 @@
by (Blast_tac 1);
qed "JN_preserves";
-AddIffs [Join_preserves, JN_preserves];
+Goal "SKIP : preserves v";
+by (auto_tac (claset(), simpset() addsimps [preserves_def]));
+qed "SKIP_preserves";
+
+AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
by (Simp_tac 1);
@@ -131,7 +136,6 @@
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "funPair_o_distrib";
-
Goal "fst o (funPair f g) = f";
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "fst_o_funPair";
@@ -141,11 +145,9 @@
qed "snd_o_funPair";
Addsimps [fst_o_funPair, snd_o_funPair];
-
Goal "preserves v <= preserves (w o v)";
by (force_tac (claset(),
- simpset() addsimps [preserves_def,
- stable_def, constrains_def]) 1);
+ simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
qed "subset_preserves_o";
Goal "preserves v <= stable {s. P (v s)}";
@@ -168,6 +170,15 @@
qed "preserves_id_subset_stable";
+(** For use with def_UNION_ok_iff **)
+
+Goal "safety_prop (preserves v)";
+by (auto_tac (claset() addIs [safety_prop_INTER1],
+ simpset() addsimps [preserves_def]));
+qed "safety_prop_preserves";
+AddIffs [safety_prop_preserves];
+
+
(** Some lemmas used only in Client.ML **)
Goal "[| F : stable {s. P (v s) (w s)}; \
--- a/src/HOL/UNITY/ELT.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/ELT.ML Sat Sep 23 16:02:01 2000 +0200
@@ -76,6 +76,7 @@
"[| F: A ensures B; A-B: insert {} CC |] ==> F : A leadsTo[CC] B";
by (blast_tac (claset() addIs [elt.Basis]) 1);
qed "leadsETo_Basis";
+AddIs [leadsETo_Basis];
Goalw [leadsETo_def]
"[| F : A leadsTo[CC] B; F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C";
@@ -350,7 +351,7 @@
by (etac leadsETo_induct 1);
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis]) 1);
+by (Blast_tac 1);
qed "leadsETo_subset_leadsTo";
Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
@@ -360,7 +361,7 @@
by (etac leadsTo_induct 1);
by (blast_tac (claset() addIs [leadsETo_Union]) 3);
by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
+by (Blast_tac 1);
qed "leadsETo_UNIV_eq_leadsTo";
(**** weak ****)
@@ -595,7 +596,8 @@
qed "project_LeadsETo_D";
Goalw [extending_def]
- "extending (v o f) (%G. UNIV) h F \
+ "(ALL G. extend h F ok G --> G : preserves (v o f)) \
+\ ==> extending (%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]));
@@ -603,7 +605,8 @@
Goalw [extending_def]
- "extending (v o f) (%G. reachable (extend h F Join G)) h F \
+ "(ALL G. extend h F ok G --> G : preserves (v o f)) \
+\ ==> extending (%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 (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
@@ -637,8 +640,7 @@
by (asm_full_simp_tac
(simpset() addsimps [givenBy_eq_extend_set]) 1);
by (rtac leadsTo_Basis 1);
-by (blast_tac (claset() addIs [leadsTo_Basis,
- ensures_extend_set_imp_project_ensures]) 1);
+by (blast_tac (claset() addIs [ensures_extend_set_imp_project_ensures]) 1);
qed "project_leadsETo_I_lemma";
--- a/src/HOL/UNITY/Extend.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML Sat Sep 23 16:02:01 2000 +0200
@@ -288,6 +288,7 @@
"project_act h (extend_act h act) = act";
by (Blast_tac 1);
qed "extend_act_inverse";
+Addsimps [extend_act_inverse];
Goalw [extend_act_def, project_act_def]
"project_act h (Restrict C (extend_act h act)) = \
@@ -345,7 +346,7 @@
simpset() addsimps [split_extended_all]) 1);
qed "Domain_project_act";
-Addsimps [extend_act_Id];
+Addsimps [extend_act_Id, project_act_Id];
(**** extend ****)
@@ -355,21 +356,43 @@
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)";
by Auto_tac;
qed "Init_extend";
+Addsimps [Init_extend];
Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
by Auto_tac;
qed "Init_project";
+Addsimps [Init_project];
Goal "Acts (extend h F) = (extend_act h `` Acts F)";
by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
qed "Acts_extend";
+Addsimps [Acts_extend];
+
+Goal "AllowedActs (extend h F) = project_act h -`` AllowedActs F";
+by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
+qed "AllowedActs_extend";
+Addsimps [AllowedActs_extend];
Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
by (auto_tac (claset(),
simpset() addsimps [project_def, image_iff]));
qed "Acts_project";
+Addsimps [Acts_project];
-Addsimps [Init_extend, Init_project, Acts_extend, Acts_project];
+Goal "AllowedActs(project h C F) = \
+\ {act. Restrict (project_set h C) act \
+\ : project_act h `` Restrict C `` AllowedActs F}";
+by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
+by (stac insert_absorb 1);
+by (auto_tac (claset() addSIs [inst "x" "Id" bexI],
+ simpset() addsimps [project_act_def]));
+qed "AllowedActs_project";
+Addsimps [AllowedActs_project];
+
+Goal "Allowed (extend h F) = project h UNIV -`` Allowed F";
+by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
+by (Blast_tac 1);
+qed "Allowed_extend";
Goalw [SKIP_def] "extend h SKIP = SKIP";
by (rtac program_equalityI 1);
@@ -386,31 +409,51 @@
by (Blast_tac 1);
qed "project_set_Union";
+(*Converse FAILS: the extended state contributing to project_set h C
+ may not coincide with the one contributing to project_act h act*)
+Goal "project_act h (Restrict C act) <= \
+\ Restrict (project_set h C) (project_act h act)";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
+qed "project_act_Restrict_subset";
+
+
+Goal "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
+qed "project_act_Restrict_Id_eq";
+
Goal "project h C (extend h F) = \
-\ mk_program (Init F, Restrict (project_set h C) `` Acts F)";
+\ mk_program (Init F, Restrict (project_set h C) `` Acts F, \
+\ {act. Restrict (project_set h C) act : project_act h `` Restrict C `` (project_act h -`` AllowedActs F)})";
by (rtac program_equalityI 1);
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [project_def]) 1);
qed "project_extend_eq";
-(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
-Goal "UNIV <= project_set h C \
-\ ==> project h C (extend h F) = F";
+Goal "project h UNIV (extend h F) = F";
by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN,
subset_UNIV RS subset_trans RS Restrict_triv]) 1);
+by (rtac program_equalityI 1);
+by (ALLGOALS Simp_tac);
+by (stac insert_absorb 1);
+by (simp_tac (simpset() addsimps [inst "x" "Id" bexI]) 1);
+by Auto_tac;
+by (rename_tac "act" 1);
+by (res_inst_tac [("x","extend_act h act")] bexI 1);
+by Auto_tac;
qed "extend_inverse";
Addsimps [extend_inverse];
Goal "inj (extend h)";
by (rtac inj_on_inverseI 1);
by (rtac extend_inverse 1);
-by (Force_tac 1);
qed "inj_extend";
Goal "extend h (F Join G) = extend h F Join extend h G";
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [image_Un]) 2);
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
+by Auto_tac;
qed "extend_Join";
Addsimps [extend_Join];
@@ -418,6 +461,7 @@
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [image_UN]) 2);
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
+by Auto_tac;
qed "extend_JN";
Addsimps [extend_JN];
@@ -430,7 +474,7 @@
Goal "F <= G ==> project h C F <= project h C G";
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by Auto_tac;
+by (Blast_tac 1);
qed "project_mono";
@@ -685,9 +729,9 @@
Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
by (rtac program_equalityI 1);
-by (asm_simp_tac
- (simpset() addsimps [image_eq_UN, UN_Un, extend_act_inverse]) 2);
+by (simp_tac (simpset() addsimps [image_eq_UN, UN_Un]) 2);
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
+by Auto_tac;
qed "project_extend_Join";
Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
@@ -698,26 +742,44 @@
(** Strong precondition and postcondition; only useful when
the old and new state sets are in bijection **)
-Goal "F : X guarantees[v] Y ==> \
-\ extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
+
+Goal "extend h F ok G ==> F ok project h UNIV G";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (dtac subsetD 1);
+by (auto_tac (claset() addSIs [rev_image_eqI], simpset()));
+qed "ok_extend_imp_ok_project";
+
+Goal "(extend h F ok extend h G) = (F ok G)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_extend_iff";
+
+Goal "OK I (%i. extend h (F i)) = (OK I F)";
+by (auto_tac (claset(), simpset() addsimps [OK_def]));
+by (dres_inst_tac [("x","i")] bspec 1);
+by (dres_inst_tac [("x","j")] bspec 2);
+by Auto_tac;
+qed "OK_extend_iff";
+
+Goal "F : X guarantees Y ==> \
+\ extend h F : (extend h `` X) guarantees (extend h `` Y)";
by (rtac guaranteesI 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [project_preserves_I]
- addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addDs [ok_extend_imp_ok_project,
+ extend_Join_eq_extend_D, guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
-Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
-\ ==> F : X guarantees[v] Y";
+Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
+\ ==> F : X guarantees Y";
by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] bspec 1);
+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]) 2);
-by (asm_simp_tac (simpset() addsimps [extend_preserves]) 1);
+ addsimps [extend_Join RS sym, ok_extend_iff,
+ inj_extend RS inj_image_mem_iff]) 1);
qed "extend_guarantees_imp_guarantees";
-Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
-\ (F : X guarantees[v] Y)";
+Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
+\ (F : X guarantees Y)";
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
extend_guarantees_imp_guarantees]) 1);
qed "extend_guarantees_eq";
--- a/src/HOL/UNITY/Extend.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy Sat Sep 23 16:02:01 2000 +0200
@@ -34,12 +34,16 @@
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
- extend_act h `` Acts F)"
+ extend_act h `` Acts F,
+ project_act h -`` AllowedActs F)"
(*Argument C allows weak safety laws to be projected*)
project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
- "project h C F == mk_program (project_set h (Init F),
- project_act h `` Restrict C `` Acts F)"
+ "project h C F ==
+ mk_program (project_set h (Init F),
+ project_act h `` Restrict C `` Acts F,
+ {act. Restrict (project_set h C) act :
+ project_act h `` Restrict C `` AllowedActs F})"
locale Extend =
fixes
--- a/src/HOL/UNITY/Guar.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Guar.ML Sat Sep 23 16:02:01 2000 +0200
@@ -65,14 +65,14 @@
(*** guarantees ***)
val prems = Goal
- "(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \
-\ ==> F : X guarantees[v] Y";
+ "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \
+\ ==> F : X guarantees 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[v] Y; G : preserves v; F Join G : X |] \
+ "[| F : X guarantees Y; F ok G; F Join G : X |] \
\ ==> F Join G : Y";
by (Blast_tac 1);
qed "guaranteesD";
@@ -80,33 +80,27 @@
(*This version of guaranteesD matches more easily in the conclusion
The major premise can no longer be F<=H since we need to reason about G*)
Goalw [guar_def]
- "[| F : X guarantees[v] Y; F Join G = H; H : X; G : preserves v |] \
+ "[| F : X guarantees Y; F Join G = H; H : X; F ok G |] \
\ ==> H : Y";
by (Blast_tac 1);
qed "component_guaranteesD";
Goalw [guar_def]
- "[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'";
+ "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
by (Blast_tac 1);
qed "guarantees_weaken";
-Goalw [guar_def]
- "[| 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[v] 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 [guar_def] "X <= Y ==> F : X guarantees[v] 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 [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] 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";
@@ -115,40 +109,40 @@
(** Distributive laws. Re-orient to perform miniscoping **)
Goalw [guar_def]
- "(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)";
+ "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
by (Blast_tac 1);
qed "guarantees_UN_left";
Goalw [guar_def]
- "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
+ "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
by (Blast_tac 1);
qed "guarantees_Un_left";
Goalw [guar_def]
- "X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)";
+ "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
by (Blast_tac 1);
qed "guarantees_INT_right";
Goalw [guar_def]
- "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
+ "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
by (Blast_tac 1);
qed "guarantees_Int_right";
-Goal "[| F : Z guarantees[v] X; F : Z guarantees[v] Y |] \
-\ ==> F : Z guarantees[v] (X Int Y)";
+Goal "[| F : Z guarantees X; F : Z guarantees Y |] \
+\ ==> F : Z guarantees (X Int Y)";
by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
qed "guarantees_Int_right_I";
-Goal "(F : X guarantees[v] (INTER I Y)) = \
-\ (ALL i:I. F : X guarantees[v] (Y i))";
+Goal "(F : X guarantees (INTER I Y)) = \
+\ (ALL i:I. F : X guarantees (Y i))";
by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
qed "guarantees_INT_right_iff";
-Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))";
+Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
by (Blast_tac 1);
qed "shunting";
-Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X";
+Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
by (Blast_tac 1);
qed "contrapositive";
@@ -157,119 +151,115 @@
**)
Goalw [guar_def]
- "[| F : V guarantees[v] X; F : (X Int Y) guarantees[v] Z |]\
-\ ==> F : (V Int Y) guarantees[v] Z";
+ "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
+\ ==> F : (V Int Y) guarantees Z";
by (Blast_tac 1);
qed "combining1";
Goalw [guar_def]
- "[| F : V guarantees[v] (X Un Y); F : Y guarantees[v] Z |]\
-\ ==> F : V guarantees[v] (X Un Z)";
+ "[| 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 guarantees[v] Y i) *)
+(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
Goalw [guar_def]
- "ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)";
+ "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 guarantees[v] Y i; i: I |] *)
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
Goalw [guar_def]
- "EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)";
+ "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 [guar_def]
- "[| 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)";
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |] \
+\ ==> F Join G: (U Int X) guarantees (V Int Y)";
by (Simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1);
by (asm_simp_tac (simpset() addsimps Join_ac) 1);
qed "guarantees_Join_Int";
Goalw [guar_def]
- "[| 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)";
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |] \
+\ ==> F Join G: (U Un X) guarantees (V Un Y)";
by (Simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 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[v] Y i; \
-\ ALL i:I. F i : preserves v |] \
-\ ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
+ "[| ALL i:I. F i : X i guarantees Y i; OK I F |] \
+\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
by Auto_tac;
by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
by (auto_tac
- (claset(),
- simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+ (claset() addIs [OK_imp_ok],
+ simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
qed "guarantees_JN_INT";
Goalw [guar_def]
- "[| 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)";
+ "[| ALL i:I. F i : X i guarantees Y i; OK I F |] \
+\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
by Auto_tac;
by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
by (auto_tac
- (claset(),
- simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+ (claset() addIs [OK_imp_ok],
+ simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
qed "guarantees_JN_INT";
Goalw [guar_def]
- "[| 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)";
+ "[| ALL i:I. F i : X i guarantees Y i; OK I F |] \
+\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
by Auto_tac;
by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
by (auto_tac
- (claset(),
- simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+ (claset() addIs [OK_imp_ok],
+ simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
qed "guarantees_JN_UN";
-(*** guarantees[v] laws for breaking down the program, by lcp ***)
+(*** guarantees laws for breaking down the program, by lcp ***)
Goalw [guar_def]
- "[| F: X guarantees[v] Y; G: preserves v |] \
-\ ==> F Join G: X guarantees[v] Y";
+ "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y";
by (Simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
qed "guarantees_Join_I1";
-Goal "[| G: X guarantees[v] Y; F: preserves v |] \
-\ ==> F Join G: X guarantees[v] Y";
-by (stac Join_commute 1);
+Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y";
+by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute,
+ inst "G" "G" ok_commute]) 1);
by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
qed "guarantees_Join_I2";
Goalw [guar_def]
- "[| 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";
+ "[| i : I; F i: X guarantees Y; OK I F |] \
+\ ==> (JN i:I. (F i)) : X guarantees Y";
by (Clarify_tac 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] bspec 1);
-by (auto_tac (claset(),
- simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
+by (auto_tac (claset() addIs [OK_imp_ok],
+ simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym]));
qed "guarantees_JN_I";
--- a/src/HOL/UNITY/Guar.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Guar.thy Sat Sep 23 16:02:01 2000 +0200
@@ -35,11 +35,9 @@
welldef :: 'a program set
"welldef == {F. Init F ~= {}}"
- 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 : preserves v.
- F Join G : X --> F Join G : Y}"
+ guar :: ['a program set, 'a program set] => 'a program set
+ (infixl "guarantees" 55) (*higher than membership, lower than Co*)
+ "X guarantees Y == {F. ALL G. F ok G --> 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/Handshake.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Handshake.thy Sat Sep 23 16:02:01 2000 +0200
@@ -21,14 +21,14 @@
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
F :: "state program"
- "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
+ "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
(*G's program*)
cmdG :: "(state*state) set"
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
G :: "state program"
- "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
+ "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
(*the joint invariant*)
invFG :: "state set"
--- a/src/HOL/UNITY/Lift.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Lift.thy Sat Sep 23 16:02:01 2000 +0200
@@ -108,6 +108,10 @@
{(s,s'). s' = s (|floor := floor s - #1|)
& ~ stop s & ~ up s & floor s ~: req s}"
+ (*This action is omitted from prior treatments, which therefore are
+ unrealistic: nobody asks the lift to do anything! But adding this
+ action invalidates many of the existing progress arguments: various
+ "ensures" properties fail.*)
button_press :: "(state*state) set"
"button_press ==
{(s,s'). EX n. s' = s (|req := insert n (req s)|)
@@ -119,7 +123,8 @@
"Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
{request_act, open_act, close_act,
- req_up, req_down, move_up, move_down})"
+ req_up, req_down, move_up, move_down},
+ UNIV)"
(** Invariants **)
--- a/src/HOL/UNITY/Lift_prog.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Sat Sep 23 16:02:01 2000 +0200
@@ -133,6 +133,11 @@
(*** the lattice operations ***)
+Goal "bij (lift i)";
+by (simp_tac (simpset() addsimps [lift_def]) 1);
+qed "bij_lift";
+AddIffs [bij_lift];
+
Goalw [lift_def] "lift i SKIP = SKIP";
by (Asm_simp_tac 1);
qed "lift_SKIP";
@@ -209,15 +214,14 @@
(** guarantees **)
Goalw [lift_def]
- "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
-\ (F : X guarantees[v] Y)";
+ "(lift i F : (lift i `` X) guarantees (lift i `` Y)) = \
+\ (F : X guarantees Y)";
by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
by (asm_simp_tac (simpset() addsimps [o_def]) 1);
qed "lift_lift_guarantees_eq";
-Goal "(lift i F : X guarantees[v] Y) = \
-\ (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
-\ (rename (drop_map i) `` Y))";
+Goal "(lift i F : X guarantees Y) = \
+\ (F : (rename (drop_map i) `` X) guarantees (rename (drop_map i) `` Y))";
by (asm_simp_tac
(simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
lift_def]) 1);
@@ -409,4 +413,74 @@
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
+(*** More lemmas about extend and project
+ They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
+Goal "extend_act h' (extend_act h act) = \
+\ extend_act (%(x,(y,y')). h'(h(x,y),y')) act";
+by (auto_tac (claset() addSEs [rev_bexI],
+ simpset() addsimps [extend_act_def]));
+by (ALLGOALS Blast_tac);
+qed "extend_act_extend_act";
+
+Goal "project_act h (project_act h' act) = \
+\ project_act (%(x,(y,y')). h'(h(x,y),y')) act";
+by (auto_tac (claset() addSEs [rev_bexI],
+ simpset() addsimps [project_act_def]));
+qed "project_act_project_act";
+
+Goal "project_act h (extend_act h' act) = \
+\ {(x,x'). EX s s' y y' z. (s,s') : act & \
+\ h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}";
+by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1);
+by (Blast_tac 1);
+qed "project_act_extend_act";
+
+
+(*** OK and "lift" ***)
+
+Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts";
+by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1);
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def,stable_def,constrains_def]));
+qed "act_in_UNION_preserves_fst";
+
+Goal "[| ALL i:I. F i : preserves snd; \
+\ ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
+\ ==> OK I (%i. lift i (F i))";
+by (auto_tac (claset(),
+ simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend,
+ export AllowedActs_extend, project_act_extend_act]));
+by (rename_tac "act" 1);
+by (subgoal_tac
+ "{(x, x'). EX s f u s' f' u'. \
+\ ((s, f, u), s', f', u') : act & \
+\ lift_map j x = lift_map i (s, f, u) & \
+\ lift_map j x' = lift_map i (s', f', u')} \
+\ <= {(x,x'). fst x = fst x'}" 1);
+by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1);
+by (Clarify_tac 1);
+by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) );
+by (dres_inst_tac [("x","i")] bspec 1);
+by (assume_tac 1);
+by (ftac preserves_imp_eq 1);
+by Auto_tac;
+qed "UNION_OK_lift_I";
+
+Goal "[| ALL i:I. F i : preserves snd; \
+\ ALL i:I. preserves fst <= Allowed (F i) |] \
+\ ==> OK I (%i. lift i (F i))";
+by (asm_full_simp_tac
+ (simpset() addsimps [safety_prop_AllowedActs_iff_Allowed,
+ UNION_OK_lift_I]) 1);
+qed "OK_lift_I";
+
+Goal "Allowed (lift i F) = lift i `` (Allowed F)";
+by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1);
+qed "Allowed_lift";
+Addsimps [Allowed_lift];
+
+Goal "lift i `` preserves v = preserves (v o drop_map i)";
+by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def,
+ inv_lift_map_eq]) 1);
+qed "lift_image_preserves";
--- a/src/HOL/UNITY/Mutex.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Mutex.thy Sat Sep 23 16:02:01 2000 +0200
@@ -55,7 +55,8 @@
Mutex :: state program
"Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
- {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4})"
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
+ UNIV)"
(** The correct invariants **)
--- a/src/HOL/UNITY/NSP_Bad.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy Sat Sep 23 16:02:01 2000 +0200
@@ -54,6 +54,6 @@
constdefs
Nprg :: state program
(*Initial trace is empty*)
- "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
+ "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
end
--- a/src/HOL/UNITY/PPROD.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML Sat Sep 23 16:02:01 2000 +0200
@@ -121,12 +121,21 @@
something like lift_preserves_sub to rewrite the third. However there's
no obvious way to alternative for the third premise.*)
Goalw [PLam_def]
- "[| lift i (F i): X guarantees[v] Y; i : I; \
-\ ALL j:I. i~=j --> lift j (F j) : preserves v |] \
-\ ==> (PLam I F) : X guarantees[v] Y";
+ "[| lift i (F i): X guarantees Y; i : I; \
+\ OK I (%i. lift i (F i)) |] \
+\ ==> (PLam I F) : X guarantees Y";
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
qed "guarantees_PLam_I";
+Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
+by (simp_tac (simpset() addsimps [PLam_def]) 1);
+qed "Allowed_PLam";
+Addsimps [Allowed_PLam];
+
+Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1);
+qed "PLam_preserves";
+Addsimps [PLam_preserves];
(**UNUSED
(*The f0 premise ensures that the product is well-defined.*)
--- a/src/HOL/UNITY/Project.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Project.ML Sat Sep 23 16:02:01 2000 +0200
@@ -120,38 +120,36 @@
qed "projecting_weaken_L";
Goalw [extending_def]
- "[| 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)";
+ "[| extending C h F YA' YA; extending C h F YB' YB |] \
+\ ==> extending C h F (YA' Int YB') (YA Int YB)";
by (Blast_tac 1);
qed "extending_Int";
Goalw [extending_def]
- "[| 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)";
+ "[| extending C h F YA' YA; extending C h F YB' YB |] \
+\ ==> extending C h F (YA' Un YB') (YA Un YB)";
by (Blast_tac 1);
qed "extending_Un";
val [prem] = Goalw [extending_def]
- "[| !!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)";
+ "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
+\ ==> extending 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 v C h F (Y' i) (Y i) |] \
-\ ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
+ "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
+\ ==> extending 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 v C h F Y' Y; Y'<=V'; V<=Y; \
-\ preserves w <= preserves v |] \
-\ ==> extending w C h F V' V";
+ "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V";
by Auto_tac;
qed "extending_weaken";
Goalw [extending_def]
- "[| extending v C h F Y' Y; Y'<=V' |] ==> extending v C h F V' Y";
+ "[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y";
by Auto_tac;
qed "extending_weaken_L";
@@ -174,22 +172,22 @@
by (blast_tac (claset() addIs [project_increasing_I]) 1);
qed "projecting_increasing";
-Goal "extending v C h F UNIV Y";
+Goal "extending C h F UNIV Y";
by (simp_tac (simpset() addsimps [extending_def]) 1);
qed "extending_UNIV";
Goalw [extending_def]
- "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
+ "extending (%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 v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
+ "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
by (rtac extending_constrains 1);
qed "extending_stable";
Goalw [extending_def]
- "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
+ "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)";
by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
qed "extending_increasing";
@@ -354,25 +352,25 @@
qed "projecting_Increasing";
Goalw [extending_def]
- "extending v (%G. reachable (extend h F Join G)) h F \
+ "extending (%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 v (%G. reachable (extend h F Join G)) h F \
+ "extending (%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 v (%G. reachable (extend h F Join G)) h F \
+ "extending (%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";
Goalw [extending_def]
- "extending v (%G. reachable (extend h F Join G)) h F \
+ "extending (%G. reachable (extend h F Join G)) h F \
\ (Increasing (func o f)) (Increasing func)";
by (blast_tac (claset() addIs [project_Increasing_D]) 1);
qed "extending_Increasing";
@@ -596,31 +594,46 @@
(*** Guarantees ***)
+Goal "project_act h (Restrict C act) <= project_act h act";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
+qed "project_act_Restrict_subset_project_act";
+
+
+Goal "[| extend h F ok G; subset_closed (AllowedActs F) |] \
+\ ==> F ok project h C G";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (dtac subsetD 1);
+by (Blast_tac 1);
+by (force_tac (claset() addSIs [rev_image_eqI], simpset()) 1);
+by (cut_facts_tac [project_act_Restrict_subset_project_act] 1);
+by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));
+qed "subset_closed_ok_extend_imp_ok_project";
+
+
(*Weak precondition and postcondition
Not clear that it has a converse [or that we want one!]*)
(*The raw version; 3rd premise could be weakened by adding the
precondition extend h F Join G : X' *)
-val [xguary,project,extend] =
-Goal "[| F : X guarantees[v] Y; \
+val [xguary,closed,project,extend] =
+Goal "[| F : X guarantees Y; subset_closed (AllowedActs F); \
\ !!G. extend h F Join G : X' ==> F Join project h (C G) G : X; \
-\ !!G. [| F Join project h (C G) G : Y; G : preserves (v o f) |] \
+\ !!G. [| F Join project h (C G) G : Y |] \
\ ==> extend h F Join G : Y' |] \
-\ ==> extend h F : X' guarantees[v o f] Y'";
+\ ==> extend h F : X' guarantees Y'";
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
-by (etac project_preserves_I 1);
+by (blast_tac (claset() addIs [closed,
+ subset_closed_ok_extend_imp_ok_project]) 1);
by (etac project 1);
-by Auto_tac;
qed "project_guarantees_raw";
-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'";
+Goal "[| F : X guarantees Y; subset_closed (AllowedActs F); \
+\ projecting C h F X' X; extending C h F Y' Y |] \
+\ ==> extend h F : X' guarantees Y'";
by (rtac guaranteesI 1);
by (auto_tac (claset(),
- simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
- extending_def]));
+ simpset() addsimps [guaranteesD, projecting_def,
+ extending_def, subset_closed_ok_extend_imp_ok_project]));
qed "project_guarantees";
@@ -631,28 +644,31 @@
(** Some could be deleted: the required versions are easy to prove **)
-Goal "F : UNIV guarantees[v] increasing func \
-\ ==> extend h F : X' guarantees[v o f] increasing (func o f)";
+Goal "[| F : UNIV guarantees increasing func; \
+\ subset_closed (AllowedActs F) |] \
+\ ==> extend h F : X' guarantees increasing (func o f)";
by (etac project_guarantees 1);
-by (rtac extending_increasing 2);
-by (rtac projecting_UNIV 1);
+by (rtac extending_increasing 3);
+by (rtac projecting_UNIV 2);
by Auto_tac;
qed "extend_guar_increasing";
-Goal "F : UNIV guarantees[v] Increasing func \
-\ ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
+Goal "[| F : UNIV guarantees Increasing func; \
+\ subset_closed (AllowedActs F) |] \
+\ ==> extend h F : X' guarantees Increasing (func o f)";
by (etac project_guarantees 1);
-by (rtac extending_Increasing 2);
-by (rtac projecting_UNIV 1);
+by (rtac extending_Increasing 3);
+by (rtac projecting_UNIV 2);
by Auto_tac;
qed "extend_guar_Increasing";
-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)";
+Goal "[| F : Always A guarantees Always B; \
+\ subset_closed (AllowedActs F) |] \
+\ ==> extend h F \
+\ : Always(extend_set h A) guarantees Always(extend_set h B)";
by (etac project_guarantees 1);
-by (rtac extending_Always 2);
-by (rtac projecting_Always 1);
+by (rtac extending_Always 3);
+by (rtac projecting_Always 2);
by Auto_tac;
qed "extend_guar_Always";
@@ -676,8 +692,8 @@
simpset()));
qed "project_leadsTo_D";
-Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
-\ G : preserves f |] \
+Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
+\ 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() addDs [preserves_project_transient_empty],
@@ -685,35 +701,17 @@
qed "project_LeadsTo_D";
Goalw [extending_def]
- "extending f (%G. UNIV) h F \
+ "(ALL G. extend h F ok G --> G : preserves f) \
+\ ==> extending (%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 f (%G. reachable (extend h F Join G)) h F \
+ "(ALL G. extend h F ok G --> G : preserves f) \
+\ ==> extending (%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[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 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[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 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 Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Project.thy Sat Sep 23 16:02:01 2000 +0200
@@ -13,13 +13,16 @@
constdefs
projecting :: "['c program => 'c set, 'a*'b => 'c,
'a program, 'c program set, 'a program set] => bool"
- "projecting C h F X' X ==
- ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
+ "projecting C h F X' X ==
+ ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
- extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program,
+ extending :: "['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'"
+ "extending C h F Y' Y ==
+ ALL G. extend h F ok G --> F Join project h (C G) G : Y
+ --> extend h F Join G : Y'"
+
+ subset_closed :: "'a set set => bool"
+ "subset_closed U == ALL A: U. Pow A <= U"
end
--- a/src/HOL/UNITY/Reach.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Reach.thy Sat Sep 23 16:02:01 2000 +0200
@@ -24,7 +24,7 @@
"asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
Rprg :: state program
- "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})"
+ "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
reach_invariant :: state set
"reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
--- a/src/HOL/UNITY/Rename.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML Sat Sep 23 16:02:01 2000 +0200
@@ -13,6 +13,7 @@
by Auto_tac;
qed "good_map_bij";
Addsimps [good_map_bij];
+AddIs [good_map_bij];
fun bij_export th = good_map_bij RS export th |> simplify (simpset());
@@ -57,12 +58,35 @@
(** for "rename" (programs) **)
Goal "bij h \
-\ ==> extend_act (%(x,u::'c). inv h x) = project_act (%(x,u::'c). h x)";
+\ ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)";
by (rtac ext 1);
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_act_def, project_act_def, bij_def,
surj_f_inv_f]));
-qed "extend_act_inv";
+qed "bij_extend_act_eq_project_act";
+
+Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))";
+by (rtac bijI 1);
+by (rtac (export inj_extend_act) 1);
+by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));
+by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI,
+ export extend_act_inverse]) 1);
+qed "bij_extend_act";
+
+Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
+by (ftac (bij_imp_bij_inv RS bij_extend_act) 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act,
+ bij_imp_bij_inv, inv_inv_eq]) 1);
+qed "bij_project_act";
+
+Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \
+\ project_act (%(x,u::'c). h x)";
+by (asm_simp_tac
+ (simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1);
+by (rtac surj_imp_inv_eq 1);
+by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1);
+by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1);
+qed "bij_inv_project_act_eq";
Goal "bij h \
\ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
@@ -71,8 +95,14 @@
by (rtac program_equalityI 1);
by (asm_simp_tac
(simpset() addsimps [export project_act_Id, export Acts_extend,
- insert_Id_image_Acts, extend_act_inv]) 2);
+ insert_Id_image_Acts, bij_extend_act_eq_project_act,
+ inv_inv_eq]) 2);
by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
+by (asm_simp_tac
+ (simpset() addsimps [export AllowedActs_extend,
+ export AllowedActs_project,
+ bij_project_act, bij_vimage_eq_inv_image,
+ bij_inv_project_act_eq]) 1);
qed "extend_inv";
Goal "bij h ==> rename (inv h) (rename h F) = F";
@@ -94,24 +124,45 @@
(** (rename h) is bijective <=> h is bijective **)
-Goal "bij h ==> inj (rename h)";
-by (asm_simp_tac (simpset() addsimps [inj_iff, expand_fun_eq, o_def,
- rename_inv_eq RS sym]) 1);
-qed "inj_rename";
+Goal "bij h ==> bij (extend (%(x,u::'c). h x))";
+by (rtac bijI 1);
+by (blast_tac (claset() addIs [export inj_extend]) 1);
+by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1);
+by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1
+ THEN stac extend_inv 2 THEN stac (export extend_inverse) 3);
+by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq]));
+qed "bij_extend";
+
+Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)";
+by (stac (extend_inv RS sym) 1);
+by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend]));
+qed "bij_project";
-Goal "bij h ==> surj (rename h)";
-by (asm_simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def,
- rename_inv_eq RS sym]) 1);
-qed "surj_rename";
+Goal "bij h \
+\ ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)";
+by (rtac inj_imp_inv_eq 1);
+by (etac (bij_project RS bij_is_inj) 1);
+by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1);
+qed "inv_project_eq";
+
+Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
+by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
+by (stac bij_vimage_eq_inv_image 1);
+by (rtac bij_project 1);
+by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1);
+qed "Allowed_rename";
+Addsimps [Allowed_rename];
Goal "bij h ==> bij (rename h)";
-by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1);
+by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1);
qed "bij_rename";
+bind_thm ("surj_rename", bij_rename RS bij_is_surj);
Goalw [inj_on_def] "inj (rename h) ==> inj h";
by Auto_tac;
-by (dres_inst_tac [("x", "mk_program ({x}, {})")] spec 1);
-by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
+by (dres_inst_tac [("x", "mk_program ({x}, {}, {})")] spec 1);
+by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
by (auto_tac (claset(),
simpset() addsimps [program_equality_iff,
rename_def, extend_def]));
@@ -119,7 +170,7 @@
Goalw [surj_def] "surj (rename h) ==> surj h";
by Auto_tac;
-by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
+by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
by (auto_tac (claset(),
simpset() addsimps [program_equality_iff,
rename_def, extend_def]));
@@ -135,6 +186,7 @@
qed "bij_rename_iff";
AddIffs [bij_rename_iff];
+
(*** the lattice operations ***)
Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
@@ -236,16 +288,16 @@
qed "rename_LeadsTo";
Goalw [rename_def]
- "bij h ==> (rename h F : (rename h `` X) guarantees[v o inv h] \
+ "bij h ==> (rename h F : (rename h `` X) guarantees \
\ (rename h `` Y)) = \
-\ (F : X guarantees[v] Y)";
+\ (F : X guarantees Y)";
by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
qed "rename_rename_guarantees_eq";
-Goal "bij h ==> (rename h F : X guarantees[v] Y) = \
-\ (F : (rename (inv h) `` X) guarantees[v o h] \
+Goal "bij h ==> (rename h F : X guarantees Y) = \
+\ (F : (rename (inv h) `` X) guarantees \
\ (rename (inv h) `` Y))";
by (stac (rename_rename_guarantees_eq RS sym) 1);
by (assume_tac 1);
@@ -260,6 +312,16 @@
bij_is_surj RS surj_f_inv_f]) 1);
qed "rename_preserves";
+Goal "bij h ==> (rename h F ok rename h G) = (F ok G)";
+by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1);
+qed "ok_rename_iff";
+Addsimps [ok_rename_iff];
+
+Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)";
+by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1);
+qed "OK_rename_iff";
+Addsimps [OK_rename_iff];
+
(*** "image" versions of the rules, for lifting "guarantees" properties ***)
@@ -294,6 +356,11 @@
by (rename_image_tac [rename_Constrains]);
qed "rename_image_Constrains";
+Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
+by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
+ preserves_def, bij_image_INT, bij_image_Collect_eq]) 1);
+qed "rename_image_preserves";
+
Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
by (rename_image_tac [rename_Stable]);
qed "rename_image_Stable";
--- a/src/HOL/UNITY/TimerArray.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.thy Sat Sep 23 16:02:01 2000 +0200
@@ -18,6 +18,6 @@
"decr == UN n uu. {((Suc n, uu), (n,uu))}"
Timer :: 'a state program
- "Timer == mk_program (UNIV, {decr})"
+ "Timer == mk_program (UNIV, {decr}, UNIV)"
end
--- a/src/HOL/UNITY/UNITY.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML Sat Sep 23 16:02:01 2000 +0200
@@ -8,16 +8,14 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-set timing;
-
(*Perhaps equalities.ML shouldn't add this in the first place!*)
Delsimps [image_Collect];
-
(*** The abstract type of programs ***)
val rep_ss = simpset() addsimps
- [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program,
+ [Init_def, Acts_def, AllowedActs_def,
+ mk_program_def, Program_def, Rep_Program,
Rep_Program_inverse, Abs_Program_inverse];
@@ -32,41 +30,59 @@
qed "insert_Id_Acts";
AddIffs [insert_Id_Acts];
+Goal "Id : AllowedActs F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
+by (auto_tac (claset(), rep_ss));
+qed "Id_in_AllowedActs";
+AddIffs [Id_in_AllowedActs];
+
+Goal "insert Id (AllowedActs F) = AllowedActs F";
+by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1);
+qed "insert_Id_AllowedActs";
+AddIffs [insert_Id_AllowedActs];
+
(** Inspectors for type "program" **)
-Goal "Init (mk_program (init,acts)) = init";
+Goal "Init (mk_program (init,acts,allowed)) = init";
by (auto_tac (claset(), rep_ss));
qed "Init_eq";
-Goal "Acts (mk_program (init,acts)) = insert Id acts";
+Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts";
by (auto_tac (claset(), rep_ss));
qed "Acts_eq";
-Addsimps [Acts_eq, Init_eq];
+Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed";
+by (auto_tac (claset(), rep_ss));
+qed "AllowedActs_eq";
+Addsimps [Init_eq, Acts_eq, AllowedActs_eq];
(** Equality for UNITY programs **)
-Goal "mk_program (Init F, Acts F) = F";
+Goal "mk_program (Init F, Acts F, AllowedActs F) = F";
by (cut_inst_tac [("x", "F")] Rep_Program 1);
by (auto_tac (claset(), rep_ss));
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
qed "surjective_mk_program";
-Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \
+\ ==> F = G";
by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
by (Asm_simp_tac 1);
qed "program_equalityI";
val [major,minor] =
-Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
+Goal "[| F = G; \
+\ [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\
+\ ==> P |] ==> P";
by (rtac minor 1);
by (auto_tac (claset(), simpset() addsimps [major]));
qed "program_equalityE";
-Goal "(F=G) = (Init F = Init G & Acts F = Acts G)";
+Goal "(F=G) = \
+\ (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)";
by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
qed "program_equality_iff";
@@ -77,13 +93,22 @@
They avoid expanding the full program, which is a large expression
***)
-Goal "F == mk_program (init,acts) ==> Init F = init";
+Goal "F == mk_program (init,acts,allowed) ==> Init F = init";
by Auto_tac;
qed "def_prg_Init";
+Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts";
+by Auto_tac;
+qed "def_prg_Acts";
+
+Goal "F == mk_program (init,acts,allowed) \
+\ ==> AllowedActs F = insert Id allowed";
+by Auto_tac;
+qed "def_prg_AllowedActs";
+
(*The program is not expanded, but its Init and Acts are*)
val [rew] = goal thy
- "[| F == mk_program (init,acts) |] \
+ "[| F == mk_program (init,acts,allowed) |] \
\ ==> Init F = init & Acts F = insert Id acts";
by (rewtac rew);
by Auto_tac;
--- a/src/HOL/UNITY/UNITY.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.thy Sat Sep 23 16:02:01 2000 +0200
@@ -11,21 +11,30 @@
UNITY = Main +
typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+ 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
+ allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
consts
constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
constdefs
- mk_program :: "('a set * ('a * 'a)set set) => 'a program"
- "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+ mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
+ => 'a program"
+ "mk_program == %(init, acts, allowed).
+ Abs_Program (init, insert Id acts, insert Id allowed)"
Init :: "'a program => 'a set"
- "Init F == (%(init, acts). init) (Rep_Program F)"
+ "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
Acts :: "'a program => ('a * 'a)set set"
- "Acts F == (%(init, acts). acts) (Rep_Program F)"
+ "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
+
+ AllowedActs :: "'a program => ('a * 'a)set set"
+ "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
+
+ Allowed :: "'a program => 'a program set"
+ "Allowed F == {G. Acts G <= AllowedActs F}"
stable :: "'a set => 'a program set"
"stable A == A co A"
--- a/src/HOL/UNITY/Union.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Union.ML Sat Sep 23 16:02:01 2000 +0200
@@ -19,7 +19,11 @@
by (simp_tac (simpset() addsimps [SKIP_def]) 1);
qed "Acts_SKIP";
-Addsimps [Init_SKIP, Acts_SKIP];
+Goal "AllowedActs SKIP = UNIV";
+by (auto_tac (claset(), simpset() addsimps [SKIP_def]));
+qed "AllowedActs_SKIP";
+
+Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP];
Goal "reachable SKIP = UNIV";
by (force_tac (claset() addEs [reachable.induct]
@@ -56,7 +60,11 @@
by (auto_tac (claset(), simpset() addsimps [Join_def]));
qed "Acts_Join";
-Addsimps [Init_Join, Acts_Join];
+Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G";
+by (auto_tac (claset(), simpset() addsimps [Join_def]));
+qed "AllowedActs_Join";
+
+Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
(** JN **)
@@ -68,7 +76,7 @@
Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)";
by (rtac program_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
+by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def]));
qed "JN_insert";
Addsimps[JN_empty, JN_insert];
@@ -80,7 +88,11 @@
by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
qed "Acts_JN";
-Addsimps [Init_JN, Acts_JN];
+Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))";
+by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
+qed "AllowedActs_JN";
+
+Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
val prems = Goalw [JOIN_def]
"[| I=J; !!i. i:J ==> F i = G i |] ==> \
@@ -97,12 +109,14 @@
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
qed "Join_commute";
+
Goal "A Join (B Join C) = B Join (A Join C)";
-by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def]) 1);
+by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def, insert_absorb]) 1);
qed "Join_left_commute";
+
Goal "(F Join G) Join H = F Join (G Join H)";
-by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
+by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
qed "Join_assoc";
Goalw [Join_def, SKIP_def] "SKIP Join F = F";
@@ -316,3 +330,142 @@
qed "stable_Join_ensures2";
+(*** the ok and OK relations ***)
+
+Goal "SKIP ok F";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_SKIP1";
+
+Goal "F ok SKIP";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_SKIP2";
+
+AddIffs [ok_SKIP1, ok_SKIP2];
+
+Goal "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute";
+
+Goal "(F ok G) = (G ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_commute";
+
+bind_thm ("ok_sym", ok_commute RS iffD1);
+
+Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
+by (asm_full_simp_tac
+ (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def,
+ OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);
+by (Blast_tac 1);
+qed "ok_iff_OK";
+
+Goal "F ok (G Join H) = (F ok G & F ok H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff1";
+
+Goal "(G Join H) ok F = (G ok F & H ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff2";
+AddIffs [ok_Join_iff1, ok_Join_iff2];
+
+(*useful? Not with the previous two around*)
+Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute_I";
+
+Goal "F ok (JOIN I G) = (ALL i:I. F ok G i)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_JN_iff1";
+
+Goal "(JOIN I G) ok F = (ALL i:I. G i ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_JN_iff2";
+AddIffs [ok_JN_iff1, ok_JN_iff2];
+
+Goal "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))";
+by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));
+qed "OK_iff_ok";
+
+Goal "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)";
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));
+qed "OK_imp_ok";
+
+
+(*** Allowed ***)
+
+Goal "Allowed SKIP = UNIV";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+qed "Allowed_SKIP";
+
+Goal "Allowed (F Join G) = Allowed F Int Allowed G";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+qed "Allowed_Join";
+
+Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+qed "Allowed_JN";
+
+Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
+
+Goal "F ok G = (F : Allowed G & G : Allowed F)";
+by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
+qed "ok_iff_Allowed";
+
+Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))";
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));
+qed "OK_iff_Allowed";
+
+(*** safety_prop, for reasoning about given instances of "ok" ***)
+
+Goal "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+qed "safety_prop_Acts_iff";
+
+Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym]));
+qed "safety_prop_AllowedActs_iff_Allowed";
+
+Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X";
+by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1);
+qed "Allowed_eq";
+
+Goal "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] \
+\ ==> Allowed F = X";
+by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1);
+qed "def_prg_Allowed";
+
+(*For safety_prop to hold, the property must be satisfiable!*)
+Goal "safety_prop (A co B) = (A <= B)";
+by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "safety_prop_constrains";
+AddIffs [safety_prop_constrains];
+
+Goal "safety_prop (stable A)";
+by (simp_tac (simpset() addsimps [stable_def]) 1);
+qed "safety_prop_stable";
+AddIffs [safety_prop_stable];
+
+Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)";
+by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1);
+by (Blast_tac 1);
+qed "safety_prop_Int";
+Addsimps [safety_prop_Int];
+
+Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+by (Blast_tac 1);
+bind_thm ("safety_prop_INTER1", allI RS result());
+Addsimps [safety_prop_INTER1];
+
+Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+by (Blast_tac 1);
+bind_thm ("safety_prop_INTER", ballI RS result());
+Addsimps [safety_prop_INTER];
+
+Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \
+\ ==> F ok G = (G : X & acts <= AllowedActs G)";
+by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff]));
+qed "def_UNION_ok_iff";
--- a/src/HOL/UNITY/Union.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Union.thy Sat Sep 23 16:02:01 2000 +0200
@@ -11,14 +11,30 @@
Union = SubstAx + FP +
constdefs
+
+ (*FIXME: conjoin Init F Int Init G ~= {} *)
+ ok :: ['a program, 'a program] => bool (infixl 65)
+ "F ok G == Acts F <= AllowedActs G &
+ Acts G <= AllowedActs F"
+
+ (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *)
+ OK :: ['a set, 'a => 'b program] => bool
+ "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
+
JOIN :: ['a set, 'a => 'b program] => 'b program
- "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
+ "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
+ INT i:I. AllowedActs (F i))"
Join :: ['a program, 'a program] => 'a program (infixl 65)
- "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
+ "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
+ AllowedActs F Int AllowedActs G)"
SKIP :: 'a program
- "SKIP == mk_program (UNIV, {})"
+ "SKIP == mk_program (UNIV, {}, UNIV)"
+
+ (*Characterizes safety properties. Used with specifying AllowedActs*)
+ safety_prop :: "'a program set => bool"
+ "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
syntax
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)
--- a/src/HOL/UNITY/WFair.ML Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/WFair.ML Sat Sep 23 16:02:01 2000 +0200
@@ -237,7 +237,7 @@
qed "leadsTo_weaken";
-(*Set difference: maybe combine with leadsTo_weaken_L??*)
+(*Set difference: maybe combine with leadsTo_weaken_L?*)
Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
qed "leadsTo_Diff";
@@ -373,7 +373,7 @@
val lemma = result();
-(** Meta or object quantifier ????? **)
+(** Meta or object quantifier ? **)
Goal "[| wf r; \
\ ALL m. F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \