# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307537043 -32400
# Node ID c78c2d565e999122098f7ec06684a11abd2a86af
# Parent  1233af5cea95c16d8bff702b105e3fb23ed59d4e
Finished the proof with the invariant

diff -r 1233af5cea95 -r c78c2d565e99 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Wed Jun 08 21:32:35 2011 +0900
+++ b/Nominal/Ex/Lambda_F_T.thy	Wed Jun 08 21:44:03 2011 +0900
@@ -90,8 +90,10 @@
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)
   apply(erule Abs1_eq_fdest)
-  defer
-  apply simp_all
+  apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
+  apply (simp add: fresh_star_def)
+  apply (rule fcb3)
+  apply (simp add: fresh_star_def)
   apply (rule fresh_fun_eqvt_app4[OF eq(3)])
   apply (simp add: fresh_at_base)
   apply assumption
@@ -104,13 +106,8 @@
   apply (simp add: eqvt_at_def)
   apply (simp add: swap_fresh_fresh)
   apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
-  apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply (rule_tac x="x # la" in meta_spec)
-  unfolding fresh_star_def
---"Exactly the assumption just for the other argument"
-  sorry
+  apply simp
+  done
 
 termination
   by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)