equal
deleted
inserted
replaced
521 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
521 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
522 unfolding fresh_def |
522 unfolding fresh_def |
523 unfolding supp_Abs |
523 unfolding supp_Abs |
524 by auto |
524 by auto |
525 |
525 |
|
526 lemma Abs_fresh_star_iff: |
|
527 fixes x::"'a::fs" |
|
528 shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x" |
|
529 and "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x" |
|
530 and "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x" |
|
531 unfolding fresh_star_def |
|
532 by (auto simp add: Abs_fresh_iff) |
|
533 |
526 lemma Abs_fresh_star: |
534 lemma Abs_fresh_star: |
527 fixes x::"'a::fs" |
535 fixes x::"'a::fs" |
528 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
536 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
529 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
537 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
530 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |
538 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |