name changes
authornipkow
Mon Mar 02 16:53:55 2009 +0100 (2009-03-02)
changeset 30198922f944f03b2
parent 30193 391e10b42889
child 30199 1b32021f6d9e
name changes
NEWS
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Equiv_Relations.thy
src/HOL/Induct/LList.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Int.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Zorn.thy
src/HOL/List.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/NSA/StarDef.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/UNITY.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/ZF/Games.thy
src/HOL/ex/Tarski.thy
     1.1 --- a/NEWS	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/NEWS	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -348,6 +348,9 @@
     1.4  etc. slightly changed.  Some theorems named order_class.* now named
     1.5  preorder_class.*.
     1.6  
     1.7 +* HOL/Relation:
     1.8 +Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on".
     1.9 +
    1.10  * HOL/Finite_Set: added a new fold combinator of type
    1.11    ('a => 'b => 'b) => 'b => 'a set => 'b
    1.12  Occasionally this is more convenient than the old fold combinator which is
     2.1 --- a/src/HOL/Algebra/Coset.thy	Mon Mar 02 08:26:03 2009 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Mon Mar 02 16:53:55 2009 +0100
     2.3 @@ -602,8 +602,8 @@
     2.4    interpret group G by fact
     2.5    show ?thesis
     2.6    proof (intro equiv.intro)
     2.7 -    show "refl (carrier G) (rcong H)"
     2.8 -      by (auto simp add: r_congruent_def refl_def) 
     2.9 +    show "refl_on (carrier G) (rcong H)"
    2.10 +      by (auto simp add: r_congruent_def refl_on_def) 
    2.11    next
    2.12      show "sym (rcong H)"
    2.13      proof (simp add: r_congruent_def sym_def, clarify)
     3.1 --- a/src/HOL/Algebra/Sylow.thy	Mon Mar 02 08:26:03 2009 +0100
     3.2 +++ b/src/HOL/Algebra/Sylow.thy	Mon Mar 02 16:53:55 2009 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4        and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
     3.5                               (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
     3.6  
     3.7 -lemma (in sylow) RelM_refl: "refl calM RelM"
     3.8 -apply (auto simp add: refl_def RelM_def calM_def)
     3.9 +lemma (in sylow) RelM_refl_on: "refl_on calM RelM"
    3.10 +apply (auto simp add: refl_on_def RelM_def calM_def)
    3.11  apply (blast intro!: coset_mult_one [symmetric])
    3.12  done
    3.13  
    3.14 @@ -40,7 +40,7 @@
    3.15  
    3.16  lemma (in sylow) RelM_equiv: "equiv calM RelM"
    3.17  apply (unfold equiv_def)
    3.18 -apply (blast intro: RelM_refl RelM_sym RelM_trans)
    3.19 +apply (blast intro: RelM_refl_on RelM_sym RelM_trans)
    3.20  done
    3.21  
    3.22  lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
     4.1 --- a/src/HOL/Equiv_Relations.thy	Mon Mar 02 08:26:03 2009 +0100
     4.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Mar 02 16:53:55 2009 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5  locale equiv =
     4.6    fixes A and r
     4.7 -  assumes refl: "refl A r"
     4.8 +  assumes refl_on: "refl_on A r"
     4.9      and sym: "sym r"
    4.10      and trans: "trans r"
    4.11  
    4.12 @@ -27,21 +27,21 @@
    4.13      "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
    4.14    by (unfold trans_def sym_def converse_def) blast
    4.15  
    4.16 -lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r"
    4.17 -  by (unfold refl_def) blast
    4.18 +lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
    4.19 +  by (unfold refl_on_def) blast
    4.20  
    4.21  lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"
    4.22    apply (unfold equiv_def)
    4.23    apply clarify
    4.24    apply (rule equalityI)
    4.25 -   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
    4.26 +   apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
    4.27    done
    4.28  
    4.29  text {* Second half. *}
    4.30  
    4.31  lemma comp_equivI:
    4.32      "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
    4.33 -  apply (unfold equiv_def refl_def sym_def trans_def)
    4.34 +  apply (unfold equiv_def refl_on_def sym_def trans_def)
    4.35    apply (erule equalityE)
    4.36    apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")
    4.37     apply fast
    4.38 @@ -63,12 +63,12 @@
    4.39    done
    4.40  
    4.41  lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}"
    4.42 -  by (unfold equiv_def refl_def) blast
    4.43 +  by (unfold equiv_def refl_on_def) blast
    4.44  
    4.45  lemma subset_equiv_class:
    4.46      "equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
    4.47    -- {* lemma for the next result *}
    4.48 -  by (unfold equiv_def refl_def) blast
    4.49 +  by (unfold equiv_def refl_on_def) blast
    4.50  
    4.51  lemma eq_equiv_class:
    4.52      "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
    4.53 @@ -79,7 +79,7 @@
    4.54    by (unfold equiv_def trans_def sym_def) blast
    4.55  
    4.56  lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
    4.57 -  by (unfold equiv_def refl_def) blast
    4.58 +  by (unfold equiv_def refl_on_def) blast
    4.59  
    4.60  theorem equiv_class_eq_iff:
    4.61    "equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
    4.62 @@ -103,7 +103,7 @@
    4.63    by (unfold quotient_def) blast
    4.64  
    4.65  lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
    4.66 -  by (unfold equiv_def refl_def quotient_def) blast
    4.67 +  by (unfold equiv_def refl_on_def quotient_def) blast
    4.68  
    4.69  lemma quotient_disj:
    4.70    "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"
    4.71 @@ -228,7 +228,7 @@
    4.72  
    4.73  lemma congruent2_implies_congruent:
    4.74      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
    4.75 -  by (unfold congruent_def congruent2_def equiv_def refl_def) blast
    4.76 +  by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast
    4.77  
    4.78  lemma congruent2_implies_congruent_UN:
    4.79    "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
    4.80 @@ -237,7 +237,7 @@
    4.81    apply clarify
    4.82    apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
    4.83    apply (simp add: UN_equiv_class congruent2_implies_congruent)
    4.84 -  apply (unfold congruent2_def equiv_def refl_def)
    4.85 +  apply (unfold congruent2_def equiv_def refl_on_def)
    4.86    apply (blast del: equalityI)
    4.87    done
    4.88  
    4.89 @@ -272,7 +272,7 @@
    4.90      ==> congruent2 r1 r2 f"
    4.91    -- {* Suggested by John Harrison -- the two subproofs may be *}
    4.92    -- {* \emph{much} simpler than the direct proof. *}
    4.93 -  apply (unfold congruent2_def equiv_def refl_def)
    4.94 +  apply (unfold congruent2_def equiv_def refl_on_def)
    4.95    apply clarify
    4.96    apply (blast intro: trans)
    4.97    done
     5.1 --- a/src/HOL/Induct/LList.thy	Mon Mar 02 08:26:03 2009 +0100
     5.2 +++ b/src/HOL/Induct/LList.thy	Mon Mar 02 16:53:55 2009 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  bounds on the amount of lookahead required.
     5.5  
     5.6  Could try (but would it work for the gfp analogue of term?)
     5.7 -  LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)"
     5.8 +  LListD_Fun_def "LListD_Fun(A) == (%Z. Id_on({Numb(0)}) <++> Id_on(A) <**> Z)"
     5.9  
    5.10  A nice but complex example would be [ML for the Working Programmer, page 176]
    5.11    from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
    5.12 @@ -95,7 +95,7 @@
    5.13    llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" where
    5.14      "llistD_Fun(r) =   
    5.15          prod_fun Abs_LList Abs_LList `         
    5.16 -                LListD_Fun (diag(range Leaf))   
    5.17 +                LListD_Fun (Id_on(range Leaf))   
    5.18                              (prod_fun Rep_LList Rep_LList ` r)"
    5.19  
    5.20  
    5.21 @@ -265,12 +265,12 @@
    5.22  subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *}
    5.23  
    5.24  text{*This theorem is actually used, unlike the many similar ones in ZF*}
    5.25 -lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
    5.26 +lemma LListD_unfold: "LListD r = dsum (Id_on {Numb 0}) (dprod r (LListD r))"
    5.27    by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
    5.28             elim: LListD.cases [unfolded NIL_def CONS_def])
    5.29  
    5.30  lemma LListD_implies_ntrunc_equality [rule_format]:
    5.31 -     "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
    5.32 +     "\<forall>M N. (M,N) \<in> LListD(Id_on A) --> ntrunc k M = ntrunc k N"
    5.33  apply (induct_tac "k" rule: nat_less_induct) 
    5.34  apply (safe del: equalityI)
    5.35  apply (erule LListD.cases)
    5.36 @@ -283,7 +283,7 @@
    5.37  
    5.38  text{*The domain of the @{text LListD} relation*}
    5.39  lemma Domain_LListD: 
    5.40 -    "Domain (LListD(diag A)) \<subseteq> llist(A)"
    5.41 +    "Domain (LListD(Id_on A)) \<subseteq> llist(A)"
    5.42  apply (rule subsetI)
    5.43  apply (erule llist.coinduct)
    5.44  apply (simp add: NIL_def CONS_def)
    5.45 @@ -291,10 +291,10 @@
    5.46  done
    5.47  
    5.48  text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*}
    5.49 -lemma LListD_subset_diag: "LListD(diag A) \<subseteq> diag(llist(A))"
    5.50 +lemma LListD_subset_Id_on: "LListD(Id_on A) \<subseteq> Id_on(llist(A))"
    5.51  apply (rule subsetI)
    5.52  apply (rule_tac p = x in PairE, safe)
    5.53 -apply (rule diag_eqI)
    5.54 +apply (rule Id_on_eqI)
    5.55  apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption) 
    5.56  apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
    5.57  done
    5.58 @@ -321,7 +321,7 @@
    5.59  by (simp add: LListD_Fun_def NIL_def)
    5.60  
    5.61  lemma LListD_Fun_CONS_I: 
    5.62 -     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
    5.63 +     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (Id_on A) s"
    5.64  by (simp add: LListD_Fun_def CONS_def, blast)
    5.65  
    5.66  text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
    5.67 @@ -335,24 +335,24 @@
    5.68  
    5.69  
    5.70  text{*This converse inclusion helps to strengthen @{text LList_equalityI}*}
    5.71 -lemma diag_subset_LListD: "diag(llist(A)) \<subseteq> LListD(diag A)"
    5.72 +lemma Id_on_subset_LListD: "Id_on(llist(A)) \<subseteq> LListD(Id_on A)"
    5.73  apply (rule subsetI)
    5.74  apply (erule LListD_coinduct)
    5.75  apply (rule subsetI)
    5.76 -apply (erule diagE)
    5.77 +apply (erule Id_onE)
    5.78  apply (erule ssubst)
    5.79  apply (erule llist.cases)
    5.80 -apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
    5.81 +apply (simp_all add: Id_onI LListD_Fun_NIL_I LListD_Fun_CONS_I)
    5.82  done
    5.83  
    5.84 -lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
    5.85 -apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
    5.86 +lemma LListD_eq_Id_on: "LListD(Id_on A) = Id_on(llist(A))"
    5.87 +apply (rule equalityI LListD_subset_Id_on Id_on_subset_LListD)+
    5.88  done
    5.89  
    5.90 -lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
    5.91 -apply (rule LListD_eq_diag [THEN subst])
    5.92 +lemma LListD_Fun_Id_on_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (Id_on A) (X Un Id_on(llist(A)))"
    5.93 +apply (rule LListD_eq_Id_on [THEN subst])
    5.94  apply (rule LListD_Fun_LListD_I)
    5.95 -apply (simp add: LListD_eq_diag diagI)
    5.96 +apply (simp add: LListD_eq_Id_on Id_onI)
    5.97  done
    5.98  
    5.99  
   5.100 @@ -360,11 +360,11 @@
   5.101        [also admits true equality]
   5.102     Replace @{text A} by some particular set, like @{text "{x. True}"}??? *}
   5.103  lemma LList_equalityI:
   5.104 -     "[| (M,N) \<in> r;  r \<subseteq> LListD_Fun (diag A) (r Un diag(llist(A))) |] 
   5.105 +     "[| (M,N) \<in> r;  r \<subseteq> LListD_Fun (Id_on A) (r Un Id_on(llist(A))) |] 
   5.106        ==>  M=N"
   5.107 -apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
   5.108 +apply (rule LListD_subset_Id_on [THEN subsetD, THEN Id_onE])
   5.109  apply (erule LListD_coinduct)
   5.110 -apply (simp add: LListD_eq_diag, safe)
   5.111 +apply (simp add: LListD_eq_Id_on, safe)
   5.112  done
   5.113  
   5.114  
   5.115 @@ -525,14 +525,14 @@
   5.116       f(NIL)=g(NIL);                                              
   5.117       !!x l. [| x\<in>A;  l \<in> llist(A) |] ==>                          
   5.118              (f(CONS x l),g(CONS x l)) \<in>                          
   5.119 -                LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un   
   5.120 -                                    diag(llist(A)))              
   5.121 +                LListD_Fun (Id_on A) ((%u.(f(u),g(u)))`llist(A) Un   
   5.122 +                                    Id_on(llist(A)))              
   5.123    |] ==> f(M) = g(M)"
   5.124  apply (rule LList_equalityI)
   5.125  apply (erule imageI)
   5.126  apply (rule image_subsetI)
   5.127  apply (erule_tac a=x in llist.cases)
   5.128 -apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) 
   5.129 +apply (erule ssubst, erule ssubst, erule LListD_Fun_Id_on_I, blast) 
   5.130  done
   5.131  
   5.132  
   5.133 @@ -687,7 +687,7 @@
   5.134  
   5.135  lemma LListD_Fun_subset_Times_llist: 
   5.136      "r \<subseteq> (llist A) <*> (llist A) 
   5.137 -     ==> LListD_Fun (diag A) r \<subseteq> (llist A) <*> (llist A)"
   5.138 +     ==> LListD_Fun (Id_on A) r \<subseteq> (llist A) <*> (llist A)"
   5.139  by (auto simp add: LListD_Fun_def)
   5.140  
   5.141  lemma subset_Times_llist:
   5.142 @@ -703,9 +703,9 @@
   5.143  apply (simp add: LListI [THEN Abs_LList_inverse])
   5.144  done
   5.145  
   5.146 -lemma prod_fun_range_eq_diag:
   5.147 +lemma prod_fun_range_eq_Id_on:
   5.148       "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) =  
   5.149 -      diag(llist(range Leaf))"
   5.150 +      Id_on(llist(range Leaf))"
   5.151  apply (rule equalityI, blast) 
   5.152  apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
   5.153  done
   5.154 @@ -730,10 +730,10 @@
   5.155  apply (rule image_compose [THEN subst])
   5.156  apply (rule prod_fun_compose [THEN subst])
   5.157  apply (subst image_Un)
   5.158 -apply (subst prod_fun_range_eq_diag)
   5.159 +apply (subst prod_fun_range_eq_Id_on)
   5.160  apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
   5.161  apply (rule subset_Times_llist [THEN Un_least])
   5.162 -apply (rule diag_subset_Times)
   5.163 +apply (rule Id_on_subset_Times)
   5.164  done
   5.165  
   5.166  subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *}
   5.167 @@ -755,8 +755,8 @@
   5.168  apply (rule Rep_LList_inverse [THEN subst])
   5.169  apply (rule prod_fun_imageI)
   5.170  apply (subst image_Un)
   5.171 -apply (subst prod_fun_range_eq_diag)
   5.172 -apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
   5.173 +apply (subst prod_fun_range_eq_Id_on)
   5.174 +apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_Id_on_I])
   5.175  done
   5.176  
   5.177  text{*A special case of @{text list_equality} for functions over lazy lists*}
     6.1 --- a/src/HOL/Induct/QuoDataType.thy	Mon Mar 02 08:26:03 2009 +0100
     6.2 +++ b/src/HOL/Induct/QuoDataType.thy	Mon Mar 02 16:53:55 2009 +0100
     6.3 @@ -47,7 +47,7 @@
     6.4  
     6.5  theorem equiv_msgrel: "equiv UNIV msgrel"
     6.6  proof -
     6.7 -  have "reflexive msgrel" by (simp add: refl_def msgrel_refl)
     6.8 +  have "refl msgrel" by (simp add: refl_on_def msgrel_refl)
     6.9    moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
    6.10    moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
    6.11    ultimately show ?thesis by (simp add: equiv_def)
     7.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Mon Mar 02 08:26:03 2009 +0100
     7.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Mon Mar 02 16:53:55 2009 +0100
     7.3 @@ -44,7 +44,7 @@
     7.4  
     7.5  theorem equiv_exprel: "equiv UNIV exprel"
     7.6  proof -
     7.7 -  have "reflexive exprel" by (simp add: refl_def exprel_refl)
     7.8 +  have "refl exprel" by (simp add: refl_on_def exprel_refl)
     7.9    moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
    7.10    moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
    7.11    ultimately show ?thesis by (simp add: equiv_def)
     8.1 --- a/src/HOL/Int.thy	Mon Mar 02 08:26:03 2009 +0100
     8.2 +++ b/src/HOL/Int.thy	Mon Mar 02 16:53:55 2009 +0100
     8.3 @@ -77,7 +77,7 @@
     8.4  by (simp add: intrel_def)
     8.5  
     8.6  lemma equiv_intrel: "equiv UNIV intrel"
     8.7 -by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
     8.8 +by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
     8.9  
    8.10  text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    8.11    @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
     9.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Mar 02 08:26:03 2009 +0100
     9.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 02 16:53:55 2009 +0100
     9.3 @@ -298,12 +298,12 @@
     9.4        (CONS a M, CONS b N) \<in> EqLList r"
     9.5  
     9.6  lemma EqLList_unfold:
     9.7 -    "EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))"
     9.8 +    "EqLList r = dsum (Id_on {Datatype.Numb 0}) (dprod r (EqLList r))"
     9.9    by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
    9.10             elim: EqLList.cases [unfolded NIL_def CONS_def])
    9.11  
    9.12  lemma EqLList_implies_ntrunc_equality:
    9.13 -    "(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
    9.14 +    "(M, N) \<in> EqLList (Id_on A) \<Longrightarrow> ntrunc k M = ntrunc k N"
    9.15    apply (induct k arbitrary: M N rule: nat_less_induct)
    9.16    apply (erule EqLList.cases)
    9.17     apply (safe del: equalityI)
    9.18 @@ -314,28 +314,28 @@
    9.19     apply (simp_all add: CONS_def less_Suc_eq)
    9.20    done
    9.21  
    9.22 -lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A"
    9.23 +lemma Domain_EqLList: "Domain (EqLList (Id_on A)) \<subseteq> LList A"
    9.24    apply (rule subsetI)
    9.25    apply (erule LList.coinduct)
    9.26    apply (subst (asm) EqLList_unfold)
    9.27    apply (auto simp add: NIL_def CONS_def)
    9.28    done
    9.29  
    9.30 -lemma EqLList_diag: "EqLList (diag A) = diag (LList A)"
    9.31 +lemma EqLList_Id_on: "EqLList (Id_on A) = Id_on (LList A)"
    9.32    (is "?lhs = ?rhs")
    9.33  proof
    9.34    show "?lhs \<subseteq> ?rhs"
    9.35      apply (rule subsetI)
    9.36      apply (rule_tac p = x in PairE)
    9.37      apply clarify
    9.38 -    apply (rule diag_eqI)
    9.39 +    apply (rule Id_on_eqI)
    9.40       apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
    9.41         assumption)
    9.42      apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
    9.43      done
    9.44    {
    9.45 -    fix M N assume "(M, N) \<in> diag (LList A)"
    9.46 -    then have "(M, N) \<in> EqLList (diag A)"
    9.47 +    fix M N assume "(M, N) \<in> Id_on (LList A)"
    9.48 +    then have "(M, N) \<in> EqLList (Id_on A)"
    9.49      proof coinduct
    9.50        case (EqLList M N)
    9.51        then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
    9.52 @@ -344,7 +344,7 @@
    9.53          case NIL with MN have ?EqNIL by simp
    9.54          then show ?thesis ..
    9.55        next
    9.56 -        case CONS with MN have ?EqCONS by (simp add: diagI)
    9.57 +        case CONS with MN have ?EqCONS by (simp add: Id_onI)
    9.58          then show ?thesis ..
    9.59        qed
    9.60      qed
    9.61 @@ -352,8 +352,8 @@
    9.62    then show "?rhs \<subseteq> ?lhs" by auto
    9.63  qed
    9.64  
    9.65 -lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
    9.66 -  by (simp only: EqLList_diag)
    9.67 +lemma EqLList_Id_on_iff [iff]: "(p \<in> EqLList (Id_on A)) = (p \<in> Id_on (LList A))"
    9.68 +  by (simp only: EqLList_Id_on)
    9.69  
    9.70  
    9.71  text {*
    9.72 @@ -367,11 +367,11 @@
    9.73      and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
    9.74        M = NIL \<and> N = NIL \<or>
    9.75          (\<exists>a b M' N'.
    9.76 -          M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
    9.77 -            ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
    9.78 +          M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> Id_on A \<and>
    9.79 +            ((M', N') \<in> r \<or> (M', N') \<in> EqLList (Id_on A)))"
    9.80    shows "M = N"
    9.81  proof -
    9.82 -  from r have "(M, N) \<in> EqLList (diag A)"
    9.83 +  from r have "(M, N) \<in> EqLList (Id_on A)"
    9.84    proof coinduct
    9.85      case EqLList
    9.86      then show ?case by (rule step)
    9.87 @@ -387,8 +387,8 @@
    9.88              (f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
    9.89              (\<exists>M N a b.
    9.90                (f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
    9.91 -                (a, b) \<in> diag A \<and>
    9.92 -                (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> diag (LList A))"
    9.93 +                (a, b) \<in> Id_on A \<and>
    9.94 +                (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> Id_on (LList A))"
    9.95        (is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
    9.96    shows "f M = g M"
    9.97  proof -
    9.98 @@ -401,8 +401,8 @@
    9.99      from L show ?case
   9.100      proof (cases L)
   9.101        case NIL
   9.102 -      with fun_NIL and MN have "(M, N) \<in> diag (LList A)" by auto
   9.103 -      then have "(M, N) \<in> EqLList (diag A)" ..
   9.104 +      with fun_NIL and MN have "(M, N) \<in> Id_on (LList A)" by auto
   9.105 +      then have "(M, N) \<in> EqLList (Id_on A)" ..
   9.106        then show ?thesis by cases simp_all
   9.107      next
   9.108        case (CONS a K)
   9.109 @@ -411,23 +411,23 @@
   9.110        then show ?thesis
   9.111        proof
   9.112          assume ?NIL
   9.113 -        with MN CONS have "(M, N) \<in> diag (LList A)" by auto
   9.114 -        then have "(M, N) \<in> EqLList (diag A)" ..
   9.115 +        with MN CONS have "(M, N) \<in> Id_on (LList A)" by auto
   9.116 +        then have "(M, N) \<in> EqLList (Id_on A)" ..
   9.117          then show ?thesis by cases simp_all
   9.118        next
   9.119          assume ?CONS
   9.120          with CONS obtain a b M' N' where
   9.121              fg: "(f L, g L) = (CONS a M', CONS b N')"
   9.122 -          and ab: "(a, b) \<in> diag A"
   9.123 -          and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
   9.124 +          and ab: "(a, b) \<in> Id_on A"
   9.125 +          and M'N': "(M', N') \<in> ?bisim \<union> Id_on (LList A)"
   9.126            by blast
   9.127          from M'N' show ?thesis
   9.128          proof
   9.129            assume "(M', N') \<in> ?bisim"
   9.130            with MN fg ab show ?thesis by simp
   9.131          next
   9.132 -          assume "(M', N') \<in> diag (LList A)"
   9.133 -          then have "(M', N') \<in> EqLList (diag A)" ..
   9.134 +          assume "(M', N') \<in> Id_on (LList A)"
   9.135 +          then have "(M', N') \<in> EqLList (Id_on A)" ..
   9.136            with MN fg ab show ?thesis by simp
   9.137          qed
   9.138        qed
   9.139 @@ -463,7 +463,7 @@
   9.140        with h h' MN have "M = CONS (fst p) (h (snd p))"
   9.141  	and "N = CONS (fst p) (h' (snd p))"
   9.142          by (simp_all split: prod.split)
   9.143 -      then have ?EqCONS by (auto iff: diag_iff)
   9.144 +      then have ?EqCONS by (auto iff: Id_on_iff)
   9.145        then show ?thesis ..
   9.146      qed
   9.147    qed
   9.148 @@ -498,7 +498,7 @@
   9.149      next
   9.150        assume "?EqLCons (l1, l2)"
   9.151        with MN have ?EqCONS
   9.152 -        by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV)
   9.153 +        by (force simp add: Rep_llist_LCons EqLList_Id_on intro: Rep_llist_UNIV)
   9.154        then show ?thesis ..
   9.155      qed
   9.156    qed
    10.1 --- a/src/HOL/Library/Order_Relation.thy	Mon Mar 02 08:26:03 2009 +0100
    10.2 +++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 02 16:53:55 2009 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4  
    10.5  subsection{* Orders on a set *}
    10.6  
    10.7 -definition "preorder_on A r \<equiv> refl A r \<and> trans r"
    10.8 +definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    10.9  
   10.10  definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
   10.11  
   10.12 @@ -57,7 +57,7 @@
   10.13  
   10.14  subsection{* Orders on the field *}
   10.15  
   10.16 -abbreviation "Refl r \<equiv> refl (Field r) r"
   10.17 +abbreviation "Refl r \<equiv> refl_on (Field r) r"
   10.18  
   10.19  abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
   10.20  
   10.21 @@ -73,7 +73,7 @@
   10.22  lemma subset_Image_Image_iff:
   10.23    "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
   10.24     r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
   10.25 -apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
   10.26 +apply(auto simp add: subset_eq preorder_on_def refl_on_def Image_def)
   10.27  apply metis
   10.28  by(metis trans_def)
   10.29  
   10.30 @@ -83,7 +83,7 @@
   10.31  
   10.32  lemma Refl_antisym_eq_Image1_Image1_iff:
   10.33    "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   10.34 -by(simp add: expand_set_eq antisym_def refl_def) metis
   10.35 +by(simp add: expand_set_eq antisym_def refl_on_def) metis
   10.36  
   10.37  lemma Partial_order_eq_Image1_Image1_iff:
   10.38    "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    11.1 --- a/src/HOL/Library/Zorn.thy	Mon Mar 02 08:26:03 2009 +0100
    11.2 +++ b/src/HOL/Library/Zorn.thy	Mon Mar 02 16:53:55 2009 +0100
    11.3 @@ -297,7 +297,7 @@
    11.4        fix a B assume aB: "B:C" "a:B"
    11.5        with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
    11.6        thus "(a,u) : r" using uA aB `Preorder r`
    11.7 -	by (auto simp add: preorder_on_def refl_def) (metis transD)
    11.8 +	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
    11.9      qed
   11.10      thus "EX u:Field r. ?P u" using `u:Field r` by blast
   11.11    qed
   11.12 @@ -322,7 +322,7 @@
   11.13               (infix "initial'_segment'_of" 55) where
   11.14  "r initial_segment_of s == (r,s):init_seg_of"
   11.15  
   11.16 -lemma refl_init_seg_of[simp]: "r initial_segment_of r"
   11.17 +lemma refl_on_init_seg_of[simp]: "r initial_segment_of r"
   11.18  by(simp add:init_seg_of_def)
   11.19  
   11.20  lemma trans_init_seg_of:
   11.21 @@ -411,7 +411,7 @@
   11.22      by(simp add:Chain_def I_def) blast
   11.23    have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   11.24    hence 0: "Partial_order I"
   11.25 -    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)
   11.26 +    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)
   11.27  -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   11.28    { fix R assume "R \<in> Chain I"
   11.29      hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
   11.30 @@ -420,7 +420,7 @@
   11.31      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"
   11.32           "\<forall>r\<in>R. wf(r-Id)"
   11.33        using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:order_on_defs)
   11.34 -    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_def)
   11.35 +    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_def)
   11.36      moreover have "trans (\<Union>R)"
   11.37        by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   11.38      moreover have "antisym(\<Union>R)"
   11.39 @@ -452,7 +452,7 @@
   11.40      proof
   11.41        assume "m={}"
   11.42        moreover have "Well_order {(x,x)}"
   11.43 -	by(simp add:order_on_defs refl_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
   11.44 +	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
   11.45        ultimately show False using max
   11.46  	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
   11.47      qed
   11.48 @@ -467,7 +467,7 @@
   11.49      have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
   11.50        using `Well_order m` by(simp_all add:order_on_defs)
   11.51  --{*We show that the extension is a well-order*}
   11.52 -    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_def)
   11.53 +    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
   11.54      moreover have "trans ?m" using `trans m` `x \<notin> Field m`
   11.55        unfolding trans_def Field_def Domain_def Range_def by blast
   11.56      moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
   11.57 @@ -500,10 +500,10 @@
   11.58      using well_ordering[where 'a = "'a"] by blast
   11.59    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
   11.60    have 1: "Field ?r = A" using wo univ
   11.61 -    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_def)
   11.62 +    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
   11.63    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
   11.64      using `Well_order r` by(simp_all add:order_on_defs)
   11.65 -  have "Refl ?r" using `Refl r` by(auto simp:refl_def 1 univ)
   11.66 +  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
   11.67    moreover have "trans ?r" using `trans r`
   11.68      unfolding trans_def by blast
   11.69    moreover have "antisym ?r" using `antisym r`
    12.1 --- a/src/HOL/List.thy	Mon Mar 02 08:26:03 2009 +0100
    12.2 +++ b/src/HOL/List.thy	Mon Mar 02 16:53:55 2009 +0100
    12.3 @@ -3226,7 +3226,7 @@
    12.4  lemma lenlex_conv:
    12.5      "lenlex r = {(xs,ys). length xs < length ys |
    12.6                   length xs = length ys \<and> (xs, ys) : lex r}"
    12.7 -by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
    12.8 +by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
    12.9  
   12.10  lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
   12.11  by (simp add: lex_conv)
   12.12 @@ -3392,8 +3392,8 @@
   12.13  apply (erule listrel.induct, auto) 
   12.14  done
   12.15  
   12.16 -lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
   12.17 -apply (simp add: refl_def listrel_subset Ball_def)
   12.18 +lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
   12.19 +apply (simp add: refl_on_def listrel_subset Ball_def)
   12.20  apply (rule allI) 
   12.21  apply (induct_tac x) 
   12.22  apply (auto intro: listrel.intros)
   12.23 @@ -3414,7 +3414,7 @@
   12.24  done
   12.25  
   12.26  theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
   12.27 -by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
   12.28 +by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
   12.29  
   12.30  lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
   12.31  by (blast intro: listrel.intros)
    13.1 --- a/src/HOL/MetisExamples/Tarski.thy	Mon Mar 02 08:26:03 2009 +0100
    13.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Mon Mar 02 16:53:55 2009 +0100
    13.3 @@ -61,7 +61,7 @@
    13.4    "Top po == greatest (%x. True) po"
    13.5  
    13.6    PartialOrder :: "('a potype) set"
    13.7 -  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
    13.8 +  "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
    13.9                         trans (order P)}"
   13.10  
   13.11    CompleteLattice :: "('a potype) set"
   13.12 @@ -126,7 +126,7 @@
   13.13  
   13.14  subsection {* Partial Order *}
   13.15  
   13.16 -lemma (in PO) PO_imp_refl: "refl A r"
   13.17 +lemma (in PO) PO_imp_refl_on: "refl_on A r"
   13.18  apply (insert cl_po)
   13.19  apply (simp add: PartialOrder_def A_def r_def)
   13.20  done
   13.21 @@ -143,7 +143,7 @@
   13.22  
   13.23  lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
   13.24  apply (insert cl_po)
   13.25 -apply (simp add: PartialOrder_def refl_def A_def r_def)
   13.26 +apply (simp add: PartialOrder_def refl_on_def A_def r_def)
   13.27  done
   13.28  
   13.29  lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
   13.30 @@ -166,7 +166,7 @@
   13.31  apply (simp (no_asm) add: PartialOrder_def)
   13.32  apply auto
   13.33  -- {* refl *}
   13.34 -apply (simp add: refl_def induced_def)
   13.35 +apply (simp add: refl_on_def induced_def)
   13.36  apply (blast intro: reflE)
   13.37  -- {* antisym *}
   13.38  apply (simp add: antisym_def induced_def)
   13.39 @@ -203,7 +203,7 @@
   13.40  
   13.41  lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
   13.42  apply (insert cl_po)
   13.43 -apply (simp add: PartialOrder_def dual_def refl_converse
   13.44 +apply (simp add: PartialOrder_def dual_def refl_on_converse
   13.45                   trans_converse antisym_converse)
   13.46  done
   13.47  
   13.48 @@ -230,12 +230,12 @@
   13.49  
   13.50  lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
   13.51  
   13.52 -declare PO.PO_imp_refl  [OF PO.intro [OF CL_imp_PO], simp]
   13.53 +declare PO.PO_imp_refl_on  [OF PO.intro [OF CL_imp_PO], simp]
   13.54  declare PO.PO_imp_sym   [OF PO.intro [OF CL_imp_PO], simp]
   13.55  declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp]
   13.56  
   13.57 -lemma (in CL) CO_refl: "refl A r"
   13.58 -by (rule PO_imp_refl)
   13.59 +lemma (in CL) CO_refl_on: "refl_on A r"
   13.60 +by (rule PO_imp_refl_on)
   13.61  
   13.62  lemma (in CL) CO_antisym: "antisym r"
   13.63  by (rule PO_imp_sym)
   13.64 @@ -501,10 +501,10 @@
   13.65  apply (rule conjI)
   13.66  ML_command{*AtpWrapper.problem_name:="Tarski__CLF_flubH_le_lubH_simpler"*}
   13.67  (*??no longer terminates, with combinators
   13.68 -apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
   13.69 +apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2) 
   13.70  *)
   13.71 -apply (metis CO_refl lubH_le_flubH monotoneE [OF monotone_f] reflD1 reflD2)
   13.72 -apply (metis CO_refl lubH_le_flubH reflD2)
   13.73 +apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2)
   13.74 +apply (metis CO_refl_on lubH_le_flubH refl_onD2)
   13.75  done
   13.76    declare CLF.f_in_funcset[rule del] funcset_mem[rule del] 
   13.77            CL.lub_in_lattice[rule del] PO.monotoneE[rule del] 
   13.78 @@ -542,12 +542,12 @@
   13.79    by (metis 5 3)
   13.80  have 7: "(lub H cl, lub H cl) \<in> r"
   13.81    by (metis 6 4)
   13.82 -have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl X1 r"
   13.83 -  by (metis 7 reflD2)
   13.84 -have 9: "\<not> refl A r"
   13.85 +have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r"
   13.86 +  by (metis 7 refl_onD2)
   13.87 +have 9: "\<not> refl_on A r"
   13.88    by (metis 8 2)
   13.89  show "False"
   13.90 -  by (metis CO_refl 9);
   13.91 +  by (metis CO_refl_on 9);
   13.92  next --{*apparently the way to insert a second structured proof*}
   13.93    show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
   13.94    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"
   13.95 @@ -589,13 +589,13 @@
   13.96  apply (simp add: fix_def)
   13.97  apply (rule conjI)
   13.98  ML_command{*AtpWrapper.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*} 
   13.99 -apply (metis CO_refl lubH_le_flubH reflD1)
  13.100 +apply (metis CO_refl_on lubH_le_flubH refl_onD1)
  13.101  apply (metis antisymE flubH_le_lubH lubH_le_flubH)
  13.102  done
  13.103  
  13.104  lemma (in CLF) fix_in_H:
  13.105       "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
  13.106 -by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl
  13.107 +by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on
  13.108                      fix_subset [of f A, THEN subsetD])
  13.109  
  13.110  
  13.111 @@ -678,16 +678,16 @@
  13.112  
  13.113  
  13.114  ML{*AtpWrapper.problem_name:="Tarski__rel_imp_elem"*}
  13.115 -  declare (in CLF) CO_refl[simp] refl_def [simp]
  13.116 +  declare (in CLF) CO_refl_on[simp] refl_on_def [simp]
  13.117  lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
  13.118 -by (metis CO_refl reflD1)
  13.119 -  declare (in CLF) CO_refl[simp del]  refl_def [simp del]
  13.120 +by (metis CO_refl_on refl_onD1)
  13.121 +  declare (in CLF) CO_refl_on[simp del]  refl_on_def [simp del]
  13.122  
  13.123  ML{*AtpWrapper.problem_name:="Tarski__interval_subset"*}
  13.124    declare (in CLF) rel_imp_elem[intro] 
  13.125    declare interval_def [simp]
  13.126  lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
  13.127 -by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_eq)
  13.128 +by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
  13.129    declare (in CLF) rel_imp_elem[rule del] 
  13.130    declare interval_def [simp del]
  13.131  
    14.1 --- a/src/HOL/NSA/StarDef.thy	Mon Mar 02 08:26:03 2009 +0100
    14.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Mar 02 16:53:55 2009 +0100
    14.3 @@ -64,7 +64,7 @@
    14.4  
    14.5  lemma equiv_starrel: "equiv UNIV starrel"
    14.6  proof (rule equiv.intro)
    14.7 -  show "reflexive starrel" by (simp add: refl_def)
    14.8 +  show "refl starrel" by (simp add: refl_on_def)
    14.9    show "sym starrel" by (simp add: sym_def eq_commute)
   14.10    show "trans starrel" by (auto intro: transI elim!: ultra)
   14.11  qed
    15.1 --- a/src/HOL/Rational.thy	Mon Mar 02 08:26:03 2009 +0100
    15.2 +++ b/src/HOL/Rational.thy	Mon Mar 02 16:53:55 2009 +0100
    15.3 @@ -21,8 +21,8 @@
    15.4    "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
    15.5    by (simp add: ratrel_def)
    15.6  
    15.7 -lemma refl_ratrel: "refl {x. snd x \<noteq> 0} ratrel"
    15.8 -  by (auto simp add: refl_def ratrel_def)
    15.9 +lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
   15.10 +  by (auto simp add: refl_on_def ratrel_def)
   15.11  
   15.12  lemma sym_ratrel: "sym ratrel"
   15.13    by (simp add: ratrel_def sym_def)
   15.14 @@ -44,7 +44,7 @@
   15.15  qed
   15.16    
   15.17  lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
   15.18 -  by (rule equiv.intro [OF refl_ratrel sym_ratrel trans_ratrel])
   15.19 +  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
   15.20  
   15.21  lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
   15.22  lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
    16.1 --- a/src/HOL/RealDef.thy	Mon Mar 02 08:26:03 2009 +0100
    16.2 +++ b/src/HOL/RealDef.thy	Mon Mar 02 16:53:55 2009 +0100
    16.3 @@ -94,7 +94,7 @@
    16.4  by (simp add: realrel_def)
    16.5  
    16.6  lemma equiv_realrel: "equiv UNIV realrel"
    16.7 -apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def)
    16.8 +apply (auto simp add: equiv_def refl_on_def sym_def trans_def realrel_def)
    16.9  apply (blast dest: preal_trans_lemma) 
   16.10  done
   16.11  
    17.1 --- a/src/HOL/Relation.thy	Mon Mar 02 08:26:03 2009 +0100
    17.2 +++ b/src/HOL/Relation.thy	Mon Mar 02 16:53:55 2009 +0100
    17.3 @@ -34,8 +34,8 @@
    17.4    "Id == {p. EX x. p = (x,x)}"
    17.5  
    17.6  definition
    17.7 -  diag  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
    17.8 -  "diag A == \<Union>x\<in>A. {(x,x)}"
    17.9 +  Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
   17.10 +  "Id_on A == \<Union>x\<in>A. {(x,x)}"
   17.11  
   17.12  definition
   17.13    Domain :: "('a * 'b) set => 'a set" where
   17.14 @@ -50,12 +50,12 @@
   17.15    "Field r == Domain r \<union> Range r"
   17.16  
   17.17  definition
   17.18 -  refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
   17.19 -  "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
   17.20 +  refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
   17.21 +  "refl_on A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
   17.22  
   17.23  abbreviation
   17.24 -  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
   17.25 -  "reflexive == refl UNIV"
   17.26 +  refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
   17.27 +  "refl == refl_on UNIV"
   17.28  
   17.29  definition
   17.30    sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
   17.31 @@ -99,8 +99,8 @@
   17.32  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
   17.33  by (unfold Id_def) blast
   17.34  
   17.35 -lemma reflexive_Id: "reflexive Id"
   17.36 -by (simp add: refl_def)
   17.37 +lemma refl_Id: "refl Id"
   17.38 +by (simp add: refl_on_def)
   17.39  
   17.40  lemma antisym_Id: "antisym Id"
   17.41    -- {* A strange result, since @{text Id} is also symmetric. *}
   17.42 @@ -115,24 +115,24 @@
   17.43  
   17.44  subsection {* Diagonal: identity over a set *}
   17.45  
   17.46 -lemma diag_empty [simp]: "diag {} = {}"
   17.47 -by (simp add: diag_def) 
   17.48 +lemma Id_on_empty [simp]: "Id_on {} = {}"
   17.49 +by (simp add: Id_on_def) 
   17.50  
   17.51 -lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
   17.52 -by (simp add: diag_def)
   17.53 +lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
   17.54 +by (simp add: Id_on_def)
   17.55  
   17.56 -lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
   17.57 -by (rule diag_eqI) (rule refl)
   17.58 +lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
   17.59 +by (rule Id_on_eqI) (rule refl)
   17.60  
   17.61 -lemma diagE [elim!]:
   17.62 -  "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   17.63 +lemma Id_onE [elim!]:
   17.64 +  "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   17.65    -- {* The general elimination rule. *}
   17.66 -by (unfold diag_def) (iprover elim!: UN_E singletonE)
   17.67 +by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
   17.68  
   17.69 -lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
   17.70 +lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
   17.71  by blast
   17.72  
   17.73 -lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
   17.74 +lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
   17.75  by blast
   17.76  
   17.77  
   17.78 @@ -184,37 +184,37 @@
   17.79  
   17.80  subsection {* Reflexivity *}
   17.81  
   17.82 -lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   17.83 -by (unfold refl_def) (iprover intro!: ballI)
   17.84 +lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
   17.85 +by (unfold refl_on_def) (iprover intro!: ballI)
   17.86  
   17.87 -lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   17.88 -by (unfold refl_def) blast
   17.89 +lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
   17.90 +by (unfold refl_on_def) blast
   17.91  
   17.92 -lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
   17.93 -by (unfold refl_def) blast
   17.94 +lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
   17.95 +by (unfold refl_on_def) blast
   17.96  
   17.97 -lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
   17.98 -by (unfold refl_def) blast
   17.99 +lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
  17.100 +by (unfold refl_on_def) blast
  17.101  
  17.102 -lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
  17.103 -by (unfold refl_def) blast
  17.104 +lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
  17.105 +by (unfold refl_on_def) blast
  17.106  
  17.107 -lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
  17.108 -by (unfold refl_def) blast
  17.109 +lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
  17.110 +by (unfold refl_on_def) blast
  17.111  
  17.112 -lemma refl_INTER:
  17.113 -  "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
  17.114 -by (unfold refl_def) fast
  17.115 +lemma refl_on_INTER:
  17.116 +  "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
  17.117 +by (unfold refl_on_def) fast
  17.118  
  17.119 -lemma refl_UNION:
  17.120 -  "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
  17.121 -by (unfold refl_def) blast
  17.122 +lemma refl_on_UNION:
  17.123 +  "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
  17.124 +by (unfold refl_on_def) blast
  17.125  
  17.126 -lemma refl_empty[simp]: "refl {} {}"
  17.127 -by(simp add:refl_def)
  17.128 +lemma refl_on_empty[simp]: "refl_on {} {}"
  17.129 +by(simp add:refl_on_def)
  17.130  
  17.131 -lemma refl_diag: "refl A (diag A)"
  17.132 -by (rule reflI [OF diag_subset_Times diagI])
  17.133 +lemma refl_on_Id_on: "refl_on A (Id_on A)"
  17.134 +by (rule refl_onI [OF Id_on_subset_Times Id_onI])
  17.135  
  17.136  
  17.137  subsection {* Antisymmetry *}
  17.138 @@ -232,7 +232,7 @@
  17.139  lemma antisym_empty [simp]: "antisym {}"
  17.140  by (unfold antisym_def) blast
  17.141  
  17.142 -lemma antisym_diag [simp]: "antisym (diag A)"
  17.143 +lemma antisym_Id_on [simp]: "antisym (Id_on A)"
  17.144  by (unfold antisym_def) blast
  17.145  
  17.146  
  17.147 @@ -256,7 +256,7 @@
  17.148  lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
  17.149  by (fast intro: symI dest: symD)
  17.150  
  17.151 -lemma sym_diag [simp]: "sym (diag A)"
  17.152 +lemma sym_Id_on [simp]: "sym (Id_on A)"
  17.153  by (rule symI) clarify
  17.154  
  17.155  
  17.156 @@ -275,7 +275,7 @@
  17.157  lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
  17.158  by (fast intro: transI elim: transD)
  17.159  
  17.160 -lemma trans_diag [simp]: "trans (diag A)"
  17.161 +lemma trans_Id_on [simp]: "trans (Id_on A)"
  17.162  by (fast intro: transI elim: transD)
  17.163  
  17.164  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
  17.165 @@ -331,11 +331,11 @@
  17.166  lemma converse_Id [simp]: "Id^-1 = Id"
  17.167  by blast
  17.168  
  17.169 -lemma converse_diag [simp]: "(diag A)^-1 = diag A"
  17.170 +lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A"
  17.171  by blast
  17.172  
  17.173 -lemma refl_converse [simp]: "refl A (converse r) = refl A r"
  17.174 -by (unfold refl_def) auto
  17.175 +lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
  17.176 +by (unfold refl_on_def) auto
  17.177  
  17.178  lemma sym_converse [simp]: "sym (converse r) = sym r"
  17.179  by (unfold sym_def) blast
  17.180 @@ -382,7 +382,7 @@
  17.181  lemma Domain_Id [simp]: "Domain Id = UNIV"
  17.182  by blast
  17.183  
  17.184 -lemma Domain_diag [simp]: "Domain (diag A) = A"
  17.185 +lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
  17.186  by blast
  17.187  
  17.188  lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
  17.189 @@ -433,7 +433,7 @@
  17.190  lemma Range_Id [simp]: "Range Id = UNIV"
  17.191  by blast
  17.192  
  17.193 -lemma Range_diag [simp]: "Range (diag A) = A"
  17.194 +lemma Range_Id_on [simp]: "Range (Id_on A) = A"
  17.195  by auto
  17.196  
  17.197  lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
  17.198 @@ -506,7 +506,7 @@
  17.199  lemma Image_Id [simp]: "Id `` A = A"
  17.200  by blast
  17.201  
  17.202 -lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
  17.203 +lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B"
  17.204  by blast
  17.205  
  17.206  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
  17.207 @@ -571,7 +571,7 @@
  17.208  lemma single_valued_Id [simp]: "single_valued Id"
  17.209  by (unfold single_valued_def) blast
  17.210  
  17.211 -lemma single_valued_diag [simp]: "single_valued (diag A)"
  17.212 +lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
  17.213  by (unfold single_valued_def) blast
  17.214  
  17.215  
    18.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 02 08:26:03 2009 +0100
    18.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 02 16:53:55 2009 +0100
    18.3 @@ -64,8 +64,8 @@
    18.4  
    18.5  subsection {* Reflexive closure *}
    18.6  
    18.7 -lemma reflexive_reflcl[simp]: "reflexive(r^=)"
    18.8 -by(simp add:refl_def)
    18.9 +lemma refl_reflcl[simp]: "refl(r^=)"
   18.10 +by(simp add:refl_on_def)
   18.11  
   18.12  lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
   18.13  by(simp add:antisym_def)
   18.14 @@ -118,8 +118,8 @@
   18.15    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   18.16                   consumes 1, case_names refl step]
   18.17  
   18.18 -lemma reflexive_rtrancl: "reflexive (r^*)"
   18.19 -  by (unfold refl_def) fast
   18.20 +lemma refl_rtrancl: "refl (r^*)"
   18.21 +by (unfold refl_on_def) fast
   18.22  
   18.23  text {* Transitivity of transitive closure. *}
   18.24  lemma trans_rtrancl: "trans (r^*)"
    19.1 --- a/src/HOL/UNITY/ListOrder.thy	Mon Mar 02 08:26:03 2009 +0100
    19.2 +++ b/src/HOL/UNITY/ListOrder.thy	Mon Mar 02 16:53:55 2009 +0100
    19.3 @@ -90,16 +90,15 @@
    19.4  
    19.5  subsection{*genPrefix is a partial order*}
    19.6  
    19.7 -lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"
    19.8 -
    19.9 -apply (unfold refl_def, auto)
   19.10 +lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
   19.11 +apply (unfold refl_on_def, auto)
   19.12  apply (induct_tac "x")
   19.13  prefer 2 apply (blast intro: genPrefix.prepend)
   19.14  apply (blast intro: genPrefix.Nil)
   19.15  done
   19.16  
   19.17 -lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
   19.18 -by (erule reflD [OF refl_genPrefix UNIV_I])
   19.19 +lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r"
   19.20 +by (erule refl_onD [OF refl_genPrefix UNIV_I])
   19.21  
   19.22  lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
   19.23  apply clarify
   19.24 @@ -178,8 +177,8 @@
   19.25  done
   19.26  
   19.27  lemma same_genPrefix_genPrefix [simp]: 
   19.28 -    "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
   19.29 -apply (unfold refl_def)
   19.30 +    "refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
   19.31 +apply (unfold refl_on_def)
   19.32  apply (induct_tac "xs")
   19.33  apply (simp_all (no_asm_simp))
   19.34  done
   19.35 @@ -190,7 +189,7 @@
   19.36  by (case_tac "xs", auto)
   19.37  
   19.38  lemma genPrefix_take_append:
   19.39 -     "[| reflexive r;  (xs,ys) : genPrefix r |]  
   19.40 +     "[| refl r;  (xs,ys) : genPrefix r |]  
   19.41        ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
   19.42  apply (erule genPrefix.induct)
   19.43  apply (frule_tac [3] genPrefix_length_le)
   19.44 @@ -198,7 +197,7 @@
   19.45  done
   19.46  
   19.47  lemma genPrefix_append_both:
   19.48 -     "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
   19.49 +     "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
   19.50        ==>  (xs@zs, ys @ zs) : genPrefix r"
   19.51  apply (drule genPrefix_take_append, assumption)
   19.52  apply (simp add: take_all)
   19.53 @@ -210,7 +209,7 @@
   19.54  by auto
   19.55  
   19.56  lemma aolemma:
   19.57 -     "[| (xs,ys) : genPrefix r;  reflexive r |]  
   19.58 +     "[| (xs,ys) : genPrefix r;  refl r |]  
   19.59        ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
   19.60  apply (erule genPrefix.induct)
   19.61    apply blast
   19.62 @@ -225,7 +224,7 @@
   19.63  done
   19.64  
   19.65  lemma append_one_genPrefix:
   19.66 -     "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |]  
   19.67 +     "[| (xs,ys) : genPrefix r;  length xs < length ys;  refl r |]  
   19.68        ==> (xs @ [ys ! length xs], ys) : genPrefix r"
   19.69  by (blast intro: aolemma [THEN mp])
   19.70  
   19.71 @@ -259,7 +258,7 @@
   19.72  
   19.73  subsection{*The type of lists is partially ordered*}
   19.74  
   19.75 -declare reflexive_Id [iff] 
   19.76 +declare refl_Id [iff] 
   19.77          antisym_Id [iff] 
   19.78          trans_Id [iff]
   19.79  
   19.80 @@ -383,8 +382,8 @@
   19.81  
   19.82  (** pfixLe **)
   19.83  
   19.84 -lemma reflexive_Le [iff]: "reflexive Le"
   19.85 -by (unfold refl_def Le_def, auto)
   19.86 +lemma refl_Le [iff]: "refl Le"
   19.87 +by (unfold refl_on_def Le_def, auto)
   19.88  
   19.89  lemma antisym_Le [iff]: "antisym Le"
   19.90  by (unfold antisym_def Le_def, auto)
   19.91 @@ -406,8 +405,8 @@
   19.92  apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
   19.93  done
   19.94  
   19.95 -lemma reflexive_Ge [iff]: "reflexive Ge"
   19.96 -by (unfold refl_def Ge_def, auto)
   19.97 +lemma refl_Ge [iff]: "refl Ge"
   19.98 +by (unfold refl_on_def Ge_def, auto)
   19.99  
  19.100  lemma antisym_Ge [iff]: "antisym Ge"
  19.101  by (unfold antisym_def Ge_def, auto)
    20.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 08:26:03 2009 +0100
    20.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 16:53:55 2009 +0100
    20.3 @@ -344,8 +344,8 @@
    20.4  apply (blast intro: clD cl_in_lattice)
    20.5  done
    20.6  
    20.7 -lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
    20.8 -by (simp add: reflI relcl_def subset_cl [THEN subsetD])
    20.9 +lemma refl_relcl: "lattice L ==> refl (relcl L)"
   20.10 +by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
   20.11  
   20.12  lemma trans_relcl: "lattice L ==> trans (relcl L)"
   20.13  by (blast intro: relcl_trans transI)
   20.14 @@ -362,12 +362,12 @@
   20.15  
   20.16  text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
   20.17  lemma cl_latticeof:
   20.18 -     "[|refl UNIV r; trans r|] 
   20.19 +     "[|refl r; trans r|] 
   20.20        ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
   20.21  apply (rule equalityI) 
   20.22   apply (rule cl_least) 
   20.23    apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
   20.24 - apply (simp add: latticeof_def refl_def, blast)
   20.25 + apply (simp add: latticeof_def refl_on_def, blast)
   20.26  apply (simp add: latticeof_def, clarify)
   20.27  apply (unfold cl_def, blast) 
   20.28  done
   20.29 @@ -400,7 +400,7 @@
   20.30  done
   20.31  
   20.32  theorem relcl_latticeof_eq:
   20.33 -     "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
   20.34 +     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
   20.35  by (simp add: relcl_def cl_latticeof)
   20.36  
   20.37  
    21.1 --- a/src/HOL/UNITY/UNITY.thy	Mon Mar 02 08:26:03 2009 +0100
    21.2 +++ b/src/HOL/UNITY/UNITY.thy	Mon Mar 02 16:53:55 2009 +0100
    21.3 @@ -359,7 +359,7 @@
    21.4  
    21.5  constdefs
    21.6    totalize_act :: "('a * 'a)set => ('a * 'a)set"
    21.7 -    "totalize_act act == act \<union> diag (-(Domain act))"
    21.8 +    "totalize_act act == act \<union> Id_on (-(Domain act))"
    21.9  
   21.10    totalize :: "'a program => 'a program"
   21.11      "totalize F == mk_program (Init F,
    22.1 --- a/src/HOL/Word/Num_Lemmas.thy	Mon Mar 02 08:26:03 2009 +0100
    22.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Mon Mar 02 16:53:55 2009 +0100
    22.3 @@ -260,7 +260,7 @@
    22.4  
    22.5  (** Rep_Integ **)
    22.6  lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
    22.7 -  unfolding equiv_def refl_def quotient_def Image_def by auto
    22.8 +  unfolding equiv_def refl_on_def quotient_def Image_def by auto
    22.9  
   22.10  lemmas Rep_Integ_ne = Integ.Rep_Integ 
   22.11    [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
    23.1 --- a/src/HOL/ZF/Games.thy	Mon Mar 02 08:26:03 2009 +0100
    23.2 +++ b/src/HOL/ZF/Games.thy	Mon Mar 02 16:53:55 2009 +0100
    23.3 @@ -847,7 +847,7 @@
    23.4    by (auto simp add: quotient_def)
    23.5  
    23.6  lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
    23.7 -  by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
    23.8 +  by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
    23.9      eq_game_sym intro: eq_game_refl eq_game_trans)
   23.10  
   23.11  instantiation Pg :: "{ord, zero, plus, minus, uminus}"
    24.1 --- a/src/HOL/ex/Tarski.thy	Mon Mar 02 08:26:03 2009 +0100
    24.2 +++ b/src/HOL/ex/Tarski.thy	Mon Mar 02 16:53:55 2009 +0100
    24.3 @@ -73,7 +73,7 @@
    24.4  
    24.5  definition
    24.6    PartialOrder :: "('a potype) set" where
    24.7 -  "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) &
    24.8 +  "PartialOrder = {P. refl_on (pset P) (order P) & antisym (order P) &
    24.9                         trans (order P)}"
   24.10  
   24.11  definition
   24.12 @@ -158,7 +158,7 @@
   24.13  unfolding PartialOrder_def dual_def
   24.14  by auto
   24.15  
   24.16 -lemma (in PO) PO_imp_refl [simp]: "refl A r"
   24.17 +lemma (in PO) PO_imp_refl_on [simp]: "refl_on A r"
   24.18  apply (insert cl_po)
   24.19  apply (simp add: PartialOrder_def A_def r_def)
   24.20  done
   24.21 @@ -175,7 +175,7 @@
   24.22  
   24.23  lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
   24.24  apply (insert cl_po)
   24.25 -apply (simp add: PartialOrder_def refl_def A_def r_def)
   24.26 +apply (simp add: PartialOrder_def refl_on_def A_def r_def)
   24.27  done
   24.28  
   24.29  lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
   24.30 @@ -198,7 +198,7 @@
   24.31  apply (simp (no_asm) add: PartialOrder_def)
   24.32  apply auto
   24.33  -- {* refl *}
   24.34 -apply (simp add: refl_def induced_def)
   24.35 +apply (simp add: refl_on_def induced_def)
   24.36  apply (blast intro: reflE)
   24.37  -- {* antisym *}
   24.38  apply (simp add: antisym_def induced_def)
   24.39 @@ -235,7 +235,7 @@
   24.40  
   24.41  lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
   24.42  apply (insert cl_po)
   24.43 -apply (simp add: PartialOrder_def dual_def refl_converse
   24.44 +apply (simp add: PartialOrder_def dual_def refl_on_converse
   24.45                   trans_converse antisym_converse)
   24.46  done
   24.47  
   24.48 @@ -266,8 +266,8 @@
   24.49  declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
   24.50  declare CL_imp_PO [THEN PO.PO_imp_trans, simp]*)
   24.51  
   24.52 -lemma (in CL) CO_refl: "refl A r"
   24.53 -by (rule PO_imp_refl)
   24.54 +lemma (in CL) CO_refl_on: "refl_on A r"
   24.55 +by (rule PO_imp_refl_on)
   24.56  
   24.57  lemma (in CL) CO_antisym: "antisym r"
   24.58  by (rule PO_imp_sym)
   24.59 @@ -533,7 +533,7 @@
   24.60  
   24.61  lemma (in CLF) fix_in_H:
   24.62       "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
   24.63 -by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl
   24.64 +by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on
   24.65                      fix_subset [of f A, THEN subsetD])
   24.66  
   24.67  lemma (in CLF) fixf_le_lubH:
   24.68 @@ -583,8 +583,8 @@
   24.69  subsection {* interval *}
   24.70  
   24.71  lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
   24.72 -apply (insert CO_refl)
   24.73 -apply (simp add: refl_def, blast)
   24.74 +apply (insert CO_refl_on)
   24.75 +apply (simp add: refl_on_def, blast)
   24.76  done
   24.77  
   24.78  lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
   24.79 @@ -754,7 +754,7 @@
   24.80  apply (rule notI)
   24.81  apply (drule_tac a = "Top cl" in equals0D)
   24.82  apply (simp add: interval_def)
   24.83 -apply (simp add: refl_def Top_in_lattice Top_prop)
   24.84 +apply (simp add: refl_on_def Top_in_lattice Top_prop)
   24.85  done
   24.86  
   24.87  lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}"