# HG changeset patch # User paulson # Date 936107816 -7200 # Node ID cf780c2bcccf3741b21cd99e61298e219cb5bcfc # Parent c68ecbf05eb6e6592e798089991fc85318cd52fc changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Alloc.ML --- a/src/HOL/UNITY/Alloc.ML Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Alloc.ML Tue Aug 31 15:56:56 1999 +0200 @@ -6,6 +6,18 @@ Specification of Chandy and Charpentier's Allocator *) + +Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)"; + +(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) +Goal "[| b:A; a=b |] ==> a:A"; +by (etac ssubst 1); +by (assume_tac 1); +qed "subst_elem"; + + + + (*Generalized version allowing different clients*) Goal "[| Alloc : alloc_spec; \ \ Client : (lessThan Nclients) funcset client_spec; \ @@ -32,6 +44,20 @@ AddIffs [inj_sysOfAlloc, surj_sysOfAlloc]; +val bij_sysOfAlloc = [inj_sysOfAlloc, surj_sysOfAlloc] MRS bijI; + +(*MUST BE AUTOMATED: even the statement of such results*) +Goal "!!s. inv sysOfAlloc s = \ +\ ((| allocGiv = allocGiv s, \ +\ allocAsk = allocAsk s, \ +\ allocRel = allocRel s|), \ +\ client s)"; +by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); +by (auto_tac (claset() addSWrapper record_split_wrapper, + simpset() addsimps [sysOfAlloc_def])); +qed "inv_sysOfAlloc_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"; @@ -49,6 +75,7 @@ AddIffs [inj_sysOfClient, surj_sysOfClient]; +val bij_sysOfClient = [inj_sysOfClient, surj_sysOfClient] MRS bijI; (*MUST BE AUTOMATED: even the statement of such results*) Goal "!!s. inv sysOfClient s = \ @@ -57,8 +84,8 @@ \ allocAsk = allocAsk s, \ \ allocRel = allocRel s|) )"; by (rtac (inj_sysOfClient RS inv_f_eq) 1); -by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]); -by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); +by (auto_tac (claset() addSWrapper record_split_wrapper, + simpset() addsimps [sysOfAlloc_def, sysOfClient_def])); qed "inv_sysOfClient_eq"; @@ -128,20 +155,21 @@ (*Not sure what to say about the other components because they involve extend*) -Goalw [System_def] "Network component System"; +Goalw [System_def] "Network <= System"; by (blast_tac (claset() addIs [componentI]) 1); qed "Network_component_System"; -AddIffs [Network_component_System]; - +Goalw [System_def] "(extend sysOfAlloc Alloc) <= System"; +by (blast_tac (claset() addIs [componentI]) 1); +qed "Alloc_component_System"; -val project_guarantees' = - [surj_sysOfClient, inj_sysOfClient] MRS export project_guarantees; +AddIffs [Network_component_System, Alloc_component_System]; + (* F : UNIV guarantees Increasing func ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *) -val extend_guar_Increasing' = - [surj_sysOfClient, inj_sysOfClient] MRS export extend_guar_Increasing +val extend_Client_guar_Increasing = + bij_sysOfClient RS export extend_guar_Increasing |> simplify (simpset() addsimps [inv_sysOfClient_eq]); @@ -154,7 +182,7 @@ MRS guaranteesD) 1); by (asm_simp_tac (simpset() addsimps [guarantees_PLam_I, - extend_guar_Increasing' RS guaranteesD, + extend_Client_guar_Increasing RS guaranteesD, lift_prog_guar_Increasing]) 1); qed "System_Increasing_rel"; @@ -169,13 +197,81 @@ System_Increasing_rel, Network]) 1); qed "System_Increasing_allocRel"; -Goal "i < Nclients \ -\ ==> System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ -\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; -fr component_guaranteesD; + +(*NEED TO PROVE something like this (maybe without premise)*) +Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network"; -val extend_guar_Increasing'' = - [surj_sysOfAlloc, inj_sysOfAlloc] MRS export extend_guar_Increasing +fun alloc_export th = bij_sysOfAlloc RS export th; + +val extend_Alloc_guar_Increasing = + alloc_export extend_guar_Increasing |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]); +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}"; +by (res_inst_tac + [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \ +\ Int Increasing (sub i o allocRel))")] + component_guaranteesD 1);; +br Alloc_component_System 3; +br project_guarantees 1; +br Alloc_Safety 1; +by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 + THEN + full_simp_tac + (simpset() addsimps [inv_sysOfAlloc_eq, + alloc_export Collect_eq_extend_set RS sym]) 2); +auto(); +by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 3); + +bd bspec 1; +by (Blast_tac 1); + + +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; + + [| i < Nclients; + extend sysOfAlloc Alloc Join G + : (sub i o allocRel) localTo Network & + extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |] + ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel) + + + [| i < Nclients; + H : (sub i o allocRel) localTo Network & + H : Increasing (sub i o allocRel) |] + ==> project sysOfAlloc H : Increasing (sub i o allocRel) + +Open_locale"Extend"; + +Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h 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); +auto(); +br Diff_project_stable 1; +PROBABLY FALSE; + +by (Clarify_tac 1); +by (dres_inst_tac [("x","z")] spec 1); + +br (alloc_export project_Always_D) 2; + +by (rtac (alloc_export extend_Always RS iffD2) 2); + +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; + +br guaranteesI 1; + +by (res_inst_tac + [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] + component_guaranteesD 1);; + + by (rtac (Alloc_Safety RS component_guaranteesD) 1); + + +br (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1; +br Alloc_Safety 1; diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Client.thy --- a/src/HOL/UNITY/Client.thy Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Client.thy Tue Aug 31 15:56:56 1999 +0200 @@ -6,7 +6,7 @@ Distributed Resource Management System: the Client *) -Client = Comp + +Client = Guar + consts Max :: nat (*Maximum number of tokens*) diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Comp.ML --- a/src/HOL/UNITY/Comp.ML Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Comp.ML Tue Aug 31 15:56:56 1999 +0200 @@ -11,7 +11,7 @@ (*** component ***) Goalw [component_def] - "H component F | H component G ==> H component (F Join G)"; + "H <= F | H <= G ==> H <= (F Join G)"; by Auto_tac; by (res_inst_tac [("x", "G Join Ga")] exI 1); by (res_inst_tac [("x", "G Join F")] exI 2); @@ -19,349 +19,61 @@ qed "componentI"; Goalw [component_def] - "(F component G) = (Init G <= Init F & Acts F <= Acts G)"; + "(F <= G) = (Init G <= Init F & Acts F <= Acts G)"; by (force_tac (claset() addSIs [exI, program_equalityI], simpset() addsimps [Acts_Join]) 1); qed "component_eq_subset"; -Goalw [component_def] "SKIP component F"; +Goalw [component_def] "SKIP <= F"; by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); qed "component_SKIP"; -Goalw [component_def] "F component F"; +Goalw [component_def] "F <= (F :: 'a program)"; by (blast_tac (claset() addIs [Join_SKIP_right]) 1); qed "component_refl"; AddIffs [component_SKIP, component_refl]; -Goal "F component SKIP ==> F = SKIP"; +Goal "F <= SKIP ==> F = SKIP"; by (auto_tac (claset() addSIs [program_equalityI], simpset() addsimps [component_eq_subset])); qed "SKIP_minimal"; -Goalw [component_def] "F component (F Join G)"; +Goalw [component_def] "F <= (F Join G)"; by (Blast_tac 1); qed "component_Join1"; -Goalw [component_def] "G component (F Join G)"; +Goalw [component_def] "G <= (F Join G)"; by (simp_tac (simpset() addsimps [Join_commute]) 1); by (Blast_tac 1); qed "component_Join2"; -Goalw [component_def] "i : I ==> (F i) component (JN i:I. (F i))"; +Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))"; by (blast_tac (claset() addIs [JN_absorb]) 1); qed "component_JN"; -Goalw [component_def] "[| F component G; G component H |] ==> F component H"; +Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"; by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); qed "component_trans"; -Goal "[| F component G; G component F |] ==> F=G"; +Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)"; by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); by (blast_tac (claset() addSIs [program_equalityI]) 1); qed "component_antisym"; Goalw [component_def] - "F component H = (EX G. F Join G = H & Disjoint F G)"; + "F <= H = (EX G. F Join G = H & Disjoint F G)"; by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1); qed "component_eq"; -Goal "((F Join G) component H) = (F component H & G component H)"; +Goal "((F Join G) <= H) = (F <= H & G <= H)"; by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1); by (Blast_tac 1); qed "Join_component_iff"; -Goal "[| F component G; G : A co B |] ==> F : A co B"; +Goal "[| F <= G; G : A co B |] ==> F : A co B"; by (auto_tac (claset(), simpset() addsimps [constrains_def, component_eq_subset])); qed "component_constrains"; -(*** existential properties ***) - -Goalw [ex_prop_def] - "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X"; -by (etac finite_induct 1); -by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); -qed_spec_mp "ex1"; - -Goalw [ex_prop_def] - "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X"; -by (Clarify_tac 1); -by (dres_inst_tac [("x", "{F,G}")] spec 1); -by Auto_tac; -qed "ex2"; - -(*Chandy & Sanders take this as a definition*) -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)"; -by (blast_tac (claset() addIs [ex1,ex2]) 1); -qed "ex_prop_finite"; - -(*Their "equivalent definition" given at the end of section 3*) -Goal "ex_prop X = (ALL G. G:X = (ALL H. G component H --> H: X))"; -by Auto_tac; -by (rewrite_goals_tac [ex_prop_def, component_def]); -by (Blast_tac 1); -by Safe_tac; -by (stac Join_commute 2); -by (ALLGOALS Blast_tac); -qed "ex_prop_equiv"; - - -(*** universal properties ***) - -Goalw [uv_prop_def] - "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X"; -by (etac finite_induct 1); -by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); -qed_spec_mp "uv1"; - -Goalw [uv_prop_def] - "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X"; -by (rtac conjI 1); -by (Clarify_tac 2); -by (dres_inst_tac [("x", "{F,G}")] spec 2); -by (dres_inst_tac [("x", "{}")] spec 1); -by Auto_tac; -qed "uv2"; - -(*Chandy & Sanders take this as a definition*) -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)"; -by (blast_tac (claset() addIs [uv1,uv2]) 1); -qed "uv_prop_finite"; - - -(*** guarantees ***) - -val prems = Goal - "(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \ -\ ==> F : X guarantees Y"; -by (simp_tac (simpset() addsimps [guar_def, component_eq]) 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"; -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 component H |] ==> 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 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'"; -by (Blast_tac 1); -qed "guarantees_weaken"; - -Goalw [guar_def] - "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y"; -by (blast_tac (claset() addIs [component_trans]) 1); -qed "guarantees_weaken_prog"; - -Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV"; -by (Blast_tac 1); -qed "subset_imp_guarantees_UNIV"; - -(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) -Goalw [guar_def] "X <= Y ==> F : X guarantees 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)"; -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)"; -by (Blast_tac 1); -qed "guarantees_UN_left"; - -Goalw [guar_def] - "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; -by (Blast_tac 1); -qed "guarantees_Un_left"; - -Goalw [guar_def] - "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"; -by (Blast_tac 1); -qed "guarantees_INT_right"; - -Goalw [guar_def] - "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; -by (Blast_tac 1); -qed "guarantees_Int_right"; - -Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; -by (Blast_tac 1); -qed "shunting"; - -Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X"; -by (Blast_tac 1); -qed "contrapositive"; - -(** The following two can be expressed using intersection and subset, which - is more faithful to the text but looks cryptic. -**) - -Goalw [guar_def] - "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ -\ ==> F : (V Int Y) guarantees Z"; -by (Blast_tac 1); -qed "combining1"; - -Goalw [guar_def] - "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ -\ ==> F : V guarantees (X Un Z)"; -by (Blast_tac 1); -qed "combining2"; - -(** The following two follow Chandy-Sanders, but the use of object-quantifiers - does not suit Isabelle... **) - -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) -Goalw [guar_def] - "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; -by (Blast_tac 1); -qed "all_guarantees"; - -(*Premises should be [| F: X guarantees Y i; i: I |] *) -Goalw [guar_def] - "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; -by (Blast_tac 1); -qed "ex_guarantees"; - -(*** Additional guarantees laws, by lcp ***) - -Goalw [guar_def] - "[| F: U guarantees V; 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); -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); -qed "guarantees_Join_Un"; - -Goal "((JOIN I F) component H) = (ALL i: I. F i component H)"; -by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); -by (Blast_tac 1); -qed "JN_component_iff"; - -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()); - -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()); - - -(*** guarantees 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"; - -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); -qed "guarantees_JN_I"; - - -(*** well-definedness ***) - -Goalw [welldef_def] "F Join G: welldef ==> F: welldef"; -by Auto_tac; -qed "Join_welldef_D1"; - -Goalw [welldef_def] "F Join G: welldef ==> G: welldef"; -by Auto_tac; -qed "Join_welldef_D2"; - -(*** refinement ***) - -Goalw [refines_def] "F refines F wrt X"; -by (Blast_tac 1); -qed "refines_refl"; - -Goalw [refines_def] - "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; -by Auto_tac; -qed "refines_trans"; - -Goalw [strict_ex_prop_def] - "strict_ex_prop X \ -\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; -by (Blast_tac 1); -qed "strict_ex_refine_lemma"; - -Goalw [strict_ex_prop_def] - "strict_ex_prop X \ -\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ -\ (F: welldef Int X --> G:X)"; -by Safe_tac; -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset())); -qed "strict_ex_refine_lemma_v"; - -Goal "[| strict_ex_prop X; \ -\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ -\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; -by (res_inst_tac [("x","SKIP")] allE 1 - THEN assume_tac 1); -by (asm_full_simp_tac - (simpset() addsimps [refines_def, iso_refines_def, - strict_ex_refine_lemma_v]) 1); -qed "ex_refinement_thm"; - - -Goalw [strict_uv_prop_def] - "strict_uv_prop X \ -\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; -by (Blast_tac 1); -qed "strict_uv_refine_lemma"; - -Goalw [strict_uv_prop_def] - "strict_uv_prop X \ -\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ -\ (F: welldef Int X --> G:X)"; -by Safe_tac; -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], - simpset())); -qed "strict_uv_refine_lemma_v"; - -Goal "[| strict_uv_prop X; \ -\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ -\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; -by (res_inst_tac [("x","SKIP")] allE 1 - THEN assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, - strict_uv_refine_lemma_v]) 1); -qed "uv_refinement_thm"; +bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq); diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Comp.thy Tue Aug 31 15:56:56 1999 +0200 @@ -10,42 +10,13 @@ Comp = Union + -constdefs - - (*Existential and Universal properties. I formalize the two-program - case, proving equivalence with Chandy and Sanders's n-ary definitions*) - - ex_prop :: 'a program set => bool - "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X" - - strict_ex_prop :: 'a program set => bool - "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)" - - uv_prop :: 'a program set => bool - "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)" - - strict_uv_prop :: 'a program set => bool - "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))" +instance + program :: (term)ord - (*Ill-defined programs can arise through "Join"*) - welldef :: 'a program set - "welldef == {F. Init F ~= {}}" - - component :: ['a program, 'a program] => bool (infixl 50) - "F component H == EX G. F Join G = H" +defs - 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 component H --> H:X --> H:Y}" + component_def "F <= H == EX G. F Join G = H" - refines :: ['a program, 'a program, 'a program set] => bool - ("(3_ refines _ wrt _)" [10,10,10] 10) - "G refines F wrt X == - ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X" - - iso_refines :: ['a program, 'a program, 'a program set] => bool - ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) - "G iso_refines F wrt X == - F : welldef Int X --> G : welldef Int X" + strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" end diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Extend.ML --- a/src/HOL/UNITY/Extend.ML Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Extend.ML Tue Aug 31 15:56:56 1999 +0200 @@ -300,8 +300,7 @@ (*Opposite direction fails because Diff in the extended state may remove fewer actions, i.e. those that affect other state variables.*) -Goal "Diff (project h G) acts component \ -\ project h (Diff G (extend_act h `` acts))"; +Goal "Diff (project h G) acts <= project h (Diff G (extend_act h `` acts))"; by (force_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def]) 1); qed "Diff_project_component_project_Diff"; diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Extend.thy Tue Aug 31 15:56:56 1999 +0200 @@ -8,7 +8,7 @@ function g (forgotten) maps the extended state to the "extending part" *) -Extend = Union + Comp + +Extend = Guar + constdefs diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Lift_prog.ML --- a/src/HOL/UNITY/Lift_prog.ML Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Lift_prog.ML Tue Aug 31 15:56:56 1999 +0200 @@ -68,12 +68,12 @@ (** These monotonicity results look natural but are UNUSED **) -Goal "F component G ==> lift_prog i F component lift_prog i G"; +Goal "F <= G ==> lift_prog i F <= lift_prog i G"; by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); by Auto_tac; qed "lift_prog_mono"; -Goal "F component G ==> drop_prog i F component drop_prog i G"; +Goal "F <= G ==> drop_prog i F <= drop_prog i G"; by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1); by Auto_tac; qed "drop_prog_mono"; @@ -218,6 +218,8 @@ (*** Diff, needed for localTo ***) +(** THESE PROOFS CAN BE GENERALIZED AS IN EXTEND.ML **) + Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B) \ \ ==> Diff (drop_prog i G) (Acts F) : A co B"; by (auto_tac (claset(), @@ -382,7 +384,10 @@ by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); qed "lift_prog_guarantees"; -(*Weak precondition and postcondition; this is the good one!*) +(*Weak precondition and postcondition; this is the good one! +CAN WEAKEN 2ND PREMISE TO + !!G. extend h F Join G : XX ==> F Join project h G : X; +*) val [xguary,drop_prog,lift_prog] = Goal "[| F : X guarantees Y; \ \ !!H. H : XX ==> drop_prog i H : X; \ diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Aug 31 15:56:56 1999 +0200 @@ -6,7 +6,7 @@ lift_prog, etc: replication of components *) -Lift_prog = Union + Comp + +Lift_prog = Guar + constdefs diff -r c68ecbf05eb6 -r cf780c2bcccf src/HOL/UNITY/PPROD.ML --- a/src/HOL/UNITY/PPROD.ML Mon Aug 30 23:19:13 1999 +0200 +++ b/src/HOL/UNITY/PPROD.ML Tue Aug 31 15:56:56 1999 +0200 @@ -40,7 +40,7 @@ by Auto_tac; qed "PLam_insert"; -Goalw [PLam_def] "i : I ==> (lift_prog i (F i)) component (PLam I F)"; +Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)"; (*blast_tac doesn't use HO unification*) by (fast_tac (claset() addIs [component_JN]) 1); qed "component_PLam";