# HG changeset patch
# User berghofe
# Date 1235556145 -3600
# Node ID 2023fb9fbf31e969e48c764828aa7ea415ef7bf4
# Parent  776de457f214eb5c546b26ed7b32f7c02c20503c
Added equivariance lemmas for fresh_star.

diff -r 776de457f214 -r 2023fb9fbf31 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Feb 25 07:42:20 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Feb 25 11:02:25 2009 +0100
@@ -1645,6 +1645,31 @@
 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"
diff -r 776de457f214 -r 2023fb9fbf31 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 25 07:42:20 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 25 11:02:25 2009 +0100
@@ -1,5 +1,4 @@
 (*  title:      HOL/Nominal/nominal_atoms.ML
-    ID:         $Id$
     Author:     Christian Urban and Stefan Berghofer, TU Muenchen
 
 Declaration of atom types to be used in nominal datatypes.
@@ -784,6 +783,8 @@
        val fresh_star_bij      = @{thms "Nominal.pt_fresh_star_bij"};
        val fresh_eqvt          = @{thm "Nominal.pt_fresh_eqvt"};
        val fresh_eqvt_ineq     = @{thm "Nominal.pt_fresh_eqvt_ineq"};
+       val fresh_star_eqvt     = @{thms "Nominal.pt_fresh_star_eqvt"};
+       val fresh_star_eqvt_ineq= @{thms "Nominal.pt_fresh_star_eqvt_ineq"};
        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"};
@@ -947,13 +948,17 @@
               in [(("fresh_bij", thms1 @ thms2),[])] end
             ||>> add_thmss_string
               let val thms1 = inst_pt_at fresh_star_bij
-                  and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq);
+                  and thms2 = maps (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq
               in [(("fresh_star_bij", thms1 @ thms2),[])] end
             ||>> add_thmss_string
               let val thms1 = inst_pt_at [fresh_eqvt]
                   and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
               in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
             ||>> add_thmss_string
+              let val thms1 = inst_pt_at fresh_star_eqvt
+                  and thms2 = maps (fn ti => inst_pt_pt_at_cp_dj [ti]) fresh_star_eqvt_ineq
+              in [(("fresh_star_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
+            ||>> add_thmss_string
               let val thms1 = inst_pt_at [in_eqvt]
               in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
             ||>> add_thmss_string