# HG changeset patch
# User haftmann
# Date 1463038447 -7200
# Node ID f2177f5d2aed353de67a495695e79cace526f710
# Parent  be252979cfe50b140459d2787d229f8e6527be08
a quasi-recursive characterization of the multiset order (by Christian Sternagel)

diff -r be252979cfe5 -r f2177f5d2aed src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu May 12 11:34:19 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu May 12 09:34:07 2016 +0200
@@ -2066,6 +2066,117 @@
     \<Longrightarrow> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
+subsection \<open>A quasi-recursive characterization\<close>
+
+text \<open>
+  The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison
+  \<open>(I + B, I + A) \<in> mult r\<close>, can always be made disjoint.
+\<close>
+lemma decreasing_parts_disj:
+  assumes "irrefl r" and "trans r"
+    and "A \<noteq> {#}" and *: "\<forall>b\<in>#B. \<exists>a\<in>#A. (b, a) \<in> r"
+  defines "Z \<equiv> A #\<inter> B"
+  defines "X \<equiv> A - Z"
+  defines "Y \<equiv> B - Z"
+  shows "X \<noteq> {#} \<and> X #\<inter> Y = {#} \<and>
+    A = X + Z \<and> B = Y + Z \<and> (\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r)"
+proof -
+  define D
+    where "D = set_mset A \<union> set_mset B"
+  let ?r = "r \<inter> D \<times> D"
+  have "irrefl ?r" and "trans ?r" and "finite ?r"
+    using \<open>irrefl r\<close> and \<open>trans r\<close> by (auto simp: D_def irrefl_def trans_Restr)
+  note wf_converse_induct = wf_induct [OF wf_converse [OF this]]
+  { fix b assume "b \<in># B"
+    then have "\<exists>x. x \<in># X \<and> (b, x) \<in> r"
+    proof (induction rule: wf_converse_induct)
+      case (1 b)
+      then obtain a where "b \<in># B" and "a \<in># A" and "(b, a) \<in> r"
+        using * by blast
+      then show ?case
+      proof (cases "a \<in># X")
+        case False
+        then have "a \<in># B" using \<open>a \<in># A\<close>
+          by (simp add: X_def Z_def not_in_iff)
+            (metis le_zero_eq not_in_iff)
+        moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>"
+          using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close>
+          by (auto simp: D_def)
+        ultimately obtain x where "x \<in># X" and "(a, x) \<in> r"
+          using "1.IH" by blast
+        moreover then have "(b, x) \<in> r"
+          using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD)
+        ultimately show ?thesis by blast
+      qed blast
+    qed }
+  note B_less = this
+  then have "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r"
+    by (auto simp: Y_def Z_def dest: in_diffD)
+  moreover have "X \<noteq> {#}"
+  proof -
+    obtain a where "a \<in># A" using \<open>A \<noteq> {#}\<close>
+      by (auto simp: multiset_eq_iff)
+    show ?thesis
+    proof (cases "a \<in># X")
+      case False
+      then have "a \<in># B" using \<open>a \<in># A\<close>
+        by (simp add: X_def Z_def not_in_iff)
+          (metis le_zero_eq not_in_iff)
+      then show ?thesis by (auto dest: B_less)
+    qed auto
+  qed
+  moreover have "A = X + Z" and "B = Y + Z" and "X #\<inter> Y = {#}"
+    by (auto simp: X_def Y_def Z_def multiset_eq_iff)
+  ultimately show ?thesis by blast
+qed
+
+text \<open>
+  A predicate variant of the reflexive closure of \<open>mult\<close>, which is
+  executable whenever the given predicate \<open>P\<close> is. Together with the
+  standard code equations for \<open>op #\<inter>\<close> and \<open>op -\<close> this should yield
+  a quadratic (with respect to calls to \<open>P\<close>) implementation of \<open>multeqp\<close>.
+\<close>
+definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multeqp P N M =
+    (let Z = M #\<inter> N; X = M - Z; Y = N - Z in
+    (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
+
+lemma multeqp_iff:
+  assumes "irrefl R" and "trans R"
+    and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
+  shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
+proof
+  assume "(N, M) \<in> (mult R)\<^sup>="
+  then show "multeqp P N M"
+  proof
+    assume "(N, M) \<in> mult R"
+    from mult_implies_one_step [OF \<open>trans R\<close> this] obtain I J K
+      where *: "I \<noteq> {#}" "\<forall>j\<in>#J. \<exists>i\<in>#I. (j, i) \<in> R"
+      and [simp]: "M = K + I" "N = K + J" by blast
+    from decreasing_parts_disj [OF \<open>irrefl R\<close> \<open>trans R\<close> *]
+      show "multeqp P N M"
+      by (auto simp: multeqp_def split: if_splits)
+  next
+    assume "(N, M) \<in> Id" then show "multeqp P N M" by (auto simp: multeqp_def)
+  qed
+next
+  assume "multeqp P N M"
+  then obtain X Y Z where *: "Z = M #\<inter> N" "X = M - Z" "Y = N - Z"
+    and **: "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> R" by (auto simp: multeqp_def Let_def)
+  then have M: "M = Z + X" and N: "N = Z + Y" by (auto simp: multiset_eq_iff)
+  show "(N, M) \<in> (mult R)\<^sup>="
+  proof (cases "X \<noteq> {#}")
+    case True
+    with * and ** have "(Z + Y, Z + X) \<in> mult R"
+      by (auto intro: one_step_implies_mult)
+    then show ?thesis by (simp add: M N)
+  next
+    case False
+    then show ?thesis using **
+      by (cases "Y = {#}") (auto simp: M N)
+  qed
+qed
+
 
 subsubsection \<open>Partial-order properties\<close>
 
diff -r be252979cfe5 -r f2177f5d2aed src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu May 12 11:34:19 2016 +0200
+++ b/src/HOL/Wellfounded.thy	Thu May 12 09:34:07 2016 +0200
@@ -459,6 +459,20 @@
 apply (erule acyclic_converse [THEN iffD2])
 done
 
+text \<open>
+  Observe that the converse of an irreflexive, transitive,
+  and finite relation is again well-founded. Thus, we may
+  employ it for well-founded induction.
+\<close>
+lemma wf_converse:
+  assumes "irrefl r" and "trans r" and "finite r"
+  shows "wf (r\<inverse>)"
+proof -
+  have "acyclic r"
+    using \<open>irrefl r\<close> and \<open>trans r\<close> by (simp add: irrefl_def acyclic_irrefl)
+  with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse)
+qed
+
 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
 by (blast intro: finite_acyclic_wf wf_acyclic)