--- a/Nominal/Ex/Lambda_F_T.thy	Tue Jun 07 10:40:06 2011 +0100
+++ b/Nominal/Ex/Lambda_F_T.thy	Tue Jun 07 23:22:58 2011 +0900
@@ -68,7 +68,7 @@
     and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
 begin
 
-nominal_primrec
+nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
   f
 where
   "f (Var x) l = f1 x l"
@@ -77,6 +77,15 @@
   apply (simp add: eqvt_def f_graph_def)
   apply (rule, perm_simp)
   apply (simp only: eq[unfolded eqvt_def])
+  apply (erule f_graph.induct)
+  apply (simp add: fcb1)
+  apply (simp add: fcb2 fresh_star_Pair)
+  apply simp
+  apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
+  apply (simp add: fresh_star_def)
+  apply (rule fcb3)
+  apply (simp add: fresh_star_def fresh_def)
+  apply simp_all
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)
@@ -99,91 +108,8 @@
   apply (simp add: fresh_star_def)
   apply (rule fcb3)
   apply (rule_tac x="x # la" in meta_spec)
-  apply (thin_tac "eqvt_at f_sumC (t, x # la)")
-  apply (thin_tac "atom x \<sharp> la")
-  apply (thin_tac "atom xa \<sharp> la")
-  apply (thin_tac "x \<noteq> xa")
-  apply (thin_tac "atom xa \<sharp> t")
-  apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)")
-  apply simp
-  apply (rule_tac x="(t, xb)" in meta_spec)
-  apply (simp only: triv_forall_equality)
---"We start induction on the graph. We need the 2nd subgoal in the first one"
-  apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y")
-  apply (rule the_default_pty[OF f_sumC_def])
-  prefer 2
-  apply blast
-  prefer 2
-  apply (erule f_graph.induct)
-  apply (simp add: fcb1)
-  apply (simp add: fcb2 fresh_star_Pair)
-  apply (simp only: snd_conv)
-  apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply assumption
---"We'd like to do the proof with this property"
-  apply (case_tac xc)
-  apply simp
-  apply (rule_tac lam="a" and c="b" in lam.strong_induct)
-  apply (rule_tac a="f1 name c" in ex1I)
-  apply (rule f_graph.intros)
-  apply (erule f_graph.cases)
-  apply simp_all[3]
-  apply (drule_tac x="c" in meta_spec)+
-  apply (erule ex1E)+
-  apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))")
-  apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))")
-  apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I)
-  apply (rule_tac f_graph.intros(2))
-  apply assumption+
-  apply (rotate_tac 8)
-  apply (erule f_graph.cases)
-  apply simp
-  apply auto[1]
-  apply metis
-  apply simp
-  apply (simp add: f_sumC_def)
-  apply (rule THE_defaultI')
-  apply metis
-  apply (simp add: f_sumC_def)
-  apply (rule THE_defaultI')
-  apply metis
---"Only the Lambda case left"
-  apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))")
-  prefer 2
-  apply (simp add: f_sumC_def)
-  apply (rule THE_defaultI')
-  apply assumption
-  apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I)
-  apply (rule f_graph.intros(3))
-  apply (simp add: fresh_star_def)
-  apply assumption
-  apply (rotate_tac -1)
-  apply (erule f_graph.cases)
-  apply simp_all[2]
-  apply simp
-  apply auto[1]
-  apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)")
-  apply simp
-  apply (rule sym)
-  apply (erule Abs1_eq_fdest)
-  apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply metis
-  apply (rule fresh_fun_eqvt_app4[OF eq(3)])
-  apply (simp add: fresh_at_base)
-  apply assumption
-defer --"eqvt_at f_sumC"
-  apply assumption
-  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
-  apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l")
-  apply (simp add: eq[unfolded eqvt_def])
-defer --"eqvt_at f_sumC"
-  apply (metis fresh_star_insert swap_fresh_fresh)
-  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
-  apply simp
+  unfolding fresh_star_def
+--"Exactly the assumption just for the other argument"
   sorry
 
 termination