(* Title: HOL/HOLCF/Deflation.thy Author: Brian Huffman *) section ‹Continuous deflations and ep-pairs› theory Deflation imports Cfun begin default_sort cpo subsection ‹Continuous deflations› 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 ‹The set of fixed points is the same as the range.› 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 ‹ The pointwise ordering on deflation functions coincides with the subset ordering of their sets of fixed-points. › 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 ‹ The composition of two deflations is equal to the lesser of the two (if they are comparable). › 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 ‹Deflations with finite range› 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 ‹Continuous embedding-projection pairs› 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 \<notsqsubseteq> y)" by (rule compactD) then have "adm (λy. e⋅x \<notsqsubseteq> e⋅y)" by (rule adm_subst [OF cont_Rep_cfun2]) then have "adm (λy. x \<notsqsubseteq> 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 \<notsqsubseteq> y)" by (rule compactD) then have "adm (λy. x \<notsqsubseteq> p⋅y)" by (rule adm_subst [OF cont_Rep_cfun2]) then have "adm (λy. e⋅x \<notsqsubseteq> 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 ‹Deflations from ep-pairs› 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 ‹Uniqueness of ep-pairs› 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 ‹Composing ep-pairs› 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