1.1 --- a/src/HOL/List.thy Sat Jan 07 20:18:56 2012 +0100
1.2 +++ b/src/HOL/List.thy Sat Jan 07 20:44:23 2012 +0100
1.3 @@ -2605,7 +2605,19 @@
1.4 "concat xss = foldr append xss []"
1.5 by (simp add: fold_append_concat_rev foldr_def)
1.6
1.7 -lemma union_set_foldr:
1.8 +lemma minus_set_foldr [code]:
1.9 + "A - set xs = foldr Set.remove xs A"
1.10 +proof -
1.11 + have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
1.12 + by (auto simp add: remove_def)
1.13 + then show ?thesis by (simp add: minus_set_fold foldr_fold)
1.14 +qed
1.15 +
1.16 +lemma subtract_coset_filter [code]:
1.17 + "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
1.18 + by auto
1.19 +
1.20 +lemma union_set_foldr [code]:
1.21 "set xs \<union> A = foldr Set.insert xs A"
1.22 proof -
1.23 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
1.24 @@ -2613,13 +2625,17 @@
1.25 then show ?thesis by (simp add: union_set_fold foldr_fold)
1.26 qed
1.27
1.28 -lemma minus_set_foldr:
1.29 - "A - set xs = foldr Set.remove xs A"
1.30 -proof -
1.31 - have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
1.32 - by (auto simp add: remove_def)
1.33 - then show ?thesis by (simp add: minus_set_fold foldr_fold)
1.34 -qed
1.35 +lemma union_coset_foldr [code]:
1.36 + "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
1.37 + by auto
1.38 +
1.39 +lemma inter_set_filer [code]:
1.40 + "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
1.41 + by auto
1.42 +
1.43 +lemma inter_coset_foldr [code]:
1.44 + "A \<inter> List.coset xs = foldr Set.remove xs A"
1.45 + by (simp add: Diff_eq [symmetric] minus_set_foldr)
1.46
1.47 lemma (in lattice) Inf_fin_set_foldr [code]:
1.48 "Inf_fin (set (x # xs)) = foldr inf xs x"
1.49 @@ -2645,6 +2661,9 @@
1.50 "Sup (set xs) = foldr sup xs bot"
1.51 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
1.52
1.53 +declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
1.54 +declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
1.55 +
1.56 lemma (in complete_lattice) INF_set_foldr [code]:
1.57 "INFI (set xs) f = foldr (inf \<circ> f) xs top"
1.58 by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
1.59 @@ -2653,6 +2672,29 @@
1.60 "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
1.61 by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
1.62
1.63 +(* FIXME: better implement conversion by bisection *)
1.64 +
1.65 +lemma pred_of_set_fold_sup:
1.66 + assumes "finite A"
1.67 + shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
1.68 +proof (rule sym)
1.69 + interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
1.70 + by (fact comp_fun_idem_sup)
1.71 + from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
1.72 +qed
1.73 +
1.74 +lemma pred_of_set_set_fold_sup:
1.75 + "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
1.76 +proof -
1.77 + interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
1.78 + by (fact comp_fun_idem_sup)
1.79 + show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
1.80 +qed
1.81 +
1.82 +lemma pred_of_set_set_foldr_sup [code]:
1.83 + "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
1.84 + by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
1.85 +
1.86
1.87 subsubsection {* @{text upt} *}
1.88
1.89 @@ -5538,15 +5580,23 @@
1.90 "{} = set []"
1.91 by simp
1.92
1.93 +lemma UNIV_coset [code]:
1.94 + "UNIV = List.coset []"
1.95 + by simp
1.96 +
1.97 +lemma compl_set [code]:
1.98 + "- set xs = List.coset xs"
1.99 + by simp
1.100 +
1.101 +lemma compl_coset [code]:
1.102 + "- List.coset xs = set xs"
1.103 + by simp
1.104 +
1.105 lemma [code]:
1.106 "x \<in> set xs \<longleftrightarrow> List.member xs x"
1.107 "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
1.108 by (simp_all add: member_def)
1.109
1.110 -lemma UNIV_coset [code]:
1.111 - "UNIV = List.coset []"
1.112 - by simp
1.113 -
1.114 lemma insert_code [code]:
1.115 "insert x (set xs) = set (List.insert x xs)"
1.116 "insert x (List.coset xs) = List.coset (removeAll x xs)"
1.117 @@ -5557,6 +5607,14 @@
1.118 "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
1.119 by (simp_all add: remove_def Compl_insert)
1.120
1.121 +lemma project_set [code]:
1.122 + "Set.project P (set xs) = set (filter P xs)"
1.123 + by auto
1.124 +
1.125 +lemma image_set [code]:
1.126 + "image f (set xs) = set (map f xs)"
1.127 + by simp
1.128 +
1.129 lemma Ball_set [code]:
1.130 "Ball (set xs) P \<longleftrightarrow> list_all P xs"
1.131 by (simp add: list_all_iff)
1.132 @@ -5573,6 +5631,15 @@
1.133 then show ?thesis by simp
1.134 qed
1.135
1.136 +lemma the_elem_set [code]:
1.137 + "the_elem (set [x]) = x"
1.138 + by simp
1.139 +
1.140 +lemma Pow_set [code]:
1.141 + "Pow (set []) = {{}}"
1.142 + "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
1.143 + by (simp_all add: Pow_insert Let_def)
1.144 +
1.145
1.146 text {* Operations on relations *}
1.147
2.1 --- a/src/HOL/Set.thy Sat Jan 07 20:18:56 2012 +0100
2.2 +++ b/src/HOL/Set.thy Sat Jan 07 20:44:23 2012 +0100
2.3 @@ -431,10 +431,6 @@
2.4 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
2.5 by blast
2.6
2.7 -lemma member_exists [code]:
2.8 - "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
2.9 - by (rule sym) (fact bex_triv_one_point2)
2.10 -
2.11 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
2.12 by blast
2.13
2.14 @@ -1837,10 +1833,6 @@
2.15 "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
2.16 by (simp add: project_def)
2.17
2.18 -lemma inter_project [code]:
2.19 - "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
2.20 - by (auto simp add: project_def)
2.21 -
2.22 instantiation set :: (equal) equal
2.23 begin
2.24