Theory HOLCFUtils

header {* HOLCF Utility lemmas *}
theory HOLCFUtils
imports HOLCF
begin

text {*
We use @{theory HOLCF} to define the denotational semantics. By default, HOLCF does not turn the regular @{text set} type into a partial order, so this is done here. Some of the lemmas here are contributed by Brian Huffman.

We start by making the type @{text bool} a pointed chain-complete partial order.
*}

instantiation bool :: po
begin
definition
  "x \<sqsubseteq> y <-> (x --> y)"
instance by (default, unfold below_bool_def, fast+)
end

instance bool :: chfin
apply default
apply (drule finite_range_imp_finch)
apply (rule finite)
apply (simp add: finite_chain_def)
done

instance bool :: pcpo
proof
  have "∀y. False \<sqsubseteq> y" by (simp add: below_bool_def)
  thus "∃x::bool. ∀y. x \<sqsubseteq> y" ..
qed

lemma is_lub_bool: "S <<| (True ∈ S)"
  unfolding is_lub_def is_ub_def below_bool_def by auto

lemma lub_bool: "lub S = (True ∈ S)"
  using is_lub_bool by (rule lub_eqI)

lemma bottom_eq_False[simp]: "⊥ = False"
by (rule below_antisym [OF minimal], simp add: below_bool_def)

text {*
To convert between the squared syntax used by @{theory HOLCF} and the regular, round syntax for sets, we state some of the equivalencies.
*}

instantiation set :: (type) po
begin
definition
  "A \<sqsubseteq> B <-> A ⊆ B"
instance by (default, unfold below_set_def, fast+)
end

lemma sqsubset_is_subset: "A \<sqsubseteq> B <-> A ⊆ B"
  by (fact below_set_def)

lemma is_lub_set: "S <<| \<Union>S"
  unfolding is_lub_def is_ub_def below_set_def by fast

lemma lub_is_union: "lub S = \<Union>S"
  using is_lub_set by (rule lub_eqI)

instance set :: (type) cpo
  by (default, fast intro: is_lub_set)

lemma emptyset_is_bot[simp]: "{} \<sqsubseteq> S"
  by (simp add:sqsubset_is_subset)

instance set :: (type) pcpo
  by (default, fast intro: emptyset_is_bot)

lemma bot_bool_is_emptyset[simp]: "⊥ = {}"
  using emptyset_is_bot by (rule bottomI [symmetric])

text {*
To actually use these instance in @{text fixrec} definitions or fixed-point inductions, we need continuity requrements for various boolean and set operations.
*}

lemma cont2cont_disj [simp, cont2cont]:
  assumes f: "cont (λx. f x)" and g: "cont (λx. g x)"
  shows "cont (λx. f x ∨ g x)"
apply (rule cont_apply [OF f])
apply (rule chfindom_monofun2cont)
apply (rule monofunI, simp add: below_bool_def)
apply (rule cont_compose [OF _ g])
apply (rule chfindom_monofun2cont)
apply (rule monofunI, simp add: below_bool_def)
done

lemma cont2cont_imp[simp, cont2cont]:
  assumes f: "cont (λx. ¬ f x)" and g: "cont (λx. g x)"
  shows "cont (λx. f x --> g x)"
unfolding imp_conv_disj by (rule cont2cont_disj[OF f g])

lemma cont2cont_Collect [simp, cont2cont]:
  assumes "!!y. cont (λx. f x y)"
  shows "cont (λx. {y. f x y})"
apply (rule contI)
apply (subst cont2contlubE [OF assms], assumption)
apply (auto simp add: is_lub_def is_ub_def below_set_def lub_bool)
done

lemma cont2cont_mem [simp, cont2cont]:
  assumes "cont (λx. f x)"
  shows "cont (λx. y ∈ f x)"
apply (rule cont_compose [OF _ assms])
apply (rule contI)
apply (auto simp add: is_lub_def is_ub_def below_bool_def lub_is_union)
done

lemma cont2cont_union [simp, cont2cont]:
  "cont (λx. f x) ==> cont (λx. g x)
==> cont (λx. f x ∪ g x)"
unfolding Un_def by simp

lemma cont2cont_insert [simp, cont2cont]:
  assumes "cont (λx. f x)"
  shows "cont (λx. insert y (f x))"
unfolding insert_def using assms
by (intro cont2cont)

lemmas adm_subset = adm_below[where ?'b = "'a::type set", unfolded sqsubset_is_subset]

lemma cont2cont_UNION[cont2cont,simp]:
  assumes "cont f"
      and "!! y. cont (λx. g x y)"
  shows "cont (λx. \<Union>y∈ f x. g x y)"
proof(induct rule: contI2[case_names Mono Limit])
case Mono
  show "monofun (λx. \<Union>y∈f x. g x y)"
    by (rule monofunI)(auto iff:sqsubset_is_subset dest: monofunE[OF assms(1)[THEN cont2mono]] monofunE[OF assms(2)[THEN cont2mono]])
next
case (Limit Y)
  have "(\<Union>y∈f (\<Squnion> i. Y i). g (\<Squnion> j. Y j) y) ⊆ (\<Squnion> k. \<Union>y∈f (Y k). g (Y k) y)"
  proof
    fix x assume "x ∈ (\<Union>y∈f (\<Squnion> i. Y i). g (\<Squnion> j. Y j) y)"
    then obtain y where "y∈f (\<Squnion> i. Y i)" and "x∈ g (\<Squnion> j. Y j) y" by auto
    hence "y ∈ (\<Squnion> i. f (Y i))" and "x∈ (\<Squnion> j. g (Y j) y)" by (auto simp add: cont2contlubE[OF assms(1) Limit(1)] cont2contlubE[OF assms(2) Limit(1)])
    then obtain i and j where yi: "y∈ f (Y i)" and xj: "x∈ g (Y j) y" by (auto simp add:lub_is_union)
    obtain k where "i≤k" and "j≤k" by (erule_tac x = "max i j" in meta_allE)auto
    from yi and xj have "y ∈ f (Y k)" and "x∈ g (Y k) y"
      using monofunE[OF assms(1)[THEN cont2mono], OF chain_mono[OF Limit(1) `i≤k`]]
        and monofunE[OF assms(2)[THEN cont2mono], OF chain_mono[OF Limit(1) `j≤k`]]
      by (auto simp add:sqsubset_is_subset)
    hence "x∈ (\<Union>y∈ f (Y k). g (Y k) y)" by auto
    thus "x∈ (\<Squnion> k. \<Union>y∈f (Y k). g (Y k) y)" by (auto simp add:lub_is_union)
  qed
  thus ?case by (simp add:sqsubset_is_subset)
qed

lemma cont2cont_Let_simple[simp,cont2cont]:
  assumes "cont (λx. g x t)"
  shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .


lemma cont2cont_list_case [simp, cont2cont]:
  assumes "!!y. cont (λx. f1 x)"
     and  "!!y z. cont (λx. f2 x y z)"
  shows "cont (λx. list_case (f1 x) (f2 x) l)"
using assms
by (cases l) auto


text {* As with the continuity lemmas, we need admissibility lemmas. *}

lemma adm_not_mem:
  assumes "cont (λx. f x)"
  shows "adm (λx. y ∉ f x)"
using assms
apply (erule_tac t = f in adm_subst)
proof (rule admI)
fix Y :: "nat => 'b set"
assume chain: "chain Y"
assume "∀i. y ∉ Y i" hence  "(\<Squnion> i. y ∈ Y i) = False"
  by auto
thus "y ∉ (\<Squnion> i. Y i)"
  using chain unfolding lub_bool lub_is_union by auto
qed

lemma adm_id[simp]: "adm (λx . x)"
by (rule adm_chfin)

lemma adm_Not[simp]: "adm Not"
by (rule adm_chfin)

lemma adm_prod_split:
  assumes "adm (λp. f (fst p) (snd p))"
  shows "adm (λ(x,y). f x y)"
using assms unfolding split_def .

lemma adm_ball':
  assumes "!! y. adm (λx. y ∈ A x --> P x y)"
  shows "adm (λx. ∀y ∈ A x . P x y)"
by (subst Ball_def, rule adm_all[OF assms])

lemma adm_not_conj:
  "[|adm (λx. ¬ P x); adm (λx. ¬ Q x)|] ==> adm (λx. ¬ (P x ∧ Q x))"
by simp

lemma adm_single_valued:
 assumes "cont (λx. f x)"
 shows "adm (λx. single_valued (f x))"
using assms
unfolding single_valued_def
by (intro adm_lemmas adm_not_mem cont2cont adm_subst[of f])

text {*
To match Shivers' syntax we introduce the power-syntax for iterated function application.
*}

abbreviation niceiterate ("(_⇗_⇖)" [1000] 1000)
  where "niceiterate f i ≡ iterate i·f"

end