canonical introduction and destruction rules for pairwise
authorhaftmann
Sun Oct 08 22:28:20 2017 +0200 (19 months ago)
changeset 66802627511c13164
parent 66801 f3fda9777f9a
child 66803 dd8922885a68
canonical introduction and destruction rules for pairwise
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Set.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -1849,12 +1849,34 @@
     1.4  definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
     1.5    where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
     1.6  
     1.7 +lemma pairwiseI:
     1.8 +  "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
     1.9 +  using that by (simp add: pairwise_def)
    1.10 +
    1.11 +lemma pairwiseD:
    1.12 +  "R x y" and "R y x"
    1.13 +  if "pairwise R S" "x \<in> S" and "y \<in> S" and "x \<noteq> y"
    1.14 +  using that by (simp_all add: pairwise_def)
    1.15 +
    1.16 +lemma pairwise_empty [simp]: "pairwise P {}"
    1.17 +  by (simp add: pairwise_def)
    1.18 +
    1.19 +lemma pairwise_singleton [simp]: "pairwise P {A}"
    1.20 +  by (simp add: pairwise_def)
    1.21 +
    1.22 +lemma pairwise_insert:
    1.23 +  "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
    1.24 +  by (force simp: pairwise_def)
    1.25 +
    1.26  lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
    1.27    by (force simp: pairwise_def)
    1.28  
    1.29  lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
    1.30    by (auto simp: pairwise_def)
    1.31  
    1.32 +lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
    1.33 +  by (force simp: pairwise_def)
    1.34 +
    1.35  definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.36    where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
    1.37  
    1.38 @@ -1882,19 +1904,6 @@
    1.39  lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
    1.40    by (auto simp: disjnt_def)
    1.41  
    1.42 -lemma pairwise_empty [simp]: "pairwise P {}"
    1.43 -  by (simp add: pairwise_def)
    1.44 -
    1.45 -lemma pairwise_singleton [simp]: "pairwise P {A}"
    1.46 -  by (simp add: pairwise_def)
    1.47 -
    1.48 -lemma pairwise_insert:
    1.49 -  "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
    1.50 -  by (force simp: pairwise_def)
    1.51 -
    1.52 -lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
    1.53 -  by (force simp: pairwise_def)
    1.54 -
    1.55  lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
    1.56    unfolding disjnt_def pairwise_def by fast
    1.57