reorganization

--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 17 16:47:24 2008 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 17 16:47:45 2008 +0100
@@ -8,9 +8,7 @@
 imports ATP_Linkup Hilbert_Choice
 begin
 
-(* FIXME to Relation *)
-
-definition "refl_on A r \<equiv> \<forall>x\<in>A. (x,x) \<in> r"
+text{* This prelude could be moved to theory Relation: *}
 
 definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
 
@@ -19,14 +17,11 @@
 abbreviation "total \<equiv> total_on UNIV"
 
 
-lemma refl_on_empty[simp]: "refl_on {} r"
-by(simp add:refl_on_def)
-
 lemma total_on_empty[simp]: "total_on {} r"
 by(simp add:total_on_def)
 
-lemma refl_on_converse[simp]: "refl_on A (r^-1) = refl_on A r"
-by(simp add:refl_on_def)
+lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r"
+by(auto simp add:refl_def)
 
 lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
 by (auto simp: total_on_def)
@@ -42,9 +37,10 @@
 lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
 by(simp add: total_on_def)
 
+
 subsection{* Orders on a set *}
 
-definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
+definition "preorder_on A r \<equiv> refl A r \<and> trans r"
 
 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
 
@@ -91,7 +87,7 @@
 
 subsection{* Orders on the field *}
 
-abbreviation "Refl r \<equiv> refl_on (Field r) r"
+abbreviation "Refl r \<equiv> refl (Field r) r"
 
 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
 
@@ -107,7 +103,7 @@
 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_on_def refl_on_def Image_def)
+apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
 apply metis
 by(metis trans_def)
 
@@ -117,7 +113,7 @@
 
 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_on_def) metis
+by(simp add: expand_set_eq antisym_def refl_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"

--- a/src/HOL/Library/Zorn.thy	Mon Mar 17 16:47:24 2008 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Mar 17 16:47:45 2008 +0100
@@ -301,7 +301,7 @@
       fix a B assume aB: "B:C" "a:B"
       with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
       thus "(a,u) : r" using uA aB `Preorder r`
-	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
+	by (auto simp add: preorder_on_def refl_def) (metis transD)
     qed
     thus "EX u:Field r. ?P u" using `u:Field r` by blast
   qed
@@ -414,7 +414,7 @@
     by(simp add:Chain_def I_def) blast
   have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   hence 0: "Partial_order I"
-    by(auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def trans_def I_def elim!: trans_init_seg_of)
+    by(auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_def trans_def I_def elim!: trans_init_seg_of)
 -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   { fix R assume "R \<in> Chain I"
     hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
@@ -423,7 +423,7 @@
     have "\<forall>r\<in>R. Refl r" "\<forall>r\<in>R. trans r" "\<forall>r\<in>R. antisym r" "\<forall>r\<in>R. Total r"
          "\<forall>r\<in>R. wf(r-Id)"
       using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:order_on_defs)
-    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_def)
+    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_def)
     moreover have "trans (\<Union>R)"
       by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
     moreover have "antisym(\<Union>R)"
@@ -455,7 +455,7 @@
     proof
       assume "m={}"
       moreover have "Well_order {(x,x)}"
-	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
+	by(simp add:order_on_defs refl_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
       ultimately show False using max
 	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
     qed
@@ -470,7 +470,7 @@
     have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
       using `Well_order m` by(simp_all add:order_on_defs)
 --{*We show that the extension is a well-order*}
-    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
+    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_def)
     moreover have "trans ?m" using `trans m` `x \<notin> Field m`
       unfolding trans_def Field_def Domain_def Range_def by blast
     moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
@@ -503,10 +503,10 @@
     using well_ordering[where 'a = "'a"] by blast
   let ?r = "{(x,y). x:A & y:A & (x,y):r}"
   have 1: "Field ?r = A" using wo univ
-    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
+    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_def)
   have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
     using `Well_order r` by(simp_all add:order_on_defs)
-  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
+  have "Refl ?r" using `Refl r` by(auto simp:refl_def 1 univ)
   moreover have "trans ?r" using `trans r`
     unfolding trans_def by blast
   moreover have "antisym ?r" using `antisym r`