--- a/Nominal/Ex/LamTest.thy	Sun Jan 09 01:17:44 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Sun Jan 09 04:28:24 2011 +0000
@@ -1600,21 +1600,73 @@
 
 ML {* trace := true *}
 
+lemma test:
+  assumes a: "[[x]]lst. t = [[x]]lst. t'"
+  shows "t = t'"
+using a
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp only: alphas)
+apply(erule conjE)+
+apply(rule sym)
+apply(clarify)
+apply(rule supp_perm_eq)
+apply(subgoal_tac "set [x] \<sharp>* p")
+apply(auto simp add: fresh_star_def)[1]
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_perm)
+done
+
+lemma test2:
+  assumes "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y"
+  and "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
+  shows "x = y"
+using assms by (simp add: swap_fresh_fresh)
+
+lemma test3:
+  assumes "x = y"
+  and "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y"
+  shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
+using assms by (simp add: swap_fresh_fresh)
+
 nominal_primrec
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
 | "depth (Lam x t) = (depth t) + 1"
-thm depth_graph.intros
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
-sorry
+apply(subgoal_tac "finite (supp (x, xa, t, ta, depth_sumC t, depth_sumC ta))")
+apply(erule_tac ?'a="name" in obtain_at_base)
+unfolding fresh_def[symmetric]
+apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2)
+apply(simp add: pure_fresh)
+apply(simp add: pure_fresh)
+apply(simp add: pure_fresh)
+apply(simp add: pure_fresh)
+apply(simp add: eqvt_at_def)
+apply(drule test)
+apply(simp)
+apply(simp add: finite_supp)
+done
+
+termination depth
+  apply(relation "measure size")
+  apply(auto simp add: lam.size)
+  done
 
 thm depth.psimps
+thm depth.simps
 
 nominal_primrec 
   frees :: "lam \<Rightarrow> name set"
@@ -1628,7 +1680,17 @@
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
-sorry
+apply(subgoal_tac "finite (supp (x, xa, t, ta, frees_sumC t, frees_sumC ta))")
+apply(erule_tac ?'a="name" in obtain_at_base)
+unfolding fresh_def[symmetric]
+apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp)
+apply(drule test)
+oops
 
 nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
@@ -1644,11 +1706,42 @@
 apply(simp add: lam.eq_iff lam.distinct)
 apply(auto)[1]
 apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)
+apply(simp_all add: lam.distinct)[5]
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
-sorry
+apply(subgoal_tac "finite (supp (ya, sa, x, xa, t, ta, subst_sumC (t, ya, sa), subst_sumC (ta, ya, sa)))")
+apply(erule_tac ?'a="name" in obtain_at_base)
+unfolding fresh_def[symmetric]
+apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(erule conjE)+
+apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: eqvt_at_def)
+apply(drule test)
+apply(simp)
+apply(subst (2) swap_fresh_fresh)
+apply(simp)
+apply(simp)
+apply(subst (2) swap_fresh_fresh)
+apply(simp)
+apply(simp)
+apply(subst (3) swap_fresh_fresh)
+apply(simp)
+apply(simp)
+apply(subst (3) swap_fresh_fresh)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp add: finite_supp)
+done
 
 (* this should not work *)
 nominal_primrec 

--- a/Nominal/Ex/Lambda.thy	Sun Jan 09 01:17:44 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Sun Jan 09 04:28:24 2011 +0000
@@ -22,6 +22,16 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+definition
+ "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+
+function
+  depth :: "lam \<Rightarrow> nat"
+where
+  "depth (Var x) = 1"
+| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
+| "depth (Lam x t) = (depth t) + 1"
+oops
 
 section {* Matching *}