author | oheimb |
Fri, 14 Jul 2000 16:32:44 +0200 | |
changeset 9345 | 2f5f6824f888 |
parent 9337 | 58bd51302b21 |
child 9403 | aad13b59b8d9 |
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 |] \ |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
53 |
\ ==> Restrict A r : Restrict A `` RR"; |
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 |
|
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8251
diff
changeset
|
61 |
Goal "(Restrict A r) ^^ B = r ^^ (A Int B)"; |
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 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
68 |
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
|
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); |
|
7499 | 91 |
by (rtac selectI2 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 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
128 |
val cT = TFree ("'c", ["term"]); |
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!*) |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
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 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
236 |
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
|
237 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
238 |
qed "project_set_Int_subset"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
239 |
|
7341 | 240 |
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B"; |
6297 | 241 |
by Auto_tac; |
242 |
qed "extend_set_Un_distrib"; |
|
243 |
||
7341 | 244 |
Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B"; |
6297 | 245 |
by Auto_tac; |
246 |
qed "extend_set_Int_distrib"; |
|
247 |
||
7341 | 248 |
Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"; |
249 |
by Auto_tac; |
|
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
250 |
qed "extend_set_INT_distrib"; |
6647 | 251 |
|
7341 | 252 |
Goal "extend_set h (A - B) = extend_set h A - extend_set h B"; |
6297 | 253 |
by Auto_tac; |
254 |
qed "extend_set_Diff_distrib"; |
|
255 |
||
7341 | 256 |
Goal "extend_set h (Union A) = (UN X:A. extend_set h X)"; |
6297 | 257 |
by (Blast_tac 1); |
258 |
qed "extend_set_Union"; |
|
259 |
||
7341 | 260 |
Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)"; |
6297 | 261 |
by Auto_tac; |
262 |
qed "extend_set_subset_Compl_eq"; |
|
263 |
||
7341 | 264 |
|
6297 | 265 |
(*** extend_act ***) |
266 |
||
8216 | 267 |
(*Can't strengthen it to |
268 |
((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') |
|
269 |
because h doesn't have to be injective in the 2nd argument*) |
|
6297 | 270 |
Goalw [extend_act_def] |
271 |
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"; |
|
272 |
by Auto_tac; |
|
273 |
qed "mem_extend_act_iff"; |
|
274 |
AddIffs [mem_extend_act_iff]; |
|
275 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
276 |
(*Converse fails: (z,z') would include actions that changed the g-part*) |
7341 | 277 |
Goalw [extend_act_def] |
278 |
"(z, z') : extend_act h act ==> (f z, f z') : act"; |
|
279 |
by Auto_tac; |
|
280 |
qed "extend_act_D"; |
|
281 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
282 |
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
|
283 |
"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
|
284 |
by (Blast_tac 1); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
285 |
qed "extend_act_inverse"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
286 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
287 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
288 |
"project_act h (Restrict C (extend_act h act)) = \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
289 |
\ Restrict (project_set h C) act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
290 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
291 |
qed "project_act_extend_act_restrict"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
292 |
Addsimps [project_act_extend_act_restrict]; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
293 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
294 |
Goalw [extend_act_def, project_act_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
295 |
"act' <= extend_act h act ==> project_act h act' <= act"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
296 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
297 |
qed "subset_extend_act_D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
298 |
|
6297 | 299 |
Goal "inj (extend_act h)"; |
7341 | 300 |
by (rtac inj_on_inverseI 1); |
301 |
by (rtac extend_act_inverse 1); |
|
6297 | 302 |
qed "inj_extend_act"; |
303 |
||
304 |
Goalw [extend_set_def, extend_act_def] |
|
305 |
"extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)"; |
|
306 |
by (Force_tac 1); |
|
307 |
qed "extend_act_Image"; |
|
308 |
Addsimps [extend_act_Image]; |
|
309 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
310 |
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
|
311 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
312 |
qed "extend_act_strict_mono"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
313 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
314 |
AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
315 |
(*The latter theorem is (extend_act h act' = extend_act h act) = (act'=act) *) |
6297 | 316 |
|
317 |
Goalw [extend_set_def, extend_act_def] |
|
318 |
"Domain (extend_act h act) = extend_set h (Domain act)"; |
|
319 |
by (Force_tac 1); |
|
320 |
qed "Domain_extend_act"; |
|
321 |
||
7341 | 322 |
Goalw [extend_act_def] |
6297 | 323 |
"extend_act h Id = Id"; |
324 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
|
325 |
qed "extend_act_Id"; |
|
7341 | 326 |
|
327 |
Goalw [project_act_def] |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
328 |
"!!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
|
329 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
330 |
simpset() addsimps [split_extended_all]) 1); |
7341 | 331 |
qed "project_act_I"; |
332 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
333 |
Goalw [project_act_def] "project_act h Id = Id"; |
7341 | 334 |
by (Force_tac 1); |
335 |
qed "project_act_Id"; |
|
336 |
||
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
337 |
Goalw [project_act_def] |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
338 |
"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
|
339 |
by (force_tac (claset(), |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
340 |
simpset() addsimps [split_extended_all]) 1); |
7482 | 341 |
qed "Domain_project_act"; |
342 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
343 |
Addsimps [extend_act_Id]; |
6297 | 344 |
|
345 |
||
346 |
(**** extend ****) |
|
347 |
||
348 |
(*** Basic properties ***) |
|
349 |
||
7341 | 350 |
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)"; |
6297 | 351 |
by Auto_tac; |
352 |
qed "Init_extend"; |
|
353 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
354 |
Goalw [project_def] "Init (project h C F) = project_set h (Init F)"; |
7341 | 355 |
by Auto_tac; |
356 |
qed "Init_project"; |
|
357 |
||
6297 | 358 |
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
|
359 |
by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1); |
6297 | 360 |
qed "Acts_extend"; |
361 |
||
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
362 |
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
|
363 |
by (auto_tac (claset(), |
7341 | 364 |
simpset() addsimps [project_def, image_iff])); |
365 |
qed "Acts_project"; |
|
366 |
||
367 |
Addsimps [Init_extend, Init_project, Acts_extend, Acts_project]; |
|
6297 | 368 |
|
369 |
Goalw [SKIP_def] "extend h SKIP = SKIP"; |
|
370 |
by (rtac program_equalityI 1); |
|
7341 | 371 |
by Auto_tac; |
372 |
qed "extend_SKIP"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
373 |
Addsimps [export extend_SKIP]; |
7341 | 374 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
375 |
Goal "project_set h UNIV = UNIV"; |
7537 | 376 |
by Auto_tac; |
377 |
qed "project_set_UNIV"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
378 |
Addsimps [project_set_UNIV]; |
7537 | 379 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
380 |
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
|
381 |
by (Blast_tac 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
382 |
qed "project_set_Union"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
383 |
|
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
384 |
Goal "project h C (extend h F) = \ |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
385 |
\ mk_program (Init F, Restrict (project_set h C) `` Acts F)"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
386 |
by (rtac program_equalityI 1); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
387 |
by (asm_simp_tac (simpset() addsimps [image_eq_UN, |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
388 |
project_act_extend_act_restrict]) 2); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
389 |
by (Simp_tac 1); |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
390 |
qed "project_extend_eq"; |
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
391 |
|
7537 | 392 |
(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*) |
393 |
Goal "UNIV <= project_set h C \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
394 |
\ ==> project h C (extend h F) = F"; |
7915
c7fd7eb3b0ef
ALMOST working version: LocalTo results commented out
paulson
parents:
7880
diff
changeset
|
395 |
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
|
396 |
subset_UNIV RS subset_trans RS Restrict_triv]) 1); |
7341 | 397 |
qed "extend_inverse"; |
398 |
Addsimps [extend_inverse]; |
|
6297 | 399 |
|
400 |
Goal "inj (extend h)"; |
|
7341 | 401 |
by (rtac inj_on_inverseI 1); |
402 |
by (rtac extend_inverse 1); |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8055
diff
changeset
|
403 |
by (Force_tac 1); |
6297 | 404 |
qed "inj_extend"; |
405 |
||
406 |
Goal "extend h (F Join G) = extend h F Join extend h G"; |
|
407 |
by (rtac program_equalityI 1); |
|
7537 | 408 |
by (simp_tac (simpset() addsimps [image_Un]) 2); |
6297 | 409 |
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1); |
410 |
qed "extend_Join"; |
|
411 |
Addsimps [extend_Join]; |
|
412 |
||
6647 | 413 |
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))"; |
414 |
by (rtac program_equalityI 1); |
|
7537 | 415 |
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
|
416 |
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1); |
6647 | 417 |
qed "extend_JN"; |
418 |
Addsimps [extend_JN]; |
|
419 |
||
7689 | 420 |
(** These monotonicity results look natural but are UNUSED **) |
421 |
||
422 |
Goal "F <= G ==> extend h F <= extend h G"; |
|
423 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
424 |
by Auto_tac; |
|
425 |
qed "extend_mono"; |
|
426 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
427 |
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
|
428 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
7689 | 429 |
by Auto_tac; |
430 |
qed "project_mono"; |
|
431 |
||
432 |
||
6536 | 433 |
(*** Safety: co, stable ***) |
6297 | 434 |
|
6536 | 435 |
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \ |
436 |
\ (F : A co B)"; |
|
6297 | 437 |
by (simp_tac (simpset() addsimps [constrains_def]) 1); |
438 |
qed "extend_constrains"; |
|
439 |
||
440 |
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)"; |
|
441 |
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1); |
|
442 |
qed "extend_stable"; |
|
443 |
||
444 |
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)"; |
|
445 |
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1); |
|
446 |
qed "extend_invariant"; |
|
447 |
||
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
448 |
(*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
|
449 |
Converse fails: A and B may differ in their extra variables*) |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
450 |
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
|
451 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
452 |
by (Force_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
453 |
qed "extend_constrains_project_set"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
454 |
|
8041 | 455 |
Goal "extend h F : stable A ==> F : stable (project_set h A)"; |
456 |
by (asm_full_simp_tac |
|
457 |
(simpset() addsimps [stable_def, extend_constrains_project_set]) 1); |
|
458 |
qed "extend_stable_project_set"; |
|
459 |
||
7341 | 460 |
|
461 |
(*** Weak safety primitives: Co, Stable ***) |
|
6297 | 462 |
|
463 |
Goal "p : reachable (extend h F) ==> f p : reachable F"; |
|
464 |
by (etac reachable.induct 1); |
|
465 |
by (auto_tac |
|
466 |
(claset() addIs reachable.intrs, |
|
7341 | 467 |
simpset() addsimps [extend_act_def, image_iff])); |
6297 | 468 |
qed "reachable_extend_f"; |
469 |
||
470 |
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F"; |
|
471 |
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1); |
|
472 |
qed "h_reachable_extend"; |
|
473 |
||
474 |
Goalw [extend_set_def] |
|
475 |
"reachable (extend h F) = extend_set h (reachable F)"; |
|
476 |
by (rtac equalityI 1); |
|
477 |
by (force_tac (claset() addIs [h_f_g_eq RS sym] |
|
478 |
addSDs [reachable_extend_f], |
|
479 |
simpset()) 1); |
|
480 |
by (Clarify_tac 1); |
|
481 |
by (etac reachable.induct 1); |
|
482 |
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, |
|
483 |
simpset()))); |
|
484 |
qed "reachable_extend_eq"; |
|
485 |
||
6536 | 486 |
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \ |
487 |
\ (F : A Co B)"; |
|
6297 | 488 |
by (simp_tac |
489 |
(simpset() addsimps [Constrains_def, reachable_extend_eq, |
|
490 |
extend_constrains, extend_set_Int_distrib RS sym]) 1); |
|
491 |
qed "extend_Constrains"; |
|
492 |
||
493 |
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)"; |
|
494 |
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1); |
|
495 |
qed "extend_Stable"; |
|
496 |
||
6647 | 497 |
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)"; |
498 |
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1); |
|
499 |
qed "extend_Always"; |
|
500 |
||
6297 | 501 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
502 |
(** Safety and "project" **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
503 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
504 |
(** projection: monotonicity for safety **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
505 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
506 |
Goal "D <= C ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
507 |
\ 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
|
508 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
509 |
qed "project_act_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
510 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
511 |
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
|
512 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
513 |
by (dtac project_act_mono 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
514 |
by (Blast_tac 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
515 |
qed "project_constrains_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
516 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
517 |
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
|
518 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
519 |
(simpset() addsimps [stable_def, project_constrains_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
520 |
qed "project_stable_mono"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
521 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
522 |
(*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
|
523 |
Goalw [constrains_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
524 |
"(project h C F : A co B) = \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
525 |
\ (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
|
526 |
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
|
527 |
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
|
528 |
(*the <== direction*) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
529 |
by (rewtac project_act_def); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
530 |
by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
531 |
qed "project_constrains"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
532 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
533 |
Goalw [stable_def] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
534 |
"(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
|
535 |
by (simp_tac (simpset() addsimps [project_constrains]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
536 |
qed "project_stable"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
537 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
538 |
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
|
539 |
by (dtac (project_stable RS iffD2) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
540 |
by (blast_tac (claset() addIs [project_stable_mono]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
541 |
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
|
542 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
543 |
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
|
544 |
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
|
545 |
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
|
546 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
547 |
(*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
|
548 |
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
|
549 |
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
|
550 |
project_act_def]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
551 |
by (Blast_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
552 |
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
|
553 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
554 |
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
|
555 |
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
|
556 |
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
|
557 |
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
|
558 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8111
diff
changeset
|
559 |
|
6297 | 560 |
(*** Progress: transient, ensures ***) |
561 |
||
562 |
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
|
563 |
by (auto_tac (claset(), |
|
564 |
simpset() addsimps [transient_def, extend_set_subset_Compl_eq, |
|
565 |
Domain_extend_act])); |
|
566 |
qed "extend_transient"; |
|
567 |
||
6536 | 568 |
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \ |
569 |
\ (F : A ensures B)"; |
|
6297 | 570 |
by (simp_tac |
571 |
(simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
572 |
extend_set_Un_distrib RS sym, |
|
573 |
extend_set_Diff_distrib RS sym]) 1); |
|
574 |
qed "extend_ensures"; |
|
575 |
||
6536 | 576 |
Goal "F : A leadsTo B \ |
577 |
\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"; |
|
6297 | 578 |
by (etac leadsTo_induct 1); |
579 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3); |
|
580 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
581 |
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1); |
|
582 |
qed "leadsTo_imp_extend_leadsTo"; |
|
583 |
||
584 |
(*** Proving the converse takes some doing! ***) |
|
585 |
||
8111 | 586 |
Goal "(x : slice C y) = (h(x,y) : C)"; |
587 |
by (simp_tac (simpset() addsimps [slice_def]) 1); |
|
588 |
qed "slice_iff"; |
|
589 |
||
590 |
AddIffs [slice_iff]; |
|
591 |
||
592 |
Goal "slice (Union S) y = (UN x:S. slice x y)"; |
|
6297 | 593 |
by Auto_tac; |
594 |
qed "slice_Union"; |
|
595 |
||
8111 | 596 |
Goal "slice (extend_set h A) y = A"; |
6297 | 597 |
by Auto_tac; |
598 |
qed "slice_extend_set"; |
|
599 |
||
8111 | 600 |
Goal "project_set h A = (UN y. slice A y)"; |
6297 | 601 |
by Auto_tac; |
7482 | 602 |
qed "project_set_is_UN_slice"; |
6297 | 603 |
|
8111 | 604 |
Goalw [transient_def] "extend h F : transient A ==> F : transient (slice A y)"; |
6297 | 605 |
by Auto_tac; |
606 |
by (rtac bexI 1); |
|
607 |
by Auto_tac; |
|
608 |
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1); |
|
609 |
qed "extend_transient_slice"; |
|
610 |
||
8111 | 611 |
(*Converse?*) |
612 |
Goal "extend h F : A co B ==> F : (slice A y) co (slice B y)"; |
|
613 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
|
614 |
qed "extend_constrains_slice"; |
|
615 |
||
7482 | 616 |
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"; |
8111 | 617 |
by (auto_tac (claset(), |
618 |
simpset() addsimps [ensures_def, extend_constrains, |
|
619 |
extend_transient])); |
|
620 |
by (etac (extend_transient_slice RS transient_strengthen) 2); |
|
621 |
by (etac (extend_constrains_slice RS constrains_weaken) 1); |
|
622 |
by Auto_tac; |
|
6297 | 623 |
qed "extend_ensures_slice"; |
624 |
||
7482 | 625 |
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"; |
626 |
by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1); |
|
6297 | 627 |
by (blast_tac (claset() addIs [leadsTo_UN]) 1); |
8111 | 628 |
qed "leadsTo_slice_project_set"; |
6297 | 629 |
|
6536 | 630 |
Goal "extend h F : AU leadsTo BU \ |
7482 | 631 |
\ ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"; |
6297 | 632 |
by (etac leadsTo_induct 1); |
8111 | 633 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, slice_Union]) 3); |
634 |
by (blast_tac (claset() addIs [leadsTo_slice_project_set, leadsTo_Trans]) 2); |
|
6297 | 635 |
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1); |
636 |
qed_spec_mp "extend_leadsTo_slice"; |
|
637 |
||
6536 | 638 |
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \ |
639 |
\ (F : A leadsTo B)"; |
|
6297 | 640 |
by Safe_tac; |
641 |
by (etac leadsTo_imp_extend_leadsTo 2); |
|
642 |
by (dtac extend_leadsTo_slice 1); |
|
643 |
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
|
644 |
qed "extend_leadsTo"; |
6297 | 645 |
|
6536 | 646 |
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \ |
647 |
\ (F : A LeadsTo B)"; |
|
6454 | 648 |
by (simp_tac |
649 |
(simpset() addsimps [LeadsTo_def, reachable_extend_eq, |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
650 |
extend_leadsTo, extend_set_Int_distrib RS sym]) 1); |
6454 | 651 |
qed "extend_LeadsTo"; |
652 |
||
6297 | 653 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
654 |
(*** preserves ***) |
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 "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
|
657 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
658 |
simpset() addsimps [preserves_def, project_stable_I, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
659 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
660 |
qed "project_preserves_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
661 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
662 |
(*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
|
663 |
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
|
664 |
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
|
665 |
qed "project_preserves_id_I"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
666 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
667 |
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
|
668 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
669 |
simpset() addsimps [preserves_def, extend_stable RS sym, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
670 |
extend_set_eq_Collect])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
671 |
qed "extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
672 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
673 |
Goal "inj h ==> (extend h G : preserves g)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
674 |
by (auto_tac (claset(), |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
675 |
simpset() addsimps [preserves_def, extend_def, extend_act_def, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
676 |
stable_def, constrains_def, g_def])); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
677 |
qed "inj_extend_preserves"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
678 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
679 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
680 |
(*** Guarantees ***) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
681 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
682 |
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
|
683 |
by (rtac program_equalityI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
684 |
by (asm_simp_tac |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
685 |
(simpset() addsimps [image_eq_UN, UN_Un, extend_act_inverse]) 2); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
686 |
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
|
687 |
qed "project_extend_Join"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
688 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
689 |
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
|
690 |
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
|
691 |
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
|
692 |
qed "extend_Join_eq_extend_D"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
693 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
694 |
(** Strong precondition and postcondition; only useful when |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
695 |
the old and new state sets are in bijection **) |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
696 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
697 |
Goal "F : X guarantees[v] Y ==> \ |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
698 |
\ 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
|
699 |
by (rtac guaranteesI 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
700 |
by Auto_tac; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
701 |
by (blast_tac (claset() addIs [project_preserves_I] |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
702 |
addDs [extend_Join_eq_extend_D, guaranteesD]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
703 |
qed "guarantees_imp_extend_guarantees"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
704 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
705 |
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
|
706 |
\ ==> F : X guarantees[v] Y"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
707 |
by (auto_tac (claset(), simpset() addsimps [guar_def])); |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
708 |
by (dres_inst_tac [("x", "extend h G")] bspec 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
709 |
by (asm_full_simp_tac |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
710 |
(simpset() delsimps [extend_Join] |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
711 |
addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 2); |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
712 |
by (asm_simp_tac (simpset() addsimps [extend_preserves]) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
713 |
qed "extend_guarantees_imp_guarantees"; |
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 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
|
716 |
\ (F : X guarantees[v] Y)"; |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
717 |
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
718 |
extend_guarantees_imp_guarantees]) 1); |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
719 |
qed "extend_guarantees_eq"; |
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 |
|
6297 | 722 |
Close_locale "Extend"; |
7482 | 723 |
|
724 |
(*Close_locale should do this! |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
725 |
Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_Image]; |
7482 | 726 |
Delrules [make_elim h_inject1]; |
727 |
*) |