--- a/Nominal/Ex/Lambda.thy	Fri Jun 03 18:33:11 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Fri Jun 03 12:46:23 2011 +0100
@@ -12,6 +12,19 @@
 
 lemma cheat: "P" sorry
 
+thm lam.strong_exhaust
+
+lemma lam_strong_exhaust2:
+  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
+    \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
+    \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
+    finite (supp c)\<rbrakk>
+    \<Longrightarrow> P"
+sorry
+
+abbreviation
+  "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" 
+
 lemma Abs1_eq_fdest:
   fixes x y :: "'a :: at_base"
     and S T :: "'b :: fs"
@@ -40,39 +53,43 @@
   using fresh_fun_eqvt_app[OF a b(1)] a b
   by (metis fresh_fun_app)
 
+locale test =
+   fixes f1::"name \<Rightarrow> ('a::pt)"
+     and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)"
+     and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)"
+   assumes fs: "finite (supp (f1, f2, f3))"
+       and eq: "eqvt f1" "eqvt f2" "eqvt f3"
+       and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r"
+begin
+
 nominal_primrec
-  f :: "(name \<Rightarrow> 'a\<Colon>{pt}) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a"
+  f :: "lam \<Rightarrow> ('a::pt)"
 where
-  "f f1 f2 f3 (Var x) = f1 x"
-| "f f1 f2 f3 (App t1 t2) = f2 t1 t2 (f f1 f2 f3 t1) (f f1 f2 f3 t2)"
-| "(\<And>a t r. atom a \<sharp> f3 a t r) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t)) = f3 x t (f f1 f2 f3 t)"
+  "f (Var x) = f1 x"
+| "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)"
+| "atom x \<sharp> (f1, f2, f3) \<Longrightarrow> f (Lam [x].t) = f3 x t (f t)"
   apply (simp add: eqvt_def f_graph_def)
-  apply (rule, perm_simp, rule)
-  apply(case_tac x)
-  apply(rule_tac y="d" and c="z" in lam.strong_exhaust)
+  apply (perm_simp)
+  apply(simp add: eq[simplified eqvt_def])
+  apply(rule_tac y="x" and c="(f1,f2,f3)" in lam_strong_exhaust2)
   apply(auto simp add: fresh_star_def)
-  apply(blast)
-  defer
+  apply(rule fs)
   apply(simp add: fresh_Pair_elim)
   apply(erule Abs1_eq_fdest)
   apply simp_all
-  apply (rule_tac f="f3a" in fresh_fun_eqvt_app3)
-  apply assumption
-  apply (simp add: fresh_at_base)
-  apply assumption
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Pair supp_fun_eqvt finite_supp)
-  apply (simp add: fresh_Pair)
-  apply (subgoal_tac "\<And>p y r. p \<bullet> (f3a x y r) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)")
+  apply(simp add: fcb)
+  apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)")
   apply (simp add: eqvt_at_def eqvt_def)
-  apply (simp add: permute_fun_app_eq)
-  apply (simp add: eqvt_def)
-  sorry (*this could be defined *)
+  apply (simp add: permute_fun_app_eq eq[simplified eqvt_def])
+  sorry
 
 termination sorry
 
-thm f.simps
+end
 
+thm test.f.simps
+
+thm test_def