equal
deleted
inserted
replaced
1598 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
1598 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
1599 |
1599 |
1600 lemma fresh_star_supp_conv: |
1600 lemma fresh_star_supp_conv: |
1601 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
1601 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
1602 by (auto simp add: fresh_star_def fresh_def) |
1602 by (auto simp add: fresh_star_def fresh_def) |
|
1603 |
|
1604 lemma fresh_star_perm_set_conv: |
|
1605 fixes p::"perm" |
|
1606 assumes fresh: "as \<sharp>* p" |
|
1607 and fin: "finite as" |
|
1608 shows "supp p \<sharp>* as" |
|
1609 apply(rule fresh_star_supp_conv) |
|
1610 apply(simp add: supp_finite_atom_set fin fresh) |
|
1611 done |
|
1612 |
1603 |
1613 |
1604 lemma fresh_star_Pair: |
1614 lemma fresh_star_Pair: |
1605 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1615 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1606 by (auto simp add: fresh_star_def fresh_Pair) |
1616 by (auto simp add: fresh_star_def fresh_Pair) |
1607 |
1617 |