--- a/Nominal/Ex/LetSimple2.thy	Sun Jul 17 04:04:17 2011 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Sun Jul 17 11:33:09 2011 +0100
@@ -53,6 +53,13 @@
 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
   using trm_assn.alpha_trans by metis
 
+lemma fv_bn_finite[simp]:
+  "finite (fv_bn as)"
+apply(case_tac as rule: trm_assn.exhaust(2))
+apply(simp add: trm_assn.supp finite_supp)
+done
+
+
 lemma k: "A \<Longrightarrow> A \<and> A" by blast
 
 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
@@ -171,34 +178,34 @@
 lemma cheat: "P" sorry
 
 nominal_primrec 
- (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y")
     height_trm2 :: "trm \<Rightarrow> nat"
 and height_assn2 :: "assn \<Rightarrow> nat"
 where
   "height_trm2 (Var x) = 1"
 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)"
-| "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
+| "set (bn as) \<sharp>* fv_bn as \<Longrightarrow> height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
 | "height_assn2 (Assn x t) = (height_trm2 t)"
   thm height_trm2_height_assn2_graph.intros[no_vars]
   thm height_trm2_height_assn2_graph_def
   apply (simp only: eqvt_def height_trm2_height_assn2_graph_def)
   apply (rule, perm_simp, rule)
-  apply(erule height_trm2_height_assn2_graph.induct)
   -- "invariant"
   apply(simp)
-  apply(simp)
-  apply(simp)
-  apply(simp)
-  apply(rule cheat)
-  apply -
   --"completeness"
   apply (case_tac x)
   apply(simp)
-  apply (case_tac a rule: trm_assn.exhaust(1))
+  apply (rule_tac y="a" and c="a" in trm_assn.strong_exhaust(1))
   apply (auto simp add: alpha_bn_refl)[3]
   apply (drule_tac x="assn" in meta_spec)
   apply (drule_tac x="trm" in meta_spec)
   apply(simp add: alpha_bn_refl)
+  apply(rotate_tac 3)
+  apply(drule meta_mp)
+  apply(simp add: fresh_star_def trm_assn.fresh)
+  apply(simp add: fresh_def)
+  apply(subst supp_finite_atom_set)
+  apply(simp)
+  apply(simp)
   apply(simp)
   apply (case_tac b rule: trm_assn.exhaust(2))
   apply (auto)[1]
@@ -241,10 +248,18 @@
   apply(erule alpha_bn_cases)
   apply(simp del: trm_assn.eq_iff)
   apply(simp only: trm_assn.bn_defs)
-  apply(erule_tac c="()" in Abs_lst1_fcb2')
-  apply(simp_all add: fresh_star_def pure_fresh)[3]
-
-  oops
+  apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2')
+  apply(simp_all add: fresh_star_def pure_fresh)[2]
+  apply(simp add: trm_assn.supp)
+  apply(simp add: fresh_def)
+  apply(subst (asm) supp_finite_atom_set)
+  apply(simp add: finite_supp)
+  apply(subst (asm) supp_finite_atom_set)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def perm_supp_eq)
+  apply(simp add: eqvt_at_def perm_supp_eq)
+  done
 
 
 lemma ww1: