merged
authorhuffman
Tue Dec 27 15:38:45 2011 +0100 (2011-12-27)
changeset 46002b319f1b0c634
parent 46001 0b562d564d5f
parent 45994 38a46e029784
child 46003 c0fe5e8e4864
child 46009 5cb7ef5bfef2
merged
src/HOL/Library/More_List.thy
src/HOL/Library/More_Set.thy
     1.1 --- a/NEWS	Tue Dec 27 15:37:33 2011 +0100
     1.2 +++ b/NEWS	Tue Dec 27 15:38:45 2011 +0100
     1.3 @@ -53,6 +53,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Finite_Set.fold now qualified.  INCOMPATIBILITY.
     1.8 +
     1.9 +* Renamed some facts on canonical fold on lists, in order to avoid problems
    1.10 +with interpretation involving corresponding facts on foldl with the same base names:
    1.11 +
    1.12 +  fold_set_remdups ~> fold_set_fold_remdups
    1.13 +  fold_set ~> fold_set_fold
    1.14 +  fold1_set ~> fold1_set_fold
    1.15 +
    1.16 +INCOMPATIBILITY.
    1.17 +
    1.18  * 'set' is now a proper type constructor.  Definitions mem_def and Collect_def
    1.19  have disappeared.  INCOMPATIBILITY, rephrase sets S used as predicates by
    1.20  `%x. x : S` and predicates P used as sets by `{x. P x}`.  For typical proofs,
     2.1 --- a/src/HOL/GCD.thy	Tue Dec 27 15:37:33 2011 +0100
     2.2 +++ b/src/HOL/GCD.thy	Tue Dec 27 15:38:45 2011 +0100
     2.3 @@ -1486,7 +1486,7 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  "Lcm (M::nat set) = (if finite M then fold lcm 1 M else 0)"
     2.8 +  "Lcm (M::nat set) = (if finite M then Finite_Set.fold lcm 1 M else 0)"
     2.9  
    2.10  definition
    2.11    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
    2.12 @@ -1608,11 +1608,11 @@
    2.13  done
    2.14  
    2.15  lemma Lcm_set_nat [code_unfold]:
    2.16 -  "Lcm (set ns) = foldl lcm (1::nat) ns"
    2.17 +  "Lcm (set ns) = fold lcm ns (1::nat)"
    2.18    by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
    2.19  
    2.20  lemma Gcd_set_nat [code_unfold]:
    2.21 -  "Gcd (set ns) = foldl gcd (0::nat) ns"
    2.22 +  "Gcd (set ns) = fold gcd ns (0::nat)"
    2.23    by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
    2.24  
    2.25  lemma mult_inj_if_coprime_nat:
     3.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Tue Dec 27 15:37:33 2011 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Tue Dec 27 15:38:45 2011 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (* Author: Tobias Nipkow *)
     3.5  
     3.6  theory Abs_Int1_ivl
     3.7 -imports Abs_Int1 Abs_Int_Tests "~~/src/HOL/Library/More_Set"
     3.8 +imports Abs_Int1 Abs_Int_Tests
     3.9  begin
    3.10  
    3.11  subsection "Interval Analysis"
     4.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Tue Dec 27 15:37:33 2011 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Tue Dec 27 15:38:45 2011 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (* Author: Tobias Nipkow *)
     4.5  
     4.6  theory Abs_Int_den1_ivl
     4.7 -imports Abs_Int_den1 "~~/src/HOL/Library/More_Set"
     4.8 +imports Abs_Int_den1
     4.9  begin
    4.10  
    4.11  subsection "Interval Analysis"
     5.1 --- a/src/HOL/IsaMakefile	Tue Dec 27 15:37:33 2011 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Tue Dec 27 15:38:45 2011 +0100
     5.3 @@ -286,6 +286,8 @@
     5.4    List.thy \
     5.5    Main.thy \
     5.6    Map.thy \
     5.7 +  More_List.thy \
     5.8 +  More_Set.thy \
     5.9    Nat_Numeral.thy \
    5.10    Nat_Transfer.thy \
    5.11    New_DSequence.thy \
    5.12 @@ -458,7 +460,7 @@
    5.13    Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
    5.14    Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy	\
    5.15    Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
    5.16 -  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
    5.17 +  Library/Monad_Syntax.thy						\
    5.18    Library/Multiset.thy Library/Nat_Bijection.thy			\
    5.19    Library/Numeral_Type.thy Library/Old_Recdef.thy			\
    5.20    Library/OptionalSugar.thy Library/Order_Relation.thy			\
     6.1 --- a/src/HOL/Library/AList_Impl.thy	Tue Dec 27 15:37:33 2011 +0100
     6.2 +++ b/src/HOL/Library/AList_Impl.thy	Tue Dec 27 15:38:45 2011 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Implementation of Association Lists *}
     6.5  
     6.6  theory AList_Impl
     6.7 -imports Main More_List
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/Library/Cset.thy	Tue Dec 27 15:37:33 2011 +0100
     7.2 +++ b/src/HOL/Library/Cset.thy	Tue Dec 27 15:38:45 2011 +0100
     7.3 @@ -4,7 +4,7 @@
     7.4  header {* A dedicated set type which is executable on its finite part *}
     7.5  
     7.6  theory Cset
     7.7 -imports More_Set More_List
     7.8 +imports Main
     7.9  begin
    7.10  
    7.11  subsection {* Lifting *}
     8.1 --- a/src/HOL/Library/Dlist.thy	Tue Dec 27 15:37:33 2011 +0100
     8.2 +++ b/src/HOL/Library/Dlist.thy	Tue Dec 27 15:38:45 2011 +0100
     8.3 @@ -3,7 +3,7 @@
     8.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     8.5  
     8.6  theory Dlist
     8.7 -imports Main More_List
     8.8 +imports Main
     8.9  begin
    8.10  
    8.11  subsection {* The type of distinct lists *}
     9.1 --- a/src/HOL/Library/Library.thy	Tue Dec 27 15:37:33 2011 +0100
     9.2 +++ b/src/HOL/Library/Library.thy	Tue Dec 27 15:38:45 2011 +0100
     9.3 @@ -33,7 +33,6 @@
     9.4    Kleene_Algebra
     9.5    Mapping
     9.6    Monad_Syntax
     9.7 -  More_List
     9.8    Multiset
     9.9    Numeral_Type
    9.10    Old_Recdef
    10.1 --- a/src/HOL/Library/Monad_Syntax.thy	Tue Dec 27 15:37:33 2011 +0100
    10.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Tue Dec 27 15:38:45 2011 +0100
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Monad notation for arbitrary types *}
    10.5  
    10.6  theory Monad_Syntax
    10.7 -imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
    10.8 +imports Main "~~/src/Tools/Adhoc_Overloading"
    10.9  begin
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Library/More_List.thy	Tue Dec 27 15:37:33 2011 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,312 +0,0 @@
    11.4 -(* Author:  Florian Haftmann, TU Muenchen *)
    11.5 -
    11.6 -header {* Operations on lists beyond the standard List theory *}
    11.7 -
    11.8 -theory More_List
    11.9 -imports Main Multiset
   11.10 -begin
   11.11 -
   11.12 -hide_const (open) Finite_Set.fold
   11.13 -
   11.14 -text {* Repairing code generator setup *}
   11.15 -
   11.16 -declare (in lattice) Inf_fin_set_fold [code_unfold del]
   11.17 -declare (in lattice) Sup_fin_set_fold [code_unfold del]
   11.18 -declare (in linorder) Min_fin_set_fold [code_unfold del]
   11.19 -declare (in linorder) Max_fin_set_fold [code_unfold del]
   11.20 -declare (in complete_lattice) Inf_set_fold [code_unfold del]
   11.21 -declare (in complete_lattice) Sup_set_fold [code_unfold del]
   11.22 -
   11.23 -
   11.24 -text {* Fold combinator with canonical argument order *}
   11.25 -
   11.26 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   11.27 -    "fold f [] = id"
   11.28 -  | "fold f (x # xs) = fold f xs \<circ> f x"
   11.29 -
   11.30 -lemma foldl_fold:
   11.31 -  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
   11.32 -  by (induct xs arbitrary: s) simp_all
   11.33 -
   11.34 -lemma foldr_fold_rev:
   11.35 -  "foldr f xs = fold f (rev xs)"
   11.36 -  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
   11.37 -
   11.38 -lemma fold_rev_conv [code_unfold]:
   11.39 -  "fold f (rev xs) = foldr f xs"
   11.40 -  by (simp add: foldr_fold_rev)
   11.41 -  
   11.42 -lemma fold_cong [fundef_cong]:
   11.43 -  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   11.44 -    \<Longrightarrow> fold f xs a = fold g ys b"
   11.45 -  by (induct ys arbitrary: a b xs) simp_all
   11.46 -
   11.47 -lemma fold_id:
   11.48 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
   11.49 -  shows "fold f xs = id"
   11.50 -  using assms by (induct xs) simp_all
   11.51 -
   11.52 -lemma fold_commute:
   11.53 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   11.54 -  shows "h \<circ> fold g xs = fold f xs \<circ> h"
   11.55 -  using assms by (induct xs) (simp_all add: fun_eq_iff)
   11.56 -
   11.57 -lemma fold_commute_apply:
   11.58 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   11.59 -  shows "h (fold g xs s) = fold f xs (h s)"
   11.60 -proof -
   11.61 -  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
   11.62 -  then show ?thesis by (simp add: fun_eq_iff)
   11.63 -qed
   11.64 -
   11.65 -lemma fold_invariant: 
   11.66 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   11.67 -    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   11.68 -  shows "P (fold f xs s)"
   11.69 -  using assms by (induct xs arbitrary: s) simp_all
   11.70 -
   11.71 -lemma fold_weak_invariant:
   11.72 -  assumes "P s"
   11.73 -    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   11.74 -  shows "P (fold f xs s)"
   11.75 -  using assms by (induct xs arbitrary: s) simp_all
   11.76 -
   11.77 -lemma fold_append [simp]:
   11.78 -  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
   11.79 -  by (induct xs) simp_all
   11.80 -
   11.81 -lemma fold_map [code_unfold]:
   11.82 -  "fold g (map f xs) = fold (g o f) xs"
   11.83 -  by (induct xs) simp_all
   11.84 -
   11.85 -lemma fold_remove1_split:
   11.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"
   11.87 -    and x: "x \<in> set xs"
   11.88 -  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
   11.89 -  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
   11.90 -
   11.91 -lemma fold_multiset_equiv:
   11.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"
   11.93 -    and equiv: "multiset_of xs = multiset_of ys"
   11.94 -  shows "fold f xs = fold f ys"
   11.95 -using f equiv [symmetric] proof (induct xs arbitrary: ys)
   11.96 -  case Nil then show ?case by simp
   11.97 -next
   11.98 -  case (Cons x xs)
   11.99 -  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
  11.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" 
  11.101 -    by (rule Cons.prems(1)) (simp_all add: *)
  11.102 -  moreover from * have "x \<in> set ys" by simp
  11.103 -  ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
  11.104 -  moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
  11.105 -  ultimately show ?case by simp
  11.106 -qed
  11.107 -
  11.108 -lemma fold_rev:
  11.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"
  11.110 -  shows "fold f (rev xs) = fold f xs"
  11.111 -  by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set)
  11.112 -
  11.113 -lemma foldr_fold:
  11.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"
  11.115 -  shows "foldr f xs = fold f xs"
  11.116 -  using assms unfolding foldr_fold_rev by (rule fold_rev)
  11.117 -
  11.118 -lemma fold_Cons_rev:
  11.119 -  "fold Cons xs = append (rev xs)"
  11.120 -  by (induct xs) simp_all
  11.121 -
  11.122 -lemma rev_conv_fold [code]:
  11.123 -  "rev xs = fold Cons xs []"
  11.124 -  by (simp add: fold_Cons_rev)
  11.125 -
  11.126 -lemma fold_append_concat_rev:
  11.127 -  "fold append xss = append (concat (rev xss))"
  11.128 -  by (induct xss) simp_all
  11.129 -
  11.130 -lemma concat_conv_foldr [code]:
  11.131 -  "concat xss = foldr append xss []"
  11.132 -  by (simp add: fold_append_concat_rev foldr_fold_rev)
  11.133 -
  11.134 -lemma fold_plus_listsum_rev:
  11.135 -  "fold plus xs = plus (listsum (rev xs))"
  11.136 -  by (induct xs) (simp_all add: add.assoc)
  11.137 -
  11.138 -lemma (in monoid_add) listsum_conv_fold [code]:
  11.139 -  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
  11.140 -  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
  11.141 -
  11.142 -lemma (in linorder) sort_key_conv_fold:
  11.143 -  assumes "inj_on f (set xs)"
  11.144 -  shows "sort_key f xs = fold (insort_key f) xs []"
  11.145 -proof -
  11.146 -  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
  11.147 -  proof (rule fold_rev, rule ext)
  11.148 -    fix zs
  11.149 -    fix x y
  11.150 -    assume "x \<in> set xs" "y \<in> set xs"
  11.151 -    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
  11.152 -    have **: "x = y \<longleftrightarrow> y = x" by auto
  11.153 -    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
  11.154 -      by (induct zs) (auto intro: * simp add: **)
  11.155 -  qed
  11.156 -  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
  11.157 -qed
  11.158 -
  11.159 -lemma (in linorder) sort_conv_fold:
  11.160 -  "sort xs = fold insort xs []"
  11.161 -  by (rule sort_key_conv_fold) simp
  11.162 -
  11.163 -
  11.164 -text {* @{const Finite_Set.fold} and @{const fold} *}
  11.165 -
  11.166 -lemma (in comp_fun_commute) fold_set_remdups:
  11.167 -  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
  11.168 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
  11.169 -
  11.170 -lemma (in comp_fun_idem) fold_set:
  11.171 -  "Finite_Set.fold f y (set xs) = fold f xs y"
  11.172 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  11.173 -
  11.174 -lemma (in ab_semigroup_idem_mult) fold1_set:
  11.175 -  assumes "xs \<noteq> []"
  11.176 -  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
  11.177 -proof -
  11.178 -  interpret comp_fun_idem times by (fact comp_fun_idem)
  11.179 -  from assms obtain y ys where xs: "xs = y # ys"
  11.180 -    by (cases xs) auto
  11.181 -  show ?thesis
  11.182 -  proof (cases "set ys = {}")
  11.183 -    case True with xs show ?thesis by simp
  11.184 -  next
  11.185 -    case False
  11.186 -    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
  11.187 -      by (simp only: finite_set fold1_eq_fold_idem)
  11.188 -    with xs show ?thesis by (simp add: fold_set mult_commute)
  11.189 -  qed
  11.190 -qed
  11.191 -
  11.192 -lemma (in lattice) Inf_fin_set_fold:
  11.193 -  "Inf_fin (set (x # xs)) = fold inf xs x"
  11.194 -proof -
  11.195 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.196 -    by (fact ab_semigroup_idem_mult_inf)
  11.197 -  show ?thesis
  11.198 -    by (simp add: Inf_fin_def fold1_set del: set.simps)
  11.199 -qed
  11.200 -
  11.201 -lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
  11.202 -  "Inf_fin (set (x # xs)) = foldr inf xs x"
  11.203 -  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  11.204 -
  11.205 -lemma (in lattice) Sup_fin_set_fold:
  11.206 -  "Sup_fin (set (x # xs)) = fold sup xs x"
  11.207 -proof -
  11.208 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.209 -    by (fact ab_semigroup_idem_mult_sup)
  11.210 -  show ?thesis
  11.211 -    by (simp add: Sup_fin_def fold1_set del: set.simps)
  11.212 -qed
  11.213 -
  11.214 -lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
  11.215 -  "Sup_fin (set (x # xs)) = foldr sup xs x"
  11.216 -  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  11.217 -
  11.218 -lemma (in linorder) Min_fin_set_fold:
  11.219 -  "Min (set (x # xs)) = fold min xs x"
  11.220 -proof -
  11.221 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.222 -    by (fact ab_semigroup_idem_mult_min)
  11.223 -  show ?thesis
  11.224 -    by (simp add: Min_def fold1_set del: set.simps)
  11.225 -qed
  11.226 -
  11.227 -lemma (in linorder) Min_fin_set_foldr [code_unfold]:
  11.228 -  "Min (set (x # xs)) = foldr min xs x"
  11.229 -  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  11.230 -
  11.231 -lemma (in linorder) Max_fin_set_fold:
  11.232 -  "Max (set (x # xs)) = fold max xs x"
  11.233 -proof -
  11.234 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.235 -    by (fact ab_semigroup_idem_mult_max)
  11.236 -  show ?thesis
  11.237 -    by (simp add: Max_def fold1_set del: set.simps)
  11.238 -qed
  11.239 -
  11.240 -lemma (in linorder) Max_fin_set_foldr [code_unfold]:
  11.241 -  "Max (set (x # xs)) = foldr max xs x"
  11.242 -  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  11.243 -
  11.244 -lemma (in complete_lattice) Inf_set_fold:
  11.245 -  "Inf (set xs) = fold inf xs top"
  11.246 -proof -
  11.247 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.248 -    by (fact comp_fun_idem_inf)
  11.249 -  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
  11.250 -qed
  11.251 -
  11.252 -lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
  11.253 -  "Inf (set xs) = foldr inf xs top"
  11.254 -  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
  11.255 -
  11.256 -lemma (in complete_lattice) Sup_set_fold:
  11.257 -  "Sup (set xs) = fold sup xs bot"
  11.258 -proof -
  11.259 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  11.260 -    by (fact comp_fun_idem_sup)
  11.261 -  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
  11.262 -qed
  11.263 -
  11.264 -lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
  11.265 -  "Sup (set xs) = foldr sup xs bot"
  11.266 -  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
  11.267 -
  11.268 -lemma (in complete_lattice) INFI_set_fold:
  11.269 -  "INFI (set xs) f = fold (inf \<circ> f) xs top"
  11.270 -  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
  11.271 -
  11.272 -lemma (in complete_lattice) SUPR_set_fold:
  11.273 -  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
  11.274 -  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
  11.275 -
  11.276 -
  11.277 -text {* @{text nth_map} *}
  11.278 -
  11.279 -definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  11.280 -  "nth_map n f xs = (if n < length xs then
  11.281 -       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
  11.282 -     else xs)"
  11.283 -
  11.284 -lemma nth_map_id:
  11.285 -  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
  11.286 -  by (simp add: nth_map_def)
  11.287 -
  11.288 -lemma nth_map_unfold:
  11.289 -  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
  11.290 -  by (simp add: nth_map_def)
  11.291 -
  11.292 -lemma nth_map_Nil [simp]:
  11.293 -  "nth_map n f [] = []"
  11.294 -  by (simp add: nth_map_def)
  11.295 -
  11.296 -lemma nth_map_zero [simp]:
  11.297 -  "nth_map 0 f (x # xs) = f x # xs"
  11.298 -  by (simp add: nth_map_def)
  11.299 -
  11.300 -lemma nth_map_Suc [simp]:
  11.301 -  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
  11.302 -  by (simp add: nth_map_def)
  11.303 -
  11.304 -
  11.305 -text {* monad operation *}
  11.306 -
  11.307 -definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  11.308 -  "bind xs f = concat (map f xs)"
  11.309 -
  11.310 -lemma bind_simps [simp]:
  11.311 -  "bind [] f = []"
  11.312 -  "bind (x # xs) f = f x @ bind xs f"
  11.313 -  by (simp_all add: bind_def)
  11.314 -
  11.315 -end
    12.1 --- a/src/HOL/Library/More_Set.thy	Tue Dec 27 15:37:33 2011 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,284 +0,0 @@
    12.4 -
    12.5 -(* Author: Florian Haftmann, TU Muenchen *)
    12.6 -
    12.7 -header {* Relating (finite) sets and lists *}
    12.8 -
    12.9 -theory More_Set
   12.10 -imports Main More_List
   12.11 -begin
   12.12 -
   12.13 -lemma comp_fun_idem_remove:
   12.14 -  "comp_fun_idem Set.remove"
   12.15 -proof -
   12.16 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   12.17 -  show ?thesis by (simp only: comp_fun_idem_remove rem)
   12.18 -qed
   12.19 -
   12.20 -lemma minus_fold_remove:
   12.21 -  assumes "finite A"
   12.22 -  shows "B - A = Finite_Set.fold Set.remove B A"
   12.23 -proof -
   12.24 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   12.25 -  show ?thesis by (simp only: rem assms minus_fold_remove)
   12.26 -qed
   12.27 -
   12.28 -lemma bounded_Collect_code [code_unfold_post]:
   12.29 -  "{x \<in> A. P x} = Set.project P A"
   12.30 -  by (simp add: project_def)
   12.31 -
   12.32 -
   12.33 -subsection {* Basic set operations *}
   12.34 -
   12.35 -lemma is_empty_set:
   12.36 -  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
   12.37 -  by (simp add: Set.is_empty_def null_def)
   12.38 -
   12.39 -lemma empty_set:
   12.40 -  "{} = set []"
   12.41 -  by simp
   12.42 -
   12.43 -lemma insert_set_compl:
   12.44 -  "insert x (- set xs) = - set (removeAll x xs)"
   12.45 -  by auto
   12.46 -
   12.47 -lemma remove_set_compl:
   12.48 -  "Set.remove x (- set xs) = - set (List.insert x xs)"
   12.49 -  by (auto simp add: remove_def List.insert_def)
   12.50 -
   12.51 -lemma image_set:
   12.52 -  "image f (set xs) = set (map f xs)"
   12.53 -  by simp
   12.54 -
   12.55 -lemma project_set:
   12.56 -  "Set.project P (set xs) = set (filter P xs)"
   12.57 -  by (auto simp add: project_def)
   12.58 -
   12.59 -
   12.60 -subsection {* Functorial set operations *}
   12.61 -
   12.62 -lemma union_set:
   12.63 -  "set xs \<union> A = fold Set.insert xs A"
   12.64 -proof -
   12.65 -  interpret comp_fun_idem Set.insert
   12.66 -    by (fact comp_fun_idem_insert)
   12.67 -  show ?thesis by (simp add: union_fold_insert fold_set)
   12.68 -qed
   12.69 -
   12.70 -lemma union_set_foldr:
   12.71 -  "set xs \<union> A = foldr Set.insert xs A"
   12.72 -proof -
   12.73 -  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
   12.74 -    by auto
   12.75 -  then show ?thesis by (simp add: union_set foldr_fold)
   12.76 -qed
   12.77 -
   12.78 -lemma minus_set:
   12.79 -  "A - set xs = fold Set.remove xs A"
   12.80 -proof -
   12.81 -  interpret comp_fun_idem Set.remove
   12.82 -    by (fact comp_fun_idem_remove)
   12.83 -  show ?thesis
   12.84 -    by (simp add: minus_fold_remove [of _ A] fold_set)
   12.85 -qed
   12.86 -
   12.87 -lemma minus_set_foldr:
   12.88 -  "A - set xs = foldr Set.remove xs A"
   12.89 -proof -
   12.90 -  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   12.91 -    by (auto simp add: remove_def)
   12.92 -  then show ?thesis by (simp add: minus_set foldr_fold)
   12.93 -qed
   12.94 -
   12.95 -
   12.96 -subsection {* Derived set operations *}
   12.97 -
   12.98 -lemma member:
   12.99 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
  12.100 -  by simp
  12.101 -
  12.102 -lemma subset_eq:
  12.103 -  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  12.104 -  by (fact subset_eq)
  12.105 -
  12.106 -lemma subset:
  12.107 -  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
  12.108 -  by (fact less_le_not_le)
  12.109 -
  12.110 -lemma set_eq:
  12.111 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  12.112 -  by (fact eq_iff)
  12.113 -
  12.114 -lemma inter:
  12.115 -  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
  12.116 -  by (auto simp add: project_def)
  12.117 -
  12.118 -
  12.119 -subsection {* Theorems on relations *}
  12.120 -
  12.121 -lemma product_code:
  12.122 -  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
  12.123 -  by (auto simp add: Product_Type.product_def)
  12.124 -
  12.125 -lemma Id_on_set:
  12.126 -  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
  12.127 -  by (auto simp add: Id_on_def)
  12.128 -
  12.129 -lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
  12.130 -  by (simp add: finite_trancl_ntranl)
  12.131 -
  12.132 -lemma set_rel_comp:
  12.133 -  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
  12.134 -  by (auto simp add: Bex_def)
  12.135 -
  12.136 -lemma wf_set:
  12.137 -  "wf (set xs) = acyclic (set xs)"
  12.138 -  by (simp add: wf_iff_acyclic_if_finite)
  12.139 -
  12.140 -
  12.141 -subsection {* Code generator setup *}
  12.142 -
  12.143 -definition coset :: "'a list \<Rightarrow> 'a set" where
  12.144 -  [simp]: "coset xs = - set xs"
  12.145 -
  12.146 -code_datatype set coset
  12.147 -
  12.148 -
  12.149 -subsection {* Basic operations *}
  12.150 -
  12.151 -lemma [code]:
  12.152 -  "x \<in> set xs \<longleftrightarrow> List.member xs x"
  12.153 -  "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
  12.154 -  by (simp_all add: member_def)
  12.155 -
  12.156 -lemma [code_unfold]:
  12.157 -  "A = {} \<longleftrightarrow> Set.is_empty A"
  12.158 -  by (simp add: Set.is_empty_def)
  12.159 -
  12.160 -declare empty_set [code]
  12.161 -
  12.162 -declare is_empty_set [code]
  12.163 -
  12.164 -lemma UNIV_coset [code]:
  12.165 -  "UNIV = coset []"
  12.166 -  by simp
  12.167 -
  12.168 -lemma insert_code [code]:
  12.169 -  "insert x (set xs) = set (List.insert x xs)"
  12.170 -  "insert x (coset xs) = coset (removeAll x xs)"
  12.171 -  by simp_all
  12.172 -
  12.173 -lemma remove_code [code]:
  12.174 -  "Set.remove x (set xs) = set (removeAll x xs)"
  12.175 -  "Set.remove x (coset xs) = coset (List.insert x xs)"
  12.176 -  by (simp_all add: remove_def Compl_insert)
  12.177 -
  12.178 -declare image_set [code]
  12.179 -
  12.180 -declare project_set [code]
  12.181 -
  12.182 -lemma Ball_set [code]:
  12.183 -  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  12.184 -  by (simp add: list_all_iff)
  12.185 -
  12.186 -lemma Bex_set [code]:
  12.187 -  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  12.188 -  by (simp add: list_ex_iff)
  12.189 -
  12.190 -lemma card_set [code]:
  12.191 -  "card (set xs) = length (remdups xs)"
  12.192 -proof -
  12.193 -  have "card (set (remdups xs)) = length (remdups xs)"
  12.194 -    by (rule distinct_card) simp
  12.195 -  then show ?thesis by simp
  12.196 -qed
  12.197 -
  12.198 -
  12.199 -subsection {* Derived operations *}
  12.200 -
  12.201 -declare subset_eq [code]
  12.202 -
  12.203 -declare subset [code]
  12.204 -
  12.205 -
  12.206 -subsection {* Functorial operations *}
  12.207 -
  12.208 -lemma inter_code [code]:
  12.209 -  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  12.210 -  "A \<inter> coset xs = foldr Set.remove xs A"
  12.211 -  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
  12.212 -
  12.213 -lemma subtract_code [code]:
  12.214 -  "A - set xs = foldr Set.remove xs A"
  12.215 -  "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  12.216 -  by (auto simp add: minus_set_foldr)
  12.217 -
  12.218 -lemma union_code [code]:
  12.219 -  "set xs \<union> A = foldr insert xs A"
  12.220 -  "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
  12.221 -  by (auto simp add: union_set_foldr)
  12.222 -
  12.223 -definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
  12.224 -  [simp]: "Inf = Complete_Lattices.Inf"
  12.225 -
  12.226 -hide_const (open) Inf
  12.227 -
  12.228 -lemma [code_unfold_post]:
  12.229 -  "Inf = More_Set.Inf"
  12.230 -  by simp
  12.231 -
  12.232 -definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
  12.233 -  [simp]: "Sup = Complete_Lattices.Sup"
  12.234 -
  12.235 -hide_const (open) Sup
  12.236 -
  12.237 -lemma [code_unfold_post]:
  12.238 -  "Sup = More_Set.Sup"
  12.239 -  by simp
  12.240 -
  12.241 -lemma Inf_code [code]:
  12.242 -  "More_Set.Inf (set xs) = foldr inf xs top"
  12.243 -  "More_Set.Inf (coset []) = bot"
  12.244 -  by (simp_all add: Inf_set_foldr)
  12.245 -
  12.246 -lemma Sup_sup [code]:
  12.247 -  "More_Set.Sup (set xs) = foldr sup xs bot"
  12.248 -  "More_Set.Sup (coset []) = top"
  12.249 -  by (simp_all add: Sup_set_foldr)
  12.250 -
  12.251 -lemma INF_code [code]:
  12.252 -  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
  12.253 -  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
  12.254 -
  12.255 -lemma SUP_sup [code]:
  12.256 -  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
  12.257 -  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
  12.258 -
  12.259 -hide_const (open) coset
  12.260 -
  12.261 -
  12.262 -subsection {* Operations on relations *}
  12.263 -
  12.264 -text {* Initially contributed by Tjark Weber. *}
  12.265 -
  12.266 -declare Domain_fst [code]
  12.267 -
  12.268 -declare Range_snd [code]
  12.269 -
  12.270 -declare trans_join [code]
  12.271 -
  12.272 -declare irrefl_distinct [code]
  12.273 -
  12.274 -declare trancl_set_ntrancl [code]
  12.275 -
  12.276 -declare acyclic_irrefl [code]
  12.277 -
  12.278 -declare product_code [code]
  12.279 -
  12.280 -declare Id_on_set [code]
  12.281 -
  12.282 -declare set_rel_comp [code]
  12.283 -
  12.284 -declare wf_set [code]
  12.285 -
  12.286 -end
  12.287 -
    13.1 --- a/src/HOL/Library/Multiset.thy	Tue Dec 27 15:37:33 2011 +0100
    13.2 +++ b/src/HOL/Library/Multiset.thy	Tue Dec 27 15:38:45 2011 +0100
    13.3 @@ -857,6 +857,23 @@
    13.4    qed
    13.5  qed
    13.6  
    13.7 +lemma fold_multiset_equiv:
    13.8 +  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"
    13.9 +    and equiv: "multiset_of xs = multiset_of ys"
   13.10 +  shows "fold f xs = fold f ys"
   13.11 +using f equiv [symmetric] proof (induct xs arbitrary: ys)
   13.12 +  case Nil then show ?case by simp
   13.13 +next
   13.14 +  case (Cons x xs)
   13.15 +  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
   13.16 +  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
   13.17 +    by (rule Cons.prems(1)) (simp_all add: *)
   13.18 +  moreover from * have "x \<in> set ys" by simp
   13.19 +  ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   13.20 +  moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   13.21 +  ultimately show ?case by simp
   13.22 +qed
   13.23 +
   13.24  context linorder
   13.25  begin
   13.26  
    14.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Dec 27 15:37:33 2011 +0100
    14.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Dec 27 15:38:45 2011 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Implementation of Red-Black Trees *}
    14.5  
    14.6  theory RBT_Impl
    14.7 -imports Main More_List
    14.8 +imports Main
    14.9  begin
   14.10  
   14.11  text {*
    15.1 --- a/src/HOL/Library/Saturated.thy	Tue Dec 27 15:37:33 2011 +0100
    15.2 +++ b/src/HOL/Library/Saturated.thy	Tue Dec 27 15:38:45 2011 +0100
    15.3 @@ -215,38 +215,38 @@
    15.4  begin
    15.5  
    15.6  definition
    15.7 -  "Inf (A :: 'a sat set) = fold min top A"
    15.8 +  "Inf (A :: 'a sat set) = Finite_Set.fold min top A"
    15.9  
   15.10  definition
   15.11 -  "Sup (A :: 'a sat set) = fold max bot A"
   15.12 +  "Sup (A :: 'a sat set) = Finite_Set.fold max bot A"
   15.13  
   15.14  instance proof
   15.15    fix x :: "'a sat"
   15.16    fix A :: "'a sat set"
   15.17    note finite
   15.18    moreover assume "x \<in> A"
   15.19 -  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
   15.20 +  ultimately have "Finite_Set.fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
   15.21    then show "Inf A \<le> x" by (simp add: Inf_sat_def)
   15.22  next
   15.23    fix z :: "'a sat"
   15.24    fix A :: "'a sat set"
   15.25    note finite
   15.26    moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   15.27 -  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
   15.28 +  ultimately have "min z top \<le> Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf)
   15.29    then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
   15.30  next
   15.31    fix x :: "'a sat"
   15.32    fix A :: "'a sat set"
   15.33    note finite
   15.34    moreover assume "x \<in> A"
   15.35 -  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
   15.36 +  ultimately have "max x bot \<le> Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup)
   15.37    then show "x \<le> Sup A" by (simp add: Sup_sat_def)
   15.38  next
   15.39    fix z :: "'a sat"
   15.40    fix A :: "'a sat set"
   15.41    note finite
   15.42    moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   15.43 -  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
   15.44 +  ultimately have "Finite_Set.fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
   15.45    then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
   15.46  qed
   15.47  
    16.1 --- a/src/HOL/List.thy	Tue Dec 27 15:37:33 2011 +0100
    16.2 +++ b/src/HOL/List.thy	Tue Dec 27 15:38:45 2011 +0100
    16.3 @@ -2536,68 +2536,6 @@
    16.4    qed
    16.5  qed
    16.6  
    16.7 -lemma (in lattice) Inf_fin_set_fold [code_unfold]:
    16.8 -  "Inf_fin (set (x # xs)) = foldl inf x xs"
    16.9 -proof -
   16.10 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.11 -    by (fact ab_semigroup_idem_mult_inf)
   16.12 -  show ?thesis
   16.13 -    by (simp add: Inf_fin_def fold1_set del: set.simps)
   16.14 -qed
   16.15 -
   16.16 -lemma (in lattice) Sup_fin_set_fold [code_unfold]:
   16.17 -  "Sup_fin (set (x # xs)) = foldl sup x xs"
   16.18 -proof -
   16.19 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.20 -    by (fact ab_semigroup_idem_mult_sup)
   16.21 -  show ?thesis
   16.22 -    by (simp add: Sup_fin_def fold1_set del: set.simps)
   16.23 -qed
   16.24 -
   16.25 -lemma (in linorder) Min_fin_set_fold [code_unfold]:
   16.26 -  "Min (set (x # xs)) = foldl min x xs"
   16.27 -proof -
   16.28 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.29 -    by (fact ab_semigroup_idem_mult_min)
   16.30 -  show ?thesis
   16.31 -    by (simp add: Min_def fold1_set del: set.simps)
   16.32 -qed
   16.33 -
   16.34 -lemma (in linorder) Max_fin_set_fold [code_unfold]:
   16.35 -  "Max (set (x # xs)) = foldl max x xs"
   16.36 -proof -
   16.37 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.38 -    by (fact ab_semigroup_idem_mult_max)
   16.39 -  show ?thesis
   16.40 -    by (simp add: Max_def fold1_set del: set.simps)
   16.41 -qed
   16.42 -
   16.43 -lemma (in complete_lattice) Inf_set_fold [code_unfold]:
   16.44 -  "Inf (set xs) = foldl inf top xs"
   16.45 -proof -
   16.46 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.47 -    by (fact comp_fun_idem_inf)
   16.48 -  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
   16.49 -qed
   16.50 -
   16.51 -lemma (in complete_lattice) Sup_set_fold [code_unfold]:
   16.52 -  "Sup (set xs) = foldl sup bot xs"
   16.53 -proof -
   16.54 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   16.55 -    by (fact comp_fun_idem_sup)
   16.56 -  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
   16.57 -qed
   16.58 -
   16.59 -lemma (in complete_lattice) INFI_set_fold:
   16.60 -  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
   16.61 -  unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
   16.62 -    by (simp add: inf_commute)
   16.63 -
   16.64 -lemma (in complete_lattice) SUPR_set_fold:
   16.65 -  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
   16.66 -  unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
   16.67 -    by (simp add: sup_commute)
   16.68 -
   16.69  
   16.70  subsubsection {* @{text upt} *}
   16.71  
    17.1 --- a/src/HOL/Main.thy	Tue Dec 27 15:37:33 2011 +0100
    17.2 +++ b/src/HOL/Main.thy	Tue Dec 27 15:38:45 2011 +0100
    17.3 @@ -1,7 +1,7 @@
    17.4  header {* Main HOL *}
    17.5  
    17.6  theory Main
    17.7 -imports Plain Predicate_Compile Nitpick
    17.8 +imports Plain Predicate_Compile Nitpick More_Set
    17.9  begin
   17.10  
   17.11  text {*
    18.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Dec 27 15:37:33 2011 +0100
    18.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Dec 27 15:38:45 2011 +0100
    18.3 @@ -9,7 +9,6 @@
    18.4    "../JVM/JVMListExample"
    18.5    BVSpecTypeSafe
    18.6    JVM
    18.7 -  "~~/src/HOL/Library/More_Set"
    18.8  begin
    18.9  
   18.10  text {*
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/More_List.thy	Tue Dec 27 15:38:45 2011 +0100
    19.3 @@ -0,0 +1,285 @@
    19.4 +(* Author:  Florian Haftmann, TU Muenchen *)
    19.5 +
    19.6 +header {* Operations on lists beyond the standard List theory *}
    19.7 +
    19.8 +theory More_List
    19.9 +imports List
   19.10 +begin
   19.11 +
   19.12 +hide_const (open) Finite_Set.fold
   19.13 +
   19.14 +text {* Fold combinator with canonical argument order *}
   19.15 +
   19.16 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   19.17 +    "fold f [] = id"
   19.18 +  | "fold f (x # xs) = fold f xs \<circ> f x"
   19.19 +
   19.20 +lemma foldl_fold:
   19.21 +  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
   19.22 +  by (induct xs arbitrary: s) simp_all
   19.23 +
   19.24 +lemma foldr_fold_rev:
   19.25 +  "foldr f xs = fold f (rev xs)"
   19.26 +  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
   19.27 +
   19.28 +lemma fold_rev_conv [code_unfold]:
   19.29 +  "fold f (rev xs) = foldr f xs"
   19.30 +  by (simp add: foldr_fold_rev)
   19.31 +  
   19.32 +lemma fold_cong [fundef_cong]:
   19.33 +  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   19.34 +    \<Longrightarrow> fold f xs a = fold g ys b"
   19.35 +  by (induct ys arbitrary: a b xs) simp_all
   19.36 +
   19.37 +lemma fold_id:
   19.38 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
   19.39 +  shows "fold f xs = id"
   19.40 +  using assms by (induct xs) simp_all
   19.41 +
   19.42 +lemma fold_commute:
   19.43 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   19.44 +  shows "h \<circ> fold g xs = fold f xs \<circ> h"
   19.45 +  using assms by (induct xs) (simp_all add: fun_eq_iff)
   19.46 +
   19.47 +lemma fold_commute_apply:
   19.48 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   19.49 +  shows "h (fold g xs s) = fold f xs (h s)"
   19.50 +proof -
   19.51 +  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
   19.52 +  then show ?thesis by (simp add: fun_eq_iff)
   19.53 +qed
   19.54 +
   19.55 +lemma fold_invariant: 
   19.56 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   19.57 +    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   19.58 +  shows "P (fold f xs s)"
   19.59 +  using assms by (induct xs arbitrary: s) simp_all
   19.60 +
   19.61 +lemma fold_weak_invariant:
   19.62 +  assumes "P s"
   19.63 +    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   19.64 +  shows "P (fold f xs s)"
   19.65 +  using assms by (induct xs arbitrary: s) simp_all
   19.66 +
   19.67 +lemma fold_append [simp]:
   19.68 +  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
   19.69 +  by (induct xs) simp_all
   19.70 +
   19.71 +lemma fold_map [code_unfold]:
   19.72 +  "fold g (map f xs) = fold (g o f) xs"
   19.73 +  by (induct xs) simp_all
   19.74 +
   19.75 +lemma fold_remove1_split:
   19.76 +  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"
   19.77 +    and x: "x \<in> set xs"
   19.78 +  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
   19.79 +  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
   19.80 +
   19.81 +lemma fold_rev:
   19.82 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   19.83 +  shows "fold f (rev xs) = fold f xs"
   19.84 +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
   19.85 +
   19.86 +lemma foldr_fold:
   19.87 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   19.88 +  shows "foldr f xs = fold f xs"
   19.89 +  using assms unfolding foldr_fold_rev by (rule fold_rev)
   19.90 +
   19.91 +lemma fold_Cons_rev:
   19.92 +  "fold Cons xs = append (rev xs)"
   19.93 +  by (induct xs) simp_all
   19.94 +
   19.95 +lemma rev_conv_fold [code]:
   19.96 +  "rev xs = fold Cons xs []"
   19.97 +  by (simp add: fold_Cons_rev)
   19.98 +
   19.99 +lemma fold_append_concat_rev:
  19.100 +  "fold append xss = append (concat (rev xss))"
  19.101 +  by (induct xss) simp_all
  19.102 +
  19.103 +lemma concat_conv_foldr [code]:
  19.104 +  "concat xss = foldr append xss []"
  19.105 +  by (simp add: fold_append_concat_rev foldr_fold_rev)
  19.106 +
  19.107 +lemma fold_plus_listsum_rev:
  19.108 +  "fold plus xs = plus (listsum (rev xs))"
  19.109 +  by (induct xs) (simp_all add: add.assoc)
  19.110 +
  19.111 +lemma (in monoid_add) listsum_conv_fold [code]:
  19.112 +  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
  19.113 +  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
  19.114 +
  19.115 +lemma (in linorder) sort_key_conv_fold:
  19.116 +  assumes "inj_on f (set xs)"
  19.117 +  shows "sort_key f xs = fold (insort_key f) xs []"
  19.118 +proof -
  19.119 +  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
  19.120 +  proof (rule fold_rev, rule ext)
  19.121 +    fix zs
  19.122 +    fix x y
  19.123 +    assume "x \<in> set xs" "y \<in> set xs"
  19.124 +    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
  19.125 +    have **: "x = y \<longleftrightarrow> y = x" by auto
  19.126 +    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
  19.127 +      by (induct zs) (auto intro: * simp add: **)
  19.128 +  qed
  19.129 +  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
  19.130 +qed
  19.131 +
  19.132 +lemma (in linorder) sort_conv_fold:
  19.133 +  "sort xs = fold insort xs []"
  19.134 +  by (rule sort_key_conv_fold) simp
  19.135 +
  19.136 +
  19.137 +text {* @{const Finite_Set.fold} and @{const fold} *}
  19.138 +
  19.139 +lemma (in comp_fun_commute) fold_set_fold_remdups:
  19.140 +  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
  19.141 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
  19.142 +
  19.143 +lemma (in comp_fun_idem) fold_set_fold:
  19.144 +  "Finite_Set.fold f y (set xs) = fold f xs y"
  19.145 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  19.146 +
  19.147 +lemma (in ab_semigroup_idem_mult) fold1_set_fold:
  19.148 +  assumes "xs \<noteq> []"
  19.149 +  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
  19.150 +proof -
  19.151 +  interpret comp_fun_idem times by (fact comp_fun_idem)
  19.152 +  from assms obtain y ys where xs: "xs = y # ys"
  19.153 +    by (cases xs) auto
  19.154 +  show ?thesis
  19.155 +  proof (cases "set ys = {}")
  19.156 +    case True with xs show ?thesis by simp
  19.157 +  next
  19.158 +    case False
  19.159 +    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
  19.160 +      by (simp only: finite_set fold1_eq_fold_idem)
  19.161 +    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
  19.162 +  qed
  19.163 +qed
  19.164 +
  19.165 +lemma (in lattice) Inf_fin_set_fold:
  19.166 +  "Inf_fin (set (x # xs)) = fold inf xs x"
  19.167 +proof -
  19.168 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.169 +    by (fact ab_semigroup_idem_mult_inf)
  19.170 +  show ?thesis
  19.171 +    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
  19.172 +qed
  19.173 +
  19.174 +lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
  19.175 +  "Inf_fin (set (x # xs)) = foldr inf xs x"
  19.176 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  19.177 +
  19.178 +lemma (in lattice) Sup_fin_set_fold:
  19.179 +  "Sup_fin (set (x # xs)) = fold sup xs x"
  19.180 +proof -
  19.181 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.182 +    by (fact ab_semigroup_idem_mult_sup)
  19.183 +  show ?thesis
  19.184 +    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
  19.185 +qed
  19.186 +
  19.187 +lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
  19.188 +  "Sup_fin (set (x # xs)) = foldr sup xs x"
  19.189 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  19.190 +
  19.191 +lemma (in linorder) Min_fin_set_fold:
  19.192 +  "Min (set (x # xs)) = fold min xs x"
  19.193 +proof -
  19.194 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.195 +    by (fact ab_semigroup_idem_mult_min)
  19.196 +  show ?thesis
  19.197 +    by (simp add: Min_def fold1_set_fold del: set.simps)
  19.198 +qed
  19.199 +
  19.200 +lemma (in linorder) Min_fin_set_foldr [code_unfold]:
  19.201 +  "Min (set (x # xs)) = foldr min xs x"
  19.202 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  19.203 +
  19.204 +lemma (in linorder) Max_fin_set_fold:
  19.205 +  "Max (set (x # xs)) = fold max xs x"
  19.206 +proof -
  19.207 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.208 +    by (fact ab_semigroup_idem_mult_max)
  19.209 +  show ?thesis
  19.210 +    by (simp add: Max_def fold1_set_fold del: set.simps)
  19.211 +qed
  19.212 +
  19.213 +lemma (in linorder) Max_fin_set_foldr [code_unfold]:
  19.214 +  "Max (set (x # xs)) = foldr max xs x"
  19.215 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
  19.216 +
  19.217 +lemma (in complete_lattice) Inf_set_fold:
  19.218 +  "Inf (set xs) = fold inf xs top"
  19.219 +proof -
  19.220 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.221 +    by (fact comp_fun_idem_inf)
  19.222 +  show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
  19.223 +qed
  19.224 +
  19.225 +lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
  19.226 +  "Inf (set xs) = foldr inf xs top"
  19.227 +  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
  19.228 +
  19.229 +lemma (in complete_lattice) Sup_set_fold:
  19.230 +  "Sup (set xs) = fold sup xs bot"
  19.231 +proof -
  19.232 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  19.233 +    by (fact comp_fun_idem_sup)
  19.234 +  show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
  19.235 +qed
  19.236 +
  19.237 +lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
  19.238 +  "Sup (set xs) = foldr sup xs bot"
  19.239 +  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
  19.240 +
  19.241 +lemma (in complete_lattice) INFI_set_fold:
  19.242 +  "INFI (set xs) f = fold (inf \<circ> f) xs top"
  19.243 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
  19.244 +
  19.245 +lemma (in complete_lattice) SUPR_set_fold:
  19.246 +  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
  19.247 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
  19.248 +
  19.249 +
  19.250 +text {* @{text nth_map} *}
  19.251 +
  19.252 +definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  19.253 +  "nth_map n f xs = (if n < length xs then
  19.254 +       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
  19.255 +     else xs)"
  19.256 +
  19.257 +lemma nth_map_id:
  19.258 +  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
  19.259 +  by (simp add: nth_map_def)
  19.260 +
  19.261 +lemma nth_map_unfold:
  19.262 +  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
  19.263 +  by (simp add: nth_map_def)
  19.264 +
  19.265 +lemma nth_map_Nil [simp]:
  19.266 +  "nth_map n f [] = []"
  19.267 +  by (simp add: nth_map_def)
  19.268 +
  19.269 +lemma nth_map_zero [simp]:
  19.270 +  "nth_map 0 f (x # xs) = f x # xs"
  19.271 +  by (simp add: nth_map_def)
  19.272 +
  19.273 +lemma nth_map_Suc [simp]:
  19.274 +  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
  19.275 +  by (simp add: nth_map_def)
  19.276 +
  19.277 +
  19.278 +text {* monad operation *}
  19.279 +
  19.280 +definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
  19.281 +  "bind xs f = concat (map f xs)"
  19.282 +
  19.283 +lemma bind_simps [simp]:
  19.284 +  "bind [] f = []"
  19.285 +  "bind (x # xs) f = f x @ bind xs f"
  19.286 +  by (simp_all add: bind_def)
  19.287 +
  19.288 +end
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/More_Set.thy	Tue Dec 27 15:38:45 2011 +0100
    20.3 @@ -0,0 +1,284 @@
    20.4 +
    20.5 +(* Author: Florian Haftmann, TU Muenchen *)
    20.6 +
    20.7 +header {* Relating (finite) sets and lists *}
    20.8 +
    20.9 +theory More_Set
   20.10 +imports More_List
   20.11 +begin
   20.12 +
   20.13 +lemma comp_fun_idem_remove:
   20.14 +  "comp_fun_idem Set.remove"
   20.15 +proof -
   20.16 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   20.17 +  show ?thesis by (simp only: comp_fun_idem_remove rem)
   20.18 +qed
   20.19 +
   20.20 +lemma minus_fold_remove:
   20.21 +  assumes "finite A"
   20.22 +  shows "B - A = Finite_Set.fold Set.remove B A"
   20.23 +proof -
   20.24 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   20.25 +  show ?thesis by (simp only: rem assms minus_fold_remove)
   20.26 +qed
   20.27 +
   20.28 +lemma bounded_Collect_code [code_unfold_post]:
   20.29 +  "{x \<in> A. P x} = Set.project P A"
   20.30 +  by (simp add: project_def)
   20.31 +
   20.32 +
   20.33 +subsection {* Basic set operations *}
   20.34 +
   20.35 +lemma is_empty_set:
   20.36 +  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
   20.37 +  by (simp add: Set.is_empty_def null_def)
   20.38 +
   20.39 +lemma empty_set:
   20.40 +  "{} = set []"
   20.41 +  by simp
   20.42 +
   20.43 +lemma insert_set_compl:
   20.44 +  "insert x (- set xs) = - set (removeAll x xs)"
   20.45 +  by auto
   20.46 +
   20.47 +lemma remove_set_compl:
   20.48 +  "Set.remove x (- set xs) = - set (List.insert x xs)"
   20.49 +  by (auto simp add: remove_def List.insert_def)
   20.50 +
   20.51 +lemma image_set:
   20.52 +  "image f (set xs) = set (map f xs)"
   20.53 +  by simp
   20.54 +
   20.55 +lemma project_set:
   20.56 +  "Set.project P (set xs) = set (filter P xs)"
   20.57 +  by (auto simp add: project_def)
   20.58 +
   20.59 +
   20.60 +subsection {* Functorial set operations *}
   20.61 +
   20.62 +lemma union_set:
   20.63 +  "set xs \<union> A = fold Set.insert xs A"
   20.64 +proof -
   20.65 +  interpret comp_fun_idem Set.insert
   20.66 +    by (fact comp_fun_idem_insert)
   20.67 +  show ?thesis by (simp add: union_fold_insert fold_set_fold)
   20.68 +qed
   20.69 +
   20.70 +lemma union_set_foldr:
   20.71 +  "set xs \<union> A = foldr Set.insert xs A"
   20.72 +proof -
   20.73 +  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
   20.74 +    by auto
   20.75 +  then show ?thesis by (simp add: union_set foldr_fold)
   20.76 +qed
   20.77 +
   20.78 +lemma minus_set:
   20.79 +  "A - set xs = fold Set.remove xs A"
   20.80 +proof -
   20.81 +  interpret comp_fun_idem Set.remove
   20.82 +    by (fact comp_fun_idem_remove)
   20.83 +  show ?thesis
   20.84 +    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
   20.85 +qed
   20.86 +
   20.87 +lemma minus_set_foldr:
   20.88 +  "A - set xs = foldr Set.remove xs A"
   20.89 +proof -
   20.90 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   20.91 +    by (auto simp add: remove_def)
   20.92 +  then show ?thesis by (simp add: minus_set foldr_fold)
   20.93 +qed
   20.94 +
   20.95 +
   20.96 +subsection {* Derived set operations *}
   20.97 +
   20.98 +lemma member:
   20.99 +  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
  20.100 +  by simp
  20.101 +
  20.102 +lemma subset_eq:
  20.103 +  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  20.104 +  by (fact subset_eq)
  20.105 +
  20.106 +lemma subset:
  20.107 +  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
  20.108 +  by (fact less_le_not_le)
  20.109 +
  20.110 +lemma set_eq:
  20.111 +  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  20.112 +  by (fact eq_iff)
  20.113 +
  20.114 +lemma inter:
  20.115 +  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
  20.116 +  by (auto simp add: project_def)
  20.117 +
  20.118 +
  20.119 +subsection {* Theorems on relations *}
  20.120 +
  20.121 +lemma product_code:
  20.122 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
  20.123 +  by (auto simp add: Product_Type.product_def)
  20.124 +
  20.125 +lemma Id_on_set:
  20.126 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
  20.127 +  by (auto simp add: Id_on_def)
  20.128 +
  20.129 +lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
  20.130 +  by (simp add: finite_trancl_ntranl)
  20.131 +
  20.132 +lemma set_rel_comp:
  20.133 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
  20.134 +  by (auto simp add: Bex_def)
  20.135 +
  20.136 +lemma wf_set:
  20.137 +  "wf (set xs) = acyclic (set xs)"
  20.138 +  by (simp add: wf_iff_acyclic_if_finite)
  20.139 +
  20.140 +
  20.141 +subsection {* Code generator setup *}
  20.142 +
  20.143 +definition coset :: "'a list \<Rightarrow> 'a set" where
  20.144 +  [simp]: "coset xs = - set xs"
  20.145 +
  20.146 +code_datatype set coset
  20.147 +
  20.148 +
  20.149 +subsection {* Basic operations *}
  20.150 +
  20.151 +lemma [code]:
  20.152 +  "x \<in> set xs \<longleftrightarrow> List.member xs x"
  20.153 +  "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
  20.154 +  by (simp_all add: member_def)
  20.155 +
  20.156 +lemma [code_unfold]:
  20.157 +  "A = {} \<longleftrightarrow> Set.is_empty A"
  20.158 +  by (simp add: Set.is_empty_def)
  20.159 +
  20.160 +declare empty_set [code]
  20.161 +
  20.162 +declare is_empty_set [code]
  20.163 +
  20.164 +lemma UNIV_coset [code]:
  20.165 +  "UNIV = coset []"
  20.166 +  by simp
  20.167 +
  20.168 +lemma insert_code [code]:
  20.169 +  "insert x (set xs) = set (List.insert x xs)"
  20.170 +  "insert x (coset xs) = coset (removeAll x xs)"
  20.171 +  by simp_all
  20.172 +
  20.173 +lemma remove_code [code]:
  20.174 +  "Set.remove x (set xs) = set (removeAll x xs)"
  20.175 +  "Set.remove x (coset xs) = coset (List.insert x xs)"
  20.176 +  by (simp_all add: remove_def Compl_insert)
  20.177 +
  20.178 +declare image_set [code]
  20.179 +
  20.180 +declare project_set [code]
  20.181 +
  20.182 +lemma Ball_set [code]:
  20.183 +  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  20.184 +  by (simp add: list_all_iff)
  20.185 +
  20.186 +lemma Bex_set [code]:
  20.187 +  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  20.188 +  by (simp add: list_ex_iff)
  20.189 +
  20.190 +lemma card_set [code]:
  20.191 +  "card (set xs) = length (remdups xs)"
  20.192 +proof -
  20.193 +  have "card (set (remdups xs)) = length (remdups xs)"
  20.194 +    by (rule distinct_card) simp
  20.195 +  then show ?thesis by simp
  20.196 +qed
  20.197 +
  20.198 +
  20.199 +subsection {* Derived operations *}
  20.200 +
  20.201 +declare subset_eq [code]
  20.202 +
  20.203 +declare subset [code]
  20.204 +
  20.205 +
  20.206 +subsection {* Functorial operations *}
  20.207 +
  20.208 +lemma inter_code [code]:
  20.209 +  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  20.210 +  "A \<inter> coset xs = foldr Set.remove xs A"
  20.211 +  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
  20.212 +
  20.213 +lemma subtract_code [code]:
  20.214 +  "A - set xs = foldr Set.remove xs A"
  20.215 +  "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
  20.216 +  by (auto simp add: minus_set_foldr)
  20.217 +
  20.218 +lemma union_code [code]:
  20.219 +  "set xs \<union> A = foldr insert xs A"
  20.220 +  "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
  20.221 +  by (auto simp add: union_set_foldr)
  20.222 +
  20.223 +definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
  20.224 +  [simp]: "Inf = Complete_Lattices.Inf"
  20.225 +
  20.226 +hide_const (open) Inf
  20.227 +
  20.228 +lemma [code_unfold_post]:
  20.229 +  "Inf = More_Set.Inf"
  20.230 +  by simp
  20.231 +
  20.232 +definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
  20.233 +  [simp]: "Sup = Complete_Lattices.Sup"
  20.234 +
  20.235 +hide_const (open) Sup
  20.236 +
  20.237 +lemma [code_unfold_post]:
  20.238 +  "Sup = More_Set.Sup"
  20.239 +  by simp
  20.240 +
  20.241 +lemma Inf_code [code]:
  20.242 +  "More_Set.Inf (set xs) = foldr inf xs top"
  20.243 +  "More_Set.Inf (coset []) = bot"
  20.244 +  by (simp_all add: Inf_set_foldr)
  20.245 +
  20.246 +lemma Sup_sup [code]:
  20.247 +  "More_Set.Sup (set xs) = foldr sup xs bot"
  20.248 +  "More_Set.Sup (coset []) = top"
  20.249 +  by (simp_all add: Sup_set_foldr)
  20.250 +
  20.251 +lemma INF_code [code]:
  20.252 +  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
  20.253 +  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
  20.254 +
  20.255 +lemma SUP_sup [code]:
  20.256 +  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
  20.257 +  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
  20.258 +
  20.259 +hide_const (open) coset
  20.260 +
  20.261 +
  20.262 +subsection {* Operations on relations *}
  20.263 +
  20.264 +text {* Initially contributed by Tjark Weber. *}
  20.265 +
  20.266 +declare Domain_fst [code]
  20.267 +
  20.268 +declare Range_snd [code]
  20.269 +
  20.270 +declare trans_join [code]
  20.271 +
  20.272 +declare irrefl_distinct [code]
  20.273 +
  20.274 +declare trancl_set_ntrancl [code]
  20.275 +
  20.276 +declare acyclic_irrefl [code]
  20.277 +
  20.278 +declare product_code [code]
  20.279 +
  20.280 +declare Id_on_set [code]
  20.281 +
  20.282 +declare set_rel_comp [code]
  20.283 +
  20.284 +declare wf_set [code]
  20.285 +
  20.286 +end
  20.287 +
    21.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 15:37:33 2011 +0100
    21.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 15:38:45 2011 +0100
    21.3 @@ -1814,7 +1814,7 @@
    21.4    unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto
    21.5  
    21.6  definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
    21.7 -definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)"
    21.8 +definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)"
    21.9  definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
   21.10  
   21.11  lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
    22.1 --- a/src/HOL/Quotient_Examples/DList.thy	Tue Dec 27 15:37:33 2011 +0100
    22.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Tue Dec 27 15:38:45 2011 +0100
    22.3 @@ -8,7 +8,7 @@
    22.4  header {* Lists with distinct elements *}
    22.5  
    22.6  theory DList
    22.7 -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    22.8 +imports "~~/src/HOL/Library/Quotient_List"
    22.9  begin
   22.10  
   22.11  text {* Some facts about lists *}
    23.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 27 15:37:33 2011 +0100
    23.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 27 15:38:45 2011 +0100
    23.3 @@ -6,7 +6,7 @@
    23.4  *)
    23.5  
    23.6  theory FSet
    23.7 -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    23.8 +imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
    23.9  begin
   23.10  
   23.11  text {* 
    24.1 --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy	Tue Dec 27 15:37:33 2011 +0100
    24.2 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy	Tue Dec 27 15:38:45 2011 +0100
    24.3 @@ -5,7 +5,7 @@
    24.4  header {* A variant of theory Cset from Library, defined as a quotient *}
    24.5  
    24.6  theory Quotient_Cset
    24.7 -imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
    24.8 +imports Main "~~/src/HOL/Library/Quotient_Syntax"
    24.9  begin
   24.10  
   24.11  subsection {* Lifting *}
    25.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Dec 27 15:37:33 2011 +0100
    25.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Tue Dec 27 15:38:45 2011 +0100
    25.3 @@ -6,7 +6,7 @@
    25.4  header {* Examples for the 'quickcheck' command *}
    25.5  
    25.6  theory Quickcheck_Examples
    25.7 -imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/More_Set"
    25.8 +imports Complex_Main "~~/src/HOL/Library/Dlist"
    25.9  begin
   25.10  
   25.11  text {*