Theory ArityAnalysisSpec

theory ArityAnalysisSpec
imports ArityAnalysisAbinds
begin

locale SubstArityAnalysis = EdomArityAnalysis + 
  assumes Aexp_subst_restr: "x ∉ S ⟹ y ∉ S ⟹ (Aexp e[x::=y] ⋅ a) f|` S = (Aexp e⋅a) f|` S"

locale ArityAnalysisSafe = SubstArityAnalysis +
  assumes Aexp_Var: "up ⋅ n ⊑ (Aexp (Var x)⋅n) x"
  assumes Aexp_App: "Aexp e ⋅(inc⋅n) ⊔ esing x ⋅ (up⋅0) ⊑  Aexp (App e x) ⋅ n"
  assumes Aexp_Lam: "env_delete y (Aexp e ⋅(pred⋅n)) ⊑ Aexp (Lam [y]. e) ⋅ n"
  assumes Aexp_IfThenElse: "Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a ⊑ Aexp (scrut ? e1 : e2)⋅a"

locale ArityAnalysisHeapSafe = ArityAnalysisSafe + ArityAnalysisHeapEqvt +
  assumes edom_Aheap: "edom (Aheap Γ e⋅ a) ⊆ domA Γ"
  assumes Aheap_subst: "x ∉ domA Γ ⟹ y ∉ domA Γ ⟹ Aheap Γ[x::h=y] e[x ::=y]  = Aheap Γ e"

locale ArityAnalysisLetSafe = ArityAnalysisHeapSafe +
  assumes Aexp_Let: "ABinds Γ⋅(Aheap Γ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a"

locale ArityAnalysisLetSafeNoCard = ArityAnalysisLetSafe +
  assumes Aheap_heap3: "x ∈ thunks Γ ⟹ (Aheap Γ e⋅a) x = up⋅0"

context SubstArityAnalysis
begin
  lemma Aexp_subst_upd: "(Aexp e[y::=x]⋅n) ⊑ (Aexp e⋅n)(y := ⊥, x := up⋅0)"
  proof-
    have "Aexp e[y::=x]⋅n f|`(-{x,y}) = Aexp e⋅n f|` (-{x,y})" by (rule Aexp_subst_restr) auto
  
    show ?thesis
    proof (rule fun_belowI)
    fix x'
      have "x' = x ∨ x' = y ∨ x' ∈ (-{x,y})" by auto
      thus "(Aexp e[y::=x]⋅n) x' ⊑ ((Aexp e⋅n)(y := ⊥, x := up⋅0)) x'"
      proof(elim disjE)
        assume "x' ∈ (-{x,y})"
        moreover
        have "Aexp e[y::=x]⋅n f|`(-{x,y}) = Aexp e⋅n f|` (-{x,y})" by (rule Aexp_subst_restr) auto
        note fun_cong[OF this, where x = x']
        ultimately
        show ?thesis by auto
      next
        assume "x' = x"
        thus ?thesis by simp
      next
        assume "x' = y"
        thus ?thesis
        using [[simp_trace]]
        by simp
     qed
   qed
  qed

  lemma Aexp_subst: "Aexp (e[y::=x])⋅a ⊑ env_delete y ((Aexp e)⋅a) ⊔ esing x⋅(up⋅0)"
    apply (rule below_trans[OF Aexp_subst_upd])
    apply (rule fun_belowI)
    apply auto
    done
end

context ArityAnalysisSafe
begin

lemma Aexp_Var_singleton: "esing x ⋅ (up⋅n) ⊑ Aexp (Var x) ⋅ n"
  by (simp add: Aexp_Var)

lemma fup_Aexp_Var: "esing x ⋅ n ⊑ fup⋅(Aexp (Var x))⋅n"
  by (cases n) (simp_all add: Aexp_Var)
end


context ArityAnalysisLetSafe
begin
  lemma Aheap_nonrec:
    assumes "nonrec Δ"
    shows "Aexp e⋅a f|` domA Δ ⊑ Aheap Δ e⋅a"
  proof-
    have "ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a" by (rule Aexp_Let)
    note env_restr_mono[where S = "domA Δ", OF this]
    moreover
    from assms
    have "ABinds Δ⋅(Aheap Δ e⋅a) f|` domA Δ = ⊥"
      by (rule nonrecE) (auto simp add: fv_def fresh_def dest!: subsetD[OF fup_Aexp_edom])
    moreover
    have "Aheap Δ e⋅a f|` domA Δ = Aheap Δ e⋅a" 
      by (rule env_restr_useless[OF edom_Aheap])
    moreover
    have "(Aexp (Let Δ e)⋅a) f|` domA Δ = ⊥" 
      by (auto dest!: subsetD[OF Aexp_edom])
    ultimately
    show "Aexp e⋅a f|` domA Δ ⊑ Aheap Δ e⋅a"
      by (simp add: env_restr_join)
  qed
end


end