--- a/Nominal/Ex/LetRec.thy	Sun Jun 19 13:14:37 2011 +0900
+++ b/Nominal/Ex/LetRec.thy	Mon Jun 20 20:09:30 2011 +0900
@@ -27,6 +27,40 @@
 thm let_rec.fv_bn_eqvt
 thm let_rec.size_eqvt
 
+lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
+  by (simp add: permute_pure)
+
+nominal_primrec
+    height_trm :: "trm \<Rightarrow> nat"
+and height_bp :: "bp \<Rightarrow> nat"
+where
+  "height_trm (Var x) = 1"
+| "height_trm (App l r) = max (height_trm l) (height_trm r)"
+| "height_trm (Lam v b) = 1 + (height_trm b)"
+| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
+| "height_bp (Bp v t) = height_trm t"
+  apply (simp only: eqvt_def height_trm_height_bp_graph_def)
+  apply (rule, perm_simp, rule, rule TrueI)
+  apply auto
+  apply (case_tac x)
+  apply (case_tac a rule: let_rec.exhaust(1))
+  apply auto
+  apply (case_tac b rule: let_rec.exhaust(2))
+  apply blast
+  apply (erule Abs_set_fcb)
+  apply (simp_all add: pure_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: Abs_eq_iff2)
+  apply (simp add: alphas)
+  apply clarify
+  apply (rule trans)
+  apply(rule_tac p="p" in supp_perm_eq[symmetric])
+  apply (simp add: pure_supp fresh_star_def)
+  apply (simp only: eqvts)
+  apply (simp add: eqvt_at_def)
+  done
+
+termination by lexicographic_order
 
 end