# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1470483409 -7200
# Node ID 7fb02cee1cba4f6cfa64717fd720075b4d2890b4
# Parent  854402aa9374948fb1685e63c9e368cc7ae1414b
some additions to FSet

diff -r 854402aa9374 -r 7fb02cee1cba src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat Aug 06 08:26:58 2016 +0200
+++ b/src/HOL/Library/FSet.thy	Sat Aug 06 13:36:49 2016 +0200
@@ -202,6 +202,8 @@
 
 lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
 
+lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)
+
 
 subsection \<open>Transferred lemmas from Set.thy\<close>
 
@@ -441,6 +443,10 @@
 lemmas fbind_const = bind_const[Transfer.transferred]
 lemmas ffmember_filter[simp] = member_filter[Transfer.transferred]
 lemmas fequalityI = equalityI[Transfer.transferred]
+lemmas fset_of_list_simps[simp] = set_simps[Transfer.transferred]
+lemmas fset_of_list_append[simp] = set_append[Transfer.transferred]
+lemmas fset_of_list_rev[simp] = set_rev[Transfer.transferred]
+lemmas fset_of_list_map[simp] = set_map[Transfer.transferred]
 
 
 subsection \<open>Additional lemmas\<close>
@@ -483,7 +489,7 @@
 lemmas minus_fset[simp] = minus_fset.rep_eq
 
 
-subsubsection \<open>\<open>filter_fset\<close>\<close>
+subsubsection \<open>\<open>ffilter\<close>\<close>
 
 lemma subset_ffilter:
   "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
@@ -499,6 +505,20 @@
   unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
 
 
+subsubsection \<open>\<open>fset_of_list\<close>\<close>
+
+lemma fset_of_list_filter[simp]:
+  "fset_of_list (filter P xs) = ffilter P (fset_of_list xs)"
+  by transfer (auto simp: Set.filter_def)
+
+lemma fset_of_list_subset[intro]:
+  "set xs \<subseteq> set ys \<Longrightarrow> fset_of_list xs |\<subseteq>| fset_of_list ys"
+  by transfer simp
+
+lemma fset_of_list_elem: "(x |\<in>| fset_of_list xs) \<longleftrightarrow> (x \<in> set xs)"
+  by transfer simp
+
+
 subsubsection \<open>\<open>finsert\<close>\<close>
 
 (* FIXME, transferred doesn't work here *)
@@ -543,7 +563,11 @@
     "(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))"
 apply (simp only: atomize_all atomize_imp)
 apply (rule equal_intr_rule)
-by (transfer, simp)+
+  by (transfer, simp)+
+
+lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q"
+by auto
+
 
 end