Theory ArityTransform

theory ArityTransform
imports ArityAnalysisSig AbstractTransform ArityEtaExpansionSafe
begin

context ArityAnalysisHeapEqvt
begin
sublocale AbstractTransformBound
  "λ a . inc⋅a"
  "λ a . pred⋅a"
  "λ Δ e a . (a, Aheap Δ e⋅a)"
  "fst"
  "snd"
  "λ _. 0"
  "Aeta_expand"
  "snd"
apply standard
apply (((rule eq_reflection)?, perm_simp, rule)+)
done

abbreviation transform_syn (‹𝒯⇘_⇙›) where "𝒯⇘a⇙ ≡ transform a"

lemma transform_simps:
  "𝒯⇘a⇙ (App e x) = App (𝒯⇘inc⋅a⇙ e) x"
  "𝒯⇘a⇙ (Lam [x]. e) = Lam [x]. 𝒯⇘pred⋅a⇙ e"
  "𝒯⇘a⇙ (Var x) = Var x"
  "𝒯⇘a⇙ (Let Γ e) = Let (map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform (λa. 𝒯⇘a⇙) (Aheap Γ e⋅a) Γ)) (𝒯⇘a⇙ e)"
  "𝒯⇘a⇙ (Bool b) = Bool b"
  "𝒯⇘a⇙ (scrut ? e1 : e2) = (𝒯⇘0⇙ scrut ? 𝒯⇘a⇙ e1 : 𝒯⇘a⇙ e2)"
  by simp_all
end


end