author | nipkow |
Mon, 13 Mar 2000 12:51:10 +0100 | |
changeset 8423 | 3c19160b6432 |
parent 8251 | 9be357df93d4 |
child 8948 | b797cfa3548d |
permissions | -rw-r--r-- |
6297 | 1 |
(* Title: HOL/UNITY/Extend.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Extending of state sets |
|
7 |
function f (forget) maps the extended state to the original state |
|
8 |
function g (forgotten) maps the extended state to the "extending part" |
|
7482 | 9 |
*) |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
10 |
|
7482 | 11 |
(** These we prove OUTSIDE the locale. **) |
12 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
13 |
Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
14 |
by (blast_tac (claset() addIs [sym RS image_eqI]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
15 |
qed "insert_Id_image_Acts"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
16 |
|
7482 | 17 |
(*Possibly easier than reasoning about "inv h"*) |
18 |
val [surj_h,prem] = |
|
19 |
Goalw [good_map_def] |
|
20 |
"[| surj h; !! x x' y y'. h(x,y) = h(x',y') ==> x=x' |] ==> good_map h"; |
|
21 |
by (safe_tac (claset() addSIs [surj_h])); |
|
22 |
by (rtac prem 1); |
|
23 |
by (stac (surjective_pairing RS sym) 1); |
|
24 |
by (stac (surj_h RS surj_f_inv_f) 1); |
|
25 |
by (rtac refl 1); |
|
26 |
qed "good_mapI"; |
|
27 |
||
28 |
Goalw [good_map_def] "good_map h ==> surj h"; |
|
29 |
by Auto_tac; |
|
30 |
qed "good_map_is_surj"; |
|
31 |
||
32 |
(*A convenient way of finding a closed form for inv h*) |
|
33 |
val [surj,prem] = Goalw [inv_def] |
|
34 |
"[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; |
|
35 |
by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); |
|
7499 | 36 |
by (rtac selectI2 1); |
7482 | 37 |
by (dres_inst_tac [("f", "g")] arg_cong 2); |
38 |
by (auto_tac (claset(), simpset() addsimps [prem])); |
|
39 |
qed "fst_inv_equalityI"; |
|
40 |
||
6297 | 41 |
|
42 |
Open_locale "Extend"; |
|
43 |
||
44 |
val slice_def = thm "slice_def"; |
|
45 |
||
46 |
(*** Trivial properties of f, g, h ***) |
|
47 |
||
7482 | 48 |
val good_h = rewrite_rule [good_map_def] (thm "good_h"); |
49 |
val surj_h = good_h RS conjunct1; |
|
6297 | 50 |
|
51 |
val f_def = thm "f_def"; |
|
52 |
val g_def = thm "g_def"; |
|
53 |
||
54 |
Goal "f(h(x,y)) = x"; |
|
7482 | 55 |
by (simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
6297 | 56 |
qed "f_h_eq"; |
57 |
Addsimps [f_h_eq]; |
|
58 |
||
7482 | 59 |
Goal "h(x,y) = h(x',y') ==> x=x'"; |
60 |
by (dres_inst_tac [("f", "fst o inv h")] arg_cong 1); |
|
61 |
(*FIXME: If locales worked properly we could put just "f" above*) |
|
62 |
by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
|
63 |
qed "h_inject1"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
64 |
AddDs [h_inject1]; |
6297 | 65 |
|
66 |
Goal "h(f z, g z) = z"; |
|
7482 | 67 |
by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym, |
68 |
surj_h RS surj_f_inv_f]) 1); |
|
6297 | 69 |
qed "h_f_g_eq"; |
70 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
71 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
72 |
(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
73 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
74 |
val cT = TFree ("'c", ["term"]); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
75 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
76 |
(* "PROP P x == PROP P (h (f x, g x))" *) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
77 |
val lemma1 = Thm.combination |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
78 |
(Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT)))) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
79 |
(Drule.unvarify (h_f_g_eq RS sym RS eq_reflection)); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
80 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
81 |
val prems = Goalw [lemma1] "(!!u y. PROP P (h (u, y))) ==> PROP P x"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
82 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
83 |
val lemma2 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
84 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
85 |
val prems = Goal "(!!u y. PROP P (h (u, y))) ==> (!!z. PROP P z)"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
86 |
by (rtac lemma2 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
87 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
88 |
val lemma3 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
89 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
90 |
val prems = Goal "(!!z. PROP P z) ==> (!!u y. PROP P (h (u, y)))"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
91 |
(*not needed for proof, but prevents generalization over h, 'c, etc.*) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
92 |
by (cut_facts_tac [surj_h] 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
93 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
94 |
val lemma4 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
95 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
96 |
val split_extended_all = Thm.equal_intr lemma4 lemma3; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
97 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
98 |
|
6297 | 99 |
(*** extend_set: basic properties ***) |
100 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
101 |
Goal "(x : project_set h C) = (EX y. h(x,y) : C)"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
102 |
by (simp_tac (simpset() addsimps [project_set_def]) 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
103 |
qed "project_set_iff"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
104 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
105 |
AddIffs [project_set_iff]; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
106 |
|
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
107 |
Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
108 |
by (Blast_tac 1); |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
109 |
qed "extend_set_mono"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
110 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
111 |
Goalw [extend_set_def] "z : extend_set h A = (f z : A)"; |
7341 | 112 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
6297 | 113 |
qed "mem_extend_set_iff"; |
114 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
115 |
AddIffs [mem_extend_set_iff]; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
116 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
117 |
Goalw [extend_set_def] "(extend_set h A <= extend_set h B) = (A <= B)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
118 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
119 |
qed "extend_set_strict_mono"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
120 |
AddIffs [extend_set_strict_mono]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
121 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
122 |
Goalw [extend_set_def] "extend_set h {} = {}"; |
7378 | 123 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
124 |
qed "extend_set_empty"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
125 |
Addsimps [extend_set_empty]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
126 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
127 |
Goal "extend_set h {s. P s} = {s. P (f s)}"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
128 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
129 |
qed "extend_set_eq_Collect"; |
7378 | 130 |
|
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
131 |
Goal "extend_set h {x} = {s. f s = x}"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
132 |
by Auto_tac; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
133 |
qed "extend_set_sing"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
134 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
135 |
Goalw [extend_set_def] "project_set h (extend_set h C) = C"; |
7341 | 136 |
by Auto_tac; |
137 |
qed "extend_set_inverse"; |
|
138 |
Addsimps [extend_set_inverse]; |
|
139 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
140 |
Goalw [extend_set_def] "C <= extend_set h (project_set h C)"; |
7947 | 141 |
by (auto_tac (claset(), |
142 |
simpset() addsimps [split_extended_all])); |
|
143 |
by (Blast_tac 1); |
|
144 |
qed "extend_set_project_set"; |
|
145 |
||
6297 | 146 |
Goal "inj (extend_set h)"; |
7341 | 147 |
by (rtac inj_on_inverseI 1); |
148 |
by (rtac extend_set_inverse 1); |
|
6297 | 149 |
qed "inj_extend_set"; |
150 |
||
7689 | 151 |
Goalw [extend_set_def] "extend_set h UNIV = UNIV"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
152 |
by (auto_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
153 |
simpset() addsimps [split_extended_all])); |
7689 | 154 |
qed "extend_set_UNIV_eq"; |
155 |
Addsimps [standard extend_set_UNIV_eq]; |
|
156 |
||
7482 | 157 |
(*** project_set: basic properties ***) |
158 |
||
159 |
(*project_set is simply image!*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
160 |
Goal "project_set h C = f `` C"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
161 |
by (auto_tac (claset() addIs [f_h_eq RS sym], |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
162 |
simpset() addsimps [split_extended_all])); |
7482 | 163 |
qed "project_set_eq"; |
164 |
||
165 |
(*Converse appears to fail*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
166 |
Goal "!!z. z : C ==> f z : project_set h C"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
167 |
by (auto_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
168 |
simpset() addsimps [split_extended_all])); |
7482 | 169 |
qed "project_set_I"; |
170 |
||
171 |
||
172 |
(*** More laws ***) |
|
173 |
||
7341 | 174 |
(*Because A and B could differ on the "other" part of the state, |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
175 |
cannot generalize to |
7341 | 176 |
project_set h (A Int B) = project_set h A Int project_set h B |
177 |
*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
178 |
Goal "project_set h ((extend_set h A) Int B) = A Int (project_set h B)"; |
7341 | 179 |
by Auto_tac; |
180 |
qed "project_set_extend_set_Int"; |
|
181 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
182 |
Goal "project_set h (A Int B) <= (project_set h A) Int (project_set h B)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
183 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
184 |
qed "project_set_Int_subset"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
185 |
|
7341 | 186 |
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B"; |
6297 | 187 |
by Auto_tac; |
188 |
qed "extend_set_Un_distrib"; |
|
189 |
||
7341 | 190 |
Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B"; |
6297 | 191 |
by Auto_tac; |
192 |
qed "extend_set_Int_distrib"; |
|
193 |
||
7341 | 194 |
Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"; |
195 |
by Auto_tac; |
|
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
196 |
qed "extend_set_INT_distrib"; |
6647 | 197 |
|
7341 | 198 |
Goal "extend_set h (A - B) = extend_set h A - extend_set h B"; |
6297 | 199 |
by Auto_tac; |
200 |
qed "extend_set_Diff_distrib"; |
|
201 |
||
7341 | 202 |
Goal "extend_set h (Union A) = (UN X:A. extend_set h X)"; |
6297 | 203 |
by (Blast_tac 1); |
204 |
qed "extend_set_Union"; |
|
205 |
||
7341 | 206 |
Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)"; |
6297 | 207 |
by Auto_tac; |
208 |
qed "extend_set_subset_Compl_eq"; |
|
209 |
||
7341 | 210 |
|
6297 | 211 |
(*** extend_act ***) |
212 |
||
8216 | 213 |
(*Can't strengthen it to |
214 |
((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') |
|
215 |
because h doesn't have to be injective in the 2nd argument*) |
|
6297 | 216 |
Goalw [extend_act_def] |
217 |
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"; |
|
218 |
by Auto_tac; |
|
219 |
qed "mem_extend_act_iff"; |
|
220 |
AddIffs [mem_extend_act_iff]; |
|
221 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
222 |
(*Converse fails: (z,z') would include actions that changed the g-part*) |
7341 | 223 |
Goalw [extend_act_def] |
224 |
"(z, z') : extend_act h act ==> (f z, f z') : act"; |
|
225 |
by Auto_tac; |
|
226 |
qed "extend_act_D"; |
|
227 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
228 |
Goalw [extend_act_def, project_act_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
229 |
"project_act h (extend_act h act) = act"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
230 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
231 |
qed "project_act_extend_act"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
232 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
233 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
234 |
"project_act h (Restrict C (extend_act h act)) = \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
235 |
\ Restrict (project_set h C) act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
236 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
237 |
qed "project_act_extend_act_restrict"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
238 |
Addsimps [project_act_extend_act_restrict]; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
239 |
|
7537 | 240 |
(*Premise is still undesirably strong, since Domain act can include |
241 |
non-reachable states, but it seems necessary for this result.*) |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
242 |
Goal "Domain act <= project_set h C \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
243 |
\ ==> project_act h (Restrict C (extend_act h act)) = act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
244 |
by (asm_simp_tac (simpset() addsimps [Restrict_triv]) 1); |
7341 | 245 |
qed "extend_act_inverse"; |
246 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
247 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
248 |
"act' <= extend_act h act ==> project_act h act' <= act"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
249 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
250 |
qed "subset_extend_act_D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
251 |
|
6297 | 252 |
Goal "inj (extend_act h)"; |
7341 | 253 |
by (rtac inj_on_inverseI 1); |
254 |
by (rtac extend_act_inverse 1); |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
255 |
by (Force_tac 1); |
6297 | 256 |
qed "inj_extend_act"; |
257 |
||
258 |
Goalw [extend_set_def, extend_act_def] |
|
259 |
"extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)"; |
|
260 |
by (Force_tac 1); |
|
261 |
qed "extend_act_Image"; |
|
262 |
Addsimps [extend_act_Image]; |
|
263 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
264 |
Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
265 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
266 |
qed "extend_act_strict_mono"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
267 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
268 |
AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
269 |
(*The latter theorem is (extend_act h act' = extend_act h act) = (act'=act) *) |
6297 | 270 |
|
271 |
Goalw [extend_set_def, extend_act_def] |
|
272 |
"Domain (extend_act h act) = extend_set h (Domain act)"; |
|
273 |
by (Force_tac 1); |
|
274 |
qed "Domain_extend_act"; |
|
275 |
||
7341 | 276 |
Goalw [extend_act_def] |
6297 | 277 |
"extend_act h Id = Id"; |
278 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
|
279 |
qed "extend_act_Id"; |
|
7341 | 280 |
|
281 |
Goalw [project_act_def] |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
282 |
"!!z z'. (z, z') : act ==> (f z, f z') : project_act h act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
283 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
284 |
simpset() addsimps [split_extended_all]) 1); |
7341 | 285 |
qed "project_act_I"; |
286 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
287 |
Goalw [project_act_def] "project_act h Id = Id"; |
7341 | 288 |
by (Force_tac 1); |
289 |
qed "project_act_Id"; |
|
290 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
291 |
Goalw [project_act_def] |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
292 |
"Domain (project_act h act) = project_set h (Domain act)"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
293 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
294 |
simpset() addsimps [split_extended_all]) 1); |
7482 | 295 |
qed "Domain_project_act"; |
296 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
297 |
Addsimps [extend_act_Id]; |
6297 | 298 |
|
299 |
||
300 |
(**** extend ****) |
|
301 |
||
302 |
(*** Basic properties ***) |
|
303 |
||
7341 | 304 |
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)"; |
6297 | 305 |
by Auto_tac; |
306 |
qed "Init_extend"; |
|
307 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
308 |
Goalw [project_def] "Init (project h C F) = project_set h (Init F)"; |
7341 | 309 |
by Auto_tac; |
310 |
qed "Init_project"; |
|
311 |
||
6297 | 312 |
Goal "Acts (extend h F) = (extend_act h `` Acts F)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
313 |
by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1); |
6297 | 314 |
qed "Acts_extend"; |
315 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
316 |
Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)"; |
7546
36b26759147e
project_act no longer has a special case to allow identity actions
paulson
parents:
7538
diff
changeset
|
317 |
by (auto_tac (claset(), |
7341 | 318 |
simpset() addsimps [project_def, image_iff])); |
319 |
qed "Acts_project"; |
|
320 |
||
321 |
Addsimps [Init_extend, Init_project, Acts_extend, Acts_project]; |
|
6297 | 322 |
|
323 |
Goalw [SKIP_def] "extend h SKIP = SKIP"; |
|
324 |
by (rtac program_equalityI 1); |
|
7341 | 325 |
by Auto_tac; |
326 |
qed "extend_SKIP"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
327 |
Addsimps [export extend_SKIP]; |
7341 | 328 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
329 |
Goal "project_set h UNIV = UNIV"; |
7537 | 330 |
by Auto_tac; |
331 |
qed "project_set_UNIV"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
332 |
Addsimps [project_set_UNIV]; |
7537 | 333 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
334 |
Goal "project_set h (Union A) = (UN X:A. project_set h X)"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
335 |
by (Blast_tac 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
336 |
qed "project_set_Union"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
337 |
|
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
338 |
Goal "project h C (extend h F) = \ |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
339 |
\ mk_program (Init F, Restrict (project_set h C) `` Acts F)"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
340 |
by (rtac program_equalityI 1); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
341 |
by (asm_simp_tac (simpset() addsimps [image_eq_UN, |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
342 |
project_act_extend_act_restrict]) 2); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
343 |
by (Simp_tac 1); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
344 |
qed "project_extend_eq"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
345 |
|
7537 | 346 |
(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*) |
347 |
Goal "UNIV <= project_set h C \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
348 |
\ ==> project h C (extend h F) = F"; |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
349 |
by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN, |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
350 |
subset_UNIV RS subset_trans RS Restrict_triv]) 1); |
7341 | 351 |
qed "extend_inverse"; |
352 |
Addsimps [extend_inverse]; |
|
6297 | 353 |
|
354 |
Goal "inj (extend h)"; |
|
7341 | 355 |
by (rtac inj_on_inverseI 1); |
356 |
by (rtac extend_inverse 1); |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
357 |
by (Force_tac 1); |
6297 | 358 |
qed "inj_extend"; |
359 |
||
360 |
Goal "extend h (F Join G) = extend h F Join extend h G"; |
|
361 |
by (rtac program_equalityI 1); |
|
7537 | 362 |
by (simp_tac (simpset() addsimps [image_Un]) 2); |
6297 | 363 |
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1); |
364 |
qed "extend_Join"; |
|
365 |
Addsimps [extend_Join]; |
|
366 |
||
6647 | 367 |
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))"; |
368 |
by (rtac program_equalityI 1); |
|
7537 | 369 |
by (simp_tac (simpset() addsimps [image_UN]) 2); |
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
370 |
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1); |
6647 | 371 |
qed "extend_JN"; |
372 |
Addsimps [extend_JN]; |
|
373 |
||
7689 | 374 |
(** These monotonicity results look natural but are UNUSED **) |
375 |
||
376 |
Goal "F <= G ==> extend h F <= extend h G"; |
|
377 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
378 |
by Auto_tac; |
|
379 |
qed "extend_mono"; |
|
380 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
381 |
Goal "F <= G ==> project h C F <= project h C G"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
382 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
7689 | 383 |
by Auto_tac; |
384 |
qed "project_mono"; |
|
385 |
||
386 |
||
6536 | 387 |
(*** Safety: co, stable ***) |
6297 | 388 |
|
6536 | 389 |
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \ |
390 |
\ (F : A co B)"; |
|
6297 | 391 |
by (simp_tac (simpset() addsimps [constrains_def]) 1); |
392 |
qed "extend_constrains"; |
|
393 |
||
394 |
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)"; |
|
395 |
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1); |
|
396 |
qed "extend_stable"; |
|
397 |
||
398 |
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)"; |
|
399 |
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1); |
|
400 |
qed "extend_invariant"; |
|
401 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
402 |
(*Converse fails: A and B may differ in their extra variables*) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
403 |
Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
404 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
405 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
406 |
qed "extend_constrains_project_set"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
407 |
|
8041 | 408 |
Goal "extend h F : stable A ==> F : stable (project_set h A)"; |
409 |
by (asm_full_simp_tac |
|
410 |
(simpset() addsimps [stable_def, extend_constrains_project_set]) 1); |
|
411 |
qed "extend_stable_project_set"; |
|
412 |
||
7341 | 413 |
|
414 |
(*** Weak safety primitives: Co, Stable ***) |
|
6297 | 415 |
|
416 |
Goal "p : reachable (extend h F) ==> f p : reachable F"; |
|
417 |
by (etac reachable.induct 1); |
|
418 |
by (auto_tac |
|
419 |
(claset() addIs reachable.intrs, |
|
7341 | 420 |
simpset() addsimps [extend_act_def, image_iff])); |
6297 | 421 |
qed "reachable_extend_f"; |
422 |
||
423 |
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F"; |
|
424 |
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1); |
|
425 |
qed "h_reachable_extend"; |
|
426 |
||
427 |
Goalw [extend_set_def] |
|
428 |
"reachable (extend h F) = extend_set h (reachable F)"; |
|
429 |
by (rtac equalityI 1); |
|
430 |
by (force_tac (claset() addIs [h_f_g_eq RS sym] |
|
431 |
addSDs [reachable_extend_f], |
|
432 |
simpset()) 1); |
|
433 |
by (Clarify_tac 1); |
|
434 |
by (etac reachable.induct 1); |
|
435 |
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, |
|
436 |
simpset()))); |
|
437 |
qed "reachable_extend_eq"; |
|
438 |
||
6536 | 439 |
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \ |
440 |
\ (F : A Co B)"; |
|
6297 | 441 |
by (simp_tac |
442 |
(simpset() addsimps [Constrains_def, reachable_extend_eq, |
|
443 |
extend_constrains, extend_set_Int_distrib RS sym]) 1); |
|
444 |
qed "extend_Constrains"; |
|
445 |
||
446 |
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)"; |
|
447 |
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1); |
|
448 |
qed "extend_Stable"; |
|
449 |
||
6647 | 450 |
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)"; |
451 |
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1); |
|
452 |
qed "extend_Always"; |
|
453 |
||
6297 | 454 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
455 |
(** Safety and "project" **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
456 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
457 |
(** projection: monotonicity for safety **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
458 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
459 |
Goal "D <= C ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
460 |
\ project_act h (Restrict D act) <= project_act h (Restrict C act)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
461 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
462 |
qed "project_act_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
463 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
464 |
Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
465 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
466 |
by (dtac project_act_mono 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
467 |
by (Blast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
468 |
qed "project_constrains_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
469 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
470 |
Goal "[| D <= C; project h C F : stable A |] ==> project h D F : stable A"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
471 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
472 |
(simpset() addsimps [stable_def, project_constrains_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
473 |
qed "project_stable_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
474 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
475 |
Goalw [constrains_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
476 |
"(project h C F : A co B) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
477 |
\ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
478 |
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
479 |
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
480 |
(*the <== direction*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
481 |
by (rewtac project_act_def); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
482 |
by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
483 |
qed "project_constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
484 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
485 |
Goalw [stable_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
486 |
"(project h UNIV F : stable A) = (F : stable (extend_set h A))"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
487 |
by (simp_tac (simpset() addsimps [project_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
488 |
qed "project_stable"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
489 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
490 |
Goal "F : stable (extend_set h A) ==> project h C F : stable A"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
491 |
by (dtac (project_stable RS iffD2) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
492 |
by (blast_tac (claset() addIs [project_stable_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
493 |
qed "project_stable_I"; |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
494 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
495 |
Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
496 |
by (auto_tac (claset(), simpset() addsimps [split_extended_all])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
497 |
qed "Int_extend_set_lemma"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
498 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
499 |
Goal "G : C co B ==> project h C G : project_set h C co project_set h B"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
500 |
by (full_simp_tac (simpset() addsimps [constrains_def, project_def, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
501 |
project_act_def]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
502 |
by (Blast_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
503 |
qed "project_constrains_project_set"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
504 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
505 |
Goal "G : stable C ==> project h C G : stable (project_set h C)"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
506 |
by (asm_full_simp_tac (simpset() addsimps [stable_def, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
507 |
project_constrains_project_set]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
508 |
qed "project_stable_project_set"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
509 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
510 |
|
6297 | 511 |
(*** Progress: transient, ensures ***) |
512 |
||
513 |
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
|
514 |
by (auto_tac (claset(), |
|
515 |
simpset() addsimps [transient_def, extend_set_subset_Compl_eq, |
|
516 |
Domain_extend_act])); |
|
517 |
qed "extend_transient"; |
|
518 |
||
6536 | 519 |
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \ |
520 |
\ (F : A ensures B)"; |
|
6297 | 521 |
by (simp_tac |
522 |
(simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
523 |
extend_set_Un_distrib RS sym, |
|
524 |
extend_set_Diff_distrib RS sym]) 1); |
|
525 |
qed "extend_ensures"; |
|
526 |
||
6536 | 527 |
Goal "F : A leadsTo B \ |
528 |
\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"; |
|
6297 | 529 |
by (etac leadsTo_induct 1); |
530 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3); |
|
531 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
532 |
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1); |
|
533 |
qed "leadsTo_imp_extend_leadsTo"; |
|
534 |
||
535 |
(*** Proving the converse takes some doing! ***) |
|
536 |
||
8111 | 537 |
Goal "(x : slice C y) = (h(x,y) : C)"; |
538 |
by (simp_tac (simpset() addsimps [slice_def]) 1); |
|
539 |
qed "slice_iff"; |
|
540 |
||
541 |
AddIffs [slice_iff]; |
|
542 |
||
543 |
Goal "slice (Union S) y = (UN x:S. slice x y)"; |
|
6297 | 544 |
by Auto_tac; |
545 |
qed "slice_Union"; |
|
546 |
||
8111 | 547 |
Goal "slice (extend_set h A) y = A"; |
6297 | 548 |
by Auto_tac; |
549 |
qed "slice_extend_set"; |
|
550 |
||
8111 | 551 |
Goal "project_set h A = (UN y. slice A y)"; |
6297 | 552 |
by Auto_tac; |
7482 | 553 |
qed "project_set_is_UN_slice"; |
6297 | 554 |
|
8111 | 555 |
Goalw [transient_def] "extend h F : transient A ==> F : transient (slice A y)"; |
6297 | 556 |
by Auto_tac; |
557 |
by (rtac bexI 1); |
|
558 |
by Auto_tac; |
|
559 |
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1); |
|
560 |
qed "extend_transient_slice"; |
|
561 |
||
8111 | 562 |
(*Converse?*) |
563 |
Goal "extend h F : A co B ==> F : (slice A y) co (slice B y)"; |
|
564 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
|
565 |
qed "extend_constrains_slice"; |
|
566 |
||
7482 | 567 |
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"; |
8111 | 568 |
by (auto_tac (claset(), |
569 |
simpset() addsimps [ensures_def, extend_constrains, |
|
570 |
extend_transient])); |
|
571 |
by (etac (extend_transient_slice RS transient_strengthen) 2); |
|
572 |
by (etac (extend_constrains_slice RS constrains_weaken) 1); |
|
573 |
by Auto_tac; |
|
6297 | 574 |
qed "extend_ensures_slice"; |
575 |
||
7482 | 576 |
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"; |
577 |
by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1); |
|
6297 | 578 |
by (blast_tac (claset() addIs [leadsTo_UN]) 1); |
8111 | 579 |
qed "leadsTo_slice_project_set"; |
6297 | 580 |
|
6536 | 581 |
Goal "extend h F : AU leadsTo BU \ |
7482 | 582 |
\ ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"; |
6297 | 583 |
by (etac leadsTo_induct 1); |
8111 | 584 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, slice_Union]) 3); |
585 |
by (blast_tac (claset() addIs [leadsTo_slice_project_set, leadsTo_Trans]) 2); |
|
6297 | 586 |
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1); |
587 |
qed_spec_mp "extend_leadsTo_slice"; |
|
588 |
||
6536 | 589 |
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \ |
590 |
\ (F : A leadsTo B)"; |
|
6297 | 591 |
by Safe_tac; |
592 |
by (etac leadsTo_imp_extend_leadsTo 2); |
|
593 |
by (dtac extend_leadsTo_slice 1); |
|
594 |
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1); |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
595 |
qed "extend_leadsTo"; |
6297 | 596 |
|
6536 | 597 |
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \ |
598 |
\ (F : A LeadsTo B)"; |
|
6454 | 599 |
by (simp_tac |
600 |
(simpset() addsimps [LeadsTo_def, reachable_extend_eq, |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
601 |
extend_leadsTo, extend_set_Int_distrib RS sym]) 1); |
6454 | 602 |
qed "extend_LeadsTo"; |
603 |
||
6297 | 604 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
605 |
(*** preserves ***) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
606 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
607 |
Goal "G : preserves (v o f) ==> project h C G : preserves v"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
608 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
609 |
simpset() addsimps [preserves_def, project_stable_I, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
610 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
611 |
qed "project_preserves_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
612 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
613 |
(*to preserve f is to preserve the whole original state*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
614 |
Goal "G : preserves f ==> project h C G : preserves id"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
615 |
by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
616 |
qed "project_preserves_id_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
617 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
618 |
Goal "(extend h G : preserves (v o f)) = (G : preserves v)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
619 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
620 |
simpset() addsimps [preserves_def, extend_stable RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
621 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
622 |
qed "extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
623 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
624 |
Goal "inj h ==> (extend h G : preserves g)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
625 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
626 |
simpset() addsimps [preserves_def, extend_def, extend_act_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
627 |
stable_def, constrains_def, g_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
628 |
qed "inj_extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
629 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
630 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
631 |
(*** Guarantees ***) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
632 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
633 |
Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
634 |
by (rtac program_equalityI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
635 |
by (asm_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
636 |
(simpset() addsimps [image_eq_UN, UN_Un, project_act_extend_act]) 2); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
637 |
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
638 |
qed "project_extend_Join"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
639 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
640 |
Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
641 |
by (dres_inst_tac [("f", "project h UNIV")] arg_cong 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
642 |
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
643 |
qed "extend_Join_eq_extend_D"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
644 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
645 |
(** Strong precondition and postcondition; only useful when |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
646 |
the old and new state sets are in bijection **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
647 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
648 |
Goal "F : X guarantees[v] Y ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
649 |
\ extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
650 |
by (rtac guaranteesI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
651 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
652 |
by (blast_tac (claset() addIs [project_preserves_I] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
653 |
addDs [extend_Join_eq_extend_D, guaranteesD]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
654 |
qed "guarantees_imp_extend_guarantees"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
655 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
656 |
Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
657 |
\ ==> F : X guarantees[v] Y"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
658 |
by (auto_tac (claset(), simpset() addsimps [guar_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
659 |
by (dres_inst_tac [("x", "extend h G")] spec 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
660 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
661 |
(simpset() delsimps [extend_Join] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
662 |
addsimps [extend_Join RS sym, extend_preserves, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
663 |
inj_extend RS inj_image_mem_iff]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
664 |
qed "extend_guarantees_imp_guarantees"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
665 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
666 |
Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
667 |
\ (F : X guarantees[v] Y)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
668 |
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
669 |
extend_guarantees_imp_guarantees]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
670 |
qed "extend_guarantees_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
671 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
672 |
|
6297 | 673 |
Close_locale "Extend"; |
7482 | 674 |
|
675 |
(*Close_locale should do this! |
|
676 |
Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_inverse, |
|
677 |
extend_act_Image]; |
|
678 |
Delrules [make_elim h_inject1]; |
|
679 |
*) |