Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma totalp_on_total_on_eq[pred_set_conv]
authordesharna
Sat, 04 Jun 2022 19:11:52 +0200
changeset 75541 a4fa039a6a60
parent 75540 02719bd7b4e6
child 75542 47abacd97f7b
added lemma totalp_on_total_on_eq[pred_set_conv]
NEWS file | annotate | diff | comparison | revisions
src/HOL/Relation.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Sat Jun 04 18:32:30 2022 +0200
+++ b/NEWS	Sat Jun 04 19:11:52 2022 +0200
@@ -66,6 +66,7 @@
       totalp_onI
       totalp_on_empty[simp]
       totalp_on_subset
+      totalp_on_total_on_eq[pred_set_conv]
 
 * Theory "HOL-Library.Multiset":
   - Consolidated operation and fact names.
--- a/src/HOL/Relation.thy	Sat Jun 04 18:32:30 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 19:11:52 2022 +0200
@@ -528,6 +528,9 @@
 abbreviation totalp where
   "totalp \<equiv> totalp_on UNIV"
 
+lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
+  by (simp add: totalp_on_def total_on_def)
+
 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)
isabelle