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. yf 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 "(yf ( i. Y i). g ( j. Y j) y)  ( k. yf (Y k). g (Y k) y)"
  proof
    fix x assume "x  (yf ( i. Y i). g ( j. Y j) y)"
    then obtain y where "yf ( 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 "ik" and "jk" 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) ik]]
        and monofunE[OF assms(2)[THEN cont2mono], OF chain_mono[OF Limit(1) jk]]
      by (auto simp add:sqsubset_is_subset)
    hence "x (y f (Y k). g (Y k) y)" by auto
    thus "x ( k. yf (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 if"

end