# HG changeset patch
# User desharna
# Date 1653661005 -7200
# Node ID 5f2a1efd05602097bca68d46cdd0f694a956a744
# Parent  d9b23902692dd811871ba4c75190eb6627b0a55c
added predicate totalp_on and abbreviation totalp

diff -r d9b23902692d -r 5f2a1efd0560 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)