--- a/Nominal/Ex/LetSimple2.thy	Sun Jul 17 11:33:09 2011 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Mon Jul 18 00:21:51 2011 +0100
@@ -62,8 +62,6 @@
 
 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)"
-  by (simp add: permute_pure)
 
 
 section {* definition with helper functions *}
@@ -261,6 +259,7 @@
   apply(simp add: eqvt_at_def perm_supp_eq)
   done
 
+termination by lexicographic_order
 
 lemma ww1:
   shows "finite (fv_trm t)"
@@ -324,7 +323,7 @@
 where
   "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])"
-| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])"
+| "(set (bn as)) \<sharp>* (y, s, fv_bn as) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])"
 | "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])"
 apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
@@ -348,9 +347,23 @@
   apply(simp)
   apply(case_tac a)
   apply(simp)
-  apply(rule_tac y="aa" and c="(b, c)" in trm_assn.strong_exhaust(1))
+  apply(rule_tac y="aa" and c="(b, c, aa)" in trm_assn.strong_exhaust(1))
   apply(blast)+
   apply(simp)
+  apply(drule_tac x="assn" in meta_spec)
+  apply(drule_tac x="b" in meta_spec)
+  apply(drule_tac x="c" in meta_spec)
+  apply(drule_tac x="trm" in meta_spec)
+  apply(simp add: trm_assn.alpha_refl)
+  apply(rotate_tac 5)
+  apply(drule meta_mp)
+  apply(simp add: fresh_star_Pair)
+  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)
   apply(simp)
   apply(rule_tac y="a" in trm_assn.exhaust(2))
@@ -362,7 +375,6 @@
   apply(simp)
   prefer 2
   apply(simp)
-  thm Inl_inject
   apply(drule Inl_inject)
   apply(rule arg_cong)
   back
@@ -376,39 +388,20 @@
   apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))")
   apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))")
   apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))")
-  defer
-  apply(simp add: Abs_eq_iff alphas)
-  apply(clarify)
-  apply(rule eqvt_at_perm)
   apply(simp)
-  apply(simp add: subst_trm2_def)
-  apply(simp add: eqvt_at_def)
-  defer
-  defer
-  defer
-  defer
-  defer
-  apply(rule conjI)
-  apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa")
-  apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa")
+  (* HERE *)
+  apply (subgoal_tac "subst_assn2 ast y s= subst_assn2 asta ya sa")
+  apply (subgoal_tac "subst_trm2 t y s = subst_trm2 ta ya sa")
+  apply(simp)
   apply(simp)
   apply(erule_tac conjE)+
   apply(erule alpha_bn_cases)
   apply(simp add: trm_assn.bn_defs)
   apply(rotate_tac 7)
-  apply(drule k)
-  apply(erule conjE)
-  apply(subst (asm) Abs1_eq_iff)
-  apply(rule sort_of_atom_eq)
-  apply(rule sort_of_atom_eq)
-  apply(erule disjE)
-  apply(simp)
-  apply(rotate_tac 12)
-  apply(drule sym)
-  apply(rule sym)
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(erule fresh_eqvt_at)
   
+  
   thm fresh_eqvt_at
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)