src/HOL/List.thy
 changeset 51489 f738e6dbd844 parent 51315 536a5603a138 child 51540 eea5c4ca4a0e
```     1.1 --- a/src/HOL/List.thy	Sat Mar 23 17:11:06 2013 +0100
1.2 +++ b/src/HOL/List.thy	Sat Mar 23 20:50:39 2013 +0100
1.3 @@ -2734,51 +2734,11 @@
1.4
1.5  lemma (in comp_fun_commute) fold_set_fold_remdups:
1.6    "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
1.7 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
1.8 -
1.9 -lemma (in ab_semigroup_mult) fold1_distinct_set_fold:
1.10 -  assumes "xs \<noteq> []"
1.11 -  assumes d: "distinct xs"
1.12 -  shows "Finite_Set.fold1 times (set xs) = List.fold times (tl xs) (hd xs)"
1.13 -proof -
1.14 -  interpret comp_fun_commute times by (fact comp_fun_commute)
1.15 -  from assms obtain y ys where xs: "xs = y # ys"
1.16 -    by (cases xs) auto
1.17 -  then have *: "y \<notin> set ys" using assms by simp
1.18 -  from xs d have **: "remdups ys = ys"  by safe (induct ys, auto)
1.19 -  show ?thesis
1.20 -  proof (cases "set ys = {}")
1.21 -    case True with xs show ?thesis by simp
1.22 -  next
1.23 -    case False
1.24 -    then have "fold1 times (Set.insert y (set ys)) = Finite_Set.fold times y (set ys)"
1.25 -      by (simp_all add: fold1_eq_fold *)
1.26 -    with xs show ?thesis
1.27 -      by (simp add: fold_set_fold_remdups **)
1.28 -  qed
1.29 -qed
1.30 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
1.31
1.32  lemma (in comp_fun_idem) fold_set_fold:
1.33    "Finite_Set.fold f y (set xs) = fold f xs y"
1.34 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
1.35 -
1.36 -lemma (in ab_semigroup_idem_mult) fold1_set_fold:
1.37 -  assumes "xs \<noteq> []"
1.38 -  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
1.39 -proof -
1.40 -  interpret comp_fun_idem times by (fact comp_fun_idem)
1.41 -  from assms obtain y ys where xs: "xs = y # ys"
1.42 -    by (cases xs) auto
1.43 -  show ?thesis
1.44 -  proof (cases "set ys = {}")
1.45 -    case True with xs show ?thesis by simp
1.46 -  next
1.47 -    case False
1.48 -    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
1.49 -      by (simp only: finite_set fold1_eq_fold_idem)
1.50 -    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
1.51 -  qed
1.52 -qed
1.53 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
1.54
1.55  lemma union_set_fold [code]:
1.56    "set xs \<union> A = fold Set.insert xs A"
1.57 @@ -2813,49 +2773,18 @@
1.58    "A \<inter> List.coset xs = fold Set.remove xs A"
1.59    by (simp add: Diff_eq [symmetric] minus_set_fold)
1.60
1.61 -lemma (in lattice) Inf_fin_set_fold:
1.62 -  "Inf_fin (set (x # xs)) = fold inf xs x"
1.63 +lemma (in semilattice_set) set_eq_fold:
1.64 +  "F (set (x # xs)) = fold f xs x"
1.65  proof -
1.66 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.67 -    by (fact ab_semigroup_idem_mult_inf)
1.68 -  show ?thesis
1.69 -    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
1.70 -qed
1.71 -
1.72 -declare Inf_fin_set_fold [code]
1.73 -
1.74 -lemma (in lattice) Sup_fin_set_fold:
1.75 -  "Sup_fin (set (x # xs)) = fold sup xs x"
1.76 -proof -
1.77 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.78 -    by (fact ab_semigroup_idem_mult_sup)
1.79 -  show ?thesis
1.80 -    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
1.81 +  interpret comp_fun_idem f
1.82 +    by default (simp_all add: fun_eq_iff left_commute)
1.83 +  show ?thesis by (simp add: eq_fold fold_set_fold)
1.84  qed
1.85
1.86 -declare Sup_fin_set_fold [code]
1.87 -
1.88 -lemma (in linorder) Min_fin_set_fold:
1.89 -  "Min (set (x # xs)) = fold min xs x"
1.90 -proof -
1.91 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.92 -    by (fact ab_semigroup_idem_mult_min)
1.93 -  show ?thesis
1.94 -    by (simp add: Min_def fold1_set_fold del: set.simps)
1.95 -qed
1.96 -
1.97 -declare Min_fin_set_fold [code]
1.98 -
1.99 -lemma (in linorder) Max_fin_set_fold:
1.100 -  "Max (set (x # xs)) = fold max xs x"
1.101 -proof -
1.102 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.103 -    by (fact ab_semigroup_idem_mult_max)
1.104 -  show ?thesis
1.105 -    by (simp add: Max_def fold1_set_fold del: set.simps)
1.106 -qed
1.107 -
1.108 -declare Max_fin_set_fold [code]
1.109 +declare Inf_fin.set_eq_fold [code]
1.110 +declare Sup_fin.set_eq_fold [code]
1.111 +declare min_max.Inf_fin.set_eq_fold [code]
1.112 +declare min_max.Sup_fin.set_eq_fold [code]
1.113
1.114  lemma (in complete_lattice) Inf_set_fold:
1.115    "Inf (set xs) = fold inf xs top"
1.116 @@ -4915,24 +4844,36 @@
1.117  sets to lists but one should convert in the other direction (via
1.118  @{const set}). *}
1.119
1.120 +subsubsection {* @{text sorted_list_of_set} *}
1.121 +
1.122 +text{* This function maps (finite) linearly ordered sets to sorted
1.123 +lists. Warning: in most cases it is not a good idea to convert from
1.124 +sets to lists but one should convert in the other direction (via
1.125 +@{const set}). *}
1.126 +
1.127 +definition (in linorder) sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
1.128 +  "sorted_list_of_set = folding.F insort []"
1.129 +
1.130 +sublocale linorder < sorted_list_of_set!: folding insort Nil
1.131 +where
1.132 +  "folding.F insort [] = sorted_list_of_set"
1.133 +proof -
1.134 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
1.135 +  show "folding insort" by default (fact comp_fun_commute)
1.136 +  show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
1.137 +qed
1.138 +
1.139  context linorder
1.140  begin
1.141
1.142 -definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
1.143 -"sorted_list_of_set = Finite_Set.fold insort []"
1.144 -
1.145 -lemma sorted_list_of_set_empty [simp]:
1.146 +lemma sorted_list_of_set_empty:
1.147    "sorted_list_of_set {} = []"
1.148 -  by (simp add: sorted_list_of_set_def)
1.149 +  by (fact sorted_list_of_set.empty)
1.150
1.151  lemma sorted_list_of_set_insert [simp]:
1.152    assumes "finite A"
1.153    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
1.154 -proof -
1.155 -  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
1.156 -  from assms show ?thesis
1.157 -    by (simp add: sorted_list_of_set_def fold_insert_remove)
1.158 -qed
1.159 +  using assms by (fact sorted_list_of_set.insert_remove)
1.160
1.161  lemma sorted_list_of_set [simp]:
1.162    "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
1.163 @@ -4943,7 +4884,7 @@
1.164    "sorted_list_of_set (set xs) = sort (remdups xs)"
1.165  proof -
1.166    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
1.167 -  show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
1.168 +  show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
1.169  qed
1.170
1.171  lemma sorted_list_of_set_remove:
```