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 multpHO_plus_plus[simp]
authordesharna
Fri, 27 Jan 2023 12:25:36 +0100
changeset 77104 9678b533119e
parent 77102 780161d4b55c
child 77105 bbe33afcfe1e
added lemma multpHO_plus_plus[simp]
NEWS file | annotate | diff | comparison | revisions
src/HOL/Library/Multiset_Order.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Thu Jan 26 13:59:51 2023 +0000
+++ b/NEWS	Fri Jan 27 12:25:36 2023 +0100
@@ -215,6 +215,7 @@
 * Theory "HOL-Library.Multiset_Order":
   - Added lemmas.
       irreflp_on_multpHO[simp]
+      multpHO_plus_plus[simp]
       totalp_multpDM
       totalp_multpHO
       totalp_on_multpDM
--- a/src/HOL/Library/Multiset_Order.thy	Thu Jan 26 13:59:51 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Fri Jan 27 12:25:36 2023 +0100
@@ -138,6 +138,9 @@
   using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
   by blast
 
+lemma multp\<^sub>H\<^sub>O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
+  unfolding multp\<^sub>H\<^sub>O_def by simp
+
 
 subsubsection \<open>Properties of Preorders\<close>
isabelle