author | paulson |
Fri, 14 Jul 2000 14:51:02 +0200 | |
changeset 9337 | 58bd51302b21 |
parent 9190 | b86ff604729f |
child 9403 | aad13b59b8d9 |
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 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
13 |
Goal "F : A co B ==> project h C (extend h F) : A co B"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
14 |
by (auto_tac (claset(), |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
15 |
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
|
16 |
qed "project_extend_constrains_I"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
17 |
|
7630 | 18 |
|
19 |
(** Safety **) |
|
20 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
21 |
(*used below to prove Join_project_ensures*) |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
22 |
Goal "[| G : stable C; project h C G : A unless B |] \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
23 |
\ ==> 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
|
24 |
by (asm_full_simp_tac |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
25 |
(simpset() addsimps [unless_def, project_constrains]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
26 |
by (blast_tac (claset() addDs [stable_constrains_Int] |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
27 |
addIs [constrains_weaken]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
28 |
qed_spec_mp "project_unless"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
29 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
30 |
(*Generalizes project_constrains to the program F Join project h C G; |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
31 |
useful with guarantees reasoning*) |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
32 |
Goal "(F Join project h C G : A co B) = \ |
7630 | 33 |
\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ |
34 |
\ F : A co B)"; |
|
35 |
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1); |
|
36 |
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken] |
|
37 |
addDs [constrains_imp_subset]) 1); |
|
38 |
qed "Join_project_constrains"; |
|
39 |
||
40 |
(*The condition is required to prove the left-to-right direction; |
|
41 |
could weaken it to G : (C Int extend_set h A) co C*) |
|
42 |
Goalw [stable_def] |
|
43 |
"extend h F Join G : stable C \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
44 |
\ ==> (F Join project h C G : stable A) = \ |
7630 | 45 |
\ (extend h F Join G : stable (C Int extend_set h A) & \ |
46 |
\ F : stable A)"; |
|
47 |
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
48 |
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
|
49 |
qed "Join_project_stable"; |
|
50 |
||
7689 | 51 |
(*For using project_guarantees in particular cases*) |
52 |
Goal "extend h F Join G : extend_set h A co extend_set h B \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
53 |
\ ==> F Join project h C G : A co B"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
54 |
by (asm_full_simp_tac |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
55 |
(simpset() addsimps [project_constrains, Join_constrains, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
56 |
extend_constrains]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
57 |
by (blast_tac (claset() addIs [constrains_weaken] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
58 |
addDs [constrains_imp_subset]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
59 |
qed "project_constrains_I"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
60 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
61 |
Goalw [increasing_def, stable_def] |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
62 |
"extend h F Join G : increasing (func o f) \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
63 |
\ ==> F Join project h C G : increasing func"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
64 |
by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
65 |
extend_set_eq_Collect]) 1); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
66 |
qed "project_increasing_I"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
67 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
68 |
Goal "(F Join project h UNIV G : increasing func) = \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
69 |
\ (extend h F Join G : increasing (func o f))"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
70 |
by (rtac iffI 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
71 |
by (etac project_increasing_I 2); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
72 |
by (asm_full_simp_tac |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
73 |
(simpset() addsimps [increasing_def, Join_project_stable]) 1); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
74 |
by (auto_tac (claset(), |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
75 |
simpset() addsimps [Join_stable, extend_set_eq_Collect, |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
76 |
extend_stable RS iffD1])); |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
77 |
qed "Join_project_increasing"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
78 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
79 |
(*The UNIV argument is essential*) |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
80 |
Goal "F Join project h UNIV G : A co B \ |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
81 |
\ ==> extend h F Join G : extend_set h A co extend_set h B"; |
7689 | 82 |
by (asm_full_simp_tac |
83 |
(simpset() addsimps [project_constrains, Join_constrains, |
|
84 |
extend_constrains]) 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
85 |
qed "project_constrains_D"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
86 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
87 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
88 |
(*** "projecting" and union/intersection (no converses) ***) |
7841 | 89 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
90 |
Goalw [projecting_def] |
7841 | 91 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \ |
92 |
\ ==> projecting C h F (XA' Int XB') (XA Int XB)"; |
|
93 |
by (Blast_tac 1); |
|
94 |
qed "projecting_Int"; |
|
95 |
||
96 |
Goalw [projecting_def] |
|
97 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \ |
|
98 |
\ ==> projecting C h F (XA' Un XB') (XA Un XB)"; |
|
99 |
by (Blast_tac 1); |
|
100 |
qed "projecting_Un"; |
|
101 |
||
102 |
val [prem] = Goalw [projecting_def] |
|
103 |
"[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
104 |
\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"; |
7841 | 105 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
106 |
qed "projecting_INT"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
107 |
|
7841 | 108 |
val [prem] = Goalw [projecting_def] |
109 |
"[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \ |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
110 |
\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"; |
7841 | 111 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
112 |
qed "projecting_UN"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
113 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
114 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
115 |
"[| 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
|
116 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
117 |
qed "projecting_weaken"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
118 |
|
8073 | 119 |
Goalw [projecting_def] |
120 |
"[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X"; |
|
121 |
by Auto_tac; |
|
122 |
qed "projecting_weaken_L"; |
|
123 |
||
7841 | 124 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
125 |
"[| extending v C h F YA' YA; extending v C h F YB' YB |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
126 |
\ ==> extending v C h F (YA' Int YB') (YA Int YB)"; |
7841 | 127 |
by (Blast_tac 1); |
128 |
qed "extending_Int"; |
|
129 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
130 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
131 |
"[| extending v C h F YA' YA; extending v C h F YB' YB |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
132 |
\ ==> extending v C h F (YA' Un YB') (YA Un YB)"; |
7841 | 133 |
by (Blast_tac 1); |
134 |
qed "extending_Un"; |
|
135 |
||
136 |
val [prem] = Goalw [extending_def] |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
137 |
"[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
138 |
\ ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)"; |
7841 | 139 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
140 |
qed "extending_INT"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
141 |
|
7841 | 142 |
val [prem] = Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
143 |
"[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
144 |
\ ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)"; |
7841 | 145 |
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
146 |
qed "extending_UN"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
147 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
148 |
Goalw [extending_def] |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
149 |
"[| extending v C h F Y' Y; Y'<=V'; V<=Y; \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
150 |
\ preserves w <= preserves v |] \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
151 |
\ ==> extending w C h F V' V"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
152 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
153 |
qed "extending_weaken"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
154 |
|
8073 | 155 |
Goalw [extending_def] |
156 |
"[| extending v C h F Y' Y; Y'<=V' |] ==> extending v C h F V' Y"; |
|
157 |
by Auto_tac; |
|
158 |
qed "extending_weaken_L"; |
|
159 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
160 |
Goal "projecting C h F X' UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
161 |
by (simp_tac (simpset() addsimps [projecting_def]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
162 |
qed "projecting_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
163 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
164 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
165 |
"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
|
166 |
by (blast_tac (claset() addIs [project_constrains_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
167 |
qed "projecting_constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
168 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
169 |
Goalw [stable_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
170 |
"projecting C h F (stable (extend_set h A)) (stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
171 |
by (rtac projecting_constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
172 |
qed "projecting_stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
173 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
174 |
Goalw [projecting_def] |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
175 |
"projecting C h F (increasing (func o f)) (increasing func)"; |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
176 |
by (blast_tac (claset() addIs [project_increasing_I]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
177 |
qed "projecting_increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
178 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
179 |
Goal "extending v C h F UNIV Y"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
180 |
by (simp_tac (simpset() addsimps [extending_def]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
181 |
qed "extending_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
182 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
183 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
184 |
"extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
185 |
by (blast_tac (claset() addIs [project_constrains_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
186 |
qed "extending_constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
187 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
188 |
Goalw [stable_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
189 |
"extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
190 |
by (rtac extending_constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
191 |
qed "extending_stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
192 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
193 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
194 |
"extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
195 |
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
196 |
qed "extending_increasing"; |
7689 | 197 |
|
7630 | 198 |
|
199 |
(** Reachability and project **) |
|
200 |
||
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
201 |
(*In practice, C = reachable(...): the inclusion is equality*) |
7630 | 202 |
Goal "[| reachable (extend h F Join G) <= C; \ |
203 |
\ z : reachable (extend h F Join G) |] \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
204 |
\ ==> f z : reachable (F Join project h C G)"; |
7630 | 205 |
by (etac reachable.induct 1); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
206 |
by (force_tac (claset() addSIs [reachable.Init], |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
207 |
simpset() addsimps [split_extended_all]) 1); |
7630 | 208 |
by Auto_tac; |
209 |
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)], |
|
210 |
simpset()) 2); |
|
211 |
by (res_inst_tac [("act","x")] reachable.Acts 1); |
|
212 |
by Auto_tac; |
|
213 |
by (etac extend_act_D 1); |
|
214 |
qed "reachable_imp_reachable_project"; |
|
215 |
||
216 |
Goalw [Constrains_def] |
|
8128 | 217 |
"F Join project h (reachable (extend h F Join G)) G : A Co B \ |
7630 | 218 |
\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
219 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
220 |
by (Clarify_tac 1); |
|
221 |
by (etac constrains_weaken 1); |
|
8128 | 222 |
by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset())); |
7630 | 223 |
qed "project_Constrains_D"; |
224 |
||
225 |
Goalw [Stable_def] |
|
8128 | 226 |
"F Join project h (reachable (extend h F Join G)) G : Stable A \ |
7630 | 227 |
\ ==> extend h F Join G : Stable (extend_set h A)"; |
228 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
|
229 |
qed "project_Stable_D"; |
|
230 |
||
231 |
Goalw [Always_def] |
|
8128 | 232 |
"F Join project h (reachable (extend h F Join G)) G : Always A \ |
7630 | 233 |
\ ==> extend h F Join G : Always (extend_set h A)"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
234 |
by (force_tac (claset() addIs [reachable.Init], |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
235 |
simpset() addsimps [project_Stable_D, split_extended_all]) 1); |
7630 | 236 |
qed "project_Always_D"; |
237 |
||
238 |
Goalw [Increasing_def] |
|
8128 | 239 |
"F Join project h (reachable (extend h F Join G)) G : Increasing func \ |
7630 | 240 |
\ ==> extend h F Join G : Increasing (func o f)"; |
241 |
by Auto_tac; |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
242 |
by (stac (extend_set_eq_Collect RS sym) 1); |
7630 | 243 |
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
244 |
qed "project_Increasing_D"; |
|
245 |
||
246 |
||
247 |
(** Converse results for weak safety: benefits of the argument C *) |
|
248 |
||
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
249 |
(*In practice, C = reachable(...): the inclusion is equality*) |
7630 | 250 |
Goal "[| C <= reachable(extend h F Join G); \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
251 |
\ x : reachable (F Join project h C G) |] \ |
7630 | 252 |
\ ==> EX y. h(x,y) : reachable (extend h F Join G)"; |
253 |
by (etac reachable.induct 1); |
|
254 |
by (ALLGOALS Asm_full_simp_tac); |
|
255 |
by (force_tac (claset() delrules [Id_in_Acts] |
|
256 |
addIs [reachable.Acts, extend_act_D], |
|
257 |
simpset() addsimps [project_act_def]) 2); |
|
258 |
by (force_tac (claset() addIs [reachable.Init], |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
259 |
simpset()) 1); |
7630 | 260 |
qed "reachable_project_imp_reachable"; |
261 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
262 |
Goal "project_set h (reachable (extend h F Join G)) = \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
263 |
\ reachable (F Join project h (reachable (extend h F Join G)) G)"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
264 |
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
|
265 |
subset_refl RS reachable_project_imp_reachable], |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
266 |
simpset())); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
267 |
qed "project_set_reachable_extend_eq"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
268 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
269 |
(*UNUSED*) |
7947 | 270 |
Goal "reachable (extend h F Join G) <= C \ |
271 |
\ ==> reachable (extend h F Join G) <= \ |
|
272 |
\ extend_set h (reachable (F Join project h C G))"; |
|
273 |
by (auto_tac (claset() addDs [reachable_imp_reachable_project], |
|
274 |
simpset())); |
|
275 |
qed "reachable_extend_Join_subset"; |
|
276 |
||
7630 | 277 |
Goalw [Constrains_def] |
8128 | 278 |
"extend h F Join G : (extend_set h A) Co (extend_set h B) \ |
279 |
\ ==> F Join project h (reachable (extend h F Join G)) G : A Co B"; |
|
7630 | 280 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains, |
281 |
extend_set_Int_distrib]) 1); |
|
282 |
by (rtac conjI 1); |
|
8128 | 283 |
by (force_tac |
284 |
(claset() addEs [constrains_weaken_L] |
|
285 |
addSDs [extend_constrains_project_set, |
|
286 |
subset_refl RS reachable_project_imp_reachable], |
|
287 |
simpset() addsimps [Join_constrains]) 2); |
|
288 |
by (blast_tac (claset() addIs [constrains_weaken_L]) 1); |
|
7630 | 289 |
qed "project_Constrains_I"; |
290 |
||
291 |
Goalw [Stable_def] |
|
8128 | 292 |
"extend h F Join G : Stable (extend_set h A) \ |
293 |
\ ==> F Join project h (reachable (extend h F Join G)) G : Stable A"; |
|
7630 | 294 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
295 |
qed "project_Stable_I"; |
|
296 |
||
7689 | 297 |
Goalw [Always_def] |
8128 | 298 |
"extend h F Join G : Always (extend_set h A) \ |
299 |
\ ==> F Join project h (reachable (extend h F Join G)) G : Always A"; |
|
7689 | 300 |
by (auto_tac (claset(), simpset() addsimps [project_Stable_I])); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
301 |
by (rewtac extend_set_def); |
7689 | 302 |
by (Blast_tac 1); |
303 |
qed "project_Always_I"; |
|
304 |
||
7630 | 305 |
Goalw [Increasing_def] |
8128 | 306 |
"extend h F Join G : Increasing (func o f) \ |
307 |
\ ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"; |
|
7630 | 308 |
by Auto_tac; |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
309 |
by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect, |
7630 | 310 |
project_Stable_I]) 1); |
311 |
qed "project_Increasing_I"; |
|
312 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
313 |
Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B) = \ |
7630 | 314 |
\ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; |
315 |
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
|
316 |
qed "project_Constrains"; |
|
317 |
||
318 |
Goalw [Stable_def] |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
319 |
"(F Join project h (reachable (extend h F Join G)) G : Stable A) = \ |
7630 | 320 |
\ (extend h F Join G : Stable (extend_set h A))"; |
321 |
by (rtac project_Constrains 1); |
|
322 |
qed "project_Stable"; |
|
323 |
||
324 |
Goal |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
325 |
"(F Join project h (reachable (extend h F Join G)) G : Increasing func) = \ |
7630 | 326 |
\ (extend h F Join G : Increasing (func o f))"; |
327 |
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
328 |
extend_set_eq_Collect]) 1); |
7630 | 329 |
qed "project_Increasing"; |
330 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
331 |
(** A lot of redundant theorems: all are proved to facilitate reasoning |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
332 |
about guarantees. **) |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
333 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
334 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
335 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
336 |
\ (extend_set h A Co extend_set h B) (A Co B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
337 |
by (blast_tac (claset() addIs [project_Constrains_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
338 |
qed "projecting_Constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
339 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
340 |
Goalw [Stable_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
341 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
342 |
\ (Stable (extend_set h A)) (Stable A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
343 |
by (rtac projecting_Constrains 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
344 |
qed "projecting_Stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
345 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
346 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
347 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
348 |
\ (Always (extend_set h A)) (Always A)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
349 |
by (blast_tac (claset() addIs [project_Always_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
350 |
qed "projecting_Always"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
351 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
352 |
Goalw [projecting_def] |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
353 |
"projecting (%G. reachable (extend h F Join G)) h F \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
354 |
\ (Increasing (func o f)) (Increasing func)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
355 |
by (blast_tac (claset() addIs [project_Increasing_I]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
356 |
qed "projecting_Increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
357 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
358 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
359 |
"extending v (%G. reachable (extend h F Join G)) h F \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
360 |
\ (extend_set h A Co extend_set h B) (A Co B)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
361 |
by (blast_tac (claset() addIs [project_Constrains_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
362 |
qed "extending_Constrains"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
363 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
364 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
365 |
"extending v (%G. reachable (extend h F Join G)) h F \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
366 |
\ (Stable (extend_set h A)) (Stable A)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
367 |
by (blast_tac (claset() addIs [project_Stable_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
368 |
qed "extending_Stable"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
369 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
370 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
371 |
"extending v (%G. reachable (extend h F Join G)) h F \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
372 |
\ (Always (extend_set h A)) (Always A)"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
373 |
by (blast_tac (claset() addIs [project_Always_D]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
374 |
qed "extending_Always"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
375 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
376 |
Goalw [extending_def] |
8128 | 377 |
"extending v (%G. reachable (extend h F Join G)) h F \ |
378 |
\ (Increasing (func o f)) (Increasing func)"; |
|
379 |
by (blast_tac (claset() addIs [project_Increasing_D]) 1); |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
380 |
qed "extending_Increasing"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
381 |
|
7630 | 382 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
383 |
(*** leadsETo in the precondition (??) ***) |
7630 | 384 |
|
385 |
(** transient **) |
|
386 |
||
387 |
Goalw [transient_def] |
|
8110 | 388 |
"[| G : transient (C Int extend_set h A); G : stable C |] \ |
389 |
\ ==> project h C G : transient (project_set h C Int A)"; |
|
390 |
by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
|
391 |
by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1); |
|
392 |
by (asm_full_simp_tac |
|
393 |
(simpset() addsimps [stable_def, constrains_def]) 2); |
|
394 |
by (Blast_tac 2); |
|
395 |
(*back to main goal*) |
|
396 |
by (thin_tac "?AA <= -C Un ?BB" 1); |
|
397 |
by (ball_tac 1); |
|
398 |
by (asm_full_simp_tac |
|
399 |
(simpset() addsimps [extend_set_def, project_act_def]) 1); |
|
400 |
by (Blast_tac 1); |
|
7630 | 401 |
qed "transient_extend_set_imp_project_transient"; |
402 |
||
8110 | 403 |
(*converse might hold too?*) |
404 |
Goalw [transient_def] |
|
405 |
"project h C (extend h F) : transient (project_set h C Int D) \ |
|
406 |
\ ==> F : transient (project_set h C Int D)"; |
|
407 |
by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); |
|
408 |
by (rtac bexI 1); |
|
409 |
by (assume_tac 2); |
|
410 |
by Auto_tac; |
|
411 |
by (rewtac extend_act_def); |
|
412 |
by (Blast_tac 1); |
|
413 |
qed "project_extend_transient_D"; |
|
7630 | 414 |
|
8110 | 415 |
|
416 |
(** ensures -- a primitive combining progress with safety **) |
|
7630 | 417 |
|
8110 | 418 |
(*Used to prove project_leadsETo_I*) |
419 |
Goal "[| extend h F : stable C; G : stable C; \ |
|
420 |
\ extend h F Join G : A ensures B; A-B = C Int extend_set h D |] \ |
|
421 |
\ ==> F Join project h C G \ |
|
422 |
\ : (project_set h C Int project_set h A) ensures (project_set h B)"; |
|
7630 | 423 |
by (asm_full_simp_tac |
8110 | 424 |
(simpset() addsimps [ensures_def, Join_constrains, project_constrains, |
425 |
Join_transient, extend_transient]) 1); |
|
426 |
by (Clarify_tac 1); |
|
427 |
by (REPEAT_FIRST (rtac conjI)); |
|
428 |
(*first subgoal*) |
|
429 |
by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS |
|
430 |
constrains_Int RS constrains_weaken] |
|
431 |
addSDs [extend_constrains_project_set] |
|
432 |
addSDs [equalityD1]) 1); |
|
433 |
(*2nd subgoal*) |
|
434 |
by (etac (stableD RS constrains_Int RS constrains_weaken) 1); |
|
435 |
by (assume_tac 1); |
|
436 |
by (Blast_tac 3); |
|
437 |
by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib, |
|
438 |
extend_set_Un_distrib]) 2); |
|
439 |
by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2); |
|
440 |
by (full_simp_tac (simpset() addsimps [extend_set_def]) 1); |
|
9190 | 441 |
by (Blast_tac 1); |
8110 | 442 |
(*The transient part*) |
443 |
by Auto_tac; |
|
444 |
by (force_tac (claset() addSDs [equalityD1] |
|
445 |
addIs [transient_extend_set_imp_project_transient RS |
|
446 |
transient_strengthen], |
|
447 |
simpset()) 2); |
|
448 |
by (full_simp_tac (simpset() addsimps [Int_Diff]) 1); |
|
449 |
by (force_tac (claset() addSDs [equalityD1] |
|
450 |
addIs [transient_extend_set_imp_project_transient RS |
|
451 |
project_extend_transient_D RS transient_strengthen], |
|
452 |
simpset()) 1); |
|
7630 | 453 |
qed "ensures_extend_set_imp_project_ensures"; |
454 |
||
8110 | 455 |
(*Used to prove project_leadsETo_D*) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
456 |
Goal "[| project h C G ~: transient (A-B) | A<=B; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
457 |
\ extend h F Join G : stable C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
458 |
\ F Join project h C G : A ensures B |] \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
459 |
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
460 |
by (etac disjE 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
461 |
by (blast_tac (claset() addIs [subset_imp_ensures]) 2); |
8002 | 462 |
by (auto_tac (claset() addDs [extend_transient RS iffD2] |
8041 | 463 |
addIs [transient_strengthen, project_set_I, |
8002 | 464 |
project_unless RS unlessD, unlessI, |
465 |
project_extend_constrains_I], |
|
466 |
simpset() addsimps [ensures_def, Join_constrains, |
|
467 |
Join_stable, Join_transient])); |
|
7630 | 468 |
qed_spec_mp "Join_project_ensures"; |
469 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
470 |
(** Lemma useful for both STRONG and WEAK progress, but the transient |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
471 |
condition's very strong **) |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
472 |
|
7947 | 473 |
(*The strange induction formula allows induction over the leadsTo |
474 |
assumption's non-atomic precondition*) |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
475 |
Goal "[| ALL D. project h C G : transient D --> D={}; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
476 |
\ extend h F Join G : stable C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
477 |
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \ |
7947 | 478 |
\ ==> extend h F Join G : \ |
479 |
\ C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"; |
|
7630 | 480 |
by (etac leadsTo_induct 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
481 |
by (asm_simp_tac (simpset() delsimps UN_simps |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
482 |
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); |
8041 | 483 |
by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L, |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
484 |
leadsTo_Trans]) 2); |
7630 | 485 |
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
|
486 |
val lemma = result(); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
487 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
488 |
Goal "[| ALL D. project h C G : transient D --> D={}; \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
489 |
\ extend h F Join G : stable C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
490 |
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
491 |
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; |
7689 | 492 |
by (rtac (lemma RS leadsTo_weaken) 1); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
493 |
by (auto_tac (claset(), simpset() addsimps [split_extended_all])); |
8110 | 494 |
qed "project_leadsTo_D_lemma"; |
7630 | 495 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
496 |
Goal "[| C = (reachable (extend h F Join G)); \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
497 |
\ ALL D. project h C G : transient D --> D={}; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
498 |
\ F Join project h C G : A LeadsTo B |] \ |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
499 |
\ ==> 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
|
500 |
by (asm_full_simp_tac |
8110 | 501 |
(simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
502 |
project_set_reachable_extend_eq]) 1); |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
503 |
qed "Join_project_LeadsTo"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
504 |
|
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
505 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
506 |
(*** Towards project_Ensures_D ***) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
507 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
508 |
|
7630 | 509 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
510 |
Goalw [project_set_def, extend_set_def, project_act_def] |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
511 |
"act ^^ (C Int extend_set h A) <= B \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
512 |
\ ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
513 |
\ <= project_set h B"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
514 |
by (Blast_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
515 |
qed "act_subset_imp_project_act_subset"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
516 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
517 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
518 |
Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
519 |
\ project h C G : transient (project_set h C Int A - B) |] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
520 |
\ ==> G : transient (C Int extend_set h A - extend_set h B)"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
521 |
by (case_tac "C Int extend_set h A <= extend_set h B" 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
522 |
by (asm_simp_tac (simpset() addsimps [Diff_eq_empty_iff RS iffD2]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
523 |
by (auto_tac (claset(), |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
524 |
simpset() addsimps [transient_def, subset_Compl_self_eq, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
525 |
Domain_project_act, split_extended_all])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
526 |
by (Blast_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
527 |
by (auto_tac (claset(), |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
528 |
simpset() addsimps [stable_def, constrains_def])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
529 |
by (ball_tac 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
530 |
by (thin_tac "ALL act: Acts G. ?P act" 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
531 |
by (auto_tac (claset(), |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
532 |
simpset() addsimps [Int_Diff, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
533 |
extend_set_Diff_distrib RS sym])); |
8128 | 534 |
by (dtac act_subset_imp_project_act_subset 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
535 |
by (subgoal_tac |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
536 |
"project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1); |
8986 | 537 |
by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
538 |
(*using Int_greatest actually slows the next step!*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
539 |
by (Blast_tac 2); |
9083 | 540 |
by (rtac ccontr 1); |
541 |
by (dtac subsetD 1); |
|
542 |
by (Blast_tac 1); |
|
543 |
by (force_tac (claset(), simpset() addsimps [split_extended_all]) 1); |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
544 |
qed "stable_project_transient"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
545 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
546 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
547 |
Goal "[| G : stable C; project h C G : (project_set h C Int A) unless B |] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
548 |
\ ==> G : (C Int extend_set h A) unless (extend_set h B)"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
549 |
by (auto_tac |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
550 |
(claset() addDs [stable_constrains_Int] |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
551 |
addIs [constrains_weaken], |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
552 |
simpset() addsimps [unless_def, project_constrains, Diff_eq, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
553 |
Int_assoc, Int_extend_set_lemma])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
554 |
qed_spec_mp "project_unless2"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
555 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
556 |
Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
557 |
\ F Join project h C G : (project_set h C Int A) ensures B; \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
558 |
\ extend h F Join G : stable C |] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
559 |
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
560 |
(*unless*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
561 |
by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
562 |
addIs [project_extend_constrains_I], |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
563 |
simpset() addsimps [ensures_def, Join_constrains, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
564 |
Join_stable])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
565 |
(*transient*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
566 |
by (auto_tac (claset(), simpset() addsimps [Join_transient])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
567 |
by (blast_tac (claset() addIs [stable_project_transient]) 2); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
568 |
by (force_tac (claset() addSEs [extend_transient RS iffD2 RS |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
569 |
transient_strengthen], |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
570 |
simpset() addsimps [Join_transient, split_extended_all]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
571 |
qed "project_ensures_D_lemma"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
572 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
573 |
Goal "[| F Join project h UNIV G : A ensures B; \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
574 |
\ G : stable (extend_set h A - extend_set h B) |] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
575 |
\ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"; |
8128 | 576 |
by (rtac (project_ensures_D_lemma RS revcut_rl) 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
577 |
by (stac stable_UNIV 3); |
8128 | 578 |
by Auto_tac; |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
579 |
qed "project_ensures_D"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
580 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
581 |
Goalw [Ensures_def] |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
582 |
"[| F Join project h (reachable (extend h F Join G)) G : A Ensures B; \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
583 |
\ G : stable (reachable (extend h F Join G) Int extend_set h A - \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
584 |
\ extend_set h B) |] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
585 |
\ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"; |
8128 | 586 |
by (rtac (project_ensures_D_lemma RS revcut_rl) 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
587 |
by (auto_tac (claset(), |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
588 |
simpset() addsimps [project_set_reachable_extend_eq RS sym])); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
589 |
qed "project_Ensures_D"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
590 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
591 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
592 |
(*** Guarantees ***) |
7630 | 593 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
594 |
(*Weak precondition and postcondition |
7630 | 595 |
Not clear that it has a converse [or that we want one!]*) |
7841 | 596 |
|
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
597 |
(*The raw version; 3rd premise could be weakened by adding the |
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
598 |
precondition extend h F Join G : X' *) |
7841 | 599 |
val [xguary,project,extend] = |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
600 |
Goal "[| F : X guarantees[v] Y; \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
601 |
\ !!G. extend h F Join G : X' ==> F Join project h (C G) G : X; \ |
9337
58bd51302b21
used bounded quantification in definition of guarantees and other minor
paulson
parents:
9190
diff
changeset
|
602 |
\ !!G. [| F Join project h (C G) G : Y; G : preserves (v o f) |] \ |
7841 | 603 |
\ ==> extend h F Join G : Y' |] \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
604 |
\ ==> extend h F : X' guarantees[v o f] Y'"; |
7841 | 605 |
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
606 |
by (etac project_preserves_I 1); |
7841 | 607 |
by (etac project 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset
|
608 |
by Auto_tac; |
8041 | 609 |
qed "project_guarantees_raw"; |
7841 | 610 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
611 |
Goal "[| F : X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
612 |
\ projecting C h F X' X; extending w C h F Y' Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
613 |
\ preserves w <= preserves (v o f) |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
614 |
\ ==> extend h F : X' guarantees[w] Y'"; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
615 |
by (rtac guaranteesI 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
616 |
by (auto_tac (claset(), |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
617 |
simpset() addsimps [project_preserves_I, guaranteesD, projecting_def, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
618 |
extending_def])); |
7630 | 619 |
qed "project_guarantees"; |
620 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
621 |
|
7841 | 622 |
(*It seems that neither "guarantees" law can be proved from the other.*) |
7630 | 623 |
|
624 |
||
625 |
(*** guarantees corollaries ***) |
|
626 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
627 |
(** Some could be deleted: the required versions are easy to prove **) |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
628 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
629 |
Goal "F : UNIV guarantees[v] increasing func \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
630 |
\ ==> extend h F : X' guarantees[v o f] increasing (func o f)"; |
7630 | 631 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
632 |
by (rtac extending_increasing 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
633 |
by (rtac projecting_UNIV 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
634 |
by Auto_tac; |
7630 | 635 |
qed "extend_guar_increasing"; |
636 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
637 |
Goal "F : UNIV guarantees[v] Increasing func \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
638 |
\ ==> extend h F : X' guarantees[v o f] Increasing (func o f)"; |
7630 | 639 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
640 |
by (rtac extending_Increasing 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
641 |
by (rtac projecting_UNIV 1); |
7630 | 642 |
by Auto_tac; |
643 |
qed "extend_guar_Increasing"; |
|
644 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
645 |
Goal "F : Always A guarantees[v] Always B \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
646 |
\ ==> extend h F : Always(extend_set h A) guarantees[v o f] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
647 |
\ Always(extend_set h B)"; |
7689 | 648 |
by (etac project_guarantees 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
649 |
by (rtac extending_Always 2); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
650 |
by (rtac projecting_Always 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
651 |
by Auto_tac; |
7689 | 652 |
qed "extend_guar_Always"; |
653 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
654 |
Goal "[| G : preserves f; project h C G : transient D |] ==> D={}"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
655 |
by (rtac stable_transient_empty 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
656 |
by (assume_tac 2); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
657 |
by (blast_tac (claset() addIs [project_preserves_id_I, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
658 |
impOfSubs preserves_id_subset_stable]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
659 |
qed "preserves_project_transient_empty"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
660 |
|
7630 | 661 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
662 |
(** Guarantees with a leadsTo postcondition |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
663 |
THESE ARE ALL TOO WEAK because G can't affect F's variables at all**) |
7630 | 664 |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
665 |
Goal "[| F Join project h UNIV G : A leadsTo B; \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
666 |
\ G : preserves f |] \ |
7689 | 667 |
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
8110 | 668 |
by (res_inst_tac [("C1", "UNIV")] |
669 |
(project_leadsTo_D_lemma RS leadsTo_weaken) 1); |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
670 |
by (auto_tac (claset() addDs [preserves_project_transient_empty], |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
671 |
simpset())); |
7689 | 672 |
qed "project_leadsTo_D"; |
673 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
674 |
Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
675 |
\ G : preserves f |] \ |
7689 | 676 |
\ ==> 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
|
677 |
by (rtac (refl RS Join_project_LeadsTo) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
678 |
by (auto_tac (claset() addDs [preserves_project_transient_empty], |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
679 |
simpset())); |
7689 | 680 |
qed "project_LeadsTo_D"; |
681 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
682 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
683 |
"extending f (%G. UNIV) h F \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
684 |
\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
685 |
by (blast_tac (claset() addIs [project_leadsTo_D]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
686 |
qed "extending_leadsTo"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
687 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
688 |
Goalw [extending_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
689 |
"extending f (%G. reachable (extend h F Join G)) h F \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
690 |
\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
691 |
by (blast_tac (claset() addIs [project_LeadsTo_D]) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
692 |
qed "extending_LeadsTo"; |
7689 | 693 |
|
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
694 |
(*STRONG precondition and postcondition*) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
695 |
Goal "F : (A co A') guarantees[v] (B leadsTo B') \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
696 |
\ ==> extend h F : (extend_set h A co extend_set h A') \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
697 |
\ guarantees[f] (extend_set h B leadsTo extend_set h B')"; |
7630 | 698 |
by (etac project_guarantees 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
699 |
by (rtac subset_preserves_o 3); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
700 |
by (rtac extending_leadsTo 2); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
701 |
by (rtac projecting_constrains 1); |
7630 | 702 |
qed "extend_co_guar_leadsTo"; |
703 |
||
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
704 |
(*WEAK precondition and postcondition*) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
705 |
Goal "F : (A Co A') guarantees[v] (B LeadsTo B') \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
706 |
\ ==> extend h F : (extend_set h A Co extend_set h A') \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
707 |
\ guarantees[f] (extend_set h B LeadsTo extend_set h B')"; |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
708 |
by (etac project_guarantees 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
709 |
by (rtac subset_preserves_o 3); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
710 |
by (rtac extending_LeadsTo 2); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
711 |
by (rtac projecting_Constrains 1); |
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
712 |
qed "extend_Co_guar_LeadsTo"; |
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset
|
713 |
|
7630 | 714 |
Close_locale "Extend"; |