author  paulson 
Fri, 16 Jun 2000 13:39:21 +0200  
changeset 9083  b36787a56a1f 
parent 8986  8b7718296a35 
child 9190  b86ff604729f 
permissions  rwrr 
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 

7630  30 
(*This form's useful with guarantees reasoning*) 
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

31 
Goal "(F Join project h C G : A co B) = \ 
7630  32 
\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ 
33 
\ F : A co B)"; 

34 
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1); 

35 
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken] 

36 
addDs [constrains_imp_subset]) 1); 

37 
qed "Join_project_constrains"; 

38 

39 
(*The condition is required to prove the lefttoright direction; 

40 
could weaken it to G : (C Int extend_set h A) co C*) 

41 
Goalw [stable_def] 

42 
"extend h F Join G : stable C \ 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

43 
\ ==> (F Join project h C G : stable A) = \ 
7630  44 
\ (extend h F Join G : stable (C Int extend_set h A) & \ 
45 
\ F : stable A)"; 

46 
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); 

47 
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); 

48 
qed "Join_project_stable"; 

49 

7689  50 
(*For using project_guarantees in particular cases*) 
51 
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

52 
\ ==> F Join project h C G : A co B"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

53 
by (asm_full_simp_tac 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

54 
(simpset() addsimps [project_constrains, Join_constrains, 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

55 
extend_constrains]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

56 
by (blast_tac (claset() addIs [constrains_weaken] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

57 
addDs [constrains_imp_subset]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

58 
qed "project_constrains_I"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

59 

8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

60 
Goalw [increasing_def, stable_def] 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

61 
"extend h F Join G : increasing (func o f) \ 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

62 
\ ==> F Join project h C G : increasing func"; 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

63 
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

64 
extend_set_eq_Collect]) 1); 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

65 
qed "project_increasing_I"; 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

66 

19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

67 
Goal "(F Join project h UNIV G : increasing func) = \ 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

68 
\ (extend h F Join G : increasing (func o f))"; 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

69 
by (rtac iffI 1); 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

70 
by (etac project_increasing_I 2); 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

71 
by (asm_full_simp_tac 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

72 
(simpset() addsimps [increasing_def, Join_project_stable]) 1); 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

73 
by (auto_tac (claset(), 
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset

74 
simpset() addsimps [Join_stable, extend_set_eq_Collect, 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

75 
extend_stable RS iffD1])); 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

76 
qed "Join_project_increasing"; 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

77 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

78 
(*The UNIV argument is essential*) 
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

79 
Goal "F Join project h UNIV G : A co B \ 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

80 
\ ==> extend h F Join G : extend_set h A co extend_set h B"; 
7689  81 
by (asm_full_simp_tac 
82 
(simpset() addsimps [project_constrains, Join_constrains, 

83 
extend_constrains]) 1); 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

84 
qed "project_constrains_D"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

85 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

86 

b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

87 
(*** "projecting" and union/intersection (no converses) ***) 
7841  88 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

89 
Goalw [projecting_def] 
7841  90 
"[ projecting C h F XA' XA; projecting C h F XB' XB ] \ 
91 
\ ==> projecting C h F (XA' Int XB') (XA Int XB)"; 

92 
by (Blast_tac 1); 

93 
qed "projecting_Int"; 

94 

95 
Goalw [projecting_def] 

96 
"[ projecting C h F XA' XA; projecting C h F XB' XB ] \ 

97 
\ ==> projecting C h F (XA' Un XB') (XA Un XB)"; 

98 
by (Blast_tac 1); 

99 
qed "projecting_Un"; 

100 

101 
val [prem] = Goalw [projecting_def] 

102 
"[ !!i. i:I ==> projecting C h F (X' i) (X i) ] \ 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

103 
\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"; 
7841  104 
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

105 
qed "projecting_INT"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

106 

7841  107 
val [prem] = Goalw [projecting_def] 
108 
"[ !!i. i:I ==> projecting C h F (X' i) (X i) ] \ 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

109 
\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"; 
7841  110 
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

111 
qed "projecting_UN"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

112 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

113 
Goalw [projecting_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

114 
"[ 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

115 
by Auto_tac; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

116 
qed "projecting_weaken"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

117 

8073  118 
Goalw [projecting_def] 
119 
"[ projecting C h F X' X; U'<=X' ] ==> projecting C h F U' X"; 

120 
by Auto_tac; 

121 
qed "projecting_weaken_L"; 

122 

7841  123 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

124 
"[ 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

125 
\ ==> extending v C h F (YA' Int YB') (YA Int YB)"; 
7841  126 
by (Blast_tac 1); 
127 
qed "extending_Int"; 

128 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

129 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

130 
"[ 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

131 
\ ==> extending v C h F (YA' Un YB') (YA Un YB)"; 
7841  132 
by (Blast_tac 1); 
133 
qed "extending_Un"; 

134 

135 
val [prem] = Goalw [extending_def] 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

136 
"[ !!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

137 
\ ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)"; 
7841  138 
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

139 
qed "extending_INT"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

140 

7841  141 
val [prem] = Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

142 
"[ !!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

143 
\ ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y 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 "extending_UN"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

146 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

147 
Goalw [extending_def] 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

148 
"[ extending v C h F Y' Y; Y'<=V'; V<=Y; \ 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

149 
\ preserves w <= preserves v ] \ 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

150 
\ ==> extending w C h F V' V"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

151 
by Auto_tac; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

152 
qed "extending_weaken"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

153 

8073  154 
Goalw [extending_def] 
155 
"[ extending v C h F Y' Y; Y'<=V' ] ==> extending v C h F V' Y"; 

156 
by Auto_tac; 

157 
qed "extending_weaken_L"; 

158 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

159 
Goal "projecting C h F X' UNIV"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

160 
by (simp_tac (simpset() addsimps [projecting_def]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

161 
qed "projecting_UNIV"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

162 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

163 
Goalw [projecting_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

164 
"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

165 
by (blast_tac (claset() addIs [project_constrains_I]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

166 
qed "projecting_constrains"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

167 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

168 
Goalw [stable_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

169 
"projecting C h F (stable (extend_set h A)) (stable A)"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

170 
by (rtac projecting_constrains 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

171 
qed "projecting_stable"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

172 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

173 
Goalw [projecting_def] 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

174 
"projecting C h F (increasing (func o f)) (increasing func)"; 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

175 
by (blast_tac (claset() addIs [project_increasing_I]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

176 
qed "projecting_increasing"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

177 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

178 
Goal "extending v C h F UNIV Y"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

179 
by (simp_tac (simpset() addsimps [extending_def]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

180 
qed "extending_UNIV"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

181 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

182 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

183 
"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

184 
by (blast_tac (claset() addIs [project_constrains_D]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

185 
qed "extending_constrains"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

186 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

187 
Goalw [stable_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

188 
"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

189 
by (rtac extending_constrains 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

190 
qed "extending_stable"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

191 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

192 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

193 
"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

194 
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

195 
qed "extending_increasing"; 
7689  196 

7630  197 

198 
(** Reachability and project **) 

199 

200 
Goal "[ reachable (extend h F Join G) <= C; \ 

201 
\ z : reachable (extend h F Join G) ] \ 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

202 
\ ==> f z : reachable (F Join project h C G)"; 
7630  203 
by (etac reachable.induct 1); 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

204 
by (force_tac (claset() addSIs [reachable.Init], 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

205 
simpset() addsimps [split_extended_all]) 1); 
7630  206 
by Auto_tac; 
207 
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)], 

208 
simpset()) 2); 

209 
by (res_inst_tac [("act","x")] reachable.Acts 1); 

210 
by Auto_tac; 

211 
by (etac extend_act_D 1); 

212 
qed "reachable_imp_reachable_project"; 

213 

214 
Goalw [Constrains_def] 

8128  215 
"F Join project h (reachable (extend h F Join G)) G : A Co B \ 
7630  216 
\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; 
217 
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); 

218 
by (Clarify_tac 1); 

219 
by (etac constrains_weaken 1); 

8128  220 
by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset())); 
7630  221 
qed "project_Constrains_D"; 
222 

223 
Goalw [Stable_def] 

8128  224 
"F Join project h (reachable (extend h F Join G)) G : Stable A \ 
7630  225 
\ ==> extend h F Join G : Stable (extend_set h A)"; 
226 
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); 

227 
qed "project_Stable_D"; 

228 

229 
Goalw [Always_def] 

8128  230 
"F Join project h (reachable (extend h F Join G)) G : Always A \ 
7630  231 
\ ==> extend h F Join G : Always (extend_set h A)"; 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

232 
by (force_tac (claset() addIs [reachable.Init], 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

233 
simpset() addsimps [project_Stable_D, split_extended_all]) 1); 
7630  234 
qed "project_Always_D"; 
235 

236 
Goalw [Increasing_def] 

8128  237 
"F Join project h (reachable (extend h F Join G)) G : Increasing func \ 
7630  238 
\ ==> extend h F Join G : Increasing (func o f)"; 
239 
by Auto_tac; 

8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset

240 
by (stac (extend_set_eq_Collect RS sym) 1); 
7630  241 
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
242 
qed "project_Increasing_D"; 

243 

244 

245 
(** Converse results for weak safety: benefits of the argument C *) 

246 

247 
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

248 
\ x : reachable (F Join project h C G) ] \ 
7630  249 
\ ==> EX y. h(x,y) : reachable (extend h F Join G)"; 
250 
by (etac reachable.induct 1); 

251 
by (ALLGOALS Asm_full_simp_tac); 

252 
(*SLOW: 6.7s*) 

253 
by (force_tac (claset() delrules [Id_in_Acts] 

254 
addIs [reachable.Acts, extend_act_D], 

255 
simpset() addsimps [project_act_def]) 2); 

256 
by (force_tac (claset() addIs [reachable.Init], 

8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

257 
simpset()) 1); 
7630  258 
qed "reachable_project_imp_reachable"; 
259 

7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

260 
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

261 
\ 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

262 
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

263 
subset_refl RS reachable_project_imp_reachable], 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

264 
simpset())); 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

265 
qed "project_set_reachable_extend_eq"; 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

266 

7947  267 
Goal "reachable (extend h F Join G) <= C \ 
268 
\ ==> reachable (extend h F Join G) <= \ 

269 
\ extend_set h (reachable (F Join project h C G))"; 

270 
by (auto_tac (claset() addDs [reachable_imp_reachable_project], 

271 
simpset())); 

272 
qed "reachable_extend_Join_subset"; 

273 

7630  274 
Goalw [Constrains_def] 
8128  275 
"extend h F Join G : (extend_set h A) Co (extend_set h B) \ 
276 
\ ==> F Join project h (reachable (extend h F Join G)) G : A Co B"; 

7630  277 
by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
278 
extend_set_Int_distrib]) 1); 

279 
by (rtac conjI 1); 

8128  280 
by (force_tac 
281 
(claset() addEs [constrains_weaken_L] 

282 
addSDs [extend_constrains_project_set, 

283 
subset_refl RS reachable_project_imp_reachable], 

284 
simpset() addsimps [Join_constrains]) 2); 

285 
by (blast_tac (claset() addIs [constrains_weaken_L]) 1); 

7630  286 
qed "project_Constrains_I"; 
287 

288 
Goalw [Stable_def] 

8128  289 
"extend h F Join G : Stable (extend_set h A) \ 
290 
\ ==> F Join project h (reachable (extend h F Join G)) G : Stable A"; 

7630  291 
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); 
292 
qed "project_Stable_I"; 

293 

7689  294 
Goalw [Always_def] 
8128  295 
"extend h F Join G : Always (extend_set h A) \ 
296 
\ ==> F Join project h (reachable (extend h F Join G)) G : Always A"; 

7689  297 
by (auto_tac (claset(), simpset() addsimps [project_Stable_I])); 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

298 
by (rewtac extend_set_def); 
7689  299 
by (Blast_tac 1); 
300 
qed "project_Always_I"; 

301 

7630  302 
Goalw [Increasing_def] 
8128  303 
"extend h F Join G : Increasing (func o f) \ 
304 
\ ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"; 

7630  305 
by Auto_tac; 
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset

306 
by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect, 
7630  307 
project_Stable_I]) 1); 
308 
qed "project_Increasing_I"; 

309 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

310 
Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B) = \ 
7630  311 
\ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; 
312 
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); 

313 
qed "project_Constrains"; 

314 

315 
Goalw [Stable_def] 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

316 
"(F Join project h (reachable (extend h F Join G)) G : Stable A) = \ 
7630  317 
\ (extend h F Join G : Stable (extend_set h A))"; 
318 
by (rtac project_Constrains 1); 

319 
qed "project_Stable"; 

320 

321 
Goal 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

322 
"(F Join project h (reachable (extend h F Join G)) G : Increasing func) = \ 
7630  323 
\ (extend h F Join G : Increasing (func o f))"; 
324 
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

325 
extend_set_eq_Collect]) 1); 
7630  326 
qed "project_Increasing"; 
327 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

328 
(** A lot of redundant theorems: all are proved to facilitate reasoning 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

329 
about guarantees. **) 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

330 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

331 
Goalw [projecting_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

332 
"projecting (%G. reachable (extend h F Join G)) h F \ 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

333 
\ (extend_set h A Co extend_set h B) (A Co B)"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

334 
by (blast_tac (claset() addIs [project_Constrains_I]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

335 
qed "projecting_Constrains"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

336 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

337 
Goalw [Stable_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

338 
"projecting (%G. reachable (extend h F Join G)) h F \ 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

339 
\ (Stable (extend_set h A)) (Stable A)"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

340 
by (rtac projecting_Constrains 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

341 
qed "projecting_Stable"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

342 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

343 
Goalw [projecting_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

344 
"projecting (%G. reachable (extend h F Join G)) h F \ 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

345 
\ (Always (extend_set h A)) (Always A)"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

346 
by (blast_tac (claset() addIs [project_Always_I]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

347 
qed "projecting_Always"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

348 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

349 
Goalw [projecting_def] 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

350 
"projecting (%G. reachable (extend h F Join G)) h F \ 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

351 
\ (Increasing (func o f)) (Increasing func)"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

352 
by (blast_tac (claset() addIs [project_Increasing_I]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

353 
qed "projecting_Increasing"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

354 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

355 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

356 
"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

357 
\ (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

358 
by (blast_tac (claset() addIs [project_Constrains_D]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

359 
qed "extending_Constrains"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

360 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

361 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

362 
"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

363 
\ (Stable (extend_set h A)) (Stable A)"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

364 
by (blast_tac (claset() addIs [project_Stable_D]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

365 
qed "extending_Stable"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

366 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

367 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

368 
"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

369 
\ (Always (extend_set h A)) (Always A)"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

370 
by (blast_tac (claset() addIs [project_Always_D]) 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

371 
qed "extending_Always"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

372 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

373 
Goalw [extending_def] 
8128  374 
"extending v (%G. reachable (extend h F Join G)) h F \ 
375 
\ (Increasing (func o f)) (Increasing func)"; 

376 
by (blast_tac (claset() addIs [project_Increasing_D]) 1); 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

377 
qed "extending_Increasing"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

378 

7630  379 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

380 
(*** leadsETo in the precondition (??) ***) 
7630  381 

382 
(** transient **) 

383 

384 
Goalw [transient_def] 

8110  385 
"[ G : transient (C Int extend_set h A); G : stable C ] \ 
386 
\ ==> project h C G : transient (project_set h C Int A)"; 

387 
by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); 

388 
by (subgoal_tac "act ^^ (C Int extend_set h A) <=  extend_set h A" 1); 

389 
by (asm_full_simp_tac 

390 
(simpset() addsimps [stable_def, constrains_def]) 2); 

391 
by (Blast_tac 2); 

392 
(*back to main goal*) 

393 
by (thin_tac "?AA <= C Un ?BB" 1); 

394 
by (ball_tac 1); 

395 
by (asm_full_simp_tac 

396 
(simpset() addsimps [extend_set_def, project_act_def]) 1); 

397 
by (Blast_tac 1); 

7630  398 
qed "transient_extend_set_imp_project_transient"; 
399 

8110  400 
(*converse might hold too?*) 
401 
Goalw [transient_def] 

402 
"project h C (extend h F) : transient (project_set h C Int D) \ 

403 
\ ==> F : transient (project_set h C Int D)"; 

404 
by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); 

405 
by (rtac bexI 1); 

406 
by (assume_tac 2); 

407 
by Auto_tac; 

408 
by (rewtac extend_act_def); 

409 
by (Blast_tac 1); 

410 
qed "project_extend_transient_D"; 

7630  411 

8110  412 

413 
(** ensures  a primitive combining progress with safety **) 

7630  414 

8110  415 
(*Used to prove project_leadsETo_I*) 
416 
Goal "[ extend h F : stable C; G : stable C; \ 

417 
\ extend h F Join G : A ensures B; AB = C Int extend_set h D ] \ 

418 
\ ==> F Join project h C G \ 

419 
\ : (project_set h C Int project_set h A) ensures (project_set h B)"; 

7630  420 
by (asm_full_simp_tac 
8110  421 
(simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
422 
Join_transient, extend_transient]) 1); 

423 
by (Clarify_tac 1); 

424 
by (REPEAT_FIRST (rtac conjI)); 

425 
(*first subgoal*) 

426 
by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS 

427 
constrains_Int RS constrains_weaken] 

428 
addSDs [extend_constrains_project_set] 

429 
addSDs [equalityD1]) 1); 

430 
(*2nd subgoal*) 

431 
by (etac (stableD RS constrains_Int RS constrains_weaken) 1); 

432 
by (assume_tac 1); 

433 
by (Blast_tac 3); 

434 
by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib, 

435 
extend_set_Un_distrib]) 2); 

436 
by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2); 

437 
by (full_simp_tac (simpset() addsimps [extend_set_def]) 1); 

438 
by (blast_tac (claset() addSEs [equalityE]) 1); 

439 
(*The transient part*) 

440 
by Auto_tac; 

441 
by (force_tac (claset() addSDs [equalityD1] 

442 
addIs [transient_extend_set_imp_project_transient RS 

443 
transient_strengthen], 

444 
simpset()) 2); 

445 
by (full_simp_tac (simpset() addsimps [Int_Diff]) 1); 

446 
by (force_tac (claset() addSDs [equalityD1] 

447 
addIs [transient_extend_set_imp_project_transient RS 

448 
project_extend_transient_D RS transient_strengthen], 

449 
simpset()) 1); 

7630  450 
qed "ensures_extend_set_imp_project_ensures"; 
451 

8110  452 
(*Used to prove project_leadsETo_D*) 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

453 
Goal "[ project h C G ~: transient (AB)  A<=B; \ 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

454 
\ extend h F Join G : stable C; \ 
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

455 
\ 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

456 
\ ==> 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

457 
by (etac disjE 1); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

458 
by (blast_tac (claset() addIs [subset_imp_ensures]) 2); 
8002  459 
by (auto_tac (claset() addDs [extend_transient RS iffD2] 
8041  460 
addIs [transient_strengthen, project_set_I, 
8002  461 
project_unless RS unlessD, unlessI, 
462 
project_extend_constrains_I], 

463 
simpset() addsimps [ensures_def, Join_constrains, 

464 
Join_stable, Join_transient])); 

7630  465 
qed_spec_mp "Join_project_ensures"; 
466 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

467 
(** 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

468 
condition's very strong **) 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

469 

7947  470 
(*The strange induction formula allows induction over the leadsTo 
471 
assumption's nonatomic precondition*) 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

472 
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

473 
\ extend h F Join G : stable C; \ 
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

474 
\ F Join project h C G : (project_set h C Int A) leadsTo B ] \ 
7947  475 
\ ==> extend h F Join G : \ 
476 
\ C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"; 

7630  477 
by (etac leadsTo_induct 1); 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

478 
by (asm_simp_tac (simpset() delsimps UN_simps 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

479 
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3); 
8041  480 
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

481 
leadsTo_Trans]) 2); 
7630  482 
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

483 
val lemma = result(); 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

484 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

485 
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

486 
\ extend h F Join G : stable C; \ 
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

487 
\ 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

488 
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"; 
7689  489 
by (rtac (lemma RS leadsTo_weaken) 1); 
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

490 
by (auto_tac (claset(), simpset() addsimps [split_extended_all])); 
8110  491 
qed "project_leadsTo_D_lemma"; 
7630  492 

7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

493 
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

494 
\ 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

495 
\ 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

496 
\ ==> 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

497 
by (asm_full_simp_tac 
8110  498 
(simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

499 
project_set_reachable_extend_eq]) 1); 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

500 
qed "Join_project_LeadsTo"; 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

501 

7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

502 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

503 
(*** Towards project_Ensures_D ***) 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

504 

b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

505 

7630  506 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

507 
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

508 
"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

509 
\ ==> 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

510 
\ <= project_set h B"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

511 
by (Blast_tac 1); 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

512 
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

513 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

514 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

515 
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

516 
\ 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

517 
\ ==> 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

518 
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

519 
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

520 
by (auto_tac (claset(), 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

521 
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

522 
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

523 
by (Blast_tac 1); 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

524 
by (auto_tac (claset(), 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

525 
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

526 
by (ball_tac 1); 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

527 
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

528 
by (auto_tac (claset(), 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

529 
simpset() addsimps [Int_Diff, 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

530 
extend_set_Diff_distrib RS sym])); 
8128  531 
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

532 
by (subgoal_tac 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

533 
"project_act h (Restrict C act) ^^ (project_set h C Int (A  B)) <= {}" 1); 
8986  534 
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

535 
(*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

536 
by (Blast_tac 2); 
9083  537 
by (rtac ccontr 1); 
538 
by (dtac subsetD 1); 

539 
by (Blast_tac 1); 

540 
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

541 
qed "stable_project_transient"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

542 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

543 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

544 
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

545 
\ ==> 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

546 
by (auto_tac 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

547 
(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

548 
addIs [constrains_weaken], 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

549 
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

550 
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

551 
qed_spec_mp "project_unless2"; 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

552 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

553 
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

554 
\ 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

555 
\ 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

556 
\ ==> 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

557 
(*unless*) 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

558 
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

559 
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

560 
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

561 
Join_stable])); 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

562 
(*transient*) 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

563 
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

564 
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

565 
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

566 
transient_strengthen], 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

567 
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

568 
qed "project_ensures_D_lemma"; 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

569 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

570 
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

571 
\ 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

572 
\ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"; 
8128  573 
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

574 
by (stac stable_UNIV 3); 
8128  575 
by Auto_tac; 
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

576 
qed "project_ensures_D"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

577 

b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

578 
Goalw [Ensures_def] 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

579 
"[ 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

580 
\ 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

581 
\ extend_set h B) ] \ 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

582 
\ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"; 
8128  583 
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

584 
by (auto_tac (claset(), 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

585 
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

586 
qed "project_Ensures_D"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

587 

b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

588 

8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset

589 
(*** Guarantees ***) 
7630  590 

8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset

591 
(*Weak precondition and postcondition 
7630  592 
Not clear that it has a converse [or that we want one!]*) 
7841  593 

594 
(*The raw version*) 

595 
val [xguary,project,extend] = 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

596 
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

597 
\ !!G. extend h F Join G : X' ==> F Join project h (C G) G : X; \ 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

598 
\ !!G. [ F Join project h (C G) G : Y; extend h F Join G : X'; \ 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8110
diff
changeset

599 
\ G : preserves (v o f) ] \ 
7841  600 
\ ==> extend h F Join G : Y' ] \ 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

601 
\ ==> extend h F : X' guarantees[v o f] Y'"; 
7841  602 
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

603 
by (etac project_preserves_I 1); 
7841  604 
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

605 
by Auto_tac; 
8041  606 
qed "project_guarantees_raw"; 
7841  607 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

608 
Goal "[ F : X guarantees[v] Y; \ 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

609 
\ 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

610 
\ preserves w <= preserves (v o f) ] \ 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

611 
\ ==> extend h F : X' guarantees[w] Y'"; 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

612 
by (rtac guaranteesI 1); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

613 
by (auto_tac (claset(), 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

614 
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

615 
extending_def])); 
7630  616 
qed "project_guarantees"; 
617 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

618 

7841  619 
(*It seems that neither "guarantees" law can be proved from the other.*) 
7630  620 

621 

622 
(*** guarantees corollaries ***) 

623 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

624 
(** Some could be deleted: the required versions are easy to prove **) 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

625 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

626 
Goal "F : UNIV guarantees[v] increasing func \ 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

627 
\ ==> extend h F : X' guarantees[v o f] increasing (func o f)"; 
7630  628 
by (etac project_guarantees 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

629 
by (rtac extending_increasing 2); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

630 
by (rtac projecting_UNIV 1); 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

631 
by Auto_tac; 
7630  632 
qed "extend_guar_increasing"; 
633 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

634 
Goal "F : UNIV guarantees[v] Increasing func \ 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

635 
\ ==> extend h F : X' guarantees[v o f] Increasing (func o f)"; 
7630  636 
by (etac project_guarantees 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

637 
by (rtac extending_Increasing 2); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

638 
by (rtac projecting_UNIV 1); 
7630  639 
by Auto_tac; 
640 
qed "extend_guar_Increasing"; 

641 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

642 
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

643 
\ ==> 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

644 
\ Always(extend_set h B)"; 
7689  645 
by (etac project_guarantees 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

646 
by (rtac extending_Always 2); 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

647 
by (rtac projecting_Always 1); 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

648 
by Auto_tac; 
7689  649 
qed "extend_guar_Always"; 
650 

8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

651 
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

652 
by (rtac stable_transient_empty 1); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

653 
by (assume_tac 2); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

654 
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

655 
impOfSubs preserves_id_subset_stable]) 1); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

656 
qed "preserves_project_transient_empty"; 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

657 

7630  658 

8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

659 
(** Guarantees with a leadsTo postcondition 
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset

660 
THESE ARE ALL TOO WEAK because G can't affect F's variables at all**) 
7630  661 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

662 
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

663 
\ G : preserves f ] \ 
7689  664 
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; 
8110  665 
by (res_inst_tac [("C1", "UNIV")] 
666 
(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

667 
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

668 
simpset())); 
7689  669 
qed "project_leadsTo_D"; 
670 

7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset

671 
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

672 
\ G : preserves f ] \ 
7689  673 
\ ==> 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

674 
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

675 
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

676 
simpset())); 
7689  677 
qed "project_LeadsTo_D"; 
678 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

679 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

680 
"extending f (%G. UNIV) h F \ 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

681 
\ (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

682 
by (blast_tac (claset() addIs [project_leadsTo_D]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

683 
qed "extending_leadsTo"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

684 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

685 
Goalw [extending_def] 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

686 
"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

687 
\ (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

688 
by (blast_tac (claset() addIs [project_LeadsTo_D]) 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset

689 
qed "extending_LeadsTo"; 
7689  690 

7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

691 
(*STRONG precondition and postcondition*) 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

692 
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

693 
\ ==> 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

694 
\ guarantees[f] (extend_set h B leadsTo extend_set h B')"; 
7630  695 
by (etac project_guarantees 1); 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

696 
by (rtac subset_preserves_o 3); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

697 
by (rtac extending_leadsTo 2); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

698 
by (rtac projecting_constrains 1); 
7630  699 
qed "extend_co_guar_leadsTo"; 
700 

7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

701 
(*WEAK precondition and postcondition*) 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

702 
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

703 
\ ==> 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

704 
\ 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

705 
by (etac project_guarantees 1); 
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

706 
by (rtac subset_preserves_o 3); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

707 
by (rtac extending_LeadsTo 2); 
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset

708 
by (rtac projecting_Constrains 1); 
7660
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

709 
qed "extend_Co_guar_LeadsTo"; 
7e38237edfcb
now with (weak safety) guarantees (weak progress) with Extend
paulson
parents:
7630
diff
changeset

710 

7630  711 
Close_locale "Extend"; 