# HG changeset patch
# User desharna
# Date 1683701984 -7200
# Node ID db041670d6bbe6464baae019e59a9d35b2697789
# Parent  b0ef3aae2bdba5ec2043b0b42bd96349bd43f32c
added lemmas transp_on_multpHO and transp_multpHO

diff -r b0ef3aae2bdb -r db041670d6bb NEWS
--- a/NEWS	Wed May 10 08:56:32 2023 +0200
+++ b/NEWS	Wed May 10 08:59:44 2023 +0200
@@ -275,6 +275,8 @@
       totalp_multpHO
       totalp_on_multpDM
       totalp_on_multpHO
+      transp_multpHO
+      transp_on_multpHO
 
 * 'primcorec': Made the internal tactic more robust in the face of
   nested corecursion.
diff -r b0ef3aae2bdb -r db041670d6bb src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed May 10 08:56:32 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Wed May 10 08:59:44 2023 +0200
@@ -311,6 +311,146 @@
 
 paragraph \<open>Transitivity\<close>
 
+lemma transp_on_multp\<^sub>H\<^sub>O:
+  assumes "asymp_on A R" and "transp_on A R" and
+    B_sub_A: "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
+  shows "transp_on B (multp\<^sub>H\<^sub>O R)"
+proof (rule transp_onI)
+  from assms have "asymp_on B (multp\<^sub>H\<^sub>O R)"
+    using asymp_on_multp\<^sub>H\<^sub>O by metis
+
+  fix M1 M2 M3
+  assume hyps: "M1 \<in> B" "M2 \<in> B" "M3 \<in> B" "multp\<^sub>H\<^sub>O R M1 M2" "multp\<^sub>H\<^sub>O R M2 M3"
+
+  from assms have
+    [intro]: "asymp_on (set_mset M1 \<union> set_mset M2) R" "transp_on (set_mset M1 \<union> set_mset M2) R"
+    using \<open>M1 \<in> B\<close> \<open>M2 \<in> B\<close>
+    by (simp_all add: asymp_on_subset transp_on_subset)
+
+  from assms have "transp_on (set_mset M1) R"
+    by (meson transp_on_subset hyps(1))
+
+  from \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> have
+    "M1 \<noteq> M2" and
+    "\<forall>y. count M2 y < count M1 y \<longrightarrow> (\<exists>x. R y x \<and> count M1 x < count M2 x)"
+    unfolding multp\<^sub>H\<^sub>O_def by simp_all
+
+  from \<open>multp\<^sub>H\<^sub>O R M2 M3\<close> have
+    "M2 \<noteq> M3" and
+    "\<forall>y. count M3 y < count M2 y \<longrightarrow> (\<exists>x. R y x \<and> count M2 x < count M3 x)"
+    unfolding multp\<^sub>H\<^sub>O_def by simp_all
+
+  show "multp\<^sub>H\<^sub>O R M1 M3"
+  proof (rule ccontr)
+    let ?P = "\<lambda>x. count M3 x < count M1 x \<and> (\<forall>y. R x y \<longrightarrow> count M1 y \<ge> count M3 y)"
+
+    assume "\<not> multp\<^sub>H\<^sub>O R M1 M3"
+    hence "M1 = M3 \<or> (\<exists>x. ?P x)"
+      unfolding multp\<^sub>H\<^sub>O_def by force
+    thus False
+    proof (elim disjE)
+      assume "M1 = M3"
+      thus False
+        using \<open>asymp_on B (multp\<^sub>H\<^sub>O R)\<close>[THEN asymp_onD]
+        using \<open>M2 \<in> B\<close> \<open>M3 \<in> B\<close> \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> \<open>multp\<^sub>H\<^sub>O R M2 M3\<close>
+        by metis
+    next
+      assume "\<exists>x. ?P x"
+      hence "\<exists>x \<in># M1 + M2. ?P x"
+        by (auto simp: count_inI)
+      have "\<exists>y \<in># M1 + M2. ?P y \<and> (\<forall>z \<in># M1 + M2. R y z \<longrightarrow> \<not> ?P z)"
+      proof (rule Finite_Set.bex_max_element_with_property)
+        show "\<exists>x \<in># M1 + M2. ?P x"
+          using \<open>\<exists>x. ?P x\<close>
+          by (auto simp: count_inI)
+      qed auto
+      then obtain x where
+        "x \<in># M1 + M2" and
+        "count M3 x < count M1 x" and
+        "\<forall>y. R x y \<longrightarrow> count M1 y \<ge> count M3 y" and
+        "\<forall>y \<in># M1 + M2. R x y \<longrightarrow> count M3 y < count M1 y \<longrightarrow> (\<exists>z. R y z \<and> count M1 z < count M3 z)"
+        by force
+
+      let ?Q = "\<lambda>x'. R\<^sup>=\<^sup>= x x' \<and> count M3 x' < count M2 x'"
+      show False
+      proof (cases "\<exists>x'. ?Q x'")
+        case True
+        have "\<exists>y \<in># M1 + M2. ?Q y \<and> (\<forall>z \<in># M1 + M2. R y z \<longrightarrow> \<not> ?Q z)"
+        proof (rule Finite_Set.bex_max_element_with_property)
+          show "\<exists>x \<in># M1 + M2. ?Q x"
+            using \<open>\<exists>x. ?Q x\<close>
+            by (auto simp: count_inI)
+        qed auto
+        then obtain x' where
+          "x' \<in># M1 + M2" and
+          "R\<^sup>=\<^sup>= x x'" and
+          "count M3 x' < count M2 x'" and
+          maximality_x': "\<forall>z \<in># M1 + M2. R x' z \<longrightarrow> \<not> (R\<^sup>=\<^sup>= x z) \<or> count M3 z \<ge> count M2 z"
+          by (auto simp: linorder_not_less)
+        with \<open>multp\<^sub>H\<^sub>O R M2 M3\<close> obtain y' where
+          "R x' y'" and "count M2 y' < count M3 y'"
+          unfolding multp\<^sub>H\<^sub>O_def by auto
+        hence "count M2 y' < count M1 y'"
+          by (smt (verit) \<open>R\<^sup>=\<^sup>= x x'\<close> \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close>
+              \<open>count M3 x < count M1 x\<close> \<open>count M3 x' < count M2 x'\<close> assms(2) count_inI
+              dual_order.strict_trans1 hyps(1) hyps(2) hyps(3) less_nat_zero_code B_sub_A subsetD
+              sup2E transp_onD)
+        with \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> obtain y'' where
+          "R y' y''" and "count M1 y'' < count M2 y''"
+          unfolding multp\<^sub>H\<^sub>O_def by auto
+        hence "count M3 y'' < count M2 y''"
+          by (smt (verit, del_insts) \<open>R x' y'\<close> \<open>R\<^sup>=\<^sup>= x x'\<close> \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close>
+              \<open>count M2 y' < count M3 y'\<close> \<open>count M3 x < count M1 x\<close> \<open>count M3 x' < count M2 x'\<close>
+              assms(2) count_greater_zero_iff dual_order.strict_trans1 hyps(1) hyps(2) hyps(3)
+              less_nat_zero_code linorder_not_less B_sub_A subset_iff sup2E transp_onD)
+
+        moreover have "count M2 y'' \<le> count M3 y''"
+        proof -
+          have "y'' \<in># M1 + M2"
+            by (metis \<open>count M1 y'' < count M2 y''\<close> count_inI not_less_iff_gr_or_eq union_iff)
+
+          moreover have "R x' y''"
+            by (metis \<open>R x' y'\<close> \<open>R y' y''\<close> \<open>count M2 y' < count M1 y'\<close>
+                \<open>transp_on (set_mset M1 \<union> set_mset M2) R\<close> \<open>x' \<in># M1 + M2\<close> calculation count_inI
+                nat_neq_iff set_mset_union transp_onD union_iff)
+
+          moreover have "R\<^sup>=\<^sup>= x y''"
+            using \<open>R\<^sup>=\<^sup>= x x'\<close>
+            by (metis (mono_tags, opaque_lifting) \<open>transp_on (set_mset M1 \<union> set_mset M2) R\<close>
+                \<open>x \<in># M1 + M2\<close> \<open>x' \<in># M1 + M2\<close> calculation(1) calculation(2) set_mset_union sup2I1
+                transp_onD transp_on_reflclp)
+
+          ultimately show ?thesis
+            using maximality_x'[rule_format, of y''] by metis
+        qed
+
+        ultimately show ?thesis
+          by linarith
+      next
+        case False
+        hence "\<And>x'. R\<^sup>=\<^sup>= x x' \<Longrightarrow> count M2 x' \<le> count M3 x'"
+          by auto
+        hence "count M2 x \<le> count M3 x"
+          by simp
+        hence "count M2 x < count M1 x"
+          using \<open>count M3 x < count M1 x\<close> by linarith
+        with \<open>multp\<^sub>H\<^sub>O R M1 M2\<close> obtain y where
+          "R x y" and "count M1 y < count M2 y"
+          unfolding multp\<^sub>H\<^sub>O_def by auto
+        hence "count M3 y < count M2 y"
+          using \<open>\<forall>y. R x y \<longrightarrow> count M3 y \<le> count M1 y\<close> dual_order.strict_trans2 by metis
+        then show ?thesis
+          using False \<open>R x y\<close> by auto
+      qed
+    qed
+  qed
+qed
+
+lemma transp_multp\<^sub>H\<^sub>O:
+  assumes "asymp R" and "transp R"
+  shows "transp (multp\<^sub>H\<^sub>O R)"
+  using assms transp_on_multp\<^sub>H\<^sub>O[of UNIV, simplified] by metis
+
 
 paragraph \<open>Totality\<close>