Theory ArityTransform

theory ArityTransform
imports ArityAnalysisSig AbstractTransform ArityEtaExpansionSafe
begin

context ArityAnalysisHeapEqvt
begin
sublocale AbstractTransformBound
  "λ a . inca"
  "λ a . preda"
  "λ Δ e a . (a, Aheap Δ ea)"
  "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 (𝒯⇘incae) x"
  "𝒯⇘a(Lam [x]. e) = Lam [x]. 𝒯⇘predae"
  "𝒯⇘a(Var x) = Var x"
  "𝒯⇘a(Let Γ e) = Let (map_transform Aeta_expand (Aheap Γ ea) (map_transform (λa. 𝒯⇘a) (Aheap Γ ea) Γ)) (𝒯⇘ae)"
  "𝒯⇘a(Bool b) = Bool b"
  "𝒯⇘a(scrut ? e1 : e2) = (𝒯⇘0scrut ? 𝒯⇘ae1 : 𝒯⇘ae2)"
  by simp_all
end


end