Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Classical.thy
changeset 2902 9c3f6a4d95d4
parent 2901 754aa24006c8
child 2903 e26c6c728b9e
equal deleted inserted replaced
2901:754aa24006c8 2902:9c3f6a4d95d4 
    27      ("OrR2 <_>._ _" [100,100,100] 100)
 
    27      ("OrR2 <_>._ _" [100,100,100] 100)
 
    28 | OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name"        bind n1 in t1, bind n2 in t2       
    28 | OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name"        bind n1 in t1, bind n2 in t2       
    29      ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
 
    29      ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
 
    30 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
 
    30 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
 
    31      ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
 
    31      ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
 
    32 | ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
    32 | ImpR n::"name" c::"coname" t::"trm" "coname"                bind n c in t
 
    33      ("ImpR '(_').<_>._ _" [100,100,100,100] 100)
 
    33      ("ImpR '(_').<_>._ _" [100,100,100,100] 100)
 
    34 
    34 
    35 thm trm.distinct
 
    35 thm trm.distinct
 
    36 thm trm.induct
 
    36 thm trm.induct
 
    37 thm trm.exhaust
 
    37 thm trm.exhaust
 
    49 lemma Abs_lst1_fcb2:
 
    49 lemma Abs_lst1_fcb2:
 
    50   fixes a b :: "'a :: at"
 
    50   fixes a b :: "'a :: at"
 
    51     and S T :: "'b :: fs"
 
    51     and S T :: "'b :: fs"
 
    52     and c::"'c::fs"
 
    52     and c::"'c::fs"
 
    53   assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
 
    53   assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
 
    54   and fcb: "\<And>a T. atom a \<sharp> f a T c"
 
    54   and fcb1: "atom a \<sharp> f a T c"
 
       
    55   and fcb2: "atom b \<sharp> f b S c"
 
    55   and fresh: "{atom a, atom b} \<sharp>* c"
 
    56   and fresh: "{atom a, atom b} \<sharp>* c"
 
    56   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
 
    57   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
 
    57   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
 
    58   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
 
    58   shows "f a T c = f b S c"
 
    59   shows "f a T c = f b S c"
 
    59 proof -
 
    60 proof -
 
   100     by (simp add: Abs1_eq_iff)
 
   101     by (simp add: Abs1_eq_iff)
 
   101   have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"
 
   102   have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"
 
   102     unfolding flip_def
 
   103     unfolding flip_def
 
   103     apply(rule sym)
 
   104     apply(rule sym)
 
   104     apply(rule swap_fresh_fresh)
 
   105     apply(rule swap_fresh_fresh)
 
   105     using fcb[where a="a"] 
   106     using fcb1 
   106     apply(simp)
 
   107     apply(simp)
 
   107     using fr
 
   108     using fr
 
   108     apply(simp add: fresh_Pair)
 
   109     apply(simp add: fresh_Pair)
 
   109     done
 
   110     done
 
   110   also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
 
   111   also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
 
   122     apply(simp add: supp_swap fresh_star_def fresh_Pair)
 
   123     apply(simp add: supp_swap fresh_star_def fresh_Pair)
 
   123     apply(simp)
 
   124     apply(simp)
 
   124     done
 
   125     done
 
   125   also have "... = f b S c"   
   126   also have "... = f b S c"   
   126     apply(rule flip_fresh_fresh)
 
   127     apply(rule flip_fresh_fresh)
 
   127     using fcb[where a="b"] 
   128     using fcb2
 
   128     apply(simp)
 
   129     apply(simp)
 
   129     using fr
 
   130     using fr
 
   130     apply(simp add: fresh_Pair)
 
   131     apply(simp add: fresh_Pair)
 
   131     done
 
   132     done
 
   132   finally show ?thesis by simp
 
   133   finally show ?thesis by simp
 
   133 qed
 
   134 qed
 
   134 
   135 
   135 
   136 
   136 lemma swap_at_base_sort: 
       
   137   "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) 
       
   138   \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x"
 
       
   139   by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1))
 
       
   140 
   137 
   141 nominal_primrec 
   138 nominal_primrec 
   142   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
   139   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
   143 where
 
   140 where
 
   144   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
   141   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
   170   apply(simp_all)
 
   167   apply(simp_all)
 
   171   apply(rule conjI)
 
   168   apply(rule conjI)
 
   172   apply(elim conjE)
 
   169   apply(elim conjE)
 
   173   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   170   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   174   apply(simp add: Abs_fresh_iff)
 
   171   apply(simp add: Abs_fresh_iff)
 
   175   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   172   apply(simp add: Abs_fresh_iff)
 
   176   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   173   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   177   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   174   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   178   apply(elim conjE)
 
   175   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   179   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   176   apply(elim conjE)
 
   180   apply(simp add: Abs_fresh_iff)
 
   177   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   181   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   178   apply(simp add: Abs_fresh_iff)
 
   182   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   179   apply(simp add: Abs_fresh_iff)
 
   183   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   180   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   184   apply(elim conjE)
 
   181   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   185   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   182   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   186   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   183   apply(elim conjE)
 
   187   apply(erule Abs_lst1_fcb2)
 
   184   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   188   apply(simp add: Abs_fresh_iff)
 
   185   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   189   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   186   apply(erule Abs_lst1_fcb2)
 
   190   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   187   apply(simp add: Abs_fresh_iff)
 
   191   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   188   apply(simp add: Abs_fresh_iff)
 
   192   apply(blast)
 
   189   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   193   apply(blast)
 
   190   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   194   apply(elim conjE)
 
   191   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   195   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   192   apply(blast)
 
       
   193   apply(blast)
 
       
   194   apply(elim conjE)
 
       
   195   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
       
   196   apply(simp add: Abs_fresh_iff)
 
   196   apply(simp add: Abs_fresh_iff)
 
   197   apply(simp add: Abs_fresh_iff)
 
   197   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   198   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   198   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   199   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   199   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   200   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   200   apply(rule conjI)
 
   201   apply(rule conjI)
 
   201   apply(elim conjE)
 
   202   apply(elim conjE)
 
   202   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   203   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   203   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   204   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   204   apply(erule Abs_lst1_fcb2)
 
   205   apply(erule Abs_lst1_fcb2)
 
       
   206   apply(simp add: Abs_fresh_iff)
 
   205   apply(simp add: Abs_fresh_iff)
 
   207   apply(simp add: Abs_fresh_iff)
 
   206   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   208   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   207   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   209   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   208   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   210   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   209   apply(blast)
 
   211   apply(blast)
 
   211   apply(erule conjE)+
 
   213   apply(erule conjE)+
 
   212   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   214   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   213   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   215   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   214   apply(erule Abs_lst1_fcb2)
 
   216   apply(erule Abs_lst1_fcb2)
 
   215   apply(simp add: Abs_fresh_iff)
 
   217   apply(simp add: Abs_fresh_iff)
 
   216   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   218   apply(simp add: Abs_fresh_iff)
 
   217   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   219   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   218   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   220   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   219   apply(blast)
 
   221   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   220   apply(blast)
 
   222   apply(blast)
 
   221   apply(elim conjE)
 
   223   apply(blast)
 
   222   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   224   apply(elim conjE)
 
   223   apply(simp add: Abs_fresh_iff)
 
   225   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   224   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   226   apply(simp add: Abs_fresh_iff)
 
   225   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   227   apply(simp add: Abs_fresh_iff)
 
   226   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   228   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   227   apply(elim conjE)
 
   229   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   228   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   230   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   229   apply(simp add: Abs_fresh_iff)
 
   231   apply(elim conjE)
 
   230   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   232   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
 
   231   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   233   apply(simp add: Abs_fresh_iff)
 
   232   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   234   apply(simp add: Abs_fresh_iff)
 
   233   apply(elim conjE)
 
   235   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   234   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   236   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   235   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   237   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   236   apply(erule Abs_lst1_fcb2)
 
   238   apply(elim conjE)
 
   237   apply(simp add: Abs_fresh_iff)
 
   239   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   238   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   240   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   239   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   241   apply(erule Abs_lst1_fcb2)
 
   240   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   242   apply(simp add: Abs_fresh_iff)
 
   241   apply(blast)
 
   243   apply(simp add: Abs_fresh_iff)
 
   242   apply(blast)
 
   244   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   243   apply(erule conjE)+
 
   245   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   244   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   246   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   245   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   247   apply(blast)
 
   246   apply(erule Abs_lst1_fcb2)
 
   248   apply(blast)
 
       
   249   apply(erule conjE)+
 
       
   250   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
       
   251   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
       
   252   apply(erule Abs_lst1_fcb2)
 
       
   253   apply(simp add: Abs_fresh_iff)
 
   247   apply(simp add: Abs_fresh_iff)
 
   254   apply(simp add: Abs_fresh_iff)
 
   248   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   255   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   249   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   256   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   250   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   257   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   251   apply(blast)
 
   258   apply(blast)
 
   253   apply(rule conjI)
 
   260   apply(rule conjI)
 
   254   apply(erule conjE)+
 
   261   apply(erule conjE)+
 
   255   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   262   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   256   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   263   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   257   apply(erule Abs_lst1_fcb2)
 
   264   apply(erule Abs_lst1_fcb2)
 
       
   265   apply(simp add: Abs_fresh_iff)
 
   258   apply(simp add: Abs_fresh_iff)
 
   266   apply(simp add: Abs_fresh_iff)
 
   259   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   267   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   260   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   268   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   261   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   269   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   262   apply(blast)
 
   270   apply(blast)
 
   264   apply(erule conjE)+
 
   272   apply(erule conjE)+
 
   265   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   273   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   266   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   274   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   267   apply(erule Abs_lst1_fcb2)
 
   275   apply(erule Abs_lst1_fcb2)
 
   268   apply(simp add: Abs_fresh_iff)
 
   276   apply(simp add: Abs_fresh_iff)
 
       
   277   apply(simp add: Abs_fresh_iff)
 
   269   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   278   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   270   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   279   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   271   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   280   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   272   apply(blast)
 
   281   apply(blast)
 
   273   apply(blast)
 
   282   apply(blast)
 
   275   apply(erule conjE)+
 
   284   apply(erule conjE)+
 
   276   apply(rule conjI)
 
   285   apply(rule conjI)
 
   277   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   286   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
 
   278   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   287   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
 
   279   apply(erule Abs_lst1_fcb2)
 
   288   apply(erule Abs_lst1_fcb2)
 
       
   289   apply(simp add: Abs_fresh_iff)
 
   280   apply(simp add: Abs_fresh_iff)
 
   290   apply(simp add: Abs_fresh_iff)
 
   281   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   291   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   282   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   292   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   283   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   293   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   284   apply(blast)
 
   294   apply(blast)
 
   285   apply(blast)  
   295   apply(blast)  
   286   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   296   apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
 
   287   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   297   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
 
   288   apply(erule Abs_lst1_fcb2)
 
   298   apply(erule Abs_lst1_fcb2)
 
   289   apply(simp add: Abs_fresh_iff)
 
   299   apply(simp add: Abs_fresh_iff)
 
       
   300   apply(simp add: Abs_fresh_iff)
 
   290   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   301   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
 
   291   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   302   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   292   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   303   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 
   293   apply(blast)
 
   304   apply(blast)
 
   294   apply(blast)
 
   305   apply(blast)
nominal2