8 theory Multiset_Order |
8 theory Multiset_Order |
9 imports Multiset |
9 imports Multiset |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Alternative Characterizations\<close> |
12 subsection \<open>Alternative Characterizations\<close> |
|
13 |
|
14 subsubsection \<open>The Dershowitz--Manna Ordering\<close> |
|
15 |
|
16 definition multp\<^sub>D\<^sub>M where |
|
17 "multp\<^sub>D\<^sub>M r M N \<longleftrightarrow> |
|
18 (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)))" |
|
19 |
|
20 lemma multp\<^sub>D\<^sub>M_imp_multp: |
|
21 "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N" |
|
22 proof - |
|
23 assume "multp\<^sub>D\<^sub>M r M N" |
|
24 then obtain X Y where |
|
25 "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)" |
|
26 unfolding multp\<^sub>D\<^sub>M_def by blast |
|
27 then have "multp r (N - X + Y) (N - X + X)" |
|
28 by (intro one_step_implies_multp) (auto simp: Bex_def trans_def) |
|
29 with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "multp r M N" |
|
30 by (metis subset_mset.diff_add) |
|
31 qed |
|
32 |
|
33 subsubsection \<open>The Huet--Oppen Ordering\<close> |
|
34 |
|
35 definition multp\<^sub>H\<^sub>O where |
|
36 "multp\<^sub>H\<^sub>O r M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. r y x \<and> count M x < count N x))" |
|
37 |
|
38 lemma multp_imp_multp\<^sub>H\<^sub>O: |
|
39 assumes "asymp r" and "transp r" |
|
40 shows "multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N" |
|
41 unfolding multp_def mult_def |
|
42 proof (induction rule: trancl_induct) |
|
43 case (base P) |
|
44 then show ?case |
|
45 using \<open>asymp r\<close> |
|
46 by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits |
|
47 dest!: Suc_lessD) |
|
48 next |
|
49 case (step N P) |
|
50 from step(3) have "M \<noteq> N" and |
|
51 **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x. r y x \<and> count M x < count N x)" |
|
52 by (simp_all add: multp\<^sub>H\<^sub>O_def) |
|
53 from step(2) obtain M0 a K where |
|
54 *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a" |
|
55 using \<open>asymp r\<close> by (auto elim: mult1_lessE) |
|
56 from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" |
|
57 using *(4) \<open>asymp r\<close> |
|
58 by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI |
|
59 count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last) |
|
60 moreover |
|
61 { assume "count P a \<le> count M a" |
|
62 with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2) |
|
63 by (auto simp add: not_in_iff) |
|
64 with ** obtain z where z: "r a z" "count M z < count N z" |
|
65 by blast |
|
66 with * have "count N z \<le> count P z" |
|
67 using \<open>asymp r\<close> |
|
68 by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset |
|
69 diff_single_trivial in_diff_count not_le_imp_less) |
|
70 with z have "\<exists>z. r a z \<and> count M z < count P z" by auto |
|
71 } note count_a = this |
|
72 { fix y |
|
73 assume count_y: "count P y < count M y" |
|
74 have "\<exists>x. r y x \<and> count M x < count P x" |
|
75 proof (cases "y = a") |
|
76 case True |
|
77 with count_y count_a show ?thesis by auto |
|
78 next |
|
79 case False |
|
80 show ?thesis |
|
81 proof (cases "y \<in># K") |
|
82 case True |
|
83 with *(4) have "r y a" by simp |
|
84 then show ?thesis |
|
85 by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD]) |
|
86 next |
|
87 case False |
|
88 with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) |
|
89 by (simp add: not_in_iff) |
|
90 with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto |
|
91 show ?thesis |
|
92 proof (cases "z \<in># K") |
|
93 case True |
|
94 with *(4) have "r z a" by simp |
|
95 with z(1) show ?thesis |
|
96 by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD]) |
|
97 next |
|
98 case False |
|
99 with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding * |
|
100 by (auto simp add: not_in_iff) |
|
101 with z show ?thesis by auto |
|
102 qed |
|
103 qed |
|
104 qed |
|
105 } |
|
106 ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast |
|
107 qed |
|
108 |
|
109 lemma multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M: "multp\<^sub>H\<^sub>O r M N \<Longrightarrow> multp\<^sub>D\<^sub>M r M N" |
|
110 unfolding multp\<^sub>D\<^sub>M_def |
|
111 proof (intro iffI exI conjI) |
|
112 assume "multp\<^sub>H\<^sub>O r M N" |
|
113 then obtain z where z: "count M z < count N z" |
|
114 unfolding multp\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff) |
|
115 define X where "X = N - M" |
|
116 define Y where "Y = M - N" |
|
117 from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq) |
|
118 from z show "X \<subseteq># N" unfolding X_def by auto |
|
119 show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force |
|
120 show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)" |
|
121 proof (intro allI impI) |
|
122 fix k |
|
123 assume "k \<in># Y" |
|
124 then have "count N k < count M k" unfolding Y_def |
|
125 by (auto simp add: in_diff_count) |
|
126 with \<open>multp\<^sub>H\<^sub>O r M N\<close> obtain a where "r k a" and "count M a < count N a" |
|
127 unfolding multp\<^sub>H\<^sub>O_def by blast |
|
128 then show "\<exists>a. a \<in># X \<and> r k a" unfolding X_def |
|
129 by (auto simp add: in_diff_count) |
|
130 qed |
|
131 qed |
|
132 |
|
133 lemma multp_eq_multp\<^sub>D\<^sub>M: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>D\<^sub>M r" |
|
134 using multp\<^sub>D\<^sub>M_imp_multp multp_imp_multp\<^sub>H\<^sub>O[THEN multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M] |
|
135 by blast |
|
136 |
|
137 lemma multp_eq_multp\<^sub>H\<^sub>O: "asymp r \<Longrightarrow> transp r \<Longrightarrow> multp r = multp\<^sub>H\<^sub>O r" |
|
138 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 |
|
139 by blast |
|
140 |
|
141 subsubsection \<open>Properties of Preorders\<close> |
13 |
142 |
14 context preorder |
143 context preorder |
15 begin |
144 begin |
16 |
145 |
17 lemma order_mult: "class.order |
146 lemma order_mult: "class.order |
57 definition less_multiset\<^sub>H\<^sub>O where |
186 definition less_multiset\<^sub>H\<^sub>O where |
58 "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))" |
187 "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))" |
59 |
188 |
60 lemma mult_imp_less_multiset\<^sub>H\<^sub>O: |
189 lemma mult_imp_less_multiset\<^sub>H\<^sub>O: |
61 "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
190 "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
62 proof (unfold mult_def, induct rule: trancl_induct) |
191 unfolding multp_def[of "(<)", symmetric] |
63 case (base P) |
192 using multp_imp_multp\<^sub>H\<^sub>O[of "(<)"] |
64 then show ?case |
193 by (simp add: less_multiset\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_def) |
65 by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD) |
|
66 next |
|
67 case (step N P) |
|
68 from step(3) have "M \<noteq> N" and |
|
69 **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)" |
|
70 by (simp_all add: less_multiset\<^sub>H\<^sub>O_def) |
|
71 from step(2) obtain M0 a K where |
|
72 *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a" |
|
73 by (auto elim: mult1_lessE) |
|
74 from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits ) |
|
75 moreover |
|
76 { assume "count P a \<le> count M a" |
|
77 with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2) |
|
78 by (auto simp add: not_in_iff) |
|
79 with ** obtain z where z: "z > a" "count M z < count N z" |
|
80 by blast |
|
81 with * have "count N z \<le> count P z" |
|
82 by (auto elim: less_asym intro: count_inI) |
|
83 with z have "\<exists>z > a. count M z < count P z" by auto |
|
84 } note count_a = this |
|
85 { fix y |
|
86 assume count_y: "count P y < count M y" |
|
87 have "\<exists>x>y. count M x < count P x" |
|
88 proof (cases "y = a") |
|
89 case True |
|
90 with count_y count_a show ?thesis by auto |
|
91 next |
|
92 case False |
|
93 show ?thesis |
|
94 proof (cases "y \<in># K") |
|
95 case True |
|
96 with *(4) have "y < a" by simp |
|
97 then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans) |
|
98 next |
|
99 case False |
|
100 with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) |
|
101 by (simp add: not_in_iff) |
|
102 with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto |
|
103 show ?thesis |
|
104 proof (cases "z \<in># K") |
|
105 case True |
|
106 with *(4) have "z < a" by simp |
|
107 with z(1) show ?thesis |
|
108 by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans) |
|
109 next |
|
110 case False |
|
111 with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding * |
|
112 by (auto simp add: not_in_iff) |
|
113 with z show ?thesis by auto |
|
114 qed |
|
115 qed |
|
116 qed |
|
117 } |
|
118 ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast |
|
119 qed |
|
120 |
194 |
121 lemma less_multiset\<^sub>D\<^sub>M_imp_mult: |
195 lemma less_multiset\<^sub>D\<^sub>M_imp_mult: |
122 "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}" |
196 "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}" |
123 proof - |
197 unfolding multp_def[of "(<)", symmetric] |
124 assume "less_multiset\<^sub>D\<^sub>M M N" |
198 by (rule multp\<^sub>D\<^sub>M_imp_multp[of "(<)" M N]) (simp add: less_multiset\<^sub>D\<^sub>M_def multp\<^sub>D\<^sub>M_def) |
125 then obtain X Y where |
|
126 "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)" |
|
127 unfolding less_multiset\<^sub>D\<^sub>M_def by blast |
|
128 then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}" |
|
129 by (intro one_step_implies_mult) (auto simp: Bex_def trans_def) |
|
130 with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close> show "(M, N) \<in> mult {(x, y). x < y}" |
|
131 by (metis subset_mset.diff_add) |
|
132 qed |
|
133 |
199 |
134 lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
200 lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
135 unfolding less_multiset\<^sub>D\<^sub>M_def |
201 unfolding less_multiset\<^sub>D\<^sub>M_def less_multiset\<^sub>H\<^sub>O_def |
136 proof (intro iffI exI conjI) |
202 unfolding multp\<^sub>D\<^sub>M_def[symmetric] multp\<^sub>H\<^sub>O_def[symmetric] |
137 assume "less_multiset\<^sub>H\<^sub>O M N" |
203 by (rule multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M) |
138 then obtain z where z: "count M z < count N z" |
|
139 unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff) |
|
140 define X where "X = N - M" |
|
141 define Y where "Y = M - N" |
|
142 from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq) |
|
143 from z show "X \<subseteq># N" unfolding X_def by auto |
|
144 show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force |
|
145 show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)" |
|
146 proof (intro allI impI) |
|
147 fix k |
|
148 assume "k \<in># Y" |
|
149 then have "count N k < count M k" unfolding Y_def |
|
150 by (auto simp add: in_diff_count) |
|
151 with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a" |
|
152 unfolding less_multiset\<^sub>H\<^sub>O_def by blast |
|
153 then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def |
|
154 by (auto simp add: in_diff_count) |
|
155 qed |
|
156 qed |
|
157 |
204 |
158 lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
205 lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
159 by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O) |
206 unfolding multp_def[of "(<)", symmetric] |
|
207 using multp_eq_multp\<^sub>D\<^sub>M[of "(<)", simplified] |
|
208 by (simp add: multp\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M_def) |
160 |
209 |
161 lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
210 lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
162 by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O) |
211 unfolding multp_def[of "(<)", symmetric] |
|
212 using multp_eq_multp\<^sub>H\<^sub>O[of "(<)", simplified] |
|
213 by (simp add: multp\<^sub>H\<^sub>O_def less_multiset\<^sub>H\<^sub>O_def) |
163 |
214 |
164 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def] |
215 lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def] |
165 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def] |
216 lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def] |
166 |
217 |
167 end |
218 end |