author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11467 | 1064effe37f6 |
child 13550 | 5a176b8dda84 |
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 |
||
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
13 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
14 |
(*** Restrict [MOVE to Relation.thy?] ***) |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
15 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
16 |
Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
17 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
18 |
qed "Restrict_iff"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
19 |
AddIffs [Restrict_iff]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
20 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
21 |
Goal "Restrict UNIV = id"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
22 |
by (rtac ext 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
23 |
by (auto_tac (claset(), simpset() addsimps [Restrict_def])); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
24 |
qed "Restrict_UNIV"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
25 |
Addsimps [Restrict_UNIV]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
26 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
27 |
Goal "Restrict {} r = {}"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
28 |
by (auto_tac (claset(), simpset() addsimps [Restrict_def])); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
29 |
qed "Restrict_empty"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
30 |
Addsimps [Restrict_empty]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
31 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
32 |
Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
33 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
34 |
qed "Restrict_Int"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
35 |
Addsimps [Restrict_Int]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
36 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
37 |
Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
38 |
by Auto_tac; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
39 |
qed "Restrict_triv"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
40 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
41 |
Goalw [Restrict_def] "Restrict A r <= r"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
42 |
by Auto_tac; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
43 |
qed "Restrict_subset"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
44 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
45 |
Goalw [Restrict_def] |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
46 |
"[| A <= B; Restrict B r = Restrict B s |] \ |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
47 |
\ ==> Restrict A r = Restrict A s"; |
9190 | 48 |
by (Blast_tac 1); |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
49 |
qed "Restrict_eq_mono"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
50 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
51 |
Goalw [Restrict_def, image_def] |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
52 |
"[| s : RR; Restrict A r = Restrict A s |] \ |
10834 | 53 |
\ ==> Restrict A r : Restrict A ` RR"; |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
54 |
by Auto_tac; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
55 |
qed "Restrict_imageI"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
56 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
57 |
Goal "Domain (Restrict A r) = A Int Domain r"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
58 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
59 |
qed "Domain_Restrict"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
60 |
|
10834 | 61 |
Goal "(Restrict A r) `` B = r `` (A Int B)"; |
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
62 |
by (Blast_tac 1); |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
63 |
qed "Image_Restrict"; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
64 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
65 |
Addsimps [Domain_Restrict, Image_Restrict]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
66 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
67 |
|
10834 | 68 |
Goal "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
69 |
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
|
70 |
qed "insert_Id_image_Acts"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
71 |
|
7482 | 72 |
(*Possibly easier than reasoning about "inv h"*) |
73 |
val [surj_h,prem] = |
|
74 |
Goalw [good_map_def] |
|
75 |
"[| surj h; !! x x' y y'. h(x,y) = h(x',y') ==> x=x' |] ==> good_map h"; |
|
76 |
by (safe_tac (claset() addSIs [surj_h])); |
|
77 |
by (rtac prem 1); |
|
78 |
by (stac (surjective_pairing RS sym) 1); |
|
79 |
by (stac (surj_h RS surj_f_inv_f) 1); |
|
80 |
by (rtac refl 1); |
|
81 |
qed "good_mapI"; |
|
82 |
||
83 |
Goalw [good_map_def] "good_map h ==> surj h"; |
|
84 |
by Auto_tac; |
|
85 |
qed "good_map_is_surj"; |
|
86 |
||
87 |
(*A convenient way of finding a closed form for inv h*) |
|
88 |
val [surj,prem] = Goalw [inv_def] |
|
89 |
"[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; |
|
90 |
by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); |
|
9969 | 91 |
by (rtac someI2 1); |
7482 | 92 |
by (dres_inst_tac [("f", "g")] arg_cong 2); |
93 |
by (auto_tac (claset(), simpset() addsimps [prem])); |
|
94 |
qed "fst_inv_equalityI"; |
|
95 |
||
6297 | 96 |
|
97 |
Open_locale "Extend"; |
|
98 |
||
99 |
val slice_def = thm "slice_def"; |
|
100 |
||
101 |
(*** Trivial properties of f, g, h ***) |
|
102 |
||
7482 | 103 |
val good_h = rewrite_rule [good_map_def] (thm "good_h"); |
104 |
val surj_h = good_h RS conjunct1; |
|
6297 | 105 |
|
106 |
val f_def = thm "f_def"; |
|
107 |
val g_def = thm "g_def"; |
|
108 |
||
109 |
Goal "f(h(x,y)) = x"; |
|
7482 | 110 |
by (simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
6297 | 111 |
qed "f_h_eq"; |
112 |
Addsimps [f_h_eq]; |
|
113 |
||
7482 | 114 |
Goal "h(x,y) = h(x',y') ==> x=x'"; |
115 |
by (dres_inst_tac [("f", "fst o inv h")] arg_cong 1); |
|
116 |
(*FIXME: If locales worked properly we could put just "f" above*) |
|
117 |
by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
|
118 |
qed "h_inject1"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
119 |
AddDs [h_inject1]; |
6297 | 120 |
|
121 |
Goal "h(f z, g z) = z"; |
|
9345 | 122 |
by (simp_tac (simpset() addsimps [f_def, g_def, surj_h RS surj_f_inv_f]) 1); |
6297 | 123 |
qed "h_f_g_eq"; |
124 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
125 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
126 |
(** 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
|
127 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11467
diff
changeset
|
128 |
val cT = TFree ("'c", HOLogic.typeS); |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
129 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
130 |
(* "PROP P x == PROP P (h (f x, g x))" *) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
131 |
val lemma1 = Thm.combination |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
132 |
(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
|
133 |
(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
|
134 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
135 |
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
|
136 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
137 |
val lemma2 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
138 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
139 |
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
|
140 |
by (rtac lemma2 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
141 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
142 |
val lemma3 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
143 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
144 |
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
|
145 |
(*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
|
146 |
by (cut_facts_tac [surj_h] 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
147 |
by (resolve_tac prems 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
148 |
val lemma4 = result(); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
149 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
150 |
val split_extended_all = Thm.equal_intr lemma4 lemma3; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
151 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
152 |
|
6297 | 153 |
(*** extend_set: basic properties ***) |
154 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
155 |
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
|
156 |
by (simp_tac (simpset() addsimps [project_set_def]) 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
157 |
qed "project_set_iff"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
158 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
159 |
AddIffs [project_set_iff]; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
160 |
|
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
161 |
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
|
162 |
by (Blast_tac 1); |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
163 |
qed "extend_set_mono"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
164 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
165 |
Goalw [extend_set_def] "z : extend_set h A = (f z : A)"; |
7341 | 166 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
6297 | 167 |
qed "mem_extend_set_iff"; |
168 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
169 |
AddIffs [mem_extend_set_iff]; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
170 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
171 |
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
|
172 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
173 |
qed "extend_set_strict_mono"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
174 |
AddIffs [extend_set_strict_mono]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
175 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
176 |
Goalw [extend_set_def] "extend_set h {} = {}"; |
7378 | 177 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
178 |
qed "extend_set_empty"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
179 |
Addsimps [extend_set_empty]; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
180 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
181 |
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
|
182 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
183 |
qed "extend_set_eq_Collect"; |
7378 | 184 |
|
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
185 |
Goal "extend_set h {x} = {s. f s = x}"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
186 |
by Auto_tac; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
187 |
qed "extend_set_sing"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7546
diff
changeset
|
188 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
189 |
Goalw [extend_set_def] "project_set h (extend_set h C) = C"; |
7341 | 190 |
by Auto_tac; |
191 |
qed "extend_set_inverse"; |
|
192 |
Addsimps [extend_set_inverse]; |
|
193 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
194 |
Goalw [extend_set_def] "C <= extend_set h (project_set h C)"; |
7947 | 195 |
by (auto_tac (claset(), |
196 |
simpset() addsimps [split_extended_all])); |
|
197 |
by (Blast_tac 1); |
|
198 |
qed "extend_set_project_set"; |
|
199 |
||
6297 | 200 |
Goal "inj (extend_set h)"; |
7341 | 201 |
by (rtac inj_on_inverseI 1); |
202 |
by (rtac extend_set_inverse 1); |
|
6297 | 203 |
qed "inj_extend_set"; |
204 |
||
7689 | 205 |
Goalw [extend_set_def] "extend_set h UNIV = UNIV"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
206 |
by (auto_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
207 |
simpset() addsimps [split_extended_all])); |
7689 | 208 |
qed "extend_set_UNIV_eq"; |
209 |
Addsimps [standard extend_set_UNIV_eq]; |
|
210 |
||
7482 | 211 |
(*** project_set: basic properties ***) |
212 |
||
213 |
(*project_set is simply image!*) |
|
10834 | 214 |
Goal "project_set h C = f ` C"; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
215 |
by (auto_tac (claset() addIs [f_h_eq RS sym], |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
216 |
simpset() addsimps [split_extended_all])); |
7482 | 217 |
qed "project_set_eq"; |
218 |
||
219 |
(*Converse appears to fail*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
220 |
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
|
221 |
by (auto_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
222 |
simpset() addsimps [split_extended_all])); |
7482 | 223 |
qed "project_set_I"; |
224 |
||
225 |
||
226 |
(*** More laws ***) |
|
227 |
||
7341 | 228 |
(*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
|
229 |
cannot generalize to |
7341 | 230 |
project_set h (A Int B) = project_set h A Int project_set h B |
231 |
*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
232 |
Goal "project_set h ((extend_set h A) Int B) = A Int (project_set h B)"; |
7341 | 233 |
by Auto_tac; |
234 |
qed "project_set_extend_set_Int"; |
|
235 |
||
9609 | 236 |
(*Unused, but interesting?*) |
237 |
Goal "project_set h ((extend_set h A) Un B) = A Un (project_set h B)"; |
|
238 |
by Auto_tac; |
|
239 |
qed "project_set_extend_set_Un"; |
|
240 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
241 |
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
|
242 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
243 |
qed "project_set_Int_subset"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
244 |
|
7341 | 245 |
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B"; |
6297 | 246 |
by Auto_tac; |
247 |
qed "extend_set_Un_distrib"; |
|
248 |
||
7341 | 249 |
Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B"; |
6297 | 250 |
by Auto_tac; |
251 |
qed "extend_set_Int_distrib"; |
|
252 |
||
7341 | 253 |
Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"; |
254 |
by Auto_tac; |
|
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
255 |
qed "extend_set_INT_distrib"; |
6647 | 256 |
|
7341 | 257 |
Goal "extend_set h (A - B) = extend_set h A - extend_set h B"; |
6297 | 258 |
by Auto_tac; |
259 |
qed "extend_set_Diff_distrib"; |
|
260 |
||
7341 | 261 |
Goal "extend_set h (Union A) = (UN X:A. extend_set h X)"; |
6297 | 262 |
by (Blast_tac 1); |
263 |
qed "extend_set_Union"; |
|
264 |
||
7341 | 265 |
Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)"; |
6297 | 266 |
by Auto_tac; |
267 |
qed "extend_set_subset_Compl_eq"; |
|
268 |
||
7341 | 269 |
|
6297 | 270 |
(*** extend_act ***) |
271 |
||
8216 | 272 |
(*Can't strengthen it to |
273 |
((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') |
|
274 |
because h doesn't have to be injective in the 2nd argument*) |
|
6297 | 275 |
Goalw [extend_act_def] |
276 |
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"; |
|
277 |
by Auto_tac; |
|
278 |
qed "mem_extend_act_iff"; |
|
279 |
AddIffs [mem_extend_act_iff]; |
|
280 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
281 |
(*Converse fails: (z,z') would include actions that changed the g-part*) |
7341 | 282 |
Goalw [extend_act_def] |
283 |
"(z, z') : extend_act h act ==> (f z, f z') : act"; |
|
284 |
by Auto_tac; |
|
285 |
qed "extend_act_D"; |
|
286 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
287 |
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
|
288 |
"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
|
289 |
by (Blast_tac 1); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
290 |
qed "extend_act_inverse"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
291 |
Addsimps [extend_act_inverse]; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
292 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
293 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
294 |
"project_act h (Restrict C (extend_act h act)) = \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
295 |
\ Restrict (project_set h C) act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
296 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
297 |
qed "project_act_extend_act_restrict"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
298 |
Addsimps [project_act_extend_act_restrict]; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
299 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
300 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
301 |
"act' <= extend_act h act ==> project_act h act' <= act"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
302 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
303 |
qed "subset_extend_act_D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
304 |
|
6297 | 305 |
Goal "inj (extend_act h)"; |
7341 | 306 |
by (rtac inj_on_inverseI 1); |
307 |
by (rtac extend_act_inverse 1); |
|
6297 | 308 |
qed "inj_extend_act"; |
309 |
||
310 |
Goalw [extend_set_def, extend_act_def] |
|
10834 | 311 |
"extend_act h act `` (extend_set h A) = extend_set h (act `` A)"; |
6297 | 312 |
by (Force_tac 1); |
313 |
qed "extend_act_Image"; |
|
314 |
Addsimps [extend_act_Image]; |
|
315 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
316 |
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
|
317 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
318 |
qed "extend_act_strict_mono"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
319 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
320 |
AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
321 |
(*The latter theorem is (extend_act h act' = extend_act h act) = (act'=act) *) |
6297 | 322 |
|
323 |
Goalw [extend_set_def, extend_act_def] |
|
324 |
"Domain (extend_act h act) = extend_set h (Domain act)"; |
|
325 |
by (Force_tac 1); |
|
326 |
qed "Domain_extend_act"; |
|
327 |
||
7341 | 328 |
Goalw [extend_act_def] |
6297 | 329 |
"extend_act h Id = Id"; |
330 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
|
331 |
qed "extend_act_Id"; |
|
7341 | 332 |
|
333 |
Goalw [project_act_def] |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
334 |
"!!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
|
335 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
336 |
simpset() addsimps [split_extended_all]) 1); |
7341 | 337 |
qed "project_act_I"; |
338 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
339 |
Goalw [project_act_def] "project_act h Id = Id"; |
7341 | 340 |
by (Force_tac 1); |
341 |
qed "project_act_Id"; |
|
342 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
343 |
Goalw [project_act_def] |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
344 |
"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
|
345 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
346 |
simpset() addsimps [split_extended_all]) 1); |
7482 | 347 |
qed "Domain_project_act"; |
348 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
349 |
Addsimps [extend_act_Id, project_act_Id]; |
6297 | 350 |
|
351 |
||
352 |
(**** extend ****) |
|
353 |
||
354 |
(*** Basic properties ***) |
|
355 |
||
7341 | 356 |
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)"; |
6297 | 357 |
by Auto_tac; |
358 |
qed "Init_extend"; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
359 |
Addsimps [Init_extend]; |
6297 | 360 |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
361 |
Goalw [project_def] "Init (project h C F) = project_set h (Init F)"; |
7341 | 362 |
by Auto_tac; |
363 |
qed "Init_project"; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
364 |
Addsimps [Init_project]; |
7341 | 365 |
|
10834 | 366 |
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
|
367 |
by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1); |
6297 | 368 |
qed "Acts_extend"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
369 |
Addsimps [Acts_extend]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
370 |
|
10834 | 371 |
Goal "AllowedActs (extend h F) = project_act h -` AllowedActs F"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
372 |
by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
373 |
qed "AllowedActs_extend"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
374 |
Addsimps [AllowedActs_extend]; |
6297 | 375 |
|
10834 | 376 |
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
|
377 |
by (auto_tac (claset(), |
7341 | 378 |
simpset() addsimps [project_def, image_iff])); |
379 |
qed "Acts_project"; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
380 |
Addsimps [Acts_project]; |
7341 | 381 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
382 |
Goal "AllowedActs(project h C F) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
383 |
\ {act. Restrict (project_set h C) act \ |
10834 | 384 |
\ : project_act h ` Restrict C ` AllowedActs F}"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
385 |
by (simp_tac (simpset() addsimps [project_def, image_iff]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
386 |
by (stac insert_absorb 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
387 |
by (auto_tac (claset() addSIs [inst "x" "Id" bexI], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
388 |
simpset() addsimps [project_act_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
389 |
qed "AllowedActs_project"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
390 |
Addsimps [AllowedActs_project]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
391 |
|
10834 | 392 |
Goal "Allowed (extend h F) = project h UNIV -` Allowed F"; |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
393 |
by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
394 |
by (Blast_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
395 |
qed "Allowed_extend"; |
6297 | 396 |
|
397 |
Goalw [SKIP_def] "extend h SKIP = SKIP"; |
|
398 |
by (rtac program_equalityI 1); |
|
7341 | 399 |
by Auto_tac; |
400 |
qed "extend_SKIP"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
401 |
Addsimps [export extend_SKIP]; |
7341 | 402 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
403 |
Goal "project_set h UNIV = UNIV"; |
7537 | 404 |
by Auto_tac; |
405 |
qed "project_set_UNIV"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
406 |
Addsimps [project_set_UNIV]; |
7537 | 407 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
408 |
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
|
409 |
by (Blast_tac 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
410 |
qed "project_set_Union"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
411 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
412 |
(*Converse FAILS: the extended state contributing to project_set h C |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
413 |
may not coincide with the one contributing to project_act h act*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
414 |
Goal "project_act h (Restrict C act) <= \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
415 |
\ Restrict (project_set h C) (project_act h act)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
416 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
417 |
qed "project_act_Restrict_subset"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
418 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
419 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
420 |
Goal "project_act h (Restrict C Id) = Restrict (project_set h C) Id"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
421 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
422 |
qed "project_act_Restrict_Id_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
423 |
|
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
424 |
Goal "project h C (extend h F) = \ |
10834 | 425 |
\ mk_program (Init F, Restrict (project_set h C) ` Acts F, \ |
426 |
\ {act. Restrict (project_set h C) act : project_act h ` Restrict C ` (project_act h -` AllowedActs F)})"; |
|
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
427 |
by (rtac program_equalityI 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9345
diff
changeset
|
428 |
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2); |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
429 |
by (Simp_tac 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
430 |
by (simp_tac (simpset() addsimps [project_def]) 1); |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
431 |
qed "project_extend_eq"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
432 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
433 |
Goal "project h UNIV (extend h F) = F"; |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
434 |
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
|
435 |
subset_UNIV RS subset_trans RS Restrict_triv]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
436 |
by (rtac program_equalityI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
437 |
by (ALLGOALS Simp_tac); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
438 |
by (stac insert_absorb 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
439 |
by (simp_tac (simpset() addsimps [inst "x" "Id" bexI]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
440 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
441 |
by (rename_tac "act" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
442 |
by (res_inst_tac [("x","extend_act h act")] bexI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
443 |
by Auto_tac; |
7341 | 444 |
qed "extend_inverse"; |
445 |
Addsimps [extend_inverse]; |
|
6297 | 446 |
|
447 |
Goal "inj (extend h)"; |
|
7341 | 448 |
by (rtac inj_on_inverseI 1); |
449 |
by (rtac extend_inverse 1); |
|
6297 | 450 |
qed "inj_extend"; |
451 |
||
452 |
Goal "extend h (F Join G) = extend h F Join extend h G"; |
|
453 |
by (rtac program_equalityI 1); |
|
7537 | 454 |
by (simp_tac (simpset() addsimps [image_Un]) 2); |
6297 | 455 |
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
456 |
by Auto_tac; |
6297 | 457 |
qed "extend_Join"; |
458 |
Addsimps [extend_Join]; |
|
459 |
||
6647 | 460 |
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))"; |
461 |
by (rtac program_equalityI 1); |
|
7537 | 462 |
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
|
463 |
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
464 |
by Auto_tac; |
6647 | 465 |
qed "extend_JN"; |
466 |
Addsimps [extend_JN]; |
|
467 |
||
7689 | 468 |
(** These monotonicity results look natural but are UNUSED **) |
469 |
||
470 |
Goal "F <= G ==> extend h F <= extend h G"; |
|
471 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
472 |
by Auto_tac; |
|
473 |
qed "extend_mono"; |
|
474 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
475 |
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
|
476 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
477 |
by (Blast_tac 1); |
7689 | 478 |
qed "project_mono"; |
479 |
||
480 |
||
6536 | 481 |
(*** Safety: co, stable ***) |
6297 | 482 |
|
6536 | 483 |
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \ |
484 |
\ (F : A co B)"; |
|
6297 | 485 |
by (simp_tac (simpset() addsimps [constrains_def]) 1); |
486 |
qed "extend_constrains"; |
|
487 |
||
488 |
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)"; |
|
489 |
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1); |
|
490 |
qed "extend_stable"; |
|
491 |
||
492 |
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)"; |
|
493 |
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1); |
|
494 |
qed "extend_invariant"; |
|
495 |
||
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
496 |
(*Projects the state predicates in the property satisfied by extend h F. |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
497 |
Converse fails: A and B may differ in their extra variables*) |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
498 |
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
|
499 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
500 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
501 |
qed "extend_constrains_project_set"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
502 |
|
8041 | 503 |
Goal "extend h F : stable A ==> F : stable (project_set h A)"; |
504 |
by (asm_full_simp_tac |
|
505 |
(simpset() addsimps [stable_def, extend_constrains_project_set]) 1); |
|
506 |
qed "extend_stable_project_set"; |
|
507 |
||
7341 | 508 |
|
509 |
(*** Weak safety primitives: Co, Stable ***) |
|
6297 | 510 |
|
511 |
Goal "p : reachable (extend h F) ==> f p : reachable F"; |
|
512 |
by (etac reachable.induct 1); |
|
513 |
by (auto_tac |
|
514 |
(claset() addIs reachable.intrs, |
|
7341 | 515 |
simpset() addsimps [extend_act_def, image_iff])); |
6297 | 516 |
qed "reachable_extend_f"; |
517 |
||
518 |
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F"; |
|
519 |
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1); |
|
520 |
qed "h_reachable_extend"; |
|
521 |
||
522 |
Goalw [extend_set_def] |
|
523 |
"reachable (extend h F) = extend_set h (reachable F)"; |
|
524 |
by (rtac equalityI 1); |
|
525 |
by (force_tac (claset() addIs [h_f_g_eq RS sym] |
|
526 |
addSDs [reachable_extend_f], |
|
527 |
simpset()) 1); |
|
528 |
by (Clarify_tac 1); |
|
529 |
by (etac reachable.induct 1); |
|
530 |
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, |
|
531 |
simpset()))); |
|
532 |
qed "reachable_extend_eq"; |
|
533 |
||
6536 | 534 |
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \ |
535 |
\ (F : A Co B)"; |
|
6297 | 536 |
by (simp_tac |
537 |
(simpset() addsimps [Constrains_def, reachable_extend_eq, |
|
538 |
extend_constrains, extend_set_Int_distrib RS sym]) 1); |
|
539 |
qed "extend_Constrains"; |
|
540 |
||
541 |
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)"; |
|
542 |
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1); |
|
543 |
qed "extend_Stable"; |
|
544 |
||
6647 | 545 |
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)"; |
546 |
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1); |
|
547 |
qed "extend_Always"; |
|
548 |
||
6297 | 549 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
550 |
(** Safety and "project" **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
551 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
552 |
(** projection: monotonicity for safety **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
553 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
554 |
Goal "D <= C ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
555 |
\ 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
|
556 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
557 |
qed "project_act_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
558 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
559 |
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
|
560 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
561 |
by (dtac project_act_mono 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
562 |
by (Blast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
563 |
qed "project_constrains_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
564 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
565 |
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
|
566 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
567 |
(simpset() addsimps [stable_def, project_constrains_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
568 |
qed "project_stable_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
569 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
570 |
(*Key lemma used in several proofs about project and co*) |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
571 |
Goalw [constrains_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
572 |
"(project h C F : A co B) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
573 |
\ (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
|
574 |
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
|
575 |
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
|
576 |
(*the <== direction*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
577 |
by (rewtac project_act_def); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
578 |
by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
579 |
qed "project_constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
580 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
581 |
Goalw [stable_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
582 |
"(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
|
583 |
by (simp_tac (simpset() addsimps [project_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
584 |
qed "project_stable"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
585 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
586 |
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
|
587 |
by (dtac (project_stable RS iffD2) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
588 |
by (blast_tac (claset() addIs [project_stable_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
589 |
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
|
590 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
591 |
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
|
592 |
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
|
593 |
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
|
594 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
595 |
(*Strange (look at occurrences of C) but used in leadsETo proofs*) |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
596 |
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
|
597 |
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
|
598 |
project_act_def]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
599 |
by (Blast_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
600 |
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
|
601 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
602 |
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
|
603 |
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
|
604 |
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
|
605 |
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
|
606 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
607 |
|
6297 | 608 |
(*** Progress: transient, ensures ***) |
609 |
||
610 |
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
|
611 |
by (auto_tac (claset(), |
|
612 |
simpset() addsimps [transient_def, extend_set_subset_Compl_eq, |
|
613 |
Domain_extend_act])); |
|
614 |
qed "extend_transient"; |
|
615 |
||
6536 | 616 |
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \ |
617 |
\ (F : A ensures B)"; |
|
6297 | 618 |
by (simp_tac |
619 |
(simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
620 |
extend_set_Un_distrib RS sym, |
|
621 |
extend_set_Diff_distrib RS sym]) 1); |
|
622 |
qed "extend_ensures"; |
|
623 |
||
6536 | 624 |
Goal "F : A leadsTo B \ |
625 |
\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"; |
|
6297 | 626 |
by (etac leadsTo_induct 1); |
627 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3); |
|
628 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
629 |
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1); |
|
630 |
qed "leadsTo_imp_extend_leadsTo"; |
|
631 |
||
632 |
(*** Proving the converse takes some doing! ***) |
|
633 |
||
8111 | 634 |
Goal "(x : slice C y) = (h(x,y) : C)"; |
635 |
by (simp_tac (simpset() addsimps [slice_def]) 1); |
|
636 |
qed "slice_iff"; |
|
637 |
||
638 |
AddIffs [slice_iff]; |
|
639 |
||
640 |
Goal "slice (Union S) y = (UN x:S. slice x y)"; |
|
6297 | 641 |
by Auto_tac; |
642 |
qed "slice_Union"; |
|
643 |
||
8111 | 644 |
Goal "slice (extend_set h A) y = A"; |
6297 | 645 |
by Auto_tac; |
646 |
qed "slice_extend_set"; |
|
647 |
||
8111 | 648 |
Goal "project_set h A = (UN y. slice A y)"; |
6297 | 649 |
by Auto_tac; |
7482 | 650 |
qed "project_set_is_UN_slice"; |
6297 | 651 |
|
8111 | 652 |
Goalw [transient_def] "extend h F : transient A ==> F : transient (slice A y)"; |
6297 | 653 |
by Auto_tac; |
654 |
by (rtac bexI 1); |
|
655 |
by Auto_tac; |
|
656 |
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1); |
|
657 |
qed "extend_transient_slice"; |
|
658 |
||
8111 | 659 |
(*Converse?*) |
660 |
Goal "extend h F : A co B ==> F : (slice A y) co (slice B y)"; |
|
661 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
|
662 |
qed "extend_constrains_slice"; |
|
663 |
||
7482 | 664 |
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"; |
8111 | 665 |
by (auto_tac (claset(), |
666 |
simpset() addsimps [ensures_def, extend_constrains, |
|
667 |
extend_transient])); |
|
668 |
by (etac (extend_transient_slice RS transient_strengthen) 2); |
|
669 |
by (etac (extend_constrains_slice RS constrains_weaken) 1); |
|
670 |
by Auto_tac; |
|
6297 | 671 |
qed "extend_ensures_slice"; |
672 |
||
7482 | 673 |
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"; |
674 |
by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1); |
|
6297 | 675 |
by (blast_tac (claset() addIs [leadsTo_UN]) 1); |
8111 | 676 |
qed "leadsTo_slice_project_set"; |
6297 | 677 |
|
6536 | 678 |
Goal "extend h F : AU leadsTo BU \ |
7482 | 679 |
\ ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"; |
6297 | 680 |
by (etac leadsTo_induct 1); |
8111 | 681 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, slice_Union]) 3); |
682 |
by (blast_tac (claset() addIs [leadsTo_slice_project_set, leadsTo_Trans]) 2); |
|
6297 | 683 |
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1); |
684 |
qed_spec_mp "extend_leadsTo_slice"; |
|
685 |
||
6536 | 686 |
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \ |
687 |
\ (F : A leadsTo B)"; |
|
6297 | 688 |
by Safe_tac; |
689 |
by (etac leadsTo_imp_extend_leadsTo 2); |
|
690 |
by (dtac extend_leadsTo_slice 1); |
|
691 |
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
|
692 |
qed "extend_leadsTo"; |
6297 | 693 |
|
6536 | 694 |
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \ |
695 |
\ (F : A LeadsTo B)"; |
|
6454 | 696 |
by (simp_tac |
697 |
(simpset() addsimps [LeadsTo_def, reachable_extend_eq, |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
698 |
extend_leadsTo, extend_set_Int_distrib RS sym]) 1); |
6454 | 699 |
qed "extend_LeadsTo"; |
700 |
||
6297 | 701 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
702 |
(*** preserves ***) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
703 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
704 |
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
|
705 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
706 |
simpset() addsimps [preserves_def, project_stable_I, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
707 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
708 |
qed "project_preserves_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
709 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
710 |
(*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
|
711 |
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
|
712 |
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
|
713 |
qed "project_preserves_id_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
714 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
715 |
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
|
716 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
717 |
simpset() addsimps [preserves_def, extend_stable RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
718 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
719 |
qed "extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
720 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
721 |
Goal "inj h ==> (extend h G : preserves g)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
722 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
723 |
simpset() addsimps [preserves_def, extend_def, extend_act_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
724 |
stable_def, constrains_def, g_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
725 |
qed "inj_extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
726 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
727 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
728 |
(*** Guarantees ***) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
729 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
730 |
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
|
731 |
by (rtac program_equalityI 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
732 |
by (simp_tac (simpset() addsimps [image_eq_UN, UN_Un]) 2); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
733 |
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
734 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
735 |
qed "project_extend_Join"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
736 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
737 |
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
|
738 |
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
|
739 |
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
|
740 |
qed "extend_Join_eq_extend_D"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
741 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
742 |
(** Strong precondition and postcondition; only useful when |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
743 |
the old and new state sets are in bijection **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
744 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
745 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
746 |
Goal "extend h F ok G ==> F ok project h UNIV G"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
747 |
by (auto_tac (claset(), simpset() addsimps [ok_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
748 |
by (dtac subsetD 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
749 |
by (auto_tac (claset() addSIs [rev_image_eqI], simpset())); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
750 |
qed "ok_extend_imp_ok_project"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
751 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
752 |
Goal "(extend h F ok extend h G) = (F ok G)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
753 |
by (auto_tac (claset(), simpset() addsimps [ok_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
754 |
qed "ok_extend_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
755 |
|
11467 | 756 |
Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)"; |
757 |
by Safe_tac; |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
758 |
by (dres_inst_tac [("x","i")] bspec 1); |
11467 | 759 |
by (dres_inst_tac [("x","j")] bspec 2); |
760 |
by (REPEAT (Force_tac 1)); |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
761 |
qed "OK_extend_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
762 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
763 |
Goal "F : X guarantees Y ==> \ |
10834 | 764 |
\ extend h F : (extend h ` X) guarantees (extend h ` Y)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
765 |
by (rtac guaranteesI 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
766 |
by (Clarify_tac 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
767 |
by (blast_tac (claset() addDs [ok_extend_imp_ok_project, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
768 |
extend_Join_eq_extend_D, guaranteesD]) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
769 |
qed "guarantees_imp_extend_guarantees"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
770 |
|
10834 | 771 |
Goal "extend h F : (extend h ` X) guarantees (extend h ` Y) \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
772 |
\ ==> F : X guarantees Y"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
773 |
by (auto_tac (claset(), simpset() addsimps [guar_def])); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
774 |
by (dres_inst_tac [("x", "extend h G")] spec 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
775 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
776 |
(simpset() delsimps [extend_Join] |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
777 |
addsimps [extend_Join RS sym, ok_extend_iff, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
778 |
inj_extend RS inj_image_mem_iff]) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
779 |
qed "extend_guarantees_imp_guarantees"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
780 |
|
10834 | 781 |
Goal "(extend h F : (extend h ` X) guarantees (extend h ` Y)) = \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9969
diff
changeset
|
782 |
\ (F : X guarantees Y)"; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
783 |
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
784 |
extend_guarantees_imp_guarantees]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
785 |
qed "extend_guarantees_eq"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
786 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
787 |
|
6297 | 788 |
Close_locale "Extend"; |
7482 | 789 |
|
790 |
(*Close_locale should do this! |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
791 |
Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_Image]; |
7482 | 792 |
Delrules [make_elim h_inject1]; |
793 |
*) |