Theory Basis

(*  Title:      Basis.thy
    Author:     Peter Gammie
*)

theory Basis
imports
  HOLCF
  "HOL-Library.Product_Order"
  "HOL-Library.Dual_Ordered_Lattice"
  "HOLCF-Library.Nat_Discrete"
begin

subsection‹Auxiliary lemmas›

lemma cfun_map_below_ID:
  assumes e: "e ⊑ ID"
  shows "cfun_map⋅e⋅e ⊑ ID"
proof(intro cfun_belowI)
  fix f x
  from e have "cfun_map⋅e⋅e⋅f⋅x ⊑ ID⋅(f⋅(ID⋅x))"
    by (simp del: ID1) (fast intro: monofun_cfun)
  thus "cfun_map⋅e⋅e⋅f⋅x ⊑ ID⋅f⋅x" by simp
qed

lemma cfun_below_ID:
  "⟦ f ⊑ ID; x ⊑ y ⟧ ⟹ f⋅x ⊑ y"
by (auto simp: cfun_below_iff elim: below_trans)

lemma oo_below:
  "⟦ f ⊑ f'; g ⊑ g' ⟧ ⟹ f oo g ⊑ f' oo g'"
by (simp add: oo_def cfun_below_iff monofun_cfun)

lemma cont_case_nat[simp]:
  "⟦cont (λx. f x); ⋀n. cont (λx. g x n) ⟧ ⟹ cont (λx. case_nat (f x) (g x) n)"
by (cases n, simp_all)

lemma cont2cont_if_below_const [cont2cont, simp]:
  assumes f: "cont (λx. f x)" and g: "cont (λx. g x)"
  shows "cont (λx. if f x ⊑ d then ⊥ else g x)"
proof (rule cont_apply [OF f])
  show "⋀x. cont (λy. if y ⊑ d then ⊥ else g x)"
    unfolding cont_def is_lub_def is_ub_def ball_simps
    by (simp add: lub_below_iff)
  show "⋀y. cont (λx. if y ⊑ d then ⊥ else g x)"
    by (simp add: g)
qed

lemma cont2cont_foldl [simp, cont2cont]:
  fixes f :: "'a::cpo ⇒ 'b::cpo ⇒ 'c::cpo ⇒ 'b"
  fixes xs :: "'c list"
  fixes z :: "'a ⇒ 'b"
  assumes "cont (λ(x, y, z). f x y z)"
  assumes "cont z"
  shows "cont (λx. foldl (f x) (z x) xs)"
using assms by (induct xs rule: rev_induct) (auto simp: prod_cont_iff intro: cont_apply)

lemma cont2cont_foldr [simp, cont2cont]:
  fixes f :: "'a::cpo ⇒ 'c::cpo ⇒ 'b::cpo ⇒ 'b"
  fixes xs :: "'c list"
  fixes z :: "'a ⇒ 'b"
  assumes "cont (λ(x, y, z). f x y z)"
  assumes "cont z"
  shows "cont (λx. foldr (f x) xs (z x))"
using assms by (induct xs) (auto simp: prod_cont_iff intro: cont_apply)

text‹

The following proof is due to
\<^citet>‹‹Eqn~2.28› in "DBLP:journals/siamcomp/Scott76"›.

›

lemma fix_argument_promote:
  assumes "cont g"
  shows "(Λ x. fix⋅(g x)) = fix⋅(Λ f x. g x⋅(f⋅x))"
proof(rule below_antisym)
  have "(Λ x. g x⋅(fix⋅(g x))) = (Λ x. fix⋅(g x))"
    by (subst fix_eq) simp
  with ‹cont g› show "fix⋅(Λ f x. g x⋅(f⋅x)) ⊑ (Λ x. fix⋅(g x))"
    by (simp add: fix_least cont2cont_LAM)
next
  show "(Λ x. fix⋅(g x)) ⊑ fix⋅(Λ f x. g x⋅(f⋅x))"
  proof(rule cfun_belowI)
    fix y
    from ‹cont g›
    have "g y⋅(fix⋅(Λ f x. g x⋅(f⋅x))⋅y) = fix⋅(Λ f x. g x⋅(f⋅x))⋅y"
      by (subst fix_eq, simp add: cont2cont_LAM)
    with ‹cont g› show "(Λ x. fix⋅(g x))⋅y ⊑ fix⋅(Λ f x. g x⋅(f⋅x))⋅y"
      by (simp add: fix_least)
  qed
qed

lemma fix_argument_promote_fun:
  fixes g :: "'a::type ⇒ 'b::pcpo → 'b"
  shows "(λx. fix⋅(g x)) = (μ f. (λx. g x⋅(f x)))"
proof(rule below_antisym)
  have "(λx. g x⋅(fix⋅(g x))) = (λx. fix⋅(g x))"
    by (subst fix_eq) simp
  then show "(μ f. (λx. g x⋅(f x))) ⊑ (λx. fix⋅(g x))"
    by (simp add: fix_least cont_fun)
next
  show "(λx. fix⋅(g x)) ⊑ (μ f. (λx. g x⋅(f x)))"
  proof(rule fun_belowI)
    fix y
    have "g y⋅((μ f. (λx. g x⋅(f x))) y) = (μ f. (λx. g x⋅(f x))) y"
      by (subst fix_eq, simp add: cont_fun)
    thus "fix⋅(g y) ⊑ (μ f. (λx. g x⋅(f x))) y"
      by (simp add: fix_least)
  qed
qed

lemma adm_cart_prod [intro, simp]:
  assumes X: "adm (λx. x ∈ X)"
  assumes Y: "adm (λx. x ∈ Y)"
  shows "adm (λx. x ∈ X × Y)"
proof(rule admI)
  fix A assume A: "chain A" and Ai: "∀i. A i ∈ X × Y"
  from Ai have "∀i. fst (A i) ∈ X" and "∀i. snd (A i) ∈ Y" by (auto simp: mem_Times_iff)
  with A X Y show "Lub A ∈ X × Y" by (auto intro: admD intro!: adm_subst simp: lub_prod)
qed

lemma adm_exists_unique [intro, simp]:
  assumes Q: "⋀y. adm (λx. Q x y)"
  assumes P: "⋀x x'. P x ∧ P x' ⟶ x = x'"
  shows "adm (λx. ∃y. P y ∧ Q x y)"
proof(rule admI)
  fix Y assume Y: "chain Y" and Yi: "∀i. ∃y. P y ∧ Q (Y i) y"
  then obtain y where Py: "P y" by blast
  with P Q Y Yi have "Q (Lub Y) y"
    by - (rule admD, fastforce+)
  with Py show "∃y. P y ∧ Q (Lub Y) y" by blast
qed


subsubsection‹Order monics›

text‹

Order monics are invertible with respect to the partial order. They
don't need to be continuous!

All domain data constructors are @{term "below_monic_cfun"}.

›

definition
  below_monic :: "('a::cpo ⇒ 'b::cpo) ⇒ bool"
where
  "below_monic f ≡ ∀x y. f x ⊑ f y ⟶ x ⊑ y"

abbreviation
  below_monic_cfun :: "('a::cpo → 'b::cpo) ⇒ bool"
where
  "below_monic_cfun f ≡ below_monic (Rep_cfun f)"

lemma below_monicI:
  "(⋀x y. f x ⊑ f y ⟹ x ⊑ y) ⟹ below_monic f"
unfolding below_monic_def by simp

lemma below_monicE:
  "⟦ below_monic f; f x ⊑ f y ⟧ ⟹ x ⊑ y"
unfolding below_monic_def by simp

lemma below_monic_inj:
  "below_monic (f :: 'a::cpo ⇒ 'b::cpo) ⟹ inj f"
by (auto intro!: below_antisym injI elim: below_monicE)

lemma below_monic_indexed:
  assumes "below_monic_cfun f"
  shows "below_monic (λy i. f⋅(y i))"
by (metis (no_types, lifting) assms below_fun_def below_monicE below_monicI)

lemma below_monic_ID [iff]:
  "below_monic_cfun ID"
by (rule below_monicI) simp

lemma below_monic_cfcomp [iff]:
  "below_monic_cfun f ⟹ below_monic_cfun (cfcomp⋅f)"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_K [iff]:
  "below_monic_cfun f ⟹ below_monic_cfun (Λ c _. f⋅c)"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_fun_K [iff]:
  "below_monic_cfun f ⟹ below_monic_cfun (Λ c. (λ_. f⋅c))"
by (rule below_monicI) (auto simp: fun_below_iff dest: below_monicE)

lemma below_monic_cfcomp2 [iff]:
  "⟦ below_monic_cfun f; below_monic_cfun g ⟧ ⟹ below_monic_cfun (f oo g)"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_pair [iff]:
  "⟦ below_monic_cfun f; below_monic_cfun g ⟧ ⟹ below_monic_cfun (Λ x. (f⋅x, g⋅x))"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_pair_split [iff]:
  "⟦ below_monic_cfun f; below_monic_cfun g ⟧ ⟹ below_monic_cfun (Λ x. (f⋅(fst x), g⋅(snd x)))"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_sinl [iff]:
  "below_monic_cfun sinl"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_sinr [iff]:
  "below_monic_cfun sinr"
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)

lemma below_monic_chain_inv:
  fixes f :: "'a::cpo ⇒ 'b::cpo"
  assumes Y: "chain (Y :: nat ⇒ 'b::cpo)"
  assumes Yi: "∀i. ∃y. Y i = f y ∧ P y"
  assumes f: "below_monic f"
  shows "∃Y'. chain Y' ∧ (∀i. Y i = f (Y' i) ∧ P (Y' i))"
proof -
  let ?Y' = "λi. SOME y. Y i = f y ∧ P y"
  have "chain ?Y'"
  proof(rule chainI)
    fix i :: nat
    show "(SOME x. Y i = f x ∧ P x) ⊑ (SOME y. Y (Suc i) = f y ∧ P y)"
      apply -
      using spec[OF Yi, where x=i] spec[OF Yi, where x="Suc i"]
      apply clarsimp
      apply (rule someI2)
       apply blast
      apply (rule someI2)
       apply blast
      apply (rule below_monicE[OF f])
      using chain_mono[OF Y, where i=i and j="Suc i"]
      apply simp
      done
  qed
  moreover
  from Yi have "Y i = f (?Y' i) ∧ P (?Y' i)" for i by (metis (mono_tags, lifting) someI_ex)
  ultimately show ?thesis by blast
qed

lemma adm_below_monic_exists:
  "⟦ adm P; below_monic (f::'a::cpo ⇒ 'b::cpo); cont f ⟧ ⟹ adm (λx. ∃y. x = f y ∧ P y)"
apply (rule admI)
apply (drule below_monic_chain_inv)
apply simp_all
apply (metis (full_types) admD cont2contlubE lub_eq)
done

end