added predicate totalp_on and abbreviation totalp
authordesharna
Fri, 27 May 2022 16:16:45 +0200
changeset 75962 5f2a1efd0560
parent 75961 d9b23902692d
child 75963 006ca44957e4
child 75964 9e34819a7ca1
child 75965 a1c7829ac2de
added predicate totalp_on and abbreviation totalp
src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri May 27 13:46:40 2022 +0200
+++ b/src/HOL/Relation.thy	Fri May 27 16:16:45 2022 +0200
@@ -486,6 +486,26 @@
 
 abbreviation "total \<equiv> total_on UNIV"
 
+definition totalp_on where
+  "totalp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> R x y \<or> R y x)"
+
+abbreviation totalp where
+  "totalp \<equiv> totalp_on UNIV"
+
+lemma totalp_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R"
+  by (simp add: totalp_on_def)
+
+lemma totalpI: "(\<And>x y. x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp R"
+  by (rule totalp_onI)
+
+lemma totalp_onD:
+  "totalp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
+  by (simp add: totalp_on_def)
+
+lemma totalpD: "totalp R \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
+  by (simp add: totalp_onD)
+
 lemma total_on_empty [simp]: "total_on {} r"
   by (simp add: total_on_def)