Some cleanup
[funcCF.git] / CFGraph / Finite_Inductive_Set.thy
1 theory Finite_Inductive_Set
2 imports Main
3 begin
4
5 primrec iterate 
6   where it_0: "iterate 0 f x = x"
7       | it_Suc: "iterate (Suc n) f x = f (iterate n f x)"
8
9 definition descending_functional :: "('a \<Rightarrow> nat) \<Rightarrow> ('a set \<Rightarrow> 'a set) \<Rightarrow> bool"
10   where "descending_functional p F = (\<forall> S. \<forall> x \<in> F (F S) - (F S).  \<exists> y \<in> (F S) - S . p x < p y)"
11
12 lemma descending_functionalD:
13   "\<lbrakk> descending_functional p F ; x \<in> F (F S); x \<notin> F S \<rbrakk> \<Longrightarrow> \<exists> y \<in> (F S) - S. p x < p y"
14 unfolding descending_functional_def by auto
15
16 lemma descending_functionalI[intro]:
17   "(\<And>S x. \<lbrakk> x \<in> F (F S);  x \<notin> F S \<rbrakk> \<Longrightarrow> \<exists> y \<in> (F S) - S. p x < p y) \<Longrightarrow> descending_functional p F"
18 unfolding descending_functional_def by auto
19
20 definition finiteness_preserving
21   where "finiteness_preserving  F = (\<forall>S . finite S \<longrightarrow> finite (F S))"
22
23 lemma finiteness_preservingD:
24   "\<lbrakk> finiteness_preserving F ; finite S \<rbrakk> \<Longrightarrow> finite (F S)"
25 unfolding finiteness_preserving_def by auto
26
27 lemma finiteness_preservingI[intro]:
28   "\<lbrakk> \<And> S. finite S \<Longrightarrow> finite (F S) \<rbrakk> \<Longrightarrow> finiteness_preserving F"
29 unfolding finiteness_preserving_def by auto
30
31
32 lemma diff_empty_iff: "A - B = {} \<longleftrightarrow> A \<subseteq> B" by auto
33
34 lemma diff_zero:
35   assumes mono: "mono F"
36      and "iterate (Suc i) F {} - iterate i F {} = {}"
37   shows "iterate (Suc (Suc i)) F {} - iterate (Suc i) F {} = {}"
38 using assms
39 by (auto simp add:diff_empty_iff iterate.simps dest: monoD)
40
41 lemma iteration_stops:
42   assumes mono: "mono F"
43       and finite: "\<And> S. finite S \<Longrightarrow> finite (F S)"
44       and desc: "descending_functional p F"
45   shows "\<exists> i :: nat . F (iterate i F {}) - iterate i F {} = {}"
46 proof-
47   def i0 == "Suc (Max (p ` (F {})))"
48   let "?Diff i" = "iterate (Suc i) F {} - iterate i F {}"
49   
50   from finite have finite_it: "\<And> i. finite (iterate i F {})" by (induct_tac i, auto)
51   have finite_p: "\<And> i. finite (p ` ?Diff i)" by (intro finite_imageI finite_Diff finite_it)
52
53   def i \<equiv> i0
54   have maxbound: "?Diff i \<noteq> {} \<Longrightarrow> Max (p ` ?Diff i) + i < i0"
55   proof(induct i)
56     case 0 show ?case by (auto simp add:i0_def) next
57     case (Suc i)
58       hence ne_p': "p ` ?Diff (Suc i) \<noteq> {}" by auto
59
60       show "?Diff (Suc i) \<noteq> {} \<Longrightarrow> Max (p ` ?Diff (Suc i)) + Suc i < i0"
61       proof(cases "?Diff i = {}")
62       case True 
63         hence "?Diff (Suc i) = {}" by (rule diff_zero[OF mono])
64         moreover assume "?Diff (Suc i) \<noteq> {}"
65         ultimately show  ?thesis by contradiction next
66       case False 
67         hence ne_p: "p ` ?Diff i \<noteq> {}" by simp
68
69         have "Max (p ` ?Diff (Suc i)) < Max (p ` ?Diff i)"
70           apply (subst Max_less_iff[OF finite_p[of "Suc i"] ne_p'])
71           apply (subst Max_gr_iff[OF finite_p[of i] ne_p])
72           by (auto dest: descending_functionalD[OF desc])
73         moreover
74         have "Max (p ` ?Diff i) + i < i0" 
75           using False and Suc(1) by simp
76         ultimately
77         show ?thesis by auto
78       qed
79   qed
80   have "?Diff i0 = {}" using maxbound[unfolded i_def] by auto
81   thus ?thesis by auto
82 qed
83
84 lemma lfp_finite:
85   assumes mono: "mono F"
86       and finite: "finiteness_preserving F"
87       and desc: "descending_functional p F"
88   shows "finite (lfp F)"
89 proof-
90   from iteration_stops[OF mono finiteness_preservingD[OF finite] desc]
91   obtain i where "F (iterate i F {}) - iterate i F {} = {}" by auto
92   hence "F (iterate i F {}) \<subseteq> iterate i F {}" by auto
93   hence "lfp F \<subseteq> iterate i F {}" by(rule lfp_lowerbound)
94   moreover
95   have "finite (iterate i F {})" 
96   apply(induct i) by (auto intro: finiteness_preservingD[OF finite])
97   ultimately
98   show ?thesis by (rule finite_subset)
99 qed
100
101 lemma finite_at_most_one:
102   assumes "\<And> x x'. \<lbrakk> x \<in> S ; x' \<in> S \<rbrakk> \<Longrightarrow> x = x'"
103   shows "finite S"
104 proof(cases "S = {}")
105   case False
106     then obtain x where "x \<in> S" by auto
107     with assms have "S = {x}" by auto
108     thus ?thesis by auto
109 qed auto
110
111 lemma finite_inj_collect:
112   assumes inj: "\<And> x x'. f x = f x' \<Longrightarrow> x = x'"
113     and  fin: "finite S" 
114   shows "finite (\<lambda> x. S (f x))"
115 proof-
116   have "finite (\<Union> z\<in>S. {x. f x = z})"
117     by (auto intro: finite_UN_I[OF fin] finite_at_most_one dest: inj)
118   moreover
119   have "(\<Union> z\<in>S. {x. f x = z}) = {x. f x \<in> S}"
120     by auto
121   ultimately
122   have "finite {x. f x \<in> S}" by auto
123   thus ?thesis unfolding mem_def Collect_def by auto
124 qed
125
126 lemmas finite_inj_collect_lfp (* Help the pattern matcher *)
127  = finite_inj_collect[of _ "lfp F", standard]
128
129 lemma ind_set_finite:
130   assumes defn: "S = lfp F"
131       and mono: "mono F"
132       and finite: "finiteness_preserving F"
133       and desc: "descending_functional p F"
134   shows "finite S"
135 by (subst defn, rule lfp_finite[OF mono finite desc])
136
137 lemma finiteness_preserving_disj:
138   assumes F1: "finiteness_preserving F1"
139       and F2: "finiteness_preserving F2"
140   shows "finiteness_preserving (\<lambda>p x.  F1 p x \<or> F2 p x)"
141 proof 
142   fix S :: "'a set"
143   assume fin: "finite S"
144   from finiteness_preservingD[OF F1 fin] finiteness_preservingD[OF F2 fin]
145   have "finite (F1 S \<union> F2 S)" by auto
146   thus "finite (\<lambda>x. F1 S x \<or> F2 S x)"
147     unfolding Un_def mem_def Collect_def by auto
148 qed
149
150 lemma finiteness_preserving_singleton:
151   "finiteness_preserving (\<lambda>p x. x = y)"
152 proof
153   have "finite {y}" by auto
154   thus "finite (\<lambda>x. x = y)"
155     unfolding insert_def mem_def Collect_def by auto
156 qed
157
158 lemma finiteness_preserving_bex_conj:
159   assumes "finiteness_preserving (\<lambda>p x. \<exists>y. p (f x y))"
160   shows "finiteness_preserving (\<lambda>p x. \<exists>y z. x = z \<and> p (f z y))"
161 using assms by simp
162
163 lemma finiteness_preserving_bex:
164   assumes "\<And> x x' y y'. f x y = f x' y' \<Longrightarrow> x = x'"
165   shows "finiteness_preserving (\<lambda>p x. \<exists>y. p (f x y))"
166 proof
167   fix S :: "'c set"
168   assume fin: "finite S"
169   have "finite (\<Union> z\<in>S. {x. \<exists>y. f x y = z})"
170     by (auto intro: finite_UN_I[OF fin] finite_at_most_one dest: assms)
171   moreover
172   have "(\<Union> z\<in>S. {x. \<exists>y. f x y = z}) = {x. \<exists>y. f x y \<in> S}"
173     by auto
174   ultimately
175   have "finite {x. \<exists>y. f x y \<in> S}" by auto
176   thus "finite (\<lambda>x. \<exists>y. S (f x y))"
177     unfolding mem_def Collect_def by auto
178 qed
179
180 lemma finiteness_preserving_split:
181   assumes "finiteness_preserving (\<lambda>p x. f p (fst x) (snd x))"
182   shows "finiteness_preserving (\<lambda>p (a,b). f p a b)"
183 using assms by (simp add:split_def)
184
185 lemmas finiteness_preserving_lemmas =
186   finiteness_preserving_disj
187   finiteness_preserving_singleton
188   finiteness_preserving_bex
189   finiteness_preserving_bex_conj
190   (* finiteness_preserving_split *)
191
192 text {* Example application *}
193
194 inductive tails for l
195   where "tails l l"
196       | "tails l (x#xs) \<Longrightarrow> tails l xs"
197
198 method_setup mono =
199 "Scan.succeed (K (SIMPLE_METHOD (EVERY [rtac @{thm monoI} 1,
200       REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
201       REPEAT (FIRST
202         [atac 1,
203          resolve_tac (Inductive.get_monos @{context}) 1,
204          etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])))"
205 "Solves monotonicity goals"
206
207 lemma "finite (tails l)"
208 unfolding tails_def
209 proof (induct rule: lfp_finite[of _ size, case_names mono finiteness desc])
210 case mono show ?case by mono
211 next
212 case finiteness show ?case by (intro finiteness_preserving_lemmas, simp)
213 next
214 case desc show ?case
215   by (rule, auto simp add: Bex_def mem_def fun_diff_def bool_diff_def)
216 qed
217
218 text {* Transform a least fixpoint with multiple parameters to one
219  with one paramter, to be able to consider it a set *}
220
221 definition splitF :: "(('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c)) \<Rightarrow> ((('a\<times>'b) \<Rightarrow> 'c) \<Rightarrow> (('a\<times>'b) \<Rightarrow> 'c))"
222   where [simp]:"splitF f = (\<lambda>S. split (f (curry S)))"
223
224 lemma split_mono_iff[simp]:
225   "split S \<le> split S' \<longleftrightarrow> S \<le> S'"
226 proof
227   assume "split S \<le> split S'"
228   show "S \<le> S'"
229   apply (rule le_funI, rule le_funI)
230   proof-
231     fix x y 
232     from le_funD[OF `split S \<le> split S'`, of "(x,y)"]
233     show "S x y \<le> S' x y"
234       by auto
235   qed 
236 qed (auto intro: le_funI dest:le_funD simp add:split_def)
237
238 lemma split_mono: "mono split" by (rule monoI, auto)
239
240 lemma curry_mono_iff[simp]:
241   "curry S \<le> curry S' \<longleftrightarrow> S \<le> S'"
242 apply (subst (3 4) split_curry[THEN sym])
243 apply (subst split_mono_iff)
244 apply (rule refl)
245 done
246
247 lemma curry_mono: "mono curry" by (rule monoI, auto)
248
249 lemma splitF_mono:
250   assumes "mono f" shows "mono (splitF f)"
251 unfolding splitF_def
252 by(intro monoI monoD[OF split_mono] monoD[OF assms] monoD[OF curry_mono])
253
254 lemma lfp_curry':
255   assumes mono: "mono f"
256   shows  "lfp(\<lambda> p x y. f p x y) = curry (lfp (splitF f))" (is "?lhs = ?rhs")
257 proof(rule antisym)
258   show "lfp f \<le> curry (lfp (splitF f))"
259   proof (rule lfp_lowerbound)
260     have "f (curry (lfp (splitF f))) = curry (split (f (curry (lfp (splitF f)))))" by simp
261     also
262     have "\<dots> = curry (splitF f (lfp (splitF f)))" by simp
263     also
264     have "\<dots> = curry (lfp (splitF f))"
265       by (subst lfp_unfold[OF splitF_mono[OF mono], THEN sym], rule refl)
266     finally
267     show "f (curry (lfp (splitF f))) \<le> curry (lfp (splitF f))" by simp
268   qed
269
270   have "lfp (splitF f) \<le> split (lfp f)"
271   proof (rule lfp_lowerbound)
272     have "splitF f (split (lfp f)) = split (f (lfp f))" by simp
273     also
274     have "\<dots> = split (lfp f)"
275       by (subst lfp_unfold[OF mono, THEN sym], rule refl)
276     finally
277     show "splitF f (split (lfp f)) \<le> split (lfp f)" by simp
278   qed
279   hence "curry (lfp (splitF f)) \<le> curry (split (lfp f))"
280     by (rule monoD[OF curry_mono])
281   thus "curry (lfp (splitF f)) \<le> lfp f" by simp
282 qed
283
284 lemmas lfp_curry = lfp_curry'[simplified splitF_def curry_def]
285
286 lemma lfp_curryD':
287   assumes mono: "mono f"
288   and curried: "mono (splitF f) \<Longrightarrow> P (curry (lfp (splitF f)))"
289   shows  "P (lfp f)"
290 by (subst lfp_curry'[OF mono], rule curried[OF splitF_mono[OF mono]])
291
292 lemmas lfp_curryD = lfp_curryD'[simplified splitF_def curry_def split_def]
293
294 text {* Now lets try this for a recursively defined functorial *}
295
296 inductive tails' and elems' for l
297   where "tails' l l"
298       | "tails' l (x#xs) \<Longrightarrow> tails' l xs"
299       | "tails' l (x#xs) \<Longrightarrow> elems' l x"
300
301 lemma "finite (tails' l)"
302 unfolding tails'_def
303 unfolding tails'_elems'_def
304 apply (rule lfp_curryD[of _ "\<lambda>l. finite (l False undefined)"])
305 apply mono
306 apply (erule lfp_curryD)
307 apply (rule finite_inj_collect_lfp)
308 apply auto[1]
309 apply (erule lfp_finite[of _ size])
310 apply (intro finiteness_preserving_lemmas)
311
312 oops
313
314 end