diff -r 4135198bbb8a -r 56cebe7f8e24 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Apr 13 00:47:57 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 13 00:53:32 2010 +0200
@@ -141,6 +141,18 @@
 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
 done
 
+lemma
+  shows "valid Gamma \<longrightarrow> valid (p \<bullet> Gamma)"
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid")
+*}
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+done
+
+
 thm eqvts
 thm eqvts_raw
 
@@ -151,8 +163,20 @@
   | 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} *}
+
+ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *}
+
+lemma 
+  shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
+*}
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(perm_strict_simp)
+apply(rule typing.intros)
+oops
 
 lemma uu[eqvt]:
   assumes a: "Gamma \<turnstile> t : T" 
@@ -168,10 +192,13 @@
 apply(rule impI)
 prefer 2
 apply(rule impI)
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(simp)
+apply(auto)[1]
+apply(simp)
 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
@@ -188,6 +215,37 @@
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 done
+*)
+
+ML {*
+val inductive_atomize = @{thms induct_atomize};
+
+val atomize_conv =
+  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
+    (HOL_basic_ss addsimps inductive_atomize);
+val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
+fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
+  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+*}
+
+ML {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
+*}
+
+ML {* val ind_params = Inductive.params_of raw_induct *}
+ML {* val raw_induct = atomize_induct @{context} raw_induct; *}
+ML {* val elims = map (atomize_induct @{context}) elims; *}
+ML {* val monos = Inductive.get_monos @{context}; *}
+
+lemma 
+  shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} intrs 1 *})
+apply(perm_strict_simp)
+apply(rule typing.intros)
+oops
+
 
 thm eqvts
 thm eqvts_raw