# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1229459561 0
# Node ID 4c243e6a71b27e2cb50909cc5c53d470fa3ac569
# Parent  2a684ee023e750fa7feb60c11d3446926ee7669c
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions

diff -r 2a684ee023e7 -r 4c243e6a71b2 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Dec 16 19:24:55 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Dec 16 20:32:41 2008 +0000
@@ -1262,19 +1262,21 @@
   apply (simp add: pt_rev_pi [OF pt at])
   done
 
-lemma insert_eqvt:
+lemma pt_insert_eqvt:
+  fixes pi::"'x prm"
+  and   x::"'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
-  shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+  shows "(pi\<bullet>(insert x X)) = insert (pi\<bullet>x) (pi\<bullet>X)"
   by (auto simp add: perm_set_eq [OF pt at])
 
-lemma set_eqvt:
+lemma pt_set_eqvt:
   fixes pi :: "'x prm"
   and   xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+by (induct xs) (auto simp add: empty_eqvt pt_insert_eqvt [OF pt at])
 
 lemma supp_singleton:
   assumes pt: "pt TYPE('a) TYPE('x)"
@@ -1568,10 +1570,10 @@
 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: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[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] set_eqvt [OF ptb at])
+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
 
diff -r 2a684ee023e7 -r 4c243e6a71b2 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 16 19:24:55 2008 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 16 20:32:41 2008 +0000
@@ -798,8 +798,8 @@
        val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
        val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
        val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
-       val insert_eqvt         = @{thm "Nominal.insert_eqvt"};
-       val set_eqvt            = @{thm "Nominal.set_eqvt"};
+       val insert_eqvt         = @{thm "Nominal.pt_insert_eqvt"};
+       val set_eqvt            = @{thm "Nominal.pt_set_eqvt"};
        val perm_set_eq         = @{thm "Nominal.perm_set_eq"};
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)