Theory Deflation

theory Deflation
imports Plain_HOLCF
(*  Title:      HOL/HOLCF/Deflation.thy
    Author:     Brian Huffman
*)

header {* Continuous deflations and ep-pairs *}

theory Deflation
imports Plain_HOLCF
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 \<sqsubseteq> x"
begin

lemma below_ID: "d \<sqsubseteq> 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 \<sqsubseteq> f"
proof (rule cfun_belowI)
  fix x
  from below have "f·(d·x) \<sqsubseteq> f·x" by (rule monofun_cfun_arg)
  also from idem have "f·(d·x) = d·x" by (rule f)
  finally show "d·x \<sqsubseteq> f·x" .
qed

lemma belowD: "[|f \<sqsubseteq> d; f·x = x|] ==> d·x = x"
proof (rule below_antisym)
  from below show "d·x \<sqsubseteq> x" .
next
  assume "f \<sqsubseteq> d"
  hence "f·x \<sqsubseteq> d·x" by (rule monofun_cfun_fun)
  also assume "f·x = x"
  finally show "x \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> g ==> f·(g·x) = f·x"
proof (rule below_antisym)
  interpret g: deflation g by fact
  from g.below show "f·(g·x) \<sqsubseteq> f·x" by (rule monofun_cfun_arg)
next
  interpret f: deflation f by fact
  assume "f \<sqsubseteq> g" hence "f·x \<sqsubseteq> g·x" by (rule monofun_cfun_fun)
  hence "f·(f·x) \<sqsubseteq> f·(g·x)" by (rule monofun_cfun_arg)
  also have "f·(f·x) = f·x" by (rule f.idem)
  finally show "f·x \<sqsubseteq> f·(g·x)" .
qed

lemma deflation_below_comp2:
  "[|deflation f; deflation g; f \<sqsubseteq> g|] ==> g·(f·x) = f·x"
by (simp only: deflation.belowD deflation.idem)


subsection {* Deflations with finite range *}

lemma finite_range_imp_finite_fixes:
  "finite (range f) ==> finite {x. f x = x}"
proof -
  have "{x. f x = x} ⊆ range f"
    by (clarify, erule subst, rule rangeI)
  moreover assume "finite (range f)"
  ultimately 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)
    show "chain (λi. d·(Y i))"
      using Y by simp
    have "range (λi. d·(Y i)) ⊆ range (λx. d·x)"
      by clarsimp
    thus "finite (range (λi. d·(Y i)))"
      using finite_range by (rule finite_subset)
  qed
  hence "∃j. (\<Squnion>i. d·(Y i)) = d·(Y j)"
    by (simp add: finite_chain_def maxinch_is_thelub Y)
  then obtain j where j: "(\<Squnion>i. d·(Y i)) = d·(Y j)" ..

  assume "d·x \<sqsubseteq> (\<Squnion>i. Y i)"
  hence "d·(d·x) \<sqsubseteq> d·(\<Squnion>i. Y i)"
    by (rule monofun_cfun_arg)
  hence "d·x \<sqsubseteq> (\<Squnion>i. d·(Y i))"
    by (simp add: contlub_cfun_arg Y idem)
  hence "d·x \<sqsubseteq> d·(Y j)"
    using j by simp
  hence "d·x \<sqsubseteq> Y j"
    using below by (rule below_trans)
  thus "∃j. d·x \<sqsubseteq> 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"
unfolding finite_deflation_def by simp

lemma finite_deflation_bottom: "finite_deflation ⊥"
by default 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) \<sqsubseteq> y"
begin

lemma e_below_iff [simp]: "e·x \<sqsubseteq> e·y <-> x \<sqsubseteq> y"
proof
  assume "e·x \<sqsubseteq> e·y"
  hence "p·(e·x) \<sqsubseteq> p·(e·y)" by (rule monofun_cfun_arg)
  thus "x \<sqsubseteq> y" by simp
next
  assume "x \<sqsubseteq> y"
  thus "e·x \<sqsubseteq> 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 \<sqsubseteq> y <-> x \<sqsubseteq> p·y"
proof
  assume "e·x \<sqsubseteq> y"
  then have "p·(e·x) \<sqsubseteq> p·y" by (rule monofun_cfun_arg)
  then show "x \<sqsubseteq> p·y" by simp
next
  assume "x \<sqsubseteq> p·y"
  then have "e·x \<sqsubseteq> e·(p·y)" by (rule monofun_cfun_arg)
  then show "e·x \<sqsubseteq> y" using e_p_below by (rule below_trans)
qed

lemma compact_e_rev: "compact (e·x) ==> compact x"
proof -
  assume "compact (e·x)"
  hence "adm (λy. e·x \<notsqsubseteq> y)" by (rule compactD)
  hence "adm (λy. e·x \<notsqsubseteq> e·y)" by (rule adm_subst [OF cont_Rep_cfun2])
  hence "adm (λy. x \<notsqsubseteq> y)" by simp
  thus "compact x" by (rule compactI)
qed

lemma compact_e: "compact x ==> compact (e·x)"
proof -
  assume "compact x"
  hence "adm (λy. x \<notsqsubseteq> y)" by (rule compactD)
  hence "adm (λy. x \<notsqsubseteq> p·y)" by (rule adm_subst [OF cont_Rep_cfun2])
  hence "adm (λy. e·x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
  thus "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 \<sqsubseteq> 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 \<sqsubseteq> 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)
  hence "finite (range (λx. (e oo d oo p)·x))"
    by (simp add: image_image)
  thus "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 \<sqsubseteq> e·(p·x)"
  shows "deflation (p oo d oo e)"
proof -
  interpret d: deflation d by fact
  {
    fix x
    have "d·(e·x) \<sqsubseteq> e·x"
      by (rule d.below)
    hence "p·(d·(e·x)) \<sqsubseteq> p·(e·x)"
      by (rule monofun_cfun_arg)
    hence "(p oo d oo e)·x \<sqsubseteq> x"
      by simp
  }
  note p_d_e_below = this
  show ?thesis
  proof
    fix x
    show "(p oo d oo e)·x \<sqsubseteq> x"
      by (rule p_d_e_below)
  next
    fix x
    show "(p oo d oo e)·((p oo d oo e)·x) = (p oo d oo e)·x"
    proof (rule below_antisym)
      show "(p oo d oo e)·((p oo d oo e)·x) \<sqsubseteq> (p oo d oo e)·x"
        by (rule p_d_e_below)
      have "p·(d·(d·(d·(e·x)))) \<sqsubseteq> p·(d·(e·(p·(d·(e·x)))))"
        by (intro monofun_cfun_arg d)
      hence "p·(d·(e·x)) \<sqsubseteq> p·(d·(e·(p·(d·(e·x)))))"
        by (simp only: d.idem)
      thus "(p oo d oo e)·x \<sqsubseteq> (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 \<sqsubseteq> 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" ..
    thus "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)
    hence "finite ((λx. p·x) ` (λx. d·x) ` range (λx. e·x))"
      by (rule finite_imageI)
    hence "finite (range (λx. (p oo d oo e)·x))"
      by (simp add: image_image)
    thus "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 \<sqsubseteq> e2"
proof (rule cfun_belowI)
  fix x
  have "e1·(p·(e2·x)) \<sqsubseteq> e2·x"
    by (rule ep_pair.e_p_below [OF 1])
  thus "e1·x \<sqsubseteq> 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 \<sqsubseteq> p2"
proof (rule cfun_belowI)
  fix x
  have "e·(p1·x) \<sqsubseteq> x"
    by (rule ep_pair.e_p_below [OF 1])
  hence "p2·(e·(p1·x)) \<sqsubseteq> p2·x"
    by (rule monofun_cfun_arg)
  thus "p1·x \<sqsubseteq> 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 default 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)) \<sqsubseteq> p2·y"
    by (rule ep1.e_p_below)
  hence "e2·(e1·(p1·(p2·y))) \<sqsubseteq> e2·(p2·y)"
    by (rule monofun_cfun_arg)
  also have "e2·(p2·y) \<sqsubseteq> y"
    by (rule ep2.e_p_below)
  finally show "(e2 oo e1)·((p1 oo p2)·y) \<sqsubseteq> 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 "⊥ \<sqsubseteq> p·⊥" by (rule minimal)
  hence "e·⊥ \<sqsubseteq> e·(p·⊥)" by (rule monofun_cfun_arg)
  also have "e·(p·⊥) \<sqsubseteq> ⊥" 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