2165 |
2165 |
2166 lemma (in fun_left_comm_idem) fold_set: |
2166 lemma (in fun_left_comm_idem) fold_set: |
2167 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" |
2167 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" |
2168 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) |
2168 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) |
2169 |
2169 |
|
2170 lemma (in ab_semigroup_idem_mult) fold1_set: |
|
2171 assumes "xs \<noteq> []" |
|
2172 shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)" |
|
2173 proof - |
|
2174 interpret fun_left_comm_idem times by (fact fun_left_comm_idem) |
|
2175 from assms obtain y ys where xs: "xs = y # ys" |
|
2176 by (cases xs) auto |
|
2177 show ?thesis |
|
2178 proof (cases "set ys = {}") |
|
2179 case True with xs show ?thesis by simp |
|
2180 next |
|
2181 case False |
|
2182 then have "fold1 times (insert y (set ys)) = fold times y (set ys)" |
|
2183 by (simp only: finite_set fold1_eq_fold_idem) |
|
2184 with xs show ?thesis by (simp add: fold_set mult_commute) |
|
2185 qed |
|
2186 qed |
|
2187 |
|
2188 lemma (in lattice) Inf_fin_set_fold [code_unfold]: |
|
2189 "Inf_fin (set (x # xs)) = foldl inf x xs" |
|
2190 proof - |
|
2191 interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2192 by (fact ab_semigroup_idem_mult_inf) |
|
2193 show ?thesis |
|
2194 by (simp add: Inf_fin_def fold1_set del: set.simps) |
|
2195 qed |
|
2196 |
|
2197 lemma (in lattice) Sup_fin_set_fold [code_unfold]: |
|
2198 "Sup_fin (set (x # xs)) = foldl sup x xs" |
|
2199 proof - |
|
2200 interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2201 by (fact ab_semigroup_idem_mult_sup) |
|
2202 show ?thesis |
|
2203 by (simp add: Sup_fin_def fold1_set del: set.simps) |
|
2204 qed |
|
2205 |
|
2206 lemma (in linorder) Min_fin_set_fold [code_unfold]: |
|
2207 "Min (set (x # xs)) = foldl min x xs" |
|
2208 proof - |
|
2209 interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2210 by (fact ab_semigroup_idem_mult_min) |
|
2211 show ?thesis |
|
2212 by (simp add: Min_def fold1_set del: set.simps) |
|
2213 qed |
|
2214 |
|
2215 lemma (in linorder) Max_fin_set_fold [code_unfold]: |
|
2216 "Max (set (x # xs)) = foldl max x xs" |
|
2217 proof - |
|
2218 interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2219 by (fact ab_semigroup_idem_mult_max) |
|
2220 show ?thesis |
|
2221 by (simp add: Max_def fold1_set del: set.simps) |
|
2222 qed |
|
2223 |
|
2224 lemma (in complete_lattice) Inf_set_fold [code_unfold]: |
|
2225 "Inf (set xs) = foldl inf top xs" |
|
2226 by (cases xs) |
|
2227 (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold |
|
2228 inf_commute del: set.simps, simp add: top_def) |
|
2229 |
|
2230 lemma (in complete_lattice) Sup_set_fold [code_unfold]: |
|
2231 "Sup (set xs) = foldl sup bot xs" |
|
2232 by (cases xs) |
|
2233 (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold |
|
2234 sup_commute del: set.simps, simp add: bot_def) |
2170 |
2235 |
2171 |
2236 |
2172 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
2237 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
2173 |
2238 |
2174 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" |
2239 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" |
3760 by (induct xs) auto |
3825 by (induct xs) auto |
3761 |
3826 |
3762 lemma length_remdups_length_unique [code_unfold]: |
3827 lemma length_remdups_length_unique [code_unfold]: |
3763 "length (remdups xs) = length_unique xs" |
3828 "length (remdups xs) = length_unique xs" |
3764 by (induct xs) simp_all |
3829 by (induct xs) simp_all |
|
3830 |
|
3831 declare INFI_def [code_unfold] |
|
3832 declare SUPR_def [code_unfold] |
|
3833 |
|
3834 declare set_map [symmetric, code_unfold] |
3765 |
3835 |
3766 hide (open) const length_unique |
3836 hide (open) const length_unique |
3767 |
3837 |
3768 |
3838 |
3769 text {* Code for bounded quantification and summation over nats. *} |
3839 text {* Code for bounded quantification and summation over nats. *} |