author nipkow Fri, 14 Mar 2008 19:58:01 +0100 changeset 26273 6c4d534af98d parent 26272 d63776c3be97 child 26274 2bdb61a28971
Orders as relations
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Order_Relation.thy	Fri Mar 14 19:58:01 2008 +0100
@@ -0,0 +1,76 @@
+(*  ID          : \$Id\$
+    Author      : Tobias Nipkow
+
+Orders as relations with implicit base set, their Field
+*)
+
+header {* Orders as Relations *}
+
+theory Order_Relation
+begin
+
+definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
+definition "Preorder r \<equiv> Refl r \<and> trans r"
+definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
+definition "Total r \<equiv> \<forall>x\<in>Field r.\<forall>y\<in>Field r. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
+definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
+definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
+
+lemmas Order_defs =
+  Preorder_def Partial_order_def Linear_order_def Well_order_def
+
+lemma Refl_empty[simp]: "Refl {}"
+
+lemma Preorder_empty[simp]: "Preorder {}"
+
+lemma Partial_order_empty[simp]: "Partial_order {}"
+
+lemma Total_empty[simp]: "Total {}"
+
+lemma Linear_order_empty[simp]: "Linear_order {}"
+
+lemma Well_order_empty[simp]: "Well_order {}"
+
+lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
+
+lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
+
+lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r"
+
+lemma Total_converse[simp]: "Total (r^-1) = Total r"
+by (auto simp: Total_def)
+
+lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r"
+
+lemma subset_Image_Image_iff:
+  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
+   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
+apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
+apply metis
+by(metis trans_def)
+
+lemma subset_Image1_Image1_iff:
+  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"