5597

1 
(* Title: HOL/UNITY/Comp.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
Composition


7 


8 
From Chandy and Sanders, "Reasoning About Program Composition"


9 
*)


10 


11 
Addsimps [Join_SKIP, Join_absorb];


12 


13 
(*split_all_tac causes a big blowup*)


14 
claset_ref() := claset() delSWrapper "split_all_tac";


15 


16 
Delsimps [split_paired_All];


17 


18 


19 
(*** component ***)


20 


21 
Goalw [component_def] "component F F";


22 
by (blast_tac (claset() addIs [Join_SKIP]) 1);


23 
qed "component_refl";


24 


25 
AddIffs [component_refl];


26 


27 
Goalw [component_def] "[ component F G; component G H ] ==> component F H";


28 
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);


29 
qed "component_trans";


30 


31 
Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";


32 
auto();


33 
qed "componet_Acts";


34 


35 
Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";


36 
auto();


37 
qed "componet_Init";


38 


39 
Goal "[ component F G; component G F ] ==> F=G";


40 
by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI,


41 
componet_Acts, componet_Init]) 1);


42 
qed "component_anti_sym";


43 


44 


45 
(*** existential properties ***)


46 


47 
Goalw [ex_prop_def]


48 
"[ ex_prop X; finite GG ] ==> GG Int X ~= {} > (JN G:GG. G) : X";


49 
by (etac finite_induct 1);


50 
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));


51 
qed_spec_mp "ex1";


52 


53 
Goalw [ex_prop_def]


54 
"ALL GG. finite GG & GG Int X ~= {} > (JN G:GG. G) : X \


55 
\ ==> ex_prop X";


56 
by (Clarify_tac 1);


57 
by (dres_inst_tac [("x", "{F,G}")] spec 1);


58 
auto();


59 
qed "ex2";


60 


61 
(*Chandy & Sanders take this as a definition*)


62 
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} > (JN G:GG. G) : X)";


63 
by (blast_tac (claset() addIs [ex1,ex2]) 1);


64 
qed "ex_prop_finite";


65 


66 
(*Their "equivalent definition" given at the end of section 3*)


67 
Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H > H: X))";


68 
auto();


69 
bws [ex_prop_def, component_def];


70 
by (Blast_tac 1);


71 
by Safe_tac;


72 
by (stac Join_commute 2);


73 
by (ALLGOALS Blast_tac);


74 
qed "ex_prop_equiv";


75 


76 


77 
(*** universal properties ***)


78 


79 
Goalw [uv_prop_def]


80 
"[ uv_prop X; finite GG ] ==> GG <= X > (JN G:GG. G) : X";


81 
by (etac finite_induct 1);


82 
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));


83 
qed_spec_mp "uv1";


84 


85 
Goalw [uv_prop_def]


86 
"ALL GG. finite GG & GG <= X > (JN G:GG. G) : X ==> uv_prop X";


87 
br conjI 1;


88 
by (Clarify_tac 2);


89 
by (dres_inst_tac [("x", "{F,G}")] spec 2);


90 
by (dres_inst_tac [("x", "{}")] spec 1);


91 
auto();


92 
qed "uv2";


93 


94 
(*Chandy & Sanders take this as a definition*)


95 
Goal "uv_prop X = (ALL GG. finite GG & GG <= X > (JN G:GG. G) : X)";


96 
by (blast_tac (claset() addIs [uv1,uv2]) 1);


97 
qed "uv_prop_finite";


98 


99 


100 
(*** guarantees ***)


101 


102 
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";


103 
by (Blast_tac 1);


104 
qed "subset_imp_guarantees";


105 


106 
Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";


107 
ex_prop_equiv


108 
by (Blast_tac 1);


109 
qed "subset_imp_guarantees";
