Theory C-restr

theory "C-restr"
imports C "C-Meet" "HOLCF-Utils"
begin

subsubsection {* The demand of a $C$-function *}

text {*
The demand is the least amount of resources required to produce a non-bottom element,
if at all.
*}

definition demand :: "(C → 'a::pcpo) ⇒ C" where
  "demand f = (if f⋅C⇧∞ ≠ ⊥ then C⇗(LEAST n. f⋅C⇗n⇖ ≠ ⊥)⇖ else C⇧∞)"

text {*
Because of continuity, a non-bottom value can always be obtained with finite resources.
*}

lemma finite_resources_suffice:
  assumes "f⋅C⇧∞ ≠ ⊥"
  obtains n where "f⋅C⇗n⇖ ≠ ⊥"
proof-
  {
  assume "∀n. f⋅(C⇗n⇖) = ⊥"
  hence "f⋅C⇧∞ ⊑ ⊥"
    by (auto intro: lub_below[OF ch2ch_Rep_cfunR[OF chain_iterate]]
             simp add: Cinf_def fix_def2 contlub_cfun_arg[OF chain_iterate])
  with assms have False by simp
  }
  thus ?thesis using that by blast
qed

text {*
Because of monotonicity, a non-bottom value can always be obtained with more resources.
*}


lemma more_resources_suffice:
  assumes "f⋅r ≠ ⊥" and "r ⊑ r'"
  shows "f⋅r' ≠ ⊥"
  using assms(1) monofun_cfun_arg[OF assms(2), where  f = f]
  by auto

lemma infinite_resources_suffice:
  shows "f⋅r ≠ ⊥ ⟹ f⋅C⇧∞ ≠ ⊥"
  by (erule more_resources_suffice[OF _ below_Cinf])

lemma demand_suffices:
  assumes "f⋅C⇧∞ ≠ ⊥"
  shows "f⋅(demand f) ≠ ⊥"
  apply (simp add: assms demand_def)
  apply (rule finite_resources_suffice[OF assms])
  apply (rule LeastI)
  apply assumption
  done

lemma not_bot_demand:
  "f⋅r ≠ ⊥ ⟷ demand f ≠ C⇧∞ ∧ demand f ⊑ r"
proof(intro iffI)
  assume "f⋅r ≠ ⊥"
  thus "demand f ≠ C⇧∞ ∧ demand f ⊑ r"
    apply (cases r rule:C_cases)
    apply (auto intro: Least_le simp add: demand_def dest: infinite_resources_suffice)
    done
next
  assume *: "demand f ≠ C⇧∞  ∧ demand f ⊑ r"
  then have "f⋅C⇧∞ ≠ ⊥" by (auto intro: Least_le simp add: demand_def dest: infinite_resources_suffice)
  hence "f⋅(demand f) ≠ ⊥" by (rule demand_suffices)
  moreover from * have "demand f ⊑ r"..
  ultimately
  show "f⋅r ≠ ⊥" by (rule more_resources_suffice)
qed

lemma infinity_bot_demand:
  "f⋅C⇧∞ = ⊥ ⟷ demand f = C⇧∞"
  by (metis below_Cinf not_bot_demand)

lemma demand_suffices':
  assumes "demand f = C⇗n⇖"
  shows "f⋅(demand f) ≠ ⊥"
  by (metis C_eq_Cinf assms demand_suffices infinity_bot_demand)

lemma demand_Suc_Least:
  assumes [simp]: "f⋅⊥ = ⊥"
  assumes "demand f ≠ C⇧∞"
  shows "demand f = C⇗(Suc (LEAST n. f⋅C⇗Suc n⇖ ≠ ⊥))⇖"
proof-
  from assms
  have "demand f = C⇗(LEAST n. f⋅C⇗n⇖ ≠ ⊥)⇖" by (auto simp add: demand_def)
  also
  then obtain n where "f⋅C⇗n⇖ ≠ ⊥" by (metis  demand_suffices')
  hence "(LEAST n. f⋅C⇗n⇖ ≠ ⊥) = Suc (LEAST n. f⋅C⇗Suc n⇖ ≠ ⊥)"
    apply (rule Least_Suc) by simp
  finally show ?thesis.
qed

lemma demand_C_case[simp]: "demand (C_case⋅f) = C ⋅ (demand f)"
proof(cases "demand (C_case⋅f) = C⇧∞")
  case True
  then have "C_case⋅f⋅C⇧∞ = ⊥"
    by (metis infinity_bot_demand)
  with True
  show ?thesis apply auto by (metis infinity_bot_demand)
next
  case False
  hence "demand (C_case⋅f) = C⇗Suc (LEAST n. (C_case⋅f)⋅C⇗Suc n⇖ ≠ ⊥)⇖"
    by (rule demand_Suc_Least[OF C.case_rews(1)])
  also have "… = C⋅C⇗LEAST n. f⋅C⇗n⇖ ≠ ⊥⇖" by simp
  also have "… = C⋅(demand  f)"
    using False unfolding demand_def by auto
  finally show ?thesis.
qed

lemma demand_contravariant:
  assumes "f ⊑ g"
  shows "demand g ⊑ demand f"
proof(cases "demand f" rule:C_cases)
  fix n
  assume "demand f = C⇗n⇖"
  hence "f⋅(demand f) ≠ ⊥" by (metis demand_suffices')
  also note monofun_cfun_fun[OF assms]
  finally have "g⋅(demand f) ≠ ⊥" by this (intro cont2cont)
  thus "demand g ⊑ demand f" unfolding not_bot_demand by auto
qed auto

subsubsection {* Restricting functions with domain C *}

fixrec C_restr :: "C → (C → 'a::pcpo) → (C → 'a)"
  where "C_restr⋅r⋅f⋅r' = (f⋅(r ⊓ r'))" 

abbreviation C_restr_syn :: "(C → 'a::pcpo) ⇒ C ⇒ (C → 'a)" ( "_|⇘_⇙" [111,110] 110)
  where "f|⇘r⇙ ≡ C_restr⋅r⋅f"

lemma [simp]: "⊥|⇘r⇙ = ⊥" by fixrec_simp
lemma [simp]: "f⋅⊥ = ⊥ ⟹ f|⇘⊥⇙ = ⊥"  by fixrec_simp

lemma C_restr_C_restr[simp]: "(v|⇘r'⇙)|⇘r⇙ = v|⇘(r' ⊓ r)⇙"
  by (rule cfun_eqI) simp

lemma C_restr_eqD:
  assumes "f|⇘r⇙ = g|⇘r⇙"
  assumes "r' ⊑ r"
  shows "f⋅r' = g⋅r'"
by (metis C_restr.simps assms below_refl is_meetI)

lemma C_restr_eq_lower:
  assumes "f|⇘r⇙ = g|⇘r⇙"
  assumes "r' ⊑ r"
  shows "f|⇘r'⇙ = g|⇘r'⇙"
by (metis C_restr_C_restr assms below_refl is_meetI)

lemma C_restr_below[intro, simp]:
  "x|⇘r⇙ ⊑ x"
  apply (rule cfun_belowI)
  apply simp
  by (metis below_refl meet_below2 monofun_cfun_arg)
  

lemma C_restr_below_cong:
  "(⋀ r'. r' ⊑ r ⟹ f ⋅ r' ⊑ g ⋅ r') ⟹ f|⇘r⇙ ⊑ g|⇘r⇙"
  apply (rule cfun_belowI)
  apply simp
  by (metis below_refl meet_below1)

lemma C_restr_cong:
  "(⋀ r'. r' ⊑ r ⟹ f ⋅ r' = g ⋅ r') ⟹ f|⇘r⇙ = g|⇘r⇙"
  apply (intro below_antisym C_restr_below_cong )
  by (metis below_refl)+

lemma C_restr_C_cong:
  "(⋀ r'. r' ⊑ r ⟹ f ⋅ (C⋅r') = g ⋅ (C⋅r')) ⟹ f⋅⊥=g⋅⊥ ⟹ f|⇘C⋅r⇙ = g|⇘C⋅r⇙"
  apply (rule C_restr_cong)
  by (case_tac r', auto)

lemma C_restr_C_case[simp]:
  "(C_case⋅f)|⇘C⋅r⇙ = C_case⋅(f|⇘r⇙)"
  apply (rule cfun_eqI)
  apply simp
  apply (case_tac x)
  apply simp
  apply simp
  done

lemma C_restr_bot_demand:
  assumes "C⋅r ⊑ demand f"
  shows "f|⇘r⇙ = ⊥"
proof(rule cfun_eqI)
  fix r'
  have "f⋅(r ⊓ r') = ⊥"
  proof(rule classical)
    have "r ⊑ C ⋅ r" by (rule below_C)
    also
    note assms
    also
    assume *: "f⋅(r ⊓ r') ≠ ⊥"
    hence "demand f ⊑ (r ⊓ r')" unfolding not_bot_demand by auto
    hence "demand f ⊑ r"  by (metis below_refl meet_below1 below_trans)
    finally (below_antisym) have "r = demand f" by this (intro cont2cont)
    with assms
    have "demand f = C⇧∞" by (cases "demand f" rule:C_cases) (auto simp add: iterate_Suc[symmetric] simp del: iterate_Suc)
    thus "f⋅(r ⊓ r') = ⊥" by (metis not_bot_demand)
  qed
  thus "(f|⇘r⇙)⋅r' = ⊥⋅r'" by simp
qed

subsubsection {* Restricting maps of C-ranged functions *}

definition env_C_restr :: "C → ('var::type ⇒ (C → 'a::pcpo)) → ('var ⇒ (C → 'a))" where
  "env_C_restr = (Λ r f.  cfun_comp⋅(C_restr⋅r)⋅f)"

abbreviation env_C_restr_syn :: "('var::type ⇒ (C → 'a::pcpo)) ⇒ C ⇒  ('var ⇒ (C → 'a))" ( "_|⇧∘⇘_⇙" [111,110] 110)
  where "f|⇧∘⇘r⇙ ≡ env_C_restr⋅r⋅f"


lemma env_C_restr_upd[simp]: "(ρ(x := v))|⇧∘⇘r⇙ = (ρ|⇧∘⇘r⇙)(x := v|⇘r⇙)"
  unfolding env_C_restr_def by simp

lemma env_C_restr_lookup[simp]: "(ρ|⇧∘⇘r⇙) v = ρ v|⇘r⇙"
  unfolding env_C_restr_def by simp

lemma env_C_restr_bot[simp]: " ⊥|⇧∘⇘r⇙ = ⊥"
  unfolding env_C_restr_def by auto

lemma env_C_restr_restr_below[intro]: "ρ|⇧∘⇘r⇙ ⊑ ρ"
  by (auto intro: fun_belowI)

lemma env_C_restr_env_C_restr[simp]: "(v|⇧∘⇘r'⇙)|⇧∘⇘r⇙ = v|⇧∘⇘(r' ⊓ r)⇙"
  unfolding env_C_restr_def by auto

lemma env_C_restr_cong:
  "(⋀ x r'. r' ⊑ r ⟹ f x ⋅ r' = g x ⋅ r') ⟹ f|⇧∘⇘r⇙ = g|⇧∘⇘r⇙"
  unfolding env_C_restr_def
  by (rule ext) (auto intro: C_restr_cong)

end