--- a/Nominal/Ex/Height.thy	Tue Jan 18 21:28:07 2011 +0100
+++ b/Nominal/Ex/Height.thy	Wed Jan 19 07:06:47 2011 +0100
@@ -1,5 +1,5 @@
 theory Height
-  imports "../Nominal2"
+  imports "Lambda"
 begin
 
 text {*  
@@ -7,96 +7,29 @@
   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)
-
-
-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. 
-*}
+by (induct e rule: lam.induct) 
+   (simp_all)
 
 theorem height_subst:
-  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
+  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'" by (rule height_ge_one)
+  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
+  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
+  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 
+  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