--- a/Nominal/Ex/Lambda.thy	Sun Apr 11 18:10:08 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Sun Apr 11 18:11:13 2010 +0200
@@ -11,6 +11,8 @@
 
 lemmas supp_fn' = lam.fv[simplified lam.supp]
 
+declare lam.perm[eqvt]
+
 section {* Strong Induction Principles*}
 
 (* 
@@ -26,9 +28,9 @@
 proof -
   have "\<And>p. P c (p \<bullet> lam)"
     apply(induct lam arbitrary: c rule: lam.induct)
-    apply(simp only: lam.perm)
+    apply(perm_simp)
     apply(rule a1)
-    apply(simp only: lam.perm)
+    apply(perm_simp)
     apply(rule a2)
     apply(assumption)
     apply(assumption)
@@ -72,9 +74,9 @@
 proof -
   have "\<And>p. P c (p \<bullet> lam)"
     apply(induct lam arbitrary: c rule: lam.induct)
-    apply(simp only: lam.perm)
+    apply(perm_simp)
     apply(rule a1)
-    apply(simp only: lam.perm)
+    apply(perm_simp)
     apply(rule a2)
     apply(assumption)
     apply(assumption)
@@ -83,7 +85,7 @@
     apply(rule_tac t="p \<bullet> Lam name lam" and 
                    s="q \<bullet> p \<bullet> Lam name lam" in subst)
     defer
-    apply(simp add: lam.perm)
+    apply(simp)
     apply(rule a3)
     apply(simp add: eqvts fresh_star_def)
     apply(drule_tac x="q + p" in meta_spec)
@@ -92,7 +94,7 @@
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
-    apply(simp only: lam.perm atom_eqvt)
+    apply(perm_simp)
     apply(simp add: fresh_star_def fresh_def supp_fn')
     apply(rule supp_perm_eq)
     apply(simp)
@@ -101,6 +103,78 @@
   then show "P c lam" by simp
 qed
 
+section {* Typing *}
+
+nominal_datatype ty =
+  TVar string
+| TFun ty ty ("_ \<rightarrow> _")
+
+inductive
+  valid :: "(name \<times> ty) list \<Rightarrow> bool"
+where
+  "valid []"
+| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
+
+ML {*
+fun my_tac ctxt intros =  
+ Nominal_Permeq.eqvt_strict_tac ctxt [] []
+ THEN' resolve_tac intros 
+ THEN_ALL_NEW 
+   (atac ORELSE'
+    EVERY'
+      [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}),
+        Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
+        atac ])
+*}
+
+
+lemma
+  assumes a: "valid Gamma" 
+  shows "valid (p \<bullet> Gamma)"
+using a
+apply(induct)
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+done
+
+declare permute_lam_raw.simps[eqvt]
+
+thm alpha_gen_real_eqvt[no_vars]
+
+lemma temporary:
+  shows "(p \<bullet> (bs, x) \<approx>gen R f q (cs, y)) = (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+apply(simp only: permute_bool_def)
+apply(rule iffI)
+apply(rule alpha_gen_real_eqvt)
+apply(assumption)
+apply(drule_tac p="-p" in alpha_gen_real_eqvt(1))
+apply(simp)
+done
+
+lemma temporary_raw:
+  shows "(p \<bullet> alpha_gen) \<equiv> alpha_gen"
+sorry
+
+declare temporary_raw[eqvt_raw]
+
+lemma
+  assumes a: "alpha_lam_raw t1 t2"
+  shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"
+using a
+apply(induct)
+apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
+apply(perm_strict_simp)
+apply(rule alpha_lam_raw.intros)
+apply(simp)
+apply(perm_strict_simp)
+apply(rule alpha_lam_raw.intros)
+apply(simp add: alphas)
+apply(rule_tac p="- p" in permute_boolE)
+apply(perm_simp permute_minus_cancel(2))
+oops
+
+
+
 section {* size function *}
 
 lemma size_eqvt_raw: