--- a/Nominal/Term1.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Term1.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -52,99 +52,10 @@
 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
 *}
 
-ML {*
-fun build_alpha_eqvts funs perms simps induct ctxt =
-let
-  val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
-  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val args2 = map Free (indnames2 ~~ types);
-  fun eqvtc ((alpha, perm), (arg, arg2)) =
-    HOLogic.mk_imp (alpha $ arg $ arg2,
-      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
-  
-in
-  gl
-end
-*}ye
-
-lemma alpha_gen_compose_eqvt:
-  assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
-  and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
-  and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s) \<and> P g pi d e t s R f pia"
-  using b
-  apply -
-sorry
-
-lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (p \<bullet> pi)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="pia \<bullet> pi" in exI)
-by auto
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
+build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *}
 
-prove {*
-  build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context}
-*}
-apply(rule alpha_rtrm1_alpha_bp.induct)
-apply(simp_all add: atom_eqvt alpha1_inj)
-apply(erule exi)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(rule conjI)
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
-apply(subst empty_eqvt[symmetric])
-apply(subst insert_eqvt[symmetric])
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply(subst eqvts)
-apply simp
-apply(rule conjI)
-apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-thm eqvts
-apply(simp add:eqvts)
-
-thm insert_eqvt
-apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric])
-
-apply(rule conjI)
-thm atom_eqvt
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply simp
-apply(rule conjI)
-apply(subst permute_eqvt[symmetric])
-apply simp
-apply(rule conjI)
-apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply simp
-apply(subst permute_eqvt[symmetric])
-apply simp
-apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
-apply(simp)
-thm permute_eq_iff[THEN iffD1]
-apply(clarify)
-apply(rule conjI)
-
-apply(erule alpha_gen_compose_eqvt)
-
-prefer 2
-apply(erule conj_forward)
-apply (simp add: eqvts)
-apply(erule alpha_gen_compose_eqvt)
 lemma alpha1_eqvt_proper[eqvt]:
   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
   "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"