--- a/Quot/Nominal/Fv.thy	Thu Feb 18 15:03:09 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Thu Feb 18 18:33:53 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms"
+imports "Nominal2_Atoms" "Abs"
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -80,12 +80,19 @@
   (* Copy from Term *)
   fun is_funtype (Type ("fun", [_, _])) = true
     | is_funtype _ = false;
+  (* Similar to one in USyntax *)
+  fun mk_pair (fst, snd) =
+    let val ty1 = fastype_of fst
+      val ty2 = fastype_of snd
+      val c = HOLogic.pair_const ty1 ty2
+    in c $ fst $ snd
+    end;
+
 *}
 
-
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
-fun define_raw_fv full_tname bindsall lthy =
+fun define_fv_alpha full_tname bindsall lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr, ...} = Datatype.the_info thy full_tname;
@@ -95,19 +102,26 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
-  fun fv_eq_constr i (cname, dts) bindcs =
+  val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
+    "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
+  val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
+  val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  fun fv_alpha_constr i (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
+      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+      val args2 = map Free (names2 ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
       val fv_c = nth fv_frees i;
-      fun fv_bind (NONE, i) =
+      val alpha = nth alpha_frees i;
+      fun fv_bind args (NONE, i) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             (* TODO we assume that all can be 'atomized' *)
             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
             mk_single_atom (nth args i)
-        | fv_bind (SOME f, i) = f $ (nth args i);
+        | fv_bind args (SOME f, i) = f $ (nth args i);
       fun fv_arg ((dt, x), bindxs) =
         let
           val arg =
@@ -115,70 +129,64 @@
             (* TODO: we just assume everything can be 'atomized' *)
             if (is_funtype o fastype_of) x then mk_atoms x else
             HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
-          val sub = mk_union (map fv_bind bindxs)
+          val sub = mk_union (map (fv_bind args) bindxs)
         in
           mk_diff arg sub
         end;
-        val _ = tracing ("d" ^ string_of_int (length dts));
-        val _ = tracing (string_of_int (length args));
-        val _ = tracing (string_of_int (length bindcs));
+      val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
+        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
+      val alpha_rhs =
+        HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
+      fun alpha_arg ((dt, bindxs), (arg, arg2)) =
+        if bindxs = [] then (
+          if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+          else (HOLogic.mk_eq (arg, arg2)))
+        else
+          if is_rec_type dt then let
+            (* THE HARD CASE *)
+            val lhs_binds = mk_union (map (fv_bind args) bindxs);
+            val lhs = mk_pair (lhs_binds, arg);
+            val rhs_binds = mk_union (map (fv_bind args2) bindxs);
+            val rhs = mk_pair (rhs_binds, arg2);
+            val alpha = nth alpha_frees (body_index dt);
+            val fv = nth fv_frees (body_index dt);
+            val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
+            val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
+          in
+            HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
+          (* TODO Add some test that is makes sense *)
+          end else @{term "True"}
+      val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
+      val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
     in
-      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
+      (fv_eq, alpha_eq)
     end;
-  fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
-  val fv_eqs = flat (map2 fv_eq descr bindsall)
+  fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
+  val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+  val add_binds = map (fn x => (Attrib.empty_binding, x))
+  val (fvs, lthy') = (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
+  val (alphas, lthy'') = (Inductive.add_inductive_i
+     {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
+     (add_binds alpha_eqs) [] lthy')
 in
-  (* The snd will be removed later *)
-  snd (Primrec.add_primrec
-    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+  ((fvs, alphas), lthy'')
 end
 *}
 
-ML {*
-fun define_alpha full_tname bindsall lthy =
-let
-  val thy = ProofContext.theory_of lthy;
-  val {descr, ...} = Datatype.the_info thy full_tname;
-  val sorts = []; (* TODO *)
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
-    "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
-  val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
-  val alpha_frees = map Free (alpha_names ~~ alpha_types);
-  fun alpha_eq_constr i (cname, dts) bindcs =
-    let
-      val Ts = map (typ_of_dtyp descr sorts) dts;
-      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
-      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
-      val args = map Free (names ~~ Ts);
-      val args2 = map Free (names2 ~~ Ts);
-      val c = Const (cname, Ts ---> (nth_dtyp i));
-      val alpha = nth alpha_frees i;
-    in
-      (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))))
-    end;
-  fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds;
-  val alpha_eqs = flat (map2 alpha_eq descr bindsall)
-in
-  (* The snd will be removed later *)
-  snd (Inductive.add_inductive_i
-     {quiet_mode = false, verbose = true, alt_name = Binding.empty,
-      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
-     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] (alpha_eqs) [] lthy)
-end
-*}
-
+(* tests
 atom_decl name
 
-(*datatype ty =
+datatype ty =
   Var "name set"
 
 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
 
-local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *}
+local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
 print_theorems
-*)
+
 
 datatype rtrm1 =
   rVr1 "name"
@@ -199,15 +207,12 @@
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
 
-local_setup {* define_raw_fv "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
+
+local_setup {* define_fv_alpha "Fv.rtrm1"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
    [[], [[]], [[], []]]] *}
 print_theorems
-
-local_setup {* define_alpha "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
-   [[], [[]], [[], []]]] *}
-print_theorems
-
+*)
 
 end

--- a/Quot/Nominal/Terms.thy	Thu Feb 18 15:03:09 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 18:33:53 2010 +0100
@@ -27,34 +27,52 @@
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
-local_setup {* define_raw_fv "Terms.rtrm1"
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
+
+local_setup {* snd o define_fv_alpha "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
    [[], [[]], [[], []]]] *}
 print_theorems
-
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
-
-inductive
-  alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
-| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
-| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
-| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
+notation
+  alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
+  alpha_bp ("_ \<approx>1b _" [100, 100] 100)
+thm alpha_rtrm1_alpha_bp.intros
 
 lemma alpha1_inj:
 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
-"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))"
-"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))"
+"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))"
+"(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) =
+   ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and>
+   (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))"
+"alpha_bp BUnit BUnit"
+"(alpha_bp (BVr name) (BVr namea)) = (name = namea)"
+"(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)"
 apply -
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
 done
 
-(* Shouyld we derive it? But bv is given by the user? *)
+lemma alpha_bp_refl: "alpha_bp a a"
+apply induct
+apply (simp_all  add: alpha1_inj)
+done
+
+lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
+apply rule
+apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
+apply (simp_all add: alpha_bp_refl)
+done
+
+lemma alpha_bp_eq: "alpha_bp = (op =)"
+apply (rule ext)+
+apply (rule alpha_bp_eq_eq)
+done
+
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
@@ -68,10 +86,10 @@
   apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
   done
 
-
 lemma alpha1_eqvt:
-  shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
-  apply (induct t s rule: alpha1.inducts)
+  "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
+  "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)
@@ -85,6 +103,8 @@
   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)+
@@ -95,12 +115,22 @@
   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])
   done
 
-lemma alpha1_equivp: "equivp alpha1" 
+lemma alpha1_equivp: "equivp alpha_rtrm1" 
   sorry
 
-quotient_type trm1 = rtrm1 / alpha1
+quotient_type trm1 = rtrm1 / alpha_rtrm1
   by (rule alpha1_equivp)
 
 local_setup {*
@@ -115,28 +145,30 @@
 
 lemma alpha_rfv1:
   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
-  apply(induct rule: alpha1.induct)
+  apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
   apply(simp_all add: alpha_gen.simps)
-  sorry
+  done
 
 lemma [quot_respect]:
- "(op = ===> alpha1) rVr1 rVr1"
- "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
- "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
- "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+ "(op = ===> alpha_rtrm1) rVr1 rVr1"
+ "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
 apply (auto simp add: alpha1_inj)
 apply (rule_tac x="0" in exI)
 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
 apply (rule_tac x="0" in exI)
+apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
+apply (rule_tac x="0" in exI)
 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
 done
 
 lemma [quot_respect]:
-  "(op = ===> alpha1 ===> alpha1) permute permute"
+  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
   by (simp add: alpha1_eqvt)
 
 lemma [quot_respect]:
-  "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
+  "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
   by (simp add: alpha_rfv1)
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
@@ -215,6 +247,12 @@
 apply(simp_all)
 done
 
+lemma helper: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
+apply auto
+apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
+apply auto
+done
+
 lemma supp_fv:
   shows "supp t = fv_trm1 t"
 apply(induct t rule: trm1_bp_inducts(1))
@@ -233,11 +271,11 @@
 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
 apply(simp (no_asm) add: supp_def)
-apply(simp add: alpha1_INJ)
+apply(simp add: alpha1_INJ alpha_bp_eq)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
+apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
+apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper)
 done
 
 lemma trm1_supp:
@@ -271,35 +309,27 @@
 where
   "rbv2 (rAs x t) = {atom x}"
 
-local_setup {* define_raw_fv "Terms.rtrm2"
+setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
+
+local_setup {* snd o define_fv_alpha "Terms.rtrm2"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
    [[[], []]]] *}
 print_theorems
 
-setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
-
-inductive
-  alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
-and
-  alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
-| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
-        \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
-        \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
-| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
+notation
+  alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
+  alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
+thm alpha_rtrm2_alpha_rassign.intros
 
 lemma alpha2_equivp:
-  "equivp alpha2"
-  "equivp alpha2a"
+  "equivp alpha_rtrm2"
+  "equivp alpha_rassign"
   sorry
 
 quotient_type
-  trm2 = rtrm2 / alpha2
+  trm2 = rtrm2 / alpha_rtrm2
 and
-  assign = rassign / alpha2a
+  assign = rassign / alpha_rassign
   by (auto intro: alpha2_equivp)
 
 local_setup {*
@@ -333,36 +363,27 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
-local_setup {* define_raw_fv "Terms.trm3"
+setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
+
+local_setup {* snd o define_fv_alpha "Terms.trm3"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
    [[], [[], [], []]]] *}
 print_theorems
 
-setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
-
-inductive
-  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
-and
-  alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
-| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
-        \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
-        \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
-| a5: "ANil \<approx>3a ANil"
-| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
+notation
+  alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and
+  alpha_assigns ("_ \<approx>3a _" [100, 100] 100)
+thm alpha_trm3_alpha_assigns.intros
 
 lemma alpha3_equivp:
-  "equivp alpha3"
-  "equivp alpha3a"
+  "equivp alpha_trm3"
+  "equivp alpha_assigns"
   sorry
 
 quotient_type
-  qtrm3 = trm3 / alpha3
+  qtrm3 = trm3 / alpha_trm3
 and
-  qassigns = assigns / alpha3a
+  qassigns = assigns / alpha_assigns
   by (auto intro: alpha3_equivp)
 
 
@@ -376,10 +397,6 @@
 
 thm trm4.recs
 
-local_setup {* define_raw_fv "Terms.trm4" [
-  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
-print_theorems
-
 (* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
 setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
@@ -395,22 +412,21 @@
 thm permute_trm4_permute_trm4_list.simps
 thm permute_trm4_permute_trm4_list.simps[simplified repaired]
 
-inductive
-    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
-and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 
-where
-  a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
-| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
-| a5: "[] \<approx>4list []"
-| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
+local_setup {* snd o define_fv_alpha "Terms.trm4" [
+  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+print_theorems
 
-lemma alpha4_equivp: "equivp alpha4" sorry
-lemma alpha4list_equivp: "equivp alpha4list" sorry
+notation
+  alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and
+  alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_trm4_alpha_trm4_list.intros
+
+lemma alpha4_equivp: "equivp alpha_trm4" sorry
+lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry
 
 quotient_type 
-  qtrm4 = trm4 / alpha4 and
-  qtrm4list = "trm4 list" / alpha4list
+  qtrm4 = trm4 / alpha_trm4 and
+  qtrm4list = "trm4 list" / alpha_trm4_list
   by (simp_all add: alpha4_equivp alpha4list_equivp)
 
 
@@ -429,66 +445,55 @@
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
 
-local_setup {* define_raw_fv "Terms.rtrm5" [
+setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
+print_theorems
+
+local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
 print_theorems
 
 (* Alternate version with additional binding of name in rlts in rLcons *)
-(*local_setup {* define_raw_fv "Terms.rtrm5" [
+(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
 print_theorems*)
 
-
-setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
-print_theorems
-
-inductive
-  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
-and
-  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
-| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
-| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2)); 
-        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk>
-        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
-| a4: "rLnil \<approx>l rLnil"
-| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
-
-print_theorems
+notation
+  alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
+  alpha_rlts ("_ \<approx>l _" [100, 100] 100)
+thm alpha_rtrm5_alpha_rlts.intros
 
 lemma alpha5_inj:
   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
-  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
-         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))"
+  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
+         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))"
   "rLnil \<approx>l rLnil"
   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
 apply -
-apply (simp_all add: alpha5_alphalts.intros)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
 apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
 apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
 apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
 apply rule
-apply (erule alphalts.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rlts.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
 done
 
 lemma alpha5_equivps:
-  shows "equivp alpha5"
-  and   "equivp alphalts"
+  shows "equivp alpha_rtrm5"
+  and   "equivp alpha_rlts"
 sorry
 
 quotient_type
-  trm5 = rtrm5 / alpha5
+  trm5 = rtrm5 / alpha_rtrm5
 and
-  lts = rlts / alphalts
+  lts = rlts / alpha_rlts
   by (auto intro: alpha5_equivps)
 
 local_setup {*
@@ -519,13 +524,13 @@
 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: alpha5_alphalts.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_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)
@@ -534,7 +539,7 @@
   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 (rule_tac x="x \<bullet> pia" in exI)
+  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)
@@ -548,27 +553,27 @@
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
   "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
-  apply(induct rule: alpha5_alphalts.inducts)
+  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
   apply(simp_all add: alpha_gen)
   done
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
-  apply(induct rule: alpha5_alphalts.inducts(2))
+  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
   apply(simp_all)
   done
 
 lemma [quot_respect]:
-  "(alphalts ===> op =) fv_rlts fv_rlts"
-  "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5"
-  "(alphalts ===> op =) rbv5 rbv5"
-  "(op = ===> alpha5) rVr5 rVr5"
-  "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
-  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
-  "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
-  "(op = ===> alpha5 ===> alpha5) permute permute"
-  "(op = ===> alphalts ===> alphalts) permute permute"
+  "(alpha_rlts ===> op =) fv_rlts fv_rlts"
+  "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
+  "(alpha_rlts ===> op =) rbv5 rbv5"
+  "(op = ===> alpha_rtrm5) rVr5 rVr5"
+  "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
+  "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
+  "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
+  "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
+  "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
+  "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
   apply (clarify) apply (rule conjI)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
@@ -579,7 +584,7 @@
   done
 
 lemma
-  shows "(alphalts ===> op =) rbv5 rbv5"
+  shows "(alpha_rlts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)
 
 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
@@ -668,7 +673,7 @@
 lemma distinct_helper:
   shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
   apply auto
-  apply (erule alpha5.cases)
+  apply (erule alpha_rtrm5.cases)
   apply (simp_all only: rtrm5.distinct)
   done
 
@@ -701,13 +706,15 @@
 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
 
-local_setup {* define_raw_fv "Terms.rtrm6" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
-print_theorems 
-
 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
 print_theorems
 
+local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
+notation alpha_rtrm6 ("_ \<approx>6a _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rtrm6.intros
+
 inductive
   alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
 where
@@ -841,13 +848,16 @@
 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
 
-local_setup {* define_raw_fv "Terms.rtrm7" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
-print_theorems 
-
 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
 print_theorems
 
+local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
+notation
+  alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rtrm7.intros
+
 inductive
   alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
 where
@@ -884,13 +894,18 @@
   "rbv8 (Bar0 x) = {}"
 | "rbv8 (Bar1 v x b) = {atom v}"
 
-local_setup {* define_raw_fv "Terms.rfoo8" [
-  [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
-print_theorems 
-
 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
 print_theorems
 
+local_setup {* snd o define_fv_alpha "Terms.rfoo8" [
+  [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+  alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
+  alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
+(* HERE THE RULE DIFFERS *)
+thm alpha_rfoo8_alpha_rbar8.intros
+
+
 inductive
   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
 and
@@ -941,12 +956,17 @@
   "rbv9 (Var9 x) = {}"
 | "rbv9 (Lam9 x b) = {atom x}"
 
-local_setup {* define_raw_fv "Terms.rlam9" [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
+setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
 print_theorems
 
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
-print_theorems
+local_setup {* snd o define_fv_alpha "Terms.rlam9" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
+notation
+  alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
+  alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rlam9_alpha_rbla9.intros
+
 
 inductive
   alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)