1277 |
1277 |
1278 |
1278 |
1279 subsubsection {* Monotonicity of multiset union *} |
1279 subsubsection {* Monotonicity of multiset union *} |
1280 |
1280 |
1281 lemma mult1_union: |
1281 lemma mult1_union: |
1282 "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r" |
1282 "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r" |
1283 apply (unfold mult1_def) |
1283 apply (unfold mult1_def) |
1284 apply auto |
1284 apply auto |
1285 apply (rule_tac x = a in exI) |
1285 apply (rule_tac x = a in exI) |
1286 apply (rule_tac x = "C + M0" in exI) |
1286 apply (rule_tac x = "C + M0" in exI) |
1287 apply (simp add: add_assoc) |
1287 apply (simp add: add_assoc) |
1288 done |
1288 done |
1289 |
1289 |
1290 lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)" |
1290 lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)" |
1291 apply (unfold less_multiset_def mult_def) |
1291 apply (unfold less_multiset_def mult_def) |
1292 apply (erule trancl_induct) |
1292 apply (erule trancl_induct) |
1293 apply (blast intro: mult1_union transI order_less_trans r_into_trancl) |
1293 apply (blast intro: mult1_union) |
1294 apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans) |
1294 apply (blast intro: mult1_union trancl_trans) |
1295 done |
1295 done |
1296 |
1296 |
1297 lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)" |
1297 lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)" |
1298 apply (subst add_commute [of B C]) |
1298 apply (subst add_commute [of B C]) |
1299 apply (subst add_commute [of D C]) |
1299 apply (subst add_commute [of D C]) |