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