1.1 --- a/src/HOL/Library/Order_Relation.thy	Fri May 24 17:37:06 2013 +0200
     1.2 +++ b/src/HOL/Library/Order_Relation.thy	Fri May 24 18:11:57 2013 +0200
     1.3 @@ -87,6 +87,23 @@
     1.4    "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
     1.5  by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
     1.6  
     1.7 +lemma Total_Id_Field:
     1.8 +assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
     1.9 +shows "Field r = Field(r - Id)"
    1.10 +using mono_Field[of "r - Id" r] Diff_subset[of r Id]
    1.11 +proof(auto)
    1.12 +  have "r \<noteq> {}" using NID by fast
    1.13 +  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast
    1.14 +  hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
    1.15 +  (*  *)
    1.16 +  fix a assume *: "a \<in> Field r"
    1.17 +  obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
    1.18 +  using * 1 by auto
    1.19 +  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
    1.20 +  by (simp add: total_on_def)
    1.21 +  thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
    1.22 +qed
    1.23 +
    1.24  
    1.25  subsection{* Orders on a type *}
    1.26