Definitions and some lemmas for reflexive orderings.
authorballarin
Tue Jul 29 17:50:12 2008 +0200 (2008-07-29)
changeset 27703cb6c513922e0
parent 27702 80608e96e760
child 27704 5b1585b48952
Definitions and some lemmas for reflexive orderings.
src/ZF/Order.thy
     1.1 --- a/src/ZF/Order.thy	Tue Jul 29 17:49:26 2008 +0200
     1.2 +++ b/src/ZF/Order.thy	Tue Jul 29 17:50:12 2008 +0200
     1.3 @@ -5,12 +5,17 @@
     1.4  
     1.5  Results from the book "Set Theory: an Introduction to Independence Proofs"
     1.6          by Kenneth Kunen.  Chapter 1, section 6.
     1.7 +Additional definitions and lemmas for reflexive orders.
     1.8  *)
     1.9  
    1.10  header{*Partial and Total Orderings: Basic Definitions and Properties*}
    1.11  
    1.12  theory Order imports WF Perm begin
    1.13  
    1.14 +text {* We adopt the following convention: @{text ord} is used for
    1.15 +  strict orders and @{text order} is used for their reflexive
    1.16 +  counterparts. *}
    1.17 +
    1.18  definition
    1.19    part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)  where
    1.20     "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    1.21 @@ -24,6 +29,18 @@
    1.22     "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
    1.23  
    1.24  definition
    1.25 +  "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)"
    1.26 +
    1.27 +definition                              (*Partial ordering*)
    1.28 +  "partial_order_on(A, r) \<equiv> preorder_on(A, r) \<and> antisym(r)"
    1.29 +
    1.30 +abbreviation
    1.31 +  "Preorder(r) \<equiv> preorder_on(field(r), r)"
    1.32 +
    1.33 +abbreviation
    1.34 +  "Partial_order(r) \<equiv> partial_order_on(field(r), r)"
    1.35 +
    1.36 +definition
    1.37    well_ord :: "[i,i]=>o"          	(*Well-ordering*)  where
    1.38     "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
    1.39  
    1.40 @@ -645,4 +662,59 @@
    1.41  apply (erule theI)
    1.42  done
    1.43  
    1.44 +
    1.45 +subsection {* Lemmas for the Reflexive Orders *}
    1.46 +
    1.47 +lemma subset_vimage_vimage_iff:
    1.48 +  "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
    1.49 +  r -`` A \<subseteq> r -`` B <-> (ALL a:A. EX b:B. <a, b> : r)"
    1.50 +  apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
    1.51 +   apply blast
    1.52 +  unfolding trans_on_def
    1.53 +  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
    1.54 +          \<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)
    1.55 +    (* instance obtained from proof term generated by best *)
    1.56 +   apply best
    1.57 +  apply blast
    1.58 +  done
    1.59 +
    1.60 +lemma subset_vimage1_vimage1_iff:
    1.61 +  "[| Preorder(r); a : field(r); b : field(r) |] ==>
    1.62 +  r -`` {a} \<subseteq> r -`` {b} <-> <a, b> : r"
    1.63 +  by (simp add: subset_vimage_vimage_iff)
    1.64 +
    1.65 +lemma Refl_antisym_eq_Image1_Image1_iff:
    1.66 +  "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
    1.67 +  r `` {a} = r `` {b} <-> a = b"
    1.68 +  apply rule
    1.69 +   apply (frule equality_iffD)
    1.70 +   apply (drule equality_iffD)
    1.71 +   apply (simp add: antisym_def refl_def)
    1.72 +   apply best
    1.73 +  apply (simp add: antisym_def refl_def)
    1.74 +  done
    1.75 +
    1.76 +lemma Partial_order_eq_Image1_Image1_iff:
    1.77 +  "[| Partial_order(r); a : field(r); b : field(r) |] ==>
    1.78 +  r `` {a} = r `` {b} <-> a = b"
    1.79 +  by (simp add: partial_order_on_def preorder_on_def
    1.80 +    Refl_antisym_eq_Image1_Image1_iff)
    1.81 +
    1.82 +lemma Refl_antisym_eq_vimage1_vimage1_iff:
    1.83 +  "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
    1.84 +  r -`` {a} = r -`` {b} <-> a = b"
    1.85 +  apply rule
    1.86 +   apply (frule equality_iffD)
    1.87 +   apply (drule equality_iffD)
    1.88 +   apply (simp add: antisym_def refl_def)
    1.89 +   apply best
    1.90 +  apply (simp add: antisym_def refl_def)
    1.91 +  done
    1.92 +
    1.93 +lemma Partial_order_eq_vimage1_vimage1_iff:
    1.94 +  "[| Partial_order(r); a : field(r); b : field(r) |] ==>
    1.95 +  r -`` {a} = r -`` {b} <-> a = b"
    1.96 +  by (simp add: partial_order_on_def preorder_on_def
    1.97 +    Refl_antisym_eq_vimage1_vimage1_iff)
    1.98 +
    1.99  end