# Theory Deflation

```(*  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 deflation_ID: "deflation ID"

lemma deflation_bottom: "deflation ⊥"

lemma deflation_below_iff: "deflation p ⟹ deflation q ⟹ p ⊑ q ⟷ (∀x. p⋅x = x ⟶ q⋅x = x)"
apply safe
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))"

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"

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 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)"

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"
show "(e oo d oo p)⋅x ⊑ x"
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"
show "(e oo d oo p)⋅x ⊑ x"
have "finite ((λx. e⋅x) ` (λx. d⋅x) ` range (λx. p⋅x))"
then have "finite (range (λx. (e oo d oo p)⋅x))"
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))"
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
```