src/HOLCF/Powerdomains.thy

improving the compilation to handle predicate arguments in higher-order argument positions

(*  Title:      HOLCF/Powerdomains.thy
    Author:     Brian Huffman
*)

header {* Powerdomains *}

theory Powerdomains
imports Representable ConvexPD
begin

subsection {* Powerdomains are representable *}

text "Upper powerdomain of a representable type is representable."

instantiation upper_pd :: (rep) rep
begin

definition emb_upper_pd_def: "emb = udom_emb oo upper_map\<cdot>emb"
definition prj_upper_pd_def: "prj = upper_map\<cdot>prj oo udom_prj"

instance
 apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def)
 apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom)
done

end

text "Lower powerdomain of a representable type is representable."

instantiation lower_pd :: (rep) rep
begin

definition emb_lower_pd_def: "emb = udom_emb oo lower_map\<cdot>emb"
definition prj_lower_pd_def: "prj = lower_map\<cdot>prj oo udom_prj"

instance
 apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def)
 apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom)
done

end

text "Convex powerdomain of a representable type is representable."

instantiation convex_pd :: (rep) rep
begin

definition emb_convex_pd_def: "emb = udom_emb oo convex_map\<cdot>emb"
definition prj_convex_pd_def: "prj = convex_map\<cdot>prj oo udom_prj"

instance
 apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def)
 apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom)
done

end

subsection {* Finite deflation lemmas *}

text "TODO: move these lemmas somewhere else"

lemma finite_compact_range_imp_finite_range:
  fixes d :: "'a::profinite \<rightarrow> 'b::cpo"
  assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
  shows "finite (range (\<lambda>x. d\<cdot>x))"
proof (rule finite_subset [OF _ prems])
  {
    fix x :: 'a
    have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
      by auto
    hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
      using prems by (rule finite_subset)
    hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
      by (simp add: finite_range_imp_finch)
    hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
      by (simp add: finite_chain_def maxinch_is_thelub)
    hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
      by (simp add: lub_distribs)
    hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
      by auto
  }
  thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
    by clarsimp
qed

lemma finite_deflation_upper_map:
  assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
  interpret d: finite_deflation d by fact
  have "deflation d" by fact
  thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
  hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
  hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` range upper_principal)"
    apply (rule finite_subset [COMP swap_prems_rl])
    apply (clarsimp, rename_tac t)
    apply (induct_tac t rule: pd_basis_induct)
    apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDUnit)
    apply (rule image_eqI)
    apply (erule sym)
    apply simp
    apply (rule exI)
    apply (rule Abs_compact_basis_inverse [symmetric])
    apply (simp add: d.compact)
    apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDPlus)
    done
  moreover have "{xs::'a upper_pd. compact xs} = range upper_principal"
    by (auto dest: upper_pd.compact_imp_principal)
  ultimately have "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
    by simp
  hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
    by (rule finite_compact_range_imp_finite_range)
  thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
    by (rule finite_range_imp_finite_fixes)
qed

lemma finite_deflation_lower_map:
  assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
  interpret d: finite_deflation d by fact
  have "deflation d" by fact
  thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
  hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
  hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` range lower_principal)"
    apply (rule finite_subset [COMP swap_prems_rl])
    apply (clarsimp, rename_tac t)
    apply (induct_tac t rule: pd_basis_induct)
    apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit)
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDUnit)
    apply (rule image_eqI)
    apply (erule sym)
    apply simp
    apply (rule exI)
    apply (rule Abs_compact_basis_inverse [symmetric])
    apply (simp add: d.compact)
    apply (simp only: lower_plus_principal [symmetric] lower_map_plus)
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDPlus)
    done
  moreover have "{xs::'a lower_pd. compact xs} = range lower_principal"
    by (auto dest: lower_pd.compact_imp_principal)
  ultimately have "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
    by simp
  hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
    by (rule finite_compact_range_imp_finite_range)
  thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
    by (rule finite_range_imp_finite_fixes)
qed

lemma finite_deflation_convex_map:
  assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
  interpret d: finite_deflation d by fact
  have "deflation d" by fact
  thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
  hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
  hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` range convex_principal)"
    apply (rule finite_subset [COMP swap_prems_rl])
    apply (clarsimp, rename_tac t)
    apply (induct_tac t rule: pd_basis_induct)
    apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit)
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDUnit)
    apply (rule image_eqI)
    apply (erule sym)
    apply simp
    apply (rule exI)
    apply (rule Abs_compact_basis_inverse [symmetric])
    apply (simp add: d.compact)
    apply (simp only: convex_plus_principal [symmetric] convex_map_plus)
    apply clarsimp
    apply (rule imageI)
    apply (rule vimageI2)
    apply (simp add: Rep_PDPlus)
    done
  moreover have "{xs::'a convex_pd. compact xs} = range convex_principal"
    by (auto dest: convex_pd.compact_imp_principal)
  ultimately have "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
    by simp
  hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
    by (rule finite_compact_range_imp_finite_range)
  thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
    by (rule finite_range_imp_finite_fixes)
qed

subsection {* Deflation combinators *}

definition "upper_defl = TypeRep_fun1 upper_map"
definition "lower_defl = TypeRep_fun1 lower_map"
definition "convex_defl = TypeRep_fun1 convex_map"

lemma cast_upper_defl:
  "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
unfolding upper_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_upper_map)
done

lemma cast_lower_defl:
  "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
unfolding lower_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_lower_map)
done

lemma cast_convex_defl:
  "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
unfolding convex_defl_def
apply (rule cast_TypeRep_fun1)
apply (erule finite_deflation_convex_map)
done

lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
apply (simp add: cast_REP cast_upper_defl)
apply (simp add: prj_upper_pd_def)
apply (simp add: emb_upper_pd_def)
apply (simp add: upper_map_map cfcomp1)
done

lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
apply (simp add: cast_REP cast_lower_defl)
apply (simp add: prj_lower_pd_def)
apply (simp add: emb_lower_pd_def)
apply (simp add: lower_map_map cfcomp1)
done

lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
apply (rule cast_eq_imp_eq, rule ext_cfun)
apply (simp add: cast_REP cast_convex_defl)
apply (simp add: prj_convex_pd_def)
apply (simp add: emb_convex_pd_def)
apply (simp add: convex_map_map cfcomp1)
done

lemma isodefl_upper:
  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
apply (rule isodeflI)
apply (simp add: cast_upper_defl cast_isodefl)
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
apply (simp add: upper_map_map)
done

lemma isodefl_lower:
  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
apply (rule isodeflI)
apply (simp add: cast_lower_defl cast_isodefl)
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
apply (simp add: lower_map_map)
done

lemma isodefl_convex:
  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
apply (rule isodeflI)
apply (simp add: cast_convex_defl cast_isodefl)
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
apply (simp add: convex_map_map)
done

subsection {* Domain package setup for powerdomains *}

setup {*
  fold Domain_Isomorphism.add_type_constructor
    [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
        @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
          @{thm deflation_upper_map}),

     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
        @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
          @{thm deflation_lower_map}),

     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
        @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
          @{thm deflation_convex_map})]
*}

end