--- 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";