added an example suggested by D. Wang on the PoplMark-mailing list;
it shows how the height of an alpha-equated lambda term interacts
with capture-avoiding substitution

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Height.thy	Thu Jun 01 14:40:22 2006 +0200
@@ -0,0 +1,114 @@
+(* $Id$ *)
+
+(*  Simple, but artificial, problem suggested by D. Wang *)
+
+theory Height
+imports Lam_substs
+(* 
+   - inherit the type of alpha-equated lambda-terms, 
+     the iteration combinator for this type and the
+     definition of capture-avoiding substitution
+
+     (the iteration combinator is not yet derived 
+      automatically in the last stable version of 
+      the nominal package) 
+
+   - capture-avoiding substitution is written
+     
+        t[x::=t']
+
+     and is defined such that
+
+     (Var y)[x::=t'] = (if x=y then t' else Var y)
+     (App t1 t2)[x::=t'] = App (t1[x::=t']) (t2[x::=t'])
+     y\<sharp>x \<and> y\<sharp>t2 \<Longrightarrow> (Lam [y].t)[x::=t'] = Lam [y].(t[x::=t'])   
+*)
+begin
+
+text {* definition of the height-function by cases *} 
+constdefs 
+  height_Var :: "name \<Rightarrow> int"
+  "height_Var \<equiv> \<lambda>(a::name). 1"
+  
+  height_App :: "int \<Rightarrow> int \<Rightarrow> int"
+  "height_App \<equiv> \<lambda>n1 n2. (max n1 n2)+1"
+
+  height_Lam :: "name \<Rightarrow> int \<Rightarrow> int"
+  "height_Lam \<equiv> \<lambda>(a::name) n. n+1"
+
+  height :: "lam \<Rightarrow> int"
+  "height \<equiv> itfun height_Var height_App height_Lam"
+
+text {* show that height is a function *}
+lemma supp_height_Lam:
+  shows "((supp height_Lam)::name set)={}"
+  apply(simp add: height_Lam_def supp_def perm_fun_def perm_int_def)
+  done
+ 
+lemma fin_supp_height:
+  shows "finite ((supp (height_Var,height_App,height_Lam))::name set)"
+  by (finite_guess add: height_Var_def height_App_def height_Lam_def perm_int_def fs_name1)
+
+lemma FCB_height_Lam:
+  shows "\<exists>(a::name). a\<sharp>height_Lam \<and> (\<forall>n. a\<sharp>height_Lam a n)"
+apply(simp add: height_Lam_def fresh_def supp_def perm_fun_def perm_int_def)
+done
+
+text {* derive the characteristic equations for height from the iteration combinator *}
+lemma height_Var:
+  shows "height (Var c) = 1"
+apply(simp add: height_def itfun_Var[OF fin_supp_height, OF FCB_height_Lam])
+apply(simp add: height_Var_def)
+done
+
+lemma height_App:
+  shows "height (App t1 t2) = (max (height t1) (height t2))+1"
+apply(simp add: height_def itfun_App[OF fin_supp_height, OF FCB_height_Lam])
+apply(simp add: height_App_def)
+done
+
+lemma height_Lam:
+  shows "height (Lam [a].t) = (height t)+1"
+apply(simp add: height_def)
+apply(rule trans)
+apply(rule itfun_Lam[OF fin_supp_height, OF FCB_height_Lam])
+apply(simp add: fresh_def supp_prod supp_height_Lam)
+apply(simp add: supp_def height_Var_def height_App_def perm_fun_def perm_int_def) 
+apply(simp add: height_Lam_def)
+done
+
+text {* add the characteristic equations of height to the simplifier *}
+declare height_Var[simp] height_App[simp] height_Lam[simp]
+
+
+text{* the next lemma is needed in the Var-case of the theorem *}
+
+lemma height_ge_one: 
+  shows "1 \<le> (height e)"
+  by (nominal_induct e rule: lam.induct) (simp | arith)+
+
+
+text {* unlike the proplem suggested by Wang, the theorem is formulated 
+        here 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.induct)
+  case (Var 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 (Lam y e1)
+  hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp
+  moreover
+  have fresh: "y\<sharp>x" "y\<sharp>e'" by fact
+  ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp 
+next    
+  case (App e1 e2)
+  hence ih1: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" 
+    and ih2: "height (e2[x::=e']) \<le> (((height e2) - 1) + (height e'))" by simp_all
+  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by (simp, arith) 
+qed
+
+end
+