diff -r 3395e87d94b8 -r 51f411b1197d Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Sun Apr 25 08:18:06 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Sun Apr 25 09:13:16 2010 +0200
@@ -126,38 +126,11 @@
   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
-  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
-inductive
-  typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60) 
-where
-    t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"
-  | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"
-  | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
-  typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60) 
-where
-    t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"
-  | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"
-  | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
-  typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)
-and  valid' :: "(name\<times>ty) list \<Rightarrow> bool"
-where
-    v1[intro]: "valid' []"
-  | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"
-  | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"
-  | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
-  | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"
-
 equivariance valid
 equivariance typing
-equivariance typing'
-equivariance typing2' 
-equivariance typing''
 
 thm valid.eqvt
 thm typing.eqvt
@@ -189,27 +162,9 @@
 declare permute_lam_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
 equivariance alpha_lam_raw'
+
 thm eqvts_raw
 
-
-
-(* HERE *)
-
-lemma
-  assumes a: "alpha_lam_raw' t1 t2"
-  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
-using a
-apply(induct)
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
-(*
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
-*)
-oops
-
 section {* size function *}
 
 lemma size_eqvt_raw:
@@ -367,6 +322,8 @@
 done
 *)
 
+
+
 end