--- a/NEWS Mon Mar 02 12:34:03 2009 +0000
+++ b/NEWS Mon Mar 02 16:54:13 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
--- a/src/HOL/Algebra/Coset.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Algebra/Coset.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/Algebra/Sylow.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Algebra/Sylow.thy Mon Mar 02 16:54:13 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"
--- a/src/HOL/Equiv_Relations.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Equiv_Relations.thy Mon Mar 02 16:54:13 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
--- a/src/HOL/Induct/LList.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Induct/LList.thy Mon Mar 02 16:54:13 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*}
--- a/src/HOL/Induct/QuoDataType.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Induct/QuoDataType.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/Induct/QuoNestedDataType.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Induct/QuoNestedDataType.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/Int.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Int.thy Mon Mar 02 16:54:13 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)"} *}
--- a/src/HOL/Library/Coinductive_List.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Library/Coinductive_List.thy Mon Mar 02 16:54:13 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
--- a/src/HOL/Library/Order_Relation.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Library/Order_Relation.thy Mon Mar 02 16:54:13 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"
--- a/src/HOL/Library/Zorn.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Library/Zorn.thy Mon Mar 02 16:54:13 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`
--- a/src/HOL/List.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/List.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/MetisExamples/Tarski.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/MetisExamples/Tarski.thy Mon Mar 02 16:54:13 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]
--- a/src/HOL/NSA/StarDef.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/NSA/StarDef.thy Mon Mar 02 16:54:13 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
--- a/src/HOL/Rational.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Rational.thy Mon Mar 02 16:54:13 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]
--- a/src/HOL/RealDef.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/RealDef.thy Mon Mar 02 16:54:13 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
--- a/src/HOL/Relation.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Relation.thy Mon Mar 02 16:54:13 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
--- a/src/HOL/Transitive_Closure.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Transitive_Closure.thy Mon Mar 02 16:54:13 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^*)"
--- a/src/HOL/UNITY/ListOrder.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/UNITY/ListOrder.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/UNITY/ProgressSets.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/UNITY/ProgressSets.thy Mon Mar 02 16:54:13 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)
--- a/src/HOL/UNITY/UNITY.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/UNITY/UNITY.thy Mon Mar 02 16:54:13 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,
--- a/src/HOL/Word/Num_Lemmas.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/Word/Num_Lemmas.thy Mon Mar 02 16:54:13 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]
--- a/src/HOL/ZF/Games.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/ZF/Games.thy Mon Mar 02 16:54:13 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}"
--- a/src/HOL/ex/Tarski.thy Mon Mar 02 12:34:03 2009 +0000
+++ b/src/HOL/ex/Tarski.thy Mon Mar 02 16:54:13 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> {}"