src/HOL/Quotient_Examples/FSet.thy

 lemma finter_raw_empty:
   "finter_raw l [] = []"
   by (induct l) (simp_all add: not_memb_nil)
 
 lemma set_cong:
-  shows "(set x = set y) = (x \<approx> y)"
+  shows "(x \<approx> y) = (set x = set y)"
   by auto
 
 lemma inj_map_eq_iff:
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
   by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)

     qed
     }
   then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
+text {* Set *}
+
+lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+  by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+
+lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+  by (auto simp add: sub_list_set)
+
+lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+
+lemma memb_set: "memb x xs = (x \<in> set xs)"
+  by (simp only: memb_def)
+
+lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+  by (induct xs, simp)
+     (metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+
+lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+  by (induct xs) auto
+
+lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+  by (induct xs) (simp_all add: memb_def)
+
 text {* Raw theorems of ffilter *}
 
 lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
 unfolding sub_list_def memb_def by auto
 

 lemma none_fin_fempty:
   "(\<forall>x. x |\<notin>| S) = (S = {||})"
   by (lifting none_memb_nil)
 
 lemma fset_cong:
-  "(fset_to_set S = fset_to_set T) = (S = T)"
+  "(S = T) = (fset_to_set S = fset_to_set T)"
   by (lifting set_cong)
 
 text {* fcard *}
 
 lemma fcard_fempty [simp]:

   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
   by (lifting map.simps)
 
 lemma fmap_set_image:
   "fset_to_set (fmap f S) = f ` (fset_to_set S)"
-  by (induct S) (simp_all)
+  by (induct S) simp_all
 
 lemma inj_fmap_eq_iff:
   "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
   by (lifting inj_map_eq_iff)
 

   by (lifting map_append)
 
 lemma fin_funion:
   "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
+
+text {* to_set *}
+
+lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+  by (lifting memb_set)
+
+lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+  by (simp add: fin_set)
+
+lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+  by (lifting fcard_raw_set)
+
+lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+  by (lifting sub_list_set)
+
+lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+  unfolding less_fset by (lifting sub_list_neq_set)
+
+lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+  by (lifting filter_set)
+
+lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+  by (lifting delete_raw_set)
+
+lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+  by (lifting inter_raw_set)
+
+lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+  by (lifting set_append)
+
+lemmas fset_to_set_trans =
+  fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+  inter_set union_set ffilter_set fset_to_set_simps
+  fset_cong fdelete_set fmap_set_image
 
 text {* ffold *}
 
 lemma ffold_nil: "ffold f z {||} = z"
   by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])

 by (lifting list_eq_filter)
 
 lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
 unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
 
-
 section {* lemmas transferred from Finite_Set theory *}
 
 text {* finiteness for finite sets holds *}
 lemma finite_fset: "finite (fset_to_set S)"
-by (induct S) auto
-
-text {* @{thm subset_empty} transferred is: *}
+  by (induct S) auto
+
+lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+  unfolding fset_to_set_trans
+  by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+
 lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
-by (cases xs) (auto simp add: fsubset_finsert not_fin_fnil)
-
-text {* @{thm not_psubset_empty} transferred is: *}
+  unfolding fset_to_set_trans
+  by (rule subset_empty)
+
 lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
-unfolding less_fset by (auto simp add: fsubseteq_fnil)
-
-text {* @{thm card_mono} transferred is: *}
+  unfolding fset_to_set_trans
+  by (rule not_psubset_empty)
+
 lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
-proof (induct xs arbitrary: ys)
-  case fempty
-  thus ?case by simp
-next
-  case (finsert x xs ys)
-  from finsert(1,3) have "xs |\<subseteq>| fdelete ys x"
-    by (auto simp add: fsubset_fin fin_fdelete)
-  from finsert(2) this have hyp: "fcard xs \<le> fcard (fdelete ys x)" by simp
-  from finsert(3) have "x |\<in>| ys" by (auto simp add: fsubset_fin)
-  from this have ys_is: "ys = finsert x (fdelete ys x)"
-    unfolding expand_fset_eq by (auto simp add: fin_fdelete)
-  from finsert(1) hyp have "fcard (finsert x xs) \<le> fcard (finsert x (fdelete ys x))"
-    by (auto simp add: fin_fdelete_ident)
-  from ys_is this show ?case by auto
-qed
-
-text {* @{thm card_seteq} transferred is: *}
+  unfolding fset_to_set_trans
+  by (rule card_mono[OF finite_fset])
+
 lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
-proof (induct xs arbitrary: ys)
-  case fempty
-  thus ?case by (simp add: fcard_0)
-next
-  case (finsert x xs ys)
-  from finsert have subset: "xs |\<subseteq>| fdelete ys x"
-    by (auto simp add: fsubset_fin fin_fdelete)
-  from finsert have x: "x |\<in>| ys"
-    by (auto simp add: fsubset_fin fin_fdelete)
-  from finsert(1,4) this have "fcard (fdelete ys x) \<le> fcard xs"
-    by (auto simp add: fcard_delete)
-  from finsert(2) this subset have hyp: "xs = fdelete ys x" by auto
-  from finsert have "x |\<in>| ys"
-    by (auto simp add: fsubset_fin fin_fdelete)
-  from this hyp show ?case
-    unfolding expand_fset_eq by (auto simp add: fin_fdelete)
-qed
-
-text {* @{thm psubset_card_mono} transferred is: *}
+  unfolding fset_to_set_trans
+  by (rule card_seteq[OF finite_fset])
+
 lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
-unfolding less_fset linorder_not_le[symmetric]
-by (auto simp add: fcard_fseteq)
-
+  unfolding fset_to_set_trans
+  by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+  unfolding fset_to_set_trans
+  by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+  unfolding fset_to_set_trans
+  by (rule card_Un_disjoint[OF finite_fset finite_fset])
+
+lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff1_less[OF finite_fset])
+
+lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+  unfolding fset_to_set_trans
+  by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_image_le[OF finite_fset])
 
 ML {*
 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}