(* Title: HOL/HOLCF/Deflation.thy
Author: Brian Huffman
*)
section \<open>Continuous deflations and ep-pairs\<close>
theory Deflation
imports Cfun
begin
default_sort cpo
subsection \<open>Continuous deflations\<close>
locale deflation =
fixes d :: "'a \ 'a"
assumes idem: "\x. d\(d\x) = d\x"
assumes below: "\x. d\x \ x"
begin
lemma below_ID: "d \ ID"
by (rule cfun_belowI) (simp add: below)
text \<open>The set of fixed points is the same as the range.\<close>
lemma fixes_eq_range: "{x. d\x = x} = range (\x. d\x)"
by (auto simp add: eq_sym_conv idem)
lemma range_eq_fixes: "range (\x. d\x) = {x. d\x = x}"
by (auto simp add: eq_sym_conv idem)
text \<open>
The pointwise ordering on deflation functions coincides with
the subset ordering of their sets of fixed-points.
\<close>
lemma belowI:
assumes f: "\x. d\x = x \ f\x = x"
shows "d \ f"
proof (rule cfun_belowI)
fix x
from below have "f\(d\x) \ f\x"
by (rule monofun_cfun_arg)
also from idem have "f\(d\x) = d\x"
by (rule f)
finally show "d\x \ f\x" .
qed
lemma belowD: "\f \ d; f\x = x\ \ d\x = x"
proof (rule below_antisym)
from below show "d\x \ x" .
assume "f \ d"
then have "f\x \ d\x" by (rule monofun_cfun_fun)
also assume "f\x = x"
finally show "x \ d\x" .
qed
end
lemma deflation_strict: "deflation d \ d\\ = \"
by (rule deflation.below [THEN bottomI])
lemma adm_deflation: "adm (\d. deflation d)"
by (simp add: deflation_def)
lemma deflation_ID: "deflation ID"
by (simp add: deflation.intro)
lemma deflation_bottom: "deflation \"
by (simp add: deflation.intro)
lemma deflation_below_iff: "deflation p \ deflation q \ p \ q \ (\x. p\x = x \ q\x = x)"
apply safe
apply (simp add: deflation.belowD)
apply (simp add: deflation.belowI)
done
text \<open>
The composition of two deflations is equal to
the lesser of the two (if they are comparable).
\<close>
lemma deflation_below_comp1:
assumes "deflation f"
assumes "deflation g"
shows "f \ g \ f\(g\x) = f\x"
proof (rule below_antisym)
interpret g: deflation g by fact
from g.below show "f\(g\x) \ f\x" by (rule monofun_cfun_arg)
next
interpret f: deflation f by fact
assume "f \ g"
then have "f\x \ g\x" by (rule monofun_cfun_fun)
then have "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg)
also have "f\(f\x) = f\x" by (rule f.idem)
finally show "f\x \ f\(g\x)" .
qed
lemma deflation_below_comp2: "deflation f \ deflation g \ f \ g \ g\(f\x) = f\x"
by (simp only: deflation.belowD deflation.idem)
subsection \<open>Deflations with finite range\<close>
lemma finite_range_imp_finite_fixes:
assumes "finite (range f)"
shows "finite {x. f x = x}"
proof -
have "{x. f x = x} \ range f"
by (clarify, erule subst, rule rangeI)
from this assms show "finite {x. f x = x}"
by (rule finite_subset)
qed
locale finite_deflation = deflation +
assumes finite_fixes: "finite {x. d\x = x}"
begin
lemma finite_range: "finite (range (\x. d\x))"
by (simp add: range_eq_fixes finite_fixes)
lemma finite_image: "finite ((\x. d\x) ` A)"
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
lemma compact: "compact (d\x)"
proof (rule compactI2)
fix Y :: "nat \ 'a"
assume Y: "chain Y"
have "finite_chain (\i. d\(Y i))"
proof (rule finite_range_imp_finch)
from Y show "chain (\i. d\(Y i))" by simp
have "range (\i. d\(Y i)) \ range (\x. d\x)" by auto
then show "finite (range (\i. d\(Y i)))"
using finite_range by (rule finite_subset)
qed
then have "\j. (\i. d\(Y i)) = d\(Y j)"
by (simp add: finite_chain_def maxinch_is_thelub Y)
then obtain j where j: "(\i. d\(Y i)) = d\(Y j)" ..
assume "d\x \ (\i. Y i)"
then have "d\(d\x) \ d\(\i. Y i)"
by (rule monofun_cfun_arg)
then have "d\x \ (\i. d\(Y i))"
by (simp add: contlub_cfun_arg Y idem)
with j have "d\x \ d\(Y j)" by simp
then have "d\x \ Y j"
using below by (rule below_trans)
then show "\j. d\x \ Y j" ..
qed
end
lemma finite_deflation_intro: "deflation d \ finite {x. d\x = x} \ finite_deflation d"
by (intro finite_deflation.intro finite_deflation_axioms.intro)
lemma finite_deflation_imp_deflation: "finite_deflation d \ deflation d"
by (simp add: finite_deflation_def)
lemma finite_deflation_bottom: "finite_deflation \"
by standard simp_all
subsection \<open>Continuous embedding-projection pairs\<close>
locale ep_pair =
fixes e :: "'a \ 'b" and p :: "'b \ 'a"
assumes e_inverse [simp]: "\x. p\(e\x) = x"
and e_p_below: "\y. e\(p\y) \ y"
begin
lemma e_below_iff [simp]: "e\x \ e\y \ x \ y"
proof
assume "e\x \ e\y"
then have "p\(e\x) \ p\(e\y)" by (rule monofun_cfun_arg)
then show "x \ y" by simp
next
assume "x \ y"
then show "e\x \ e\y" by (rule monofun_cfun_arg)
qed
lemma e_eq_iff [simp]: "e\x = e\y \ x = y"
unfolding po_eq_conv e_below_iff ..
lemma p_eq_iff: "e\(p\x) = x \ e\(p\y) = y \ p\x = p\y \ x = y"
by (safe, erule subst, erule subst, simp)
lemma p_inverse: "(\x. y = e\x) \ e\(p\y) = y"
by (auto, rule exI, erule sym)
lemma e_below_iff_below_p: "e\x \ y \ x \ p\y"
proof
assume "e\x \ y"
then have "p\(e\x) \ p\y" by (rule monofun_cfun_arg)
then show "x \ p\y" by simp
next
assume "x \ p\y"
then have "e\x \ e\(p\y)" by (rule monofun_cfun_arg)
then show "e\x \ y" using e_p_below by (rule below_trans)
qed
lemma compact_e_rev: "compact (e\x) \ compact x"
proof -
assume "compact (e\x)"
then have "adm (\y. e\x \ y)" by (rule compactD)
then have "adm (\y. e\x \ e\y)" by (rule adm_subst [OF cont_Rep_cfun2])
then have "adm (\y. x \ y)" by simp
then show "compact x" by (rule compactI)
qed
lemma compact_e:
assumes "compact x"
shows "compact (e\x)"
proof -
from assms have "adm (\y. x \ y)" by (rule compactD)
then have "adm (\y. x \ p\y)" by (rule adm_subst [OF cont_Rep_cfun2])
then have "adm (\y. e\x \ y)" by (simp add: e_below_iff_below_p)
then show "compact (e\x)" by (rule compactI)
qed
lemma compact_e_iff: "compact (e\x) \ compact x"
by (rule iffI [OF compact_e_rev compact_e])
text \<open>Deflations from ep-pairs\<close>
lemma deflation_e_p: "deflation (e oo p)"
by (simp add: deflation.intro e_p_below)
lemma deflation_e_d_p:
assumes "deflation d"
shows "deflation (e oo d oo p)"
proof
interpret deflation d by fact
fix x :: 'b
show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
by (simp add: idem)
show "(e oo d oo p)\x \ x"
by (simp add: e_below_iff_below_p below)
qed
lemma finite_deflation_e_d_p:
assumes "finite_deflation d"
shows "finite_deflation (e oo d oo p)"
proof
interpret finite_deflation d by fact
fix x :: 'b
show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
by (simp add: idem)
show "(e oo d oo p)\x \ x"
by (simp add: e_below_iff_below_p below)
have "finite ((\x. e\x) ` (\x. d\x) ` range (\x. p\x))"
by (simp add: finite_image)
then have "finite (range (\x. (e oo d oo p)\x))"
by (simp add: image_image)
then show "finite {x. (e oo d oo p)\x = x}"
by (rule finite_range_imp_finite_fixes)
qed
lemma deflation_p_d_e:
assumes "deflation d"
assumes d: "\x. d\x \ e\(p\x)"
shows "deflation (p oo d oo e)"
proof -
interpret d: deflation d by fact
have p_d_e_below: "(p oo d oo e)\x \ x" for x
proof -
have "d\(e\x) \ e\x"
by (rule d.below)
then have "p\(d\(e\x)) \ p\(e\x)"
by (rule monofun_cfun_arg)
then show ?thesis by simp
qed
show ?thesis
proof
show "(p oo d oo e)\x \ x" for x
by (rule p_d_e_below)
show "(p oo d oo e)\((p oo d oo e)\x) = (p oo d oo e)\x" for x
proof (rule below_antisym)
show "(p oo d oo e)\((p oo d oo e)\x) \ (p oo d oo e)\x"
by (rule p_d_e_below)
have "p\(d\(d\(d\(e\x)))) \ p\(d\(e\(p\(d\(e\x)))))"
by (intro monofun_cfun_arg d)
then have "p\(d\(e\x)) \ p\(d\(e\(p\(d\(e\x)))))"
by (simp only: d.idem)
then show "(p oo d oo e)\x \ (p oo d oo e)\((p oo d oo e)\x)"
by simp
qed
qed
qed
lemma finite_deflation_p_d_e:
assumes "finite_deflation d"
assumes d: "\x. d\x \ e\(p\x)"
shows "finite_deflation (p oo d oo e)"
proof -
interpret d: finite_deflation d by fact
show ?thesis
proof (rule finite_deflation_intro)
have "deflation d" ..
then show "deflation (p oo d oo e)"
using d by (rule deflation_p_d_e)
next
have "finite ((\x. d\x) ` range (\x. e\x))"
by (rule d.finite_image)
then have "finite ((\x. p\x) ` (\x. d\x) ` range (\x. e\x))"
by (rule finite_imageI)
then have "finite (range (\x. (p oo d oo e)\x))"
by (simp add: image_image)
then show "finite {x. (p oo d oo e)\x = x}"
by (rule finite_range_imp_finite_fixes)
qed
qed
end
subsection \<open>Uniqueness of ep-pairs\<close>
lemma ep_pair_unique_e_lemma:
assumes 1: "ep_pair e1 p"
and 2: "ep_pair e2 p"
shows "e1 \ e2"
proof (rule cfun_belowI)
fix x
have "e1\(p\(e2\x)) \ e2\x"
by (rule ep_pair.e_p_below [OF 1])
then show "e1\x \ e2\x"
by (simp only: ep_pair.e_inverse [OF 2])
qed
lemma ep_pair_unique_e: "ep_pair e1 p \ ep_pair e2 p \ e1 = e2"
by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
lemma ep_pair_unique_p_lemma:
assumes 1: "ep_pair e p1"
and 2: "ep_pair e p2"
shows "p1 \ p2"
proof (rule cfun_belowI)
fix x
have "e\(p1\x) \ x"
by (rule ep_pair.e_p_below [OF 1])
then have "p2\(e\(p1\x)) \ p2\x"
by (rule monofun_cfun_arg)
then show "p1\x \ p2\x"
by (simp only: ep_pair.e_inverse [OF 2])
qed
lemma ep_pair_unique_p: "ep_pair e p1 \ ep_pair e p2 \ p1 = p2"
by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
subsection \<open>Composing ep-pairs\<close>
lemma ep_pair_ID_ID: "ep_pair ID ID"
by standard simp_all
lemma ep_pair_comp:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
shows "ep_pair (e2 oo e1) (p1 oo p2)"
proof
interpret ep1: ep_pair e1 p1 by fact
interpret ep2: ep_pair e2 p2 by fact
fix x y
show "(p1 oo p2)\((e2 oo e1)\x) = x"
by simp
have "e1\(p1\(p2\y)) \ p2\y"
by (rule ep1.e_p_below)
then have "e2\(e1\(p1\(p2\y))) \ e2\(p2\y)"
by (rule monofun_cfun_arg)
also have "e2\(p2\y) \ y"
by (rule ep2.e_p_below)
finally show "(e2 oo e1)\((p1 oo p2)\y) \ y"
by simp
qed
locale pcpo_ep_pair = ep_pair e p
for e :: "'a::pcpo \ 'b::pcpo"
and p :: "'b::pcpo \ 'a::pcpo"
begin
lemma e_strict [simp]: "e\\ = \"
proof -
have "\ \ p\\" by (rule minimal)
then have "e\\ \ e\(p\\)" by (rule monofun_cfun_arg)
also have "e\(p\\) \ \" by (rule e_p_below)
finally show "e\\ = \" by simp
qed
lemma e_bottom_iff [simp]: "e\x = \ \ x = \"
by (rule e_eq_iff [where y="\", unfolded e_strict])
lemma e_defined: "x \ \ \ e\x \ \"
by simp
lemma p_strict [simp]: "p\\ = \"
by (rule e_inverse [where x="\", unfolded e_strict])
lemmas stricts = e_strict p_strict
end
end
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
