(*  Title:      HOLCF/Powerdomains.thy

    Author:     Brian Huffman

*)

header {* Powerdomains *}

theory Powerdomains

imports ConvexPD Domain

begin

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 *}

lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex

lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID

lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex

lemmas [domain_deflation] =

  deflation_upper_map deflation_lower_map deflation_convex_map

setup {*

  fold Domain_Take_Proofs.add_rec_type

    [(@{type_name "upper_pd"}, [true]),

     (@{type_name "lower_pd"}, [true]),

     (@{type_name "convex_pd"}, [true])]

*}

end