equal
deleted
inserted
replaced
1903 |
1903 |
1904 text \<open>Misc\<close> |
1904 text \<open>Misc\<close> |
1905 |
1905 |
1906 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)" |
1906 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)" |
1907 |
1907 |
|
1908 lemma pairwise_subset: "\<lbrakk>pairwise P S; T \<subseteq> S\<rbrakk> \<Longrightarrow> pairwise P T" |
|
1909 by (force simp: pairwise_def) |
|
1910 |
1908 definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}" |
1911 definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}" |
1909 |
1912 |
1910 lemma pairwise_disjoint_empty [simp]: "pairwise disjnt {}" |
1913 lemma pairwise_empty [simp]: "pairwise P {}" |
1911 by (simp add: pairwise_def disjnt_def) |
1914 by (simp add: pairwise_def) |
1912 |
1915 |
1913 lemma pairwise_disjoint_singleton [simp]: "pairwise disjnt {A}" |
1916 lemma pairwise_singleton [simp]: "pairwise P {A}" |
1914 by (simp add: pairwise_def disjnt_def) |
1917 by (simp add: pairwise_def) |
1915 |
1918 |
1916 hide_const (open) member not_member |
1919 hide_const (open) member not_member |
1917 |
1920 |
1918 lemmas equalityI = subset_antisym |
1921 lemmas equalityI = subset_antisym |
1919 |
1922 |