diff -r 480324a48a1c -r 66097fe4942a Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 08 13:13:20 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 08 13:50:52 2010 +0100
@@ -2,35 +2,37 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd"
 begin
 
-(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+(* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+lemma ball_image: 
+  shows "(\<forall>x \<in> p \<bullet> S. P x) = (\<forall>x \<in> S. P (p \<bullet> x))"
+apply(auto)
+apply(drule_tac x="p \<bullet> x" in bspec)
+apply(simp add: mem_permute_iff)
+apply(simp)
+apply(drule_tac x="(- p) \<bullet> x" in bspec)
+apply(rule_tac p1="p" in mem_permute_iff[THEN iffD1])
+apply(simp)
+apply(simp)
+done
+
 lemma fresh_star_plus:
   fixes p q::perm
   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
   unfolding fresh_star_def
   by (simp add: fresh_plus_perm)
 
-
 lemma fresh_star_permute_iff:
   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
 apply(simp add: fresh_star_def)
-apply(auto)
-apply(drule_tac x="p \<bullet> xa" in bspec)
-apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts del: permute_eqvt)
+apply(simp add: ball_image)
 apply(simp add: fresh_permute_iff)
-apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
-apply(simp)
-apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in mem_permute_iff[THEN iffD1])
-apply(simp)
-apply(simp)
 done
 
 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)"
+  "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"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
@@ -129,7 +131,6 @@
   apply(simp)
   done
 
-
 fun
   alpha_abs 
 where
@@ -171,15 +172,18 @@
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(simp_all)
+  (* refl *)
   apply(clarify)
   apply(rule exI)
   apply(rule alpha_gen_refl)
   apply(simp)
+  (* symm *)
   apply(clarify)
   apply(rule exI)
   apply(rule alpha_gen_sym)
   apply(assumption)
   apply(clarsimp)
+  (* trans *)
   apply(clarify)
   apply(rule exI)
   apply(rule alpha_gen_trans)
@@ -220,6 +224,11 @@
   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
   done
 
+(* TEST case *)
+lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
+
+thm abs_induct abs_induct2
+
 instantiation abs :: (pt) pt
 begin