theory ArityAnalysisSpec imports ArityAnalysisAbinds begin locale SubstArityAnalysis = EdomArityAnalysis + assumes Aexp_subst_restr: "x ∉ S ⟹ y ∉ S ⟹ (Aexp e[x::=y] ⋅ a) f|` S = (Aexp e⋅a) f|` S" locale ArityAnalysisSafe = SubstArityAnalysis + assumes Aexp_Var: "up ⋅ n ⊑ (Aexp (Var x)⋅n) x" assumes Aexp_App: "Aexp e ⋅(inc⋅n) ⊔ esing x ⋅ (up⋅0) ⊑ Aexp (App e x) ⋅ n" assumes Aexp_Lam: "env_delete y (Aexp e ⋅(pred⋅n)) ⊑ Aexp (Lam [y]. e) ⋅ n" assumes Aexp_IfThenElse: "Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a ⊑ Aexp (scrut ? e1 : e2)⋅a" locale ArityAnalysisHeapSafe = ArityAnalysisSafe + ArityAnalysisHeapEqvt + assumes edom_Aheap: "edom (Aheap Γ e⋅ a) ⊆ domA Γ" assumes Aheap_subst: "x ∉ domA Γ ⟹ y ∉ domA Γ ⟹ Aheap Γ[x::h=y] e[x ::=y] = Aheap Γ e" locale ArityAnalysisLetSafe = ArityAnalysisHeapSafe + assumes Aexp_Let: "ABinds Γ⋅(Aheap Γ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a" locale ArityAnalysisLetSafeNoCard = ArityAnalysisLetSafe + assumes Aheap_heap3: "x ∈ thunks Γ ⟹ (Aheap Γ e⋅a) x = up⋅0" context SubstArityAnalysis begin lemma Aexp_subst_upd: "(Aexp e[y::=x]⋅n) ⊑ (Aexp e⋅n)(y := ⊥, x := up⋅0)" proof- have "Aexp e[y::=x]⋅n f|`(-{x,y}) = Aexp e⋅n f|` (-{x,y})" by (rule Aexp_subst_restr) auto show ?thesis proof (rule fun_belowI) fix x' have "x' = x ∨ x' = y ∨ x' ∈ (-{x,y})" by auto thus "(Aexp e[y::=x]⋅n) x' ⊑ ((Aexp e⋅n)(y := ⊥, x := up⋅0)) x'" proof(elim disjE) assume "x' ∈ (-{x,y})" moreover have "Aexp e[y::=x]⋅n f|`(-{x,y}) = Aexp e⋅n f|` (-{x,y})" by (rule Aexp_subst_restr) auto note fun_cong[OF this, where x = x'] ultimately show ?thesis by auto next assume "x' = x" thus ?thesis by simp next assume "x' = y" thus ?thesis using [[simp_trace]] by simp qed qed qed lemma Aexp_subst: "Aexp (e[y::=x])⋅a ⊑ env_delete y ((Aexp e)⋅a) ⊔ esing x⋅(up⋅0)" apply (rule below_trans[OF Aexp_subst_upd]) apply (rule fun_belowI) apply auto done end context ArityAnalysisSafe begin lemma Aexp_Var_singleton: "esing x ⋅ (up⋅n) ⊑ Aexp (Var x) ⋅ n" by (simp add: Aexp_Var) lemma fup_Aexp_Var: "esing x ⋅ n ⊑ fup⋅(Aexp (Var x))⋅n" by (cases n) (simp_all add: Aexp_Var) end context ArityAnalysisLetSafe begin lemma Aheap_nonrec: assumes "nonrec Δ" shows "Aexp e⋅a f|` domA Δ ⊑ Aheap Δ e⋅a" proof- have "ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a" by (rule Aexp_Let) note env_restr_mono[where S = "domA Δ", OF this] moreover from assms have "ABinds Δ⋅(Aheap Δ e⋅a) f|` domA Δ = ⊥" by (rule nonrecE) (auto simp add: fv_def fresh_def dest!: set_mp[OF fup_Aexp_edom]) moreover have "Aheap Δ e⋅a f|` domA Δ = Aheap Δ e⋅a" by (rule env_restr_useless[OF edom_Aheap]) moreover have "(Aexp (Let Δ e)⋅a) f|` domA Δ = ⊥" by (auto dest!: set_mp[OF Aexp_edom]) ultimately show "Aexp e⋅a f|` domA Δ ⊑ Aheap Δ e⋅a" by (simp add: env_restr_join) qed end end