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