summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Tue, 27 Dec 2011 15:38:45 +0100 | |

changeset 46002 | b319f1b0c634 |

parent 46001 | 0b562d564d5f (current diff) |

parent 45994 | 38a46e029784 (diff) |

child 46003 | c0fe5e8e4864 |

child 46009 | 5cb7ef5bfef2 |

merged

src/HOL/Library/More_List.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/More_Set.thy | file | annotate | diff | comparison | revisions |

--- a/NEWS Tue Dec 27 15:37:33 2011 +0100 +++ b/NEWS Tue Dec 27 15:38:45 2011 +0100 @@ -53,6 +53,17 @@ *** HOL *** +* Finite_Set.fold now qualified. INCOMPATIBILITY. + +* Renamed some facts on canonical fold on lists, in order to avoid problems +with interpretation involving corresponding facts on foldl with the same base names: + + fold_set_remdups ~> fold_set_fold_remdups + fold_set ~> fold_set_fold + fold1_set ~> fold1_set_fold + +INCOMPATIBILITY. + * 'set' is now a proper type constructor. Definitions mem_def and Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`. For typical proofs,

--- a/src/HOL/GCD.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/GCD.thy Tue Dec 27 15:38:45 2011 +0100 @@ -1486,7 +1486,7 @@ begin definition - "Lcm (M::nat set) = (if finite M then fold lcm 1 M else 0)" + "Lcm (M::nat set) = (if finite M then Finite_Set.fold lcm 1 M else 0)" definition "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}" @@ -1608,11 +1608,11 @@ done lemma Lcm_set_nat [code_unfold]: - "Lcm (set ns) = foldl lcm (1::nat) ns" + "Lcm (set ns) = fold lcm ns (1::nat)" by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold) lemma Gcd_set_nat [code_unfold]: - "Gcd (set ns) = foldl gcd (0::nat) ns" + "Gcd (set ns) = fold gcd ns (0::nat)" by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold) lemma mult_inj_if_coprime_nat:

--- a/src/HOL/IMP/Abs_Int1_ivl.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy Tue Dec 27 15:38:45 2011 +0100 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int1_ivl -imports Abs_Int1 Abs_Int_Tests "~~/src/HOL/Library/More_Set" +imports Abs_Int1 Abs_Int_Tests begin subsection "Interval Analysis"

--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Dec 27 15:38:45 2011 +0100 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory Abs_Int_den1_ivl -imports Abs_Int_den1 "~~/src/HOL/Library/More_Set" +imports Abs_Int_den1 begin subsection "Interval Analysis"

--- a/src/HOL/IsaMakefile Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 27 15:38:45 2011 +0100 @@ -286,6 +286,8 @@ List.thy \ Main.thy \ Map.thy \ + More_List.thy \ + More_Set.thy \ Nat_Numeral.thy \ Nat_Transfer.thy \ New_DSequence.thy \ @@ -458,7 +460,7 @@ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ - Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ + Library/Monad_Syntax.thy \ Library/Multiset.thy Library/Nat_Bijection.thy \ Library/Numeral_Type.thy Library/Old_Recdef.thy \ Library/OptionalSugar.thy Library/Order_Relation.thy \

--- a/src/HOL/Library/AList_Impl.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/AList_Impl.thy Tue Dec 27 15:38:45 2011 +0100 @@ -5,7 +5,7 @@ header {* Implementation of Association Lists *} theory AList_Impl -imports Main More_List +imports Main begin text {*

--- a/src/HOL/Library/Cset.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Cset.thy Tue Dec 27 15:38:45 2011 +0100 @@ -4,7 +4,7 @@ header {* A dedicated set type which is executable on its finite part *} theory Cset -imports More_Set More_List +imports Main begin subsection {* Lifting *}

--- a/src/HOL/Library/Dlist.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Dec 27 15:38:45 2011 +0100 @@ -3,7 +3,7 @@ header {* Lists with elements distinct as canonical example for datatype invariants *} theory Dlist -imports Main More_List +imports Main begin subsection {* The type of distinct lists *}

--- a/src/HOL/Library/Library.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Library.thy Tue Dec 27 15:38:45 2011 +0100 @@ -33,7 +33,6 @@ Kleene_Algebra Mapping Monad_Syntax - More_List Multiset Numeral_Type Old_Recdef

--- a/src/HOL/Library/Monad_Syntax.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Monad_Syntax.thy Tue Dec 27 15:38:45 2011 +0100 @@ -5,7 +5,7 @@ header {* Monad notation for arbitrary types *} theory Monad_Syntax -imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List" +imports Main "~~/src/Tools/Adhoc_Overloading" begin text {*

--- a/src/HOL/Library/More_List.thy Tue Dec 27 15:37:33 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,312 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Operations on lists beyond the standard List theory *} - -theory More_List -imports Main Multiset -begin - -hide_const (open) Finite_Set.fold - -text {* Repairing code generator setup *} - -declare (in lattice) Inf_fin_set_fold [code_unfold del] -declare (in lattice) Sup_fin_set_fold [code_unfold del] -declare (in linorder) Min_fin_set_fold [code_unfold del] -declare (in linorder) Max_fin_set_fold [code_unfold del] -declare (in complete_lattice) Inf_set_fold [code_unfold del] -declare (in complete_lattice) Sup_set_fold [code_unfold del] - - -text {* Fold combinator with canonical argument order *} - -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where - "fold f [] = id" - | "fold f (x # xs) = fold f xs \<circ> f x" - -lemma foldl_fold: - "foldl f s xs = fold (\<lambda>x s. f s x) xs s" - by (induct xs arbitrary: s) simp_all - -lemma foldr_fold_rev: - "foldr f xs = fold f (rev xs)" - by (simp add: foldr_foldl foldl_fold fun_eq_iff) - -lemma fold_rev_conv [code_unfold]: - "fold f (rev xs) = foldr f xs" - by (simp add: foldr_fold_rev) - -lemma fold_cong [fundef_cong]: - "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) - \<Longrightarrow> fold f xs a = fold g ys b" - by (induct ys arbitrary: a b xs) simp_all - -lemma fold_id: - assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id" - shows "fold f xs = id" - using assms by (induct xs) simp_all - -lemma fold_commute: - assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" - shows "h \<circ> fold g xs = fold f xs \<circ> h" - using assms by (induct xs) (simp_all add: fun_eq_iff) - -lemma fold_commute_apply: - assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" - shows "h (fold g xs s) = fold f xs (h s)" -proof - - from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute) - then show ?thesis by (simp add: fun_eq_iff) -qed - -lemma fold_invariant: - assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s" - and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)" - shows "P (fold f xs s)" - using assms by (induct xs arbitrary: s) simp_all - -lemma fold_weak_invariant: - assumes "P s" - and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)" - shows "P (fold f xs s)" - using assms by (induct xs arbitrary: s) simp_all - -lemma fold_append [simp]: - "fold f (xs @ ys) = fold f ys \<circ> fold f xs" - by (induct xs) simp_all - -lemma fold_map [code_unfold]: - "fold g (map f xs) = fold (g o f) xs" - by (induct xs) simp_all - -lemma fold_remove1_split: - assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" - and x: "x \<in> set xs" - shows "fold f xs = fold f (remove1 x xs) \<circ> f x" - using assms by (induct xs) (auto simp add: o_assoc [symmetric]) - -lemma fold_multiset_equiv: - assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" - and equiv: "multiset_of xs = multiset_of ys" - shows "fold f xs = fold f ys" -using f equiv [symmetric] proof (induct xs arbitrary: ys) - case Nil then show ?case by simp -next - case (Cons x xs) - then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) - have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" - by (rule Cons.prems(1)) (simp_all add: *) - moreover from * have "x \<in> set ys" by simp - ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) - moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) - ultimately show ?case by simp -qed - -lemma fold_rev: - assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" - shows "fold f (rev xs) = fold f xs" - by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set) - -lemma foldr_fold: - assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" - shows "foldr f xs = fold f xs" - using assms unfolding foldr_fold_rev by (rule fold_rev) - -lemma fold_Cons_rev: - "fold Cons xs = append (rev xs)" - by (induct xs) simp_all - -lemma rev_conv_fold [code]: - "rev xs = fold Cons xs []" - by (simp add: fold_Cons_rev) - -lemma fold_append_concat_rev: - "fold append xss = append (concat (rev xss))" - by (induct xss) simp_all - -lemma concat_conv_foldr [code]: - "concat xss = foldr append xss []" - by (simp add: fold_append_concat_rev foldr_fold_rev) - -lemma fold_plus_listsum_rev: - "fold plus xs = plus (listsum (rev xs))" - by (induct xs) (simp_all add: add.assoc) - -lemma (in monoid_add) listsum_conv_fold [code]: - "listsum xs = fold (\<lambda>x y. y + x) xs 0" - by (auto simp add: listsum_foldl foldl_fold fun_eq_iff) - -lemma (in linorder) sort_key_conv_fold: - assumes "inj_on f (set xs)" - shows "sort_key f xs = fold (insort_key f) xs []" -proof - - have "fold (insort_key f) (rev xs) = fold (insort_key f) xs" - proof (rule fold_rev, rule ext) - fix zs - fix x y - assume "x \<in> set xs" "y \<in> set xs" - with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD) - have **: "x = y \<longleftrightarrow> y = x" by auto - show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs" - by (induct zs) (auto intro: * simp add: **) - qed - then show ?thesis by (simp add: sort_key_def foldr_fold_rev) -qed - -lemma (in linorder) sort_conv_fold: - "sort xs = fold insort xs []" - by (rule sort_key_conv_fold) simp - - -text {* @{const Finite_Set.fold} and @{const fold} *} - -lemma (in comp_fun_commute) fold_set_remdups: - "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" - by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) - -lemma (in comp_fun_idem) fold_set: - "Finite_Set.fold f y (set xs) = fold f xs y" - by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) - -lemma (in ab_semigroup_idem_mult) fold1_set: - assumes "xs \<noteq> []" - shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" -proof - - interpret comp_fun_idem times by (fact comp_fun_idem) - from assms obtain y ys where xs: "xs = y # ys" - by (cases xs) auto - show ?thesis - proof (cases "set ys = {}") - case True with xs show ?thesis by simp - next - case False - then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" - by (simp only: finite_set fold1_eq_fold_idem) - with xs show ?thesis by (simp add: fold_set mult_commute) - qed -qed - -lemma (in lattice) Inf_fin_set_fold: - "Inf_fin (set (x # xs)) = fold inf xs x" -proof - - interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_inf) - show ?thesis - by (simp add: Inf_fin_def fold1_set del: set.simps) -qed - -lemma (in lattice) Inf_fin_set_foldr [code_unfold]: - "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) - -lemma (in lattice) Sup_fin_set_fold: - "Sup_fin (set (x # xs)) = fold sup xs x" -proof - - interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_sup) - show ?thesis - by (simp add: Sup_fin_def fold1_set del: set.simps) -qed - -lemma (in lattice) Sup_fin_set_foldr [code_unfold]: - "Sup_fin (set (x # xs)) = foldr sup xs x" - by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) - -lemma (in linorder) Min_fin_set_fold: - "Min (set (x # xs)) = fold min xs x" -proof - - interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_min) - show ?thesis - by (simp add: Min_def fold1_set del: set.simps) -qed - -lemma (in linorder) Min_fin_set_foldr [code_unfold]: - "Min (set (x # xs)) = foldr min xs x" - by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) - -lemma (in linorder) Max_fin_set_fold: - "Max (set (x # xs)) = fold max xs x" -proof - - interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_max) - show ?thesis - by (simp add: Max_def fold1_set del: set.simps) -qed - -lemma (in linorder) Max_fin_set_foldr [code_unfold]: - "Max (set (x # xs)) = foldr max xs x" - by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) - -lemma (in complete_lattice) Inf_set_fold: - "Inf (set xs) = fold inf xs top" -proof - - interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact comp_fun_idem_inf) - show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute) -qed - -lemma (in complete_lattice) Inf_set_foldr [code_unfold]: - "Inf (set xs) = foldr inf xs top" - by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) - -lemma (in complete_lattice) Sup_set_fold: - "Sup (set xs) = fold sup xs bot" -proof - - interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact comp_fun_idem_sup) - show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) -qed - -lemma (in complete_lattice) Sup_set_foldr [code_unfold]: - "Sup (set xs) = foldr sup xs bot" - by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) - -lemma (in complete_lattice) INFI_set_fold: - "INFI (set xs) f = fold (inf \<circ> f) xs top" - unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. - -lemma (in complete_lattice) SUPR_set_fold: - "SUPR (set xs) f = fold (sup \<circ> f) xs bot" - unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. - - -text {* @{text nth_map} *} - -definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where - "nth_map n f xs = (if n < length xs then - take n xs @ [f (xs ! n)] @ drop (Suc n) xs - else xs)" - -lemma nth_map_id: - "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs" - by (simp add: nth_map_def) - -lemma nth_map_unfold: - "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs" - by (simp add: nth_map_def) - -lemma nth_map_Nil [simp]: - "nth_map n f [] = []" - by (simp add: nth_map_def) - -lemma nth_map_zero [simp]: - "nth_map 0 f (x # xs) = f x # xs" - by (simp add: nth_map_def) - -lemma nth_map_Suc [simp]: - "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" - by (simp add: nth_map_def) - - -text {* monad operation *} - -definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where - "bind xs f = concat (map f xs)" - -lemma bind_simps [simp]: - "bind [] f = []" - "bind (x # xs) f = f x @ bind xs f" - by (simp_all add: bind_def) - -end

--- a/src/HOL/Library/More_Set.thy Tue Dec 27 15:37:33 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,284 +0,0 @@ - -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Relating (finite) sets and lists *} - -theory More_Set -imports Main More_List -begin - -lemma comp_fun_idem_remove: - "comp_fun_idem Set.remove" -proof - - have rem: "Set.remove = (\<lambda>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 = (\<lambda>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 [code_unfold_post]: - "{x \<in> A. P x} = Set.project P A" - by (simp add: project_def) - - -subsection {* Basic set operations *} - -lemma is_empty_set: - "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" - by (simp add: Set.is_empty_def null_def) - -lemma empty_set: - "{} = 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: - "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) -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 foldr_fold) -qed - -lemma minus_set: - "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) -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 foldr_fold) -qed - - -subsection {* Derived set operations *} - -lemma member: - "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" - by simp - -lemma subset_eq: - "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" - by (fact subset_eq) - -lemma subset: - "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" - by (fact less_le_not_le) - -lemma set_eq: - "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" - by (fact eq_iff) - -lemma inter: - "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" - by (auto simp add: project_def) - - -subsection {* Theorems on relations *} - -lemma product_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: - "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" - by (auto simp add: Id_on_def) - -lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" - by (simp add: finite_trancl_ntranl) - -lemma set_rel_comp: - "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: - "wf (set xs) = acyclic (set xs)" - by (simp add: wf_iff_acyclic_if_finite) - - -subsection {* Code generator setup *} - -definition coset :: "'a list \<Rightarrow> 'a set" where - [simp]: "coset xs = - set xs" - -code_datatype set coset - - -subsection {* Basic operations *} - -lemma [code]: - "x \<in> set xs \<longleftrightarrow> List.member xs x" - "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" - by (simp_all add: member_def) - -lemma [code_unfold]: - "A = {} \<longleftrightarrow> Set.is_empty A" - by (simp add: Set.is_empty_def) - -declare empty_set [code] - -declare is_empty_set [code] - -lemma UNIV_coset [code]: - "UNIV = coset []" - by simp - -lemma insert_code [code]: - "insert x (set xs) = set (List.insert x xs)" - "insert x (coset xs) = 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)" - by (simp_all add: remove_def Compl_insert) - -declare image_set [code] - -declare project_set [code] - -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 {* Derived operations *} - -declare subset_eq [code] - -declare subset [code] - - -subsection {* Functorial operations *} - -lemma inter_code [code]: - "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" - "A \<inter> coset xs = foldr Set.remove xs A" - by (simp add: inter 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 (\<lambda>x. x \<in> A) xs)" - by (auto simp add: minus_set_foldr) - -lemma union_code [code]: - "set xs \<union> A = foldr insert xs A" - "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)" - by (auto simp add: union_set_foldr) - -definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where - [simp]: "Inf = Complete_Lattices.Inf" - -hide_const (open) Inf - -lemma [code_unfold_post]: - "Inf = More_Set.Inf" - by simp - -definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where - [simp]: "Sup = Complete_Lattices.Sup" - -hide_const (open) Sup - -lemma [code_unfold_post]: - "Sup = More_Set.Sup" - by simp - -lemma Inf_code [code]: - "More_Set.Inf (set xs) = foldr inf xs top" - "More_Set.Inf (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" - by (simp_all add: Sup_set_foldr) - -lemma INF_code [code]: - "INFI (set xs) f = foldr (inf \<circ> f) xs top" - by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map) - -lemma SUP_sup [code]: - "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" - by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map) - -hide_const (open) coset - - -subsection {* Operations on relations *} - -text {* Initially contributed by Tjark Weber. *} - -declare Domain_fst [code] - -declare Range_snd [code] - -declare trans_join [code] - -declare irrefl_distinct [code] - -declare trancl_set_ntrancl [code] - -declare acyclic_irrefl [code] - -declare product_code [code] - -declare Id_on_set [code] - -declare set_rel_comp [code] - -declare wf_set [code] - -end -

--- a/src/HOL/Library/Multiset.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Dec 27 15:38:45 2011 +0100 @@ -857,6 +857,23 @@ qed qed +lemma fold_multiset_equiv: + assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" + and equiv: "multiset_of xs = multiset_of ys" + shows "fold f xs = fold f ys" +using f equiv [symmetric] proof (induct xs arbitrary: ys) + case Nil then show ?case by simp +next + case (Cons x xs) + then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) + have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" + by (rule Cons.prems(1)) (simp_all add: *) + moreover from * have "x \<in> set ys" by simp + ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) + moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) + ultimately show ?case by simp +qed + context linorder begin

--- a/src/HOL/Library/RBT_Impl.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/RBT_Impl.thy Tue Dec 27 15:38:45 2011 +0100 @@ -6,7 +6,7 @@ header {* Implementation of Red-Black Trees *} theory RBT_Impl -imports Main More_List +imports Main begin text {*

--- a/src/HOL/Library/Saturated.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Library/Saturated.thy Tue Dec 27 15:38:45 2011 +0100 @@ -215,38 +215,38 @@ begin definition - "Inf (A :: 'a sat set) = fold min top A" + "Inf (A :: 'a sat set) = Finite_Set.fold min top A" definition - "Sup (A :: 'a sat set) = fold max bot A" + "Sup (A :: 'a sat set) = Finite_Set.fold max bot A" instance proof fix x :: "'a sat" fix A :: "'a sat set" note finite moreover assume "x \<in> A" - ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf) + ultimately have "Finite_Set.fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf) then show "Inf A \<le> x" by (simp add: Inf_sat_def) next fix z :: "'a sat" fix A :: "'a sat set" note finite moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" - ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf) + ultimately have "min z top \<le> Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf) then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def) next fix x :: "'a sat" fix A :: "'a sat set" note finite moreover assume "x \<in> A" - ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup) + ultimately have "max x bot \<le> Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup) then show "x \<le> Sup A" by (simp add: Sup_sat_def) next fix z :: "'a sat" fix A :: "'a sat set" note finite moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" - ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup) + ultimately have "Finite_Set.fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup) then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique) qed

--- a/src/HOL/List.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/List.thy Tue Dec 27 15:38:45 2011 +0100 @@ -2536,68 +2536,6 @@ qed qed -lemma (in lattice) Inf_fin_set_fold [code_unfold]: - "Inf_fin (set (x # xs)) = foldl inf x xs" -proof - - interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_inf) - show ?thesis - by (simp add: Inf_fin_def fold1_set del: set.simps) -qed - -lemma (in lattice) Sup_fin_set_fold [code_unfold]: - "Sup_fin (set (x # xs)) = foldl sup x xs" -proof - - interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_sup) - show ?thesis - by (simp add: Sup_fin_def fold1_set del: set.simps) -qed - -lemma (in linorder) Min_fin_set_fold [code_unfold]: - "Min (set (x # xs)) = foldl min x xs" -proof - - interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_min) - show ?thesis - by (simp add: Min_def fold1_set del: set.simps) -qed - -lemma (in linorder) Max_fin_set_fold [code_unfold]: - "Max (set (x # xs)) = foldl max x xs" -proof - - interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact ab_semigroup_idem_mult_max) - show ?thesis - by (simp add: Max_def fold1_set del: set.simps) -qed - -lemma (in complete_lattice) Inf_set_fold [code_unfold]: - "Inf (set xs) = foldl inf top xs" -proof - - interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact comp_fun_idem_inf) - show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute) -qed - -lemma (in complete_lattice) Sup_set_fold [code_unfold]: - "Sup (set xs) = foldl sup bot xs" -proof - - interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" - by (fact comp_fun_idem_sup) - show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) -qed - -lemma (in complete_lattice) INFI_set_fold: - "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs" - unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map - by (simp add: inf_commute) - -lemma (in complete_lattice) SUPR_set_fold: - "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs" - unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map - by (simp add: sup_commute) - subsubsection {* @{text upt} *}

--- a/src/HOL/Main.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Main.thy Tue Dec 27 15:38:45 2011 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Predicate_Compile Nitpick +imports Plain Predicate_Compile Nitpick More_Set begin text {*

--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Dec 27 15:38:45 2011 +0100 @@ -9,7 +9,6 @@ "../JVM/JVMListExample" BVSpecTypeSafe JVM - "~~/src/HOL/Library/More_Set" begin text {*

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/More_List.thy Tue Dec 27 15:38:45 2011 +0100 @@ -0,0 +1,285 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Operations on lists beyond the standard List theory *} + +theory More_List +imports List +begin + +hide_const (open) Finite_Set.fold + +text {* Fold combinator with canonical argument order *} + +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where + "fold f [] = id" + | "fold f (x # xs) = fold f xs \<circ> f x" + +lemma foldl_fold: + "foldl f s xs = fold (\<lambda>x s. f s x) xs s" + by (induct xs arbitrary: s) simp_all + +lemma foldr_fold_rev: + "foldr f xs = fold f (rev xs)" + by (simp add: foldr_foldl foldl_fold fun_eq_iff) + +lemma fold_rev_conv [code_unfold]: + "fold f (rev xs) = foldr f xs" + by (simp add: foldr_fold_rev) + +lemma fold_cong [fundef_cong]: + "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) + \<Longrightarrow> fold f xs a = fold g ys b" + by (induct ys arbitrary: a b xs) simp_all + +lemma fold_id: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id" + shows "fold f xs = id" + using assms by (induct xs) simp_all + +lemma fold_commute: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" + shows "h \<circ> fold g xs = fold f xs \<circ> h" + using assms by (induct xs) (simp_all add: fun_eq_iff) + +lemma fold_commute_apply: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" + shows "h (fold g xs s) = fold f xs (h s)" +proof - + from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute) + then show ?thesis by (simp add: fun_eq_iff) +qed + +lemma fold_invariant: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s" + and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)" + shows "P (fold f xs s)" + using assms by (induct xs arbitrary: s) simp_all + +lemma fold_weak_invariant: + assumes "P s" + and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)" + shows "P (fold f xs s)" + using assms by (induct xs arbitrary: s) simp_all + +lemma fold_append [simp]: + "fold f (xs @ ys) = fold f ys \<circ> fold f xs" + by (induct xs) simp_all + +lemma fold_map [code_unfold]: + "fold g (map f xs) = fold (g o f) xs" + by (induct xs) simp_all + +lemma fold_remove1_split: + assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" + and x: "x \<in> set xs" + shows "fold f xs = fold f (remove1 x xs) \<circ> f x" + using assms by (induct xs) (auto simp add: o_assoc [symmetric]) + +lemma fold_rev: + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" + shows "fold f (rev xs) = fold f xs" +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff) + +lemma foldr_fold: + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" + shows "foldr f xs = fold f xs" + using assms unfolding foldr_fold_rev by (rule fold_rev) + +lemma fold_Cons_rev: + "fold Cons xs = append (rev xs)" + by (induct xs) simp_all + +lemma rev_conv_fold [code]: + "rev xs = fold Cons xs []" + by (simp add: fold_Cons_rev) + +lemma fold_append_concat_rev: + "fold append xss = append (concat (rev xss))" + by (induct xss) simp_all + +lemma concat_conv_foldr [code]: + "concat xss = foldr append xss []" + by (simp add: fold_append_concat_rev foldr_fold_rev) + +lemma fold_plus_listsum_rev: + "fold plus xs = plus (listsum (rev xs))" + by (induct xs) (simp_all add: add.assoc) + +lemma (in monoid_add) listsum_conv_fold [code]: + "listsum xs = fold (\<lambda>x y. y + x) xs 0" + by (auto simp add: listsum_foldl foldl_fold fun_eq_iff) + +lemma (in linorder) sort_key_conv_fold: + assumes "inj_on f (set xs)" + shows "sort_key f xs = fold (insort_key f) xs []" +proof - + have "fold (insort_key f) (rev xs) = fold (insort_key f) xs" + proof (rule fold_rev, rule ext) + fix zs + fix x y + assume "x \<in> set xs" "y \<in> set xs" + with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD) + have **: "x = y \<longleftrightarrow> y = x" by auto + show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs" + by (induct zs) (auto intro: * simp add: **) + qed + then show ?thesis by (simp add: sort_key_def foldr_fold_rev) +qed + +lemma (in linorder) sort_conv_fold: + "sort xs = fold insort xs []" + by (rule sort_key_conv_fold) simp + + +text {* @{const Finite_Set.fold} and @{const fold} *} + +lemma (in comp_fun_commute) fold_set_fold_remdups: + "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" + by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) + +lemma (in comp_fun_idem) fold_set_fold: + "Finite_Set.fold f y (set xs) = fold f xs y" + by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) + +lemma (in ab_semigroup_idem_mult) fold1_set_fold: + assumes "xs \<noteq> []" + shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" +proof - + interpret comp_fun_idem times by (fact comp_fun_idem) + from assms obtain y ys where xs: "xs = y # ys" + by (cases xs) auto + show ?thesis + proof (cases "set ys = {}") + case True with xs show ?thesis by simp + next + case False + then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" + by (simp only: finite_set fold1_eq_fold_idem) + with xs show ?thesis by (simp add: fold_set_fold mult_commute) + qed +qed + +lemma (in lattice) Inf_fin_set_fold: + "Inf_fin (set (x # xs)) = fold inf xs x" +proof - + interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_inf) + show ?thesis + by (simp add: Inf_fin_def fold1_set_fold del: set.simps) +qed + +lemma (in lattice) Inf_fin_set_foldr [code_unfold]: + "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) + +lemma (in lattice) Sup_fin_set_fold: + "Sup_fin (set (x # xs)) = fold sup xs x" +proof - + interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_sup) + show ?thesis + by (simp add: Sup_fin_def fold1_set_fold del: set.simps) +qed + +lemma (in lattice) Sup_fin_set_foldr [code_unfold]: + "Sup_fin (set (x # xs)) = foldr sup xs x" + by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in linorder) Min_fin_set_fold: + "Min (set (x # xs)) = fold min xs x" +proof - + interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_min) + show ?thesis + by (simp add: Min_def fold1_set_fold del: set.simps) +qed + +lemma (in linorder) Min_fin_set_foldr [code_unfold]: + "Min (set (x # xs)) = foldr min xs x" + by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in linorder) Max_fin_set_fold: + "Max (set (x # xs)) = fold max xs x" +proof - + interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_max) + show ?thesis + by (simp add: Max_def fold1_set_fold del: set.simps) +qed + +lemma (in linorder) Max_fin_set_foldr [code_unfold]: + "Max (set (x # xs)) = foldr max xs x" + by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in complete_lattice) Inf_set_fold: + "Inf (set xs) = fold inf xs top" +proof - + interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact comp_fun_idem_inf) + show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute) +qed + +lemma (in complete_lattice) Inf_set_foldr [code_unfold]: + "Inf (set xs) = foldr inf xs top" + by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) + +lemma (in complete_lattice) Sup_set_fold: + "Sup (set xs) = fold sup xs bot" +proof - + interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact comp_fun_idem_sup) + show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute) +qed + +lemma (in complete_lattice) Sup_set_foldr [code_unfold]: + "Sup (set xs) = foldr sup xs bot" + by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) + +lemma (in complete_lattice) INFI_set_fold: + "INFI (set xs) f = fold (inf \<circ> f) xs top" + unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. + +lemma (in complete_lattice) SUPR_set_fold: + "SUPR (set xs) f = fold (sup \<circ> f) xs bot" + unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. + + +text {* @{text nth_map} *} + +definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where + "nth_map n f xs = (if n < length xs then + take n xs @ [f (xs ! n)] @ drop (Suc n) xs + else xs)" + +lemma nth_map_id: + "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs" + by (simp add: nth_map_def) + +lemma nth_map_unfold: + "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs" + by (simp add: nth_map_def) + +lemma nth_map_Nil [simp]: + "nth_map n f [] = []" + by (simp add: nth_map_def) + +lemma nth_map_zero [simp]: + "nth_map 0 f (x # xs) = f x # xs" + by (simp add: nth_map_def) + +lemma nth_map_Suc [simp]: + "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" + by (simp add: nth_map_def) + + +text {* monad operation *} + +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where + "bind xs f = concat (map f xs)" + +lemma bind_simps [simp]: + "bind [] f = []" + "bind (x # xs) f = f x @ bind xs f" + by (simp_all add: bind_def) + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/More_Set.thy Tue Dec 27 15:38:45 2011 +0100 @@ -0,0 +1,284 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Relating (finite) sets and lists *} + +theory More_Set +imports More_List +begin + +lemma comp_fun_idem_remove: + "comp_fun_idem Set.remove" +proof - + have rem: "Set.remove = (\<lambda>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 = (\<lambda>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 [code_unfold_post]: + "{x \<in> A. P x} = Set.project P A" + by (simp add: project_def) + + +subsection {* Basic set operations *} + +lemma is_empty_set: + "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" + by (simp add: Set.is_empty_def null_def) + +lemma empty_set: + "{} = 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: + "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 foldr_fold) +qed + +lemma minus_set: + "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 foldr_fold) +qed + + +subsection {* Derived set operations *} + +lemma member: + "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" + by simp + +lemma subset_eq: + "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" + by (fact subset_eq) + +lemma subset: + "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" + by (fact less_le_not_le) + +lemma set_eq: + "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" + by (fact eq_iff) + +lemma inter: + "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" + by (auto simp add: project_def) + + +subsection {* Theorems on relations *} + +lemma product_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: + "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" + by (auto simp add: Id_on_def) + +lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" + by (simp add: finite_trancl_ntranl) + +lemma set_rel_comp: + "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: + "wf (set xs) = acyclic (set xs)" + by (simp add: wf_iff_acyclic_if_finite) + + +subsection {* Code generator setup *} + +definition coset :: "'a list \<Rightarrow> 'a set" where + [simp]: "coset xs = - set xs" + +code_datatype set coset + + +subsection {* Basic operations *} + +lemma [code]: + "x \<in> set xs \<longleftrightarrow> List.member xs x" + "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" + by (simp_all add: member_def) + +lemma [code_unfold]: + "A = {} \<longleftrightarrow> Set.is_empty A" + by (simp add: Set.is_empty_def) + +declare empty_set [code] + +declare is_empty_set [code] + +lemma UNIV_coset [code]: + "UNIV = coset []" + by simp + +lemma insert_code [code]: + "insert x (set xs) = set (List.insert x xs)" + "insert x (coset xs) = 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)" + by (simp_all add: remove_def Compl_insert) + +declare image_set [code] + +declare project_set [code] + +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 {* Derived operations *} + +declare subset_eq [code] + +declare subset [code] + + +subsection {* Functorial operations *} + +lemma inter_code [code]: + "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" + "A \<inter> coset xs = foldr Set.remove xs A" + by (simp add: inter 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 (\<lambda>x. x \<in> A) xs)" + by (auto simp add: minus_set_foldr) + +lemma union_code [code]: + "set xs \<union> A = foldr insert xs A" + "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)" + by (auto simp add: union_set_foldr) + +definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where + [simp]: "Inf = Complete_Lattices.Inf" + +hide_const (open) Inf + +lemma [code_unfold_post]: + "Inf = More_Set.Inf" + by simp + +definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where + [simp]: "Sup = Complete_Lattices.Sup" + +hide_const (open) Sup + +lemma [code_unfold_post]: + "Sup = More_Set.Sup" + by simp + +lemma Inf_code [code]: + "More_Set.Inf (set xs) = foldr inf xs top" + "More_Set.Inf (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" + by (simp_all add: Sup_set_foldr) + +lemma INF_code [code]: + "INFI (set xs) f = foldr (inf \<circ> f) xs top" + by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map) + +lemma SUP_sup [code]: + "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" + by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map) + +hide_const (open) coset + + +subsection {* Operations on relations *} + +text {* Initially contributed by Tjark Weber. *} + +declare Domain_fst [code] + +declare Range_snd [code] + +declare trans_join [code] + +declare irrefl_distinct [code] + +declare trancl_set_ntrancl [code] + +declare acyclic_irrefl [code] + +declare product_code [code] + +declare Id_on_set [code] + +declare set_rel_comp [code] + +declare wf_set [code] + +end +

--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 27 15:38:45 2011 +0100 @@ -1814,7 +1814,7 @@ unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}" -definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)" +definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)" definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)" lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto

--- a/src/HOL/Quotient_Examples/DList.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Quotient_Examples/DList.thy Tue Dec 27 15:38:45 2011 +0100 @@ -8,7 +8,7 @@ header {* Lists with distinct elements *} theory DList -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" +imports "~~/src/HOL/Library/Quotient_List" begin text {* Some facts about lists *}

--- a/src/HOL/Quotient_Examples/FSet.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Dec 27 15:38:45 2011 +0100 @@ -6,7 +6,7 @@ *) theory FSet -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" +imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List" begin text {*

--- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Tue Dec 27 15:38:45 2011 +0100 @@ -5,7 +5,7 @@ header {* A variant of theory Cset from Library, defined as a quotient *} theory Quotient_Cset -imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax" +imports Main "~~/src/HOL/Library/Quotient_Syntax" begin subsection {* Lifting *}

--- a/src/HOL/ex/Quickcheck_Examples.thy Tue Dec 27 15:37:33 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Examples.thy Tue Dec 27 15:38:45 2011 +0100 @@ -6,7 +6,7 @@ header {* Examples for the 'quickcheck' command *} theory Quickcheck_Examples -imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/More_Set" +imports Complex_Main "~~/src/HOL/Library/Dlist" begin text {*