# HG changeset patch # User paulson # Date 907576024 -7200 # Node ID e981ca6f733259730700506e23e0fe4c60528cd9 # Parent 6957f124ca97b5fae745cef4bec61d248c8d7e44 Finished proofs to end of section 5.1 of Chandy and Sanders diff -r 6957f124ca97 -r e981ca6f7332 src/HOL/UNITY/Comp.ML --- a/src/HOL/UNITY/Comp.ML Mon Oct 05 10:22:49 1998 +0200 +++ b/src/HOL/UNITY/Comp.ML Mon Oct 05 10:27:04 1998 +0200 @@ -8,8 +8,6 @@ From Chandy and Sanders, "Reasoning About Program Composition" *) -Addsimps [Join_SKIP, Join_absorb]; - (*split_all_tac causes a big blow-up*) claset_ref() := claset() delSWrapper "split_all_tac"; @@ -18,22 +16,26 @@ (*** component ***) +Goalw [component_def] "component SKIP F"; +by (blast_tac (claset() addIs [Join_SKIP_left]) 1); +qed "component_SKIP"; + Goalw [component_def] "component F F"; -by (blast_tac (claset() addIs [Join_SKIP]) 1); +by (blast_tac (claset() addIs [Join_SKIP_right]) 1); qed "component_refl"; -AddIffs [component_refl]; +AddIffs [component_SKIP, component_refl]; Goalw [component_def] "[| component F G; component G H |] ==> component F H"; by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); qed "component_trans"; Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G"; -auto(); +by Auto_tac; qed "componet_Acts"; Goalw [component_def,Join_def] "component F G ==> Init G <= Init F"; -auto(); +by Auto_tac; qed "componet_Init"; Goal "[| component F G; component G F |] ==> F=G"; @@ -51,11 +53,10 @@ qed_spec_mp "ex1"; Goalw [ex_prop_def] - "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X \ -\ ==> ex_prop X"; + "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); -auto(); +by Auto_tac; qed "ex2"; (*Chandy & Sanders take this as a definition*) @@ -65,8 +66,8 @@ (*Their "equivalent definition" given at the end of section 3*) Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))"; -auto(); -bws [ex_prop_def, component_def]; +by Auto_tac; +by (rewrite_goals_tac [ex_prop_def, component_def]); by (Blast_tac 1); by Safe_tac; by (stac Join_commute 2); @@ -84,11 +85,11 @@ Goalw [uv_prop_def] "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X"; -br conjI 1; +by (rtac conjI 1); by (Clarify_tac 2); by (dres_inst_tac [("x", "{F,G}")] spec 2); by (dres_inst_tac [("x", "{}")] spec 1); -auto(); +by Auto_tac; qed "uv2"; (*Chandy & Sanders take this as a definition*) @@ -103,7 +104,107 @@ by (Blast_tac 1); qed "subset_imp_guarantees"; +(*Remark at end of section 4.1*) Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)"; -ex_prop_equiv +by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); +by (blast_tac (claset() addEs [equalityE]) 1); +qed "ex_prop_equiv2"; + +Goalw [guarantees_def] + "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y"; +by (Blast_tac 1); +qed "INT_guarantees_left"; + +Goalw [guarantees_def] + "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)"; +by (Blast_tac 1); +qed "INT_guarantees_right"; + +Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; +by (Blast_tac 1); +qed "shunting"; + +Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X"; +by (Blast_tac 1); +qed "contrapositive"; + +Goalw [guarantees_def] + "V guarantees X Int ((X Int Y) guarantees Z) <= (V Int Y) guarantees Z"; +by (Blast_tac 1); +qed "combining1"; + +Goalw [guarantees_def] + "V guarantees (X Un Y) Int (Y guarantees Z) <= V guarantees (X Un Z)"; +by (Blast_tac 1); +qed "combining2"; + + +(*** 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 "subset_imp_guarantees"; +qed "refines_refl"; + +Goalw [refines_def] + "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; +by (Blast_tac 1); +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"; diff -r 6957f124ca97 -r e981ca6f7332 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Mon Oct 05 10:22:49 1998 +0200 +++ b/src/HOL/UNITY/Comp.thy Mon Oct 05 10:27:04 1998 +0200 @@ -16,24 +16,35 @@ 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 --> (Join F G) : X" + "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) = (Join F G : X)" + "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 --> (Join F G) : X)" + "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) = (Join F G : X))" + "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))" - compatible :: ['a program, 'a program] => bool - "compatible F G == Init F Int Init G ~= {}" + (*Ill-defined programs can arise through "Join"*) + welldef :: 'a program set + "welldef == {F. Init F ~= {}}" component :: ['a program, 'a program] => bool - "component F H == EX G. Join F G = H" + "component F H == EX G. F Join G = H" guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65) "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}" + 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" + end