diff -r fee2389789ad -r a5ba76208983 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Mar 20 02:46:07 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 20 04:51:26 2010 +0100
@@ -72,111 +72,34 @@
   by (auto simp add:  fresh_minus_perm)
 
 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)"
-  using a b c using supp_plus_perm
-  apply(simp add: alpha_gen fresh_star_def fresh_def)
-  apply(blast)
-  done
+  assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+  shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+  and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+  and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+  using a 
+  unfolding alphas
+  unfolding fresh_star_def
+  by (simp_all add: fresh_plus_perm)
 
 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)"
-  and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
-  and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
-  shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  using a b
-  apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: permute_eqvt[symmetric])
-  apply(simp add: fresh_star_permute_iff)
-  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)
-  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
-  done
-
-lemma alpha_gen_compose_sym2:
-  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
-  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
-  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
-  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+  assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+  and     b: "p \<bullet> (f x) = f (p \<bullet> x)"
+  and     c: "p \<bullet> (f y) = f (p \<bullet> y)"
+  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
+  unfolding alphas
+  unfolding set_eqvt[symmetric]
+  unfolding b[symmetric] c[symmetric]
+  unfolding Diff_eqvt[symmetric]
+  unfolding permute_eqvt[symmetric]
   using a
-  apply(simp add: alpha_gen)
-  apply clarify
-  apply (rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply (rule conjI)
-  apply (rotate_tac 3)
-  apply (drule_tac pi="- pi" in r1)
-  apply simp
-  apply (rule conjI)
-  apply (rotate_tac -1)
-  apply (drule_tac pi="- pi" in r2)
-  apply simp_all
-  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)
-  sorry
+  by (auto simp add: fresh_star_permute_iff)
 
 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 _")
@@ -185,17 +108,15 @@
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
   shows "(bs, x) \<approx>abs ((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: supp_eqvt[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: swap_set_not_in[OF a1 a2])
-  apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
   using a1 a2
-  apply(simp add: fresh_star_def fresh_def)
-  apply(blast)
-  apply(simp add: supp_swap)
-  done
+  unfolding Diff_iff
+  unfolding alpha_abs.simps
+  unfolding alphas
+  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+  unfolding fresh_star_def fresh_def
+  unfolding swap_set_not_in[OF a1 a2] 
+  by (rule_tac x="(a \<rightleftharpoons> b)" in exI)
+     (auto simp add: supp_perm swap_atom)
 
 lemma alpha_gen_swap_fun:
   assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
@@ -213,12 +134,12 @@
   apply(simp add: supp_swap)
   done
 
-
 fun
   supp_abs_fun
 where
   "supp_abs_fun (bs, x) = (supp x) - bs"
 
+
 lemma supp_abs_fun_lemma:
   assumes a: "x \<approx>abs y" 
   shows "supp_abs_fun x = supp_abs_fun y"
@@ -227,7 +148,8 @@
   apply(simp add: alpha_gen)
   done
   
-quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
+
+quotient_type 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(simp_all)
@@ -246,13 +168,11 @@
   apply(clarify)
   apply(rule_tac x="pa + p" in exI)
   apply(rule alpha_gen_trans)
-  apply(assumption)
-  apply(assumption)
-  apply(simp)
+  apply(auto)
   done
 
 quotient_definition
-  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
+  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
@@ -269,7 +189,6 @@
   apply(clarsimp)
   apply(rule exI)
   apply(rule alpha_gen_eqvt)
-  apply(assumption)
   apply(simp_all add: supp_eqvt)
   done
 
@@ -287,17 +206,19 @@
 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
 thm abs_induct abs_induct2
 
-instantiation abs :: (pt) pt
+instantiation abs_gen :: (pt) pt
 begin
 
 quotient_definition
-  "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
+  "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
+(* ??? has to be 'a \<dots> 'b does not work *)
 lemma permute_ABS [simp]:
-  fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)
+  fixes x::"'a::pt"  
   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+  thm permute_prod.simps
   by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
 
 instance
@@ -309,7 +230,7 @@
 end
 
 quotient_definition
-  "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
+  "supp_Abs_fun :: ('a::pt) abs_gen \<Rightarrow> atom \<Rightarrow> bool"
 is
   "supp_abs_fun"
 
@@ -379,7 +300,7 @@
   apply(simp add: finite_supp)
   done
 
-instance abs :: (fs) fs
+instance abs_gen :: (fs) fs
   apply(default)
   apply(induct_tac x rule: abs_induct)
   apply(simp add: supp_Abs)
@@ -765,12 +686,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 supp_atom_image:
@@ -807,5 +722,84 @@
 by (simp add: alpha_gen)
 
 
+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)
+  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
+  done
+
+lemma alpha_gen_compose_sym2:
+  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
+  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
+  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+  using a
+  apply(simp add: alpha_gen)
+  apply clarify
+  apply (rule conjI)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+  apply (rule conjI)
+  apply (rotate_tac 3)
+  apply (drule_tac pi="- pi" in r1)
+  apply simp
+  apply (rule conjI)
+  apply (rotate_tac -1)
+  apply (drule_tac pi="- pi" in r2)
+  apply simp_all
+  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)
+  sorry
+
 end