1.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6  theory Abs_Int1_ivl
     1.7 -imports Abs_Int1 Abs_Int_Tests "~~/src/HOL/Library/More_Set"
     1.8 +imports Abs_Int1 Abs_Int_Tests
     1.9  begin
    1.10  
    1.11  subsection "Interval Analysis"

     2.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (* Author: Tobias Nipkow *)
     2.5  
     2.6  theory Abs_Int_den1_ivl
     2.7 -imports Abs_Int_den1 "~~/src/HOL/Library/More_Set"
     2.8 +imports Abs_Int_den1
     2.9  begin
    2.10  
    2.11  subsection "Interval Analysis"

     3.1 --- a/src/HOL/IsaMakefile	Mon Dec 26 22:17:10 2011 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Dec 26 22:17:10 2011 +0100
     3.3 @@ -286,6 +286,8 @@
     3.4    List.thy \
     3.5    Main.thy \
     3.6    Map.thy \
     3.7 +  More_List.thy \
     3.8 +  More_Set.thy \
     3.9    Nat_Numeral.thy \
    3.10    Nat_Transfer.thy \
    3.11    New_DSequence.thy \
    3.12 @@ -458,7 +460,7 @@
    3.13    Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
    3.14    Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy	\
    3.15    Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
    3.16 -  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
    3.17 +  Library/Monad_Syntax.thy						\
    3.18    Library/Multiset.thy Library/Nat_Bijection.thy			\
    3.19    Library/Numeral_Type.thy Library/Old_Recdef.thy			\
    3.20    Library/OptionalSugar.thy Library/Order_Relation.thy			\

     4.1 --- a/src/HOL/Library/AList_Impl.thy	Mon Dec 26 22:17:10 2011 +0100
     4.2 +++ b/src/HOL/Library/AList_Impl.thy	Mon Dec 26 22:17:10 2011 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Implementation of Association Lists *}
     4.5  
     4.6  theory AList_Impl
     4.7 -imports Main More_List
     4.8 +imports Main
     4.9  begin
    4.10  
    4.11  text {*

     5.1 --- a/src/HOL/Library/Cset.thy	Mon Dec 26 22:17:10 2011 +0100
     5.2 +++ b/src/HOL/Library/Cset.thy	Mon Dec 26 22:17:10 2011 +0100
     5.3 @@ -4,7 +4,7 @@
     5.4  header {* A dedicated set type which is executable on its finite part *}
     5.5  
     5.6  theory Cset
     5.7 -imports More_Set More_List
     5.8 +imports Main
     5.9  begin
    5.10  
    5.11  subsection {* Lifting *}

     6.1 --- a/src/HOL/Library/Dlist.thy	Mon Dec 26 22:17:10 2011 +0100
     6.2 +++ b/src/HOL/Library/Dlist.thy	Mon Dec 26 22:17:10 2011 +0100
     6.3 @@ -3,7 +3,7 @@
     6.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     6.5  
     6.6  theory Dlist
     6.7 -imports Main More_List
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  subsection {* The type of distinct lists *}

     7.1 --- a/src/HOL/Library/Library.thy	Mon Dec 26 22:17:10 2011 +0100
     7.2 +++ b/src/HOL/Library/Library.thy	Mon Dec 26 22:17:10 2011 +0100
     7.3 @@ -33,7 +33,6 @@
     7.4    Kleene_Algebra
     7.5    Mapping
     7.6    Monad_Syntax
     7.7 -  More_List
     7.8    Multiset
     7.9    Numeral_Type
    7.10    Old_Recdef

     8.1 --- a/src/HOL/Library/Monad_Syntax.thy	Mon Dec 26 22:17:10 2011 +0100
     8.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Mon Dec 26 22:17:10 2011 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* Monad notation for arbitrary types *}
     8.5  
     8.6  theory Monad_Syntax
     8.7 -imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
     8.8 +imports Main "~~/src/Tools/Adhoc_Overloading"
     8.9  begin
    8.10  
    8.11  text {*

     9.1 --- a/src/HOL/Library/More_List.thy	Mon Dec 26 22:17:10 2011 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,312 +0,0 @@
     9.4 -(* Author:  Florian Haftmann, TU Muenchen *)
     9.5 -
     9.6 -header {* Operations on lists beyond the standard List theory *}
     9.7 -
     9.8 -theory More_List
     9.9 -imports Main Multiset
    9.10 -begin
    9.11 -
    9.12 -hide_const (open) Finite_Set.fold
    9.13 -
    9.14 -text {* Repairing code generator setup *}
    9.15 -
    9.16 -declare (in lattice) Inf_fin_set_fold [code_unfold del]
    9.17 -declare (in lattice) Sup_fin_set_fold [code_unfold del]
    9.18 -declare (in linorder) Min_fin_set_fold [code_unfold del]
    9.19 -declare (in linorder) Max_fin_set_fold [code_unfold del]
    9.20 -declare (in complete_lattice) Inf_set_fold [code_unfold del]
    9.21 -declare (in complete_lattice) Sup_set_fold [code_unfold del]
    9.22 -
    9.23 -
    9.24 -text {* Fold combinator with canonical argument order *}
    9.25 -
    9.26 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    9.27 -    "fold f [] = id"
    9.28 -  | "fold f (x # xs) = fold f xs \<circ> f x"
    9.29 -
    9.30 -lemma foldl_fold:
    9.31 -  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
    9.32 -  by (induct xs arbitrary: s) simp_all
    9.33 -
    9.34 -lemma foldr_fold_rev:
    9.35 -  "foldr f xs = fold f (rev xs)"
    9.36 -  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
    9.37 -
    9.38 -lemma fold_rev_conv [code_unfold]:
    9.39 -  "fold f (rev xs) = foldr f xs"
    9.40 -  by (simp add: foldr_fold_rev)
    9.41 -  
    9.42 -lemma fold_cong [fundef_cong]:
    9.43 -  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
    9.44 -    \<Longrightarrow> fold f xs a = fold g ys b"
    9.45 -  by (induct ys arbitrary: a b xs) simp_all
    9.46 -
    9.47 -lemma fold_id:
    9.48 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
    9.49 -  shows "fold f xs = id"
    9.50 -  using assms by (induct xs) simp_all
    9.51 -
    9.52 -lemma fold_commute:
    9.53 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    9.54 -  shows "h \<circ> fold g xs = fold f xs \<circ> h"
    9.55 -  using assms by (induct xs) (simp_all add: fun_eq_iff)
    9.56 -
    9.57 -lemma fold_commute_apply:
    9.58 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    9.59 -  shows "h (fold g xs s) = fold f xs (h s)"
    9.60 -proof -
    9.61 -  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
    9.62 -  then show ?thesis by (simp add: fun_eq_iff)
    9.63 -qed
    9.64 -
    9.65 -lemma fold_invariant: 
    9.66 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
    9.67 -    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    9.68 -  shows "P (fold f xs s)"
    9.69 -  using assms by (induct xs arbitrary: s) simp_all
    9.70 -
    9.71 -lemma fold_weak_invariant:
    9.72 -  assumes "P s"
    9.73 -    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    9.74 -  shows "P (fold f xs s)"
    9.75 -  using assms by (induct xs arbitrary: s) simp_all
    9.76 -
    9.77 -lemma fold_append [simp]:
    9.78 -  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
    9.79 -  by (induct xs) simp_all
    9.80 -
    9.81 -lemma fold_map [code_unfold]:
    9.82 -  "fold g (map f xs) = fold (g o f) xs"
    9.83 -  by (induct xs) simp_all
    9.84 -
    9.85 -lemma fold_remove1_split:
    9.86 -  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"
    9.87 -    and x: "x \<in> set xs"
    9.88 -  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
    9.89 -  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
    9.90 -
    9.91 -lemma fold_multiset_equiv:
    9.92 -  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"
    9.93 -    and equiv: "multiset_of xs = multiset_of ys"
    9.94 -  shows "fold f xs = fold f ys"
    9.95 -using f equiv [symmetric] proof (induct xs arbitrary: ys)
    9.96 -  case Nil then show ?case by simp
    9.97 -next
    9.98 -  case (Cons x xs)
    9.99 -  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
   9.100 -  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
   9.101 -    by (rule Cons.prems(1)) (simp_all add: *)
   9.102 -  moreover from * have "x \<in> set ys" by simp
   9.103 -  ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   9.104 -  moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   9.105 -  ultimately show ?case by simp
   9.106 -qed
   9.107 -
   9.108 -lemma fold_rev:
   9.109 -  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   9.110 -  shows "fold f (rev xs) = fold f xs"
   9.111 -  by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set)
   9.112 -
   9.113 -lemma foldr_fold:
   9.114 -  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   9.115 -  shows "foldr f xs = fold f xs"
   9.116 -  using assms unfolding foldr_fold_rev by (rule fold_rev)
   9.117 -
   9.118 -lemma fold_Cons_rev:
   9.119 -  "fold Cons xs = append (rev xs)"
   9.120 -  by (induct xs) simp_all
   9.121 -
   9.122 -lemma rev_conv_fold [code]:
   9.123 -  "rev xs = fold Cons xs []"
   9.124 -  by (simp add: fold_Cons_rev)
   9.125 -
   9.126 -lemma fold_append_concat_rev:
   9.127 -  "fold append xss = append (concat (rev xss))"
   9.128 -  by (induct xss) simp_all
   9.129 -
   9.130 -lemma concat_conv_foldr [code]:
   9.131 -  "concat xss = foldr append xss []"
   9.132 -  by (simp add: fold_append_concat_rev foldr_fold_rev)
   9.133 -
   9.134 -lemma fold_plus_listsum_rev:
   9.135 -  "fold plus xs = plus (listsum (rev xs))"
   9.136 -  by (induct xs) (simp_all add: add.assoc)
   9.137 -
   9.138 -lemma (in monoid_add) listsum_conv_fold [code]:
   9.139 -  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
   9.140 -  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
   9.141 -
   9.142 -lemma (in linorder) sort_key_conv_fold:
   9.143 -  assumes "inj_on f (set xs)"
   9.144 -  shows "sort_key f xs = fold (insort_key f) xs []"
   9.145 -proof -
   9.146 -  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
   9.147 -  proof (rule fold_rev, rule ext)
   9.148 -    fix zs
   9.149 -    fix x y
   9.150 -    assume "x \<in> set xs" "y \<in> set xs"
   9.151 -    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
   9.152 -    have **: "x = y \<longleftrightarrow> y = x" by auto
   9.153 -    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   9.154 -      by (induct zs) (auto intro: * simp add: **)
   9.155 -  qed
   9.156 -  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
   9.157 -qed
   9.158 -
   9.159 -lemma (in linorder) sort_conv_fold:
   9.160 -  "sort xs = fold insort xs []"
   9.161 -  by (rule sort_key_conv_fold) simp
   9.162 -
   9.163 -
   9.164 -text {* @{const Finite_Set.fold} and @{const fold} *}
   9.165 -
   9.166 -lemma (in comp_fun_commute) fold_set_remdups:
   9.167 -  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   9.168 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
   9.169 -
   9.170 -lemma (in comp_fun_idem) fold_set:
   9.171 -  "Finite_Set.fold f y (set xs) = fold f xs y"
   9.172 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
   9.173 -
   9.174 -lemma (in ab_semigroup_idem_mult) fold1_set:
   9.175 -  assumes "xs \<noteq> []"
   9.176 -  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
   9.177 -proof -
   9.178 -  interpret comp_fun_idem times by (fact comp_fun_idem)
   9.179 -  from assms obtain y ys where xs: "xs = y # ys"
   9.180 -    by (cases xs) auto
   9.181 -  show ?thesis
   9.182 -  proof (cases "set ys = {}")
   9.183 -    case True with xs show ?thesis by simp
   9.184 -  next
   9.185 -    case False
   9.186 -    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
   9.187 -      by (simp only: finite_set fold1_eq_fold_idem)
   9.188 -    with xs show ?thesis by (simp add: fold_set mult_commute)
   9.189 -  qed
   9.190 -qed
   9.191 -
   9.192 -lemma (in lattice) Inf_fin_set_fold:
   9.193 -  "Inf_fin (set (x # xs)) = fold inf xs x"
   9.194 -proof -
   9.195 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.196 -    by (fact ab_semigroup_idem_mult_inf)
   9.197 -  show ?thesis
   9.198 -    by (simp add: Inf_fin_def fold1_set del: set.simps)
   9.199 -qed
   9.200 -
   9.201 -lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
   9.202 -  "Inf_fin (set (x # xs)) = foldr inf xs x"
   9.203 -  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.204 -
   9.205 -lemma (in lattice) Sup_fin_set_fold:
   9.206 -  "Sup_fin (set (x # xs)) = fold sup xs x"
   9.207 -proof -
   9.208 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.209 -    by (fact ab_semigroup_idem_mult_sup)
   9.210 -  show ?thesis
   9.211 -    by (simp add: Sup_fin_def fold1_set del: set.simps)
   9.212 -qed
   9.213 -
   9.214 -lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
   9.215 -  "Sup_fin (set (x # xs)) = foldr sup xs x"
   9.216 -  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.217 -
   9.218 -lemma (in linorder) Min_fin_set_fold:
   9.219 -  "Min (set (x # xs)) = fold min xs x"
   9.220 -proof -
   9.221 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.222 -    by (fact ab_semigroup_idem_mult_min)
   9.223 -  show ?thesis
   9.224 -    by (simp add: Min_def fold1_set del: set.simps)
   9.225 -qed
   9.226 -
   9.227 -lemma (in linorder) Min_fin_set_foldr [code_unfold]:
   9.228 -  "Min (set (x # xs)) = foldr min xs x"
   9.229 -  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.230 -
   9.231 -lemma (in linorder) Max_fin_set_fold:
   9.232 -  "Max (set (x # xs)) = fold max xs x"
   9.233 -proof -
   9.234 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.235 -    by (fact ab_semigroup_idem_mult_max)
   9.236 -  show ?thesis
   9.237 -    by (simp add: Max_def fold1_set del: set.simps)
   9.238 -qed
   9.239 -
   9.240 -lemma (in linorder) Max_fin_set_foldr [code_unfold]:
   9.241 -  "Max (set (x # xs)) = foldr max xs x"
   9.242 -  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.243 -
   9.244 -lemma (in complete_lattice) Inf_set_fold:
   9.245 -  "Inf (set xs) = fold inf xs top"
   9.246 -proof -
   9.247 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.248 -    by (fact comp_fun_idem_inf)
   9.249 -  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
   9.250 -qed
   9.251 -
   9.252 -lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
   9.253 -  "Inf (set xs) = foldr inf xs top"
   9.254 -  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
   9.255 -
   9.256 -lemma (in complete_lattice) Sup_set_fold:
   9.257 -  "Sup (set xs) = fold sup xs bot"
   9.258 -proof -
   9.259 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.260 -    by (fact comp_fun_idem_sup)
   9.261 -  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
   9.262 -qed
   9.263 -
   9.264 -lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
   9.265 -  "Sup (set xs) = foldr sup xs bot"
   9.266 -  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   9.267 -
   9.268 -lemma (in complete_lattice) INFI_set_fold:
   9.269 -  "INFI (set xs) f = fold (inf \<circ> f) xs top"
   9.270 -  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   9.271 -
   9.272 -lemma (in complete_lattice) SUPR_set_fold:
   9.273 -  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   9.274 -  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   9.275 -
   9.276 -
   9.277 -text {* @{text nth_map} *}
   9.278 -
   9.279 -definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   9.280 -  "nth_map n f xs = (if n < length xs then
   9.281 -       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
   9.282 -     else xs)"
   9.283 -
   9.284 -lemma nth_map_id:
   9.285 -  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
   9.286 -  by (simp add: nth_map_def)
   9.287 -
   9.288 -lemma nth_map_unfold:
   9.289 -  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
   9.290 -  by (simp add: nth_map_def)
   9.291 -
   9.292 -lemma nth_map_Nil [simp]:
   9.293 -  "nth_map n f [] = []"
   9.294 -  by (simp add: nth_map_def)
   9.295 -
   9.296 -lemma nth_map_zero [simp]:
   9.297 -  "nth_map 0 f (x # xs) = f x # xs"
   9.298 -  by (simp add: nth_map_def)
   9.299 -
   9.300 -lemma nth_map_Suc [simp]:
   9.301 -  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
   9.302 -  by (simp add: nth_map_def)
   9.303 -
   9.304 -
   9.305 -text {* monad operation *}
   9.306 -
   9.307 -definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   9.308 -  "bind xs f = concat (map f xs)"
   9.309 -
   9.310 -lemma bind_simps [simp]:
   9.311 -  "bind [] f = []"
   9.312 -  "bind (x # xs) f = f x @ bind xs f"
   9.313 -  by (simp_all add: bind_def)
   9.314 -
   9.315 -end

    10.1 --- a/src/HOL/Library/More_Set.thy	Mon Dec 26 22:17:10 2011 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,284 +0,0 @@
    10.4 -
    10.5 -(* Author: Florian Haftmann, TU Muenchen *)
    10.6 -
    10.7 -header {* Relating (finite) sets and lists *}
    10.8 -
    10.9 -theory More_Set
   10.10 -imports Main More_List
   10.11 -begin
   10.12 -
   10.13 -lemma comp_fun_idem_remove:
   10.14 -  "comp_fun_idem Set.remove"
   10.15 -proof -
   10.16 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   10.17 -  show ?thesis by (simp only: comp_fun_idem_remove rem)
   10.18 -qed
   10.19 -
   10.20 -lemma minus_fold_remove:
   10.21 -  assumes "finite A"
   10.22 -  shows "B - A = Finite_Set.fold Set.remove B A"
   10.23 -proof -
   10.24 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   10.25 -  show ?thesis by (simp only: rem assms minus_fold_remove)
   10.26 -qed
   10.27 -
   10.28 -lemma bounded_Collect_code [code_unfold_post]:
   10.29 -  "{x \<in> A. P x} = Set.project P A"
   10.30 -  by (simp add: project_def)
   10.31 -
   10.32 -
   10.33 -subsection {* Basic set operations *}
   10.34 -
   10.35 -lemma is_empty_set:
   10.36 -  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
   10.37 -  by (simp add: Set.is_empty_def null_def)
   10.38 -
   10.39 -lemma empty_set:
   10.40 -  "{} = set []"
   10.41 -  by simp
   10.42 -
   10.43 -lemma insert_set_compl:
   10.44 -  "insert x (- set xs) = - set (removeAll x xs)"
   10.45 -  by auto
   10.46 -
   10.47 -lemma remove_set_compl:
   10.48 -  "Set.remove x (- set xs) = - set (List.insert x xs)"
   10.49 -  by (auto simp add: remove_def List.insert_def)
   10.50 -
   10.51 -lemma image_set:
   10.52 -  "image f (set xs) = set (map f xs)"
   10.53 -  by simp
   10.54 -
   10.55 -lemma project_set:
   10.56 -  "Set.project P (set xs) = set (filter P xs)"
   10.57 -  by (auto simp add: project_def)
   10.58 -
   10.59 -
   10.60 -subsection {* Functorial set operations *}
   10.61 -
   10.62 -lemma union_set:
   10.63 -  "set xs \<union> A = fold Set.insert xs A"
   10.64 -proof -
   10.65 -  interpret comp_fun_idem Set.insert
   10.66 -    by (fact comp_fun_idem_insert)
   10.67 -  show ?thesis by (simp add: union_fold_insert fold_set)
   10.68 -qed
   10.69 -
   10.70 -lemma union_set_foldr:
   10.71 -  "set xs \<union> A = foldr Set.insert xs A"
   10.72 -proof -
   10.73 -  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
   10.74 -    by auto
   10.75 -  then show ?thesis by (simp add: union_set foldr_fold)
   10.76 -qed
   10.77 -
   10.78 -lemma minus_set:
   10.79 -  "A - set xs = fold Set.remove xs A"
   10.80 -proof -
   10.81 -  interpret comp_fun_idem Set.remove
   10.82 -    by (fact comp_fun_idem_remove)
   10.83 -  show ?thesis
   10.84 -    by (simp add: minus_fold_remove [of _ A] fold_set)
   10.85 -qed
   10.86 -
   10.87 -lemma minus_set_foldr:
   10.88 -  "A - set xs = foldr Set.remove xs A"
   10.89 -proof -
   10.90 -  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   10.91 -    by (auto simp add: remove_def)
   10.92 -  then show ?thesis by (simp add: minus_set foldr_fold)
   10.93 -qed
   10.94 -
   10.95 -
   10.96 -subsection {* Derived set operations *}
   10.97 -
   10.98 -lemma member:
   10.99 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
  10.100 -  by simp
  10.101 -
  10.102 -lemma subset_eq:
  10.103 -  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  10.104 -  by (fact subset_eq)
  10.105 -
  10.106 -lemma subset:
  10.107 -  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
  10.108 -  by (fact less_le_not_le)
  10.109 -
  10.110 -lemma set_eq:
  10.111 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  10.112 -  by (fact eq_iff)
  10.113 -
  10.114 -lemma inter:
  10.115 -  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
  10.116 -  by (auto simp add: project_def)
  10.117 -
  10.118 -
  10.119 -subsection {* Theorems on relations *}
  10.120 -
  10.121 -lemma product_code:
  10.122 -  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
  10.123 -  by (auto simp add: Product_Type.product_def)
  10.124 -
  10.125 -lemma Id_on_set:
  10.126 -  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
  10.127 -  by (auto simp add: Id_on_def)
  10.128 -
  10.129 -lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
  10.130 -  by (simp add: finite_trancl_ntranl)
  10.131 -
  10.132 -lemma set_rel_comp:
  10.133 -  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
  10.134 -  by (auto simp add: Bex_def)
  10.135 -
  10.136 -lemma wf_set:
  10.137 -  "wf (set xs) = acyclic (set xs)"
  10.138 -  by (simp add: wf_iff_acyclic_if_finite)
  10.139 -
  10.140 -
  10.141 -subsection {* Code generator setup *}
  10.142 -
  10.143 -definition coset :: "'a list \<Rightarrow> 'a set" where
  10.144 -  [simp]: "coset xs = - set xs"
  10.145 -
  10.146 -code_datatype set coset
  10.147 -
  10.148 -
  10.149 -subsection {* Basic operations *}
  10.150 -
  10.151 -lemma [code]:
  10.152 -  "x \<in> set xs \<longleftrightarrow> List.member xs x"
  10.153 -  "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
  10.154 -  by (simp_all add: member_def)
  10.155 -
  10.156 -lemma [code_unfold]:
  10.157 -  "A = {} \<longleftrightarrow> Set.is_empty A"
  10.158 -  by (simp add: Set.is_empty_def)
  10.159 -
  10.160 -declare empty_set [code]
  10.161 -
  10.162 -declare is_empty_set [code]
  10.163 -
  10.164 -lemma UNIV_coset [code]:
  10.165 -  "UNIV = coset []"
  10.166 -  by simp
  10.167 -
  10.168 -lemma insert_code [code]:
  10.169 -  "insert x (set xs) = set (List.insert x xs)"
  10.170 -  "insert x (coset xs) = coset (removeAll x xs)"
  10.171 -  by simp_all
  10.172 -
  10.173 -lemma remove_code [code]:
  10.174 -  "Set.remove x (set xs) = set (removeAll x xs)"
  10.175 -  "Set.remove x (coset xs) = coset (List.insert x xs)"
  10.176 -  by (simp_all add: remove_def Compl_insert)
  10.177 -
  10.178 -declare image_set [code]
  10.179 -
  10.180 -declare project_set [code]
  10.181 -
  10.182 -lemma Ball_set [code]:
  10.183 -  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  10.184 -  by (simp add: list_all_iff)
  10.185 -
  10.186 -lemma Bex_set [code]:
  10.187 -  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  10.188 -  by (simp add: list_ex_iff)
  10.189 -
  10.190 -lemma card_set [code]:
  10.191 -  "card (set xs) = length (remdups xs)"
  10.192 -proof -
  10.193 -  have "card (set (remdups xs)) = length (remdups xs)"
  10.194 -    by (rule distinct_card) simp
  10.195 -  then show ?thesis by simp
  10.196 -qed
  10.197 -
  10.198 -
  10.199 -subsection {* Derived operations *}
  10.200 -
  10.201 -declare subset_eq [code]
  10.202 -
  10.203 -declare subset [code]
  10.204 -
  10.205 -
  10.206 -subsection {* Functorial operations *}
  10.207 -
  10.208 -lemma inter_code [code]:
  10.209 -  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  10.210 -  "A \<inter> coset xs = foldr Set.remove xs A"
  10.211 -  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
  10.212 -
  10.213 -lemma subtract_code [code]:
  10.214 -  "A - set xs = foldr Set.remove xs A"
  10.215 -  "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  10.216 -  by (auto simp add: minus_set_foldr)
  10.217 -
  10.218 -lemma union_code [code]:
  10.219 -  "set xs \<union> A = foldr insert xs A"
  10.220 -  "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
  10.221 -  by (auto simp add: union_set_foldr)
  10.222 -
  10.223 -definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
  10.224 -  [simp]: "Inf = Complete_Lattices.Inf"
  10.225 -
  10.226 -hide_const (open) Inf
  10.227 -
  10.228 -lemma [code_unfold_post]:
  10.229 -  "Inf = More_Set.Inf"
  10.230 -  by simp
  10.231 -
  10.232 -definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
  10.233 -  [simp]: "Sup = Complete_Lattices.Sup"
  10.234 -
  10.235 -hide_const (open) Sup
  10.236 -
  10.237 -lemma [code_unfold_post]:
  10.238 -  "Sup = More_Set.Sup"
  10.239 -  by simp
  10.240 -
  10.241 -lemma Inf_code [code]:
  10.242 -  "More_Set.Inf (set xs) = foldr inf xs top"
  10.243 -  "More_Set.Inf (coset []) = bot"
  10.244 -  by (simp_all add: Inf_set_foldr)
  10.245 -
  10.246 -lemma Sup_sup [code]:
  10.247 -  "More_Set.Sup (set xs) = foldr sup xs bot"
  10.248 -  "More_Set.Sup (coset []) = top"
  10.249 -  by (simp_all add: Sup_set_foldr)
  10.250 -
  10.251 -lemma INF_code [code]:
  10.252 -  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
  10.253 -  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
  10.254 -
  10.255 -lemma SUP_sup [code]:
  10.256 -  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
  10.257 -  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
  10.258 -
  10.259 -hide_const (open) coset
  10.260 -
  10.261 -
  10.262 -subsection {* Operations on relations *}
  10.263 -
  10.264 -text {* Initially contributed by Tjark Weber. *}
  10.265 -
  10.266 -declare Domain_fst [code]
  10.267 -
  10.268 -declare Range_snd [code]
  10.269 -
  10.270 -declare trans_join [code]
  10.271 -
  10.272 -declare irrefl_distinct [code]
  10.273 -
  10.274 -declare trancl_set_ntrancl [code]
  10.275 -
  10.276 -declare acyclic_irrefl [code]
  10.277 -
  10.278 -declare product_code [code]
  10.279 -
  10.280 -declare Id_on_set [code]
  10.281 -
  10.282 -declare set_rel_comp [code]
  10.283 -
  10.284 -declare wf_set [code]
  10.285 -
  10.286 -end
  10.287 -

    11.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Dec 26 22:17:10 2011 +0100
    11.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Dec 26 22:17:10 2011 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Implementation of Red-Black Trees *}
    11.5  
    11.6  theory RBT_Impl
    11.7 -imports Main More_List
    11.8 +imports Main
    11.9  begin
   11.10  
   11.11  text {*

    12.1 --- a/src/HOL/Main.thy	Mon Dec 26 22:17:10 2011 +0100
    12.2 +++ b/src/HOL/Main.thy	Mon Dec 26 22:17:10 2011 +0100
    12.3 @@ -1,7 +1,7 @@
    12.4  header {* Main HOL *}
    12.5  
    12.6  theory Main
    12.7 -imports Plain Predicate_Compile Nitpick
    12.8 +imports Plain Predicate_Compile Nitpick More_Set
    12.9  begin
   12.10  
   12.11  text {*

    13.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 22:17:10 2011 +0100
    13.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 22:17:10 2011 +0100
    13.3 @@ -9,7 +9,6 @@
    13.4    "../JVM/JVMListExample"
    13.5    BVSpecTypeSafe
    13.6    JVM
    13.7 -  "~~/src/HOL/Library/More_Set"
    13.8  begin
    13.9  
   13.10  text {*

    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/More_List.thy	Mon Dec 26 22:17:10 2011 +0100
    14.3 @@ -0,0 +1,295 @@
    14.4 +(* Author:  Florian Haftmann, TU Muenchen *)
    14.5 +
    14.6 +header {* Operations on lists beyond the standard List theory *}
    14.7 +
    14.8 +theory More_List
    14.9 +imports List
   14.10 +begin
   14.11 +
   14.12 +hide_const (open) Finite_Set.fold
   14.13 +
   14.14 +text {* Repairing code generator setup *}
   14.15 +
   14.16 +declare (in lattice) Inf_fin_set_fold [code_unfold del]
   14.17 +declare (in lattice) Sup_fin_set_fold [code_unfold del]
   14.18 +declare (in linorder) Min_fin_set_fold [code_unfold del]
   14.19 +declare (in linorder) Max_fin_set_fold [code_unfold del]
   14.20 +declare (in complete_lattice) Inf_set_fold [code_unfold del]
   14.21 +declare (in complete_lattice) Sup_set_fold [code_unfold del]
   14.22 +
   14.23 +
   14.24 +text {* Fold combinator with canonical argument order *}
   14.25 +
   14.26 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   14.27 +    "fold f [] = id"
   14.28 +  | "fold f (x # xs) = fold f xs \<circ> f x"
   14.29 +
   14.30 +lemma foldl_fold:
   14.31 +  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
   14.32 +  by (induct xs arbitrary: s) simp_all
   14.33 +
   14.34 +lemma foldr_fold_rev:
   14.35 +  "foldr f xs = fold f (rev xs)"
   14.36 +  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
   14.37 +
   14.38 +lemma fold_rev_conv [code_unfold]:
   14.39 +  "fold f (rev xs) = foldr f xs"
   14.40 +  by (simp add: foldr_fold_rev)
   14.41 +  
   14.42 +lemma fold_cong [fundef_cong]:
   14.43 +  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   14.44 +    \<Longrightarrow> fold f xs a = fold g ys b"
   14.45 +  by (induct ys arbitrary: a b xs) simp_all
   14.46 +
   14.47 +lemma fold_id:
   14.48 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
   14.49 +  shows "fold f xs = id"
   14.50 +  using assms by (induct xs) simp_all
   14.51 +
   14.52 +lemma fold_commute:
   14.53 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   14.54 +  shows "h \<circ> fold g xs = fold f xs \<circ> h"
   14.55 +  using assms by (induct xs) (simp_all add: fun_eq_iff)
   14.56 +
   14.57 +lemma fold_commute_apply:
   14.58 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   14.59 +  shows "h (fold g xs s) = fold f xs (h s)"
   14.60 +proof -
   14.61 +  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
   14.62 +  then show ?thesis by (simp add: fun_eq_iff)
   14.63 +qed
   14.64 +
   14.65 +lemma fold_invariant: 
   14.66 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   14.67 +    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   14.68 +  shows "P (fold f xs s)"
   14.69 +  using assms by (induct xs arbitrary: s) simp_all
   14.70 +
   14.71 +lemma fold_weak_invariant:
   14.72 +  assumes "P s"
   14.73 +    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   14.74 +  shows "P (fold f xs s)"
   14.75 +  using assms by (induct xs arbitrary: s) simp_all
   14.76 +
   14.77 +lemma fold_append [simp]:
   14.78 +  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
   14.79 +  by (induct xs) simp_all
   14.80 +
   14.81 +lemma fold_map [code_unfold]:
   14.82 +  "fold g (map f xs) = fold (g o f) xs"
   14.83 +  by (induct xs) simp_all
   14.84 +
   14.85 +lemma fold_remove1_split:
   14.86 +  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"
   14.87 +    and x: "x \<in> set xs"
   14.88 +  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
   14.89 +  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
   14.90 +
   14.91 +lemma fold_rev:
   14.92 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   14.93 +  shows "fold f (rev xs) = fold f xs"
   14.94 +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
   14.95 +
   14.96 +lemma foldr_fold:
   14.97 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   14.98 +  shows "foldr f xs = fold f xs"
   14.99 +  using assms unfolding foldr_fold_rev by (rule fold_rev)
  14.100 +
  14.101 +lemma fold_Cons_rev:
  14.102 +  "fold Cons xs = append (rev xs)"
  14.103 +  by (induct xs) simp_all
  14.104 +
  14.105 +lemma rev_conv_fold [code]:
  14.106 +  "rev xs = fold Cons xs []"
  14.107 +  by (simp add: fold_Cons_rev)
  14.108 +
  14.109 +lemma fold_append_concat_rev:
  14.110 +  "fold append xss = append (concat (rev xss))"
  14.111 +  by (induct xss) simp_all
  14.112 +
  14.113 +lemma concat_conv_foldr [code]:
  14.114 +  "concat xss = foldr append xss []"
  14.115 +  by (simp add: fold_append_concat_rev foldr_fold_rev)
  14.116 +
  14.117 +lemma fold_plus_listsum_rev:
  14.118 +  "fold plus xs = plus (listsum (rev xs))"
  14.119 +  by (induct xs) (simp_all add: add.assoc)
  14.120 +
  14.121 +lemma (in monoid_add) listsum_conv_fold [code]:
  14.122 +  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
  14.123 +  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
  14.124 +
  14.125 +lemma (in linorder) sort_key_conv_fold:
  14.126 +  assumes "inj_on f (set xs)"
  14.127 +  shows "sort_key f xs = fold (insort_key f) xs []"
  14.128 +proof -
  14.129 +  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
  14.130 +  proof (rule fold_rev, rule ext)
  14.131 +    fix zs
  14.132 +    fix x y
  14.133 +    assume "x \<in> set xs" "y \<in> set xs"
  14.134 +    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
  14.135 +    have **: "x = y \<longleftrightarrow> y = x" by auto
  14.136 +    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
  14.137 +      by (induct zs) (auto intro: * simp add: **)
  14.138 +  qed
  14.139 +  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
  14.140 +qed
  14.141 +
  14.142 +lemma (in linorder) sort_conv_fold:
  14.143 +  "sort xs = fold insort xs []"
  14.144 +  by (rule sort_key_conv_fold) simp
  14.145 +
  14.146 +
  14.147 +text {* @{const Finite_Set.fold} and @{const fold} *}
  14.148 +
  14.149 +lemma (in comp_fun_commute) fold_set_fold_remdups:
  14.150 +  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
  14.151 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
  14.152 +
  14.153 +lemma (in comp_fun_idem) fold_set_fold:
  14.154 +  "Finite_Set.fold f y (set xs) = fold f xs y"
  14.155 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  14.156 +
  14.157 +lemma (in ab_semigroup_idem_mult) fold1_set_fold:
  14.158 +  assumes "xs \<noteq> []"
  14.159 +  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
  14.160 +proof -
  14.161 +  interpret comp_fun_idem times by (fact comp_fun_idem)
  14.162 +  from assms obtain y ys where xs: "xs = y # ys"
  14.163 +    by (cases xs) auto
  14.164 +  show ?thesis
  14.165 +  proof (cases "set ys = {}")
  14.166 +    case True with xs show ?thesis by simp
  14.167 +  next
  14.168 +    case False
  14.169 +    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
  14.170 +      by (simp only: finite_set fold1_eq_fold_idem)
  14.171 +    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
  14.172 +  qed
  14.173 +qed
  14.174 +
  14.175 +lemma (in lattice) Inf_fin_set_fold:
  14.176 +  "Inf_fin (set (x # xs)) = fold inf xs x"
  14.177 +proof -
  14.178 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.179 +    by (fact ab_semigroup_idem_mult_inf)
  14.180 +  show ?thesis
  14.181 +    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
  14.182 +qed
  14.183 +
  14.184 +lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
  14.185 +  "Inf_fin (set (x # xs)) = foldr inf xs x"
  14.186 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  14.187 +
  14.188 +lemma (in lattice) Sup_fin_set_fold:
  14.189 +  "Sup_fin (set (x # xs)) = fold sup xs x"
  14.190 +proof -
  14.191 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.192 +    by (fact ab_semigroup_idem_mult_sup)
  14.193 +  show ?thesis
  14.194 +    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
  14.195 +qed
  14.196 +
  14.197 +lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
  14.198 +  "Sup_fin (set (x # xs)) = foldr sup xs x"
  14.199 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  14.200 +
  14.201 +lemma (in linorder) Min_fin_set_fold:
  14.202 +  "Min (set (x # xs)) = fold min xs x"
  14.203 +proof -
  14.204 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.205 +    by (fact ab_semigroup_idem_mult_min)
  14.206 +  show ?thesis
  14.207 +    by (simp add: Min_def fold1_set_fold del: set.simps)
  14.208 +qed
  14.209 +
  14.210 +lemma (in linorder) Min_fin_set_foldr [code_unfold]:
  14.211 +  "Min (set (x # xs)) = foldr min xs x"
  14.212 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  14.213 +
  14.214 +lemma (in linorder) Max_fin_set_fold:
  14.215 +  "Max (set (x # xs)) = fold max xs x"
  14.216 +proof -
  14.217 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.218 +    by (fact ab_semigroup_idem_mult_max)
  14.219 +  show ?thesis
  14.220 +    by (simp add: Max_def fold1_set_fold del: set.simps)
  14.221 +qed
  14.222 +
  14.223 +lemma (in linorder) Max_fin_set_foldr [code_unfold]:
  14.224 +  "Max (set (x # xs)) = foldr max xs x"
  14.225 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  14.226 +
  14.227 +lemma (in complete_lattice) Inf_set_fold:
  14.228 +  "Inf (set xs) = fold inf xs top"
  14.229 +proof -
  14.230 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.231 +    by (fact comp_fun_idem_inf)
  14.232 +  show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
  14.233 +qed
  14.234 +
  14.235 +lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
  14.236 +  "Inf (set xs) = foldr inf xs top"
  14.237 +  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
  14.238 +
  14.239 +lemma (in complete_lattice) Sup_set_fold:
  14.240 +  "Sup (set xs) = fold sup xs bot"
  14.241 +proof -
  14.242 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  14.243 +    by (fact comp_fun_idem_sup)
  14.244 +  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
  14.245 +qed
  14.246 +
  14.247 +lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
  14.248 +  "Sup (set xs) = foldr sup xs bot"
  14.249 +  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
  14.250 +
  14.251 +lemma (in complete_lattice) INFI_set_fold:
  14.252 +  "INFI (set xs) f = fold (inf \<circ> f) xs top"
  14.253 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
  14.254 +
  14.255 +lemma (in complete_lattice) SUPR_set_fold:
  14.256 +  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
  14.257 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
  14.258 +
  14.259 +
  14.260 +text {* @{text nth_map} *}
  14.261 +
  14.262 +definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  14.263 +  "nth_map n f xs = (if n < length xs then
  14.264 +       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
  14.265 +     else xs)"
  14.266 +
  14.267 +lemma nth_map_id:
  14.268 +  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
  14.269 +  by (simp add: nth_map_def)
  14.270 +
  14.271 +lemma nth_map_unfold:
  14.272 +  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
  14.273 +  by (simp add: nth_map_def)
  14.274 +
  14.275 +lemma nth_map_Nil [simp]:
  14.276 +  "nth_map n f [] = []"
  14.277 +  by (simp add: nth_map_def)
  14.278 +
  14.279 +lemma nth_map_zero [simp]:
  14.280 +  "nth_map 0 f (x # xs) = f x # xs"
  14.281 +  by (simp add: nth_map_def)
  14.282 +
  14.283 +lemma nth_map_Suc [simp]:
  14.284 +  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
  14.285 +  by (simp add: nth_map_def)
  14.286 +
  14.287 +
  14.288 +text {* monad operation *}
  14.289 +
  14.290 +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  14.291 +  "bind xs f = concat (map f xs)"
  14.292 +
  14.293 +lemma bind_simps [simp]:
  14.294 +  "bind [] f = []"
  14.295 +  "bind (x # xs) f = f x @ bind xs f"
  14.296 +  by (simp_all add: bind_def)
  14.297 +
  14.298 +end

    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/More_Set.thy	Mon Dec 26 22:17:10 2011 +0100
    15.3 @@ -0,0 +1,284 @@
    15.4 +
    15.5 +(* Author: Florian Haftmann, TU Muenchen *)
    15.6 +
    15.7 +header {* Relating (finite) sets and lists *}
    15.8 +
    15.9 +theory More_Set
   15.10 +imports More_List
   15.11 +begin
   15.12 +
   15.13 +lemma comp_fun_idem_remove:
   15.14 +  "comp_fun_idem Set.remove"
   15.15 +proof -
   15.16 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   15.17 +  show ?thesis by (simp only: comp_fun_idem_remove rem)
   15.18 +qed
   15.19 +
   15.20 +lemma minus_fold_remove:
   15.21 +  assumes "finite A"
   15.22 +  shows "B - A = Finite_Set.fold Set.remove B A"
   15.23 +proof -
   15.24 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   15.25 +  show ?thesis by (simp only: rem assms minus_fold_remove)
   15.26 +qed
   15.27 +
   15.28 +lemma bounded_Collect_code [code_unfold_post]:
   15.29 +  "{x \<in> A. P x} = Set.project P A"
   15.30 +  by (simp add: project_def)
   15.31 +
   15.32 +
   15.33 +subsection {* Basic set operations *}
   15.34 +
   15.35 +lemma is_empty_set:
   15.36 +  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
   15.37 +  by (simp add: Set.is_empty_def null_def)
   15.38 +
   15.39 +lemma empty_set:
   15.40 +  "{} = set []"
   15.41 +  by simp
   15.42 +
   15.43 +lemma insert_set_compl:
   15.44 +  "insert x (- set xs) = - set (removeAll x xs)"
   15.45 +  by auto
   15.46 +
   15.47 +lemma remove_set_compl:
   15.48 +  "Set.remove x (- set xs) = - set (List.insert x xs)"
   15.49 +  by (auto simp add: remove_def List.insert_def)
   15.50 +
   15.51 +lemma image_set:
   15.52 +  "image f (set xs) = set (map f xs)"
   15.53 +  by simp
   15.54 +
   15.55 +lemma project_set:
   15.56 +  "Set.project P (set xs) = set (filter P xs)"
   15.57 +  by (auto simp add: project_def)
   15.58 +
   15.59 +
   15.60 +subsection {* Functorial set operations *}
   15.61 +
   15.62 +lemma union_set:
   15.63 +  "set xs \<union> A = fold Set.insert xs A"
   15.64 +proof -
   15.65 +  interpret comp_fun_idem Set.insert
   15.66 +    by (fact comp_fun_idem_insert)
   15.67 +  show ?thesis by (simp add: union_fold_insert fold_set_fold)
   15.68 +qed
   15.69 +
   15.70 +lemma union_set_foldr:
   15.71 +  "set xs \<union> A = foldr Set.insert xs A"
   15.72 +proof -
   15.73 +  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
   15.74 +    by auto
   15.75 +  then show ?thesis by (simp add: union_set foldr_fold)
   15.76 +qed
   15.77 +
   15.78 +lemma minus_set:
   15.79 +  "A - set xs = fold Set.remove xs A"
   15.80 +proof -
   15.81 +  interpret comp_fun_idem Set.remove
   15.82 +    by (fact comp_fun_idem_remove)
   15.83 +  show ?thesis
   15.84 +    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
   15.85 +qed
   15.86 +
   15.87 +lemma minus_set_foldr:
   15.88 +  "A - set xs = foldr Set.remove xs A"
   15.89 +proof -
   15.90 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   15.91 +    by (auto simp add: remove_def)
   15.92 +  then show ?thesis by (simp add: minus_set foldr_fold)
   15.93 +qed
   15.94 +
   15.95 +
   15.96 +subsection {* Derived set operations *}
   15.97 +
   15.98 +lemma member:
   15.99 +  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
  15.100 +  by simp
  15.101 +
  15.102 +lemma subset_eq:
  15.103 +  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  15.104 +  by (fact subset_eq)
  15.105 +
  15.106 +lemma subset:
  15.107 +  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
  15.108 +  by (fact less_le_not_le)
  15.109 +
  15.110 +lemma set_eq:
  15.111 +  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  15.112 +  by (fact eq_iff)
  15.113 +
  15.114 +lemma inter:
  15.115 +  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
  15.116 +  by (auto simp add: project_def)
  15.117 +
  15.118 +
  15.119 +subsection {* Theorems on relations *}
  15.120 +
  15.121 +lemma product_code:
  15.122 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
  15.123 +  by (auto simp add: Product_Type.product_def)
  15.124 +
  15.125 +lemma Id_on_set:
  15.126 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
  15.127 +  by (auto simp add: Id_on_def)
  15.128 +
  15.129 +lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
  15.130 +  by (simp add: finite_trancl_ntranl)
  15.131 +
  15.132 +lemma set_rel_comp:
  15.133 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
  15.134 +  by (auto simp add: Bex_def)
  15.135 +
  15.136 +lemma wf_set:
  15.137 +  "wf (set xs) = acyclic (set xs)"
  15.138 +  by (simp add: wf_iff_acyclic_if_finite)
  15.139 +
  15.140 +
  15.141 +subsection {* Code generator setup *}
  15.142 +
  15.143 +definition coset :: "'a list \<Rightarrow> 'a set" where
  15.144 +  [simp]: "coset xs = - set xs"
  15.145 +
  15.146 +code_datatype set coset
  15.147 +
  15.148 +
  15.149 +subsection {* Basic operations *}
  15.150 +
  15.151 +lemma [code]:
  15.152 +  "x \<in> set xs \<longleftrightarrow> List.member xs x"
  15.153 +  "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
  15.154 +  by (simp_all add: member_def)
  15.155 +
  15.156 +lemma [code_unfold]:
  15.157 +  "A = {} \<longleftrightarrow> Set.is_empty A"
  15.158 +  by (simp add: Set.is_empty_def)
  15.159 +
  15.160 +declare empty_set [code]
  15.161 +
  15.162 +declare is_empty_set [code]
  15.163 +
  15.164 +lemma UNIV_coset [code]:
  15.165 +  "UNIV = coset []"
  15.166 +  by simp
  15.167 +
  15.168 +lemma insert_code [code]:
  15.169 +  "insert x (set xs) = set (List.insert x xs)"
  15.170 +  "insert x (coset xs) = coset (removeAll x xs)"
  15.171 +  by simp_all
  15.172 +
  15.173 +lemma remove_code [code]:
  15.174 +  "Set.remove x (set xs) = set (removeAll x xs)"
  15.175 +  "Set.remove x (coset xs) = coset (List.insert x xs)"
  15.176 +  by (simp_all add: remove_def Compl_insert)
  15.177 +
  15.178 +declare image_set [code]
  15.179 +
  15.180 +declare project_set [code]
  15.181 +
  15.182 +lemma Ball_set [code]:
  15.183 +  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  15.184 +  by (simp add: list_all_iff)
  15.185 +
  15.186 +lemma Bex_set [code]:
  15.187 +  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  15.188 +  by (simp add: list_ex_iff)
  15.189 +
  15.190 +lemma card_set [code]:
  15.191 +  "card (set xs) = length (remdups xs)"
  15.192 +proof -
  15.193 +  have "card (set (remdups xs)) = length (remdups xs)"
  15.194 +    by (rule distinct_card) simp
  15.195 +  then show ?thesis by simp
  15.196 +qed
  15.197 +
  15.198 +
  15.199 +subsection {* Derived operations *}
  15.200 +
  15.201 +declare subset_eq [code]
  15.202 +
  15.203 +declare subset [code]
  15.204 +
  15.205 +
  15.206 +subsection {* Functorial operations *}
  15.207 +
  15.208 +lemma inter_code [code]:
  15.209 +  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  15.210 +  "A \<inter> coset xs = foldr Set.remove xs A"
  15.211 +  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
  15.212 +
  15.213 +lemma subtract_code [code]:
  15.214 +  "A - set xs = foldr Set.remove xs A"
  15.215 +  "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  15.216 +  by (auto simp add: minus_set_foldr)
  15.217 +
  15.218 +lemma union_code [code]:
  15.219 +  "set xs \<union> A = foldr insert xs A"
  15.220 +  "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
  15.221 +  by (auto simp add: union_set_foldr)
  15.222 +
  15.223 +definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
  15.224 +  [simp]: "Inf = Complete_Lattices.Inf"
  15.225 +
  15.226 +hide_const (open) Inf
  15.227 +
  15.228 +lemma [code_unfold_post]:
  15.229 +  "Inf = More_Set.Inf"
  15.230 +  by simp
  15.231 +
  15.232 +definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
  15.233 +  [simp]: "Sup = Complete_Lattices.Sup"
  15.234 +
  15.235 +hide_const (open) Sup
  15.236 +
  15.237 +lemma [code_unfold_post]:
  15.238 +  "Sup = More_Set.Sup"
  15.239 +  by simp
  15.240 +
  15.241 +lemma Inf_code [code]:
  15.242 +  "More_Set.Inf (set xs) = foldr inf xs top"
  15.243 +  "More_Set.Inf (coset []) = bot"
  15.244 +  by (simp_all add: Inf_set_foldr)
  15.245 +
  15.246 +lemma Sup_sup [code]:
  15.247 +  "More_Set.Sup (set xs) = foldr sup xs bot"
  15.248 +  "More_Set.Sup (coset []) = top"
  15.249 +  by (simp_all add: Sup_set_foldr)
  15.250 +
  15.251 +lemma INF_code [code]:
  15.252 +  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
  15.253 +  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
  15.254 +
  15.255 +lemma SUP_sup [code]:
  15.256 +  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
  15.257 +  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
  15.258 +
  15.259 +hide_const (open) coset
  15.260 +
  15.261 +
  15.262 +subsection {* Operations on relations *}
  15.263 +
  15.264 +text {* Initially contributed by Tjark Weber. *}
  15.265 +
  15.266 +declare Domain_fst [code]
  15.267 +
  15.268 +declare Range_snd [code]
  15.269 +
  15.270 +declare trans_join [code]
  15.271 +
  15.272 +declare irrefl_distinct [code]
  15.273 +
  15.274 +declare trancl_set_ntrancl [code]
  15.275 +
  15.276 +declare acyclic_irrefl [code]
  15.277 +
  15.278 +declare product_code [code]
  15.279 +
  15.280 +declare Id_on_set [code]
  15.281 +
  15.282 +declare set_rel_comp [code]
  15.283 +
  15.284 +declare wf_set [code]
  15.285 +
  15.286 +end
  15.287 +

    16.1 --- a/src/HOL/Quotient_Examples/DList.thy	Mon Dec 26 22:17:10 2011 +0100
    16.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Mon Dec 26 22:17:10 2011 +0100
    16.3 @@ -8,7 +8,7 @@
    16.4  header {* Lists with distinct elements *}
    16.5  
    16.6  theory DList
    16.7 -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    16.8 +imports "~~/src/HOL/Library/Quotient_List"
    16.9  begin
   16.10  
   16.11  text {* Some facts about lists *}

    17.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Mon Dec 26 22:17:10 2011 +0100
    17.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Mon Dec 26 22:17:10 2011 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  *)
    17.5  
    17.6  theory FSet
    17.7 -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    17.8 +imports "~~/src/HOL/Library/Quotient_List"
    17.9  begin
   17.10  
   17.11  text {* 

    18.1 --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy	Mon Dec 26 22:17:10 2011 +0100
    18.2 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy	Mon Dec 26 22:17:10 2011 +0100
    18.3 @@ -5,7 +5,7 @@
    18.4  header {* A variant of theory Cset from Library, defined as a quotient *}
    18.5  
    18.6  theory Quotient_Cset
    18.7 -imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
    18.8 +imports Main "~~/src/HOL/Library/Quotient_Syntax"
    18.9  begin
   18.10  
   18.11  subsection {* Lifting *}

    19.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 26 22:17:10 2011 +0100
    19.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 26 22:17:10 2011 +0100
    19.3 @@ -6,7 +6,7 @@
    19.4  header {* Examples for the 'quickcheck' command *}
    19.5  
    19.6  theory Quickcheck_Examples
    19.7 -imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/More_Set"
    19.8 +imports Complex_Main "~~/src/HOL/Library/Dlist"
    19.9  begin
   19.10  
   19.11  text {*