# HG changeset patch
# User desharna
# Date 1671182631 -3600
# Node ID 9bbc085fce861123be4f1347afd1f68defd21a5c
# Parent  d616622812b2054daa83a9b11d7c68949f08102b
added lemmas sym_onI and symp_onI

diff -r d616622812b2 -r 9bbc085fce86 NEWS
--- a/NEWS	Fri Dec 16 10:18:35 2022 +0100
+++ b/NEWS	Fri Dec 16 10:23:51 2022 +0100
@@ -79,6 +79,8 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      sym_onI
+      symp_onI
       symp_on_sym_on_eq[pred_set_conv]
       totalI
       totalp_on_converse[simp]
diff -r d616622812b2 -r 9bbc085fce86 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 10:18:35 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:23:51 2022 +0100
@@ -386,11 +386,17 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
-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"