--- a/src/HOL/Library/Multiset.thy Fri Aug 22 14:39:40 2014 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 25 08:45:32 2014 +0200
@@ -530,6 +530,17 @@
"Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
by (rule multiset_eqI) simp
+lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
+ unfolding less_eq_multiset.rep_eq by auto
+
+lemma multiset_filter_mono: assumes "A \<le> B"
+ shows "Multiset.filter f A \<le> Multiset.filter f B"
+proof -
+ from assms[unfolded mset_le_exists_conv]
+ obtain C where B: "B = A + C" by auto
+ show ?thesis unfolding B by auto
+qed
+
syntax
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})")
syntax (xsymbol)
@@ -1325,6 +1336,17 @@
"mcard (multiset_of xs) = length xs"
by (induct xs) simp_all
+lemma mcard_mono: assumes "A \<le> B"
+ shows "mcard A \<le> mcard B"
+proof -
+ from assms[unfolded mset_le_exists_conv]
+ obtain C where B: "B = A + C" by auto
+ show ?thesis unfolding B by (induct C, auto)
+qed
+
+lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
+ by (rule mcard_mono[OF multiset_filter_subset])
+
subsection {* Alternative representations *}
--- a/src/Pure/Isar/method.ML Fri Aug 22 14:39:40 2014 +0200
+++ b/src/Pure/Isar/method.ML Mon Aug 25 08:45:32 2014 +0200
@@ -474,8 +474,8 @@
| _ =>
let
val facts =
- Attrib.partial_evaluation ctxt
- [((Binding.empty, [Attrib.internal (K att)]), thms)];
+ Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
+ |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
fun decl phi =
Context.mapping I init #>
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
--- a/src/Pure/ML/ml_thms.ML Fri Aug 22 14:39:40 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML Mon Aug 25 08:45:32 2014 +0200
@@ -37,7 +37,6 @@
val cons_thms = Data.map o apsnd o cons;
-
(* attribute source *)
val _ = Theory.setup