--- a/Nominal/Ex/Lambda.thy	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Sun Apr 11 22:48:49 2010 +0200
@@ -107,7 +107,12 @@
 
 nominal_datatype ty =
   TVar string
-| TFun ty ty ("_ \<rightarrow> _")
+| TFun ty ty
+
+notation
+ TFun ("_ \<rightarrow> _") 
+
+declare ty.perm[eqvt]
 
 inductive
   valid :: "(name \<times> ty) list \<Rightarrow> bool"
@@ -128,7 +133,7 @@
 *}
 
 
-lemma
+lemma 
   assumes a: "valid Gamma" 
   shows "valid (p \<bullet> Gamma)"
 using a
@@ -137,6 +142,31 @@
 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
 done
 
+lemma
+  "(p \<bullet> valid) = valid"
+oops
+
+lemma temp[eqvt_raw]: 
+  "(p \<bullet> valid) \<equiv> valid"
+sorry
+
+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; \<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"
+
+lemma
+  assumes a: "Gamma \<turnstile> t : T" 
+  shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+using a
+apply(induct)
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+done
+
 declare permute_lam_raw.simps[eqvt]
 
 thm alpha_gen_real_eqvt[no_vars]
@@ -173,6 +203,30 @@
 apply(perm_simp permute_minus_cancel(2))
 oops
 
+thm alpha_lam_raw.intros[no_vars]
+
+inductive
+ alpha_lam_raw'
+where
+  "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
+| "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
+   alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
+| "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+   alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
+
+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(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *})
+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 *}