--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 12:14:03 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 22:24:33 2011 +0900
@@ -12,27 +12,62 @@
 
 lemma cheat: "P" sorry
 
+lemma Abs1_eq_fdest:
+  fixes x y :: "'a :: at_base"
+    and S T :: "'b :: fs"
+  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
+  and "sort_of (atom x) = sort_of (atom y)"
+  shows "f x T = f y S"
+using assms apply -
+apply (subst (asm) Abs1_eq_iff')
+apply simp_all
+apply (elim conjE disjE)
+apply simp
+apply(rule trans)
+apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_swap fresh_star_def)
+apply(simp add: swap_commute)
+done
+
+lemma fresh_fun_eqvt_app3:
+  assumes a: "eqvt f"
+  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
+  shows "a \<sharp> f x y z"
+  using fresh_fun_eqvt_app[OF a b(1)] a b
+  by (metis fresh_fun_app)
+
 nominal_primrec
-  f
+  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"
 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)"
-| "atom x \<sharp> (f1,f2,f3) \<Longrightarrow> f f1 f2 f3 (Lam [x].t) = f3 x t (f f1 f2 f3 t)"
-unfolding eqvt_def f_graph_def
-apply (rule, perm_simp, rule)
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="d" in lam.exhaust)
-apply(auto)[1]
-apply(auto simp add: lam.distinct lam.eq_iff)[3]
-apply(blast)
-apply(rule cheat) (* this can be solved *)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-sorry (*this could be defined *)
+| "(\<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)"
+  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(auto simp add: fresh_star_def)
+  apply(blast)
+  defer
+  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: eqvt_at_def eqvt_def)
+  apply (simp add: permute_fun_app_eq)
+  apply (simp add: eqvt_def)
+  sorry (*this could be defined *)
 
 termination sorry
 
@@ -76,26 +111,6 @@
 equivariance triv2
 nominal_inductive triv2 .
 
-lemma Abs1_eq_fdest:
-  fixes x y :: "'a :: at_base"
-    and S T :: "'b :: fs"
-  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
-  and "sort_of (atom x) = sort_of (atom y)"
-  shows "f x T = f y S"
-using assms apply -
-apply (subst (asm) Abs1_eq_iff')
-apply simp_all
-apply (elim conjE disjE)
-apply simp
-apply(rule trans)
-apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp add: supp_swap fresh_star_def)
-apply(simp add: swap_commute)
-done
 
 text {* height function *}