# HG changeset patch
# User desharna
# Date 1671182032 -3600
# Node ID 99d6e9217586d2351bf97aa82b83bb5f13fb60f2
# Parent  f8826fc8c4191cafa8cc8100596bddba7bafc62e
added predicates sym_on and symp_on and redefined sym and symp to be abbreviations

diff -r f8826fc8c419 -r 99d6e9217586 NEWS
--- a/NEWS	Fri Dec 16 09:55:22 2022 +0100
+++ b/NEWS	Fri Dec 16 10:13:52 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
diff -r f8826fc8c419 -r 99d6e9217586 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:13:52 2022 +0100
@@ -361,11 +361,25 @@
 
 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)
diff -r f8826fc8c419 -r 99d6e9217586 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Dec 16 10:13:52 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];