--- a/Nominal/Abs.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Abs.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -113,11 +113,12 @@
   apply(simp)
   done
 
-lemma alpha_gen_atom_eqvt:
-  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
-  shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
-  using b 
+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)"
+  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)"
+  using b
   apply -
   apply(erule exE)
   apply(rule_tac x="pi \<bullet> pia" in exI)
@@ -125,10 +126,10 @@
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
   done

--- a/Nominal/LFex.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/LFex.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -20,6 +20,7 @@
 
 
 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+print_theorems
 
 local_setup {*
   snd o define_fv_alpha "LFex.rkind"
@@ -117,29 +118,11 @@
 thm rkind_rty_rtrm.inducts
 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
 
-instantiation kind and ty and trm :: pt
-begin
-
-quotient_definition
-  "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
-is
-  "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
-
-quotient_definition
-  "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
-is
-  "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
-
-quotient_definition
-  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
-is
-  "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
-
-instance by default (simp_all add:
-  permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
-  permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] 
+  [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}),
+   ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}),
+   ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})]
+  @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *}
 
 (*
 Lifts, but slow and not needed?.

--- a/Nominal/Perm.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Perm.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -13,13 +13,11 @@
 let
   val perm_types = map fastype_of perm_frees;
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
   val gl =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) => HOLogic.mk_eq
-          (perm $ @{term "0 :: perm"} $ Free (x, T),
-           Free (x, T)))
-       (perm_frees ~~
-        map body_type perm_types ~~ perm_indnames)));
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,
@@ -38,15 +36,13 @@
   val pi2 = Free ("pi2", @{typ perm});
   val perm_types = map fastype_of perm_frees
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (
+      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
+      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
   val gl =
     (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) =>
-          let
-            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-          in HOLogic.mk_eq (lhs, rhs)
-          end)
-        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,
@@ -102,30 +98,43 @@
     val lthy =
       Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
     (* TODO: Use the version of prmrec that gives the names explicitely. *)
-    val ((_, perm_ldef), lthy') =
+    val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
-    val perm_frees =
-      (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
     val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
     val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
     val perms_name = space_implode "_" perm_names'
     val perms_zero_bind = Binding.name (perms_name ^ "_zero")
     val perms_append_bind = Binding.name (perms_name ^ "_append")
-    fun tac _ perm_thms =
-      (Class.intro_classes_tac []) THEN (ALLGOALS (
-        simp_tac (HOL_ss addsimps perm_thms
-      )));
-    fun morphism phi = map (Morphism.thm phi);
+    fun tac _ (_, simps, _) =
+      (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));
+    fun morphism phi (dfs, simps, fvs) =
+      (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   in
   lthy'
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
-  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms)
+  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
   end
 
 *}
 
+ML {*
+fun define_lifted_perms full_tnames name_term_pairs thms thy =
+let
+  val lthy =
+    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
+  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+    (ALLGOALS (resolve_tac lifted_thms))
+  val lthy'' = Class.prove_instantiation_instance tac lthy'
+in
+  Local_Theory.exit_global lthy''
+end
+*}
+
 (* Test
 atom_decl name
 

--- a/Nominal/Terms.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 07:48:57 2010 +0100
@@ -65,14 +65,14 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-  apply (simp_all add: atom_eqvt eqvts)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma fv_rtrm1_eqvt[eqvt]:
     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
   apply (induct t and b)
-  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma alpha1_eqvt:
@@ -80,40 +80,12 @@
   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
   apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
   apply (simp_all add:eqvts alpha1_inj)
-  apply (erule exE)
-  apply (rule_tac x="pi \<bullet> pia" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (erule exE)
-  apply (erule exE)
-  apply (rule conjI)
-  apply (rule_tac x="pi \<bullet> pia" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (rule_tac x="pi \<bullet> piaa" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
@@ -150,18 +122,8 @@
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 
-instantiation trm1 and bp :: pt
-begin
-
-quotient_definition
-  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
-
-instance by default 
-  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
+  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
 
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
@@ -463,45 +425,30 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
-lemma rbv5_eqvt:
+lemma rbv5_eqvt[eqvt]:
   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
-sorry
+  apply (induct x)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
-lemma fv_rtrm5_eqvt:
+lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
-sorry
-
-lemma fv_rlts_eqvt:
-  "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"
-sorry
+  "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+  apply (induct x and l)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
 lemma alpha5_eqvt:
   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
   apply (simp_all add: alpha5_inj)
-  apply (erule exE)+
-  apply(unfold alpha_gen)
-  apply (erule conjE)+
-  apply (rule conjI)
-  apply (rule_tac x="x \<bullet> pi" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
-  apply (rule_tac x="x \<bullet> pia" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),