equal
deleted
inserted
replaced
1847 text \<open>Misc\<close> |
1847 text \<open>Misc\<close> |
1848 |
1848 |
1849 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" |
1849 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" |
1850 where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)" |
1850 where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)" |
1851 |
1851 |
1852 lemma pairwiseI: |
1852 lemma pairwiseI [intro?]: |
1853 "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y" |
1853 "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y" |
1854 using that by (simp add: pairwise_def) |
1854 using that by (simp add: pairwise_def) |
1855 |
1855 |
1856 lemma pairwiseD: |
1856 lemma pairwiseD: |
1857 "R x y" and "R y x" |
1857 "R x y" and "R y x" |
1869 by (force simp: pairwise_def) |
1869 by (force simp: pairwise_def) |
1870 |
1870 |
1871 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T" |
1871 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T" |
1872 by (force simp: pairwise_def) |
1872 by (force simp: pairwise_def) |
1873 |
1873 |
1874 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A" |
1874 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y; B \<subseteq> A\<rbrakk> \<Longrightarrow> pairwise Q B" |
1875 by (auto simp: pairwise_def) |
1875 by (fastforce simp: pairwise_def) |
1876 |
1876 |
1877 lemma pairwise_imageI: |
1877 lemma pairwise_imageI: |
1878 "pairwise P (f ` A)" |
1878 "pairwise P (f ` A)" |
1879 if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)" |
1879 if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)" |
1880 using that by (auto intro: pairwiseI) |
1880 using that by (auto intro: pairwiseI) |