added eqvt-flag to subseteq-lemma

--- a/src/HOL/Nominal/Nominal.thy	Mon Feb 18 02:10:55 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Feb 18 03:12:08 2008 +0100
@@ -38,7 +38,7 @@
   by (simp add: perm_set_def)
 
 lemma union_eqvt:
-  shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)"
+  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   by (auto simp add: perm_set_def)
 
 lemma insert_eqvt:
@@ -47,7 +47,7 @@
 
 (* permutation on units and products *)
 primrec (unchecked perm_unit)
-  "pi\<bullet>()    = ()"
+  "pi\<bullet>() = ()"
   
 primrec (unchecked perm_prod)
   "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
@@ -82,7 +82,7 @@
   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)
+by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
 
 (* permutation on functions *)
 defs (unchecked overloaded)
@@ -1308,20 +1308,8 @@
   and   X  :: "'a set"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "((pi\<bullet>X)\<subseteq>(pi\<bullet>Y)) = (X\<subseteq>Y)"
-proof (auto)
-  fix x::"'a"
-  assume a: "(pi\<bullet>X)\<subseteq>(pi\<bullet>Y)"
-  and    "x\<in>X"
-  hence  "(pi\<bullet>x)\<in>(pi\<bullet>X)" by (simp add: pt_set_bij[OF pt, OF at])
-  with a have "(pi\<bullet>x)\<in>(pi\<bullet>Y)" by force
-  thus "x\<in>Y" by (simp add: pt_set_bij[OF pt, OF at])
-next
-  fix x::"'a"
-  assume a: "X\<subseteq>Y"
-  and    "x\<in>(pi\<bullet>X)"
-  thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
-qed
+  shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
+by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
 
 lemma pt_set_diff_eqvt:
   fixes X::"'a set"
@@ -3270,7 +3258,7 @@
   plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
   
   (* sets *)
-  union_eqvt empty_eqvt insert_eqvt set_eqvt
+  union_eqvt empty_eqvt insert_eqvt set_eqvt 
   
  
 (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)

--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 02:10:55 2008 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 03:12:08 2008 +0100
@@ -775,6 +775,7 @@
        val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
        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"};
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -922,6 +923,9 @@
 	      let val thms1 = inst_pt_at [set_diff_eqvt]
 	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
             ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [subseteq_eqvt]
+	      in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
+            ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_aux]
 		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
 	      in  [(("fresh_aux", thms1 @ thms2),[])] end