a quasi-recursive characterization of the multiset order (by Christian Sternagel)
authorhaftmann
Thu May 12 09:34:07 2016 +0200 (2016-05-12 ago)
changeset 63088f2177f5d2aed
parent 63087 be252979cfe5
child 63089 40134ddec3bf
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
src/HOL/Library/Multiset.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu May 12 11:34:19 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 12 09:34:07 2016 +0200
     1.3 @@ -2066,6 +2066,117 @@
     1.4      \<Longrightarrow> (I + K, I + J) \<in> mult r"
     1.5  using one_step_implies_mult_aux by blast
     1.6  
     1.7 +subsection \<open>A quasi-recursive characterization\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison
    1.11 +  \<open>(I + B, I + A) \<in> mult r\<close>, can always be made disjoint.
    1.12 +\<close>
    1.13 +lemma decreasing_parts_disj:
    1.14 +  assumes "irrefl r" and "trans r"
    1.15 +    and "A \<noteq> {#}" and *: "\<forall>b\<in>#B. \<exists>a\<in>#A. (b, a) \<in> r"
    1.16 +  defines "Z \<equiv> A #\<inter> B"
    1.17 +  defines "X \<equiv> A - Z"
    1.18 +  defines "Y \<equiv> B - Z"
    1.19 +  shows "X \<noteq> {#} \<and> X #\<inter> Y = {#} \<and>
    1.20 +    A = X + Z \<and> B = Y + Z \<and> (\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r)"
    1.21 +proof -
    1.22 +  define D
    1.23 +    where "D = set_mset A \<union> set_mset B"
    1.24 +  let ?r = "r \<inter> D \<times> D"
    1.25 +  have "irrefl ?r" and "trans ?r" and "finite ?r"
    1.26 +    using \<open>irrefl r\<close> and \<open>trans r\<close> by (auto simp: D_def irrefl_def trans_Restr)
    1.27 +  note wf_converse_induct = wf_induct [OF wf_converse [OF this]]
    1.28 +  { fix b assume "b \<in># B"
    1.29 +    then have "\<exists>x. x \<in># X \<and> (b, x) \<in> r"
    1.30 +    proof (induction rule: wf_converse_induct)
    1.31 +      case (1 b)
    1.32 +      then obtain a where "b \<in># B" and "a \<in># A" and "(b, a) \<in> r"
    1.33 +        using * by blast
    1.34 +      then show ?case
    1.35 +      proof (cases "a \<in># X")
    1.36 +        case False
    1.37 +        then have "a \<in># B" using \<open>a \<in># A\<close>
    1.38 +          by (simp add: X_def Z_def not_in_iff)
    1.39 +            (metis le_zero_eq not_in_iff)
    1.40 +        moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>"
    1.41 +          using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close>
    1.42 +          by (auto simp: D_def)
    1.43 +        ultimately obtain x where "x \<in># X" and "(a, x) \<in> r"
    1.44 +          using "1.IH" by blast
    1.45 +        moreover then have "(b, x) \<in> r"
    1.46 +          using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD)
    1.47 +        ultimately show ?thesis by blast
    1.48 +      qed blast
    1.49 +    qed }
    1.50 +  note B_less = this
    1.51 +  then have "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r"
    1.52 +    by (auto simp: Y_def Z_def dest: in_diffD)
    1.53 +  moreover have "X \<noteq> {#}"
    1.54 +  proof -
    1.55 +    obtain a where "a \<in># A" using \<open>A \<noteq> {#}\<close>
    1.56 +      by (auto simp: multiset_eq_iff)
    1.57 +    show ?thesis
    1.58 +    proof (cases "a \<in># X")
    1.59 +      case False
    1.60 +      then have "a \<in># B" using \<open>a \<in># A\<close>
    1.61 +        by (simp add: X_def Z_def not_in_iff)
    1.62 +          (metis le_zero_eq not_in_iff)
    1.63 +      then show ?thesis by (auto dest: B_less)
    1.64 +    qed auto
    1.65 +  qed
    1.66 +  moreover have "A = X + Z" and "B = Y + Z" and "X #\<inter> Y = {#}"
    1.67 +    by (auto simp: X_def Y_def Z_def multiset_eq_iff)
    1.68 +  ultimately show ?thesis by blast
    1.69 +qed
    1.70 +
    1.71 +text \<open>
    1.72 +  A predicate variant of the reflexive closure of \<open>mult\<close>, which is
    1.73 +  executable whenever the given predicate \<open>P\<close> is. Together with the
    1.74 +  standard code equations for \<open>op #\<inter>\<close> and \<open>op -\<close> this should yield
    1.75 +  a quadratic (with respect to calls to \<open>P\<close>) implementation of \<open>multeqp\<close>.
    1.76 +\<close>
    1.77 +definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.78 +  "multeqp P N M =
    1.79 +    (let Z = M #\<inter> N; X = M - Z; Y = N - Z in
    1.80 +    (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
    1.81 +
    1.82 +lemma multeqp_iff:
    1.83 +  assumes "irrefl R" and "trans R"
    1.84 +    and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
    1.85 +  shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
    1.86 +proof
    1.87 +  assume "(N, M) \<in> (mult R)\<^sup>="
    1.88 +  then show "multeqp P N M"
    1.89 +  proof
    1.90 +    assume "(N, M) \<in> mult R"
    1.91 +    from mult_implies_one_step [OF \<open>trans R\<close> this] obtain I J K
    1.92 +      where *: "I \<noteq> {#}" "\<forall>j\<in>#J. \<exists>i\<in>#I. (j, i) \<in> R"
    1.93 +      and [simp]: "M = K + I" "N = K + J" by blast
    1.94 +    from decreasing_parts_disj [OF \<open>irrefl R\<close> \<open>trans R\<close> *]
    1.95 +      show "multeqp P N M"
    1.96 +      by (auto simp: multeqp_def split: if_splits)
    1.97 +  next
    1.98 +    assume "(N, M) \<in> Id" then show "multeqp P N M" by (auto simp: multeqp_def)
    1.99 +  qed
   1.100 +next
   1.101 +  assume "multeqp P N M"
   1.102 +  then obtain X Y Z where *: "Z = M #\<inter> N" "X = M - Z" "Y = N - Z"
   1.103 +    and **: "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> R" by (auto simp: multeqp_def Let_def)
   1.104 +  then have M: "M = Z + X" and N: "N = Z + Y" by (auto simp: multiset_eq_iff)
   1.105 +  show "(N, M) \<in> (mult R)\<^sup>="
   1.106 +  proof (cases "X \<noteq> {#}")
   1.107 +    case True
   1.108 +    with * and ** have "(Z + Y, Z + X) \<in> mult R"
   1.109 +      by (auto intro: one_step_implies_mult)
   1.110 +    then show ?thesis by (simp add: M N)
   1.111 +  next
   1.112 +    case False
   1.113 +    then show ?thesis using **
   1.114 +      by (cases "Y = {#}") (auto simp: M N)
   1.115 +  qed
   1.116 +qed
   1.117 +
   1.118  
   1.119  subsubsection \<open>Partial-order properties\<close>
   1.120  
     2.1 --- a/src/HOL/Wellfounded.thy	Thu May 12 11:34:19 2016 +0200
     2.2 +++ b/src/HOL/Wellfounded.thy	Thu May 12 09:34:07 2016 +0200
     2.3 @@ -459,6 +459,20 @@
     2.4  apply (erule acyclic_converse [THEN iffD2])
     2.5  done
     2.6  
     2.7 +text \<open>
     2.8 +  Observe that the converse of an irreflexive, transitive,
     2.9 +  and finite relation is again well-founded. Thus, we may
    2.10 +  employ it for well-founded induction.
    2.11 +\<close>
    2.12 +lemma wf_converse:
    2.13 +  assumes "irrefl r" and "trans r" and "finite r"
    2.14 +  shows "wf (r\<inverse>)"
    2.15 +proof -
    2.16 +  have "acyclic r"
    2.17 +    using \<open>irrefl r\<close> and \<open>trans r\<close> by (simp add: irrefl_def acyclic_irrefl)
    2.18 +  with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse)
    2.19 +qed
    2.20 +
    2.21  lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
    2.22  by (blast intro: finite_acyclic_wf wf_acyclic)
    2.23