updated
authorurbanc
Mon Feb 18 05:51:16 2008 +0100 (2008-02-18)
changeset 26091f31d4fe763aa
parent 26090 ec111fa4f8c5
child 26092 260cca2e16fa
updated
src/HOL/Nominal/Examples/Class.thy
src/HOL/Nominal/Examples/Fsub.thy
     1.1 --- a/src/HOL/Nominal/Examples/Class.thy	Mon Feb 18 03:12:08 2008 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Mon Feb 18 05:51:16 2008 +0100
     1.3 @@ -11159,14 +11159,24 @@
     1.4  apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
     1.5  apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
     1.6  apply(perm_simp)
     1.7 -apply(simp add: pt_subseteq_eqvt[OF pt_name_inst,OF at_name_inst])
     1.8 +apply(rule Collect_cong)
     1.9 +apply(rule iffI)
    1.10 +apply(rule subseteq_eqvt(1)[THEN iffD1])
    1.11 +apply(simp add: perm_bool)
    1.12 +apply(drule subseteq_eqvt(1)[THEN iffD2])
    1.13 +apply(simp add: perm_bool)
    1.14  apply(simp add: lfp_def)
    1.15  apply(simp add: Inf_set_def)
    1.16  apply(simp add: big_inter_eqvt)
    1.17  apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
    1.18  apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
    1.19  apply(perm_simp)
    1.20 -apply(simp add: pt_subseteq_eqvt[OF pt_coname_inst,OF at_coname_inst])
    1.21 +apply(rule Collect_cong)
    1.22 +apply(rule iffI)
    1.23 +apply(rule subseteq_eqvt(2)[THEN iffD1])
    1.24 +apply(simp add: perm_bool)
    1.25 +apply(drule subseteq_eqvt(2)[THEN iffD2])
    1.26 +apply(simp add: perm_bool)
    1.27  done
    1.28  
    1.29  abbreviation
     2.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 18 03:12:08 2008 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Feb 18 05:51:16 2008 +0100
     2.3 @@ -147,12 +147,9 @@
     2.4    assumes a: "S closed_in \<Gamma>" 
     2.5    shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
     2.6    using a
     2.7 -proof (unfold "closed_in_def")
     2.8 -  assume "supp S \<subseteq> (domain \<Gamma>)" 
     2.9 -  hence "pi\<bullet>(supp S) \<subseteq> pi\<bullet>(domain \<Gamma>)"
    2.10 -    by (simp add: pt_subseteq_eqvt[OF pt_tyvrs_inst, OF at_tyvrs_inst])
    2.11 -  thus "(supp (pi\<bullet>S)) \<subseteq> (domain (pi\<bullet>\<Gamma>))"
    2.12 -    by (simp add: domain_eqvt pt_perm_supp[OF pt_tyvrs_inst, OF at_tyvrs_inst])
    2.13 +proof -
    2.14 +  from a have "pi\<bullet>(S closed_in \<Gamma>)" by (simp add: perm_bool)
    2.15 +  then show "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_def eqvts)
    2.16  qed
    2.17  
    2.18  lemma ty_vrs_prm_simp: