diff -r 2e849bc2163a -r 01ae96fa4bf9 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Apr 12 14:31:23 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 12 17:44:26 2010 +0200
@@ -132,13 +132,6 @@
         atac ])
 *}
 
-ML {* try hd [1] *}
-
-ML {*
-Skip_Proof.cheat_tac
-*}
-
-
 lemma [eqvt]:
   assumes a: "valid Gamma" 
   shows "valid (p \<bullet> Gamma)"
@@ -155,7 +148,35 @@
   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_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"
+
+thm typing.induct
+ML {* Inductive.get_monos @{context} *}
+
+lemma uu[eqvt]:
+  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(perm_strict_simp)
+apply(rule typing.intros)
+apply(rule conj_mono[THEN mp])
+prefer 3
+apply(assumption)
+apply(rule impI)
+prefer 2
+apply(rule impI)
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+done
+
+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"
 
 lemma uu[eqvt]:
@@ -172,24 +193,8 @@
 thm eqvts_raw
 
 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]
+thm alpha_gen_real_eqvt
+(*declare alpha_gen_real_eqvt[eqvt]*)
 
 lemma
   assumes a: "alpha_lam_raw t1 t2"
@@ -197,6 +202,7 @@
 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)