# HG changeset patch
# User desharna
# Date 1671097906 -3600
# Node ID e322abb912af69f1e80f46e36f6d1acc38f6b284
# Parent  d8ca2d0e81e57cbb4653700fc4a46e4e113a6e37
added lemmas antisym_onI and antisymp_onI

diff -r d8ca2d0e81e5 -r e322abb912af NEWS
--- a/NEWS	Thu Dec 15 09:44:50 2022 +0100
+++ b/NEWS	Thu Dec 15 10:51:46 2022 +0100
@@ -41,7 +41,9 @@
       total_on_singleton
   - Added lemmas.
       antisym_if_asymp
+      antisym_onI
       antisymp_if_asymp
+      antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
       asym_if_irrefl_and_trans
       asymp_if_irreflp_and_transp
diff -r d8ca2d0e81e5 -r e322abb912af src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Dec 15 09:44:50 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 15 10:51:46 2022 +0100
@@ -449,13 +449,21 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV]
 
+lemma antisym_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym_on A r"
+  unfolding antisym_on_def by simp
+
 lemma antisymI [intro?]:
   "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
-  unfolding antisym_def by iprover
+  by (simp add: antisym_onI)
+
+lemma antisymp_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp_on A R"
+  by (rule antisym_onI[to_pred])
 
 lemma antisympI [intro?]:
-  "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r"
-  by (fact antisymI [to_pred])
+  "(\<And>x y. R x y \<Longrightarrow> R y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp R"
+  by (rule antisymI[to_pred])
     
 lemma antisymD [dest?]:
   "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"