# HG changeset patch
# User ballarin
# Date 1217346612 -7200
# Node ID cb6c513922e0fb273cb6e5fa47c1d4ca64ff2550
# Parent  80608e96e76062aa646db9360fc7cc545204b55b
Definitions and some lemmas for reflexive orderings.

diff -r 80608e96e760 -r cb6c513922e0 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Tue Jul 29 17:49:26 2008 +0200
+++ b/src/ZF/Order.thy	Tue Jul 29 17:50:12 2008 +0200
@@ -5,12 +5,17 @@
 
 Results from the book "Set Theory: an Introduction to Independence Proofs"
         by Kenneth Kunen.  Chapter 1, section 6.
+Additional definitions and lemmas for reflexive orders.
 *)
 
 header{*Partial and Total Orderings: Basic Definitions and Properties*}
 
 theory Order imports WF Perm begin
 
+text {* We adopt the following convention: @{text ord} is used for
+  strict orders and @{text order} is used for their reflexive
+  counterparts. *}
+
 definition
   part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)  where
    "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
@@ -24,6 +29,18 @@
    "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
 
 definition
+  "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)"
+
+definition                              (*Partial ordering*)
+  "partial_order_on(A, r) \<equiv> preorder_on(A, r) \<and> antisym(r)"
+
+abbreviation
+  "Preorder(r) \<equiv> preorder_on(field(r), r)"
+
+abbreviation
+  "Partial_order(r) \<equiv> partial_order_on(field(r), r)"
+
+definition
   well_ord :: "[i,i]=>o"          	(*Well-ordering*)  where
    "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
 
@@ -645,4 +662,59 @@
 apply (erule theI)
 done
 
+
+subsection {* Lemmas for the Reflexive Orders *}
+
+lemma subset_vimage_vimage_iff:
+  "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
+  r -`` A \<subseteq> r -`` B <-> (ALL a:A. EX b:B. <a, b> : r)"
+  apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
+   apply blast
+  unfolding trans_on_def
+  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
+          \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
+    (* instance obtained from proof term generated by best *)
+   apply best
+  apply blast
+  done
+
+lemma subset_vimage1_vimage1_iff:
+  "[| Preorder(r); a : field(r); b : field(r) |] ==>
+  r -`` {a} \<subseteq> r -`` {b} <-> <a, b> : r"
+  by (simp add: subset_vimage_vimage_iff)
+
+lemma Refl_antisym_eq_Image1_Image1_iff:
+  "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
+  r `` {a} = r `` {b} <-> a = b"
+  apply rule
+   apply (frule equality_iffD)
+   apply (drule equality_iffD)
+   apply (simp add: antisym_def refl_def)
+   apply best
+  apply (simp add: antisym_def refl_def)
+  done
+
+lemma Partial_order_eq_Image1_Image1_iff:
+  "[| Partial_order(r); a : field(r); b : field(r) |] ==>
+  r `` {a} = r `` {b} <-> a = b"
+  by (simp add: partial_order_on_def preorder_on_def
+    Refl_antisym_eq_Image1_Image1_iff)
+
+lemma Refl_antisym_eq_vimage1_vimage1_iff:
+  "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
+  r -`` {a} = r -`` {b} <-> a = b"
+  apply rule
+   apply (frule equality_iffD)
+   apply (drule equality_iffD)
+   apply (simp add: antisym_def refl_def)
+   apply best
+  apply (simp add: antisym_def refl_def)
+  done
+
+lemma Partial_order_eq_vimage1_vimage1_iff:
+  "[| Partial_order(r); a : field(r); b : field(r) |] ==>
+  r -`` {a} = r -`` {b} <-> a = b"
+  by (simp add: partial_order_on_def preorder_on_def
+    Refl_antisym_eq_vimage1_vimage1_iff)
+
 end