--- a/src/HOL/UNITY/Alloc.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Mon Oct 11 10:53:39 1999 +0200
@@ -71,6 +71,16 @@
qed "inv_sysOfAlloc_eq";
Addsimps [inv_sysOfAlloc_eq];
+
+(*SHOULD NOT BE NECESSARY????????????????
+Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \
+\ allocRel = allocRel z |) = z";
+by (auto_tac (claset() addSWrapper record_split_wrapper,
+ simpset()));
+qed "allocState_eq";
+Addsimps [allocState_eq];
+????*)
+
(**SHOULD NOT BE NECESSARY: The various injections into the system
state need to be treated symmetrically or done automatically*)
Goalw [sysOfClient_def] "inj sysOfClient";
@@ -183,15 +193,14 @@
AddIffs [Network_component_System, Alloc_component_System];
-fun alloc_export th = good_map_sysOfAlloc RS export th;
+fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
-fun client_export th = good_map_sysOfClient RS export th;
+fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
(* F : UNIV guarantees Increasing func
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
val extend_Client_guar_Increasing =
- client_export extend_guar_Increasing
- |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
+ client_export extend_guar_Increasing;
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
Goal "i < Nclients \
@@ -221,6 +230,8 @@
System_Increasing_rel]) 1);
qed "System_Increasing_allocRel";
+
+
(*safety (1), step 3*)
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
@@ -230,14 +241,14 @@
by (rtac Alloc_component_System 3);
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
by (rtac (Alloc_Safety RS project_guarantees) 1);
+(*1: Increasing precondition*)
+br (ballI RS projecting_INT) 1;
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken) 1);
by Auto_tac;
-(*1: Increasing precondition*)
-by (stac (alloc_export project_Increasing) 1);
-by (force_tac
- (claset(),
- simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
(*2: Always postcondition*)
-by (dtac (subset_refl RS alloc_export project_Always_D) 1);
+by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
+by Auto_tac;
by (asm_full_simp_tac
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
qed "System_sum_bounded";
--- a/src/HOL/UNITY/Client.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Mon Oct 11 10:53:39 1999 +0200
@@ -114,6 +114,7 @@
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
addIs [Increasing_localTo_Stable,
stable_size_rel_le_giv]) 2);
+by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
addIs [stable_localTo_stable2 RS stable_imp_Stable,
stable_size_ask_le_rel]) 1);
@@ -133,7 +134,7 @@
simpset()) 1);
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
by (Blast_tac 1);
-by (auto_tac (claset(),
- simpset() addsimps [Always_eq_includes_reachable, giv_meets_ask_def]));
-by (ALLGOALS Force_tac);
+by (force_tac (claset(),
+ simpset() addsimps [Always_eq_includes_reachable,
+ giv_meets_ask_def]) 1);
qed "client_correct";
--- a/src/HOL/UNITY/Common.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Common.ML Mon Oct 11 10:53:39 1999 +0200
@@ -40,7 +40,6 @@
\ : {m} co (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
le_max_iff_disj, fasc]) 1);
-by (Blast_tac 1);
result();
(*This one is t := max (ftime t) (gtime t)*)
@@ -48,7 +47,6 @@
\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
-by (Blast_tac 1);
result();
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
@@ -56,7 +54,6 @@
\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
-by (blast_tac (claset() addIs [Suc_leI]) 1);
result();
--- a/src/HOL/UNITY/Extend.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Mon Oct 11 10:53:39 1999 +0200
@@ -70,12 +70,17 @@
by (Blast_tac 1);
qed "extend_set_mono";
-Goalw [extend_set_def]
- "z : extend_set h A = (f z : A)";
+Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);
qed "mem_extend_set_iff";
AddIffs [mem_extend_set_iff];
+Goalw [extend_set_def]
+ "(extend_set h A <= extend_set h B) = (A <= B)";
+by (Force_tac 1);
+qed "extend_set_strict_mono";
+AddIffs [extend_set_strict_mono];
+
Goal "{s. P (f s)} = extend_set h {s. P s}";
by Auto_tac;
qed "Collect_eq_extend_set";
@@ -177,6 +182,12 @@
qed "extend_act_inverse";
Addsimps [extend_act_inverse];
+(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
+Goalw [extend_act_def, project_act_def]
+ "act' <= extend_act h act ==> project_act C h act' <= act";
+by (Force_tac 1);
+qed "subset_extend_act_D";
+
Goal "inj (extend_act h)";
by (rtac inj_on_inverseI 1);
by (rtac extend_act_inverse 1);
@@ -189,11 +200,12 @@
qed "extend_act_Image";
Addsimps [extend_act_Image];
-Goalw [extend_set_def, extend_act_def]
- "(extend_set h A <= extend_set h B) = (A <= B)";
-by (Force_tac 1);
-qed "extend_set_strict_mono";
-Addsimps [extend_set_strict_mono];
+Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)";
+by Auto_tac;
+qed "extend_act_strict_mono";
+
+AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq];
+(*The latter theorem is (extend_act h act' = extend_act h act) = (act'=act) *)
Goalw [extend_set_def, extend_act_def]
"Domain (extend_act h act) = extend_set h (Domain act)";
@@ -226,6 +238,12 @@
Addsimps [extend_act_Id, project_act_Id];
+Goal "(extend_act h act = Id) = (act = Id)";
+by Auto_tac;
+by (rewtac extend_act_def);
+by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
+qed "extend_act_Id_iff";
+
Goal "Id : extend_act h `` Acts F";
by (auto_tac (claset() addSIs [extend_act_Id RS sym],
simpset() addsimps [image_iff]));
@@ -326,26 +344,56 @@
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
qed "extend_invariant";
+(*Converse fails: A and B may differ in their extra variables*)
+Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
+by (auto_tac (claset(),
+ simpset() addsimps [constrains_def, project_set_def]));
+by (Force_tac 1);
+qed "extend_constrains_project_set";
+
(*** Diff, needed for localTo ***)
Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
by (auto_tac (claset() addSIs [program_equalityI],
simpset() addsimps [Diff_def,
- inj_extend_act RS image_set_diff RS sym]));
+ inj_extend_act RS image_set_diff]));
qed "Diff_extend_eq";
Goal "(Diff (extend h G) (extend_act h `` acts) \
\ : (extend_set h A) co (extend_set h B)) \
\ = (Diff G acts : A co B)";
by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
-qed "Diff_extend_co";
+qed "Diff_extend_constrains";
Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
\ = (Diff G acts : stable A)";
-by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1);
+by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
qed "Diff_extend_stable";
+Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
+\ ==> Diff G acts : (project_set h A) co (project_set h B)";
+by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq,
+ extend_constrains_project_set]) 1);
+qed "Diff_extend_constrains_project_set";
+
+Goalw [localTo_def]
+ "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
+by (simp_tac (simpset() addsimps []) 1);
+(*A trick to strip both quantifiers*)
+by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
+by (stac Collect_eq_extend_set 1);
+by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
+qed "extend_localTo_extend_eq";
+
+Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
+by (simp_tac (simpset() addsimps [Disjoint_def,
+ inj_extend_act RS image_Int RS sym]) 1);
+by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "Disjoint_extend_eq";
+Addsimps [Disjoint_extend_eq];
+
(*** Weak safety primitives: Co, Stable ***)
Goal "p : reachable (extend h F) ==> f p : reachable F";
--- a/src/HOL/UNITY/Extend.thy Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Mon Oct 11 10:53:39 1999 +0200
@@ -23,7 +23,7 @@
"project_set h C == {x. EX y. h(x,y) : C}"
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
- "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
+ "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
(*Argument C allows weak safety laws to be projected*)
project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
--- a/src/HOL/UNITY/Lift_prog.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Mon Oct 11 10:53:39 1999 +0200
@@ -3,13 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-THESE PROOFS CAN BE REPLACED BY INVOCATIONS OF RESULTS FROM EXTEND.ML
+Arrays of processes. Many results are instances of those in Extend & Project.
*)
-val image_eqI' = read_instantiate_sg (sign_of thy)
- [("x", "?ff(i := ?u)")] image_eqI;
-
(*** Basic properties ***)
(** lift_set and drop_set **)
@@ -283,6 +280,13 @@
simpset() addsimps [invariant_def, lift_prog_stable]));
qed "lift_prog_invariant";
+Goal "[| lift_prog i F : A co B |] \
+\ ==> F : (drop_set i A) co (drop_set i B)";
+by (asm_full_simp_tac
+ (simpset() addsimps [drop_set_correct, lift_prog_correct,
+ lift_export extend_constrains_project_set]) 1);
+qed "lift_prog_constrains_drop_set";
+
(*This one looks strange! Proof probably is by case analysis on i=j.
If i~=j then lift_prog j (F j) does nothing to lift_set i, and the
premise ensures A<=B.*)
@@ -316,14 +320,14 @@
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, drop_prog_correct,
lift_set_correct, lift_act_correct,
- lift_export Diff_project_co]) 1);
-qed "Diff_drop_prog_co";
+ lift_export Diff_project_constrains]) 1);
+qed "Diff_drop_prog_constrains";
Goalw [stable_def]
"[| (UN act:acts. Domain act) <= drop_set i C; \
\ Diff G (lift_act i `` acts) : stable (lift_set i A) |] \
\ ==> Diff (drop_prog C i G) acts : stable A";
-by (etac Diff_drop_prog_co 1);
+by (etac Diff_drop_prog_constrains 1);
by (assume_tac 1);
qed "Diff_drop_prog_stable";
@@ -487,11 +491,3 @@
(simpset() addsimps [lift_set_correct, lift_prog_correct,
lift_export extend_guar_Always]) 1);
qed "lift_prog_guar_Always";
-
-(*No analogue of this in Extend.ML!*)
-Goal "[| lift_prog i F : A co B |] \
-\ ==> F : (drop_set i A) co (drop_set i B)";
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def, drop_set_def]));
-by (force_tac (claset() addSIs [image_eqI'], simpset()) 1);
-qed "lift_prog_constrains_drop_set";
--- a/src/HOL/UNITY/PPROD.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Mon Oct 11 10:53:39 1999 +0200
@@ -6,10 +6,13 @@
Abstraction over replicated components (PLam)
General products of programs (Pi operation)
-It is not clear that any of this is good for anything.
+Probably some dead wood here!
*)
+val image_eqI' = read_instantiate_sg (sign_of thy)
+ [("x", "?ff(i := ?u)")] image_eqI;
+
(*** Basic properties ***)
Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
--- a/src/HOL/UNITY/Project.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Project.ML Mon Oct 11 10:53:39 1999 +0200
@@ -108,13 +108,95 @@
(*For using project_guarantees in particular cases*)
Goal "extend h F Join G : extend_set h A co extend_set h B \
-\ ==> F Join project UNIV h G : A co B";
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
+\ ==> F Join project C h G : A co B";
+by (asm_full_simp_tac
+ (simpset() addsimps [project_constrains, Join_constrains,
+ extend_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_weaken]
+ addDs [constrains_imp_subset]) 1);
+qed "project_constrains_I";
+
+(*The UNIV argument is essential*)
+Goal "F Join project UNIV h G : A co B \
+\ ==> extend h F Join G : extend_set h A co extend_set h B";
by (asm_full_simp_tac
(simpset() addsimps [project_constrains, Join_constrains,
extend_constrains]) 1);
-by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
-qed "project_constrains_I";
+qed "project_constrains_D";
+
+Goalw [projecting_def]
+ "[| ALL i:I. projecting C h F (X' i) (X i) |] \
+\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
+by Auto_tac;
+qed "projecting_INT";
+
+Goalw [projecting_def]
+ "[| ALL i:I. projecting C h F (X' i) (X i) |] \
+\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
+by Auto_tac;
+qed "projecting_UN";
+
+Goalw [projecting_def]
+ "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U";
+by Auto_tac;
+qed "projecting_weaken";
+
+(*Is this the right way to handle the X' argument?*)
+Goalw [extending_def]
+ "[| ALL i:I. extending C h F (X' i) (Y' i) (Y i) |] \
+\ ==> extending C h F (INT i:I. X' i) (INT i:I. Y' i) (INT i:I. Y i)";
+by Auto_tac;
+qed "extending_INT";
+
+Goalw [extending_def]
+ "[| ALL i:I. extending C h F X' (Y' i) (Y i) |] \
+\ ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
+by Auto_tac;
+qed "extending_UN";
+
+Goalw [extending_def]
+ "[| extending C h F X' Y' Y; U'<= X'; Y'<=V'; V<=Y |] \
+\ ==> extending C h F U' V' V";
+by Auto_tac;
+qed "extending_weaken";
+
+Goal "projecting C h F X' UNIV";
+by (simp_tac (simpset() addsimps [projecting_def]) 1);
+qed "projecting_UNIV";
+
+Goalw [projecting_def]
+ "projecting C h F (extend_set h A co extend_set h B) (A co B)";
+by (blast_tac (claset() addIs [project_constrains_I]) 1);
+qed "projecting_constrains";
+
+Goalw [stable_def]
+ "projecting C h F (stable (extend_set h A)) (stable A)";
+by (rtac projecting_constrains 1);
+qed "projecting_stable";
+
+Goalw [projecting_def]
+ "projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)";
+by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+qed "projecting_increasing";
+
+Goal "extending C h F X' UNIV Y";
+by (simp_tac (simpset() addsimps [extending_def]) 1);
+qed "extending_UNIV";
+
+Goalw [extending_def]
+ "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
+by (blast_tac (claset() addIs [project_constrains_D]) 1);
+qed "extending_constrains";
+
+Goalw [stable_def]
+ "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
+by (rtac extending_constrains 1);
+qed "extending_stable";
+
+Goalw [extending_def]
+ "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
+by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+qed "extending_increasing";
(*** Diff, needed for localTo ***)
@@ -139,17 +221,19 @@
by (ftac constrains_imp_subset 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "Diff_project_co";
+qed "Diff_project_constrains";
Goalw [stable_def]
"[| (UN act:acts. Domain act) <= project_set h C; \
\ Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
\ ==> Diff (project C h G) acts : stable A";
-by (etac Diff_project_co 1);
+by (etac Diff_project_constrains 1);
by (assume_tac 1);
qed "Diff_project_stable";
-(*Converse appears to fail*)
+(*Converse fails: even if the conclusion holds, H could modify (v o f)
+ simultaneously with other variables, and this action would not be
+ superseded by anything in (extend h G) *)
Goal "[| UNIV <= project_set h C; H : (func o f) localTo extend h G |] \
\ ==> project C h H : func localTo G";
by (asm_full_simp_tac
@@ -166,6 +250,11 @@
(simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
qed "project_localTo_I";
+Goalw [projecting_def]
+ "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
+by (blast_tac (claset() addIs [project_localTo_I]) 1);
+qed "projecting_localTo";
+
(** Reachability and project **)
@@ -243,7 +332,7 @@
simpset() addsimps [project_set_def]));
qed "project_set_reachable_extend_eq";
-
+(*Perhaps should replace C by reachable...*)
Goalw [Constrains_def]
"[| C <= reachable (extend h F Join G); \
\ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
@@ -274,7 +363,7 @@
\ extend h F Join G : Always (extend_set h A) |] \
\ ==> F Join project C h G : Always A";
by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
-bws [project_set_def, extend_set_def];
+by (rewrite_goals_tac [project_set_def, extend_set_def]);
by (Blast_tac 1);
qed "project_Always_I";
@@ -305,6 +394,59 @@
Collect_eq_extend_set RS sym]) 1);
qed "project_Increasing";
+(** A lot of redundant theorems: all are proved to facilitate reasoning
+ about guarantees. **)
+
+Goalw [projecting_def]
+ "projecting (%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_I]) 1);
+qed "projecting_Constrains";
+
+Goalw [Stable_def]
+ "projecting (%G. reachable (extend h F Join G)) h F \
+\ (Stable (extend_set h A)) (Stable A)";
+by (rtac projecting_Constrains 1);
+qed "projecting_Stable";
+
+Goalw [projecting_def]
+ "projecting (%G. reachable (extend h F Join G)) h F \
+\ (Always (extend_set h A)) (Always A)";
+by (blast_tac (claset() addIs [project_Always_I]) 1);
+qed "projecting_Always";
+
+Goalw [projecting_def]
+ "projecting (%G. reachable (extend h F Join G)) h F \
+\ (Increasing (func o f)) (Increasing func)";
+by (blast_tac (claset() addIs [project_Increasing_I]) 1);
+qed "projecting_Increasing";
+
+Goalw [extending_def]
+ "extending (%G. reachable (extend h F Join G)) h F X' \
+\ (extend_set h A Co extend_set h B) (A Co B)";
+by (blast_tac (claset() addIs [project_Constrains_D]) 1);
+qed "extending_Constrains";
+
+Goalw [extending_def]
+ "extending (%G. reachable (extend h F Join G)) h F X' \
+\ (Stable (extend_set h A)) (Stable A)";
+by (blast_tac (claset() addIs [project_Stable_D]) 1);
+qed "extending_Stable";
+
+Goalw [extending_def]
+ "extending (%G. reachable (extend h F Join G)) h F X' \
+\ (Always (extend_set h A)) (Always A)";
+by (blast_tac (claset() addIs [project_Always_D]) 1);
+qed "extending_Always";
+
+val [prem] =
+Goalw [extending_def]
+ "(!!G. reachable (extend h F Join G) <= C G) \
+\ ==> extending C h F X' \
+\ (Increasing (func o f)) (Increasing func)";
+by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
+qed "extending_Increasing";
+
(** Progress includes safety in the definition of ensures **)
@@ -369,9 +511,8 @@
by (Blast_tac 1);
qed "ensures_extend_set_imp_project_ensures";
-(*A super-strong condition: G is not allowed to affect the
- shared variables at all.*)
-Goal "[| ALL x. project C h G ~: transient {x}; \
+(*A strong condition: F can do anything that project G can.*)
+Goal "[| ALL D. project C h G : transient D --> F : transient D; \
\ extend h F Join G : stable C; \
\ F Join project C h G : A ensures B |] \
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
@@ -387,7 +528,7 @@
simpset()) 1));
qed_spec_mp "Join_project_ensures";
-Goal "[| ALL x. project C h G ~: transient {x}; \
+Goal "[| ALL D. project C h G : transient D --> F : transient D; \
\ extend h F Join G : stable C; \
\ F Join project C h G : A leadsTo B |] \
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
@@ -400,7 +541,7 @@
qed "project_leadsTo_lemma";
(*Instance of the previous theorem for STRONG progress*)
-Goal "[| ALL x. project UNIV h G ~: transient {x}; \
+Goal "[| ALL D. project UNIV h G : transient D --> F : transient D; \
\ F Join project UNIV h G : A leadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
by (dtac project_leadsTo_lemma 1);
@@ -409,7 +550,7 @@
(** Towards the analogous theorem for WEAK progress*)
-Goal "[| ALL x. project C h G ~: transient {x}; \
+Goal "[| ALL D. project C h G : transient D --> F : transient D; \
\ extend h F Join G : stable C; \
\ F Join project C h G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
@@ -421,7 +562,7 @@
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
val lemma = result();
-Goal "[| ALL x. project C h G ~: transient {x}; \
+Goal "[| ALL D. project C h G : transient D --> F : transient D; \
\ extend h F Join G : stable C; \
\ F Join project C h G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
@@ -430,7 +571,7 @@
val lemma2 = result();
Goal "[| C = (reachable (extend h F Join G)); \
-\ ALL x. project C h G ~: transient {x}; \
+\ ALL D. project C h G : transient D --> F : transient D; \
\ F Join project C h G : A LeadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (asm_full_simp_tac
@@ -453,13 +594,11 @@
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
\ ==> F : X guarantees Y";
-by (rtac guaranteesI 1);
-by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
-by (dtac spec 1);
-by (dtac (mp RS mp) 1);
-by (Blast_tac 2);
-by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
+by (dres_inst_tac [("x", "extend h G")] spec 1);
+by (asm_full_simp_tac
+ (simpset() delsimps [extend_Join]
+ addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
qed "extend_guarantees_imp_guarantees";
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
@@ -471,17 +610,12 @@
(*Weak precondition and postcondition; this is the good one!
Not clear that it has a converse [or that we want one!]*)
-val [xguary,project,extend] =
Goal "[| F : X guarantees Y; \
-\ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \
-\ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
-\ Disjoint (extend h F) G |] \
-\ ==> extend h F Join G : Y' |] \
+\ projecting C h F X' X; extending C h F X' Y' Y |] \
\ ==> extend h F : X' guarantees Y'";
-by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
-by (etac project 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (rtac guaranteesI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [guaranteesD, projecting_def, extending_def]));
qed "project_guarantees";
(** It seems that neither "guarantees" law can be proved from the other. **)
@@ -489,17 +623,20 @@
(*** guarantees corollaries ***)
+(** Most could be deleted: the required versions are easy to prove **)
+
Goal "F : UNIV guarantees increasing func \
-\ ==> extend h F : UNIV guarantees increasing (func o f)";
+\ ==> extend h F : X' guarantees increasing (func o f)";
by (etac project_guarantees 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
+by (rtac extending_increasing 2);
+by (rtac projecting_UNIV 1);
qed "extend_guar_increasing";
Goal "F : UNIV guarantees Increasing func \
-\ ==> extend h F : UNIV guarantees Increasing (func o f)";
+\ ==> extend h F : X' guarantees Increasing (func o f)";
by (etac project_guarantees 1);
-by (rtac (subset_UNIV RS project_Increasing_D) 2);
+by (rtac extending_Increasing 2);
+by (rtac projecting_UNIV 1);
by Auto_tac;
qed "extend_guar_Increasing";
@@ -507,30 +644,42 @@
\ ==> extend h F : (v o f) localTo (extend h G) \
\ guarantees increasing (func o f)";
by (etac project_guarantees 1);
-(*the "increasing" guarantee*)
-by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
-by (etac project_localTo_I 1);
+by (rtac extending_increasing 2);
+by (rtac projecting_localTo 1);
qed "extend_localTo_guar_increasing";
Goal "F : (v localTo G) guarantees Increasing func \
\ ==> extend h F : (v o f) localTo (extend h G) \
\ guarantees Increasing (func o f)";
by (etac project_guarantees 1);
-(*the "Increasing" guarantee*)
-by (etac (subset_UNIV RS project_Increasing_D) 2);
-by (etac project_localTo_I 1);
+by (rtac extending_Increasing 2);
+by (rtac projecting_localTo 1);
+by Auto_tac;
qed "extend_localTo_guar_Increasing";
Goal "F : Always A guarantees Always B \
\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
by (etac project_guarantees 1);
-by (etac (subset_refl RS project_Always_D) 2);
-by (etac (subset_refl RS project_Always_I) 1);
+by (rtac extending_Always 2);
+by (rtac projecting_Always 1);
qed "extend_guar_Always";
(** Guarantees with a leadsTo postcondition **)
+(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
+Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
+\ ==> F : transient D";
+by (case_tac "D={}" 1);
+by (auto_tac (claset() addIs [transient_strengthen], simpset()));
+qed "transient_lemma";
+
+
+(*Previously tried to prove
+[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
+but it can fail if C removes some parts of an action of G.*)
+
+
Goal "[| G : f localTo extend h F; \
\ Disjoint (extend h F) G |] ==> project C h G : stable {x}";
by (asm_full_simp_tac
@@ -544,31 +693,50 @@
stable_def, constrains_def]));
qed "stable_sing_imp_not_transient";
+by (auto_tac (claset(),
+ simpset() addsimps [FP_def, transient_def,
+ stable_def, constrains_def]));
+qed "stable_sing_imp_not_transient";
+
Goal "[| F Join project UNIV h G : A leadsTo B; \
-\ extend h F Join G : f localTo extend h F; \
+\ G : f localTo extend h F; \
\ Disjoint (extend h F) G |] \
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
by (rtac project_UNIV_leadsTo_lemma 1);
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [Join_localTo, self_localTo,
- localTo_imp_project_stable,
- stable_sing_imp_not_transient]) 1);
+by (Clarify_tac 1);
+by (rtac transient_lemma 1);
+by (auto_tac (claset(),
+ simpset() addsimps [localTo_imp_project_stable,
+ stable_sing_imp_not_transient]));
qed "project_leadsTo_D";
-
Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
-\ extend h F Join G : f localTo extend h F; \
-\ Disjoint (extend h F) G |] \
+\ G : f localTo extend h F; \
+\ Disjoint (extend h F) G |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
-by (rtac Join_project_LeadsTo 1);
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [Join_localTo, self_localTo,
- localTo_imp_project_stable,
- stable_sing_imp_not_transient]) 1);
+by (rtac (refl RS Join_project_LeadsTo) 1);
+by (Clarify_tac 1);
+by (rtac transient_lemma 1);
+by (auto_tac (claset(),
+ simpset() addsimps [localTo_imp_project_stable,
+ stable_sing_imp_not_transient]));
qed "project_LeadsTo_D";
+Goalw [extending_def]
+ "extending (%G. UNIV) h F \
+\ (f localTo extend h F) \
+\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
+by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
+ addIs [project_leadsTo_D]) 1);
+qed "extending_leadsTo";
+
+Goalw [extending_def]
+ "extending (%G. reachable (extend h F Join G)) h F \
+\ (f localTo extend h F) \
+\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
+by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
+ addIs [project_LeadsTo_D]) 1);
+qed "extending_LeadsTo";
(*STRONG precondition and postcondition*)
Goal "F : (A co A') guarantees (B leadsTo B') \
@@ -576,10 +744,9 @@
\ Int (f localTo (extend h F)) \
\ guarantees ((extend_set h B) leadsTo (extend_set h B'))";
by (etac project_guarantees 1);
-(*the safety precondition*)
-by (fast_tac (claset() addIs [project_constrains_I]) 1);
-(*the liveness postcondition*)
-by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
+by (rtac (extending_leadsTo RS extending_weaken) 2);
+by (rtac (projecting_constrains RS projecting_weaken) 1);
+by Auto_tac;
qed "extend_co_guar_leadsTo";
(*WEAK precondition and postcondition*)
@@ -588,10 +755,9 @@
\ Int (f localTo (extend h F)) \
\ guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
by (etac project_guarantees 1);
-(*the safety precondition*)
-by (fast_tac (claset() addIs [project_Constrains_I]) 1);
-(*the liveness postcondition*)
-by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
+by (rtac (extending_LeadsTo RS extending_weaken) 2);
+by (rtac (projecting_Constrains RS projecting_weaken) 1);
+by Auto_tac;
qed "extend_Co_guar_LeadsTo";
Close_locale "Extend";
--- a/src/HOL/UNITY/Project.thy Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Project.thy Mon Oct 11 10:53:39 1999 +0200
@@ -8,4 +8,19 @@
Inheritance of GUARANTEES properties under extension
*)
-Project = Extend
+Project = Extend +
+
+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 (C G) h G : X"
+
+ extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
+ 'c program set, 'c program set, 'a program set] => bool"
+ "extending C h F X' Y' Y ==
+ ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
+ Disjoint (extend h F) G
+ --> extend h F Join G : Y'"
+
+end
--- a/src/HOL/UNITY/UNITY.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML Mon Oct 11 10:53:39 1999 +0200
@@ -133,10 +133,20 @@
by (Blast_tac 1);
qed "constrains_empty";
+Goalw [constrains_def] "(F : A co {}) = (A={})";
+by (Blast_tac 1);
+qed "constrains_empty2";
+
+Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)";
+by (Blast_tac 1);
+qed "constrains_UNIV";
+
Goalw [constrains_def] "F : A co UNIV";
by (Blast_tac 1);
-qed "constrains_UNIV";
-AddIffs [constrains_empty, constrains_UNIV];
+qed "constrains_UNIV2";
+
+AddIffs [constrains_empty, constrains_empty2,
+ constrains_UNIV, constrains_UNIV2];
(*monotonic in 2nd argument*)
Goalw [constrains_def]
@@ -167,6 +177,22 @@
by (Blast_tac 1);
qed "ball_constrains_UN";
+Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)";
+by (Blast_tac 1);
+qed "constrains_Un_distrib";
+
+Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)";
+by (Blast_tac 1);
+qed "constrains_UN_distrib";
+
+Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)";
+by (Blast_tac 1);
+qed "constrains_Int_distrib";
+
+Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)";
+by (Blast_tac 1);
+qed "constrains_INT_distrib";
+
(** Intersection **)
Goalw [constrains_def]
--- a/src/HOL/UNITY/Union.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Mon Oct 11 10:53:39 1999 +0200
@@ -307,22 +307,13 @@
by Auto_tac;
qed "Diff_Disjoint";
-Goal "[| G : v localTo F; Disjoint F G |] \
-\ ==> G : stable {s. v s = z}";
+Goal "[| G : v localTo F; Disjoint F G |] ==> G : stable {s. v s = z}";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
stable_def, constrains_def]) 1);
by (Blast_tac 1);
qed "localTo_imp_stable";
-Goal "[| F Join G : v localTo F; (s,s') : act; \
-\ act : Acts G; Disjoint F G |] ==> v s' = v s";
-by (asm_full_simp_tac
- (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
- stable_def, constrains_def]) 1);
-by (Blast_tac 1);
-qed "localTo_imp_equals";
-
Goalw [localTo_def, stable_def, constrains_def]
"v localTo F <= (f o v) localTo F";
by (Clarify_tac 1);
@@ -350,46 +341,62 @@
(*** Higher-level rules involving localTo and Join ***)
+Goal "[| F : {s. P (v s)} co {s. P' (v s)}; G : v localTo F |] \
+\ ==> F Join G : {s. P (v s)} co {s. P' (v s)}";
+by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [localTo_def, stable_def, constrains_def,
+ Diff_def]));
+by (case_tac "act: Acts F" 1);
+by (Blast_tac 1);
+by (dtac bspec 1 THEN rtac Id_in_Acts 1);
+by (subgoal_tac "v x = v xa" 1);
+by Auto_tac;
+qed "constrains_localTo_constrains";
+
+Goalw [localTo_def, stable_def, constrains_def, Diff_def]
+ "[| G : v localTo F; G : w localTo F |] \
+\ ==> G : (%s. (v s, w s)) localTo F";
+by (Blast_tac 1);
+qed "localTo_pairfun";
+
Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)}; \
-\ F Join G : v localTo F; \
-\ F Join G : w localTo F; \
-\ Disjoint F G |] \
+\ G : v localTo F; \
+\ G : w localTo F |] \
\ ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
+by (res_inst_tac [("A", "{s. (%(x,y). P x y) (v s, w s)}"),
+ ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")]
+ constrains_weaken 1);
+by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
by Auto_tac;
qed "constrains_localTo_constrains2";
Goalw [stable_def]
"[| F : stable {s. P (v s) (w s)}; \
-\ F Join G : v localTo F; \
-\ F Join G : w localTo F; \
-\ Disjoint F G |] \
+\ G : v localTo F; G : w localTo F |] \
\ ==> F Join G : stable {s. P (v s) (w s)}";
by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
qed "stable_localTo_stable2";
-
-Goal "(UN k. {s. f s = k}) = UNIV";
-by (Blast_tac 1);
-qed "UN_eq_UNIV";
-
Goal "[| F : stable {s. v s <= w s}; \
\ G : v localTo F; \
-\ F Join G : Increasing w; \
-\ Disjoint F G |] \
+\ F Join G : Increasing w |] \
\ ==> F Join G : Stable {s. v s <= w s}";
-by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
-by (subgoal_tac "ALL k: UNIV. ?H : ({s. v s = k} Int ?AA) Co ?AA" 1);
-by (dtac ball_Constrains_UN 1);
-by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
-by (rtac ballI 1);
-by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
-\ ({s. v s = k} Un {s. v s <= w s})" 1);
-by (asm_simp_tac (simpset() addsimps [Join_constrains]) 2);
-by (fast_tac (claset() addIs [constrains_weaken]
- addEs [localTo_imp_stable RS stableD RS constrains_weaken]) 2);
-by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
-by (etac Constrains_weaken 2);
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def, Stable_def, Increasing_def,
+ Constrains_def, Join_constrains, all_conj_distrib]));
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+(*The G case remains; proved like constrains_localTo_constrains*)
+by (auto_tac (claset(),
+ simpset() addsimps [localTo_def, stable_def, constrains_def,
+ Diff_def]));
+by (case_tac "act: Acts F" 1);
+by (Blast_tac 1);
+by (thin_tac "ALL act:Acts F. ?P act" 1);
+by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
+by (dres_inst_tac [("x", "v xa")] spec 1 THEN dtac bspec 1 THEN rtac DiffI 1);
+by (assume_tac 1);
+by (Blast_tac 1);
+by (subgoal_tac "v x = v xa" 1);
by Auto_tac;
qed "Increasing_localTo_Stable";
--- a/src/HOL/UNITY/Union.thy Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Union.thy Mon Oct 11 10:53:39 1999 +0200
@@ -29,7 +29,8 @@
localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
"v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
- (*Two programs with disjoint actions, except for identity actions *)
+ (*Two programs with disjoint actions, except for identity actions.
+ It's a weak property but still useful.*)
Disjoint :: ['a program, 'a program] => bool
"Disjoint F G == Acts F Int Acts G <= {Id}"
--- a/src/HOL/UNITY/WFair.ML Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML Mon Oct 11 10:53:39 1999 +0200
@@ -31,6 +31,15 @@
by (Blast_tac 1);
qed "transient_mem";
+Goalw [transient_def] "transient UNIV = {}";
+by Auto_tac;
+qed "transient_UNIV";
+
+Goalw [transient_def] "transient {} = UNIV";
+by Auto_tac;
+qed "transient_empty";
+Addsimps [transient_UNIV, transient_empty];
+
(*** ensures ***)