wenzelm@42151: (* Title: HOL/HOLCF/Deflation.thy
huffman@27401: Author: Brian Huffman
huffman@27401: *)
huffman@27401:
huffman@35901: header {* Continuous deflations and ep-pairs *}
huffman@27401:
huffman@27401: theory Deflation
huffman@40502: imports Plain_HOLCF
huffman@27401: begin
huffman@27401:
wenzelm@36452: default_sort cpo
huffman@27401:
huffman@27401: subsection {* Continuous deflations *}
huffman@27401:
huffman@27401: locale deflation =
huffman@27401: fixes d :: "'a \ 'a"
huffman@27401: assumes idem: "\x. d\(d\x) = d\x"
huffman@31076: assumes below: "\x. d\x \ x"
huffman@27401: begin
huffman@27401:
huffman@31076: lemma below_ID: "d \ ID"
huffman@40002: by (rule cfun_belowI, simp add: below)
huffman@27401:
huffman@27401: text {* The set of fixed points is the same as the range. *}
huffman@27401:
huffman@27401: lemma fixes_eq_range: "{x. d\x = x} = range (\x. d\x)"
huffman@27401: by (auto simp add: eq_sym_conv idem)
huffman@27401:
huffman@27401: lemma range_eq_fixes: "range (\x. d\x) = {x. d\x = x}"
huffman@27401: by (auto simp add: eq_sym_conv idem)
huffman@27401:
huffman@27401: text {*
huffman@27401: The pointwise ordering on deflation functions coincides with
huffman@27401: the subset ordering of their sets of fixed-points.
huffman@27401: *}
huffman@27401:
huffman@31076: lemma belowI:
huffman@27401: assumes f: "\x. d\x = x \ f\x = x" shows "d \ f"
huffman@40002: proof (rule cfun_belowI)
huffman@27401: fix x
huffman@31076: from below have "f\(d\x) \ f\x" by (rule monofun_cfun_arg)
huffman@27401: also from idem have "f\(d\x) = d\x" by (rule f)
huffman@27401: finally show "d\x \ f\x" .
huffman@27401: qed
huffman@27401:
huffman@31076: lemma belowD: "\f \ d; f\x = x\ \ d\x = x"
huffman@31076: proof (rule below_antisym)
huffman@31076: from below show "d\x \ x" .
huffman@27401: next
huffman@27401: assume "f \ d"
huffman@27401: hence "f\x \ d\x" by (rule monofun_cfun_fun)
huffman@27401: also assume "f\x = x"
huffman@27401: finally show "x \ d\x" .
huffman@27401: qed
huffman@27401:
huffman@27401: end
huffman@27401:
huffman@33503: lemma deflation_strict: "deflation d \ d\\ = \"
huffman@41430: by (rule deflation.below [THEN bottomI])
huffman@33503:
huffman@27401: lemma adm_deflation: "adm (\d. deflation d)"
huffman@27401: by (simp add: deflation_def)
huffman@27401:
huffman@27401: lemma deflation_ID: "deflation ID"
huffman@27401: by (simp add: deflation.intro)
huffman@27401:
huffman@41430: lemma deflation_bottom: "deflation \"
huffman@27401: by (simp add: deflation.intro)
huffman@27401:
huffman@31076: lemma deflation_below_iff:
huffman@27401: "\deflation p; deflation q\ \ p \ q \ (\x. p\x = x \ q\x = x)"
huffman@27401: apply safe
huffman@31076: apply (simp add: deflation.belowD)
huffman@31076: apply (simp add: deflation.belowI)
huffman@27401: done
huffman@27401:
huffman@27401: text {*
huffman@27401: The composition of two deflations is equal to
huffman@27401: the lesser of the two (if they are comparable).
huffman@27401: *}
huffman@27401:
huffman@31076: lemma deflation_below_comp1:
ballarin@28611: assumes "deflation f"
ballarin@28611: assumes "deflation g"
huffman@27401: shows "f \ g \ f\(g\x) = f\x"
huffman@31076: proof (rule below_antisym)
ballarin@29237: interpret g: deflation g by fact
huffman@31076: from g.below show "f\(g\x) \ f\x" by (rule monofun_cfun_arg)
huffman@27401: next
ballarin@29237: interpret f: deflation f by fact
huffman@27401: assume "f \ g" hence "f\x \ g\x" by (rule monofun_cfun_fun)
huffman@27401: hence "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg)
huffman@27401: also have "f\(f\x) = f\x" by (rule f.idem)
huffman@27401: finally show "f\x \ f\(g\x)" .
huffman@27401: qed
huffman@27401:
huffman@31076: lemma deflation_below_comp2:
huffman@27401: "\deflation f; deflation g; f \ g\ \ g\(f\x) = f\x"
huffman@31076: by (simp only: deflation.belowD deflation.idem)
huffman@27401:
huffman@27401:
huffman@27401: subsection {* Deflations with finite range *}
huffman@27401:
huffman@27401: lemma finite_range_imp_finite_fixes:
huffman@27401: "finite (range f) \ finite {x. f x = x}"
huffman@27401: proof -
huffman@27401: have "{x. f x = x} \ range f"
huffman@27401: by (clarify, erule subst, rule rangeI)
huffman@27401: moreover assume "finite (range f)"
huffman@27401: ultimately show "finite {x. f x = x}"
huffman@27401: by (rule finite_subset)
huffman@27401: qed
huffman@27401:
huffman@27401: locale finite_deflation = deflation +
huffman@27401: assumes finite_fixes: "finite {x. d\x = x}"
huffman@27401: begin
huffman@27401:
huffman@27401: lemma finite_range: "finite (range (\x. d\x))"
huffman@27401: by (simp add: range_eq_fixes finite_fixes)
huffman@27401:
huffman@27401: lemma finite_image: "finite ((\x. d\x) ` A)"
huffman@27401: by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
huffman@27401:
huffman@27401: lemma compact: "compact (d\x)"
huffman@27401: proof (rule compactI2)
huffman@27401: fix Y :: "nat \ 'a"
huffman@27401: assume Y: "chain Y"
huffman@27401: have "finite_chain (\i. d\(Y i))"
huffman@27401: proof (rule finite_range_imp_finch)
huffman@27401: show "chain (\i. d\(Y i))"
huffman@27401: using Y by simp
huffman@27401: have "range (\i. d\(Y i)) \ range (\x. d\x)"
huffman@27401: by clarsimp
huffman@27401: thus "finite (range (\i. d\(Y i)))"
huffman@27401: using finite_range by (rule finite_subset)
huffman@27401: qed
huffman@27401: hence "\j. (\i. d\(Y i)) = d\(Y j)"
huffman@27401: by (simp add: finite_chain_def maxinch_is_thelub Y)
huffman@27401: then obtain j where j: "(\i. d\(Y i)) = d\(Y j)" ..
huffman@27401:
huffman@27401: assume "d\x \ (\i. Y i)"
huffman@27401: hence "d\(d\x) \ d\(\i. Y i)"
huffman@27401: by (rule monofun_cfun_arg)
huffman@27401: hence "d\x \ (\i. d\(Y i))"
huffman@27401: by (simp add: contlub_cfun_arg Y idem)
huffman@27401: hence "d\x \ d\(Y j)"
huffman@27401: using j by simp
huffman@27401: hence "d\x \ Y j"
huffman@31076: using below by (rule below_trans)
huffman@27401: thus "\j. d\x \ Y j" ..
huffman@27401: qed
huffman@27401:
huffman@27401: end
huffman@27401:
brianh@39973: lemma finite_deflation_intro:
brianh@39973: "deflation d \ finite {x. d\x = x} \ finite_deflation d"
brianh@39973: by (intro finite_deflation.intro finite_deflation_axioms.intro)
brianh@39973:
brianh@39971: lemma finite_deflation_imp_deflation:
brianh@39971: "finite_deflation d \ deflation d"
brianh@39971: unfolding finite_deflation_def by simp
brianh@39971:
huffman@41430: lemma finite_deflation_bottom: "finite_deflation \"
brianh@39971: by default simp_all
brianh@39971:
huffman@27401:
huffman@27401: subsection {* Continuous embedding-projection pairs *}
huffman@27401:
huffman@27401: locale ep_pair =
huffman@27401: fixes e :: "'a \ 'b" and p :: "'b \ 'a"
huffman@27401: assumes e_inverse [simp]: "\x. p\(e\x) = x"
huffman@31076: and e_p_below: "\y. e\(p\y) \ y"
huffman@27401: begin
huffman@27401:
huffman@31076: lemma e_below_iff [simp]: "e\x \ e\y \ x \ y"
huffman@27401: proof
huffman@27401: assume "e\x \ e\y"
huffman@27401: hence "p\(e\x) \ p\(e\y)" by (rule monofun_cfun_arg)
huffman@27401: thus "x \ y" by simp
huffman@27401: next
huffman@27401: assume "x \ y"
huffman@27401: thus "e\x \ e\y" by (rule monofun_cfun_arg)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma e_eq_iff [simp]: "e\x = e\y \ x = y"
huffman@31076: unfolding po_eq_conv e_below_iff ..
huffman@27401:
huffman@27401: lemma p_eq_iff:
huffman@27401: "\e\(p\x) = x; e\(p\y) = y\ \ p\x = p\y \ x = y"
huffman@27401: by (safe, erule subst, erule subst, simp)
huffman@27401:
huffman@27401: lemma p_inverse: "(\x. y = e\x) = (e\(p\y) = y)"
huffman@27401: by (auto, rule exI, erule sym)
huffman@27401:
huffman@31076: lemma e_below_iff_below_p: "e\x \ y \ x \ p\y"
huffman@27401: proof
huffman@27401: assume "e\x \ y"
huffman@27401: then have "p\(e\x) \ p\y" by (rule monofun_cfun_arg)
huffman@27401: then show "x \ p\y" by simp
huffman@27401: next
huffman@27401: assume "x \ p\y"
huffman@27401: then have "e\x \ e\(p\y)" by (rule monofun_cfun_arg)
huffman@31076: then show "e\x \ y" using e_p_below by (rule below_trans)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma compact_e_rev: "compact (e\x) \ compact x"
huffman@27401: proof -
huffman@27401: assume "compact (e\x)"
huffman@41182: hence "adm (\y. e\x \ y)" by (rule compactD)
huffman@41182: hence "adm (\y. e\x \ e\y)" by (rule adm_subst [OF cont_Rep_cfun2])
huffman@41182: hence "adm (\y. x \ y)" by simp
huffman@27401: thus "compact x" by (rule compactI)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma compact_e: "compact x \ compact (e\x)"
huffman@27401: proof -
huffman@27401: assume "compact x"
huffman@41182: hence "adm (\y. x \ y)" by (rule compactD)
huffman@41182: hence "adm (\y. x \ p\y)" by (rule adm_subst [OF cont_Rep_cfun2])
huffman@41182: hence "adm (\y. e\x \ y)" by (simp add: e_below_iff_below_p)
huffman@27401: thus "compact (e\x)" by (rule compactI)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma compact_e_iff: "compact (e\x) \ compact x"
huffman@27401: by (rule iffI [OF compact_e_rev compact_e])
huffman@27401:
huffman@27401: text {* Deflations from ep-pairs *}
huffman@27401:
huffman@27401: lemma deflation_e_p: "deflation (e oo p)"
huffman@31076: by (simp add: deflation.intro e_p_below)
huffman@27401:
huffman@27401: lemma deflation_e_d_p:
ballarin@28611: assumes "deflation d"
huffman@27401: shows "deflation (e oo d oo p)"
huffman@27401: proof
ballarin@29237: interpret deflation d by fact
huffman@27401: fix x :: 'b
huffman@27401: show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
huffman@27401: by (simp add: idem)
huffman@27401: show "(e oo d oo p)\x \ x"
huffman@31076: by (simp add: e_below_iff_below_p below)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma finite_deflation_e_d_p:
ballarin@28611: assumes "finite_deflation d"
huffman@27401: shows "finite_deflation (e oo d oo p)"
huffman@27401: proof
ballarin@29237: interpret finite_deflation d by fact
huffman@27401: fix x :: 'b
huffman@27401: show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
huffman@27401: by (simp add: idem)
huffman@27401: show "(e oo d oo p)\x \ x"
huffman@31076: by (simp add: e_below_iff_below_p below)
huffman@27401: have "finite ((\x. e\x) ` (\x. d\x) ` range (\x. p\x))"
huffman@27401: by (simp add: finite_image)
huffman@27401: hence "finite (range (\x. (e oo d oo p)\x))"
huffman@27401: by (simp add: image_image)
huffman@27401: thus "finite {x. (e oo d oo p)\x = x}"
huffman@27401: by (rule finite_range_imp_finite_fixes)
huffman@27401: qed
huffman@27401:
huffman@27401: lemma deflation_p_d_e:
ballarin@28611: assumes "deflation d"
huffman@27401: assumes d: "\x. d\x \