theory Height imports "Lambda"begintext {* A small problem suggested by D. Wang. It shows how the height of a lambda-terms behaves under substitution.*}lemma height_ge_one: shows "1 \<le> (height e)"by (induct e rule: lam.induct) (simp_all)theorem height_subst: shows "height (e[x::=e']) \<le> height e - 1 + height e'"proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) case (Var y) have "1 \<le> height e'" using height_ge_one by simp then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simpnext case (Lam y e1) have ih: "height (e1[x::=e']) \<le> height e1 - 1 + height e'" by fact moreover have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *) ultimately show "height ((Lam y e1)[x::=e']) \<le> height (Lam y e1) - 1 + height e'" by simpnext case (App e1 e2) have ih1: "height (e1[x::=e']) \<le> (height e1) - 1 + height e'" and ih2: "height (e2[x::=e']) \<le> (height e2) - 1 + height e'" by fact+ then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp qedend