theory Height

  imports "Lambda"

begin

text {*  

  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 simp

next

  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 simp

next    

  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  

qed

end