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```