equal
deleted
inserted
replaced
2000 lemma mset_rev [simp]: |
2000 lemma mset_rev [simp]: |
2001 "mset (rev xs) = mset xs" |
2001 "mset (rev xs) = mset xs" |
2002 by (induct xs) simp_all |
2002 by (induct xs) simp_all |
2003 |
2003 |
2004 lemma surj_mset: "surj mset" |
2004 lemma surj_mset: "surj mset" |
2005 apply (unfold surj_def) |
2005 unfolding surj_def |
2006 apply (rule allI) |
2006 proof (rule allI) |
2007 apply (rule_tac M = y in multiset_induct) |
2007 fix M |
2008 apply auto |
2008 show "\<exists>xs. M = mset xs" |
2009 apply (rule_tac x = "x # xa" in exI) |
2009 by (induction M) (auto intro: exI[of _ "_ # _"]) |
2010 apply auto |
2010 qed |
2011 done |
|
2012 |
2011 |
2013 lemma distinct_count_atmost_1: |
2012 lemma distinct_count_atmost_1: |
2014 "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))" |
2013 "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))" |
2015 proof (induct x) |
2014 proof (induct x) |
2016 case Nil then show ?case by simp |
2015 case Nil then show ?case by simp |