--- a/Quot/Nominal/Abs.thy	Mon Feb 01 12:06:46 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 01 12:48:18 2010 +0100
@@ -26,38 +26,11 @@
 done
 
 
-datatype 'a rabst = 
-  RAbst "atom set" "'a::pt"
-
-fun map_fun 
-where "map_fun f (RAbst bs x) = RAbst bs (f x)"
-
-fun map_rel
-where "map_rel R (RAbst bs x) (RAbst cs y) = R x y"
-
-declare [[map "rabst" = (map_fun, map_rel)]]
-
-instantiation rabst :: (pt) pt
-begin
-
-primrec
-  permute_rabst
+fun
+  alpha_gen 
 where
-  "p \<bullet> (RAbst bs x) = RAbst (p \<bullet> bs) (p \<bullet> x)"
-
-instance
-apply(default)
-apply(case_tac [!] x)
-apply(simp_all)
-done
-
-end
-
-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[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)"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _")
@@ -100,67 +73,17 @@
   done
 
 fun
-  alpha_rabst :: "('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool" ("_ \<approx>raw _") 
+  alpha_abst 
 where
-  "(RAbst bs x) \<approx>raw (RAbst cs y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" 
-
-lemma alpha_reflp:
-  shows "abst \<approx>raw abst"
-apply(induct abst)
-apply(simp)
-apply(rule exI)
-apply(rule alpha_gen_refl)
-apply(simp)
-done
-
-lemma alpha_symp:
-  assumes a: "abst1 \<approx>raw abst2"
-  shows "abst2 \<approx>raw abst1"
-using a
-apply(induct rule: alpha_rabst.induct)
-apply(simp)
-apply(erule exE)
-apply(rule exI)
-apply(rule alpha_gen_sym)
-apply(assumption)
-apply(clarsimp)
-done
+  "alpha_abst (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
-lemma alpha_transp:
-  assumes a1: "abst1 \<approx>raw abst2"
-  and     a2: "abst2 \<approx>raw abst3"
-  shows "abst1 \<approx>raw abst3"
-using a1 a2
-apply(induct rule: alpha_rabst.induct)
-apply(induct rule: alpha_rabst.induct)
-apply(simp)
-apply(erule exE)+
-apply(rule exI)
-apply(rule alpha_gen_trans)
-apply(assumption)
-apply(assumption)
-apply(simp)
-done
-
-lemma alpha_eqvt:
-  assumes a: "abst1 \<approx>raw abst2"
-  shows "(p \<bullet> abst1) \<approx>raw(p \<bullet> abst2)"
-using a
-apply(induct abst1 abst2 rule: alpha_rabst.induct)
-apply(simp)
-apply(erule exE)
-apply(rule exI)
-apply(rule alpha_gen_eqvt)
-apply(assumption)
-apply(simp)
-apply(simp add: supp_eqvt)
-apply(simp add: supp_eqvt)
-done
+notation
+  alpha_abst ("_ \<approx>abst _")
 
 lemma test1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
-  shows "(RAbst bs x) \<approx>raw (RAbst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
+  shows "(bs, x) \<approx>abst ((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)
@@ -176,46 +99,67 @@
 fun
   s_test
 where
-  "s_test (RAbst bs x) = (supp x) - bs"
+  "s_test (bs, x) = (supp x) - bs"
 
 lemma s_test_lemma:
-  assumes a: "x \<approx>raw y" 
+  assumes a: "x \<approx>abst y" 
   shows "s_test x = s_test y"
 using a
-apply(induct rule: alpha_rabst.induct)
+apply(induct rule: alpha_abst.induct)
 apply(simp add: alpha_gen)
 done
   
-
-quotient_type 'a abst = "('a::pt) rabst" / "alpha_rabst::('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool"
+quotient_type 'a abst = "(atom set \<times> 'a::pt)" / "alpha_abst"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
-  apply(auto intro: alpha_reflp alpha_symp alpha_transp)
+  apply(simp_all)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_refl)
+  apply(simp)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_sym)
+  apply(assumption)
+  apply(clarsimp)
+  apply(clarify)
+  apply(rule exI)
+  apply(rule alpha_gen_trans)
+  apply(assumption)
+  apply(assumption)
+  apply(simp)
   done
 
 quotient_definition
    "Abst::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abst"
 as
-   "RAbst"
+   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 lemma [quot_respect]:
-  shows "((op =) ===> (op =) ===> alpha_rabst) RAbst RAbst"
-apply(simp del: alpha_rabst.simps add: alpha_reflp)
+  shows "((op =) ===> (op =) ===> alpha_abst) Pair Pair"
+apply(clarsimp)
+apply(rule exI)
+apply(rule alpha_gen_refl)
+apply(simp)
 done
 
 lemma [quot_respect]:
-  shows "((op =) ===> alpha_rabst ===> alpha_rabst) permute permute"
-apply(simp add: alpha_eqvt)
+  shows "((op =) ===> alpha_abst ===> alpha_abst) permute permute"
+apply(clarsimp)
+apply(rule exI)
+apply(rule alpha_gen_eqvt)
+apply(assumption)
+apply(simp_all add: supp_eqvt)
 done
 
 lemma [quot_respect]:
-  shows "(alpha_rabst ===> (op =)) s_test s_test"
+  shows "(alpha_abst ===> (op =)) s_test s_test"
 apply(simp add: s_test_lemma)
 done
 
 lemma abst_induct:
   "\<lbrakk>\<And>as (x::'a::pt). P (Abst as x)\<rbrakk> \<Longrightarrow> P t"
-apply(lifting rabst.induct)
+apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
 done
 
 instantiation abst :: (pt) pt
@@ -224,12 +168,12 @@
 quotient_definition
   "permute_abst::perm \<Rightarrow> ('a::pt abst) \<Rightarrow> 'a abst"
 as
-  "permute::perm \<Rightarrow> ('a::pt rabst) \<Rightarrow> 'a rabst"
+  "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
 lemma permute_ABS [simp]:
   fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)
   shows "(p \<bullet> (Abst as x)) = Abst (p \<bullet> as) (p \<bullet> x)"
-apply(lifting permute_rabst.simps(1))
+apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
 done
 
 instance
@@ -260,7 +204,7 @@
 quotient_definition
   "s_test_lifted :: ('a::pt) abst \<Rightarrow> atom \<Rightarrow> bool"
 as
-  "s_test::('a::pt) rabst \<Rightarrow> atom \<Rightarrow> bool"
+  "s_test"
 
 lemma s_test_lifted_simp:
   shows "s_test_lifted (Abst bs x) = (supp x) - bs"
@@ -296,6 +240,7 @@
 apply(simp)
 done
 
+
 lemma supp_finite_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -315,6 +260,7 @@
 apply(rule contrapos_pp)
 apply(assumption)
 unfolding fresh_def[symmetric]
+thm s_test_fresh_lemma
 apply(drule_tac s_test_fresh_lemma)
 apply(simp only: s_test_lifted_simp)
 apply(simp add: fresh_def)
@@ -348,11 +294,9 @@
 apply(auto)
 done
 
-thm alpha_rabst.simps(1)
-
 lemma abs_eq:
   shows "(Abst bs x) = (Abst cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-apply(lifting alpha_rabst.simps(1))
+apply(lifting alpha_abst.simps(1))
 done
 
 end