--- a/src/HOL/Finite_Set.thy Mon Jun 18 10:50:24 2018 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jun 18 11:15:46 2018 +0200
@@ -491,6 +491,9 @@
shows "finite (Set.bind S f)"
using assms by (simp add: bind_UNION)
+lemma finite_filter [simp]: "finite S \<Longrightarrow> finite (Set.filter P S)"
+unfolding Set.filter_def by simp
+
lemma finite_set_of_finite_funs:
assumes "finite A" "finite B"
shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
--- a/src/HOL/Library/FSet.thy Mon Jun 18 10:50:24 2018 +0200
+++ b/src/HOL/Library/FSet.thy Mon Jun 18 11:15:46 2018 +0200
@@ -203,6 +203,8 @@
lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)
+lift_definition sorted_list_of_fset :: "'a::linorder fset \<Rightarrow> 'a list" is sorted_list_of_set .
+
subsection \<open>Transferred lemmas from Set.thy\<close>
lemmas fset_eqI = set_eqI[Transfer.transferred]
@@ -387,6 +389,9 @@
lemmas funion_fempty[iff] = Un_empty[Transfer.transferred]
lemmas funion_fsubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred]
lemmas funion_fminus_finter = Un_Diff_Int[Transfer.transferred]
+lemmas ffunion_empty[simp] = Union_empty[Transfer.transferred]
+lemmas ffunion_mono = Union_mono[Transfer.transferred]
+lemmas ffunion_insert[simp] = Union_insert[Transfer.transferred]
lemmas fminus_finter2 = Diff_Int2[Transfer.transferred]
lemmas funion_finter_assoc_eq = Un_Int_assoc_eq[Transfer.transferred]
lemmas fBall_funion = ball_Un[Transfer.transferred]
@@ -583,6 +588,8 @@
lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q"
by auto
+lemma fBex_mono[mono]: "P \<le> Q \<Longrightarrow> fBex S P \<le> fBex S Q"
+by auto
end
@@ -670,6 +677,14 @@
by transfer (rule card_psubset)
+subsubsection \<open>\<open>sorted_list_of_fset\<close>\<close>
+
+lemma sorted_list_of_fset_simps[simp]:
+ "set (sorted_list_of_fset S) = fset S"
+ "fset_of_list (sorted_list_of_fset S) = S"
+by (transfer, simp)+
+
+
subsubsection \<open>\<open>ffold\<close>\<close>
(* FIXME: improve transferred to handle bounded meta quantification *)
--- a/src/HOL/Library/Finite_Map.thy Mon Jun 18 10:50:24 2018 +0200
+++ b/src/HOL/Library/Finite_Map.thy Mon Jun 18 11:15:46 2018 +0200
@@ -946,6 +946,20 @@
lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
by transfer' (auto simp: map_le_def dom_def)
+definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
+"sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
+
+lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
+unfolding sorted_list_of_fmap_def curry_def list.pred_map
+apply (auto simp: list_all_iff)
+including fmap.lifting fset.lifting
+by (transfer; auto simp: dom_def map_pred_def split: option.splits)+
+
+lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
+unfolding sorted_list_of_fmap_def
+including fmap.lifting fset.lifting
+by transfer (simp add: map_of_map_keys)
+
subsection \<open>Lifting/transfer setup\<close>