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 blow-up*)
|
|
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";
|