1 theory Finite_Inductive_Set
6 where it_0: "iterate 0 f x = x"
7 | it_Suc: "iterate (Suc n) f x = f (iterate n f x)"
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)"
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
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
20 definition finiteness_preserving
21 where "finiteness_preserving F = (\<forall>S . finite S \<longrightarrow> finite (F S))"
23 lemma finiteness_preservingD:
24 "\<lbrakk> finiteness_preserving F ; finite S \<rbrakk> \<Longrightarrow> finite (F S)"
25 unfolding finiteness_preserving_def by auto
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
32 lemma diff_empty_iff: "A - B = {} \<longleftrightarrow> A \<subseteq> B" by auto
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 {} = {}"
39 by (auto simp add:diff_empty_iff iterate.simps dest: monoD)
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 {} = {}"
47 def i0 == "Suc (Max (p ` (F {})))"
48 let "?Diff i" = "iterate (Suc i) F {} - iterate i F {}"
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)
54 have maxbound: "?Diff i \<noteq> {} \<Longrightarrow> Max (p ` ?Diff i) + i < i0"
56 case 0 show ?case by (auto simp add:i0_def) next
58 hence ne_p': "p ` ?Diff (Suc i) \<noteq> {}" by auto
60 show "?Diff (Suc i) \<noteq> {} \<Longrightarrow> Max (p ` ?Diff (Suc i)) + Suc i < i0"
61 proof(cases "?Diff i = {}")
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
67 hence ne_p: "p ` ?Diff i \<noteq> {}" by simp
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])
74 have "Max (p ` ?Diff i) + i < i0"
75 using False and Suc(1) by simp
80 have "?Diff i0 = {}" using maxbound[unfolded i_def] by auto
85 assumes mono: "mono F"
86 and finite: "finiteness_preserving F"
87 and desc: "descending_functional p F"
88 shows "finite (lfp F)"
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)
95 have "finite (iterate i F {})"
96 apply(induct i) by (auto intro: finiteness_preservingD[OF finite])
98 show ?thesis by (rule finite_subset)
101 lemma finite_at_most_one:
102 assumes "\<And> x x'. \<lbrakk> x \<in> S ; x' \<in> S \<rbrakk> \<Longrightarrow> x = x'"
104 proof(cases "S = {}")
106 then obtain x where "x \<in> S" by auto
107 with assms have "S = {x}" by auto
111 lemma finite_inj_collect:
112 assumes inj: "\<And> x x'. f x = f x' \<Longrightarrow> x = x'"
114 shows "finite (\<lambda> x. S (f x))"
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)
119 have "(\<Union> z\<in>S. {x. f x = z}) = {x. f x \<in> S}"
122 have "finite {x. f x \<in> S}" by auto
123 thus ?thesis unfolding mem_def Collect_def by auto
126 lemmas finite_inj_collect_lfp (* Help the pattern matcher *)
127 = finite_inj_collect[of _ "lfp F", standard]
129 lemma ind_set_finite:
130 assumes defn: "S = lfp F"
132 and finite: "finiteness_preserving F"
133 and desc: "descending_functional p F"
135 by (subst defn, rule lfp_finite[OF mono finite desc])
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)"
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
150 lemma finiteness_preserving_singleton:
151 "finiteness_preserving (\<lambda>p x. x = y)"
153 have "finite {y}" by auto
154 thus "finite (\<lambda>x. x = y)"
155 unfolding insert_def mem_def Collect_def by auto
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))"
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))"
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)
172 have "(\<Union> z\<in>S. {x. \<exists>y. f x y = z}) = {x. \<exists>y. f x y \<in> S}"
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
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)
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 *)
192 text {* Example application *}
194 inductive tails for l
196 | "tails l (x#xs) \<Longrightarrow> tails l xs"
199 "Scan.succeed (K (SIMPLE_METHOD (EVERY [rtac @{thm monoI} 1,
200 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
203 resolve_tac (Inductive.get_monos @{context}) 1,
204 etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])))"
205 "Solves monotonicity goals"
207 lemma "finite (tails l)"
209 proof (induct rule: lfp_finite[of _ size, case_names mono finiteness desc])
210 case mono show ?case by mono
212 case finiteness show ?case by (intro finiteness_preserving_lemmas, simp)
215 by (rule, auto simp add: Bex_def mem_def fun_diff_def bool_diff_def)
218 text {* Transform a least fixpoint with multiple parameters to one
219 with one paramter, to be able to consider it a set *}
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)))"
224 lemma split_mono_iff[simp]:
225 "split S \<le> split S' \<longleftrightarrow> S \<le> S'"
227 assume "split S \<le> split S'"
229 apply (rule le_funI, rule le_funI)
232 from le_funD[OF `split S \<le> split S'`, of "(x,y)"]
233 show "S x y \<le> S' x y"
236 qed (auto intro: le_funI dest:le_funD simp add:split_def)
238 lemma split_mono: "mono split" by (rule monoI, auto)
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)
247 lemma curry_mono: "mono curry" by (rule monoI, auto)
250 assumes "mono f" shows "mono (splitF f)"
252 by(intro monoI monoD[OF split_mono] monoD[OF assms] monoD[OF curry_mono])
255 assumes mono: "mono f"
256 shows "lfp(\<lambda> p x y. f p x y) = curry (lfp (splitF f))" (is "?lhs = ?rhs")
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
262 have "\<dots> = curry (splitF f (lfp (splitF f)))" by simp
264 have "\<dots> = curry (lfp (splitF f))"
265 by (subst lfp_unfold[OF splitF_mono[OF mono], THEN sym], rule refl)
267 show "f (curry (lfp (splitF f))) \<le> curry (lfp (splitF f))" by simp
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
274 have "\<dots> = split (lfp f)"
275 by (subst lfp_unfold[OF mono, THEN sym], rule refl)
277 show "splitF f (split (lfp f)) \<le> split (lfp f)" by simp
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
284 lemmas lfp_curry = lfp_curry'[simplified splitF_def curry_def]
287 assumes mono: "mono f"
288 and curried: "mono (splitF f) \<Longrightarrow> P (curry (lfp (splitF f)))"
290 by (subst lfp_curry'[OF mono], rule curried[OF splitF_mono[OF mono]])
292 lemmas lfp_curryD = lfp_curryD'[simplified splitF_def curry_def split_def]
294 text {* Now lets try this for a recursively defined functorial *}
296 inductive tails' and elems' for l
298 | "tails' l (x#xs) \<Longrightarrow> tails' l xs"
299 | "tails' l (x#xs) \<Longrightarrow> elems' l x"
301 lemma "finite (tails' l)"
303 unfolding tails'_elems'_def
304 apply (rule lfp_curryD[of _ "\<lambda>l. finite (l False undefined)"])
306 apply (erule lfp_curryD)
307 apply (rule finite_inj_collect_lfp)
309 apply (erule lfp_finite[of _ size])
310 apply (intro finiteness_preserving_lemmas)