author | ehmety |
Fri, 02 Mar 2001 13:18:56 +0100 | |
changeset 11190 | 44e157622cb2 |
parent 10064 | 1a77667b21ef |
child 11383 | 297625089e80 |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.ML |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
5 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
6 |
Guarantees, etc. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
7 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
8 |
From Chandy and Sanders, "Reasoning About Program Composition" |
11190 | 9 |
Revised by Sidi Ehmety on January 2001 |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
10 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
11 |
|
11190 | 12 |
Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))"; |
13 |
by (auto_tac (claset() addIs [ok_sym], |
|
14 |
simpset() addsimps [OK_iff_ok])); |
|
15 |
qed "OK_insert_iff"; |
|
16 |
||
17 |
||
18 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
19 |
(*** existential properties ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
20 |
Goalw [ex_prop_def] |
11190 | 21 |
"[| ex_prop X; finite GG |] ==> \ |
22 |
\ GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
23 |
by (etac finite_induct 1); |
11190 | 24 |
by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left])); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
25 |
qed_spec_mp "ex1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
26 |
|
11190 | 27 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
28 |
Goalw [ex_prop_def] |
11190 | 29 |
"ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
30 |
by (Clarify_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
31 |
by (dres_inst_tac [("x", "{F,G}")] spec 1); |
11190 | 32 |
by (auto_tac (claset() addDs [ok_sym], |
33 |
simpset() addsimps [OK_iff_ok])); |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
34 |
qed "ex2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
35 |
|
11190 | 36 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
37 |
(*Chandy & Sanders take this as a definition*) |
11190 | 38 |
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
39 |
by (blast_tac (claset() addIs [ex1,ex2]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
40 |
qed "ex_prop_finite"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
41 |
|
11190 | 42 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
43 |
(*Their "equivalent definition" given at the end of section 3*) |
11190 | 44 |
Goal |
45 |
"ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))"; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
46 |
by Auto_tac; |
11190 | 47 |
by (rewrite_goals_tac |
48 |
[ex_prop_def, component_of_def]); |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
49 |
by Safe_tac; |
11190 | 50 |
by (stac Join_commute 3); |
51 |
by (dtac ok_sym 3); |
|
52 |
by (REPEAT(Blast_tac 1)); |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
53 |
qed "ex_prop_equiv"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
54 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
55 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
56 |
(*** universal properties ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
57 |
Goalw [uv_prop_def] |
11190 | 58 |
"[| uv_prop X; finite GG |] ==> \ |
59 |
\ GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
60 |
by (etac finite_induct 1); |
11190 | 61 |
by (auto_tac (claset(), simpset() addsimps |
62 |
[Int_insert_left, OK_insert_iff])); |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
63 |
qed_spec_mp "uv1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
64 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
65 |
Goalw [uv_prop_def] |
11190 | 66 |
"ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X ==> uv_prop X"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
67 |
by (rtac conjI 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
68 |
by (Clarify_tac 2); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
69 |
by (dres_inst_tac [("x", "{F,G}")] spec 2); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
70 |
by (dres_inst_tac [("x", "{}")] spec 1); |
11190 | 71 |
by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok])); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
72 |
qed "uv2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
73 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
74 |
(*Chandy & Sanders take this as a definition*) |
11190 | 75 |
Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
76 |
by (blast_tac (claset() addIs [uv1,uv2]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
77 |
qed "uv_prop_finite"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
78 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
79 |
(*** guarantees ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
80 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
81 |
val prems = Goal |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
82 |
"(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
83 |
\ ==> F : X guarantees Y"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
84 |
by (simp_tac (simpset() addsimps [guar_def, component_def]) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
85 |
by (blast_tac (claset() addIs prems) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
86 |
qed "guaranteesI"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
87 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
88 |
Goalw [guar_def, component_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
89 |
"[| F : X guarantees Y; F ok G; F Join G : X |] \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
90 |
\ ==> F Join G : Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
91 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
92 |
qed "guaranteesD"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
93 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
94 |
(*This version of guaranteesD matches more easily in the conclusion |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
95 |
The major premise can no longer be F<=H since we need to reason about G*) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
96 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
97 |
"[| F : X guarantees Y; F Join G = H; H : X; F ok G |] \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
98 |
\ ==> H : Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
99 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
100 |
qed "component_guaranteesD"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
101 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
102 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
103 |
"[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
104 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
105 |
qed "guarantees_weaken"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
106 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
107 |
Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
108 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
109 |
qed "subset_imp_guarantees_UNIV"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
110 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
111 |
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
112 |
Goalw [guar_def] "X <= Y ==> F : X guarantees Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
113 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
114 |
qed "subset_imp_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
115 |
|
11190 | 116 |
(*Remark at end of section 4.1 *) |
117 |
||
118 |
Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)"; |
|
119 |
by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
|
120 |
by Safe_tac; |
|
121 |
by (dres_inst_tac [("x", "x")] spec 1); |
|
122 |
by (dres_inst_tac [("x", "x")] spec 2); |
|
123 |
by (dtac sym 2); |
|
124 |
by (ALLGOALS(etac iffE)); |
|
125 |
by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); |
|
126 |
by (REPEAT(Blast_tac 1)); |
|
127 |
qed "ex_prop_imp"; |
|
128 |
||
129 |
Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)"; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
130 |
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
11190 | 131 |
by Safe_tac; |
132 |
by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); |
|
133 |
by (dtac sym 2); |
|
134 |
by (ALLGOALS(etac equalityE)); |
|
135 |
by (REPEAT(Blast_tac 1)); |
|
136 |
qed "guarantees_imp"; |
|
137 |
||
138 |
Goal "(ex_prop Y) = (Y = UNIV guarantees Y)"; |
|
139 |
by (rtac iffI 1); |
|
140 |
by (rtac ex_prop_imp 1); |
|
141 |
by (rtac guarantees_imp 2); |
|
142 |
by (ALLGOALS(Asm_simp_tac)); |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
143 |
qed "ex_prop_equiv2"; |
11190 | 144 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
145 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
146 |
(** Distributive laws. Re-orient to perform miniscoping **) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
147 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
148 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
149 |
"(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
150 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
151 |
qed "guarantees_UN_left"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
152 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
153 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
154 |
"(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
155 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
156 |
qed "guarantees_Un_left"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
157 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
158 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
159 |
"X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
160 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
161 |
qed "guarantees_INT_right"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
162 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
163 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
164 |
"Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
165 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
166 |
qed "guarantees_Int_right"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
167 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
168 |
Goal "[| F : Z guarantees X; F : Z guarantees Y |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
169 |
\ ==> F : Z guarantees (X Int Y)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
170 |
by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
171 |
qed "guarantees_Int_right_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
172 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
173 |
Goal "(F : X guarantees (INTER I Y)) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
174 |
\ (ALL i:I. F : X guarantees (Y i))"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
175 |
by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
176 |
qed "guarantees_INT_right_iff"; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
177 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
178 |
Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
179 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
180 |
qed "shunting"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
181 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
182 |
Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
183 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
184 |
qed "contrapositive"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
185 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
186 |
(** The following two can be expressed using intersection and subset, which |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
187 |
is more faithful to the text but looks cryptic. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
188 |
**) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
189 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
190 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
191 |
"[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
192 |
\ ==> F : (V Int Y) guarantees Z"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
193 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
194 |
qed "combining1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
195 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
196 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
197 |
"[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
198 |
\ ==> F : V guarantees (X Un Z)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
199 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
200 |
qed "combining2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
201 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
202 |
(** The following two follow Chandy-Sanders, but the use of object-quantifiers |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
203 |
does not suit Isabelle... **) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
204 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
205 |
(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
206 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
207 |
"ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
208 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
209 |
qed "all_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
210 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
211 |
(*Premises should be [| F: X guarantees Y i; i: I |] *) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
212 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
213 |
"EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
214 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
215 |
qed "ex_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
216 |
|
11190 | 217 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
218 |
(*** Additional guarantees laws, by lcp ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
219 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
220 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
221 |
"[| F: U guarantees V; G: X guarantees Y; F ok G |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
222 |
\ ==> F Join G: (U Int X) guarantees (V Int Y)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
223 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
224 |
by Safe_tac; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
225 |
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
226 |
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
227 |
by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
228 |
by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
229 |
qed "guarantees_Join_Int"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
230 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
231 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
232 |
"[| F: U guarantees V; G: X guarantees Y; F ok G |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
233 |
\ ==> F Join G: (U Un X) guarantees (V Un Y)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
234 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
235 |
by Safe_tac; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
236 |
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
237 |
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
238 |
by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
239 |
by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
240 |
qed "guarantees_Join_Un"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
241 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
242 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
243 |
"[| ALL i:I. F i : X i guarantees Y i; OK I F |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
244 |
\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"; |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
245 |
by Auto_tac; |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
246 |
by (ball_tac 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
247 |
by (rename_tac "i" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
248 |
by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
249 |
by (auto_tac |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
250 |
(claset() addIs [OK_imp_ok], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
251 |
simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
252 |
qed "guarantees_JN_INT"; |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
253 |
|
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
254 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
255 |
"[| ALL i:I. F i : X i guarantees Y i; OK I F |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
256 |
\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
257 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
258 |
by (ball_tac 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
259 |
by (rename_tac "i" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
260 |
by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
8251
diff
changeset
|
261 |
by (auto_tac |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
262 |
(claset() addIs [OK_imp_ok], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
263 |
simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
264 |
qed "guarantees_JN_INT"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
265 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
266 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
267 |
"[| ALL i:I. F i : X i guarantees Y i; OK I F |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
268 |
\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
269 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
270 |
by (ball_tac 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
271 |
by (rename_tac "i" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
272 |
by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
273 |
by (auto_tac |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
274 |
(claset() addIs [OK_imp_ok], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
275 |
simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
276 |
qed "guarantees_JN_UN"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
277 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
278 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
279 |
(*** guarantees laws for breaking down the program, by lcp ***) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
280 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
281 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
282 |
"[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
283 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
284 |
by Safe_tac; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
285 |
by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
286 |
qed "guarantees_Join_I1"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
287 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
288 |
Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
289 |
by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
290 |
inst "G" "G" ok_commute]) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
291 |
by (blast_tac (claset() addIs [guarantees_Join_I1]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
292 |
qed "guarantees_Join_I2"; |
7689 | 293 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
294 |
Goalw [guar_def] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
295 |
"[| i : I; F i: X guarantees Y; OK I F |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
296 |
\ ==> (JN i:I. (F i)) : X guarantees Y"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
297 |
by (Clarify_tac 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
298 |
by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
299 |
by (auto_tac (claset() addIs [OK_imp_ok], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
300 |
simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym])); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
301 |
qed "guarantees_JN_I"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
302 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
303 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
304 |
(*** well-definedness ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
305 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
306 |
Goalw [welldef_def] "F Join G: welldef ==> F: welldef"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
307 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
308 |
qed "Join_welldef_D1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
309 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
310 |
Goalw [welldef_def] "F Join G: welldef ==> G: welldef"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
311 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
312 |
qed "Join_welldef_D2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
313 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
314 |
(*** refinement ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
315 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
316 |
Goalw [refines_def] "F refines F wrt X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
317 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
318 |
qed "refines_refl"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
319 |
|
11190 | 320 |
(* Goalw [refines_def] |
321 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
322 |
by Auto_tac; |
11190 | 323 |
qed "refines_trans"; *) |
324 |
||
325 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
326 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
327 |
Goalw [strict_ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
328 |
"strict_ex_prop X \ |
11190 | 329 |
\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \ |
330 |
\ = (F:X --> G:X)"; |
|
331 |
by Auto_tac; |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
332 |
qed "strict_ex_refine_lemma"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
333 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
334 |
Goalw [strict_ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
335 |
"strict_ex_prop X \ |
11190 | 336 |
\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \ |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
337 |
\ (F: welldef Int X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
338 |
by Safe_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
339 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
340 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset())); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
341 |
qed "strict_ex_refine_lemma_v"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
342 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
343 |
Goal "[| strict_ex_prop X; \ |
11190 | 344 |
\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \ |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
345 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
346 |
by (res_inst_tac [("x","SKIP")] allE 1 |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
347 |
THEN assume_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
348 |
by (asm_full_simp_tac |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
349 |
(simpset() addsimps [refines_def, iso_refines_def, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
350 |
strict_ex_refine_lemma_v]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
351 |
qed "ex_refinement_thm"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
352 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
353 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
354 |
Goalw [strict_uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
355 |
"strict_uv_prop X \ |
11190 | 356 |
\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
357 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
358 |
qed "strict_uv_refine_lemma"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
359 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
360 |
Goalw [strict_uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
361 |
"strict_uv_prop X \ |
11190 | 362 |
\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \ |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
363 |
\ (F: welldef Int X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
364 |
by Safe_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
365 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
366 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
367 |
simpset())); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
368 |
qed "strict_uv_refine_lemma_v"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
369 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
370 |
Goal "[| strict_uv_prop X; \ |
11190 | 371 |
\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \ |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
372 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
373 |
by (res_inst_tac [("x","SKIP")] allE 1 |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
374 |
THEN assume_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
375 |
by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
376 |
strict_uv_refine_lemma_v]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
377 |
qed "uv_refinement_thm"; |
11190 | 378 |
|
379 |
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) |
|
380 |
Goalw [guar_def, component_of_def] |
|
381 |
"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))"; |
|
382 |
by Auto_tac; |
|
383 |
qed "guarantees_equiv"; |
|
384 |
||
385 |
Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"; |
|
386 |
by Auto_tac; |
|
387 |
qed "wg_weakest"; |
|
388 |
||
389 |
Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)"; |
|
390 |
by (Blast_tac 1); |
|
391 |
qed "wg_guarantees"; |
|
392 |
||
393 |
Goalw [wg_def] |
|
394 |
"(H: wg F X) = (F component_of H --> H:X)"; |
|
395 |
by (simp_tac (simpset() addsimps [guarantees_equiv]) 1); |
|
396 |
by (rtac iffI 1); |
|
397 |
by (res_inst_tac [("x", "{H}")] exI 2); |
|
398 |
by (REPEAT(Blast_tac 1)); |
|
399 |
qed "wg_equiv"; |
|
400 |
||
401 |
||
402 |
Goal |
|
403 |
"F component_of H ==> (H:wg F X) = (H:X)"; |
|
404 |
by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1); |
|
405 |
qed "component_of_wg"; |
|
406 |
||
407 |
||
408 |
Goal |
|
409 |
"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \ |
|
410 |
\ --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"; |
|
411 |
by (Clarify_tac 1); |
|
412 |
by (subgoal_tac "F component_of (JN F:FF. F)" 1); |
|
413 |
by (dres_inst_tac [("X", "X")] component_of_wg 1); |
|
414 |
by (Asm_full_simp_tac 1); |
|
415 |
by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1); |
|
416 |
by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1); |
|
417 |
by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], |
|
418 |
simpset() addsimps [OK_iff_ok])); |
|
419 |
qed "wg_finite"; |
|
420 |
||
421 |
Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)"; |
|
422 |
by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); |
|
423 |
by (Blast_tac 1); |
|
424 |
qed "wg_ex_prop"; |
|
425 |
||
426 |
(** From Charpentier and Chandy "Theorems About Composition" **) |
|
427 |
(* Proposition 2 *) |
|
428 |
Goalw [wx_def] "(wx X)<=X"; |
|
429 |
by Auto_tac; |
|
430 |
qed "wx_subset"; |
|
431 |
||
432 |
Goalw [wx_def] |
|
433 |
"ex_prop (wx X)"; |
|
434 |
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
|
435 |
by Safe_tac; |
|
436 |
by (Blast_tac 1); |
|
437 |
by Auto_tac; |
|
438 |
qed "wx_ex_prop"; |
|
439 |
||
440 |
Goalw [wx_def] |
|
441 |
"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X"; |
|
442 |
by Auto_tac; |
|
443 |
qed "wx_weakest"; |
|
444 |
||
445 |
||
446 |
(* Proposition 6 *) |
|
447 |
Goalw [ex_prop_def] |
|
448 |
"ex_prop({F. ALL G. F ok G --> F Join G:X})"; |
|
449 |
by Safe_tac; |
|
450 |
by (dres_inst_tac [("x", "G Join Ga")] spec 1); |
|
451 |
by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1); |
|
452 |
by (dres_inst_tac [("x", "F Join Ga")] spec 1); |
|
453 |
by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1); |
|
454 |
by Safe_tac; |
|
455 |
by (asm_simp_tac (simpset() addsimps [ok_commute]) 1); |
|
456 |
by (subgoal_tac "F Join G = G Join F" 1); |
|
457 |
by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1); |
|
458 |
by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
459 |
qed "wx'_ex_prop"; |
|
460 |
||
461 |
(* Equivalence with the other definition of wx *) |
|
462 |
||
463 |
Goalw [wx_def] |
|
464 |
"wx X = {F. ALL G. F ok G --> (F Join G):X}"; |
|
465 |
by Safe_tac; |
|
466 |
by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1); |
|
467 |
by (dres_inst_tac [("x", "x")] spec 1); |
|
468 |
by (dres_inst_tac [("x", "G")] spec 1); |
|
469 |
by (forw_inst_tac [("c", "x Join G")] subsetD 1); |
|
470 |
by Safe_tac; |
|
471 |
by (Simp_tac 1); |
|
472 |
by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1); |
|
473 |
by Safe_tac; |
|
474 |
by (rtac wx'_ex_prop 2); |
|
475 |
by (rotate_tac 1 1); |
|
476 |
by (dres_inst_tac [("x", "SKIP")] spec 1); |
|
477 |
by Auto_tac; |
|
478 |
qed "wx_equiv"; |
|
479 |
||
480 |
||
481 |
(* Propositions 7 to 11 are about this second definition of wx. And |
|
482 |
they are the same as the ones proved for the first definition of wx by equivalence *) |
|
483 |
||
484 |
(* Proposition 12 *) |
|
485 |
(* Main result of the paper *) |
|
486 |
Goalw [guar_def] |
|
487 |
"(X guarantees Y) = wx(-X Un Y)"; |
|
488 |
by (simp_tac (simpset() addsimps [wx_equiv]) 1); |
|
489 |
qed "guarantees_wx_eq"; |
|
490 |
||
491 |
(* {* Corollary, but this result has already been proved elsewhere *} |
|
492 |
"ex_prop(X guarantees Y)"; |
|
493 |
by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); |
|
494 |
qed "guarantees_ex_prop"; |
|
495 |
*) |
|
496 |
||
497 |
(* Rules given in section 7 of Chandy and Sander's |
|
498 |
Reasoning About Program composition paper *) |
|
499 |
||
500 |
Goal "Init F <= A ==> F:(stable A) guarantees (Always A)"; |
|
501 |
by (rtac guaranteesI 1); |
|
502 |
by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
503 |
by (rtac stable_Join_Always1 1); |
|
504 |
by (ALLGOALS(asm_full_simp_tac (simpset() |
|
505 |
addsimps [invariant_def, Join_stable]))); |
|
506 |
qed "stable_guarantees_Always"; |
|
507 |
||
508 |
(* To be moved to WFair.ML *) |
|
509 |
Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"; |
|
510 |
by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); |
|
511 |
by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); |
|
512 |
by (rtac (ensuresI RS leadsTo_Basis) 3); |
|
513 |
by (ALLGOALS(Blast_tac)); |
|
514 |
qed "leadsTo_Basis'"; |
|
515 |
||
516 |
||
517 |
||
518 |
Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; |
|
519 |
by (rtac guaranteesI 1); |
|
520 |
by (rtac leadsTo_Basis' 1); |
|
521 |
by (dtac constrains_weaken_R 1); |
|
522 |
by (assume_tac 2); |
|
523 |
by (Blast_tac 1); |
|
524 |
by (blast_tac (claset() addIs [Join_transient_I1]) 1); |
|
525 |
qed "constrains_guarantees_leadsTo"; |
|
526 |
||
527 |
||
528 |
||
529 |
||
530 |
||
531 |
||
532 |