# HG changeset patch
# User haftmann
# Date 1507494500 -7200
# Node ID 627511c13164eea39b69c2dddb5d9ce46bc21c7e
# Parent  f3fda9777f9a0259ee4768683c7df97ff8d9b859
canonical introduction and destruction rules for pairwise

diff -r f3fda9777f9a -r 627511c13164 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Set.thy	Sun Oct 08 22:28:20 2017 +0200
@@ -1849,12 +1849,34 @@
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
+lemma pairwiseI:
+  "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
+  using that by (simp add: pairwise_def)
+
+lemma pairwiseD:
+  "R x y" and "R y x"
+  if "pairwise R S" "x \<in> S" and "y \<in> S" and "x \<noteq> y"
+  using that by (simp_all add: pairwise_def)
+
+lemma pairwise_empty [simp]: "pairwise P {}"
+  by (simp add: pairwise_def)
+
+lemma pairwise_singleton [simp]: "pairwise P {A}"
+  by (simp add: pairwise_def)
+
+lemma pairwise_insert:
+  "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"
+  by (force simp: pairwise_def)
+
 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
   by (force simp: pairwise_def)
 
 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
   by (auto simp: pairwise_def)
 
+lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
+  by (force simp: pairwise_def)
+
 definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
 
@@ -1882,19 +1904,6 @@
 lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
   by (auto simp: disjnt_def)
 
-lemma pairwise_empty [simp]: "pairwise P {}"
-  by (simp add: pairwise_def)
-
-lemma pairwise_singleton [simp]: "pairwise P {A}"
-  by (simp add: pairwise_def)
-
-lemma pairwise_insert:
-  "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"
-  by (force simp: pairwise_def)
-
-lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
-  by (force simp: pairwise_def)
-
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast