# HG changeset patch # User haftmann # Date 1325965463 -3600 # Node ID f58b7f9d39208ef124395e98924c9b6f24b455e5 # Parent f27cf421500abc49b8b05ac1ad46cf3d6baa7463 massaging of code setup for sets diff -r f27cf421500a -r f58b7f9d3920 src/HOL/List.thy --- a/src/HOL/List.thy Sat Jan 07 20:18:56 2012 +0100 +++ b/src/HOL/List.thy Sat Jan 07 20:44:23 2012 +0100 @@ -2605,7 +2605,19 @@ "concat xss = foldr append xss []" by (simp add: fold_append_concat_rev foldr_def) -lemma union_set_foldr: +lemma minus_set_foldr [code]: + "A - set xs = foldr Set.remove xs A" +proof - + have "\x y :: 'a. Set.remove y \ Set.remove x = Set.remove x \ Set.remove y" + by (auto simp add: remove_def) + then show ?thesis by (simp add: minus_set_fold foldr_fold) +qed + +lemma subtract_coset_filter [code]: + "A - List.coset xs = set (List.filter (\x. x \ A) xs)" + by auto + +lemma union_set_foldr [code]: "set xs \ A = foldr Set.insert xs A" proof - have "\x y :: 'a. insert y \ insert x = insert x \ insert y" @@ -2613,13 +2625,17 @@ then show ?thesis by (simp add: union_set_fold foldr_fold) qed -lemma minus_set_foldr: - "A - set xs = foldr Set.remove xs A" -proof - - have "\x y :: 'a. Set.remove y \ Set.remove x = Set.remove x \ Set.remove y" - by (auto simp add: remove_def) - then show ?thesis by (simp add: minus_set_fold foldr_fold) -qed +lemma union_coset_foldr [code]: + "List.coset xs \ A = List.coset (List.filter (\x. x \ A) xs)" + by auto + +lemma inter_set_filer [code]: + "A \ set xs = set (List.filter (\x. x \ A) xs)" + by auto + +lemma inter_coset_foldr [code]: + "A \ List.coset xs = foldr Set.remove xs A" + by (simp add: Diff_eq [symmetric] minus_set_foldr) lemma (in lattice) Inf_fin_set_foldr [code]: "Inf_fin (set (x # xs)) = foldr inf xs x" @@ -2645,6 +2661,9 @@ "Sup (set xs) = foldr sup xs bot" by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) +declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code] +declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code] + lemma (in complete_lattice) INF_set_foldr [code]: "INFI (set xs) f = foldr (inf \ f) xs top" by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric]) @@ -2653,6 +2672,29 @@ "SUPR (set xs) f = foldr (sup \ f) xs bot" by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric]) +(* FIXME: better implement conversion by bisection *) + +lemma pred_of_set_fold_sup: + assumes "finite A" + shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") +proof (rule sym) + interpret comp_fun_idem "sup :: 'a Predicate.pred \ 'a Predicate.pred \ 'a Predicate.pred" + by (fact comp_fun_idem_sup) + from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) +qed + +lemma pred_of_set_set_fold_sup: + "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot" +proof - + interpret comp_fun_idem "sup :: 'a Predicate.pred \ 'a Predicate.pred \ 'a Predicate.pred" + by (fact comp_fun_idem_sup) + show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) +qed + +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) + subsubsection {* @{text upt} *} @@ -5538,15 +5580,23 @@ "{} = set []" by simp +lemma UNIV_coset [code]: + "UNIV = List.coset []" + by simp + +lemma compl_set [code]: + "- set xs = List.coset xs" + by simp + +lemma compl_coset [code]: + "- List.coset xs = set xs" + by simp + lemma [code]: "x \ set xs \ List.member xs x" "x \ List.coset xs \ \ 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)" @@ -5557,6 +5607,14 @@ "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" by (simp_all add: remove_def Compl_insert) +lemma project_set [code]: + "Set.project P (set xs) = set (filter P xs)" + by auto + +lemma image_set [code]: + "image f (set xs) = set (map f xs)" + by simp + lemma Ball_set [code]: "Ball (set xs) P \ list_all P xs" by (simp add: list_all_iff) @@ -5573,6 +5631,15 @@ then show ?thesis by simp qed +lemma the_elem_set [code]: + "the_elem (set [x]) = x" + by simp + +lemma Pow_set [code]: + "Pow (set []) = {{}}" + "Pow (set (x # xs)) = (let A = Pow (set xs) in A \ insert x ` A)" + by (simp_all add: Pow_insert Let_def) + text {* Operations on relations *} diff -r f27cf421500a -r f58b7f9d3920 src/HOL/Set.thy --- a/src/HOL/Set.thy Sat Jan 07 20:18:56 2012 +0100 +++ b/src/HOL/Set.thy Sat Jan 07 20:44:23 2012 +0100 @@ -431,10 +431,6 @@ lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" by blast -lemma member_exists [code]: - "a \ A \ (\x\A. a = x)" - by (rule sym) (fact bex_triv_one_point2) - lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" by blast @@ -1837,10 +1833,6 @@ "x \ Set.project P A \ x \ A \ P x" by (simp add: project_def) -lemma inter_project [code]: - "A \ B = Set.project (\x. x \ A) B" - by (auto simp add: project_def) - instantiation set :: (equal) equal begin