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