--- a/Nominal/Abs.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -114,14 +114,13 @@
   done
 
 lemma alpha_gen_compose_eqvt:
-  assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+  fixes  pia
+  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)"
+  shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
   using b
   apply -
-  apply(erule exE)
-  apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(rule conjI)
@@ -419,6 +418,7 @@
 apply(simp add: supp_swap)
 done
 
+(*
 thm supp_perm
 
 lemma perm_induct_test:
@@ -502,6 +502,6 @@
 apply(simp)
 oops
 
-
+*)
 end
 

--- a/Nominal/LFex.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -24,9 +24,9 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
-  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+  [[ [], [(NONE, 1, 2)]],
+   [ [], [], [(NONE, 1, 2)] ],
+   [ [], [], [], [(NONE, 1, 2)]]] *}
 notation
     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)

--- a/Nominal/Rsp.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -136,6 +136,10 @@
 end
 *}
 
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
 
 ML {*
 fun build_alpha_eqvts funs perms simps induct ctxt =
@@ -151,18 +155,20 @@
       (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 
+  (
+   (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
+    THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN'
+      REPEAT o etac conjE THEN'
+      (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
+      (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
 end
 *}
 
-
 end

--- 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))"

--- a/Nominal/Term4.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Term4.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -30,7 +30,7 @@
 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+  [[[], [], [(NONE, 0,1)]], [[], []]  ] *}
 print_theorems
 
 notation

--- a/Nominal/Term6.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Term6.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -22,7 +22,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+  [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *}
 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
 thm alpha_rtrm6.intros
 
@@ -41,7 +41,7 @@
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
   build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
 *}
-
+thm alpha6_eqvt
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
   (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}
 thm alpha6_equivp