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