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