Theory ResourcedAdequacy

theory ResourcedAdequacy
imports "ResourcedDenotational" "Launchbury" "AList-Utils" "CorrectnessResourced"
begin

lemma demand_not_0: "demand (𝒩⟦e⟧⇘ρ⇙) ≠ ⊥"
proof
  assume "demand (𝒩⟦e⟧⇘ρ⇙) = ⊥"
  with demand_suffices'[where n = 0, simplified, OF this]
  have "(𝒩⟦e⟧⇘ρ⇙)⋅⊥ ≠ ⊥" by simp
  thus False by simp
qed

text {*
The semantics of an expression, given only @{term r} resources, will only use values from the
environment with less resources.
*}

lemma restr_can_restrict_env: "(𝒩⟦ e ⟧⇘ρ⇙)|⇘C⋅r⇙ = (𝒩⟦ e ⟧⇘ρ|⇧∘⇘r⇙⇙)|⇘C⋅r⇙"
proof(induction e arbitrary: ρ r rule: exp_induct)
  case (Var x)
  show ?case
  proof (rule C_restr_C_cong)
    fix r'
    assume "r' ⊑ r"
    have "(𝒩⟦ Var x ⟧⇘ρ⇙)⋅(C⋅r') = ρ x⋅r'" by simp
    also have "… = ((ρ x)|⇘r⇙)⋅r'" using `r' ⊑ r` by simp
    also have "… =  (𝒩⟦ Var x ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')" by simp
    finally show "(𝒩⟦ Var x ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ Var x ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')".
  qed simp
next
  case (Lam x e)
  show ?case
  proof(rule C_restr_C_cong)
    fix r'
    assume "r' ⊑ r"
    hence "r' ⊑ C⋅r" by (metis below_C below_trans)
    {
      fix v
      have "ρ(x := v)|⇧∘⇘r⇙ = (ρ|⇧∘⇘r⇙)(x := v)|⇧∘⇘r⇙"
        by simp
      hence "(𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r'⇙ = (𝒩⟦ e ⟧⇘(ρ|⇧∘⇘r⇙)(x := v)⇙)|⇘r'⇙"
        by  (subst (1 2) C_restr_eq_lower[OF Lam `r' ⊑ C⋅r` ]) simp
    }
    thus "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ Lam [x]. e ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')"
      by simp
  qed simp
next
  case (App e x)
  show ?case
  proof (rule C_restr_C_cong)
    fix r'
    assume "r' ⊑ r"
    hence "r' ⊑ C⋅r" by (metis below_C below_trans)
    hence "(𝒩⟦ e ⟧⇘ρ⇙)⋅r' = (𝒩⟦ e ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅r'"
        by (rule C_restr_eqD[OF App])
    thus "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ App e x ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')"
      using `r' ⊑ r` by simp
  qed simp
next
  case (Bool b)
  show ?case by simp
next
  case (IfThenElse scrut e⇩1 e⇩2)
  show ?case
  proof (rule C_restr_C_cong)
    fix r'
    assume "r' ⊑ r"
    hence "r' ⊑ C⋅r" by (metis below_C below_trans)

    have "(𝒩⟦ scrut ⟧⇘ρ⇙)⋅r' = (𝒩⟦ scrut ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅r'"
      using `r' ⊑ C⋅r` by (rule C_restr_eqD[OF IfThenElse(1)])
    moreover
    have "(𝒩⟦ e⇩1 ⟧⇘ρ⇙)⋅r' = (𝒩⟦ e⇩1 ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅r'"
      using `r' ⊑ C⋅r` by (rule C_restr_eqD[OF IfThenElse(2)])
    moreover
    have "(𝒩⟦ e⇩2 ⟧⇘ρ⇙)⋅r' = (𝒩⟦ e⇩2 ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅r'"
      using `r' ⊑ C⋅r` by (rule C_restr_eqD[OF IfThenElse(3)])
    ultimately
    show "(𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')"
      using `r' ⊑ r` by simp
  qed simp
next
  case (Let Γ e)

  txt {* The lemma, lifted to heaps *}
  have restr_can_restrict_env_heap : "⋀ r. (𝒩⦃Γ⦄ρ)|⇧∘⇘r⇙ = (𝒩⦃Γ⦄ρ|⇧∘⇘r⇙)|⇧∘⇘r⇙"
  proof(rule has_ESem.parallel_HSem_ind)
    fix ρ⇩1 ρ⇩2 :: CEnv and r :: C
    assume "ρ⇩1|⇧∘⇘r⇙ = ρ⇩2|⇧∘⇘r⇙"

    show " (ρ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩1⇙)|⇧∘⇘r⇙ = (ρ|⇧∘⇘r⇙ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩2⇙)|⇧∘⇘r⇙"
    proof(rule env_C_restr_cong)
      fix x and r'
      assume "r' ⊑ r"
      hence "r' ⊑ C⋅r" by (metis below_C below_trans)

      show "(ρ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩1⇙) x⋅r' = (ρ|⇧∘⇘r⇙ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩2⇙) x⋅r'"
      proof(cases "x ∈ domA Γ")
        case True
        have "(𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩1⇙)⋅r' = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩1|⇧∘⇘r⇙⇙)⋅r'"
         by (rule C_restr_eqD[OF Let(1)[OF True] `r' ⊑ C⋅r`])
        also have "… = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩2|⇧∘⇘r⇙⇙)⋅r'"
          unfolding `ρ⇩1|⇧∘⇘r⇙ = ρ⇩2|⇧∘⇘r⇙`..
        also have "…   = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩2⇙)⋅r'"
          by (rule C_restr_eqD[OF Let(1)[OF True] `r' ⊑ C⋅r`, symmetric])
        finally
        show ?thesis using True by (simp add: lookupEvalHeap)
      next
        case False
        with `r' ⊑ r`
        show ?thesis by simp
      qed
    qed
  qed simp_all

  show ?case
  proof (rule C_restr_C_cong)
    fix r'
    assume "r' ⊑ r"
    hence "r' ⊑ C⋅r" by (metis below_C below_trans)

    have "(𝒩⦃Γ⦄ρ)|⇧∘⇘r⇙ = (𝒩⦃Γ⦄(ρ|⇧∘⇘r⇙))|⇧∘⇘r⇙"
      by (rule restr_can_restrict_env_heap)
    hence "(𝒩⟦ e ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r' = (𝒩⟦ e ⟧⇘𝒩⦃Γ⦄ρ|⇧∘⇘r⇙⇙)⋅r'"
      by (subst (1 2) C_restr_eqD[OF Let(2) `r' ⊑ C⋅r`]) simp

    thus "(𝒩⟦ Let Γ e ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ Let Γ e ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r')"
      using `r' ⊑ r` by simp
  qed simp
qed

lemma can_restrict_env:
  "(𝒩⟦e⟧⇘ρ⇙)⋅(C⋅r) = (𝒩⟦ e ⟧⇘ρ|⇧∘⇘r⇙⇙)⋅(C⋅r)"
  by (rule C_restr_eqD[OF restr_can_restrict_env below_refl])

text {*
When an expression @{term e} terminates, then we can remove such an expression from the heap and it
still terminates. This is the crucial trick to handle black-holing in the resourced semantics.
*}

lemma add_BH:
  assumes "map_of Γ x = Some e"
  assumes  "(𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅r' ≠ ⊥"
  shows "(𝒩⟦e⟧⇘𝒩⦃delete x Γ⦄⇙)⋅r' ≠ ⊥"
proof-
  obtain r where r: "C⋅r = demand (𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)"
    using demand_not_0 by (cases "demand (𝒩⟦ e ⟧⇘𝒩⦃Γ⦄⇙)") auto

  from  assms(2)
  have "C⋅r ⊑ r'" unfolding r not_bot_demand by simp

  from assms(1)
  have [simp]: "the (map_of Γ x) = e" by (metis option.sel)

  from assms(1)
  have [simp]: "x ∈ domA Γ" by (metis domIff dom_map_of_conv_domA not_Some_eq)

  def ub ≡ "𝒩⦃Γ⦄" -- "An upper bound for the induction"

  have heaps: "(𝒩⦃Γ⦄)|⇧∘⇘r⇙ ⊑ 𝒩⦃delete x Γ⦄" and "𝒩⦃Γ⦄ ⊑ ub"
  proof (induction rule: HSem_bot_ind) 
    fix ρ
    assume "ρ|⇧∘⇘r⇙ ⊑ 𝒩⦃delete x Γ⦄"
    assume "ρ ⊑ ub"

    show "(❙𝒩⟦ Γ ❙⟧⇘ρ⇙)|⇧∘⇘r⇙ ⊑ 𝒩⦃delete x Γ⦄"
    proof (rule fun_belowI)
      fix y
      show "((❙𝒩⟦ Γ ❙⟧⇘ρ⇙)|⇧∘⇘r⇙) y ⊑ (𝒩⦃delete x Γ⦄) y"
      proof (cases "y = x")
        case True
        have "((❙𝒩⟦ Γ ❙⟧⇘ρ⇙)|⇧∘⇘r⇙) x = (𝒩⟦ e ⟧⇘ρ⇙)|⇘r⇙"
          by (simp add: lookupEvalHeap)
        also have "… ⊑ (𝒩⟦ e ⟧⇘ub⇙)|⇘r⇙"
          using `ρ ⊑ ub` by (intro monofun_cfun_arg)
        also have "… = (𝒩⟦ e ⟧⇘𝒩⦃Γ⦄⇙)|⇘r⇙"
          unfolding ub_def..
        also have "… = ⊥"
          using r by (rule  C_restr_bot_demand[OF eq_imp_below])
        also have "… = (𝒩⦃delete x Γ⦄) x"
          by (simp add: lookup_HSem_other)
        finally
        show ?thesis unfolding True.
      next
        case False
        show ?thesis
        proof (cases "y ∈ domA Γ")
          case True
          have "(𝒩⟦ the (map_of Γ y) ⟧⇘ρ⇙)|⇘r⇙ = (𝒩⟦ the (map_of Γ y) ⟧⇘ρ|⇧∘⇘r⇙⇙)|⇘r⇙"
            by (rule C_restr_eq_lower[OF restr_can_restrict_env below_C])
          also have "… ⊑ 𝒩⟦ the (map_of Γ y) ⟧⇘ρ|⇧∘⇘r⇙⇙"
            by (rule C_restr_below)
          also note `ρ|⇧∘⇘r⇙ ⊑ 𝒩⦃delete x Γ⦄`
          finally
          show ?thesis
            using `y ∈ domA Γ` `y ≠ x`
            by (simp add: lookupEvalHeap lookup_HSem_heap)
        next
          case False
          thus ?thesis by simp
        qed
      qed
    qed

    from `ρ ⊑ ub`
    have "(❙𝒩⟦ Γ ❙⟧⇘ρ⇙) ⊑ (❙𝒩⟦ Γ ❙⟧⇘ub⇙)" 
      by (rule cont2monofunE[rotated]) simp
    also have "… = ub"
      unfolding ub_def HSem_bot_eq[symmetric]..
    finally     
    show "(❙𝒩⟦ Γ ❙⟧⇘ρ⇙) ⊑ ub".
  qed simp_all

  from assms(2)
  have "(𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅(C⋅r) ≠ ⊥"
    unfolding r
    by (rule demand_suffices[OF infinite_resources_suffice])
  also
  have "(𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅(C⋅r) = (𝒩⟦e⟧⇘(𝒩⦃Γ⦄)|⇧∘⇘r⇙⇙)⋅(C⋅r)"
    by (rule can_restrict_env)
  also
  have "… ⊑ (𝒩⟦e⟧⇘𝒩⦃delete x Γ⦄⇙)⋅(C⋅r)"
    by (intro monofun_cfun_arg monofun_cfun_fun heaps )
  also
  have "… ⊑ (𝒩⟦e⟧⇘𝒩⦃delete x Γ⦄⇙)⋅r'"
    using `C⋅r ⊑ r'` by (rule monofun_cfun_arg)
  finally
  show ?thesis by this (intro cont2cont)+
qed

text {*
The semantics is continuous, so we can apply induction here:
*}

lemma resourced_adequacy:
  assumes "(𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅r ≠ ⊥"
  shows "∃ Δ v. Γ : e ⇓⇘S⇙ Δ : v"
using assms
proof(induction r arbitrary: Γ e S rule: C.induct[case_names adm bot step])
  case adm show ?case by simp
next
  case bot
  hence False by auto
  thus ?case..
next
  case (step r)
  show ?case
  proof(cases e rule:exp_strong_exhaust(1)[where c = "(Γ,S)", case_names Var App Let Lam Bool IfThenElse])
  case (Var x)
    let ?e = "the (map_of Γ x)"
    from step.prems[unfolded Var]
    have "x ∈ domA Γ" 
      by (auto intro: ccontr simp add: lookup_HSem_other)
    hence "map_of Γ x = Some ?e" by (rule domA_map_of_Some_the)
    moreover
    from step.prems[unfolded Var] `map_of Γ x = Some ?e` `x ∈ domA Γ`
    have "(𝒩⟦?e⟧⇘𝒩⦃Γ⦄⇙)⋅r ≠ ⊥" by (auto simp add: lookup_HSem_heap  simp del: app_strict)
    hence "(𝒩⟦?e⟧⇘𝒩⦃delete x Γ⦄⇙)⋅r ≠ ⊥" by (rule add_BH[OF `map_of Γ x = Some ?e`])
    from step.IH[OF this]
    obtain Δ v where "delete x Γ : ?e ⇓⇘x # S⇙ Δ : v" by blast
    ultimately
    have "Γ : (Var x) ⇓⇘S⇙ (x,v) #  Δ : v" by (rule Variable)
    thus ?thesis using Var by auto
  next
  case (App e' x)
    have "finite (set S ∪ fv (Γ, e'))" by simp
    from finite_list[OF this]
    obtain S' where S': "set S' = set S ∪ fv (Γ, e')"..

    from step.prems[unfolded App]
    have prem: "((𝒩⟦ e' ⟧⇘𝒩⦃Γ⦄⇙)⋅r ↓CFn (𝒩⦃Γ⦄) x|⇘r⇙)⋅r ≠ ⊥" by (auto simp del: app_strict)
    hence "(𝒩⟦e'⟧⇘𝒩⦃Γ⦄⇙)⋅r ≠ ⊥" by auto
    from step.IH[OF this]
    obtain Δ v where lhs': "Γ : e' ⇓⇘S'⇙ Δ : v" by blast 

    have "fv (Γ, e') ⊆ set S'" using S' by auto
    from correctness_empty_env[OF lhs' this]
    have correct1: "𝒩⟦e'⟧⇘𝒩⦃Γ⦄⇙ ⊑ 𝒩⟦v⟧⇘𝒩⦃Δ⦄⇙" and "𝒩⦃Γ⦄ ⊑ 𝒩⦃Δ⦄" by auto

    from prem
    have "((𝒩⟦ v ⟧⇘𝒩⦃Δ⦄⇙)⋅r ↓CFn (𝒩⦃Γ⦄) x|⇘r⇙)⋅r ≠ ⊥"
      by (rule not_bot_below_trans)(intro correct1 monofun_cfun_fun  monofun_cfun_arg)
    with result_evaluated[OF lhs']
    have "isLam v" by (cases r, auto, cases v rule: isVal.cases, auto)
    then obtain y e'' where n': "v = (Lam [y]. e'')" by (rule isLam_obtain_fresh)
    with lhs'
    have lhs: "Γ : e' ⇓⇘S'⇙ Δ : Lam [y]. e''" by simp

    have "((𝒩⟦ v ⟧⇘𝒩⦃Δ⦄⇙)⋅r ↓CFn (𝒩⦃Γ⦄) x|⇘r⇙)⋅r ≠ ⊥" by fact
    also have "(𝒩⦃Γ⦄) x|⇘r⇙ ⊑ (𝒩⦃Γ⦄) x" by (rule C_restr_below)
    also note `v = _`
    also note `(𝒩⦃Γ⦄) ⊑ (𝒩⦃Δ⦄)`
    also have "(𝒩⟦ Lam [y]. e'' ⟧⇘𝒩⦃Δ⦄⇙)⋅r ⊑ CFn⋅(Λ v. 𝒩⟦e''⟧⇘(𝒩⦃Δ⦄)(y := v)⇙)"
      by (rule CELam_no_restr)
    also have "(… ↓CFn (𝒩⦃Δ⦄) x)⋅r = (𝒩⟦e''⟧⇘(𝒩⦃Δ⦄)(y := ((𝒩⦃Δ⦄) x))⇙)⋅r" by simp
    also have "… = (𝒩⟦e''[y::=x]⟧⇘𝒩⦃Δ⦄⇙)⋅r"
      unfolding ESem_subst..
    finally
    have "… ≠ ⊥" by this (intro cont2cont cont_fun)+
    then
    obtain Θ v' where rhs: "Δ : e''[y::=x] ⇓⇘S'⇙ Θ : v'" using step.IH by blast

    have "Γ : App e' x ⇓⇘S'⇙ Θ : v'"
      by (rule reds_ApplicationI[OF lhs rhs])
    hence "Γ : App e' x ⇓⇘S⇙ Θ : v'"
      apply (rule reds_smaller_L) using S' by auto
    thus ?thesis using App by auto
  next
  case (Lam v e')
    have "Γ : Lam [v]. e' ⇓⇘S⇙ Γ : Lam [v]. e'" ..
    thus ?thesis using Lam by blast
  next
  case (Bool b)
    have "Γ : Bool b ⇓⇘S⇙ Γ : Bool b" by rule
    thus ?thesis using Bool by blast
  next
  case (IfThenElse scrut e⇩1 e⇩2)

    from step.prems[unfolded IfThenElse]
    have prem: "CB_project⋅((𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘𝒩⦃Γ⦄⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘𝒩⦃Γ⦄⇙)⋅r) ≠ ⊥" by (auto simp del: app_strict)
    then obtain b where
      is_CB: "(𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄⇙)⋅r = CB⋅(Discr b)"
      and not_bot2: "((𝒩⟦ (if b then e⇩1 else e⇩2) ⟧⇘𝒩⦃Γ⦄⇙)⋅r) ≠ ⊥"
    unfolding CB_project_not_bot by (auto split: if_splits)

    have "finite (set S ∪ fv (Γ, scrut))" by simp
    from finite_list[OF this]
    obtain S' where S': "set S' = set S ∪ fv (Γ, scrut)"..


    from is_CB have "(𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄⇙)⋅r ≠ ⊥" by simp
    from step.IH[OF this]
    obtain Δ v where lhs': "Γ : scrut ⇓⇘S'⇙ Δ : v" by blast
    then have "isVal v" by (rule result_evaluated)

    have "fv (Γ, scrut) ⊆ set S'" using S' by simp
    from correctness_empty_env[OF lhs' this]
    have correct1: "𝒩⟦scrut⟧⇘𝒩⦃Γ⦄⇙ ⊑ 𝒩⟦v⟧⇘𝒩⦃Δ⦄⇙" and correct2: "𝒩⦃Γ⦄ ⊑ 𝒩⦃Δ⦄" by auto

    from correct1
    have "(𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄⇙)⋅r ⊑ (𝒩⟦ v ⟧⇘𝒩⦃Δ⦄⇙)⋅r" by (rule monofun_cfun_fun)
    with is_CB
    have "(𝒩⟦ v ⟧⇘𝒩⦃Δ⦄⇙)⋅r = CB⋅(Discr b)" by simp
    with `isVal v`
    have "v = Bool b" by (cases v rule: isVal.cases) (case_tac r, auto)+

    from not_bot2 `𝒩⦃Γ⦄ ⊑ 𝒩⦃Δ⦄`
    have "(𝒩⟦ (if b then e⇩1 else e⇩2) ⟧⇘𝒩⦃Δ⦄⇙)⋅r ≠ ⊥"
      by (rule not_bot_below_trans[OF _ monofun_cfun_fun[OF monofun_cfun_arg]])
    from step.IH[OF this]
    obtain Θ v' where rhs: "Δ : (if b then e⇩1 else e⇩2) ⇓⇘S'⇙ Θ : v'" by blast

    from lhs'[unfolded `v = _`] rhs
    have "Γ : (scrut ? e⇩1 : e⇩2) ⇓⇘S'⇙ Θ : v'" by rule
    hence "Γ : (scrut ? e⇩1 : e⇩2) ⇓⇘S⇙ Θ : v'"
      apply (rule reds_smaller_L) using S' by auto
    thus ?thesis unfolding IfThenElse by blast
  next
  case (Let Δ e')
    from step.prems[unfolded Let(2)]
    have prem: "(𝒩⟦e'⟧⇘𝒩⦃Δ⦄𝒩⦃Γ⦄⇙)⋅r ≠ ⊥" 
      by (simp  del: app_strict)
    also
      have "atom ` domA Δ ♯* Γ" using Let(1) by (simp add: fresh_star_Pair)
      hence "𝒩⦃Δ⦄𝒩⦃Γ⦄ = 𝒩⦃Δ @ Γ⦄" by (rule HSem_merge)
    finally 
    have "(𝒩⟦e'⟧⇘𝒩⦃Δ @ Γ⦄⇙)⋅r ≠ ⊥".
    then
    obtain Θ v where "Δ @ Γ : e' ⇓⇘S⇙ Θ : v" using step.IH by blast
    hence "Γ : Let Δ e' ⇓⇘S⇙ Θ : v"
      by (rule reds.Let[OF Let(1)])
    thus ?thesis using Let by auto
  qed
qed

end