huffman@39999: (* Title: HOLCF/Library/Defl_Bifinite.thy
huffman@39999: Author: Brian Huffman
huffman@39999: *)
huffman@39999:
huffman@39999: header {* Algebraic deflations are a bifinite domain *}
huffman@39999:
huffman@39999: theory Defl_Bifinite
huffman@39999: imports HOLCF Infinite_Set
huffman@39999: begin
huffman@39999:
huffman@39999: subsection {* Lemmas about MOST *}
huffman@39999:
huffman@39999: default_sort type
huffman@39999:
huffman@39999: lemma MOST_INFM:
huffman@39999: assumes inf: "infinite (UNIV::'a set)"
huffman@39999: shows "MOST x::'a. P x \ INFM x::'a. P x"
huffman@39999: unfolding Alm_all_def Inf_many_def
huffman@39999: apply (auto simp add: Collect_neg_eq)
huffman@39999: apply (drule (1) finite_UnI)
huffman@39999: apply (simp add: Compl_partition2 inf)
huffman@39999: done
huffman@39999:
huffman@39999: lemma MOST_SucI: "MOST n. P n \ MOST n. P (Suc n)"
huffman@39999: by (rule MOST_inj [OF _ inj_Suc])
huffman@39999:
huffman@39999: lemma MOST_SucD: "MOST n. P (Suc n) \ MOST n. P n"
huffman@39999: unfolding MOST_nat
huffman@39999: apply (clarify, rule_tac x="Suc m" in exI, clarify)
huffman@39999: apply (erule Suc_lessE, simp)
huffman@39999: done
huffman@39999:
huffman@39999: lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \ (MOST n. P n)"
huffman@39999: by (rule iffI [OF MOST_SucD MOST_SucI])
huffman@39999:
huffman@39999: lemma INFM_finite_Bex_distrib:
huffman@39999: "finite A \ (INFM y. \x\A. P x y) \ (\x\A. INFM y. P x y)"
huffman@39999: by (induct set: finite, simp, simp add: INFM_disj_distrib)
huffman@39999:
huffman@39999: lemma MOST_finite_Ball_distrib:
huffman@39999: "finite A \ (MOST y. \x\A. P x y) \ (\x\A. MOST y. P x y)"
huffman@39999: by (induct set: finite, simp, simp add: MOST_conj_distrib)
huffman@39999:
huffman@39999: lemma MOST_ge_nat: "MOST n::nat. m \ n"
huffman@39999: unfolding MOST_nat_le by fast
huffman@39999:
huffman@39999: subsection {* Eventually constant sequences *}
huffman@39999:
huffman@39999: definition
huffman@39999: eventually_constant :: "(nat \ 'a) \ bool"
huffman@39999: where
huffman@39999: "eventually_constant S = (\x. MOST i. S i = x)"
huffman@39999:
huffman@39999: lemma eventually_constant_MOST_MOST:
huffman@39999: "eventually_constant S \ (MOST m. MOST n. S n = S m)"
huffman@39999: unfolding eventually_constant_def MOST_nat
huffman@39999: apply safe
huffman@39999: apply (rule_tac x=m in exI, clarify)
huffman@39999: apply (rule_tac x=m in exI, clarify)
huffman@39999: apply simp
huffman@39999: apply fast
huffman@39999: done
huffman@39999:
huffman@39999: lemma eventually_constantI: "MOST i. S i = x \ eventually_constant S"
huffman@39999: unfolding eventually_constant_def by fast
huffman@39999:
huffman@39999: lemma eventually_constant_comp:
huffman@39999: "eventually_constant (\i. S i) \ eventually_constant (\i. f (S i))"
huffman@39999: unfolding eventually_constant_def
huffman@39999: apply (erule exE, rule_tac x="f x" in exI)
huffman@39999: apply (erule MOST_mono, simp)
huffman@39999: done
huffman@39999:
huffman@39999: lemma eventually_constant_Suc_iff:
huffman@39999: "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)"
huffman@39999: unfolding eventually_constant_def
huffman@39999: by (subst MOST_Suc_iff, rule refl)
huffman@39999:
huffman@39999: lemma eventually_constant_SucD:
huffman@39999: "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)"
huffman@39999: by (rule eventually_constant_Suc_iff [THEN iffD1])
huffman@39999:
huffman@39999: subsection {* Limits of eventually constant sequences *}
huffman@39999:
huffman@39999: definition
huffman@39999: eventual :: "(nat \ 'a) \ 'a" where
huffman@39999: "eventual S = (THE x. MOST i. S i = x)"
huffman@39999:
huffman@39999: lemma eventual_eqI: "MOST i. S i = x \ eventual S = x"
huffman@39999: unfolding eventual_def
huffman@39999: apply (rule the_equality, assumption)
huffman@39999: apply (rename_tac y)
huffman@39999: apply (subgoal_tac "MOST i::nat. y = x", simp)
huffman@39999: apply (erule MOST_rev_mp)
huffman@39999: apply (erule MOST_rev_mp)
huffman@39999: apply simp
huffman@39999: done
huffman@39999:
huffman@39999: lemma MOST_eq_eventual:
huffman@39999: "eventually_constant S \ MOST i. S i = eventual S"
huffman@39999: unfolding eventually_constant_def
huffman@39999: by (erule exE, simp add: eventual_eqI)
huffman@39999:
huffman@39999: lemma eventual_mem_range:
huffman@39999: "eventually_constant S \ eventual S \ range S"
huffman@39999: apply (drule MOST_eq_eventual)
huffman@39999: apply (simp only: MOST_nat_le, clarify)
huffman@39999: apply (drule spec, drule mp, rule order_refl)
huffman@39999: apply (erule range_eqI [OF sym])
huffman@39999: done
huffman@39999:
huffman@39999: lemma eventually_constant_MOST_iff:
huffman@39999: assumes S: "eventually_constant S"
huffman@39999: shows "(MOST n. P (S n)) \ P (eventual S)"
huffman@39999: apply (subgoal_tac "(MOST n. P (S n)) \ (MOST n::nat. P (eventual S))")
huffman@39999: apply simp
huffman@39999: apply (rule iffI)
huffman@39999: apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@39999: apply (erule MOST_mono, force)
huffman@39999: apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]])
huffman@39999: apply (erule MOST_mono, simp)
huffman@39999: done
huffman@39999:
huffman@39999: lemma MOST_eventual:
huffman@39999: "\eventually_constant S; MOST n. P (S n)\ \ P (eventual S)"
huffman@39999: proof -
huffman@39999: assume "eventually_constant S"
huffman@39999: hence "MOST n. S n = eventual S"
huffman@39999: by (rule MOST_eq_eventual)
huffman@39999: moreover assume "MOST n. P (S n)"
huffman@39999: ultimately have "MOST n. S n = eventual S \ P (S n)"
huffman@39999: by (rule MOST_conj_distrib [THEN iffD2, OF conjI])
huffman@39999: hence "MOST n::nat. P (eventual S)"
huffman@39999: by (rule MOST_mono) auto
huffman@39999: thus ?thesis by simp
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventually_constant_MOST_Suc_eq:
huffman@39999: "eventually_constant S \ MOST n. S (Suc n) = S n"
huffman@39999: apply (drule MOST_eq_eventual)
huffman@39999: apply (frule MOST_Suc_iff [THEN iffD2])
huffman@39999: apply (erule MOST_rev_mp)
huffman@39999: apply (erule MOST_rev_mp)
huffman@39999: apply simp
huffman@39999: done
huffman@39999:
huffman@39999: lemma eventual_comp:
huffman@39999: "eventually_constant S \ eventual (\i. f (S i)) = f (eventual (\i. S i))"
huffman@39999: apply (rule eventual_eqI)
huffman@39999: apply (rule MOST_mono)
huffman@39999: apply (erule MOST_eq_eventual)
huffman@39999: apply simp
huffman@39999: done
huffman@39999:
huffman@39999: subsection {* Constructing finite deflations by iteration *}
huffman@39999:
huffman@39999: default_sort cpo
huffman@39999:
huffman@39999: lemma le_Suc_induct:
huffman@39999: assumes le: "i \ j"
huffman@39999: assumes step: "\i. P i (Suc i)"
huffman@39999: assumes refl: "\i. P i i"
huffman@39999: assumes trans: "\i j k. \P i j; P j k\ \ P i k"
huffman@39999: shows "P i j"
huffman@39999: proof (cases "i = j")
huffman@39999: assume "i = j"
huffman@39999: thus "P i j" by (simp add: refl)
huffman@39999: next
huffman@39999: assume "i \ j"
huffman@39999: with le have "i < j" by simp
huffman@39999: thus "P i j" using step trans by (rule less_Suc_induct)
huffman@39999: qed
huffman@39999:
huffman@39999: definition
huffman@39999: eventual_iterate :: "('a \ 'a::cpo) \ ('a \ 'a)"
huffman@39999: where
huffman@39999: "eventual_iterate f = eventual (\n. iterate n\f)"
huffman@39999:
huffman@39999: text {* A pre-deflation is like a deflation, but not idempotent. *}
huffman@39999:
huffman@39999: locale pre_deflation =
huffman@39999: fixes f :: "'a \ 'a::cpo"
huffman@39999: assumes below: "\x. f\x \ x"
huffman@39999: assumes finite_range: "finite (range (\x. f\x))"
huffman@39999: begin
huffman@39999:
huffman@39999: lemma iterate_below: "iterate i\f\x \ x"
huffman@39999: by (induct i, simp_all add: below_trans [OF below])
huffman@39999:
huffman@39999: lemma iterate_fixed: "f\x = x \ iterate i\f\x = x"
huffman@39999: by (induct i, simp_all)
huffman@39999:
huffman@39999: lemma antichain_iterate_app: "i \ j \ iterate j\f\x \ iterate i\f\x"
huffman@39999: apply (erule le_Suc_induct)
huffman@39999: apply (simp add: below)
huffman@39999: apply (rule below_refl)
huffman@39999: apply (erule (1) below_trans)
huffman@39999: done
huffman@39999:
huffman@39999: lemma finite_range_iterate_app: "finite (range (\i. iterate i\f\x))"
huffman@39999: proof (rule finite_subset)
huffman@39999: show "range (\i. iterate i\f\x) \ insert x (range (\x. f\x))"
huffman@39999: by (clarify, case_tac i, simp_all)
huffman@39999: show "finite (insert x (range (\x. f\x)))"
huffman@39999: by (simp add: finite_range)
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventually_constant_iterate_app:
huffman@39999: "eventually_constant (\i. iterate i\f\x)"
huffman@39999: unfolding eventually_constant_def MOST_nat_le
huffman@39999: proof -
huffman@39999: let ?Y = "\i. iterate i\f\x"
huffman@39999: have "\j. \k. ?Y j \ ?Y k"
huffman@39999: apply (rule finite_range_has_max)
huffman@39999: apply (erule antichain_iterate_app)
huffman@39999: apply (rule finite_range_iterate_app)
huffman@39999: done
huffman@39999: then obtain j where j: "\k. ?Y j \ ?Y k" by fast
huffman@39999: show "\z m. \n\m. ?Y n = z"
huffman@39999: proof (intro exI allI impI)
huffman@39999: fix k
huffman@39999: assume "j \ k"
huffman@39999: hence "?Y k \ ?Y j" by (rule antichain_iterate_app)
huffman@39999: also have "?Y j \ ?Y k" by (rule j)
huffman@39999: finally show "?Y k = ?Y j" .
huffman@39999: qed
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventually_constant_iterate:
huffman@39999: "eventually_constant (\n. iterate n\f)"
huffman@39999: proof -
huffman@39999: have "\y\range (\x. f\x). eventually_constant (\i. iterate i\f\y)"
huffman@39999: by (simp add: eventually_constant_iterate_app)
huffman@39999: hence "\y\range (\x. f\x). MOST i. MOST j. iterate j\f\y = iterate i\f\y"
huffman@39999: unfolding eventually_constant_MOST_MOST .
huffman@39999: hence "MOST i. MOST j. \y\range (\x. f\x). iterate j\f\y = iterate i\f\y"
huffman@39999: by (simp only: MOST_finite_Ball_distrib [OF finite_range])
huffman@39999: hence "MOST i. MOST j. \x. iterate j\f\(f\x) = iterate i\f\(f\x)"
huffman@39999: by simp
huffman@39999: hence "MOST i. MOST j. \x. iterate (Suc j)\f\x = iterate (Suc i)\f\x"
huffman@39999: by (simp only: iterate_Suc2)
huffman@39999: hence "MOST i. MOST j. iterate (Suc j)\f = iterate (Suc i)\f"
huffman@40002: by (simp only: cfun_eq_iff)
huffman@39999: hence "eventually_constant (\i. iterate (Suc i)\f)"
huffman@39999: unfolding eventually_constant_MOST_MOST .
huffman@39999: thus "eventually_constant (\i. iterate i\f)"
huffman@39999: by (rule eventually_constant_SucD)
huffman@39999: qed
huffman@39999:
huffman@39999: abbreviation
huffman@39999: d :: "'a \ 'a"
huffman@39999: where
huffman@39999: "d \ eventual_iterate f"
huffman@39999:
huffman@39999: lemma MOST_d: "MOST n. P (iterate n\f) \ P d"
huffman@39999: unfolding eventual_iterate_def
huffman@39999: using eventually_constant_iterate by (rule MOST_eventual)
huffman@39999:
huffman@39999: lemma f_d: "f\(d\x) = d\x"
huffman@39999: apply (rule MOST_d)
huffman@39999: apply (subst iterate_Suc [symmetric])
huffman@39999: apply (rule eventually_constant_MOST_Suc_eq)
huffman@39999: apply (rule eventually_constant_iterate_app)
huffman@39999: done
huffman@39999:
huffman@39999: lemma d_fixed_iff: "d\x = x \ f\x = x"
huffman@39999: proof
huffman@39999: assume "d\x = x"
huffman@39999: with f_d [where x=x]
huffman@39999: show "f\x = x" by simp
huffman@39999: next
huffman@39999: assume f: "f\x = x"
huffman@39999: have "\n. iterate n\f\x = x"
huffman@39999: by (rule allI, rule nat.induct, simp, simp add: f)
huffman@39999: hence "MOST n. iterate n\f\x = x"
huffman@39999: by (rule ALL_MOST)
huffman@39999: thus "d\x = x"
huffman@39999: by (rule MOST_d)
huffman@39999: qed
huffman@39999:
huffman@39999: lemma finite_deflation_d: "finite_deflation d"
huffman@39999: proof
huffman@39999: fix x :: 'a
huffman@39999: have "d \ range (\n. iterate n\f)"
huffman@39999: unfolding eventual_iterate_def
huffman@39999: using eventually_constant_iterate
huffman@39999: by (rule eventual_mem_range)
huffman@39999: then obtain n where n: "d = iterate n\f" ..
huffman@39999: have "iterate n\f\(d\x) = d\x"
huffman@39999: using f_d by (rule iterate_fixed)
huffman@39999: thus "d\(d\x) = d\x"
huffman@39999: by (simp add: n)
huffman@39999: next
huffman@39999: fix x :: 'a
huffman@39999: show "d\x \ x"
huffman@39999: by (rule MOST_d, simp add: iterate_below)
huffman@39999: next
huffman@39999: from finite_range
huffman@39999: have "finite {x. f\x = x}"
huffman@39999: by (rule finite_range_imp_finite_fixes)
huffman@39999: thus "finite {x. d\x = x}"
huffman@39999: by (simp add: d_fixed_iff)
huffman@39999: qed
huffman@39999:
huffman@39999: lemma deflation_d: "deflation d"
huffman@39999: using finite_deflation_d
huffman@39999: by (rule finite_deflation_imp_deflation)
huffman@39999:
huffman@39999: end
huffman@39999:
huffman@39999: lemma finite_deflation_eventual_iterate:
huffman@39999: "pre_deflation d \ finite_deflation (eventual_iterate d)"
huffman@39999: by (rule pre_deflation.finite_deflation_d)
huffman@39999:
huffman@39999: lemma pre_deflation_oo:
huffman@39999: assumes "finite_deflation d"
huffman@39999: assumes f: "\x. f\x \ x"
huffman@39999: shows "pre_deflation (d oo f)"
huffman@39999: proof
huffman@39999: interpret d: finite_deflation d by fact
huffman@39999: fix x
huffman@39999: show "\x. (d oo f)\x \ x"
huffman@39999: by (simp, rule below_trans [OF d.below f])
huffman@39999: show "finite (range (\x. (d oo f)\x))"
huffman@39999: by (rule finite_subset [OF _ d.finite_range], auto)
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventual_iterate_oo_fixed_iff:
huffman@39999: assumes "finite_deflation d"
huffman@39999: assumes f: "\x. f\x \ x"
huffman@39999: shows "eventual_iterate (d oo f)\x = x \ d\x = x \ f\x = x"
huffman@39999: proof -
huffman@39999: interpret d: finite_deflation d by fact
huffman@39999: let ?e = "d oo f"
huffman@39999: interpret e: pre_deflation "d oo f"
huffman@39999: using `finite_deflation d` f
huffman@39999: by (rule pre_deflation_oo)
huffman@39999: let ?g = "eventual (\n. iterate n\?e)"
huffman@39999: show ?thesis
huffman@39999: apply (subst e.d_fixed_iff)
huffman@39999: apply simp
huffman@39999: apply safe
huffman@39999: apply (erule subst)
huffman@39999: apply (rule d.idem)
huffman@39999: apply (rule below_antisym)
huffman@39999: apply (rule f)
huffman@39999: apply (erule subst, rule d.below)
huffman@39999: apply simp
huffman@39999: done
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventual_mono:
huffman@39999: assumes A: "eventually_constant A"
huffman@39999: assumes B: "eventually_constant B"
huffman@39999: assumes below: "\n. A n \ B n"
huffman@39999: shows "eventual A \ eventual B"
huffman@39999: proof -
huffman@39999: from A have "MOST n. A n = eventual A"
huffman@39999: by (rule MOST_eq_eventual)
huffman@39999: then have "MOST n. eventual A \ B n"
huffman@39999: by (rule MOST_mono) (erule subst, rule below)
huffman@39999: with B show "eventual A \ eventual B"
huffman@39999: by (rule MOST_eventual)
huffman@39999: qed
huffman@39999:
huffman@39999: lemma eventual_iterate_mono:
huffman@39999: assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \ g"
huffman@39999: shows "eventual_iterate f \ eventual_iterate g"
huffman@39999: unfolding eventual_iterate_def
huffman@39999: apply (rule eventual_mono)
huffman@39999: apply (rule pre_deflation.eventually_constant_iterate [OF f])
huffman@39999: apply (rule pre_deflation.eventually_constant_iterate [OF g])
huffman@39999: apply (rule monofun_cfun_arg [OF `f \ g`])
huffman@39999: done
huffman@39999:
huffman@39999: lemma cont2cont_eventual_iterate_oo:
huffman@39999: assumes d: "finite_deflation d"
huffman@39999: assumes cont: "cont f" and below: "\x y. f x\y \ y"
huffman@39999: shows "cont (\x. eventual_iterate (d oo f x))"
huffman@39999: (is "cont ?e")
huffman@39999: proof (rule contI2)
huffman@39999: show "monofun ?e"
huffman@39999: apply (rule monofunI)
huffman@39999: apply (rule eventual_iterate_mono)
huffman@39999: apply (rule pre_deflation_oo [OF d below])
huffman@39999: apply (rule pre_deflation_oo [OF d below])
huffman@39999: apply (rule monofun_cfun_arg)
huffman@39999: apply (erule cont2monofunE [OF cont])
huffman@39999: done
huffman@39999: next
huffman@39999: fix Y :: "nat \ 'b"
huffman@39999: assume Y: "chain Y"
huffman@39999: with cont have fY: "chain (\i. f (Y i))"
huffman@39999: by (rule ch2ch_cont)
huffman@39999: assume eY: "chain (\i. ?e (Y i))"
huffman@39999: have lub_below: "\x. f (\i. Y i)\x \ x"
huffman@39999: by (rule admD [OF _ Y], simp add: cont, rule below)
huffman@39999: have "deflation (?e (\i. Y i))"
huffman@39999: apply (rule pre_deflation.deflation_d)
huffman@39999: apply (rule pre_deflation_oo [OF d lub_below])
huffman@39999: done
huffman@39999: then show "?e (\i. Y i) \ (\i. ?e (Y i))"
huffman@39999: proof (rule deflation.belowI)
huffman@39999: fix x :: 'a
huffman@39999: assume "?e (\i. Y i)\x = x"
huffman@39999: hence "d\x = x" and "f (\i. Y i)\x = x"
huffman@39999: by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
huffman@39999: hence "(\i. f (Y i)\x) = x"
huffman@39999: apply (simp only: cont2contlubE [OF cont Y])
huffman@39999: apply (simp only: contlub_cfun_fun [OF fY])
huffman@39999: done
huffman@39999: have "compact (d\x)"
huffman@39999: using d by (rule finite_deflation.compact)
huffman@39999: then have "compact x"
huffman@39999: using `d\x = x` by simp
huffman@39999: then have "compact (\i. f (Y i)\x)"
huffman@39999: using `(\i. f (Y i)\x) = x` by simp
huffman@39999: then have "\n. max_in_chain n (\i. f (Y i)\x)"
huffman@39999: by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
huffman@39999: then obtain n where n: "max_in_chain n (\i. f (Y i)\x)" ..
huffman@39999: then have "f (Y n)\x = x"
huffman@39999: using `(\i. f (Y i)\x) = x` fY by (simp add: maxinch_is_thelub)
huffman@39999: with `d\x = x` have "?e (Y n)\x = x"
huffman@39999: by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
huffman@39999: moreover have "?e (Y n)\x \ (\i. ?e (Y i)\x)"
huffman@39999: by (rule is_ub_thelub, simp add: eY)
huffman@39999: ultimately have "x \ (\