equal
deleted
inserted
replaced
765 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
765 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
766 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
766 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
767 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |
767 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |
768 unfolding fresh_star_def |
768 unfolding fresh_star_def |
769 by(auto simp add: Abs_fresh_iff) |
769 by(auto simp add: Abs_fresh_iff) |
|
770 |
|
771 lemma Abs_fresh_star2: |
|
772 fixes x::"'a::fs" |
|
773 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x" |
|
774 and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x" |
|
775 and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x" |
|
776 unfolding fresh_star_def Abs_fresh_iff |
|
777 by auto |
|
778 |
770 |
779 |
771 lemma Abs1_eq: |
780 lemma Abs1_eq: |
772 fixes x::"'a::fs" |
781 fixes x::"'a::fs" |
773 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y" |
782 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y" |
774 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y" |
783 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y" |