--- a/Nominal/Term1.thy	Mon Mar 01 16:04:03 2010 +0100
+++ b/Nominal/Term1.thy	Mon Mar 01 21:50:24 2010 +0100
@@ -32,8 +32,8 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
-  [[], [[]], [[], []]]] *}
+  [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]],
+  [[], [], []]] *}
 
 notation
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
@@ -52,13 +52,99 @@
 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
 
-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))
+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
+
+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}
 *}
-print_theorems
+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))"