diff -r ffd5540ac2e9 -r b66d754bf1c2 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 15 17:51:35 2010 +0100
@@ -2,45 +2,145 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
 begin
 
-(* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+lemma permute_boolI:
+  fixes P::"bool"
+  shows "p \<bullet> P \<Longrightarrow> P"
+apply(simp add: permute_bool_def)
+done
+
+lemma permute_boolE:
+  fixes P::"bool"
+  shows "P \<Longrightarrow> p \<bullet> P"
+apply(simp add: permute_bool_def)
+done
 
+fun
+  alpha_tst
+where
+  alpha_tst[simp del]:
+  "alpha_tst (bs, x) R bv bv' fv p (cs, y) \<longleftrightarrow> 
+     fv x - bv bs = fv y - bv' cs \<and> 
+     (fv x - bv bs) \<sharp>* p \<and> 
+     R (p \<bullet> x) y \<and> 
+     (p \<bullet> bv bs) = bv' cs"
+
+notation
+  alpha_tst ("_ \<approx>tst _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
+
+(*
+fun
+  alpha_tst_rec
+where
+  alpha_tst_rec[simp del]:
+  "alpha_tst_rec (bs, x) R1 R2 bv fv p (cs, y) \<longleftrightarrow> 
+     fv x - bv bs = fv y - bv cs \<and> 
+     (fv x - bv bs) \<sharp>* p \<and> 
+     R1 (p \<bullet> x) y \<and> 
+     R2 (p \<bullet> bs) cs \<and> 
+     (p \<bullet> bv bs) = bv cs"
+
+notation
+  alpha_tst_rec ("_ \<approx>tstrec _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
+*)
 
 fun
   alpha_gen 
 where
   alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
-     f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs"
+  "alpha_gen (bs, x) R fv pi (cs, y) \<longleftrightarrow> 
+     fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
 
-lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
-  by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
+fun
+  alpha_res
+where
+  alpha_res[simp del]:
+  "alpha_res (bs, x) R fv pi (cs, y) \<longleftrightarrow> 
+     fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+
+notation
+  alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100)
+
+fun
+  alpha_lst
+where
+  alpha_lst[simp del]:
+  "alpha_lst (bs, x) R fv pi (cs, y) \<longleftrightarrow> 
+     fv x - set bs = fv y - set cs \<and> (fv x - set bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+
+notation
+  alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
+
+
+lemma [mono]: 
+  shows "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
+  and   "R1 \<le> R2 \<Longrightarrow> alpha_res x R1 \<le> alpha_res x R2"
+apply(case_tac [!] x) 
+apply(auto simp add: le_fun_def le_bool_def alpha_gen.simps alpha_res.simps)
+done
 
 lemma alpha_gen_refl:
   assumes a: "R x x"
-  shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+  shows "(bs, x) \<approx>gen R fv 0 (bs, x)"
   using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
 
+lemma alpha_gen_refl_tst:
+  assumes a: "R1 x x" "bv bs = bv' bs"
+  shows "(bs, x) \<approx>tst R1 bv bv' fv 0 (bs, x)"
+  using a 
+  apply (simp add: alpha_tst fresh_star_def fresh_zero_perm)
+  done
+  
+
 lemma alpha_gen_sym:
-  assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
+  assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
-  using a b 
-  by (auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  shows "(cs, y) \<approx>gen R fv (- p) (bs, x)"
+  using a
+  apply(auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  apply(simp add: b)
+  done  
+  
+lemma alpha_gen_sym_tst:
+  assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
+  and     b: "R1 (p \<bullet> x) y \<Longrightarrow> R1 (- p \<bullet> y) x"
+  shows "(cs, y) \<approx>tst R1 bv' bv fv (- p) (bs, x)"
+  using a
+  apply(auto simp add: alpha_tst fresh_star_def fresh_def supp_minus_perm)
+  apply(simp add: b)
+  apply(rule_tac p="p" in permute_boolI)
+  apply(simp add: mem_eqvt)
+  apply(rule_tac p="- p" in permute_boolI)
+  apply(simp add: mem_eqvt)
+  apply(rotate_tac 3)
+  apply(drule sym)
+  apply(simp)
+  done  
 
 lemma alpha_gen_trans:
-  assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
-  and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
-  and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
-  shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
+  assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
+  and     b: "(cs, y) \<approx>gen R fv q (ds, z)"
+  and     c: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+  shows "(bs, x) \<approx>gen R fv (q + p) (ds, z)"
   using a b c 
   using supp_plus_perm
   apply(simp add: alpha_gen fresh_star_def fresh_def)
   apply(blast)
   done
 
+lemma alpha_gen_trans_tst:
+  assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
+  and     b: "(cs, y) \<approx>tst R1 bv' bv'' fv q (ds, z)"
+  and     c: "\<lbrakk>R1 (p \<bullet> x) y; R1 (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R1 ((q + p) \<bullet> x) z"
+  shows "(bs, x) \<approx>tst R1 bv bv'' fv (q + p) (ds, z)"
+  using a b c
+  using supp_plus_perm
+  apply(simp add: alpha_tst fresh_star_def fresh_def)
+  apply(blast)
+  done
+
 lemma alpha_gen_eqvt:
   assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
   and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
@@ -54,72 +154,40 @@
   apply(clarsimp)
   done
 
-lemma alpha_gen_compose_sym:
-  fixes pi
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
-  using b apply -
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(clarify)
-  apply(simp)
-  apply(rule a)
-  apply assumption
+lemma alpha_gen_eqvt_tst:
+  assumes a: "(bs, x) \<approx>tst R1 bv bv' fv q (cs, y)"
+  and     b1: "R1 (q \<bullet> x) y \<Longrightarrow> R1 (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+  and     c: "p \<bullet> (fv x) = fv (p \<bullet> x)"
+  and     d: "p \<bullet> (fv y) = fv (p \<bullet> y)"
+  and     e: "p \<bullet> (bv bs) = bv (p \<bullet> bs)"
+  and     f: "p \<bullet> (bv cs) = bv (p \<bullet> cs)"
+  and     e': "p \<bullet> (bv' bs) = bv' (p \<bullet> bs)"
+  and     f': "p \<bullet> (bv' cs) = bv' (p \<bullet> cs)"
+  shows "(p \<bullet> bs, p \<bullet> x) \<approx>tst R1 bv bv' fv (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  using a b1
+  apply(simp add: alpha_tst c[symmetric] d[symmetric] 
+    e'[symmetric] f'[symmetric] e[symmetric] f[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: permute_eqvt[symmetric])
+  apply(simp add: fresh_star_permute_iff)
+  apply(clarsimp)
   done
 
-lemma alpha_gen_compose_trans:
-  fixes pi pia
-  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
-  using b c apply -
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(simp add: fresh_star_plus)
-  apply(drule_tac x="- pia \<bullet> sa" in spec)
-  apply(drule mp)
-  apply(rotate_tac 5)
-  apply(drule_tac pi="- pia" in a)
-  apply(simp)
-  apply(rotate_tac 7)
-  apply(drule_tac pi="pia" in a)
-  apply(simp)
-  done
-
-lemma alpha_gen_compose_eqvt:
-  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  "(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(simp add: alpha_gen.simps)
-  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 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 c[symmetric])
-  apply(subst permute_eqvt[symmetric])
-  apply(simp)
-  oops
-
 fun
   alpha_abs 
 where
-  "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+  "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
 notation
   alpha_abs ("_ \<approx>abs _")
 
+fun
+  alpha_abs_tst
+where
+  "alpha_abs_tst (bv, bs, x) (bv',cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op=) bv bv' supp p (cs, y))"
+
+notation
+  alpha_abs_tst ("_ \<approx>abstst _")
+
 lemma alpha_abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -137,14 +205,15 @@
   apply(simp add: supp_swap)
   done
 
-lemma alpha_gen_swap_fun:
-  assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
-  assumes a1: "a \<notin> (f x) - bs"
-  and     a2: "b \<notin> (f x) - bs"
-  shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
+lemma alpha_abs_tst_swap:
+  assumes a1: "a \<notin> (supp x) - bv bs"
+  and     a2: "b \<notin> (supp x) - bv bs"
+  shows "(bv, bs, x) \<approx>abstst ((a \<rightleftharpoons> b) \<bullet> bv, (a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
+  apply(simp)
   apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
-  apply(simp add: alpha_gen)
-  apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
+  unfolding alpha_tst
+  apply(simp)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric])
   apply(simp add: swap_set_not_in[OF a1 a2])
   apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
   using a1 a2
@@ -155,9 +224,14 @@
 
 fun
   supp_abs_fun
-where
+  where
   "supp_abs_fun (bs, x) = (supp x) - bs"
 
+fun
+  supp_abstst_fun::"('b::pt \<Rightarrow> atom set) \<times> 'b \<times> ('a::pt) \<Rightarrow> atom set" 
+  where
+  "supp_abstst_fun (bv, bs, x) = (supp x - bv bs)"
+
 lemma supp_abs_fun_lemma:
   assumes a: "x \<approx>abs y" 
   shows "supp_abs_fun x = supp_abs_fun y"
@@ -165,6 +239,14 @@
   apply(induct rule: alpha_abs.induct)
   apply(simp add: alpha_gen)
   done
+
+lemma supp_abstst_fun_lemma:
+  assumes a: "(bv, bs, x) \<approx>abstst (bv', cs, y)"
+  shows "supp_abstst_fun (bv, bs, x) = supp_abstst_fun (bv', cs, y)"
+  using a
+  apply(induct x\<equiv>"(bv, bs, x)" y\<equiv>"(bv', cs, y)" rule: alpha_abs_tst.induct)
+  apply(simp add: alpha_tst)
+  done
   
 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
   apply(rule equivpI)
@@ -190,11 +272,49 @@
   apply(simp)
   done
 
+term "alpha_abs_tst"
+
+quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst"
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(simp_all)
+  (* refl *)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_refl_tst)
+  apply(simp)
+  apply(simp)
+  (* symm *)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_sym_tst)
+  apply(assumption)
+  apply(clarsimp)
+  (* trans *)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_trans_tst)
+  apply(assumption)
+  apply(assumption)
+  apply(simp)
+  done
+
+
 quotient_definition
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
+fun
+  Pair_tst
+where
+  "Pair_tst a b c = (a, b, c)"
+
+quotient_definition
+  "Abs_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> ('b, 'a) abs_tst"
+is
+  "Pair_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> (('b \<Rightarrow> atom set) \<times> 'b \<times> 'a)"
+
 lemma [quot_respect]:
   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
   apply(clarsimp)
@@ -204,6 +324,22 @@
   done
 
 lemma [quot_respect]:
+  shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
+  apply(clarsimp)
+  apply(rule exI)
+  apply(rule alpha_gen_refl_tst)
+  apply(simp_all)
+  done
+
+lemma [quot_respect]:
+  shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
+  apply(clarsimp)
+  apply(rule exI)
+  apply(rule alpha_gen_refl_tst)
+  apply(simp_all)
+  done
+
+lemma [quot_respect]:
   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
   apply(clarsimp)
   apply(rule exI)
@@ -217,11 +353,23 @@
   apply(simp add: supp_abs_fun_lemma)
   done
 
+lemma [quot_respect]:
+  shows "(alpha_abs_tst ===> (op =)) supp_abstst_fun supp_abstst_fun"
+  apply(simp)
+  apply(clarify)
+  apply(simp add: alpha_tst.simps)
+  sorry
+
+
 lemma abs_induct:
   "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
   done
 
+lemma abs_tst_induct:
+  "\<lbrakk>\<And>bv as (x::'a::pt). P (Abs_tst bv as x)\<rbrakk> \<Longrightarrow> P t"
+  sorry
+
 (* TEST case *)
 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
 thm abs_induct abs_induct2
@@ -247,14 +395,56 @@
 
 end
 
+instantiation abs_tst :: (pt, pt) pt
+begin
+
+quotient_definition
+  "permute_abs_tst::perm \<Rightarrow> (('a::pt, 'b::pt) abs_tst) \<Rightarrow> ('a, 'b) abs_tst"
+is
+  "permute:: perm \<Rightarrow> ((('a::pt) \<Rightarrow> atom set) \<times> 'a \<times> 'b::pt) \<Rightarrow> (('a \<Rightarrow> atom set) \<times> 'a \<times> 'b)"
+
+lemma permute_ABS_tst [simp]:
+  fixes x::"'a::pt"  
+  shows "(p \<bullet> (Abs_tst bv as x)) = Abs_tst (p \<bullet> bv) (p \<bullet> as) (p \<bullet> x)"
+  sorry
+
+instance
+  apply(default)
+  apply(induct_tac [!] x rule: abs_tst_induct)
+  apply(simp_all)
+  done
+
+end
+
 quotient_definition
   "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
 is
   "supp_abs_fun"
 
+term supp_abstst_fun
+
+quotient_definition
+  "supp_Abstst_fun :: ('a::pt, 'b::pt) abs_tst \<Rightarrow> atom \<Rightarrow> bool"
+is
+  "supp_abstst_fun :: (('a::pt \<Rightarrow> atom \<Rightarrow> bool) \<times> 'a \<times> 'b::pt) \<Rightarrow> atom \<Rightarrow> bool"
+(* leave out type *)
+
 lemma supp_Abs_fun_simp:
   shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
   by (lifting supp_abs_fun.simps(1))
+thm supp_abs_fun.simps(1)
+
+term supp_Abs_fun
+term supp_Abstst_fun
+
+lemma supp_Abs_tst_fun_simp:
+  fixes bv::"'b::pt \<Rightarrow> atom set"
+  shows "supp_Abstst_fun (Abs_tst bv bs x) = (supp x) - (bv bs)"
+sorry
+(* PROBLEM: regularisation fails
+  by (lifting supp_abstst_fun.simps(1))
+*)
+
 
 lemma supp_Abs_fun_eqvt [eqvt]:
   shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
@@ -262,6 +452,13 @@
   apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
   done
 
+lemma supp_Abs_test_fun_eqvt [eqvt]:
+  shows "(p \<bullet> supp_Abstst_fun x) = supp_Abstst_fun (p \<bullet> x)"
+  apply(induct_tac x rule: abs_tst_induct)
+  apply(simp add: supp_Abs_tst_fun_simp supp_eqvt Diff_eqvt)
+  apply(simp add: eqvt_apply)
+  done
+
 lemma supp_Abs_fun_fresh:
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
   apply(rule fresh_fun_eqvt_app)
@@ -269,14 +466,36 @@
   apply(simp)
   done
 
+
+lemma supp_Abs_tst_fun_fresh:
+  shows "a \<sharp> Abs_tst bv bs x \<Longrightarrow> a \<sharp> supp_Abstst_fun (Abs_tst bv bs x)"
+  apply(rule fresh_fun_eqvt_app)
+  apply(simp add: eqvts_raw)
+  apply(simp)
+  done
+
 lemma Abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
   shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
-  using a1 a2 by (lifting alpha_abs_swap)
+  using a1 a2 
+  by (lifting alpha_abs_swap)
+
+thm alpha_abs_swap
+thm alpha_abs_tst_swap
+
+lemma Abs_tst_swap:
+  assumes a1: "a \<notin> (supp x) - bv bs"
+  and     a2: "b \<notin> (supp x) - bv bs"
+  shows "(Abs_tst bv bs x) = (Abs_tst ((a \<rightleftharpoons> b) \<bullet> bv) ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
+  using a1 a2
+  sorry
+(* PROBLEM
+  by (lifting alpha_abs_tst_swap)
+*)
 
 lemma Abs_supports:
-  shows "((supp x) - as) supports (Abs as x)"
+  shows "(supp x - as) supports (Abs as x)"
   unfolding supports_def
   apply(clarify)
   apply(simp (no_asm))
@@ -284,6 +503,15 @@
   apply(simp_all)
   done
 
+lemma Abs_tst_supports:
+  shows "(supp x - bv as) supports (Abs_tst bv as x)"
+  unfolding supports_def
+  apply(clarify)
+  apply(simp (no_asm))
+  apply(subst Abs_tst_swap[symmetric])
+  apply(simp_all)
+  done
+
 lemma supp_Abs_subset1:
   fixes x::"'a::fs"
   shows "(supp x) - as \<subseteq> supp (Abs as x)"
@@ -295,6 +523,17 @@
   apply(simp add: supp_finite_atom_set finite_supp)
   done
 
+lemma supp_Abs_tst_subset1:
+  fixes x::"'a::fs"
+  shows "(supp x - bv as) \<subseteq> supp (Abs_tst bv as x)"
+  apply(simp add: supp_conv_fresh)
+  apply(auto)
+  apply(drule_tac supp_Abs_tst_fun_fresh)
+  apply(simp only: supp_Abs_tst_fun_simp)
+  apply(simp add: fresh_def)
+  apply(simp add: supp_finite_atom_set finite_supp)
+  done
+
 lemma supp_Abs_subset2:
   fixes x::"'a::fs"
   shows "supp (Abs as x) \<subseteq> (supp x) - as"
@@ -303,6 +542,14 @@
   apply(simp add: finite_supp)
   done
 
+lemma supp_Abs_tst_subset2:
+  fixes x::"'a::fs"
+  shows "supp (Abs_tst bv as x) \<subseteq> (supp x - bv as)"
+  apply(rule supp_is_subset)
+  apply(rule Abs_tst_supports)
+  apply(simp add: finite_supp)
+  done
+
 lemma supp_Abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
@@ -311,6 +558,14 @@
   apply(rule supp_Abs_subset1)
   done
 
+lemma supp_Abs_tst:
+  fixes x::"'a::fs"
+  shows "supp (Abs_tst bv as x) = (supp x - bv as)"
+  apply(rule_tac subset_antisym)
+  apply(rule supp_Abs_tst_subset2)
+  apply(rule supp_Abs_tst_subset1)
+  done
+
 instance abs :: (fs) fs
   apply(default)
   apply(induct_tac x rule: abs_induct)
@@ -318,6 +573,13 @@
   apply(simp add: finite_supp)
   done
 
+instance abs_tst :: (pt, fs) fs
+  apply(default)
+  apply(induct_tac x rule: abs_tst_induct)
+  apply(simp add: supp_Abs_tst)
+  apply(simp add: finite_supp)
+  done
+
 lemma Abs_fresh_iff:
   fixes x::"'a::fs"
   shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
@@ -326,10 +588,26 @@
   apply(auto)
   done
 
+lemma Abs_tst_fresh_iff:
+  fixes x::"'a::fs"
+  shows "a \<sharp> Abs_tst bv bs x \<longleftrightarrow> a \<in> bv bs \<or> (a \<notin> bv bs \<and> a \<sharp> x)"
+  apply(simp add: fresh_def)
+  apply(simp add: supp_Abs_tst)
+  apply(auto)
+  done
+
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   by (lifting alpha_abs.simps(1))
 
+term alpha_tst
+
+lemma Abs_tst_eq_iff:
+  shows "Abs_tst bv bs x = Abs_tst bv cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op =) bv bv supp p (cs, y))"
+sorry
+(* PROBLEM  
+by (lifting alpha_abs_tst.simps(1))
+*)
 
 
 (* 
@@ -346,15 +624,6 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
-fun
-  alpha2
-where
-  "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"
-
-notation 
-  alpha2 ("_ \<approx>abs2 _")
-
-
 lemma
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -365,11 +634,12 @@
 apply(rule exI)
 apply(rule alpha_gen_refl)
 apply(simp)
+apply(simp)
 apply(rule_tac x="(a \<rightleftharpoons> b)" in  exI)
 apply(simp add: alpha_gen)
 apply(simp add: fresh_def)
 apply(rule conjI)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])
+apply(rule_tac p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])
 apply(rule trans)
 apply(simp add: Diff_eqvt supp_eqvt)
 apply(subst swap_set_not_in)
@@ -378,7 +648,7 @@
 apply(simp)
 apply(simp add: permute_set_eq)
 apply(simp add: eqvts)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
+apply(rule_tac p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
 apply(simp add: permute_self)
 apply(simp add: Diff_eqvt supp_eqvt)
 apply(simp add: permute_set_eq)
@@ -533,18 +803,6 @@
 apply (metis insert_Diff_single insert_absorb)
 done
 
-lemma permute_boolI:
-  fixes P::"bool"
-  shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
-  fixes P::"bool"
-  shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
 lemma kk:
   assumes a: "p \<bullet> x = y"
   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
@@ -673,12 +931,6 @@
 apply(simp)
 done
 
-fun
-  distinct_perms 
-where
-  "distinct_perms [] = True"
-| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
-
 (* support of concrete atom sets *)
 
 lemma atom_eqvt_raw:
@@ -701,11 +953,52 @@
 apply(simp add: atom_image_cong)
 done
 
-lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
-  apply (simp add: fresh_def)
-  apply (simp add: supp_atom_image)
-  apply (fold fresh_def)
-  apply (simp add: swap_fresh_fresh)
+lemma swap_atom_image_fresh: 
+  "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+apply (simp add: fresh_def)
+apply (simp add: supp_atom_image)
+apply (fold fresh_def)
+apply (simp add: swap_fresh_fresh)
+done
+
+
+(******************************************************)
+lemma alpha_gen_compose_sym:
+  fixes pi
+  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
+  using b 
+  apply -
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+  apply simp
+  apply(clarsimp)
+  apply(rule a)
+  apply assumption
+  done
+
+lemma alpha_gen_compose_trans:
+  fixes pi pia
+  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+  and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
+  using b c apply -
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa" in spec)
+  apply(drule mp)
+  apply(rotate_tac 5)
+  apply(drule_tac pi="- pia" in a)
+  apply(simp)
+  apply(rotate_tac 7)
+  apply(drule_tac pi="pia" in a)
+  apply(simp)
   done