author | paulson |
Mon, 18 Oct 1999 15:18:24 +0200 | |
changeset 7878 | 43b03d412b82 |
parent 7841 | 65d91d13fc13 |
child 7880 | 62fb24e28e5e |
permissions | -rw-r--r-- |
7630 | 1 |
(* Title: HOL/UNITY/Project.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Projections of state sets (also of actions and programs) |
|
7 |
||
8 |
Inheritance of GUARANTEES properties under extension |
|
9 |
*) |
|
10 |
||
11 |
Open_locale "Extend"; |
|
12 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
13 |
(** projection: monotonicity for safety **) |
7630 | 14 |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
15 |
Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
16 |
by (auto_tac (claset(), simpset() addsimps [project_act_def])); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
17 |
qed "project_act_mono"; |
7630 | 18 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
19 |
Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B"; |
7630 | 20 |
by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
7689 | 21 |
by (dtac project_act_mono 1); |
7630 | 22 |
by (Blast_tac 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
23 |
qed "project_constrains_mono"; |
7630 | 24 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
25 |
Goal "[| D <= C; project C h F : stable A |] ==> project D h F : stable A"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
26 |
by (asm_full_simp_tac |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
27 |
(simpset() addsimps [stable_def, project_constrains_mono]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
28 |
qed "project_stable_mono"; |
7630 | 29 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
30 |
Goal "F : A co B ==> project C h (extend h F) : A co B"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
31 |
by (auto_tac (claset(), |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
32 |
simpset() addsimps [extend_act_def, project_act_def, constrains_def])); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
33 |
qed "project_extend_constrains_I"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
34 |
|
7630 | 35 |
Goal "UNIV <= project_set h C \ |
36 |
\ ==> project C h ((extend h F) Join G) = F Join (project C h G)"; |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
37 |
by (rtac program_equalityI 1); |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
38 |
by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
39 |
subset_UNIV RS subset_trans RS Restrict_triv]) 2); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
40 |
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1); |
7630 | 41 |
qed "project_extend_Join"; |
42 |
||
43 |
Goal "UNIV <= project_set h C \ |
|
44 |
\ ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)"; |
|
45 |
by (dres_inst_tac [("f", "project C h")] arg_cong 1); |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
46 |
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1); |
7630 | 47 |
qed "extend_Join_eq_extend_D"; |
48 |
||
49 |
||
50 |
(** Safety **) |
|
51 |
||
52 |
Goalw [constrains_def] |
|
53 |
"(project C h F : A co B) = \ |
|
54 |
\ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
|
55 |
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un])); |
|
56 |
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1); |
|
57 |
(*the <== direction*) |
|
58 |
by (rewtac project_act_def); |
|
59 |
by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
|
60 |
qed "project_constrains"; |
|
61 |
||
62 |
Goalw [stable_def] |
|
63 |
"(project UNIV h F : stable A) = (F : stable (extend_set h A))"; |
|
64 |
by (simp_tac (simpset() addsimps [project_constrains]) 1); |
|
65 |
qed "project_stable"; |
|
66 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
67 |
Goal "F : stable (extend_set h A) ==> project C h F : stable A"; |
7689 | 68 |
by (dtac (project_stable RS iffD2) 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
69 |
by (blast_tac (claset() addIs [project_stable_mono]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
70 |
qed "project_stable_I"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
71 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
72 |
(*used below to prove Join_project_ensures*) |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
73 |
Goal "[| G : stable C; project C h G : A unless B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
74 |
\ ==> G : (C Int extend_set h A) unless (extend_set h B)"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
75 |
by (asm_full_simp_tac |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
76 |
(simpset() addsimps [unless_def, project_constrains]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
77 |
by (blast_tac (claset() addDs [stable_constrains_Int] |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
78 |
addIs [constrains_weaken]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
79 |
qed_spec_mp "project_unless"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
80 |
|
7630 | 81 |
(*This form's useful with guarantees reasoning*) |
82 |
Goal "(F Join project C h G : A co B) = \ |
|
83 |
\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ |
|
84 |
\ F : A co B)"; |
|
85 |
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1); |
|
86 |
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken] |
|
87 |
addDs [constrains_imp_subset]) 1); |
|
88 |
qed "Join_project_constrains"; |
|
89 |
||
90 |
(*The condition is required to prove the left-to-right direction; |
|
91 |
could weaken it to G : (C Int extend_set h A) co C*) |
|
92 |
Goalw [stable_def] |
|
93 |
"extend h F Join G : stable C \ |
|
94 |
\ ==> (F Join project C h G : stable A) = \ |
|
95 |
\ (extend h F Join G : stable (C Int extend_set h A) & \ |
|
96 |
\ F : stable A)"; |
|
97 |
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
98 |
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
|
99 |
qed "Join_project_stable"; |
|
100 |
||
101 |
Goal "(F Join project UNIV h G : increasing func) = \ |
|
102 |
\ (extend h F Join G : increasing (func o f))"; |
|
103 |
by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1); |
|
104 |
by (auto_tac (claset(), |
|
105 |
simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
|
106 |
extend_stable RS iffD1])); |
|
107 |
qed "Join_project_increasing"; |
|
108 |
||
7689 | 109 |
(*For using project_guarantees in particular cases*) |
110 |
Goal "extend h F Join G : extend_set h A co extend_set h B \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
111 |
\ ==> F Join project C h G : A co B"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
112 |
by (asm_full_simp_tac |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
113 |
(simpset() addsimps [project_constrains, Join_constrains, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
114 |
extend_constrains]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
115 |
by (blast_tac (claset() addIs [constrains_weaken] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
116 |
addDs [constrains_imp_subset]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
117 |
qed "project_constrains_I"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
118 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
119 |
(*The UNIV argument is essential*) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
120 |
Goal "F Join project UNIV h G : A co B \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
121 |
\ ==> extend h F Join G : extend_set h A co extend_set h B"; |
7689 | 122 |
by (asm_full_simp_tac |
123 |
(simpset() addsimps [project_constrains, Join_constrains, |
|
124 |
extend_constrains]) 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
125 |
qed "project_constrains_D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
126 |
|
7841 | 127 |
(** "projecting" and union/intersection **) |
128 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
129 |
Goalw [projecting_def] |
7841 | 130 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \ |
131 |
\ ==> projecting C h F (XA' Int XB') (XA Int XB)"; |
|
132 |
by (Blast_tac 1); |
|
133 |
qed "projecting_Int"; |
|
134 |
||
135 |
Goalw [projecting_def] |
|
136 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \ |
|
137 |
\ ==> projecting C h F (XA' Un XB') (XA Un XB)"; |
|
138 |
by (Blast_tac 1); |
|
139 |
qed "projecting_Un"; |
|
140 |
||
141 |
val [prem] = Goalw [projecting_def] |
|
142 |
"[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
143 |
\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"; |
7841 | 144 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
145 |
qed "projecting_INT"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
146 |
|
7841 | 147 |
val [prem] = Goalw [projecting_def] |
148 |
"[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
149 |
\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"; |
7841 | 150 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
151 |
qed "projecting_UN"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
152 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
153 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
154 |
"[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
155 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
156 |
qed "projecting_weaken"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
157 |
|
7841 | 158 |
Goalw [extending_def] |
159 |
"[| extending C h F X' YA' YA; extending C h F X' YB' YB |] \ |
|
160 |
\ ==> extending C h F X' (YA' Int YB') (YA Int YB)"; |
|
161 |
by (Blast_tac 1); |
|
162 |
qed "extending_Int"; |
|
163 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
164 |
Goalw [extending_def] |
7841 | 165 |
"[| extending C h F X' YA' YA; extending C h F X' YB' YB |] \ |
166 |
\ ==> extending C h F X' (YA' Un YB') (YA Un YB)"; |
|
167 |
by (Blast_tac 1); |
|
168 |
qed "extending_Un"; |
|
169 |
||
170 |
(*This is the right way to handle the X' argument. Having (INT i:I. X' i) |
|
171 |
would strengthen the premise.*) |
|
172 |
val [prem] = Goalw [extending_def] |
|
173 |
"[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \ |
|
174 |
\ ==> extending C h F X' (INT i:I. Y' i) (INT i:I. Y i)"; |
|
175 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
176 |
qed "extending_INT"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
177 |
|
7841 | 178 |
val [prem] = Goalw [extending_def] |
179 |
"[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
180 |
\ ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)"; |
7841 | 181 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
182 |
qed "extending_UN"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
183 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
184 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
185 |
"[| extending C h F X' Y' Y; U'<= X'; Y'<=V'; V<=Y |] \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
186 |
\ ==> extending C h F U' V' V"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
187 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
188 |
qed "extending_weaken"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
189 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
190 |
Goal "projecting C h F X' UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
191 |
by (simp_tac (simpset() addsimps [projecting_def]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
192 |
qed "projecting_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
193 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
194 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
195 |
"projecting C h F (extend_set h A co extend_set h B) (A co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
196 |
by (blast_tac (claset() addIs [project_constrains_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
197 |
qed "projecting_constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
198 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
199 |
Goalw [stable_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
200 |
"projecting C h F (stable (extend_set h A)) (stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
201 |
by (rtac projecting_constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
202 |
qed "projecting_stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
203 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
204 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
205 |
"projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
206 |
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
207 |
qed "projecting_increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
208 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
209 |
Goal "extending C h F X' UNIV Y"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
210 |
by (simp_tac (simpset() addsimps [extending_def]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
211 |
qed "extending_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
212 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
213 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
214 |
"extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
215 |
by (blast_tac (claset() addIs [project_constrains_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
216 |
qed "extending_constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
217 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
218 |
Goalw [stable_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
219 |
"extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
220 |
by (rtac extending_constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
221 |
qed "extending_stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
222 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
223 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
224 |
"extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
225 |
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
226 |
qed "extending_increasing"; |
7689 | 227 |
|
7630 | 228 |
|
229 |
(*** Diff, needed for localTo ***) |
|
230 |
||
231 |
(*Opposite direction fails because Diff in the extended state may remove |
|
232 |
fewer actions, i.e. those that affect other state variables.*) |
|
7841 | 233 |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
234 |
Goalw [project_set_def, project_act_def] |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
235 |
"Restrict (project_set h C) (project_act h (Restrict C act)) = \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
236 |
\ project_act h (Restrict C act)"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
237 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
238 |
qed "Restrict_project_act"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
239 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
240 |
Goalw [project_set_def, project_act_def] |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
241 |
"project_act h (Restrict C Id) = Restrict (project_set h C) Id"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
242 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
243 |
qed "project_act_Restrict_Id"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
244 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
245 |
Goal |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
246 |
"Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
247 |
\ <= project C h (Diff C G acts)"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
248 |
by (simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
249 |
(simpset() addsimps [component_eq_subset, Diff_def, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
250 |
Restrict_project_act, project_act_Restrict_Id, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
251 |
image_image_eq_UN, image_UN, Restrict_image_Diff]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
252 |
by (Force_tac 1); |
7841 | 253 |
qed "Diff_project_project_component_project_Diff"; |
254 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
255 |
Goal "Diff (project_set h C) (project C h G) acts <= \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
256 |
\ project C h (Diff C G (extend_act h `` acts))"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
257 |
by (rtac component_trans 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
258 |
by (rtac Diff_project_project_component_project_Diff 2); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
259 |
by (simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
260 |
(simpset() addsimps [component_eq_subset, Diff_def, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
261 |
Restrict_project_act, project_act_Restrict_Id, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
262 |
image_image_eq_UN, image_UN, Restrict_image_Diff]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
263 |
by (Blast_tac 1); |
7630 | 264 |
qed "Diff_project_component_project_Diff"; |
265 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
266 |
Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
267 |
\ ==> Diff (project_set h C) (project C h G) acts : A co B"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
268 |
by (rtac (Diff_project_component_project_Diff RS component_constrains) 1); |
7630 | 269 |
by (rtac (project_constrains RS iffD2) 1); |
270 |
by (ftac constrains_imp_subset 1); |
|
271 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
272 |
qed "Diff_project_constrains"; |
7630 | 273 |
|
274 |
Goalw [stable_def] |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
275 |
"Diff C G (extend_act h `` acts) : stable (extend_set h A) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
276 |
\ ==> Diff (project_set h C) (project C h G) acts : stable A"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
277 |
by (etac Diff_project_constrains 1); |
7630 | 278 |
qed "Diff_project_stable"; |
279 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
280 |
(** Some results for Diff, extend and project_set **) |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
281 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
282 |
Goal "Diff C (extend h G) (extend_act h `` acts) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
283 |
\ : (extend_set h A) co (extend_set h B) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
284 |
\ ==> Diff (project_set h C) G acts : A co B"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
285 |
br (Diff_project_set_component RS component_constrains) 1; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
286 |
by (forward_tac [constrains_imp_subset] 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
287 |
by (asm_full_simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
288 |
(simpset() addsimps [project_constrains, extend_set_strict_mono]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
289 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
290 |
qed "Diff_project_set_constrains_I"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
291 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
292 |
Goalw [stable_def] |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
293 |
"Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
294 |
\ ==> Diff (project_set h C) G acts : stable A"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
295 |
by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
296 |
qed "Diff_project_set_stable_I"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
297 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
298 |
Goalw [LOCALTO_def] |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
299 |
"extend h F : (v o f) localTo[C] extend h H \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
300 |
\ ==> F : v localTo[project_set h C] H"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
301 |
by Auto_tac; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
302 |
br Diff_project_set_stable_I 1; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
303 |
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
304 |
qed "localTo_project_set_I"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
305 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
306 |
(*Converse fails: even if the conclusion holds, H could modify (v o f) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
307 |
simultaneously with other variables, and this action would not be |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
308 |
superseded by anything in (extend h G) *) |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
309 |
Goal "H : (v o f) localTo[C] extend h G \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
310 |
\ ==> project C h H : v localTo[project_set h C] G"; |
7630 | 311 |
by (asm_full_simp_tac |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
312 |
(simpset() addsimps [LOCALTO_def, |
7630 | 313 |
project_extend_Join RS sym, |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
314 |
Diff_project_stable, |
7630 | 315 |
Collect_eq_extend_set RS sym]) 1); |
7689 | 316 |
qed "project_localTo_lemma"; |
317 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
318 |
Goal "extend h F Join G : (v o f) localTo[C] extend h H \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
319 |
\ ==> F Join project C h G : v localTo[project_set h C] H"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
320 |
by (asm_full_simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
321 |
(simpset() addsimps [Join_localTo, localTo_project_set_I, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
322 |
project_localTo_lemma]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
323 |
qed "gen_project_localTo_I"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
324 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
325 |
Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
326 |
\ ==> F Join project UNIV h G : v localTo[UNIV] H"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
327 |
bd gen_project_localTo_I 1; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
328 |
by (Asm_full_simp_tac 1); |
7630 | 329 |
qed "project_localTo_I"; |
330 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
331 |
Goalw [projecting_def] |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
332 |
"projecting (%G. UNIV) h F \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
333 |
\ ((v o f) localTo[UNIV] extend h H) (v localTo[UNIV] H)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
334 |
by (blast_tac (claset() addIs [project_localTo_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
335 |
qed "projecting_localTo"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
336 |
|
7630 | 337 |
|
338 |
(** Reachability and project **) |
|
339 |
||
340 |
Goal "[| reachable (extend h F Join G) <= C; \ |
|
341 |
\ z : reachable (extend h F Join G) |] \ |
|
342 |
\ ==> f z : reachable (F Join project C h G)"; |
|
343 |
by (etac reachable.induct 1); |
|
344 |
by (force_tac (claset() addIs [reachable.Init, project_set_I], |
|
345 |
simpset()) 1); |
|
346 |
by Auto_tac; |
|
347 |
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)], |
|
348 |
simpset()) 2); |
|
349 |
by (res_inst_tac [("act","x")] reachable.Acts 1); |
|
350 |
by Auto_tac; |
|
351 |
by (etac extend_act_D 1); |
|
352 |
qed "reachable_imp_reachable_project"; |
|
353 |
||
7689 | 354 |
(*The extra generality in the first premise allows guarantees with STRONG |
355 |
preconditions (localTo) and WEAK postconditions.*) |
|
7630 | 356 |
Goalw [Constrains_def] |
357 |
"[| reachable (extend h F Join G) <= C; \ |
|
358 |
\ F Join project C h G : A Co B |] \ |
|
359 |
\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
|
360 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
361 |
by (Clarify_tac 1); |
|
362 |
by (etac constrains_weaken 1); |
|
363 |
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset())); |
|
364 |
qed "project_Constrains_D"; |
|
365 |
||
366 |
Goalw [Stable_def] |
|
367 |
"[| reachable (extend h F Join G) <= C; \ |
|
368 |
\ F Join project C h G : Stable A |] \ |
|
369 |
\ ==> extend h F Join G : Stable (extend_set h A)"; |
|
370 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
|
371 |
qed "project_Stable_D"; |
|
372 |
||
373 |
Goalw [Always_def] |
|
374 |
"[| reachable (extend h F Join G) <= C; \ |
|
375 |
\ F Join project C h G : Always A |] \ |
|
376 |
\ ==> extend h F Join G : Always (extend_set h A)"; |
|
377 |
by (force_tac (claset() addIs [reachable.Init, project_set_I], |
|
7689 | 378 |
simpset() addsimps [project_Stable_D]) 1); |
7630 | 379 |
qed "project_Always_D"; |
380 |
||
381 |
Goalw [Increasing_def] |
|
382 |
"[| reachable (extend h F Join G) <= C; \ |
|
383 |
\ F Join project C h G : Increasing func |] \ |
|
384 |
\ ==> extend h F Join G : Increasing (func o f)"; |
|
385 |
by Auto_tac; |
|
386 |
by (stac Collect_eq_extend_set 1); |
|
387 |
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
|
388 |
qed "project_Increasing_D"; |
|
389 |
||
390 |
||
391 |
(** Converse results for weak safety: benefits of the argument C *) |
|
392 |
||
393 |
Goal "[| C <= reachable(extend h F Join G); \ |
|
394 |
\ x : reachable (F Join project C h G) |] \ |
|
395 |
\ ==> EX y. h(x,y) : reachable (extend h F Join G)"; |
|
396 |
by (etac reachable.induct 1); |
|
397 |
by (ALLGOALS Asm_full_simp_tac); |
|
398 |
(*SLOW: 6.7s*) |
|
399 |
by (force_tac (claset() delrules [Id_in_Acts] |
|
400 |
addIs [reachable.Acts, extend_act_D], |
|
401 |
simpset() addsimps [project_act_def]) 2); |
|
402 |
by (force_tac (claset() addIs [reachable.Init], |
|
403 |
simpset() addsimps [project_set_def]) 1); |
|
404 |
qed "reachable_project_imp_reachable"; |
|
405 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
406 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
407 |
Goal "project_set h (reachable (extend h F Join G)) = \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
408 |
\ reachable (F Join project (reachable (extend h F Join G)) h G)"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
409 |
by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
410 |
subset_refl RS reachable_project_imp_reachable], |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
411 |
simpset() addsimps [project_set_def])); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
412 |
qed "project_set_reachable_extend_eq"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
413 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
414 |
(*Perhaps should replace C by reachable...*) |
7630 | 415 |
Goalw [Constrains_def] |
416 |
"[| C <= reachable (extend h F Join G); \ |
|
417 |
\ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \ |
|
418 |
\ ==> F Join project C h G : A Co B"; |
|
419 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains, |
|
420 |
extend_set_Int_distrib]) 1); |
|
421 |
by (rtac conjI 1); |
|
422 |
by (etac constrains_weaken 1); |
|
423 |
by Auto_tac; |
|
424 |
by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1); |
|
425 |
(*Some generalization of constrains_weaken_L would be better, but what is it?*) |
|
426 |
by (rewtac constrains_def); |
|
427 |
by Auto_tac; |
|
428 |
by (thin_tac "ALL act : Acts G. ?P act" 1); |
|
429 |
by (force_tac (claset() addSDs [reachable_project_imp_reachable], |
|
430 |
simpset()) 1); |
|
431 |
qed "project_Constrains_I"; |
|
432 |
||
433 |
Goalw [Stable_def] |
|
434 |
"[| C <= reachable (extend h F Join G); \ |
|
435 |
\ extend h F Join G : Stable (extend_set h A) |] \ |
|
436 |
\ ==> F Join project C h G : Stable A"; |
|
437 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
|
438 |
qed "project_Stable_I"; |
|
439 |
||
7689 | 440 |
Goalw [Always_def] |
441 |
"[| C <= reachable (extend h F Join G); \ |
|
442 |
\ extend h F Join G : Always (extend_set h A) |] \ |
|
443 |
\ ==> F Join project C h G : Always A"; |
|
444 |
by (auto_tac (claset(), simpset() addsimps [project_Stable_I])); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
445 |
by (rewrite_goals_tac [project_set_def, extend_set_def]); |
7689 | 446 |
by (Blast_tac 1); |
447 |
qed "project_Always_I"; |
|
448 |
||
7630 | 449 |
Goalw [Increasing_def] |
450 |
"[| C <= reachable (extend h F Join G); \ |
|
451 |
\ extend h F Join G : Increasing (func o f) |] \ |
|
452 |
\ ==> F Join project C h G : Increasing func"; |
|
453 |
by Auto_tac; |
|
454 |
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym, |
|
455 |
project_Stable_I]) 1); |
|
456 |
qed "project_Increasing_I"; |
|
457 |
||
458 |
Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B) = \ |
|
459 |
\ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; |
|
460 |
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
|
461 |
qed "project_Constrains"; |
|
462 |
||
463 |
Goalw [Stable_def] |
|
464 |
"(F Join project (reachable (extend h F Join G)) h G : Stable A) = \ |
|
465 |
\ (extend h F Join G : Stable (extend_set h A))"; |
|
466 |
by (rtac project_Constrains 1); |
|
467 |
qed "project_Stable"; |
|
468 |
||
469 |
Goal |
|
470 |
"(F Join project (reachable (extend h F Join G)) h G : Increasing func) = \ |
|
471 |
\ (extend h F Join G : Increasing (func o f))"; |
|
472 |
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
|
473 |
Collect_eq_extend_set RS sym]) 1); |
|
474 |
qed "project_Increasing"; |
|
475 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
476 |
Goal "extend h F Join G : (v o f) LocalTo extend h H \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
477 |
\ ==> F Join project (reachable (extend h F Join G)) h G : v LocalTo H"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
478 |
by (asm_full_simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
479 |
(simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
480 |
gen_project_localTo_I]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
481 |
qed "project_LocalTo_I"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
482 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
483 |
(** A lot of redundant theorems: all are proved to facilitate reasoning |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
484 |
about guarantees. **) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
485 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
486 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
487 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
488 |
\ (extend_set h A Co extend_set h B) (A Co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
489 |
by (blast_tac (claset() addIs [project_Constrains_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
490 |
qed "projecting_Constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
491 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
492 |
Goalw [Stable_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
493 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
494 |
\ (Stable (extend_set h A)) (Stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
495 |
by (rtac projecting_Constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
496 |
qed "projecting_Stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
497 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
498 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
499 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
500 |
\ (Always (extend_set h A)) (Always A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
501 |
by (blast_tac (claset() addIs [project_Always_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
502 |
qed "projecting_Always"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
503 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
504 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
505 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
506 |
\ (Increasing (func o f)) (Increasing func)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
507 |
by (blast_tac (claset() addIs [project_Increasing_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
508 |
qed "projecting_Increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
509 |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
510 |
Goalw [projecting_def] |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
511 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
512 |
\ ((v o f) LocalTo extend h H) (v LocalTo H)"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
513 |
by (blast_tac (claset() addIs [project_LocalTo_I]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
514 |
qed "projecting_LocalTo"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
515 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
516 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
517 |
"extending (%G. reachable (extend h F Join G)) h F X' \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
518 |
\ (extend_set h A Co extend_set h B) (A Co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
519 |
by (blast_tac (claset() addIs [project_Constrains_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
520 |
qed "extending_Constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
521 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
522 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
523 |
"extending (%G. reachable (extend h F Join G)) h F X' \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
524 |
\ (Stable (extend_set h A)) (Stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
525 |
by (blast_tac (claset() addIs [project_Stable_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
526 |
qed "extending_Stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
527 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
528 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
529 |
"extending (%G. reachable (extend h F Join G)) h F X' \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
530 |
\ (Always (extend_set h A)) (Always A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
531 |
by (blast_tac (claset() addIs [project_Always_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
532 |
qed "extending_Always"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
533 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
534 |
val [prem] = |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
535 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
536 |
"(!!G. reachable (extend h F Join G) <= C G) \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
537 |
\ ==> extending C h F X' \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
538 |
\ (Increasing (func o f)) (Increasing func)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
539 |
by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
540 |
qed "extending_Increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
541 |
|
7630 | 542 |
|
543 |
(** Progress includes safety in the definition of ensures **) |
|
544 |
||
545 |
(*** Progress for (project C h F) ***) |
|
546 |
||
547 |
(** transient **) |
|
548 |
||
549 |
(*Premise is that C includes the domains of all actions that could be the |
|
550 |
transient one. Could have C=UNIV of course*) |
|
551 |
Goalw [transient_def] |
|
552 |
"[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \ |
|
553 |
\ Domain act <= C; \ |
|
554 |
\ F : transient (extend_set h A) |] \ |
|
555 |
\ ==> project C h F : transient A"; |
|
556 |
by (auto_tac (claset() delrules [ballE], |
|
557 |
simpset() addsimps [Domain_project_act, Int_absorb2])); |
|
558 |
by (REPEAT (ball_tac 1)); |
|
559 |
by (auto_tac (claset(), |
|
560 |
simpset() addsimps [extend_set_def, project_set_def, |
|
561 |
project_act_def])); |
|
562 |
by (ALLGOALS Blast_tac); |
|
563 |
qed "transient_extend_set_imp_project_transient"; |
|
564 |
||
565 |
||
566 |
(*UNUSED. WHY?? |
|
567 |
Converse of the above...it requires a strong assumption about actions |
|
568 |
being enabled for all possible values of the new variables.*) |
|
569 |
Goalw [transient_def] |
|
570 |
"[| project C h F : transient A; \ |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
571 |
\ ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \ |
7630 | 572 |
\ Domain act <= C \ |
573 |
\ & extend_set h (project_set h (Domain act)) <= Domain act |] \ |
|
574 |
\ ==> F : transient (extend_set h A)"; |
|
575 |
by (auto_tac (claset() delrules [ballE], |
|
576 |
simpset() addsimps [Domain_project_act])); |
|
577 |
by (ball_tac 1); |
|
578 |
by (rtac bexI 1); |
|
579 |
by (assume_tac 2); |
|
580 |
by Auto_tac; |
|
581 |
by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1); |
|
582 |
by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1); |
|
583 |
(*The Domain requirement's proved; must prove the Image requirement*) |
|
584 |
by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1); |
|
585 |
by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1); |
|
586 |
by Auto_tac; |
|
587 |
by (thin_tac "A <= ?B" 1); |
|
588 |
by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1); |
|
589 |
qed "project_transient_imp_transient_extend_set"; |
|
590 |
||
591 |
||
592 |
(** ensures **) |
|
593 |
||
594 |
(*For simplicity, the complicated condition on C is eliminated |
|
595 |
NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*) |
|
596 |
Goal "F : (extend_set h A) ensures (extend_set h B) \ |
|
597 |
\ ==> project UNIV h F : A ensures B"; |
|
598 |
by (asm_full_simp_tac |
|
599 |
(simpset() addsimps [ensures_def, project_constrains, |
|
600 |
transient_extend_set_imp_project_transient, |
|
601 |
extend_set_Un_distrib RS sym, |
|
602 |
extend_set_Diff_distrib RS sym]) 1); |
|
603 |
by (Blast_tac 1); |
|
604 |
qed "ensures_extend_set_imp_project_ensures"; |
|
605 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
606 |
(*A strong condition: F can do anything that project G can.*) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
607 |
Goal "[| ALL D. project C h G : transient D --> F : transient D; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
608 |
\ extend h F Join G : stable C; \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
609 |
\ F Join project C h G : A ensures B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
610 |
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"; |
7630 | 611 |
by (case_tac "A <= B" 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
612 |
by (blast_tac (claset() addIs [subset_imp_ensures] addDs [extend_set_mono]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
613 |
by (full_simp_tac (simpset() addsimps [ensures_def, Join_constrains, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
614 |
Join_stable, Join_transient]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
615 |
by (REPEAT_FIRST (rtac conjI)); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
616 |
by (blast_tac (claset() addDs [extend_transient RS iffD2] |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
617 |
addIs [transient_strengthen]) 3); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
618 |
by (REPEAT (force_tac (claset() addIs [project_unless RS unlessD, unlessI, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
619 |
project_extend_constrains_I], |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
620 |
simpset()) 1)); |
7630 | 621 |
qed_spec_mp "Join_project_ensures"; |
622 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
623 |
Goal "[| ALL D. project C h G : transient D --> F : transient D; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
624 |
\ extend h F Join G : stable C; \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
625 |
\ F Join project C h G : A leadsTo B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
626 |
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
627 |
by (etac leadsTo_induct 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
628 |
by (asm_simp_tac (simpset() delsimps UN_simps |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
629 |
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
630 |
by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
631 |
leadsTo_Trans]) 2); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
632 |
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1); |
7689 | 633 |
qed "project_leadsTo_lemma"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
634 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
635 |
(*Instance of the previous theorem for STRONG progress*) |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
636 |
Goal "[| ALL D. project UNIV h G : transient D --> F : transient D; \ |
7630 | 637 |
\ F Join project UNIV h G : A leadsTo B |] \ |
638 |
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
|
7689 | 639 |
by (dtac project_leadsTo_lemma 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
640 |
by Auto_tac; |
7689 | 641 |
qed "project_UNIV_leadsTo_lemma"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
642 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
643 |
(** Towards the analogous theorem for WEAK progress*) |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
644 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
645 |
Goal "[| ALL D. project C h G : transient D --> F : transient D; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
646 |
\ extend h F Join G : stable C; \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
647 |
\ F Join project C h G : (project_set h C Int A) leadsTo B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
648 |
\ ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"; |
7630 | 649 |
by (etac leadsTo_induct 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
650 |
by (asm_simp_tac (simpset() delsimps UN_simps |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
651 |
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
652 |
by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
653 |
leadsTo_Trans]) 2); |
7630 | 654 |
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
655 |
val lemma = result(); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
656 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
657 |
Goal "[| ALL D. project C h G : transient D --> F : transient D; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
658 |
\ extend h F Join G : stable C; \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
659 |
\ F Join project C h G : (project_set h C Int A) leadsTo B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
660 |
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; |
7689 | 661 |
by (rtac (lemma RS leadsTo_weaken) 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
662 |
by (auto_tac (claset() addIs [project_set_I], simpset())); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
663 |
val lemma2 = result(); |
7630 | 664 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
665 |
Goal "[| C = (reachable (extend h F Join G)); \ |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
666 |
\ ALL D. project C h G : transient D --> F : transient D; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
667 |
\ F Join project C h G : A LeadsTo B |] \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
668 |
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
669 |
by (asm_full_simp_tac |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
670 |
(simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
671 |
project_set_reachable_extend_eq]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
672 |
qed "Join_project_LeadsTo"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
673 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
674 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
675 |
(*** GUARANTEES and EXTEND ***) |
7630 | 676 |
|
677 |
(** Strong precondition and postcondition; doesn't seem very useful. **) |
|
678 |
||
679 |
Goal "F : X guarantees Y ==> \ |
|
680 |
\ extend h F : (extend h `` X) guarantees (extend h `` Y)"; |
|
681 |
by (rtac guaranteesI 1); |
|
682 |
by Auto_tac; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
683 |
by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
684 |
extend_Join_eq_extend_D, |
7630 | 685 |
guaranteesD]) 1); |
686 |
qed "guarantees_imp_extend_guarantees"; |
|
687 |
||
688 |
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \ |
|
689 |
\ ==> F : X guarantees Y"; |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
690 |
by (auto_tac (claset(), simpset() addsimps [guarantees_eq])); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
691 |
by (dres_inst_tac [("x", "extend h G")] spec 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
692 |
by (asm_full_simp_tac |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
693 |
(simpset() delsimps [extend_Join] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
694 |
addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1); |
7630 | 695 |
qed "extend_guarantees_imp_guarantees"; |
696 |
||
697 |
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \ |
|
698 |
\ (F : X guarantees Y)"; |
|
699 |
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
|
700 |
extend_guarantees_imp_guarantees]) 1); |
|
701 |
qed "extend_guarantees_eq"; |
|
702 |
||
703 |
||
704 |
(*Weak precondition and postcondition; this is the good one! |
|
705 |
Not clear that it has a converse [or that we want one!]*) |
|
7841 | 706 |
|
707 |
(*The raw version*) |
|
708 |
val [xguary,project,extend] = |
|
709 |
Goal "[| F : X guarantees Y; \ |
|
710 |
\ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \ |
|
711 |
\ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \ |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
712 |
\ Disjoint UNIV (extend h F) G |] \ |
7841 | 713 |
\ ==> extend h F Join G : Y' |] \ |
714 |
\ ==> extend h F : X' guarantees Y'"; |
|
715 |
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1); |
|
716 |
by (etac project 1); |
|
717 |
by (assume_tac 1); |
|
718 |
by (assume_tac 1); |
|
719 |
qed "project_guarantees_lemma"; |
|
720 |
||
7630 | 721 |
Goal "[| F : X guarantees Y; \ |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
722 |
\ projecting C h F X' X; extending C h F X' Y' Y |] \ |
7630 | 723 |
\ ==> extend h F : X' guarantees Y'"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
724 |
by (rtac guaranteesI 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
725 |
by (auto_tac (claset(), |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
726 |
simpset() addsimps [guaranteesD, projecting_def, extending_def])); |
7630 | 727 |
qed "project_guarantees"; |
728 |
||
7841 | 729 |
(*It seems that neither "guarantees" law can be proved from the other.*) |
7630 | 730 |
|
731 |
||
732 |
(*** guarantees corollaries ***) |
|
733 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
734 |
(** Most could be deleted: the required versions are easy to prove **) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
735 |
|
7630 | 736 |
Goal "F : UNIV guarantees increasing func \ |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
737 |
\ ==> extend h F : X' guarantees increasing (func o f)"; |
7630 | 738 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
739 |
by (rtac extending_increasing 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
740 |
by (rtac projecting_UNIV 1); |
7630 | 741 |
qed "extend_guar_increasing"; |
742 |
||
743 |
Goal "F : UNIV guarantees Increasing func \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
744 |
\ ==> extend h F : X' guarantees Increasing (func o f)"; |
7630 | 745 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
746 |
by (rtac extending_Increasing 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
747 |
by (rtac projecting_UNIV 1); |
7630 | 748 |
by Auto_tac; |
749 |
qed "extend_guar_Increasing"; |
|
750 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
751 |
Goal "F : (v localTo[UNIV] G) guarantees increasing func \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
752 |
\ ==> extend h F : (v o f) localTo[UNIV] (extend h G) \ |
7630 | 753 |
\ guarantees increasing (func o f)"; |
754 |
by (etac project_guarantees 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
755 |
by (rtac extending_increasing 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
756 |
by (rtac projecting_localTo 1); |
7630 | 757 |
qed "extend_localTo_guar_increasing"; |
758 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
759 |
Goal "F : (v LocalTo G) guarantees Increasing func \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
760 |
\ ==> extend h F : (v o f) LocalTo (extend h G) \ |
7630 | 761 |
\ guarantees Increasing (func o f)"; |
762 |
by (etac project_guarantees 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
763 |
by (rtac extending_Increasing 2); |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
764 |
by (rtac projecting_LocalTo 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
765 |
by Auto_tac; |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
766 |
qed "extend_LocalTo_guar_Increasing"; |
7630 | 767 |
|
7689 | 768 |
Goal "F : Always A guarantees Always B \ |
769 |
\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)"; |
|
770 |
by (etac project_guarantees 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
771 |
by (rtac extending_Always 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
772 |
by (rtac projecting_Always 1); |
7689 | 773 |
qed "extend_guar_Always"; |
774 |
||
7630 | 775 |
|
776 |
(** Guarantees with a leadsTo postcondition **) |
|
777 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
778 |
(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
779 |
Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
780 |
\ ==> F : transient D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
781 |
by (case_tac "D={}" 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
782 |
by (auto_tac (claset() addIs [transient_strengthen], simpset())); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
783 |
qed "transient_lemma"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
784 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
785 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
786 |
(*Previously tried to prove |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
787 |
[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
788 |
but it can fail if C removes some parts of an action of G.*) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
789 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
790 |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
791 |
Goal "[| G : v localTo[UNIV] F; Disjoint UNIV F G |] ==> G : stable {s. v s = z}"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
792 |
by (asm_full_simp_tac |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
793 |
(simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def, |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
794 |
stable_def, constrains_def]) 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
795 |
by (Blast_tac 1); |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
796 |
qed "localTo_imp_stable"; |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
797 |
|
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
798 |
Goal "[| G : f localTo[UNIV] extend h F; \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
799 |
\ Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}"; |
7630 | 800 |
by (asm_full_simp_tac |
801 |
(simpset() addsimps [localTo_imp_stable, |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
802 |
extend_set_sing, project_stable_I]) 1); |
7630 | 803 |
qed "localTo_imp_project_stable"; |
804 |
||
805 |
Goal "F : stable{s} ==> F ~: transient {s}"; |
|
806 |
by (auto_tac (claset(), |
|
807 |
simpset() addsimps [FP_def, transient_def, |
|
808 |
stable_def, constrains_def])); |
|
809 |
qed "stable_sing_imp_not_transient"; |
|
810 |
||
7689 | 811 |
Goal "[| F Join project UNIV h G : A leadsTo B; \ |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
812 |
\ G : f localTo[UNIV] extend h F; \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
813 |
\ Disjoint UNIV (extend h F) G |] \ |
7689 | 814 |
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
815 |
by (rtac project_UNIV_leadsTo_lemma 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
816 |
by (Clarify_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
817 |
by (rtac transient_lemma 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
818 |
by (auto_tac (claset(), |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
819 |
simpset() addsimps [localTo_imp_project_stable, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
820 |
stable_sing_imp_not_transient])); |
7689 | 821 |
qed "project_leadsTo_D"; |
822 |
||
823 |
Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \ |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
824 |
\ G : f localTo[UNIV] extend h F; \ |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
825 |
\ Disjoint UNIV (extend h F) G |] \ |
7689 | 826 |
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
827 |
by (rtac (refl RS Join_project_LeadsTo) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
828 |
by (Clarify_tac 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
829 |
by (rtac transient_lemma 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
830 |
by (auto_tac (claset(), |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
831 |
simpset() addsimps [localTo_imp_project_stable, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
832 |
stable_sing_imp_not_transient])); |
7689 | 833 |
qed "project_LeadsTo_D"; |
834 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
835 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
836 |
"extending (%G. UNIV) h F \ |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
837 |
\ (f localTo[UNIV] extend h F) \ |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
838 |
\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
839 |
by (blast_tac (claset() addSDs [Join_localTo RS iffD1] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
840 |
addIs [project_leadsTo_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
841 |
qed "extending_leadsTo"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
842 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
843 |
Goalw [extending_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
844 |
"extending (%G. reachable (extend h F Join G)) h F \ |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
845 |
\ (f localTo[UNIV] extend h F) \ |
7841 | 846 |
\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
847 |
by (blast_tac (claset() addSDs [Join_localTo RS iffD1] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
848 |
addIs [project_LeadsTo_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
849 |
qed "extending_LeadsTo"; |
7689 | 850 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
851 |
(*STRONG precondition and postcondition*) |
7630 | 852 |
Goal "F : (A co A') guarantees (B leadsTo B') \ |
853 |
\ ==> extend h F : ((extend_set h A) co (extend_set h A')) \ |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
854 |
\ Int (f localTo[UNIV] (extend h F)) \ |
7630 | 855 |
\ guarantees ((extend_set h B) leadsTo (extend_set h B'))"; |
856 |
by (etac project_guarantees 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
857 |
by (rtac (extending_leadsTo RS extending_weaken) 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
858 |
by (rtac (projecting_constrains RS projecting_weaken) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
859 |
by Auto_tac; |
7630 | 860 |
qed "extend_co_guar_leadsTo"; |
861 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
862 |
(*WEAK precondition and postcondition*) |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
863 |
Goal "F : (A Co A') guarantees (B LeadsTo B') \ |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
864 |
\ ==> extend h F : ((extend_set h A) Co (extend_set h A')) \ |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
865 |
\ Int (f localTo[UNIV] (extend h F)) \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
866 |
\ guarantees ((extend_set h B) LeadsTo (extend_set h B'))"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
867 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
868 |
by (rtac (extending_LeadsTo RS extending_weaken) 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
869 |
by (rtac (projecting_Constrains RS projecting_weaken) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
870 |
by Auto_tac; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
871 |
qed "extend_Co_guar_LeadsTo"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
872 |
|
7630 | 873 |
Close_locale "Extend"; |