Theory TrivialArityAnal

theory TrivialArityAnal
imports ArityAnalysisSpec "Launchbury.Env-Nominal"
begin

definition Trivial_Aexp :: "exp ⇒ Arity → AEnv"
  where "Trivial_Aexp e = (Λ n. (λ x. up⋅0) f|` fv e)"

lemma Trivial_Aexp_simp: "Trivial_Aexp e ⋅ n = (λ x. up⋅0) f|` fv e"
  unfolding Trivial_Aexp_def by simp

lemma edom_Trivial_Aexp[simp]: "edom (Trivial_Aexp e ⋅ n) = fv e"
  by (auto simp add: edom_def env_restr_def Trivial_Aexp_def) 

lemma Trivial_Aexp_eq[iff]: "Trivial_Aexp e ⋅ n = Trivial_Aexp e' ⋅ n' ⟷ fv e = (fv e' :: var set)"
  apply (auto simp add: Trivial_Aexp_simp env_restr_def)
  apply (metis up_defined)+
  done
  
lemma below_Trivial_Aexp[simp]: "(ae ⊑ Trivial_Aexp e ⋅ n) ⟷ edom ae ⊆ fv e"
  by (auto dest:fun_belowD intro!: fun_belowI  simp add: Trivial_Aexp_def env_restr_def edom_def split:if_splits)


interpretation ArityAnalysis Trivial_Aexp.
interpretation EdomArityAnalysis Trivial_Aexp
  by standard simp


interpretation ArityAnalysisSafe Trivial_Aexp
proof
(*
  fix π
  show "π ∙ Trivial_Aexp = Trivial_Aexp" by perm_simp rule
next
*)
  fix n x
  show "up⋅n ⊑ (Trivial_Aexp (Var x)⋅n) x"
    by (simp add: Trivial_Aexp_simp)
next
  fix e x n
  show "Trivial_Aexp e⋅(inc⋅n) ⊔ esing x⋅(up⋅0) ⊑ Trivial_Aexp (App e x)⋅n"
    by (auto intro: fun_belowI simp add: Trivial_Aexp_def env_restr_def )
next
  fix y e n
  show "env_delete y (Trivial_Aexp e⋅(pred⋅n)) ⊑ Trivial_Aexp (Lam [y]. e)⋅n"
    by (auto simp add: Trivial_Aexp_simp env_delete_restr Diff_eq inf_commute)
next
  fix x y :: var and S e a
  assume "x ∉ S" and "y ∉ S"
  thus "Trivial_Aexp e[x::=y]⋅a f|` S = Trivial_Aexp e⋅a f|` S"
    by (auto simp add: Trivial_Aexp_simp fv_subst_eq intro!: arg_cong[where f = "λ S. env_restr S e" for e])
next
  fix scrut e1 a e2
  show "Trivial_Aexp scrut⋅0 ⊔ Trivial_Aexp e1⋅a ⊔ Trivial_Aexp e2⋅a ⊑ Trivial_Aexp (scrut ? e1 : e2)⋅a"
    by (auto intro: env_restr_mono2 simp add: Trivial_Aexp_simp join_below_iff )
qed

definition Trivial_Aheap :: "heap ⇒ exp ⇒ Arity → AEnv" where
  "Trivial_Aheap Γ e = (Λ a. (λ x. up⋅0) f|` domA Γ)"

lemma Trivial_Aheap_eqvt[eqvt]: "π ∙  (Trivial_Aheap Γ e) = Trivial_Aheap (π ∙ Γ) (π ∙ e)"
  unfolding Trivial_Aheap_def
  apply perm_simp
  apply (simp add: Abs_cfun_eqvt)
  done

lemma Trivial_Aheap_simp: "Trivial_Aheap Γ e⋅ a = (λ x. up⋅0) f|` domA Γ"
  unfolding Trivial_Aheap_def by simp

lemma Trivial_fup_Aexp_below_fv: "fup⋅(Trivial_Aexp e)⋅a ⊑ (λ x . up⋅0) f|` fv e"
  by (cases a)(auto simp add: Trivial_Aexp_simp)

lemma Trivial_Abinds_below_fv: "ABinds Γ⋅ae ⊑ (λ x . up⋅0) f|` fv Γ"
  by (induction Γ rule:ABinds.induct)
     (auto simp add: join_below_iff intro!: below_trans[OF Trivial_fup_Aexp_below_fv] env_restr_mono2 elim: below_trans dest: subsetD[OF fv_delete_subset] simp del: fun_meet_simp)

interpretation ArityAnalysisLetSafe Trivial_Aexp Trivial_Aheap
proof
  fix π
  show "π ∙ Trivial_Aheap = Trivial_Aheap" by perm_simp rule  
next
  fix Γ e ae show "edom (Trivial_Aheap Γ e⋅ae) ⊆ domA Γ"
  by (simp add: Trivial_Aheap_simp)
next
  fix Γ :: heap and e and a
  show "ABinds Γ⋅(Trivial_Aheap Γ e⋅a) ⊔ Trivial_Aexp e⋅a ⊑ Trivial_Aheap Γ e⋅a ⊔ Trivial_Aexp (Terms.Let Γ e)⋅a"
    by (auto simp add: Trivial_Aheap_simp Trivial_Aexp_simp join_below_iff env_restr_join2 intro!: env_restr_mono2 below_trans[OF Trivial_Abinds_below_fv])
next
  fix x y :: var and Γ :: heap and e
  assume "x ∉ domA Γ" and "y ∉ domA Γ"
  thus "Trivial_Aheap Γ[x::h=y] e[x::=y] = Trivial_Aheap Γ e"
    by (auto intro: cfun_eqI simp add: Trivial_Aheap_simp)
qed

end