# HG changeset patch
# User urbanc
# Date 1203310276 -3600
# Node ID f31d4fe763aa2531ef8c1c89c69a171b00e5265b
# Parent  ec111fa4f8c5ccaa861880843d518d22c1af7bba
updated

diff -r ec111fa4f8c5 -r f31d4fe763aa src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Mon Feb 18 03:12:08 2008 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy	Mon Feb 18 05:51:16 2008 +0100
@@ -11159,14 +11159,24 @@
 apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
 apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
 apply(perm_simp)
-apply(simp add: pt_subseteq_eqvt[OF pt_name_inst,OF at_name_inst])
+apply(rule Collect_cong)
+apply(rule iffI)
+apply(rule subseteq_eqvt(1)[THEN iffD1])
+apply(simp add: perm_bool)
+apply(drule subseteq_eqvt(1)[THEN iffD2])
+apply(simp add: perm_bool)
 apply(simp add: lfp_def)
 apply(simp add: Inf_set_def)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
 apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
 apply(perm_simp)
-apply(simp add: pt_subseteq_eqvt[OF pt_coname_inst,OF at_coname_inst])
+apply(rule Collect_cong)
+apply(rule iffI)
+apply(rule subseteq_eqvt(2)[THEN iffD1])
+apply(simp add: perm_bool)
+apply(drule subseteq_eqvt(2)[THEN iffD2])
+apply(simp add: perm_bool)
 done
 
 abbreviation
diff -r ec111fa4f8c5 -r f31d4fe763aa src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 18 03:12:08 2008 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 18 05:51:16 2008 +0100
@@ -147,12 +147,9 @@
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
   using a
-proof (unfold "closed_in_def")
-  assume "supp S \<subseteq> (domain \<Gamma>)" 
-  hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)"
-    by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-  thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))"
-    by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst])
+proof -
+  from a have "pi\<bullet>(S closed_in \<Gamma>)" by (simp add: perm_bool)
+  then show "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_def eqvts)
 qed
 
 lemma ty_vrs_prm_simp: