# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307000469 -32400
# Node ID 377bea405940f3133cff345d99adca06d05c1c09
# Parent  a72a04f3d6bf49b30a5662b9e80ed0f7df00ab3d
Use FCB to simplify proof

diff -r a72a04f3d6bf -r 377bea405940 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 10:11:50 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 16:41:09 2011 +0900
@@ -531,16 +531,9 @@
   apply (rule, perm_simp, rule)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
-  apply (simp add: Abs1_eq_iff)
-  apply (auto)
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
   apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
-  apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
   done
 
 termination
@@ -590,6 +583,7 @@
   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 unfolding eqvt_def Z_graph_def
 apply (rule, perm_simp, rule)
 oops
@@ -603,7 +597,7 @@
   "f [] = 0"
 | "f [e] = e"
 | "f (l @ m) = f l + f m"
-apply(simp_all)
+  apply(simp_all)
 oops