--- a/NEWS Sat Mar 15 14:39:45 2025 +0100
+++ b/NEWS Sat Mar 15 19:40:10 2025 +0100
@@ -16,10 +16,12 @@
monotone_on_inf_fun
monotone_on_sup_fun
-* Theory "HOL.Relations":
+* Theory "HOL.Relation":
- Changed definition of predicate refl_on to not constrain the domain
and range of the relation. To get the old semantics, explicitely use
the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
+ - Removed predicate single_valuedp. Use predicate right_unique instead.
+ INCOMPATIBILITY.
- Strengthened lemmas. Minor INCOMPATIBILITY.
refl_on_empty[simp]
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
@@ -53,7 +55,7 @@
quotient_disj_strong
* Theory "HOL.Transfer":
- - Moved right_unique from HOL.Transfer to HOL.Relations.
+ - Moved right_unique from HOL.Transfer to HOL.Relation.
Minor INCOMPATIBILITY.
- Added lemmas.
single_valuedp_eq_right_unique
--- a/src/HOL/Relation.thy Sat Mar 15 14:39:45 2025 +0100
+++ b/src/HOL/Relation.thy Sat Mar 15 19:40:10 2025 +0100
@@ -829,31 +829,21 @@
definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
-definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
-
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
"right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
-lemma single_valuedp_eq_right_unique: "single_valuedp = right_unique"
- by (rule ext) (simp add: single_valuedp_def right_unique_def)
+lemma right_unique_single_valued_eq [pred_set_conv]:
+ "right_unique (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
+ by (simp add: single_valued_def right_unique_def)
-lemma single_valuedp_single_valued_eq [pred_set_conv]:
- "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
- by (simp add: single_valued_def single_valuedp_def)
-
-lemma single_valuedp_iff_Uniq:
- "single_valuedp r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)"
- unfolding Uniq_def single_valuedp_def by auto
+lemma right_unique_iff_Uniq:
+ "right_unique r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)"
+ unfolding Uniq_def right_unique_def by auto
lemma single_valuedI:
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
unfolding single_valued_def by blast
-lemma single_valuedpI:
- "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
- by (fact single_valuedI [to_pred])
-
lemma right_uniqueI: "(\<And>x y z. R x y \<Longrightarrow> R x z \<Longrightarrow> y = z) \<Longrightarrow> right_unique R"
unfolding right_unique_def by fast
@@ -861,10 +851,6 @@
"single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
by (simp add: single_valued_def)
-lemma single_valuedpD:
- "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
- by (fact single_valuedD [to_pred])
-
lemma right_uniqueD: "right_unique R \<Longrightarrow> R x y \<Longrightarrow> R x z \<Longrightarrow> y = z"
unfolding right_unique_def by fast
@@ -872,16 +858,14 @@
"single_valued {}"
by (simp add: single_valued_def)
-lemma single_valuedp_bot [simp]:
- "single_valuedp \<bottom>"
- by (fact single_valued_empty [to_pred])
+lemma right_unique_bot[simp]: "right_unique \<bottom>"
+ by (fact single_valued_empty[to_pred])
lemma single_valued_subset:
"r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
unfolding single_valued_def by blast
-lemma single_valuedp_less_eq:
- "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r"
+lemma right_unique_less_eq: "r \<le> s \<Longrightarrow> right_unique s \<Longrightarrow> right_unique r"
by (fact single_valued_subset [to_pred])