4 

     5 

     6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)

     7 lemma in_permute_iff:

     8   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"

     9 apply(unfold mem_def permute_fun_def)[1]

    10 apply(simp add: permute_bool_def) 

    11 done

    12 

    13 lemma fresh_star_permute_iff:

    14   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"

    15 apply(simp add: fresh_star_def)

    16 apply(auto)

    17 apply(drule_tac x="p \<bullet> xa" in bspec)

    18 apply(unfold mem_def permute_fun_def)[1] 

    19 apply(simp add: eqvts)

    20 apply(simp add: fresh_permute_iff)

    21 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])

    22 apply(simp)

    23 apply(drule_tac x="- p \<bullet> xa" in bspec)

    24 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])

    25 apply(simp)

    26 apply(simp)

    27 done

    28 

    29 lemma fresh_minus_perm:

    30   fixes p::perm

    31   shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"

    32   apply(simp add: fresh_def)

    33   apply(simp only: supp_minus_perm)

    34   done

    35 

    36 lemma fresh_plus:

    37   fixes p q::perm

    38   shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"

    39 unfolding fresh_def

    40 using supp_plus_perm

    41 apply(auto)

    42 done

    43 

    44 lemma fresh_star_plus:

    45   fixes p q::perm

    46   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"

    47 unfolding fresh_star_def

    48 by (simp add: fresh_plus)

    49