# HG changeset patch
# User urbanc
# Date 1219805250 -7200
# Node ID 90074908db1664f12802ea5ea2cf00e782740d92
# Parent  8312edc51969bc0548de0a594d6eac029ddb1f51
added equivariance lemmas for ex1 and the

diff -r 8312edc51969 -r 90074908db16 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Aug 27 01:27:33 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Wed Aug 27 04:47:30 2008 +0200
@@ -1882,6 +1882,31 @@
 apply(simp add: pt_rev_pi[OF pt, OF at])
 done
 
+lemma pt_ex1_eqvt:
+  fixes  pi :: "'x prm"
+  and     x :: "'a"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows  "(pi\<bullet>(\<exists>!x. P (x::'a))) = (\<exists>!x. pi\<bullet>(P (rev pi\<bullet>x)))"
+unfolding Ex1_def
+by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] 
+              imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at])
+
+lemma pt_the_eqvt:
+  fixes  pi :: "'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     unique: "\<exists>!x. P x"
+  shows "pi\<bullet>(THE(x::'a). P x) = (THE(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
+  apply(rule the1_equality [symmetric])
+  apply(simp add: pt_ex1_eqvt[OF pt at,symmetric])
+  apply(simp add: perm_bool unique)
+  apply(simp add: perm_bool pt_rev_pi [OF pt at])
+  apply(rule theI'[OF unique])
+  done
+
+
+
 section {* facts about supports *}
 (*==============================*)
 
diff -r 8312edc51969 -r 90074908db16 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 01:27:33 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 04:47:30 2008 +0200
@@ -750,6 +750,8 @@
        val eq_eqvt             = @{thm "Nominal.pt_eq_eqvt"};
        val all_eqvt            = @{thm "Nominal.pt_all_eqvt"};
        val ex_eqvt             = @{thm "Nominal.pt_ex_eqvt"};
+       val ex1_eqvt            = @{thm "Nominal.pt_ex1_eqvt"};
+       val the_eqvt            = @{thm "Nominal.pt_the_eqvt"};
        val pt_pi_rev           = @{thm "Nominal.pt_pi_rev"};
        val pt_rev_pi           = @{thm "Nominal.pt_rev_pi"};
        val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
@@ -864,6 +866,8 @@
                 [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
               end
             ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
+            ||>> PureThy.add_thmss [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])]
+            ||>> PureThy.add_thmss [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])]
             ||>> PureThy.add_thmss 
               let val thms1 = inst_at [at_fresh]
                   val thms2 = inst_dj [at_fresh_ineq]