Theory HOLCFUtils

section ‹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 ‹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 ‹bool› a pointed chain-complete partial order.
›

instantiation bool :: po
begin
definition
  "x ⊑ y ⟷ (x ⟶ y)"
instance by standard (unfold below_bool_def, fast+)
end

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

instance bool :: pcpo
proof
  have "∀y. False ⊑ y" by (simp add: below_bool_def)
  thus "∃x::bool. ∀y. x ⊑ 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 ⊑ B ⟷ A ⊆ B"
instance by standard (unfold below_set_def, fast+)
end

lemma sqsubset_is_subset: "A ⊑ B ⟷ A ⊆ B"
  by (fact below_set_def)

lemma is_lub_set: "S <<| ⋃S"
  unfolding is_lub_def is_ub_def below_set_def by fast

lemma lub_is_union: "lub S = ⋃S"
  using is_lub_set by (rule lub_eqI)

instance set :: (type) cpo
  by standard (fast intro: is_lub_set)

lemma emptyset_is_bot[simp]: "{} ⊑ S"
  by (simp add:sqsubset_is_subset)

instance set :: (type) pcpo
  by standard (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 ‹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. ⋃y∈ f x. g x y)"
proof(induct rule: contI2[case_names Mono Limit])
case Mono
  show "monofun (λx. ⋃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 "(⋃y∈f (⨆ i. Y i). g (⨆ j. Y j) y) ⊆ (⨆ k. ⋃y∈f (Y k). g (Y k) y)"
  proof
    fix x assume "x ∈ (⋃y∈f (⨆ i. Y i). g (⨆ j. Y j) y)"
    then obtain y where "y∈f (⨆ i. Y i)" and "x∈ g (⨆ j. Y j) y" by auto
    hence "y ∈ (⨆ i. f (Y i))" and "x∈ (⨆ 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∈ (⋃y∈ f (Y k). g (Y k) y)" by auto
    thus "x∈ (⨆ k. ⋃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_case_list [simp, cont2cont]:
  assumes "⋀y. cont (λx. f1 x)"
     and  "⋀y z. cont (λx. f2 x y z)"
  shows "cont (λx. case_list (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  "(⨆ i. y ∈ Y i) = False"
  by auto
thus "y ∉ (⨆ 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