# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268758928 -3600
# Node ID 0fd03936dedb46641ab6af7dcbd9a95a9621232e
# Parent  d6d22254aeb7262371a34dd78037f04bb884454e
merge and proof of support for non-recursive case

diff -r d6d22254aeb7 -r 0fd03936dedb Attic/IsaMakefile
--- a/Attic/IsaMakefile	Tue Mar 16 17:20:46 2010 +0100
+++ b/Attic/IsaMakefile	Tue Mar 16 18:02:08 2010 +0100
@@ -21,7 +21,7 @@
 Quot: $(LOG)/HOL-Quot.gz
 
 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
-	@$(USEDIR) HOL-Nominal Quot
+	@$(USEDIR) HOL-Plain Quot
 
 paper: $(LOG)/HOL-Quot-Paper.gz
 
@@ -38,8 +38,7 @@
 	cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/HOL-Nominal.gz tmp
 	cp $(LOG)/HOL-Nominal-Quot.gz tmp
 	isabelle keywords -k quot tmp/*
-	
-	
+
 ## clean
 
 clean:
diff -r d6d22254aeb7 -r 0fd03936dedb Attic/Quot/Quotient.thy
--- a/Attic/Quot/Quotient.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Attic/Quot/Quotient.thy	Tue Mar 16 18:02:08 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Quotient
-imports Plain ATP_Linkup
+imports Plain ATP_Linkup 
 uses
   ("quotient_info.ML")
   ("quotient_typ.ML")
diff -r d6d22254aeb7 -r 0fd03936dedb Attic/Quot/quotient_typ.ML
--- a/Attic/Quot/quotient_typ.ML	Tue Mar 16 17:20:46 2010 +0100
+++ b/Attic/Quot/quotient_typ.ML	Tue Mar 16 18:02:08 2010 +0100
@@ -1,7 +1,7 @@
-(*  Title:      quotient_typ.thy
+(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Definition of a quotient type.
+Definition of a quotient type.
 
 *)
 
@@ -74,11 +74,8 @@
   val typedef_tac =
     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
-  Local_Theory.theory_result
-  (Typedef.add_typedef_global false NONE
-    (qty_name, vs, mx)
-      (typedef_term rel rty lthy)
-        NONE typedef_tac) lthy
+  Typedef.add_typedef false NONE (qty_name, vs, mx) 
+    (typedef_term rel rty lthy) NONE typedef_tac lthy
 end
 
 
@@ -282,7 +279,12 @@
       Syntax.parse_term lthy1 rel_str
       |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
       |> Syntax.check_term lthy1 
-    val lthy2 = Variable.declare_term rel lthy1 
+    val (newT, lthy2) = lthy1
+      |> Typedecl.typedecl_wrt [rel] (qty_name, vs, mx)
+      ||> Variable.declare_term rel 
+   
+    (*val Type (full_qty_name, type_args) = newT
+    val vs' = map Term.dest_TFree type_args*)
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end
diff -r d6d22254aeb7 -r 0fd03936dedb Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 16 18:02:08 2010 +0100
@@ -1,146 +1,40 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Quotient" "Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
 begin
 
-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 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"
+  "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)
 
-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 [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)
 
 lemma alpha_gen_refl:
   assumes a: "R x x"
-  shows "(bs, x) \<approx>gen R fv 0 (bs, x)"
+  shows "(bs, x) \<approx>gen R f 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 fv p (cs, y)"
+  assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  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  
+  shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
+  using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
 
 lemma alpha_gen_trans:
-  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
+  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
 
-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)"
@@ -154,48 +48,77 @@
   apply(clarsimp)
   done
 
-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)
+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(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 4)
+  apply(drule_tac pi="- pia" in a)
+  apply(simp)
+  apply(rotate_tac 6)
+  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)
   done
 
 fun
   alpha_abs 
 where
-  "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+  "alpha_abs (bs, x) (cs, y) = (\<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"
   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)
-  unfolding alpha_gen
-  apply(simp)
+  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}")
@@ -205,15 +128,14 @@
   apply(simp add: supp_swap)
   done
 
-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)
+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)"
   apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
-  unfolding alpha_tst
-  apply(simp)
-  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric])
+  apply(simp add: alpha_gen)
+  apply(simp add: f_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
@@ -222,16 +144,12 @@
   apply(simp add: supp_swap)
   done
 
+
 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"
@@ -239,14 +157,6 @@
   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)
@@ -272,46 +182,11 @@
   apply(simp)
   done
 
-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)
@@ -321,22 +196,6 @@
   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)
@@ -350,23 +209,11 @@
   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
@@ -392,56 +239,14 @@
 
 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)"
@@ -449,13 +254,6 @@
   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)
@@ -463,36 +261,14 @@
   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)
-
-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)
-*)
+  using a1 a2 by (lifting alpha_abs_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))
@@ -500,15 +276,6 @@
   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)"
@@ -520,17 +287,6 @@
   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"
@@ -539,14 +295,6 @@
   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"
@@ -555,14 +303,6 @@
   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)
@@ -570,13 +310,6 @@
   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)"
@@ -585,26 +318,10 @@
   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))
-*)
 
 
 (* 
@@ -621,7 +338,32 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
-lemma
+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 qq:
+  fixes S::"atom set"
+  assumes a: "supp p \<inter> S = {}"
+  shows "p \<bullet> S = S"
+using a
+apply(simp add: supp_perm permute_set_eq)
+apply(auto)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply (metis permute_atom_def_raw)
+apply(rule_tac x="(- p) \<bullet> x" in exI)
+apply(simp)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply(metis permute_minus_cancel)
+done
+
+lemma alpha_old_new:
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
 using a
@@ -631,12 +373,11 @@
 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)
@@ -644,8 +385,7 @@
 apply(simp)
 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)
@@ -792,6 +532,9 @@
 apply(simp add: zero)
 apply(rotate_tac 3)
 oops
+lemma tt:
+  "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+oops
 
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
@@ -800,6 +543,18 @@
 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"
@@ -928,6 +683,12 @@
 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:
@@ -950,52 +711,11 @@
 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)
-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)
+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
 
 
diff -r d6d22254aeb7 -r 0fd03936dedb Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 18:02:08 2010 +0100
@@ -10,7 +10,6 @@
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = recursive := false *}
 
-(*
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -22,19 +21,6 @@
   bi::"bp \<Rightarrow> atom set"
 where
   "bi (BP x t) = {atom x}"
-*)
-
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x) = {atom x}"
 
 thm lam_bp_fv
 thm lam_bp_inject
@@ -56,28 +42,10 @@
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
   by (rule eqvts)
 
-term alpha_bi
-
-lemma alpha_bi:
-  shows "alpha_bi b b' = True"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp_all)
-apply(induct b' rule: lam_bp_inducts(2))
-apply (simp_all add: lam_bp_inject)
-done
-
-lemma fv_bi:
-  shows "fv_bi b = {}"
-apply(induct b rule: lam_bp_inducts(2))
-apply(auto)[1]
-apply(simp_all)
-apply(simp add: lam_bp_fv)
-done
-
 lemma supp_fv:
   "supp t = fv_lam t" and 
-  "supp b = fv_bp b"
-apply(induct t and b rule: lam_bp_inducts)
+  "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
+apply(induct t and bp rule: lam_bp_inducts)
 apply(simp_all add: lam_bp_fv)
 (* VAR case *)
 apply(simp only: supp_def)
@@ -111,31 +79,32 @@
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: lam_bp_inject)
-(*
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
-*)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
-(*apply(simp)*)
+apply(simp)
 (* LET case *)
-apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs_tst bi bp_raw lam_raw)" in subst)
+apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: permute_ABS_tst)
+apply(simp only: permute_ABS)
 apply(simp only: lam_bp_inject)
-apply(simp only: eqvts_raw)
-apply(simp only: Abs_tst_eq_iff)
-apply(simp only: alpha_bi)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(simp only: ex_simps)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
 apply(simp only: alpha_gen)
-apply(simp only: alpha_tst) 
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-apply simp
-apply(simp add: supp_Abs_tst)
-apply(simp add: fv_bi)
+apply(blast)
+apply(simp add: supp_Abs)
+apply(blast)
 done
 
 text {* example 2 *}
diff -r d6d22254aeb7 -r 0fd03936dedb Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/nominal_atoms.ML	Tue Mar 16 18:02:08 2010 +0100
@@ -44,7 +44,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
-      Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type info;