# HG changeset patch
# User chaieb
# Date 1181034004 -7200
# Node ID 57aee3d85ff33ff43b9381917d4c3d68fef82644
# Parent  1630951f0512e8957738beaace46ee4578f40299
added a few theorems about foldl and set

diff -r 1630951f0512 -r 57aee3d85ff3 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 05 10:42:31 2007 +0200
+++ b/src/HOL/List.thy	Tue Jun 05 11:00:04 2007 +0200
@@ -3031,4 +3031,24 @@
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   by auto
 
+lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
+by (induct xs, simp_all)
+
+lemma foldl_append_map_set: "\<And> ss. set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))"
+proof(induct xs)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs ss)
+  have "set (foldl op @ ss (map f (x # xs))) = set (foldl op @ (ss @ f x) (map f xs))" by simp
+  also have "\<dots> = set (ss@ f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" using prems  by simp
+  also have "\<dots>= set ss \<union> set (f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" by simp
+  also have "\<dots> = set ss \<union> UNION (set (x#xs)) (\<lambda>x. set (f x))"
+    by (simp add: Un_assoc)
+  finally show ?case by simp
+qed
+
+lemma foldl_append_map_Nil_set: 
+  "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))"
+using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp
+
 end
\ No newline at end of file