# HG changeset patch
# User haftmann
# Date 1240813357 -7200
# Node ID c2524d1235281a3097e1dd0e62b5262602713a0e
# Parent  e46639644fcd2ab7f9a05747d0d07c088eb86ba7# Parent  a1efb13fc5d8b8cf356676a7d9cdd60eacb3224f
merged

diff -r a1efb13fc5d8 -r c2524d123528 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 27 08:22:37 2009 +0200
@@ -963,7 +963,7 @@
   (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
 
 lemma fps_power_mult_eq_shift:
-  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}" (is "?lhs = ?rhs")
+  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}" (is "?lhs = ?rhs")
 proof-
   {fix n:: nat
     have "?lhs $ n = (if n < Suc k then 0 else a n)"
@@ -974,7 +974,7 @@
     next
       case (Suc k)
       note th = Suc.hyps[symmetric]
-      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps)
+      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps)
       also  have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
 	using th
 	unfolding fps_sub_nth by simp
@@ -1012,8 +1012,9 @@
 
 lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
 
+
 lemma fps_mult_XD_shift:
-  "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+  "(XD ^^ k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
 
 subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
diff -r a1efb13fc5d8 -r c2524d123528 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 27 08:22:37 2009 +0200
@@ -18,7 +18,7 @@
 types 
   'x prm = "('x \<times> 'x) list"
 
-(* polymorphic operations for permutation and swapping *)
+(* polymorphic constants for permutation and swapping *)
 consts 
   perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
@@ -34,7 +34,7 @@
 constdefs
   "perm_aux pi x \<equiv> pi\<bullet>x"
 
-(* permutation operations *)
+(* overloaded permutation operations *)
 overloading
   perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
   perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
@@ -203,11 +203,12 @@
    supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80)
    "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
 
+(* lemmas about supp *)
 lemma supp_fresh_iff: 
   fixes x :: "'a"
   shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
-apply(simp add: fresh_def)
-done
+  by (simp add: fresh_def)
+
 
 lemma supp_unit:
   shows "supp () = {}"
@@ -238,14 +239,13 @@
   fixes x  :: "'a"
   and   xs :: "'a list"
   shows "supp (x#xs) = (supp x)\<union>(supp xs)"
-apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
-done
+  by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
 lemma supp_list_append:
   fixes xs :: "'a list"
   and   ys :: "'a list"
   shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
-  by (induct xs, auto simp add: supp_list_nil supp_list_cons)
+  by (induct xs) (auto simp add: supp_list_nil supp_list_cons)
 
 lemma supp_list_rev:
   fixes xs :: "'a list"
@@ -287,6 +287,7 @@
   shows "(supp s) = {}"
   by (simp add: supp_def perm_string)
 
+(* lemmas about freshness *)
 lemma fresh_set_empty:
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)
@@ -395,63 +396,6 @@
   Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
 *}
 
-section {* generalisation of freshness to lists and sets of atoms *}
-(*================================================================*)
- 
-consts
-  fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
-
-defs (overloaded)
-  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
-
-defs (overloaded)
-  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
-
-lemmas fresh_star_def = fresh_star_list fresh_star_set
-
-lemma fresh_star_prod_set:
-  fixes xs::"'a set"
-  shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
-by (auto simp add: fresh_star_def fresh_prod)
-
-lemma fresh_star_prod_list:
-  fixes xs::"'a list"
-  shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
-  by (auto simp add: fresh_star_def fresh_prod)
-
-lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
-
-lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
-  by (simp add: fresh_star_def)
-
-lemma fresh_star_Un_elim:
-  "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
-  apply rule
-  apply (simp_all add: fresh_star_def)
-  apply (erule meta_mp)
-  apply blast
-  done
-
-lemma fresh_star_insert_elim:
-  "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
-  by rule (simp_all add: fresh_star_def)
-
-lemma fresh_star_empty_elim:
-  "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
-  by (simp add: fresh_star_def)
-
-text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
-
-lemma fresh_star_unit_elim: 
-  shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
-  and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
-  by (simp_all add: fresh_star_def fresh_def supp_unit)
-
-lemma fresh_star_prod_elim: 
-  shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
-  and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
-  by (rule, simp_all add: fresh_star_prod)+
-
 section {* Abstract Properties for Permutations and  Atoms *}
 (*=========================================================*)
 
@@ -511,7 +455,7 @@
   shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
   using a by (simp only: at_def)
 
-(* rules to calculate simple premutations *)
+(* rules to calculate simple permutations *)
 lemmas at_calc = at2 at1 at3
 
 lemma at_swap_simps:
@@ -706,7 +650,6 @@
   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   by (simp add: at_prm_rev_eq[OF at])
 
-
 lemma at_ds1:
   fixes a  :: "'x"
   assumes at: "at TYPE('x)"
@@ -862,15 +805,18 @@
   by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
 
 lemma at_finite_select: 
-  shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
-  apply (drule Diff_infinite_finite)
-  apply (simp add: at_def)
-  apply blast
-  apply (subgoal_tac "UNIV - S \<noteq> {}")
-  apply (simp only: ex_in_conv [symmetric])
-  apply blast
-  apply (rule notI)
-  apply simp
+  fixes S::"'a set"
+  assumes a: "at TYPE('a)"
+  and     b: "finite S" 
+  shows "\<exists>x. x \<notin> S" 
+  using a b
+  apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
+  apply(simp add: at_def)
+  apply(subgoal_tac "UNIV - S \<noteq> {}")
+  apply(simp only: ex_in_conv [symmetric])
+  apply(blast)
+  apply(rule notI)
+  apply(simp)
   done
 
 lemma at_different:
@@ -1246,8 +1192,8 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
-using assms
-by (auto simp add: pt_bij perm_bool)
+  using pt at
+  by (auto simp add: pt_bij perm_bool)
 
 lemma pt_bij3:
   fixes pi :: "'x prm"
@@ -1255,7 +1201,7 @@
   and   y  :: "'a"
   assumes a:  "x=y"
   shows "(pi\<bullet>x = pi\<bullet>y)"
-using a by simp 
+  using a by simp 
 
 lemma pt_bij4:
   fixes pi :: "'x prm"
@@ -1265,7 +1211,7 @@
   and     at: "at TYPE('x)"
   and     a:  "pi\<bullet>x = pi\<bullet>y"
   shows "x = y"
-using a by (simp add: pt_bij[OF pt, OF at])
+  using a by (simp add: pt_bij[OF pt, OF at])
 
 lemma pt_swap_bij:
   fixes a  :: "'x"
@@ -1598,35 +1544,6 @@
 apply(simp add: pt_rev_pi[OF ptb, OF at])
 done
 
-lemma pt_fresh_star_bij_ineq:
-  fixes  pi :: "'x prm"
-  and     x :: "'a"
-  and     a :: "'y set"
-  and     b :: "'y list"
-  assumes pta: "pt TYPE('a) TYPE('x)"
-  and     ptb: "pt TYPE('y) TYPE('x)"
-  and     at:  "at TYPE('x)"
-  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
-  shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
-  and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-apply(unfold fresh_star_def)
-apply(auto)
-apply(drule_tac x="pi\<bullet>xa" in bspec)
-apply(rule pt_set_bij2[OF ptb, OF at])
-apply(assumption)
-apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="pi\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
-apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
-apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
-apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
-done
-
 lemma pt_fresh_left:  
   fixes  pi :: "'x prm"
   and     x :: "'a"
@@ -1675,56 +1592,6 @@
 apply(rule at)
 done
 
-lemma pt_fresh_star_bij:
-  fixes  pi :: "'x prm"
-  and     x :: "'a"
-  and     a :: "'x set"
-  and     b :: "'x list"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
-  and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
-apply(rule pt_fresh_star_bij_ineq(1))
-apply(rule pt)
-apply(rule at_pt_inst)
-apply(rule at)+
-apply(rule cp_pt_inst)
-apply(rule pt)
-apply(rule at)
-apply(rule pt_fresh_star_bij_ineq(2))
-apply(rule pt)
-apply(rule at_pt_inst)
-apply(rule at)+
-apply(rule cp_pt_inst)
-apply(rule pt)
-apply(rule at)
-done
-
-lemma pt_fresh_star_eqvt:
-  fixes  pi :: "'x prm"
-  and     x :: "'a"
-  and     a :: "'x set"
-  and     b :: "'x list"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
-  and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
-  by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
-
-lemma pt_fresh_star_eqvt_ineq:
-  fixes pi::"'x prm"
-  and   a::"'y set"
-  and   b::"'y list"
-  and   x::"'a"
-  assumes pta: "pt TYPE('a) TYPE('x)"
-  and     ptb: "pt TYPE('y) TYPE('x)"
-  and     at:  "at TYPE('x)"
-  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
-  and     dj:  "disjoint TYPE('y) TYPE('x)"
-  shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
-  and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
-  by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
-
 lemma pt_fresh_bij1:
   fixes  pi :: "'x prm"
   and     x :: "'a"
@@ -1777,7 +1644,6 @@
 
 (* the next two lemmas are needed in the proof *)
 (* of the structural induction principle       *)
-
 lemma pt_fresh_aux:
   fixes a::"'x"
   and   b::"'x"
@@ -1881,27 +1747,6 @@
   thus ?thesis using eq3 by simp
 qed
 
-lemma pt_freshs_freshs:
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and at: "at TYPE ('x)"
-  and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
-  and Xs: "Xs \<sharp>* (x::'a)"
-  and Ys: "Ys \<sharp>* x"
-  shows "pi \<bullet> x = x"
-  using pi
-proof (induct pi)
-  case Nil
-  show ?case by (simp add: pt1 [OF pt])
-next
-  case (Cons p pi)
-  obtain a b where p: "p = (a, b)" by (cases p)
-  with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
-    by (simp_all add: fresh_star_def)
-  with Cons p show ?case
-    by (simp add: pt_fresh_fresh [OF pt at]
-      pt2 [OF pt, of "[(a, b)]" pi, simplified])
-qed
-
 lemma pt_pi_fresh_fresh:
   fixes   x :: "'a"
   and     pi :: "'x prm"
@@ -1967,8 +1812,7 @@
   thus ?thesis by (simp add: pt2[OF pt])
 qed
 
-section {* equivaraince for some connectives *}
-
+section {* equivariance for some connectives *}
 lemma pt_all_eqvt:
   fixes  pi :: "'x prm"
   and     x :: "'a"
@@ -2014,8 +1858,6 @@
   apply(rule theI'[OF unique])
   done
 
-
-
 section {* facts about supports *}
 (*==============================*)
 
@@ -2184,6 +2026,7 @@
   shows "(x \<sharp> X) = (x \<notin> X)"
   by (simp add: at_fin_set_supp fresh_def at fs)
 
+
 section {* Permutations acting on Functions *}
 (*==========================================*)
 
@@ -2564,9 +2407,8 @@
   and     a1:  "a\<sharp>x"
   and     a2:  "a\<sharp>X"
   shows "a\<sharp>(insert x X)"
-using a1 a2
-apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
-done
+  using a1 a2
+  by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
 
 lemma pt_list_set_supp:
   fixes xs :: "'a list"
@@ -2595,14 +2437,191 @@
   shows "a\<sharp>(set xs) = a\<sharp>xs"
 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
 
+
+section {* generalisation of freshness to lists and sets of atoms *}
+(*================================================================*)
+ 
+consts
+  fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
+
+defs (overloaded)
+  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
+
+defs (overloaded)
+  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+
+lemmas fresh_star_def = fresh_star_list fresh_star_set
+
+lemma fresh_star_prod_set:
+  fixes xs::"'a set"
+  shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
+by (auto simp add: fresh_star_def fresh_prod)
+
+lemma fresh_star_prod_list:
+  fixes xs::"'a list"
+  shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
+  by (auto simp add: fresh_star_def fresh_prod)
+
+lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
+
+lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
+  by (simp add: fresh_star_def)
+
+lemma fresh_star_Un_elim:
+  "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
+  apply rule
+  apply (simp_all add: fresh_star_def)
+  apply (erule meta_mp)
+  apply blast
+  done
+
+lemma fresh_star_insert_elim:
+  "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
+  by rule (simp_all add: fresh_star_def)
+
+lemma fresh_star_empty_elim:
+  "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_star_def)
+
+text {* Normalization of freshness results; see \ @{text nominal_induct} *}
+
+lemma fresh_star_unit_elim: 
+  shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+  and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp_all add: fresh_star_def fresh_def supp_unit)
+
+lemma fresh_star_prod_elim: 
+  shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
+  and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
+  by (rule, simp_all add: fresh_star_prod)+
+
+
+lemma pt_fresh_star_bij_ineq:
+  fixes  pi :: "'x prm"
+  and     x :: "'a"
+  and     a :: "'y set"
+  and     b :: "'y list"
+  assumes pta: "pt TYPE('a) TYPE('x)"
+  and     ptb: "pt TYPE('y) TYPE('x)"
+  and     at:  "at TYPE('x)"
+  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
+  shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+  and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(unfold fresh_star_def)
+apply(auto)
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(erule pt_set_bij2[OF ptb, OF at])
+apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+done
+
+lemma pt_fresh_star_bij:
+  fixes  pi :: "'x prm"
+  and     x :: "'a"
+  and     a :: "'x set"
+  and     b :: "'x list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+  and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(rule pt_fresh_star_bij_ineq(1))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+apply(rule pt_fresh_star_bij_ineq(2))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_fresh_star_eqvt:
+  fixes  pi :: "'x prm"
+  and     x :: "'a"
+  and     a :: "'x set"
+  and     b :: "'x list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+  and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+  by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
+
+lemma pt_fresh_star_eqvt_ineq:
+  fixes pi::"'x prm"
+  and   a::"'y set"
+  and   b::"'y list"
+  and   x::"'a"
+  assumes pta: "pt TYPE('a) TYPE('x)"
+  and     ptb: "pt TYPE('y) TYPE('x)"
+  and     at:  "at TYPE('x)"
+  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
+  and     dj:  "disjoint TYPE('y) TYPE('x)"
+  shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+  and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+  by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
+
+lemma pt_freshs_freshs:
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE ('x)"
+  and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
+  and Xs: "Xs \<sharp>* (x::'a)"
+  and Ys: "Ys \<sharp>* x"
+  shows "pi\<bullet>x = x"
+  using pi
+proof (induct pi)
+  case Nil
+  show ?case by (simp add: pt1 [OF pt])
+next
+  case (Cons p pi)
+  obtain a b where p: "p = (a, b)" by (cases p)
+  with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
+    by (simp_all add: fresh_star_def)
+  with Cons p show ?case
+    by (simp add: pt_fresh_fresh [OF pt at]
+      pt2 [OF pt, of "[(a, b)]" pi, simplified])
+qed
+
+lemma pt_fresh_star_pi: 
+  fixes x::"'a"
+  and   pi::"'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     a: "((supp x)::'x set)\<sharp>* pi"
+  shows "pi\<bullet>x = x"
+using a
+apply(induct pi)
+apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
+apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x")
+apply(simp only: pt2[OF pt])
+apply(rule pt_fresh_fresh[OF pt at])
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: fresh_def at_supp[OF at])
+apply(blast)
+apply(simp add: pt2[OF pt])
+done
+
 section {* Infrastructure lemmas for strong rule inductions *}
 (*==========================================================*)
 
-
 text {* 
   For every set of atoms, there is another set of atoms
   avoiding a finitely supported c and there is a permutation
-  which make 'translates' between both sets.
+  which 'translates' between both sets.
 *}
 lemma at_set_avoiding_aux:
   fixes Xs::"'a set"
@@ -3389,7 +3408,6 @@
 
 syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
 
-
 section {* lemmas for deciding permutation equations *}
 (*===================================================*)
 
@@ -3550,8 +3568,8 @@
   shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 
 by (simp add:perm_int_def) 
 
-(*******************************************************************)
-(* Setup of the theorem attributes eqvt, eqvt_force, fresh and bij *)
+(*******************************************************)
+(* Setup of the theorem attributes eqvt and eqvt_force *)
 use "nominal_thmdecls.ML"
 setup "NominalThmDecls.setup"
 
diff -r a1efb13fc5d8 -r c2524d123528 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Apr 26 20:23:41 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 27 08:22:37 2009 +0200
@@ -3,10 +3,10 @@
    This file introduces the infrastructure for the lemma
    collection "eqvts".
 
-   By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets 
+   By attaching [eqvt] or [eqvt_force] to a lemma, it will get 
    stored in a data-slot in the context. Possible modifiers
-   are [... add] and [... del] for adding and deleting, respectively 
-   the lemma from the data-slot.
+   are [... add] and [... del] for adding and deleting, 
+   respectively, the lemma from the data-slot.
 *)
 
 signature NOMINAL_THMDECLS =
@@ -43,9 +43,6 @@
 (* equality-lemma can be derived. *)
 exception EQVT_FORM of string
 
-(* FIXME: should be a function in a library *)
-fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
-
 val NOMINAL_EQVT_DEBUG = ref false
 
 fun tactic (msg, tac) =
@@ -53,14 +50,14 @@
   then tac THEN' (K (print_tac ("after " ^ msg)))
   else tac
 
-fun tactic_eqvt ctx orig_thm pi pi' =
+fun prove_eqvt_tac ctxt orig_thm pi pi' =
 let
-  val mypi = Thm.cterm_of ctx pi
+  val mypi = Thm.cterm_of ctxt pi
   val T = fastype_of pi'
-  val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
-  val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
+  val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
+  val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
 in
-  EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
+  EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
 	  tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
           tactic ("solve with orig_thm", etac orig_thm),
           tactic ("applies orig_thm instantiated with rev pi",
@@ -74,36 +71,38 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val pi' = Var (pi, typi);
-    val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
+    val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false
       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
     val _ = Display.print_cterm (cterm_of thy goal_term)
   in
     Goal.prove ctxt' [] [] goal_term
-      (fn _ => tactic_eqvt thy orig_thm pi' pi'') |>
+      (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
     singleton (ProofContext.export ctxt' ctxt)
   end
 
-(* replaces every variable x in t with pi o x *)
+(* replaces in t every variable, say x, with pi o x *)
 fun apply_pi trm (pi, typi) =
 let
-  fun only_vars t =
-     (case t of
-         Var (n, ty) => 
-           (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty) 
-                $ (Var (pi, typi)) $ (Var (n, ty)))
-       | _ => t)
+  fun replace n ty =
+  let 
+    val c  = Const (@{const_name "perm"}, typi --> ty --> ty) 
+    val v1 = Var (pi, typi)
+    val v2 = Var (n, ty)
+  in
+    c $ v1 $ v2 
+  end
 in
-    map_aterms only_vars trm
-end;
+  map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
+end
 
 (* returns *the* pi which is in front of all variables, provided there *)
 (* exists such a pi; otherwise raises EQVT_FORM                        *)
 fun get_pi t thy =
   let fun get_pi_aux s =
         (case s of
-          (Const (@{const_name "Nominal.perm"} ,typrm) $
-             (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
+          (Const (@{const_name "perm"} ,typrm) $
+             (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
                (Var (n,ty))) =>
              let
                 (* FIXME: this should be an operation the library *)
@@ -148,7 +147,7 @@
           end
        (* case: eqvt-lemma is of the equational form *)
       | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
-            (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
+            (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
            (if (apply_pi lhs (pi,typi)) = rhs
                then [orig_thm]
                else raise EQVT_FORM "Type Equality")
@@ -161,13 +160,11 @@
                " does not comply with the form of an equivariance lemma (" ^ s ^").")
 
 
-fun eqvt_map f (r:Data.T)  = f r;
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
 
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
-
-val eqvt_force_add  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
-val eqvt_force_del  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
+val eqvt_force_add  = Thm.declaration_attribute (Data.map o Thm.add_thm);
+val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
 
 val get_eqvt_thms = Context.Proof #> Data.get;