src/HOL/Library/Order_Relation.thy

 imports Main
 begin
 
 subsection{* Orders on a set *}
 
-definition "preorder_on A r \<equiv> refl A r \<and> trans r"
+definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
 
 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
 
 definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
 

 by(simp add: order_on_defs trans_diff_Id)
 
 
 subsection{* Orders on the field *}
 
-abbreviation "Refl r \<equiv> refl (Field r) r"
+abbreviation "Refl r \<equiv> refl_on (Field r) r"
 
 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
 
 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) 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_eq preorder_on_def refl_def Image_def)
+apply(auto simp add: subset_eq preorder_on_def refl_on_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"
 by(simp add:subset_Image_Image_iff)
 
 lemma Refl_antisym_eq_Image1_Image1_iff:
   "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(simp add: expand_set_eq antisym_def refl_def) metis
+by(simp add: expand_set_eq antisym_def refl_on_def) metis
 
 lemma Partial_order_eq_Image1_Image1_iff:
   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
 by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)