Theory TrivialArityAnal

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

definition Trivial_Aexp :: "exp  Arity  AEnv"
  where "Trivial_Aexp e = (Λ n. (λ x. up0) f|` fv e)"

lemma Trivial_Aexp_simp: "Trivial_Aexp e  n = (λ x. up0) 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 "upn  (Trivial_Aexp (Var x)n) x"
    by (simp add: Trivial_Aexp_simp)
next
  fix e x n
  show "Trivial_Aexp e(incn)  esing x(up0)  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(predn))  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 ea 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 scrut0  Trivial_Aexp e1a  Trivial_Aexp e2a  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. up0) 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. up0) f|` domA Γ"
  unfolding Trivial_Aheap_def by simp

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

lemma Trivial_Abinds_below_fv: "ABinds Γae  (λ x . up0) 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 Γ eae)  domA Γ"
  by (simp add: Trivial_Aheap_simp)
next
  fix Γ :: heap and e and a
  show "ABinds Γ(Trivial_Aheap Γ ea)  Trivial_Aexp ea  Trivial_Aheap Γ ea  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