# HG changeset patch # User haftmann # Date 1325882925 -3600 # Node ID 6baea4fca6bd75139ac4197fb754d49542cf08e3 # Parent 0ec0af1c651d804c360a5f1923e04a612e1ddf12 incorporated various theorems from theory More_Set into corpus diff -r 0ec0af1c651d -r 6baea4fca6bd src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/Finite_Set.thy Fri Jan 06 21:48:45 2012 +0100 @@ -718,7 +718,7 @@ qed auto lemma comp_fun_idem_remove: - "comp_fun_idem (\x A. A - {x})" + "comp_fun_idem Set.remove" proof qed auto @@ -742,10 +742,11 @@ lemma minus_fold_remove: assumes "finite A" - shows "B - A = fold (\x A. A - {x}) B A" + shows "B - A = fold Set.remove B A" proof - - interpret comp_fun_idem "\x A. A - {x}" by (fact comp_fun_idem_remove) - from `finite A` show ?thesis by (induct A arbitrary: B) auto + interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove) + from `finite A` have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto + then show ?thesis .. qed context complete_lattice @@ -779,7 +780,7 @@ shows "Sup A = fold sup bot A" using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) -lemma inf_INFI_fold_inf: +lemma inf_INF_fold_inf: assumes "finite A" shows "inf B (INFI A f) = fold (inf \ f) B A" (is "?inf = ?fold") proof (rule sym) @@ -790,7 +791,7 @@ (simp_all add: INF_def inf_left_commute) qed -lemma sup_SUPR_fold_sup: +lemma sup_SUP_fold_sup: assumes "finite A" shows "sup B (SUPR A f) = fold (sup \ f) B A" (is "?sup = ?fold") proof (rule sym) @@ -801,15 +802,15 @@ (simp_all add: SUP_def sup_left_commute) qed -lemma INFI_fold_inf: +lemma INF_fold_inf: assumes "finite A" shows "INFI A f = fold (inf \ f) top A" - using assms inf_INFI_fold_inf [of A top] by simp + using assms inf_INF_fold_inf [of A top] by simp -lemma SUPR_fold_sup: +lemma SUP_fold_sup: assumes "finite A" shows "SUPR A f = fold (sup \ f) bot A" - using assms sup_SUPR_fold_sup [of A bot] by simp + using assms sup_SUP_fold_sup [of A bot] by simp end @@ -2066,10 +2067,10 @@ assumes fin: "finite (UNIV :: ('a \ 'b) set)" shows "finite (UNIV :: 'b set)" proof - - from fin have "finite (range (\f :: 'a \ 'b. f arbitrary))" - by(rule finite_imageI) - moreover have "UNIV = range (\f :: 'a \ 'b. f arbitrary)" - by(rule UNIV_eq_I) auto + from fin have "\arbitrary. finite (range (\f :: 'a \ 'b. f arbitrary))" + by (rule finite_imageI) + moreover have "\arbitrary. UNIV = range (\f :: 'a \ 'b. f arbitrary)" + by (rule UNIV_eq_I) auto ultimately show "finite (UNIV :: 'b set)" by simp qed diff -r 0ec0af1c651d -r 6baea4fca6bd src/HOL/Library/Cset.thy --- a/src/HOL/Library/Cset.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/Library/Cset.thy Fri Jan 06 21:48:45 2012 +0100 @@ -276,7 +276,7 @@ fix xs :: "'a list" show "member (Cset.set xs) = member (fold insert xs Cset.empty)" by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert] - fun_eq_iff Cset.set_def union_set [symmetric]) + fun_eq_iff Cset.set_def union_set_fold [symmetric]) qed lemma single_code [code]: @@ -296,7 +296,7 @@ "inf A (Cset.coset xs) = foldr Cset.remove xs A" proof - show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)" - by (simp add: inter project_def Cset.set_def member_def) + by (simp add: project_def Cset.set_def member_def) auto have *: "\x::'a. Cset.remove = (\x. Set \ Set.remove x \ set_of)" by (simp add: fun_eq_iff Set.remove_def) have "set_of \ fold (\x. Set \ Set.remove x \ set_of) xs = @@ -306,7 +306,7 @@ set_of (fold (\x. Set \ Set.remove x \ set_of) xs A)" by (simp add: fun_eq_iff) then have "inf A (Cset.coset xs) = fold Cset.remove xs A" - by (simp add: Diff_eq [symmetric] minus_set *) + by (simp add: Diff_eq [symmetric] minus_set_fold *) moreover have "\x y :: 'a. Cset.remove y \ Cset.remove x = Cset.remove x \ Cset.remove y" by (auto simp add: Set.remove_def *) ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A" @@ -326,7 +326,7 @@ set_of (fold (\x. Set \ Set.insert x \ set_of) xs A)" by (simp add: fun_eq_iff) then have "sup (Cset.set xs) A = fold Cset.insert xs A" - by (simp add: union_set *) + by (simp add: union_set_fold *) moreover have "\x y :: 'a. Cset.insert y \ Cset.insert x = Cset.insert x \ Cset.insert y" by (auto simp add: *) ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" diff -r 0ec0af1c651d -r 6baea4fca6bd 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 21:48:45 2012 +0100 @@ -7,26 +7,6 @@ imports List begin -lemma comp_fun_idem_remove: - "comp_fun_idem Set.remove" -proof - - have rem: "Set.remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) - show ?thesis by (simp only: comp_fun_idem_remove rem) -qed - -lemma minus_fold_remove: - assumes "finite A" - shows "B - A = Finite_Set.fold Set.remove B A" -proof - - have rem: "Set.remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) - show ?thesis by (simp only: rem assms minus_fold_remove) -qed - -lemma bounded_Collect_code: (* FIXME delete candidate *) - "{x \ A. P x} = Set.project P A" - by (simp add: project_def) - - subsection {* Basic set operations *} lemma is_empty_set [code]: @@ -37,26 +17,10 @@ "{} = set []" by simp -lemma insert_set_compl: - "insert x (- set xs) = - set (removeAll x xs)" - by auto - -lemma remove_set_compl: - "Set.remove x (- set xs) = - set (List.insert x xs)" - by (auto simp add: remove_def List.insert_def) - -lemma image_set: - "image f (set xs) = set (map f xs)" - by simp - -lemma project_set: - "Set.project P (set xs) = set (filter P xs)" - by (auto simp add: project_def) - subsection {* Functorial set operations *} -lemma union_set: +lemma union_set_fold: "set xs \ A = fold Set.insert xs A" proof - interpret comp_fun_idem Set.insert @@ -69,10 +33,10 @@ proof - have "\x y :: 'a. insert y \ insert x = insert x \ insert y" by auto - then show ?thesis by (simp add: union_set foldr_fold) + then show ?thesis by (simp add: union_set_fold foldr_fold) qed -lemma minus_set: +lemma minus_set_fold: "A - set xs = fold Set.remove xs A" proof - interpret comp_fun_idem Set.remove @@ -86,56 +50,29 @@ 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 foldr_fold) + then show ?thesis by (simp add: minus_set_fold foldr_fold) qed -subsection {* Derived set operations *} - -lemma member [code]: - "a \ A \ (\x\A. a = x)" - by simp - -lemma subset [code]: - "A \ B \ A \ B \ \ B \ A" - by (fact less_le_not_le) - -lemma set_eq [code]: - "A = B \ A \ B \ B \ A" - by (fact eq_iff) - -lemma inter [code]: - "A \ B = Set.project (\x. x \ A) B" - by (auto simp add: project_def) - - -subsection {* Code generator setup *} - -definition coset :: "'a list \ 'a set" where - [simp]: "coset xs = - set xs" - -code_datatype set coset - - subsection {* Basic operations *} lemma [code]: "x \ set xs \ List.member xs x" - "x \ coset xs \ \ List.member xs x" + "x \ List.coset xs \ \ List.member xs x" by (simp_all add: member_def) lemma UNIV_coset [code]: - "UNIV = coset []" + "UNIV = List.coset []" by simp lemma insert_code [code]: "insert x (set xs) = set (List.insert x xs)" - "insert x (coset xs) = coset (removeAll 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 (coset xs) = coset (List.insert 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]: @@ -159,17 +96,17 @@ lemma inter_code [code]: "A \ set xs = set (List.filter (\x. x \ A) xs)" - "A \ coset xs = foldr Set.remove xs A" - by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) + "A \ List.coset xs = foldr Set.remove xs A" + by (simp add: inter_project project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) lemma subtract_code [code]: "A - set xs = foldr Set.remove xs A" - "A - coset xs = set (List.filter (\x. x \ A) xs)" + "A - List.coset xs = set (List.filter (\x. x \ A) xs)" by (auto simp add: minus_set_foldr) lemma union_code [code]: "set xs \ A = foldr insert xs A" - "coset xs \ A = coset (List.filter (\x. x \ A) xs)" + "List.coset xs \ A = List.coset (List.filter (\x. x \ A) xs)" by (auto simp add: union_set_foldr) definition Inf :: "'a::complete_lattice set \ 'a" where @@ -184,12 +121,12 @@ lemma Inf_code [code]: "More_Set.Inf (set xs) = foldr inf xs top" - "More_Set.Inf (coset []) = bot" + "More_Set.Inf (List.coset []) = bot" by (simp_all add: Inf_set_foldr) lemma Sup_sup [code]: "More_Set.Sup (set xs) = foldr sup xs bot" - "More_Set.Sup (coset []) = top" + "More_Set.Sup (List.coset []) = top" by (simp_all add: Sup_set_foldr) (* FIXME: better implement conversion by bisection *) @@ -226,7 +163,8 @@ "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)" +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]: diff -r 0ec0af1c651d -r 6baea4fca6bd src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/Set.thy Fri Jan 06 21:48:45 2012 +0100 @@ -431,6 +431,10 @@ 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 @@ -522,6 +526,10 @@ lemma set_mp: "A \ B ==> x:A ==> x:B" by (rule subsetD) +lemma subset_not_subset_eq [code]: + "A \ B \ A \ B \ \ B \ A" + by (fact less_le_not_le) + lemma eq_mem_trans: "a=b ==> b \ A ==> a \ A" by simp @@ -1829,6 +1837,10 @@ "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