Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution



I use the following additional lemmas when working with mset_le:

subsubsection {* Pointwise ordering *}
  interpretation mset_le: partial_order["\<lambda>x y. (x\<le>#y)"] by
(auto intro: partial_order.intro mset_le_refl mset_le_antisym mset_le_trans)

  lemma mset_empty_minimal[simp, intro!]: "{#} \<le># c" by (unfold
mset_le_def, auto)
  lemma mset_empty_least[simp]: "c \<le># {#} = (c={#})" by (unfold
mset_le_def, auto iff add: multiset_eq_conv_count_eq)
  lemma mset_empty_leastI[intro!]: "c={#} \<Longrightarrow> c \<le>#
{#}" by (simp only: mset_empty_least)

  lemma mset_le_add_left: "a\<le>#b \<Longrightarrow> a\<le>#b+c" using
mset_le_mono_add[of a b "{#}" c, simplified] .
  lemma mset_le_add_right: "a\<le>#b \<Longrightarrow> a\<le>#c+b" using
mset_le_add_left by (auto simp add: union_commute)
  lemmas mset_le_add = mset_le_add_left mset_le_add_right
 
  lemma mset_le_single_conv[simp]: "({#e#}\<le>#M) = (e:#M)" by (unfold
mset_le_def) auto

  lemma mset_le_trans_elem: "\<lbrakk>e :# c; c \<le># c'\<rbrakk>
\<Longrightarrow> e :# c'" using mset_le_trans[of "{#e#}" c c',
simplified] by assumption

  lemma mset_le_subtract: "A\<le>#B \<Longrightarrow> A-C \<le># B-C"
    apply (unfold mset_le_def)
    apply auto
    apply (subgoal_tac "count A a \<le> count B a")
    apply arith
    apply simp
    done

  lemma mset_le_subtract_left: "A+B \<le># V+W \<Longrightarrow> B
\<le># V+W-A" by (auto dest: mset_le_subtract[of "A+B" "V+W" "A"])
  lemma mset_le_subtract_right: "A+B \<le># V+W \<Longrightarrow> A
\<le># V+W-B" by (auto dest: mset_le_subtract[of "A+B" "V+W" "B"])
 
  lemma mset_2dist2_cases:
    assumes A: "{#a#}+{#b#} \<le># A+B"
    assumes CASES: "{#a#}+{#b#} \<le># A \<Longrightarrow> P"
"{#a#}+{#b#} \<le># B \<Longrightarrow> P" "\<lbrakk>a :# A; b :#
B\<rbrakk> \<Longrightarrow> P" "\<lbrakk>a :# B; b :# A\<rbrakk>
\<Longrightarrow> P"
    shows "P"
  proof -
    { assume C: "a :# A" "b :# A-{#a#}"
      with mset_le_mono_add[of "{#a#}" "{#a#}" "{#b#}" "A-{#a#}"] have
"{#a#}+{#b#} \<le># A" by auto
    } moreover {
      assume C: "a :# A" "\<not> (b :# A-{#a#})"
      with A have "b:#B" by (unfold mset_le_def) (auto split: split_if_asm)
    } moreover {
      assume C: "\<not> (a :# A)" "b :# B-{#a#}"
      with A have "a :# B" by (unfold mset_le_def) (auto split:
split_if_asm)
      with C mset_le_mono_add[of "{#a#}" "{#a#}" "{#b#}" "B-{#a#}"] have
"{#a#}+{#b#} \<le># B" by auto
    } moreover {
      assume C: "\<not> (a :# A)" "\<not> (b :# B-{#a#})"
      with A have "a:#B \<and> b:#A" by (unfold mset_le_def) (auto
split: split_if_asm)
    } ultimately show P using CASES by blast
  qed

  lemma mset_union_subset: "A+B \<le># C \<Longrightarrow> A\<le>#C
\<and> B\<le># C"
    apply (unfold mset_le_def)
    apply auto
    apply (subgoal_tac "count A a + count B a \<le> count C a", arith,
simp)+
    done

  lemma mset_union_subset_s: "{#a#}+B \<le># C \<Longrightarrow> a :# C
\<and> B \<le># C" by (auto dest: mset_union_subset)


maybe that helps

-- Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.