4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 The "Follows" relation of Charpentier and Sivilotte |
6 The "Follows" relation of Charpentier and Sivilotte |
7 *) |
7 *) |
8 |
8 |
9 Follows = SubstAx + ListOrder + Multiset + |
9 theory Follows = SubstAx + ListOrder + Multiset: |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" |
13 Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" |
14 (infixl "Fols" 65) |
14 (infixl "Fols" 65) |
15 "f Fols g == Increasing g Int Increasing f Int |
15 "f Fols g == Increasing g Int Increasing f Int |
16 Always {s. f s <= g s} Int |
16 Always {s. f s <= g s} Int |
17 (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" |
17 (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" |
18 |
18 |
19 |
19 |
|
20 (*Does this hold for "invariant"?*) |
|
21 lemma mono_Always_o: |
|
22 "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}" |
|
23 apply (simp add: Always_eq_includes_reachable) |
|
24 apply (blast intro: monoD) |
|
25 done |
|
26 |
|
27 lemma mono_LeadsTo_o: |
|
28 "mono (h::'a::order => 'b::order) |
|
29 ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= |
|
30 (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})" |
|
31 apply auto |
|
32 apply (rule single_LeadsTo_I) |
|
33 apply (drule_tac x = "g s" in spec) |
|
34 apply (erule LeadsTo_weaken) |
|
35 apply (blast intro: monoD order_trans)+ |
|
36 done |
|
37 |
|
38 lemma Follows_constant: "F : (%s. c) Fols (%s. c)" |
|
39 by (unfold Follows_def, auto) |
|
40 declare Follows_constant [iff] |
|
41 |
|
42 lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)" |
|
43 apply (unfold Follows_def, clarify) |
|
44 apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD] |
|
45 mono_Always_o [THEN [2] rev_subsetD] |
|
46 mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D]) |
|
47 done |
|
48 |
|
49 lemma mono_Follows_apply: |
|
50 "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))" |
|
51 apply (drule mono_Follows_o) |
|
52 apply (force simp add: o_def) |
|
53 done |
|
54 |
|
55 lemma Follows_trans: |
|
56 "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h" |
|
57 apply (unfold Follows_def) |
|
58 apply (simp add: Always_eq_includes_reachable) |
|
59 apply (blast intro: order_trans LeadsTo_Trans) |
|
60 done |
|
61 |
|
62 |
|
63 (** Destructiom rules **) |
|
64 |
|
65 lemma Follows_Increasing1: |
|
66 "F : f Fols g ==> F : Increasing f" |
|
67 |
|
68 apply (unfold Follows_def, blast) |
|
69 done |
|
70 |
|
71 lemma Follows_Increasing2: |
|
72 "F : f Fols g ==> F : Increasing g" |
|
73 apply (unfold Follows_def, blast) |
|
74 done |
|
75 |
|
76 lemma Follows_Bounded: |
|
77 "F : f Fols g ==> F : Always {s. f s <= g s}" |
|
78 apply (unfold Follows_def, blast) |
|
79 done |
|
80 |
|
81 lemma Follows_LeadsTo: |
|
82 "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}" |
|
83 apply (unfold Follows_def, blast) |
|
84 done |
|
85 |
|
86 lemma Follows_LeadsTo_pfixLe: |
|
87 "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}" |
|
88 apply (rule single_LeadsTo_I, clarify) |
|
89 apply (drule_tac k="g s" in Follows_LeadsTo) |
|
90 apply (erule LeadsTo_weaken) |
|
91 apply blast |
|
92 apply (blast intro: pfixLe_trans prefix_imp_pfixLe) |
|
93 done |
|
94 |
|
95 lemma Follows_LeadsTo_pfixGe: |
|
96 "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}" |
|
97 apply (rule single_LeadsTo_I, clarify) |
|
98 apply (drule_tac k="g s" in Follows_LeadsTo) |
|
99 apply (erule LeadsTo_weaken) |
|
100 apply blast |
|
101 apply (blast intro: pfixGe_trans prefix_imp_pfixGe) |
|
102 done |
|
103 |
|
104 |
|
105 lemma Always_Follows1: |
|
106 "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g" |
|
107 |
|
108 apply (unfold Follows_def Increasing_def Stable_def, auto) |
|
109 apply (erule_tac [3] Always_LeadsTo_weaken) |
|
110 apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" in Always_Constrains_weaken, auto) |
|
111 apply (drule Always_Int_I, assumption) |
|
112 apply (force intro: Always_weaken) |
|
113 done |
|
114 |
|
115 lemma Always_Follows2: |
|
116 "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'" |
|
117 apply (unfold Follows_def Increasing_def Stable_def, auto) |
|
118 apply (erule_tac [3] Always_LeadsTo_weaken) |
|
119 apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" in Always_Constrains_weaken, auto) |
|
120 apply (drule Always_Int_I, assumption) |
|
121 apply (force intro: Always_weaken) |
|
122 done |
|
123 |
|
124 |
|
125 (** Union properties (with the subset ordering) **) |
|
126 |
|
127 (*Can replace "Un" by any sup. But existing max only works for linorders.*) |
|
128 lemma increasing_Un: |
|
129 "[| F : increasing f; F: increasing g |] |
|
130 ==> F : increasing (%s. (f s) Un (g s))" |
|
131 apply (unfold increasing_def stable_def constrains_def, auto) |
|
132 apply (drule_tac x = "f xa" in spec) |
|
133 apply (drule_tac x = "g xa" in spec) |
|
134 apply (blast dest!: bspec) |
|
135 done |
|
136 |
|
137 lemma Increasing_Un: |
|
138 "[| F : Increasing f; F: Increasing g |] |
|
139 ==> F : Increasing (%s. (f s) Un (g s))" |
|
140 apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto) |
|
141 apply (drule_tac x = "f xa" in spec) |
|
142 apply (drule_tac x = "g xa" in spec) |
|
143 apply (blast dest!: bspec) |
|
144 done |
|
145 |
|
146 |
|
147 lemma Always_Un: |
|
148 "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] |
|
149 ==> F : Always {s. f' s Un g' s <= f s Un g s}" |
|
150 apply (simp add: Always_eq_includes_reachable, blast) |
|
151 done |
|
152 |
|
153 (*Lemma to re-use the argument that one variable increases (progress) |
|
154 while the other variable doesn't decrease (safety)*) |
|
155 lemma Follows_Un_lemma: |
|
156 "[| F : Increasing f; F : Increasing g; |
|
157 F : Increasing g'; F : Always {s. f' s <= f s}; |
|
158 ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |] |
|
159 ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}" |
|
160 apply (rule single_LeadsTo_I) |
|
161 apply (drule_tac x = "f s" in IncreasingD) |
|
162 apply (drule_tac x = "g s" in IncreasingD) |
|
163 apply (rule LeadsTo_weaken) |
|
164 apply (rule PSP_Stable) |
|
165 apply (erule_tac x = "f s" in spec) |
|
166 apply (erule Stable_Int, assumption) |
|
167 apply blast |
|
168 apply blast |
|
169 done |
|
170 |
|
171 lemma Follows_Un: |
|
172 "[| F : f' Fols f; F: g' Fols g |] |
|
173 ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))" |
|
174 apply (unfold Follows_def) |
|
175 apply (simp add: Increasing_Un Always_Un, auto) |
|
176 apply (rule LeadsTo_Trans) |
|
177 apply (blast intro: Follows_Un_lemma) |
|
178 (*Weakening is used to exchange Un's arguments*) |
|
179 apply (blast intro: Follows_Un_lemma [THEN LeadsTo_weaken]) |
|
180 done |
|
181 |
|
182 |
|
183 (** Multiset union properties (with the multiset ordering) **) |
|
184 |
|
185 lemma increasing_union: |
|
186 "[| F : increasing f; F: increasing g |] |
|
187 ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
|
188 |
|
189 apply (unfold increasing_def stable_def constrains_def, auto) |
|
190 apply (drule_tac x = "f xa" in spec) |
|
191 apply (drule_tac x = "g xa" in spec) |
|
192 apply (drule bspec, assumption) |
|
193 apply (blast intro: union_le_mono order_trans) |
|
194 done |
|
195 |
|
196 lemma Increasing_union: |
|
197 "[| F : Increasing f; F: Increasing g |] |
|
198 ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
|
199 apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto) |
|
200 apply (drule_tac x = "f xa" in spec) |
|
201 apply (drule_tac x = "g xa" in spec) |
|
202 apply (drule bspec, assumption) |
|
203 apply (blast intro: union_le_mono order_trans) |
|
204 done |
|
205 |
|
206 lemma Always_union: |
|
207 "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] |
|
208 ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}" |
|
209 apply (simp add: Always_eq_includes_reachable) |
|
210 apply (blast intro: union_le_mono) |
|
211 done |
|
212 |
|
213 (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*) |
|
214 lemma Follows_union_lemma: |
|
215 "[| F : Increasing f; F : Increasing g; |
|
216 F : Increasing g'; F : Always {s. f' s <= f s}; |
|
217 ALL k::('a::order) multiset. |
|
218 F : {s. k <= f s} LeadsTo {s. k <= f' s} |] |
|
219 ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}" |
|
220 apply (rule single_LeadsTo_I) |
|
221 apply (drule_tac x = "f s" in IncreasingD) |
|
222 apply (drule_tac x = "g s" in IncreasingD) |
|
223 apply (rule LeadsTo_weaken) |
|
224 apply (rule PSP_Stable) |
|
225 apply (erule_tac x = "f s" in spec) |
|
226 apply (erule Stable_Int, assumption) |
|
227 apply blast |
|
228 apply (blast intro: union_le_mono order_trans) |
|
229 done |
|
230 |
|
231 (*The !! is there to influence to effect of permutative rewriting at the end*) |
|
232 lemma Follows_union: |
|
233 "!!g g' ::'b => ('a::order) multiset. |
|
234 [| F : f' Fols f; F: g' Fols g |] |
|
235 ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))" |
|
236 apply (unfold Follows_def) |
|
237 apply (simp add: Increasing_union Always_union, auto) |
|
238 apply (rule LeadsTo_Trans) |
|
239 apply (blast intro: Follows_union_lemma) |
|
240 (*now exchange union's arguments*) |
|
241 apply (simp add: union_commute) |
|
242 apply (blast intro: Follows_union_lemma) |
|
243 done |
|
244 |
|
245 lemma Follows_setsum: |
|
246 "!!f ::['c,'b] => ('a::order) multiset. |
|
247 [| ALL i: I. F : f' i Fols f i; finite I |] |
|
248 ==> F : (%s. \<Sum>i:I. f' i s) Fols (%s. \<Sum>i:I. f i s)" |
|
249 apply (erule rev_mp) |
|
250 apply (erule finite_induct, simp) |
|
251 apply (simp add: Follows_union) |
|
252 done |
|
253 |
|
254 |
|
255 (*Currently UNUSED, but possibly of interest*) |
|
256 lemma Increasing_imp_Stable_pfixGe: |
|
257 "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}" |
|
258 apply (simp add: Increasing_def Stable_def Constrains_def constrains_def) |
|
259 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] |
|
260 prefix_imp_pfixGe) |
|
261 done |
|
262 |
|
263 (*Currently UNUSED, but possibly of interest*) |
|
264 lemma LeadsTo_le_imp_pfixGe: |
|
265 "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} |
|
266 ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}" |
|
267 apply (rule single_LeadsTo_I) |
|
268 apply (drule_tac x = "f s" in spec) |
|
269 apply (erule LeadsTo_weaken) |
|
270 prefer 2 |
|
271 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] |
|
272 prefix_imp_pfixGe, blast) |
|
273 done |
|
274 |
20 end |
275 end |