# HG changeset patch
# User urbanc
# Date 1177346322 -7200
# Node ID d41fe3416f5217a37acb7ffdad321827492a3e33
# Parent  125363bf751819822ad9d9e14e2668e332ef91f0
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)

diff -r 125363bf7518 -r d41fe3416f52 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 23 16:38:40 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 23 18:38:42 2007 +0200
@@ -78,6 +78,12 @@
   shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
   by (induct l) (simp_all add: append_eqvt)
 
+lemma set_eqvt:
+  fixes pi :: "'x prm"
+  and   xs :: "'a list"
+  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs, auto simp add: empty_eqvt insert_eqvt)
+
 (* permutation on functions *)
 defs (unchecked overloaded)
   perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
@@ -2279,13 +2285,6 @@
 apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
 done
 
-lemma pt_set_eqvt:
-  fixes pi :: "'x prm"
-  and   xs :: "'a list"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs, auto simp add: perm_set_def pt1[OF pt])
-
 lemma pt_list_set_supp:
   fixes xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE('x)"
@@ -3187,7 +3186,7 @@
   plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
   
   (* sets *)
-  union_eqvt empty_eqvt insert_eqvt
+  union_eqvt empty_eqvt insert_eqvt set_eqvt
   
  
 (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
diff -r 125363bf7518 -r d41fe3416f52 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 23 16:38:40 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 23 18:38:42 2007 +0200
@@ -707,7 +707,6 @@
        val fresh_aux           = thm "Nominal.pt_fresh_aux";
        val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
        val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
-       val set_eqvt            = thm "Nominal.pt_set_eqvt";
        val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
        val in_eqvt             = thm "Nominal.pt_in_eqvt";
        val eq_eqvt             = thm "Nominal.pt_eq_eqvt";
@@ -854,9 +853,6 @@
 	      let val thms1 = inst_pt_at [eq_eqvt]
 	      in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
 	    ||>> PureThy.add_thmss
-	      let val thms1 = inst_pt [set_eqvt]
-	      in [(("set_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
-	    ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [set_diff_eqvt]
 	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
             ||>> PureThy.add_thmss