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