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⇩₁ e⇩₂)
  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⇩₁ ⟧⇘ρ⇙)⋅r' = (𝒩⟦ e⇩₁ ⟧⇘ρ|⇧^∘⇘r⇙⇙)⋅r'"
      using ‹r' ⊑ C⋅r› by (rule C_restr_eqD[OF IfThenElse(2)])
    moreover
    have "(𝒩⟦ e⇩₂ ⟧⇘ρ⇙)⋅r' = (𝒩⟦ e⇩₂ ⟧⇘ρ|⇧^∘⇘r⇙⇙)⋅r'"
      using ‹r' ⊑ C⋅r› by (rule C_restr_eqD[OF IfThenElse(3)])
    ultimately
    show "(𝒩⟦ (scrut ? e⇩₁ : e⇩₂) ⟧⇘ρ⇙)⋅(C⋅r') = (𝒩⟦ (scrut ? e⇩₁ : e⇩₂) ⟧⇘ρ|⇧^∘⇘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 ρ⇩₁ ρ⇩₂ :: CEnv and r :: C
    assume "ρ⇩₁|⇧^∘⇘r⇙ = ρ⇩₂|⇧^∘⇘r⇙"

    show " (ρ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩₁⇙)|⇧^∘⇘r⇙ = (ρ|⇧^∘⇘r⇙ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩₂⇙)|⇧^∘⇘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 Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩₁⇙) x⋅r' = (ρ|⇧^∘⇘r⇙ ++⇘domA Γ⇙ ❙𝒩⟦ Γ ❙⟧⇘ρ⇩₂⇙) x⋅r'"
      proof(cases "x ∈ domA Γ")
        case True
        have "(𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩₁⇙)⋅r' = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩₁|⇧^∘⇘r⇙⇙)⋅r'"
         by (rule C_restr_eqD[OF Let(1)[OF True] ‹r' ⊑ C⋅r›])
        also have "… = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩₂|⇧^∘⇘r⇙⇙)⋅r'"
          unfolding ‹ρ⇩₁|⇧^∘⇘r⇙ = ρ⇩₂|⇧^∘⇘r⇙›..
        also have "…   = (𝒩⟦ the (map_of Γ x) ⟧⇘ρ⇩₂⇙)⋅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)

  define ub where "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⇩₁ e⇩₂)

    from step.prems[unfolded IfThenElse]
    have prem: "CB_project⋅((𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄⇙)⋅r)⋅((𝒩⟦ e⇩₁ ⟧⇘𝒩⦃Γ⦄⇙)⋅r)⋅((𝒩⟦ e⇩₂ ⟧⇘𝒩⦃Γ⦄⇙)⋅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⇩₁ else e⇩₂) ⟧⇘𝒩⦃Γ⦄⇙)⋅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⇩₁ else e⇩₂) ⟧⇘𝒩⦃Δ⦄⇙)⋅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⇩₁ else e⇩₂) ⇓⇘S'⇙ Θ : v'" by blast

    from lhs'[unfolded ‹v = _›] rhs
    have "Γ : (scrut ? e⇩₁ : e⇩₂) ⇓⇘S'⇙ Θ : v'" by rule
    hence "Γ : (scrut ? e⇩₁ : e⇩₂) ⇓⇘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