# HG changeset patch # User haftmann # Date 1325884561 -3600 # Node ID 2c4d8de91c4ca5b631a97730e7320aecd0bb4b3d # Parent 6baea4fca6bd75139ac4197fb754d49542cf08e3 moved lemmas about List.set and set operations to List theory diff -r 6baea4fca6bd -r 2c4d8de91c4c src/HOL/Library/List_Cset.thy --- a/src/HOL/Library/List_Cset.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/Library/List_Cset.thy Fri Jan 06 22:16:01 2012 +0100 @@ -72,7 +72,7 @@ lemma filter_set [code]: "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" - by (simp add: Cset.set_def project_set) + by (simp add: Cset.set_def) lemma forall_set [code]: "Cset.forall P (Cset.set xs) \ list_all P xs" diff -r 6baea4fca6bd -r 2c4d8de91c4c src/HOL/List.thy --- a/src/HOL/List.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/List.thy Fri Jan 06 22:16:01 2012 +0100 @@ -2470,6 +2470,23 @@ qed qed +lemma union_set_fold: + "set xs \ 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 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 (in lattice) Inf_fin_set_fold: "Inf_fin (set (x # xs)) = fold inf xs x" proof - @@ -2588,6 +2605,22 @@ "concat xss = foldr append xss []" by (simp add: fold_append_concat_rev foldr_def) +lemma union_set_foldr: + "set xs \ A = foldr Set.insert xs A" +proof - + have "\x y :: 'a. insert y \ insert x = insert x \ insert y" + by auto + 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 (in lattice) Inf_fin_set_foldr [code]: "Inf_fin (set (x # xs)) = foldr inf xs x" by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) @@ -5166,7 +5199,7 @@ subsubsection {* Counterparts for set-related operations *} definition member :: "'a list \ 'a \ bool" where - [code_abbrev]: "member xs x \ x \ set xs" + "member xs x \ x \ set xs" text {* Use @{text member} only for generating executable code. Otherwise use @@ -5182,16 +5215,11 @@ "x \ set xs \ member xs x" by (simp add: member_def) -declare INF_def [code_unfold] -declare SUP_def [code_unfold] - -declare set_map [symmetric, code_unfold] - definition list_all :: "('a \ bool) \ 'a list \ bool" where - list_all_iff [code_abbrev]: "list_all P xs \ Ball (set xs) P" + list_all_iff: "list_all P xs \ Ball (set xs) P" definition list_ex :: "('a \ bool) \ 'a list \ bool" where - list_ex_iff [code_abbrev]: "list_ex P xs \ Bex (set xs) P" + list_ex_iff: "list_ex P xs \ Bex (set xs) P" definition list_ex1 :: "('a \ bool) \ 'a list \ bool" where list_ex1_iff [code_abbrev]: "list_ex1 P xs \ (\! x. x \ set xs \ P x)" @@ -5497,4 +5525,75 @@ code_const list_ex (Haskell "any") + +subsubsection {* Implementation of sets by lists *} + +text {* Basic operations *} + +lemma is_empty_set [code]: + "Set.is_empty (set xs) \ List.null xs" + by (simp add: Set.is_empty_def null_def) + +lemma empty_set [code]: + "{} = set []" + 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)" + 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 \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set [code]: + "Bex (set xs) P \ 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 + + +text {* Operations on relations *} + +lemma product_code [code]: + "Product_Type.product (set xs) (set ys) = set [(x, y). x \ xs, y \ ys]" + by (auto simp add: Product_Type.product_def) + +lemma Id_on_set [code]: + "Id_on (set xs) = set [(x, x). x \ 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 \ xys, yz \ 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 diff -r 6baea4fca6bd -r 2c4d8de91c4c src/HOL/More_Set.thy --- a/src/HOL/More_Set.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/More_Set.thy Fri Jan 06 22:16:01 2012 +0100 @@ -7,91 +7,6 @@ imports List begin -subsection {* Basic set operations *} - -lemma is_empty_set [code]: - "Set.is_empty (set xs) \ 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 \ 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 \ A = foldr Set.insert xs A" -proof - - have "\x y :: 'a. insert y \ insert x = insert x \ 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 "\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 - - -subsection {* Basic operations *} - -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)" - 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 \ list_all P xs" - by (simp add: list_all_iff) - -lemma Bex_set [code]: - "Bex (set xs) P \ 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]: @@ -152,28 +67,5 @@ "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 \ xs, y \ ys]" - by (auto simp add: Product_Type.product_def) - -lemma Id_on_set [code]: - "Id_on (set xs) = set [(x, x). x \ 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 \ xys, yz \ 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