# Theory Deflation

Up to index of Isabelle/HOL/HOLCF

theory Deflation
imports Plain_HOLCF
`(*  Title:      HOL/HOLCF/Deflation.thy    Author:     Brian Huffman*)header {* Continuous deflations and ep-pairs *}theory Deflationimports Plain_HOLCFbegindefault_sort cposubsection {* Continuous deflations *}locale deflation =  fixes d :: "'a -> 'a"  assumes idem: "!!x. d·(d·x) = d·x"  assumes below: "!!x. d·x \<sqsubseteq> x"beginlemma 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" .qedlemma 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" .qedendlemma 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)donetext {*  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)" .qedlemma 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)qedlocale finite_deflation = deflation +  assumes finite_fixes: "finite {x. d·x = x}"beginlemma 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" ..qedendlemma 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 simplemma finite_deflation_bottom: "finite_deflation ⊥"by default simp_allsubsection {* 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"beginlemma 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 simpnext  assume "x \<sqsubseteq> y"  thus "e·x \<sqsubseteq> e·y" by (rule monofun_cfun_arg)qedlemma 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 simpnext  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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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  qedqedlemma 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)  qedqedendsubsection {* 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])qedlemma 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])qedlemma 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_alllemma 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 simpqedlocale pcpo_ep_pair = ep_pair e p  for e :: "'a::pcpo -> 'b::pcpo"  and p :: "'b::pcpo -> 'a::pcpo"beginlemma 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 simpqedlemma e_bottom_iff [simp]: "e·x = ⊥ <-> x = ⊥"by (rule e_eq_iff [where y="⊥", unfolded e_strict])lemma e_defined: "x ≠ ⊥ ==> e·x ≠ ⊥"by simplemma p_strict [simp]: "p·⊥ = ⊥"by (rule e_inverse [where x="⊥", unfolded e_strict])lemmas stricts = e_strict p_strictendend`