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

author | haftmann |

Thu, 29 Dec 2011 13:42:21 +0100 | |

changeset 46034 | 773c0c4994df |

parent 46033 | 6fc579c917b8 |

child 46035 | 313be214e40a |

qualified Finite_Set.fold

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Thu Dec 29 13:41:41 2011 +0100 +++ b/src/HOL/List.thy Thu Dec 29 13:42:21 2011 +0100 @@ -2511,11 +2511,11 @@ text {* @{const Finite_Set.fold} and @{const foldl} *} lemma (in comp_fun_commute) fold_set_remdups: - "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)" + "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) lemma (in comp_fun_idem) fold_set: - "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" + "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) lemma (in ab_semigroup_idem_mult) fold1_set: @@ -2530,7 +2530,7 @@ case True with xs show ?thesis by simp next case False - then have "fold1 times (insert y (set ys)) = fold times y (set ys)" + then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" by (simp only: finite_set fold1_eq_fold_idem) with xs show ?thesis by (simp add: fold_set mult_commute) qed