# HG changeset patch # User paulson # Date 939632019 -7200 # Node ID c6a8b73b6c2a150a2d35467fd164d2e60886f0a2 # Parent 1be9b63e7d93e70910d56160c5d65ef804f711b9 working shapshot with "projecting" and "extending" diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Alloc.ML --- 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Client.ML --- 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Common.ML --- 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 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Extend.thy --- 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" diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Lift_prog.ML --- 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/PPROD.ML --- 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)))"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Project.ML --- 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Project.thy --- 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 diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/UNITY.ML --- 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] diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Union.ML --- 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"; diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/Union.thy --- 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}" diff -r 1be9b63e7d93 -r c6a8b73b6c2a src/HOL/UNITY/WFair.ML --- 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 ***)