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

subsubsection ‹The demand of a $C$-function›

text ‹
  demand is the least amount of resources required to produce a non-bottom element,
  at all.
 ›

definition demand :: "(C → 'a::pcpo) → C" where
  "demand f = (if f⋅C^\<infinity> ≠ ⊥ then C^{LEAST n. f⋅C ≠ ⊥)} else C^\<infinity>)"

text ‹
  of continuity, a non-bottom value can always be obtained with finite resources.
 ›

lemma finite_resources_suffice:
  assumes "f⋅C^\<infinity> ≠ ⊥"
  obtains n where "f⋅C ≠ ⊥"
proof-
  {
  assume "∀n. f⋅(C) = ⊥"
  hence "f⋅C^\<infinity> ⊑ ⊥"
    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 ‹
  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^\<infinity> ≠ ⊥"
  by (erule more_resources_suffice[OF _ below_Cinf])

lemma demand_suffices:
  assumes "f⋅C^\<infinity> ≠ ⊥"
  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^\<infinity> ∧ demand f ⊑ r"
proof(intro iffI)
  assume "f⋅r ≠ ⊥"
  thus "demand f ≠ C^\<infinity> ∧ 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^\<infinity> ∧ demand f ⊑ r"
  then have "f⋅C^\<infinity> ≠ ⊥" 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^\<infinity> = ⊥ ⟷ demand f = C^\<infinity>"
  by (metis below_Cinf not_bot_demand)

lemma demand_suffices':
  assumes "demand f = C"
  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^\<infinity>"
  shows "demand f = C^{Suc (LEAST n. f⋅C n ≠ ⊥))}"
proof-
  from assms
  have "demand f = C^{LEAST n. f⋅C ≠ ⊥)}" by (auto simp add: demand_def)
  also
  then obtain n where "f⋅C ≠ ⊥" by (metis  demand_suffices')
  hence "(LEAST n. f⋅C ≠ ⊥) = Suc (LEAST n. f⋅C ⁿ ≠ ⊥)"
    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^\<infinity>")
  case True
  then have "C_case⋅f⋅C^\<infinity> = ⊥"
    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 ^{(LEAST n. (C_case⋅f)⋅C n ≠ ⊥)}"
    by (rule demand_Suc_Least[OF C.case_rews(1)])
  also have "… = C⋅C ^{n. f⋅C ≠ ⊥}" 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"
  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| ≡ C_restr⋅r⋅f"

lemma [simp]: "⊥| = ⊥" by fixrec_simp
lemma [simp]: "f⋅⊥ = ⊥ ==> f|_<bottom> = ⊥"  by fixrec_simp

lemma C_restr_C_restr[simp]: "(v|_')| = v|_{r' ⊓ r)}"
  by (rule cfun_eqI) simp

lemma C_restr_eqD:
  assumes "f| = g|"
  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| = g|"
  assumes "r' ⊑ r"
  shows "f|_' = g|_'"
by (metis C_restr_C_restr assms below_refl is_meetI)

lemma C_restr_below[intro, simp]:
  "x| ⊑ 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| ⊑ g|"
  apply (rule cfun_belowI)
  apply simp
  by (metis below_refl meet_below1)

lemma C_restr_cong:
  "(∧ r'. r' ⊑ r ==> f ⋅ r' = g ⋅ r') ==> f| = g|"
  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|_⋅r = g|_⋅r"
  apply (rule C_restr_cong)
  by (case_tac r', auto)

lemma C_restr_C_case[simp]:
  "(C_case⋅f)|_⋅r = C_case⋅(f|)"
  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| = ⊥"
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^\<infinity>" 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'" 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|^\<circ> ≡ env_C_restr⋅r⋅f"


lemma env_C_restr_upd[simp]: "(ρ(x := v))|^\<circ> = (ρ|^\<circ>)(x := v|)"
  unfolding env_C_restr_def by simp

lemma env_C_restr_lookup[simp]: "(ρ|^\<circ>) v = ρ v|"
  unfolding env_C_restr_def by simp

lemma env_C_restr_bot[simp]: " ⊥|^\<circ> = ⊥"
  unfolding env_C_restr_def by auto

lemma env_C_restr_restr_below[intro]: "ρ|^\<circ> ⊑ ρ"
  by (auto intro: fun_belowI)

lemma env_C_restr_env_C_restr[simp]: "(v|^\<circ>_')|^\<circ> = v|^\<circ>_{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|^\<circ> = g|^\<circ>"
  unfolding env_C_restr_def
  by (rule ext) (auto intro: C_restr_cong)

end