# HG changeset patch
# User nipkow
# Date 1236009235 -3600
# Node ID 922f944f03b268ba7bd21a6f766b0f178e8411be
# Parent  391e10b42889eddaef4d031b901c07fd27bc4031
name changes

diff -r 391e10b42889 -r 922f944f03b2 NEWS
--- a/NEWS	Mon Mar 02 08:26:03 2009 +0100
+++ b/NEWS	Mon Mar 02 16:53:55 2009 +0100
@@ -348,6 +348,9 @@
 etc. slightly changed.  Some theorems named order_class.* now named
 preorder_class.*.
 
+* HOL/Relation:
+Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on".
+
 * HOL/Finite_Set: added a new fold combinator of type
   ('a => 'b => 'b) => 'b => 'a set => 'b
 Occasionally this is more convenient than the old fold combinator which is
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -602,8 +602,8 @@
   interpret group G by fact
   show ?thesis
   proof (intro equiv.intro)
-    show "refl (carrier G) (rcong H)"
-      by (auto simp add: r_congruent_def refl_def) 
+    show "refl_on (carrier G) (rcong H)"
+      by (auto simp add: r_congruent_def refl_on_def) 
   next
     show "sym (rcong H)"
     proof (simp add: r_congruent_def sym_def, clarify)
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -20,8 +20,8 @@
       and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
                              (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
 
-lemma (in sylow) RelM_refl: "refl calM RelM"
-apply (auto simp add: refl_def RelM_def calM_def)
+lemma (in sylow) RelM_refl_on: "refl_on calM RelM"
+apply (auto simp add: refl_on_def RelM_def calM_def)
 apply (blast intro!: coset_mult_one [symmetric])
 done
 
@@ -40,7 +40,7 @@
 
 lemma (in sylow) RelM_equiv: "equiv calM RelM"
 apply (unfold equiv_def)
-apply (blast intro: RelM_refl RelM_sym RelM_trans)
+apply (blast intro: RelM_refl_on RelM_sym RelM_trans)
 done
 
 lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Equiv_Relations.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -12,7 +12,7 @@
 
 locale equiv =
   fixes A and r
-  assumes refl: "refl A r"
+  assumes refl_on: "refl_on A r"
     and sym: "sym r"
     and trans: "trans r"
 
@@ -27,21 +27,21 @@
     "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
   by (unfold trans_def sym_def converse_def) blast
 
-lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r"
-  by (unfold refl_def) blast
+lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
+  by (unfold refl_on_def) blast
 
 lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"
   apply (unfold equiv_def)
   apply clarify
   apply (rule equalityI)
-   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
+   apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
   done
 
 text {* Second half. *}
 
 lemma comp_equivI:
     "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
-  apply (unfold equiv_def refl_def sym_def trans_def)
+  apply (unfold equiv_def refl_on_def sym_def trans_def)
   apply (erule equalityE)
   apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")
    apply fast
@@ -63,12 +63,12 @@
   done
 
 lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}"
-  by (unfold equiv_def refl_def) blast
+  by (unfold equiv_def refl_on_def) blast
 
 lemma subset_equiv_class:
     "equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
   -- {* lemma for the next result *}
-  by (unfold equiv_def refl_def) blast
+  by (unfold equiv_def refl_on_def) blast
 
 lemma eq_equiv_class:
     "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
@@ -79,7 +79,7 @@
   by (unfold equiv_def trans_def sym_def) blast
 
 lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
-  by (unfold equiv_def refl_def) blast
+  by (unfold equiv_def refl_on_def) blast
 
 theorem equiv_class_eq_iff:
   "equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
@@ -103,7 +103,7 @@
   by (unfold quotient_def) blast
 
 lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
-  by (unfold equiv_def refl_def quotient_def) blast
+  by (unfold equiv_def refl_on_def quotient_def) blast
 
 lemma quotient_disj:
   "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"
@@ -228,7 +228,7 @@
 
 lemma congruent2_implies_congruent:
     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
-  by (unfold congruent_def congruent2_def equiv_def refl_def) blast
+  by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast
 
 lemma congruent2_implies_congruent_UN:
   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
@@ -237,7 +237,7 @@
   apply clarify
   apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
   apply (simp add: UN_equiv_class congruent2_implies_congruent)
-  apply (unfold congruent2_def equiv_def refl_def)
+  apply (unfold congruent2_def equiv_def refl_on_def)
   apply (blast del: equalityI)
   done
 
@@ -272,7 +272,7 @@
     ==> congruent2 r1 r2 f"
   -- {* Suggested by John Harrison -- the two subproofs may be *}
   -- {* \emph{much} simpler than the direct proof. *}
-  apply (unfold congruent2_def equiv_def refl_def)
+  apply (unfold congruent2_def equiv_def refl_on_def)
   apply clarify
   apply (blast intro: trans)
   done
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Induct/LList.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -8,7 +8,7 @@
 bounds on the amount of lookahead required.
 
 Could try (but would it work for the gfp analogue of term?)
-  LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)"
+  LListD_Fun_def "LListD_Fun(A) == (%Z. Id_on({Numb(0)}) <++> Id_on(A) <**> Z)"
 
 A nice but complex example would be [ML for the Working Programmer, page 176]
   from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
@@ -95,7 +95,7 @@
   llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" where
     "llistD_Fun(r) =   
         prod_fun Abs_LList Abs_LList `         
-                LListD_Fun (diag(range Leaf))   
+                LListD_Fun (Id_on(range Leaf))   
                             (prod_fun Rep_LList Rep_LList ` r)"
 
 
@@ -265,12 +265,12 @@
 subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *}
 
 text{*This theorem is actually used, unlike the many similar ones in ZF*}
-lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
+lemma LListD_unfold: "LListD r = dsum (Id_on {Numb 0}) (dprod r (LListD r))"
   by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
            elim: LListD.cases [unfolded NIL_def CONS_def])
 
 lemma LListD_implies_ntrunc_equality [rule_format]:
-     "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
+     "\<forall>M N. (M,N) \<in> LListD(Id_on A) --> ntrunc k M = ntrunc k N"
 apply (induct_tac "k" rule: nat_less_induct) 
 apply (safe del: equalityI)
 apply (erule LListD.cases)
@@ -283,7 +283,7 @@
 
 text{*The domain of the @{text LListD} relation*}
 lemma Domain_LListD: 
-    "Domain (LListD(diag A)) \<subseteq> llist(A)"
+    "Domain (LListD(Id_on A)) \<subseteq> llist(A)"
 apply (rule subsetI)
 apply (erule llist.coinduct)
 apply (simp add: NIL_def CONS_def)
@@ -291,10 +291,10 @@
 done
 
 text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*}
-lemma LListD_subset_diag: "LListD(diag A) \<subseteq> diag(llist(A))"
+lemma LListD_subset_Id_on: "LListD(Id_on A) \<subseteq> Id_on(llist(A))"
 apply (rule subsetI)
 apply (rule_tac p = x in PairE, safe)
-apply (rule diag_eqI)
+apply (rule Id_on_eqI)
 apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption) 
 apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
 done
@@ -321,7 +321,7 @@
 by (simp add: LListD_Fun_def NIL_def)
 
 lemma LListD_Fun_CONS_I: 
-     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
+     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (Id_on A) s"
 by (simp add: LListD_Fun_def CONS_def, blast)
 
 text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
@@ -335,24 +335,24 @@
 
 
 text{*This converse inclusion helps to strengthen @{text LList_equalityI}*}
-lemma diag_subset_LListD: "diag(llist(A)) \<subseteq> LListD(diag A)"
+lemma Id_on_subset_LListD: "Id_on(llist(A)) \<subseteq> LListD(Id_on A)"
 apply (rule subsetI)
 apply (erule LListD_coinduct)
 apply (rule subsetI)
-apply (erule diagE)
+apply (erule Id_onE)
 apply (erule ssubst)
 apply (erule llist.cases)
-apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
+apply (simp_all add: Id_onI LListD_Fun_NIL_I LListD_Fun_CONS_I)
 done
 
-lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
-apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
+lemma LListD_eq_Id_on: "LListD(Id_on A) = Id_on(llist(A))"
+apply (rule equalityI LListD_subset_Id_on Id_on_subset_LListD)+
 done
 
-lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
-apply (rule LListD_eq_diag [THEN subst])
+lemma LListD_Fun_Id_on_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (Id_on A) (X Un Id_on(llist(A)))"
+apply (rule LListD_eq_Id_on [THEN subst])
 apply (rule LListD_Fun_LListD_I)
-apply (simp add: LListD_eq_diag diagI)
+apply (simp add: LListD_eq_Id_on Id_onI)
 done
 
 
@@ -360,11 +360,11 @@
       [also admits true equality]
    Replace @{text A} by some particular set, like @{text "{x. True}"}??? *}
 lemma LList_equalityI:
-     "[| (M,N) \<in> r;  r \<subseteq> LListD_Fun (diag A) (r Un diag(llist(A))) |] 
+     "[| (M,N) \<in> r;  r \<subseteq> LListD_Fun (Id_on A) (r Un Id_on(llist(A))) |] 
       ==>  M=N"
-apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
+apply (rule LListD_subset_Id_on [THEN subsetD, THEN Id_onE])
 apply (erule LListD_coinduct)
-apply (simp add: LListD_eq_diag, safe)
+apply (simp add: LListD_eq_Id_on, safe)
 done
 
 
@@ -525,14 +525,14 @@
      f(NIL)=g(NIL);                                              
      !!x l. [| x\<in>A;  l \<in> llist(A) |] ==>                          
             (f(CONS x l),g(CONS x l)) \<in>                          
-                LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un   
-                                    diag(llist(A)))              
+                LListD_Fun (Id_on A) ((%u.(f(u),g(u)))`llist(A) Un   
+                                    Id_on(llist(A)))              
   |] ==> f(M) = g(M)"
 apply (rule LList_equalityI)
 apply (erule imageI)
 apply (rule image_subsetI)
 apply (erule_tac a=x in llist.cases)
-apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) 
+apply (erule ssubst, erule ssubst, erule LListD_Fun_Id_on_I, blast) 
 done
 
 
@@ -687,7 +687,7 @@
 
 lemma LListD_Fun_subset_Times_llist: 
     "r \<subseteq> (llist A) <*> (llist A) 
-     ==> LListD_Fun (diag A) r \<subseteq> (llist A) <*> (llist A)"
+     ==> LListD_Fun (Id_on A) r \<subseteq> (llist A) <*> (llist A)"
 by (auto simp add: LListD_Fun_def)
 
 lemma subset_Times_llist:
@@ -703,9 +703,9 @@
 apply (simp add: LListI [THEN Abs_LList_inverse])
 done
 
-lemma prod_fun_range_eq_diag:
+lemma prod_fun_range_eq_Id_on:
      "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) =  
-      diag(llist(range Leaf))"
+      Id_on(llist(range Leaf))"
 apply (rule equalityI, blast) 
 apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
 done
@@ -730,10 +730,10 @@
 apply (rule image_compose [THEN subst])
 apply (rule prod_fun_compose [THEN subst])
 apply (subst image_Un)
-apply (subst prod_fun_range_eq_diag)
+apply (subst prod_fun_range_eq_Id_on)
 apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
 apply (rule subset_Times_llist [THEN Un_least])
-apply (rule diag_subset_Times)
+apply (rule Id_on_subset_Times)
 done
 
 subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *}
@@ -755,8 +755,8 @@
 apply (rule Rep_LList_inverse [THEN subst])
 apply (rule prod_fun_imageI)
 apply (subst image_Un)
-apply (subst prod_fun_range_eq_diag)
-apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
+apply (subst prod_fun_range_eq_Id_on)
+apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_Id_on_I])
 done
 
 text{*A special case of @{text list_equality} for functions over lazy lists*}
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -47,7 +47,7 @@
 
 theorem equiv_msgrel: "equiv UNIV msgrel"
 proof -
-  have "reflexive msgrel" by (simp add: refl_def msgrel_refl)
+  have "refl msgrel" by (simp add: refl_on_def msgrel_refl)
   moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
   moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
   ultimately show ?thesis by (simp add: equiv_def)
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -44,7 +44,7 @@
 
 theorem equiv_exprel: "equiv UNIV exprel"
 proof -
-  have "reflexive exprel" by (simp add: refl_def exprel_refl)
+  have "refl exprel" by (simp add: refl_on_def exprel_refl)
   moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
   moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
   ultimately show ?thesis by (simp add: equiv_def)
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Int.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -77,7 +77,7 @@
 by (simp add: intrel_def)
 
 lemma equiv_intrel: "equiv UNIV intrel"
-by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
+by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
 
 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -298,12 +298,12 @@
       (CONS a M, CONS b N) \<in> EqLList r"
 
 lemma EqLList_unfold:
-    "EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))"
+    "EqLList r = dsum (Id_on {Datatype.Numb 0}) (dprod r (EqLList r))"
   by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
            elim: EqLList.cases [unfolded NIL_def CONS_def])
 
 lemma EqLList_implies_ntrunc_equality:
-    "(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
+    "(M, N) \<in> EqLList (Id_on A) \<Longrightarrow> ntrunc k M = ntrunc k N"
   apply (induct k arbitrary: M N rule: nat_less_induct)
   apply (erule EqLList.cases)
    apply (safe del: equalityI)
@@ -314,28 +314,28 @@
    apply (simp_all add: CONS_def less_Suc_eq)
   done
 
-lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A"
+lemma Domain_EqLList: "Domain (EqLList (Id_on A)) \<subseteq> LList A"
   apply (rule subsetI)
   apply (erule LList.coinduct)
   apply (subst (asm) EqLList_unfold)
   apply (auto simp add: NIL_def CONS_def)
   done
 
-lemma EqLList_diag: "EqLList (diag A) = diag (LList A)"
+lemma EqLList_Id_on: "EqLList (Id_on A) = Id_on (LList A)"
   (is "?lhs = ?rhs")
 proof
   show "?lhs \<subseteq> ?rhs"
     apply (rule subsetI)
     apply (rule_tac p = x in PairE)
     apply clarify
-    apply (rule diag_eqI)
+    apply (rule Id_on_eqI)
      apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
        assumption)
     apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
     done
   {
-    fix M N assume "(M, N) \<in> diag (LList A)"
-    then have "(M, N) \<in> EqLList (diag A)"
+    fix M N assume "(M, N) \<in> Id_on (LList A)"
+    then have "(M, N) \<in> EqLList (Id_on A)"
     proof coinduct
       case (EqLList M N)
       then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
@@ -344,7 +344,7 @@
         case NIL with MN have ?EqNIL by simp
         then show ?thesis ..
       next
-        case CONS with MN have ?EqCONS by (simp add: diagI)
+        case CONS with MN have ?EqCONS by (simp add: Id_onI)
         then show ?thesis ..
       qed
     qed
@@ -352,8 +352,8 @@
   then show "?rhs \<subseteq> ?lhs" by auto
 qed
 
-lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
-  by (simp only: EqLList_diag)
+lemma EqLList_Id_on_iff [iff]: "(p \<in> EqLList (Id_on A)) = (p \<in> Id_on (LList A))"
+  by (simp only: EqLList_Id_on)
 
 
 text {*
@@ -367,11 +367,11 @@
     and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
       M = NIL \<and> N = NIL \<or>
         (\<exists>a b M' N'.
-          M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
-            ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
+          M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> Id_on A \<and>
+            ((M', N') \<in> r \<or> (M', N') \<in> EqLList (Id_on A)))"
   shows "M = N"
 proof -
-  from r have "(M, N) \<in> EqLList (diag A)"
+  from r have "(M, N) \<in> EqLList (Id_on A)"
   proof coinduct
     case EqLList
     then show ?case by (rule step)
@@ -387,8 +387,8 @@
             (f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
             (\<exists>M N a b.
               (f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
-                (a, b) \<in> diag A \<and>
-                (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> diag (LList A))"
+                (a, b) \<in> Id_on A \<and>
+                (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> Id_on (LList A))"
       (is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
   shows "f M = g M"
 proof -
@@ -401,8 +401,8 @@
     from L show ?case
     proof (cases L)
       case NIL
-      with fun_NIL and MN have "(M, N) \<in> diag (LList A)" by auto
-      then have "(M, N) \<in> EqLList (diag A)" ..
+      with fun_NIL and MN have "(M, N) \<in> Id_on (LList A)" by auto
+      then have "(M, N) \<in> EqLList (Id_on A)" ..
       then show ?thesis by cases simp_all
     next
       case (CONS a K)
@@ -411,23 +411,23 @@
       then show ?thesis
       proof
         assume ?NIL
-        with MN CONS have "(M, N) \<in> diag (LList A)" by auto
-        then have "(M, N) \<in> EqLList (diag A)" ..
+        with MN CONS have "(M, N) \<in> Id_on (LList A)" by auto
+        then have "(M, N) \<in> EqLList (Id_on A)" ..
         then show ?thesis by cases simp_all
       next
         assume ?CONS
         with CONS obtain a b M' N' where
             fg: "(f L, g L) = (CONS a M', CONS b N')"
-          and ab: "(a, b) \<in> diag A"
-          and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
+          and ab: "(a, b) \<in> Id_on A"
+          and M'N': "(M', N') \<in> ?bisim \<union> Id_on (LList A)"
           by blast
         from M'N' show ?thesis
         proof
           assume "(M', N') \<in> ?bisim"
           with MN fg ab show ?thesis by simp
         next
-          assume "(M', N') \<in> diag (LList A)"
-          then have "(M', N') \<in> EqLList (diag A)" ..
+          assume "(M', N') \<in> Id_on (LList A)"
+          then have "(M', N') \<in> EqLList (Id_on A)" ..
           with MN fg ab show ?thesis by simp
         qed
       qed
@@ -463,7 +463,7 @@
       with h h' MN have "M = CONS (fst p) (h (snd p))"
 	and "N = CONS (fst p) (h' (snd p))"
         by (simp_all split: prod.split)
-      then have ?EqCONS by (auto iff: diag_iff)
+      then have ?EqCONS by (auto iff: Id_on_iff)
       then show ?thesis ..
     qed
   qed
@@ -498,7 +498,7 @@
     next
       assume "?EqLCons (l1, l2)"
       with MN have ?EqCONS
-        by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV)
+        by (force simp add: Rep_llist_LCons EqLList_Id_on intro: Rep_llist_UNIV)
       then show ?thesis ..
     qed
   qed
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -10,7 +10,7 @@
 
 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"
 
@@ -57,7 +57,7 @@
 
 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"
 
@@ -73,7 +73,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_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)
 
@@ -83,7 +83,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_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"
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -297,7 +297,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_def) (metis transD)
+	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
     qed
     thus "EX u:Field r. ?P u" using `u:Field r` by blast
   qed
@@ -322,7 +322,7 @@
              (infix "initial'_segment'_of" 55) where
 "r initial_segment_of s == (r,s):init_seg_of"
 
-lemma refl_init_seg_of[simp]: "r initial_segment_of r"
+lemma refl_on_init_seg_of[simp]: "r initial_segment_of r"
 by(simp add:init_seg_of_def)
 
 lemma trans_init_seg_of:
@@ -411,7 +411,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_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_on_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
@@ -420,7 +420,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_def)
+    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_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)"
@@ -452,7 +452,7 @@
     proof
       assume "m={}"
       moreover have "Well_order {(x,x)}"
-	by(simp add:order_on_defs refl_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
+	by(simp add:order_on_defs refl_on_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
@@ -467,7 +467,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_def)
+    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_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`
@@ -500,10 +500,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_def)
+    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_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_def 1 univ)
+  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
   moreover have "trans ?r" using `trans r`
     unfolding trans_def by blast
   moreover have "antisym ?r" using `antisym r`
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/List.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -3226,7 +3226,7 @@
 lemma lenlex_conv:
     "lenlex r = {(xs,ys). length xs < length ys |
                  length xs = length ys \<and> (xs, ys) : lex r}"
-by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
+by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
 
 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
 by (simp add: lex_conv)
@@ -3392,8 +3392,8 @@
 apply (erule listrel.induct, auto) 
 done
 
-lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
-apply (simp add: refl_def listrel_subset Ball_def)
+lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
+apply (simp add: refl_on_def listrel_subset Ball_def)
 apply (rule allI) 
 apply (induct_tac x) 
 apply (auto intro: listrel.intros)
@@ -3414,7 +3414,7 @@
 done
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
-by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
+by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
 
 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
 by (blast intro: listrel.intros)
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/MetisExamples/Tarski.thy
--- a/src/HOL/MetisExamples/Tarski.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/MetisExamples/Tarski.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -61,7 +61,7 @@
   "Top po == greatest (%x. True) po"
 
   PartialOrder :: "('a potype) set"
-  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
+  "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
                        trans (order P)}"
 
   CompleteLattice :: "('a potype) set"
@@ -126,7 +126,7 @@
 
 subsection {* Partial Order *}
 
-lemma (in PO) PO_imp_refl: "refl A r"
+lemma (in PO) PO_imp_refl_on: "refl_on A r"
 apply (insert cl_po)
 apply (simp add: PartialOrder_def A_def r_def)
 done
@@ -143,7 +143,7 @@
 
 lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
 apply (insert cl_po)
-apply (simp add: PartialOrder_def refl_def A_def r_def)
+apply (simp add: PartialOrder_def refl_on_def A_def r_def)
 done
 
 lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
@@ -166,7 +166,7 @@
 apply (simp (no_asm) add: PartialOrder_def)
 apply auto
 -- {* refl *}
-apply (simp add: refl_def induced_def)
+apply (simp add: refl_on_def induced_def)
 apply (blast intro: reflE)
 -- {* antisym *}
 apply (simp add: antisym_def induced_def)
@@ -203,7 +203,7 @@
 
 lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
 apply (insert cl_po)
-apply (simp add: PartialOrder_def dual_def refl_converse
+apply (simp add: PartialOrder_def dual_def refl_on_converse
                  trans_converse antisym_converse)
 done
 
@@ -230,12 +230,12 @@
 
 lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
 
-declare PO.PO_imp_refl  [OF PO.intro [OF CL_imp_PO], simp]
+declare PO.PO_imp_refl_on  [OF PO.intro [OF CL_imp_PO], simp]
 declare PO.PO_imp_sym   [OF PO.intro [OF CL_imp_PO], simp]
 declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp]
 
-lemma (in CL) CO_refl: "refl A r"
-by (rule PO_imp_refl)
+lemma (in CL) CO_refl_on: "refl_on A r"
+by (rule PO_imp_refl_on)
 
 lemma (in CL) CO_antisym: "antisym r"
 by (rule PO_imp_sym)
@@ -501,10 +501,10 @@
 apply (rule conjI)
 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
 (*??no longer terminates, with combinators
-apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
+apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
 *)
-apply (metis CO_refl lubH_le_flubH monotoneE [OF monotone_f] reflD1 reflD2)
-apply (metis CO_refl lubH_le_flubH reflD2)
+apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2)
+apply (metis CO_refl_on lubH_le_flubH refl_onD2)
 done
   declare CLF.f_in_funcset[rule del] funcset_mem[rule del] 
           CL.lub_in_lattice[rule del] PO.monotoneE[rule del] 
@@ -542,12 +542,12 @@
   by (metis 5 3)
 have 7: "(lub H cl, lub H cl) \<in> r"
   by (metis 6 4)
-have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r"
-  by (metis 7 reflD2)
-have 9: "\<not> refl A r"
+have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r"
+  by (metis 7 refl_onD2)
+have 9: "\<not> refl_on A r"
   by (metis 8 2)
 show "False"
-  by (metis CO_refl 9);
+  by (metis CO_refl_on 9);
 next --{*apparently the way to insert a second structured proof*}
   show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
   f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
@@ -589,13 +589,13 @@
 apply (simp add: fix_def)
 apply (rule conjI)
 ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} 
-apply (metis CO_refl lubH_le_flubH reflD1)
+apply (metis CO_refl_on lubH_le_flubH refl_onD1)
 apply (metis antisymE flubH_le_lubH lubH_le_flubH)
 done
 
 lemma (in CLF) fix_in_H:
      "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
-by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl
+by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on
                     fix_subset [of f A, THEN subsetD])
 
 
@@ -678,16 +678,16 @@
 
 
 ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*}
-  declare (in CLF) CO_refl[simp] refl_def [simp]
+  declare (in CLF) CO_refl_on[simp] refl_on_def [simp]
 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
-by (metis CO_refl reflD1)
-  declare (in CLF) CO_refl[simp del]  refl_def [simp del]
+by (metis CO_refl_on refl_onD1)
+  declare (in CLF) CO_refl_on[simp del]  refl_on_def [simp del]
 
 ML{*AtpWrapper.problem_name:="Tarski__interval_subset"*}
   declare (in CLF) rel_imp_elem[intro] 
   declare interval_def [simp]
 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_eq)
+by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
   declare (in CLF) rel_imp_elem[rule del] 
   declare interval_def [simp del]
 
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -64,7 +64,7 @@
 
 lemma equiv_starrel: "equiv UNIV starrel"
 proof (rule equiv.intro)
-  show "reflexive starrel" by (simp add: refl_def)
+  show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
   show "trans starrel" by (auto intro: transI elim!: ultra)
 qed
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Rational.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -21,8 +21,8 @@
   "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
   by (simp add: ratrel_def)
 
-lemma refl_ratrel: "refl {x. snd x \<noteq> 0} ratrel"
-  by (auto simp add: refl_def ratrel_def)
+lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
+  by (auto simp add: refl_on_def ratrel_def)
 
 lemma sym_ratrel: "sym ratrel"
   by (simp add: ratrel_def sym_def)
@@ -44,7 +44,7 @@
 qed
   
 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
-  by (rule equiv.intro [OF refl_ratrel sym_ratrel trans_ratrel])
+  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
 
 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/RealDef.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -94,7 +94,7 @@
 by (simp add: realrel_def)
 
 lemma equiv_realrel: "equiv UNIV realrel"
-apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def)
+apply (auto simp add: equiv_def refl_on_def sym_def trans_def realrel_def)
 apply (blast dest: preal_trans_lemma) 
 done
 
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -34,8 +34,8 @@
   "Id == {p. EX x. p = (x,x)}"
 
 definition
-  diag  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
-  "diag A == \<Union>x\<in>A. {(x,x)}"
+  Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
+  "Id_on A == \<Union>x\<in>A. {(x,x)}"
 
 definition
   Domain :: "('a * 'b) set => 'a set" where
@@ -50,12 +50,12 @@
   "Field r == Domain r \<union> Range r"
 
 definition
-  refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
-  "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
+  refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
+  "refl_on A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
 
 abbreviation
-  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
-  "reflexive == refl UNIV"
+  refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
+  "refl == refl_on UNIV"
 
 definition
   sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
@@ -99,8 +99,8 @@
 lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
 by (unfold Id_def) blast
 
-lemma reflexive_Id: "reflexive Id"
-by (simp add: refl_def)
+lemma refl_Id: "refl Id"
+by (simp add: refl_on_def)
 
 lemma antisym_Id: "antisym Id"
   -- {* A strange result, since @{text Id} is also symmetric. *}
@@ -115,24 +115,24 @@
 
 subsection {* Diagonal: identity over a set *}
 
-lemma diag_empty [simp]: "diag {} = {}"
-by (simp add: diag_def) 
+lemma Id_on_empty [simp]: "Id_on {} = {}"
+by (simp add: Id_on_def) 
 
-lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
-by (simp add: diag_def)
+lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
+by (simp add: Id_on_def)
 
-lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
-by (rule diag_eqI) (rule refl)
+lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
+by (rule Id_on_eqI) (rule refl)
 
-lemma diagE [elim!]:
-  "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
+lemma Id_onE [elim!]:
+  "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   -- {* The general elimination rule. *}
-by (unfold diag_def) (iprover elim!: UN_E singletonE)
+by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
 
-lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
+lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
 by blast
 
-lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
+lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
 by blast
 
 
@@ -184,37 +184,37 @@
 
 subsection {* Reflexivity *}
 
-lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
-by (unfold refl_def) (iprover intro!: ballI)
+lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
+by (unfold refl_on_def) (iprover intro!: ballI)
 
-lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
-by (unfold refl_def) blast
+lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
+by (unfold refl_on_def) blast
 
-lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
-by (unfold refl_def) blast
+lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
+by (unfold refl_on_def) blast
 
-lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
-by (unfold refl_def) blast
+lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
+by (unfold refl_on_def) blast
 
-lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
-by (unfold refl_def) blast
+lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
+by (unfold refl_on_def) blast
 
-lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
-by (unfold refl_def) blast
+lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
+by (unfold refl_on_def) blast
 
-lemma refl_INTER:
-  "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
-by (unfold refl_def) fast
+lemma refl_on_INTER:
+  "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
+by (unfold refl_on_def) fast
 
-lemma refl_UNION:
-  "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
-by (unfold refl_def) blast
+lemma refl_on_UNION:
+  "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
+by (unfold refl_on_def) blast
 
-lemma refl_empty[simp]: "refl {} {}"
-by(simp add:refl_def)
+lemma refl_on_empty[simp]: "refl_on {} {}"
+by(simp add:refl_on_def)
 
-lemma refl_diag: "refl A (diag A)"
-by (rule reflI [OF diag_subset_Times diagI])
+lemma refl_on_Id_on: "refl_on A (Id_on A)"
+by (rule refl_onI [OF Id_on_subset_Times Id_onI])
 
 
 subsection {* Antisymmetry *}
@@ -232,7 +232,7 @@
 lemma antisym_empty [simp]: "antisym {}"
 by (unfold antisym_def) blast
 
-lemma antisym_diag [simp]: "antisym (diag A)"
+lemma antisym_Id_on [simp]: "antisym (Id_on A)"
 by (unfold antisym_def) blast
 
 
@@ -256,7 +256,7 @@
 lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
 by (fast intro: symI dest: symD)
 
-lemma sym_diag [simp]: "sym (diag A)"
+lemma sym_Id_on [simp]: "sym (Id_on A)"
 by (rule symI) clarify
 
 
@@ -275,7 +275,7 @@
 lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
 by (fast intro: transI elim: transD)
 
-lemma trans_diag [simp]: "trans (diag A)"
+lemma trans_Id_on [simp]: "trans (Id_on A)"
 by (fast intro: transI elim: transD)
 
 lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
@@ -331,11 +331,11 @@
 lemma converse_Id [simp]: "Id^-1 = Id"
 by blast
 
-lemma converse_diag [simp]: "(diag A)^-1 = diag A"
+lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A"
 by blast
 
-lemma refl_converse [simp]: "refl A (converse r) = refl A r"
-by (unfold refl_def) auto
+lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
+by (unfold refl_on_def) auto
 
 lemma sym_converse [simp]: "sym (converse r) = sym r"
 by (unfold sym_def) blast
@@ -382,7 +382,7 @@
 lemma Domain_Id [simp]: "Domain Id = UNIV"
 by blast
 
-lemma Domain_diag [simp]: "Domain (diag A) = A"
+lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
 by blast
 
 lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
@@ -433,7 +433,7 @@
 lemma Range_Id [simp]: "Range Id = UNIV"
 by blast
 
-lemma Range_diag [simp]: "Range (diag A) = A"
+lemma Range_Id_on [simp]: "Range (Id_on A) = A"
 by auto
 
 lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
@@ -506,7 +506,7 @@
 lemma Image_Id [simp]: "Id `` A = A"
 by blast
 
-lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
+lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B"
 by blast
 
 lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
@@ -571,7 +571,7 @@
 lemma single_valued_Id [simp]: "single_valued Id"
 by (unfold single_valued_def) blast
 
-lemma single_valued_diag [simp]: "single_valued (diag A)"
+lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
 by (unfold single_valued_def) blast
 
 
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -64,8 +64,8 @@
 
 subsection {* Reflexive closure *}
 
-lemma reflexive_reflcl[simp]: "reflexive(r^=)"
-by(simp add:refl_def)
+lemma refl_reflcl[simp]: "refl(r^=)"
+by(simp add:refl_on_def)
 
 lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
 by(simp add:antisym_def)
@@ -118,8 +118,8 @@
   rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
                  consumes 1, case_names refl step]
 
-lemma reflexive_rtrancl: "reflexive (r^*)"
-  by (unfold refl_def) fast
+lemma refl_rtrancl: "refl (r^*)"
+by (unfold refl_on_def) fast
 
 text {* Transitivity of transitive closure. *}
 lemma trans_rtrancl: "trans (r^*)"
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -90,16 +90,15 @@
 
 subsection{*genPrefix is a partial order*}
 
-lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"
-
-apply (unfold refl_def, auto)
+lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
+apply (unfold refl_on_def, auto)
 apply (induct_tac "x")
 prefer 2 apply (blast intro: genPrefix.prepend)
 apply (blast intro: genPrefix.Nil)
 done
 
-lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
-by (erule reflD [OF refl_genPrefix UNIV_I])
+lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r"
+by (erule refl_onD [OF refl_genPrefix UNIV_I])
 
 lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
 apply clarify
@@ -178,8 +177,8 @@
 done
 
 lemma same_genPrefix_genPrefix [simp]: 
-    "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
-apply (unfold refl_def)
+    "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
+apply (unfold refl_on_def)
 apply (induct_tac "xs")
 apply (simp_all (no_asm_simp))
 done
@@ -190,7 +189,7 @@
 by (case_tac "xs", auto)
 
 lemma genPrefix_take_append:
-     "[| reflexive r;  (xs,ys) : genPrefix r |]  
+     "[| refl r;  (xs,ys) : genPrefix r |]  
       ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
 apply (erule genPrefix.induct)
 apply (frule_tac [3] genPrefix_length_le)
@@ -198,7 +197,7 @@
 done
 
 lemma genPrefix_append_both:
-     "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
+     "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
       ==>  (xs@zs, ys @ zs) : genPrefix r"
 apply (drule genPrefix_take_append, assumption)
 apply (simp add: take_all)
@@ -210,7 +209,7 @@
 by auto
 
 lemma aolemma:
-     "[| (xs,ys) : genPrefix r;  reflexive r |]  
+     "[| (xs,ys) : genPrefix r;  refl r |]  
       ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
 apply (erule genPrefix.induct)
   apply blast
@@ -225,7 +224,7 @@
 done
 
 lemma append_one_genPrefix:
-     "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |]  
+     "[| (xs,ys) : genPrefix r;  length xs < length ys;  refl r |]  
       ==> (xs @ [ys ! length xs], ys) : genPrefix r"
 by (blast intro: aolemma [THEN mp])
 
@@ -259,7 +258,7 @@
 
 subsection{*The type of lists is partially ordered*}
 
-declare reflexive_Id [iff] 
+declare refl_Id [iff] 
         antisym_Id [iff] 
         trans_Id [iff]
 
@@ -383,8 +382,8 @@
 
 (** pfixLe **)
 
-lemma reflexive_Le [iff]: "reflexive Le"
-by (unfold refl_def Le_def, auto)
+lemma refl_Le [iff]: "refl Le"
+by (unfold refl_on_def Le_def, auto)
 
 lemma antisym_Le [iff]: "antisym Le"
 by (unfold antisym_def Le_def, auto)
@@ -406,8 +405,8 @@
 apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
 done
 
-lemma reflexive_Ge [iff]: "reflexive Ge"
-by (unfold refl_def Ge_def, auto)
+lemma refl_Ge [iff]: "refl Ge"
+by (unfold refl_on_def Ge_def, auto)
 
 lemma antisym_Ge [iff]: "antisym Ge"
 by (unfold antisym_def Ge_def, auto)
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -344,8 +344,8 @@
 apply (blast intro: clD cl_in_lattice)
 done
 
-lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
-by (simp add: reflI relcl_def subset_cl [THEN subsetD])
+lemma refl_relcl: "lattice L ==> refl (relcl L)"
+by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
 
 lemma trans_relcl: "lattice L ==> trans (relcl L)"
 by (blast intro: relcl_trans transI)
@@ -362,12 +362,12 @@
 
 text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
 lemma cl_latticeof:
-     "[|refl UNIV r; trans r|] 
+     "[|refl r; trans r|] 
       ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
 apply (rule equalityI) 
  apply (rule cl_least) 
   apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
- apply (simp add: latticeof_def refl_def, blast)
+ apply (simp add: latticeof_def refl_on_def, blast)
 apply (simp add: latticeof_def, clarify)
 apply (unfold cl_def, blast) 
 done
@@ -400,7 +400,7 @@
 done
 
 theorem relcl_latticeof_eq:
-     "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
+     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
 by (simp add: relcl_def cl_latticeof)
 
 
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -359,7 +359,7 @@
 
 constdefs
   totalize_act :: "('a * 'a)set => ('a * 'a)set"
-    "totalize_act act == act \<union> diag (-(Domain act))"
+    "totalize_act act == act \<union> Id_on (-(Domain act))"
 
   totalize :: "'a program => 'a program"
     "totalize F == mk_program (Init F,
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -260,7 +260,7 @@
 
 (** Rep_Integ **)
 lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
-  unfolding equiv_def refl_def quotient_def Image_def by auto
+  unfolding equiv_def refl_on_def quotient_def Image_def by auto
 
 lemmas Rep_Integ_ne = Integ.Rep_Integ 
   [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/ZF/Games.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -847,7 +847,7 @@
   by (auto simp add: quotient_def)
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
-  by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
+  by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
     eq_game_sym intro: eq_game_refl eq_game_trans)
 
 instantiation Pg :: "{ord, zero, plus, minus, uminus}"
diff -r 391e10b42889 -r 922f944f03b2 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/ex/Tarski.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -73,7 +73,7 @@
 
 definition
   PartialOrder :: "('a potype) set" where
-  "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) &
+  "PartialOrder = {P. refl_on (pset P) (order P) & antisym (order P) &
                        trans (order P)}"
 
 definition
@@ -158,7 +158,7 @@
 unfolding PartialOrder_def dual_def
 by auto
 
-lemma (in PO) PO_imp_refl [simp]: "refl A r"
+lemma (in PO) PO_imp_refl_on [simp]: "refl_on A r"
 apply (insert cl_po)
 apply (simp add: PartialOrder_def A_def r_def)
 done
@@ -175,7 +175,7 @@
 
 lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
 apply (insert cl_po)
-apply (simp add: PartialOrder_def refl_def A_def r_def)
+apply (simp add: PartialOrder_def refl_on_def A_def r_def)
 done
 
 lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
@@ -198,7 +198,7 @@
 apply (simp (no_asm) add: PartialOrder_def)
 apply auto
 -- {* refl *}
-apply (simp add: refl_def induced_def)
+apply (simp add: refl_on_def induced_def)
 apply (blast intro: reflE)
 -- {* antisym *}
 apply (simp add: antisym_def induced_def)
@@ -235,7 +235,7 @@
 
 lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
 apply (insert cl_po)
-apply (simp add: PartialOrder_def dual_def refl_converse
+apply (simp add: PartialOrder_def dual_def refl_on_converse
                  trans_converse antisym_converse)
 done
 
@@ -266,8 +266,8 @@
 declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
 declare CL_imp_PO [THEN PO.PO_imp_trans, simp]*)
 
-lemma (in CL) CO_refl: "refl A r"
-by (rule PO_imp_refl)
+lemma (in CL) CO_refl_on: "refl_on A r"
+by (rule PO_imp_refl_on)
 
 lemma (in CL) CO_antisym: "antisym r"
 by (rule PO_imp_sym)
@@ -533,7 +533,7 @@
 
 lemma (in CLF) fix_in_H:
      "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
-by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl
+by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on
                     fix_subset [of f A, THEN subsetD])
 
 lemma (in CLF) fixf_le_lubH:
@@ -583,8 +583,8 @@
 subsection {* interval *}
 
 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
-apply (insert CO_refl)
-apply (simp add: refl_def, blast)
+apply (insert CO_refl_on)
+apply (simp add: refl_on_def, blast)
 done
 
 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
@@ -754,7 +754,7 @@
 apply (rule notI)
 apply (drule_tac a = "Top cl" in equals0D)
 apply (simp add: interval_def)
-apply (simp add: refl_def Top_in_lattice Top_prop)
+apply (simp add: refl_on_def Top_in_lattice Top_prop)
 done
 
 lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}"