src/HOL/More_Set.thy

 header {* Relating (finite) sets and lists *}
 
 theory More_Set
 imports List
 begin
-
-subsection {* Basic set operations *}
-
-lemma is_empty_set [code]:
-  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
-  by (simp add: Set.is_empty_def null_def)
-
-lemma empty_set [code]:
-  "{} = set []"
-  by simp
-
-
-subsection {* Functorial set operations *}
-
-lemma union_set_fold:
-  "set xs \<union> A = fold Set.insert xs A"
-proof -
-  interpret comp_fun_idem Set.insert
-    by (fact comp_fun_idem_insert)
-  show ?thesis by (simp add: union_fold_insert fold_set_fold)
-qed
-
-lemma union_set_foldr:
-  "set xs \<union> A = foldr Set.insert xs A"
-proof -
-  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by auto
-  then show ?thesis by (simp add: union_set_fold foldr_fold)
-qed
-
-lemma minus_set_fold:
-  "A - set xs = fold Set.remove xs A"
-proof -
-  interpret comp_fun_idem Set.remove
-    by (fact comp_fun_idem_remove)
-  show ?thesis
-    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
-qed
-
-lemma minus_set_foldr:
-  "A - set xs = foldr Set.remove xs A"
-proof -
-  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
-    by (auto simp add: remove_def)
-  then show ?thesis by (simp add: minus_set_fold foldr_fold)
-qed
-
-
-subsection {* Basic operations *}
-
-lemma [code]:
-  "x \<in> set xs \<longleftrightarrow> List.member xs x"
-  "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
-  by (simp_all add: member_def)
-
-lemma UNIV_coset [code]:
-  "UNIV = List.coset []"
-  by simp
-
-lemma insert_code [code]:
-  "insert x (set xs) = set (List.insert x xs)"
-  "insert x (List.coset xs) = List.coset (removeAll x xs)"
-  by simp_all
-
-lemma remove_code [code]:
-  "Set.remove x (set xs) = set (removeAll x xs)"
-  "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
-  by (simp_all add: remove_def Compl_insert)
-
-lemma Ball_set [code]:
-  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
-  by (simp add: list_all_iff)
-
-lemma Bex_set [code]:
-  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
-  by (simp add: list_ex_iff)
-
-lemma card_set [code]:
-  "card (set xs) = length (remdups xs)"
-proof -
-  have "card (set (remdups xs)) = length (remdups xs)"
-    by (rule distinct_card) simp
-  then show ?thesis by simp
-qed
-
 
 subsection {* Functorial operations *}
 
 lemma inter_code [code]:
   "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"

 
 lemma pred_of_set_set_foldr_sup [code]:
   "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
-
-subsection {* Operations on relations *}
-
-lemma product_code [code]:
-  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
-  by (auto simp add: Product_Type.product_def)
-
-lemma Id_on_set [code]:
-  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
-  by (auto simp add: Id_on_def)
-
-lemma trancl_set_ntrancl [code]:
-  "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
-  by (simp add: finite_trancl_ntranl)
-
-lemma set_rel_comp [code]:
-  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
-  by (auto simp add: Bex_def)
-
-lemma wf_set [code]:
-  "wf (set xs) = acyclic (set xs)"
-  by (simp add: wf_iff_acyclic_if_finite)
-
 end