--- a/Nominal/Ex/Lambda.thy	Mon Jan 17 14:37:18 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jan 17 15:12:03 2011 +0100
@@ -19,6 +19,110 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+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"
+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)
+apply(subst (asm) Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(simp add: pure_supp)
+apply(simp add: fresh_star_def)
+apply(simp add: eqvt_at_def)
+done
+
+termination
+  apply(relation "measure size")
+  apply(simp_all add: lam.size)
+  done
+  
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+by (induct xs) (auto)
+
+lemma supp_removeAll:
+  fixes x::"atom"
+  shows "supp (removeAll x xs) = (supp xs - {x})"
+apply(induct xs)
+apply(simp_all add: supp_Nil supp_Cons)
+apply(rule conjI)
+apply(rule impI)
+apply(simp add: supp_atom)
+apply(rule impI)
+apply(simp add: supp_atom)
+apply(blast)
+done
+
+nominal_primrec 
+  frees_lst :: "lam \<Rightarrow> atom list"
+where
+  "frees_lst (Var x) = [atom x]"
+| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
+| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
+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)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(simp (no_asm) add: supp_removeAll)
+apply(drule supp_eqvt_at)
+apply(simp add: finite_supp)
+apply(auto simp add: fresh_star_def)[1]
+unfolding eqvt_at_def
+apply(simp only: removeAll_eqvt atom_eqvt)
+done
+
+termination
+  apply(relation "measure size")
+  apply(simp_all add: lam.size)
+  done
+
+(* a small lemma *)
+lemma
+  "supp t = set (frees_lst t)"
+apply(induct t rule: lam.induct)
+apply(simp_all add: lam.supp supp_at_base)
+done
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
+where
+  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp add: lam.eq_iff lam.distinct)
+apply(auto)[1]
+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)[5]
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(erule conjE)+
+oops
+
 
 end