--- a/Nominal/Ex/Lambda.thy	Tue May 03 13:25:02 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue May 03 15:39:30 2011 +0100
@@ -2,6 +2,23 @@
 imports "../Nominal2" 
 begin
 
+inductive
+  even :: "nat \<Rightarrow> bool" and
+  odd  :: "nat \<Rightarrow> bool"
+where
+  "even 0"
+| "odd n \<Longrightarrow> even (Suc n)"
+| "even n \<Longrightarrow> odd (Suc n)"
+
+thm even_odd_def
+
+lemma
+  shows "p \<bullet> (even n) = even (p \<bullet> n)"
+unfolding even_def
+unfolding even_odd_def
+apply(perm_simp)
+apply(rule refl)
+done
 
 atom_decl name
 
@@ -10,18 +27,27 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
   Var: "triv (Var x) n"
+| App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n"
 
 lemma 
   "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)"
 unfolding triv_def
 apply(perm_simp)
+apply(rule refl)
 oops
 (*apply(perm_simp)*)
 
+ML {*
+  Inductive.the_inductive @{context} "Lambda.triv"
+*}
+
+thm triv_def
+
 equivariance triv
 nominal_inductive triv avoids Var: "{}::name set"
 apply(auto simp add: fresh_star_def)