--- a/Nominal/Ex/Lambda.thy	Sun Jul 03 21:04:46 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Mon Jul 04 23:54:05 2011 +0200
@@ -204,60 +204,6 @@
   by (metis fresh_fun_app)
 
 
-section {* A test with a locale and an interpretation. *}
-
-text {* conclusion: it is no necessary *}
-
-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 :: "lam \<Rightarrow> ('a::pt)"
-where
-  "f (Var x) = f1 x"
-| "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)"
-| "f (Lam [x].t) = f3 x t (f t)"
-  apply (simp add: eqvt_def f_graph_def)
-  apply (perm_simp)
-  apply(simp add: eq[simplified eqvt_def])
-  apply(rule TrueI)
-  apply(rule_tac y="x" in lam.exhaust)
-  apply(auto simp add: fresh_star_def)
-  apply(erule Abs_lst1_fcb)
-  apply simp_all
-  apply(simp add: fcb)
-  apply (rule fresh_fun_eqvt_app3[OF eq(3)])
-  apply (simp add: fresh_at_base)
-  apply assumption
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply assumption
-  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)
-  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
-  done
-
-termination
-  by lexicographic_order
-
-end
-
-interpretation hei: test
-  "%n. (1 :: nat)"
-  "%t1 t2 r1 r2. (r1 + r2)"
-  "%n t r. r + 1"
-  apply default
-  apply (auto simp add: pure_fresh supp_Pair)
-  apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3]
-  apply (simp_all add: eqvt_def permute_fun_def permute_pure)
-  done
-
 section {* height function *}
 
 nominal_primrec
@@ -817,6 +763,74 @@
 apply(rule refl)
 oops
 
+
+lemma test:
+  assumes "t = s"
+  and "supp p \<sharp>* t" "supp p \<sharp>* x"
+  and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y"
+  shows "x = y"
+using assms by (simp add: perm_supp_eq)
+
+lemma test2:
+  assumes "cs \<subseteq> as \<union> bs"
+  and "as \<sharp>* x" "bs \<sharp>* x"
+  shows "cs \<sharp>* x"
+using assms
+by (auto simp add: fresh_star_def) 
+
+lemma test3:
+  assumes "cs \<subseteq> as"
+  and "as \<sharp>* x"
+  shows "cs \<sharp>* x"
+using assms
+by (auto simp add: fresh_star_def) 
+
+
+
+nominal_primrec  (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
+  aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
+where
+  "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
+| "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
+| "aux (Var x) (App t1 t2) xs = False"
+| "aux (Var x) (Lam [y].t) xs = False"
+| "aux (App t1 t2) (Var x) xs = False"
+| "aux (App t1 t2) (Lam [x].t) xs = False"
+| "aux (Lam [x].t) (Var y) xs = False"
+| "aux (Lam [x].t) (App t1 t2) xs = False"
+| "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
+       aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
+  apply (simp add: eqvt_def aux_graph_def)
+  apply (rule, perm_simp, rule)
+  apply(erule aux_graph.induct)
+  apply(simp_all add: fresh_star_def pure_fresh)[9]
+  apply(case_tac x)
+  apply(simp)
+  apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+  apply(simp)
+  apply(rule_tac y="b" and c="c" in lam.strong_exhaust)
+  apply(metis)+
+  apply(simp)
+  apply(rule_tac y="b" and c="c" in lam.strong_exhaust)
+  apply(metis)+
+  apply(simp)
+  apply(rule_tac y="b" and c="(lam, c, name)" in lam.strong_exhaust)
+  apply(metis)+
+  apply(simp)
+  apply(drule_tac x="name" in meta_spec)
+  apply(drule_tac x="lama" in meta_spec)
+  apply(drule_tac x="c" in meta_spec)
+  apply(drule_tac x="namea" in meta_spec)
+  apply(drule_tac x="lam" in meta_spec)
+  apply(simp add: fresh_star_Pair)
+  apply(simp add: fresh_star_def fresh_at_base lam.fresh)
+  apply(auto)[1]
+  apply(simp_all)[44]
+  apply(simp del: Product_Type.prod.inject)  
+  sorry
+
+termination by lexicographic_order
+
 end