theory Height

  imports "../Nominal2"

begin

text {*  

  A small problem suggested by D. Wang. It shows how

  the height of a lambda-terms behaves under substitution.

*}

atom_decl name

nominal_datatype lam = 

    Var "name"

  | App "lam" "lam"

  | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100)

thm lam.strong_induct

text {* Definition of the height-function on lambda-terms. *} 

function

  height :: "lam \<Rightarrow> int"

where

  "height (Var x) = 1"

| "height (App t1 t2) = (max (height t1) (height t2)) + 1"

| "height (Lam [a].t) = (height t) + 1"

  apply(rule_tac y="x" in lam.exhaust)

  apply(simp_all)[3]

  apply(simp add: lam.eq_iff)

  apply(simp add: lam.distinct)

  apply(simp add: lam.distinct)

  apply(simp add: lam.eq_iff)

  apply(simp add: lam.distinct)

  apply(simp add: lam.eq_iff)

  sorry

termination

  apply(relation "measure size")

  apply(simp_all add: lam.size)

  done

text {* Definition of capture-avoiding substitution. *}

function

  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)

where

  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"

| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"

| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"

apply(case_tac x)

apply(simp)

apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)

apply(simp_all)[3]

apply(blast)

apply(blast)

apply(simp add: fresh_star_def fresh_Pair)

apply(blast)

apply(simp add: lam.eq_iff)

apply(simp add: lam.distinct)

apply(simp add: lam.distinct)

apply(simp add: lam.eq_iff)

apply(simp add: lam.distinct)

apply(simp add: lam.eq_iff)

sorry

termination

  apply(relation "measure (size o fst)")

  apply(simp_all add: lam.size)

  done

text{* The next lemma is needed in the Var-case of the theorem below. *}

lemma height_ge_one: 

  shows "1 \<le> (height e)"

apply(nominal_induct e rule: lam.strong_induct) 

apply(simp_all)

done

text {* 

  Unlike the proplem suggested by Wang, however, the 

  theorem is here formulated entirely by using functions. 

*}

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 (1 y)

  have "1 \<le> height e'" by (rule height_ge_one)

  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp

next

  case (3 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 (2 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