# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1529313346 -7200
# Node ID 410818a69ee382bbefcf8628f5422dcf1f5f9d35
# Parent  8d1bf38c6fe673a4eda5a14a8826e338e3b64da6
material on finite sets and maps

diff -r 8d1bf38c6fe6 -r 410818a69ee3 src/HOL/Finite_Set.thy
--- 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")
diff -r 8d1bf38c6fe6 -r 410818a69ee3 src/HOL/Library/FSet.thy
--- 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 *)
diff -r 8d1bf38c6fe6 -r 410818a69ee3 src/HOL/Library/Finite_Map.thy
--- 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>