merged

--- a/NEWS	Fri Dec 16 18:18:57 2022 +0100
+++ b/NEWS	Fri Dec 16 18:19:23 2022 +0100
@@ -30,6 +30,10 @@
     irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
+  - Added predicates sym_on and symp_on and redefined sym and
+    symp to be abbreviations. Lemmas sym_def and symp_def are explicitly
+    provided for backward compatibility but their usage is discouraged.
+    Minor INCOMPATIBILITY.
   - Added predicates antisym_on and antisymp_on and redefined antisym and
     antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
     explicitly provided for backward compatibility but their usage is
@@ -75,6 +79,13 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      sym_onD
+      sym_onI
+      sym_on_subset
+      symp_onD
+      symp_onI
+      symp_on_subset
+      symp_on_sym_on_eq[pred_set_conv]
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]

--- a/src/HOL/Relation.thy	Fri Dec 16 18:18:57 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 18:19:23 2022 +0100
@@ -361,20 +361,48 @@
 
 subsubsection \<open>Symmetry\<close>
 
-definition sym :: "'a rel \<Rightarrow> bool"
-  where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+definition sym_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "sym_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+
+abbreviation sym :: "'a rel \<Rightarrow> bool" where
+  "sym \<equiv> sym_on UNIV"
+
+definition symp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "symp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. R x y \<longrightarrow> R y x)"
 
-definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)"
+abbreviation symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "symp \<equiv> symp_on UNIV"
+
+lemma sym_def[no_atp]: "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
+  by (simp add: sym_on_def)
+
+lemma symp_def[no_atp]: "symp R \<longleftrightarrow> (\<forall>x y. R x y \<longrightarrow> R y x)"
+  by (simp add: symp_on_def)
+
+text \<open>@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\<close>
 
-lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
-  by (simp add: sym_def symp_def)
+lemma symp_on_sym_on_eq[pred_set_conv]: "symp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym_on A r"
+  by (simp add: sym_on_def symp_on_def)
+
+lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
+
+lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
+  by (auto simp: sym_on_def)
+
+lemma symp_on_subset: "symp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> symp_on B R"
+  by (auto simp: symp_on_def)
 
-lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
-  by (unfold sym_def) iprover
+lemma sym_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym_on A r"
+  by (simp add: sym_on_def)
+
+lemma symI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym r"
+  by (simp add: sym_onI)
 
-lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
-  by (fact symI [to_pred])
+lemma symp_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x) \<Longrightarrow> symp_on A R"
+  by (rule sym_onI[to_pred])
+
+lemma sympI [intro?]: "(\<And>x y. R x y \<Longrightarrow> R y x) \<Longrightarrow> symp R"
+  by (rule symI[to_pred])
 
 lemma symE:
   assumes "sym r" and "(b, a) \<in> r"
@@ -386,15 +414,17 @@
   obtains "r a b"
   using assms by (rule symE [to_pred])
 
-lemma symD [dest?]:
-  assumes "sym r" and "(b, a) \<in> r"
-  shows "(a, b) \<in> r"
-  using assms by (rule symE)
+lemma sym_onD: "sym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_on_def)
+
+lemma symD [dest?]: "sym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_onD)
 
-lemma sympD [dest?]:
-  assumes "symp r" and "r b a"
-  shows "r a b"
-  using assms by (rule symD [to_pred])
+lemma symp_onD: "symp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule sym_onD[to_pred])
+
+lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule symD[to_pred])
 
 lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
   by (fast intro: symI elim: symE)

--- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Dec 16 18:18:57 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Dec 16 18:19:23 2022 +0100
@@ -399,7 +399,7 @@
 fun mk_pred name R =
   Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
 val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
-val mk_symp = mk_pred \<^const_name>\<open>symp\<close>;
+val mk_symp = mk_pred \<^const_abbrev>\<open>symp\<close>;
 val mk_transp =  mk_pred \<^const_name>\<open>transp\<close>;
 
 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];