author | haftmann |

Thu May 12 09:34:07 2016 +0200 (2016-05-12 ago) | |

changeset 63088 | f2177f5d2aed |

parent 63087 | be252979cfe5 |

child 63089 | 40134ddec3bf |

a quasi-recursive characterization of the multiset order (by Christian Sternagel)

src/HOL/Library/Multiset.thy | file | annotate | diff | revisions | |

src/HOL/Wellfounded.thy | file | annotate | diff | revisions |

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