[STATEMENT]
lemma take_from_mset_correct:
  assumes "s \<noteq> {#}"
  shows "take_from_mset s \<le> SPEC (\<lambda> (x, s'). x \<in># s \<and> s' = s - {#x#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_from_mset s \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {#}

goal (1 subgoal):
 1. take_from_mset s \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
unfolding take_from_mset_def
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {#}

goal (1 subgoal):
 1. ASSERT (s \<noteq> {#}) \<bind> (\<lambda>_. SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})) \<le> SPEC (\<lambda>(x, s'). x \<in># s \<and> s' = s - {#x#})
[PROOF STEP]
by simp