# HG changeset patch
# User nipkow
# Date 1187626213 -7200
# Node ID 0dd8782fb02dc5b9fe9966e12fd6c6036c5126e0
# Parent  c708ea5b109a83bdfa5b1a9bb5e24e5281a6d225
Final mods for list comprehension

diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Aug 20 18:07:49 2007 +0200
+++ b/src/HOL/Inductive.thy	Mon Aug 20 18:10:13 2007 +0200
@@ -141,8 +141,8 @@
   fun fun_tr ctxt [cs] =
     let
       val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
-      val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
-                 [x, cs]
+      val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
+                 ctxt [x, cs]
     in lambda x ft end
 in [("_lam_pats_syntax", fun_tr)] end
 *}
diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 20 18:07:49 2007 +0200
+++ b/src/HOL/List.thy	Mon Aug 20 18:10:13 2007 +0200
@@ -222,22 +222,30 @@
 
 subsubsection {* List comprehension *}
 
-text{* Input syntax for Haskell-like list comprehension
-notation. Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, the list of all pairs of distinct elements from @{text xs} and @{text ys}.
-
-There are two differences to Haskell.  The general synatx is
-@{text"[e. p \<leftarrow> xs, \<dots>]"} rather than \verb![x| x <- xs, ...]!. Patterns in
-generators can only be tuples (at the moment).
+text{* Input syntax for Haskell-like list comprehension notation.
+Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
+the list of all pairs of distinct elements from @{text xs} and @{text ys}.
+The syntax is as in Haskell, except that @{text"|"} becomes a dot
+(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
+\verb![e| x <- xs, ...]!.
+
+The qualifiers after the dot are
+\begin{description}
+\item[generators] @{text"p \<leftarrow> xs"},
+ where @{text p} is a pattern and @{text xs} an expression of list type,
+\item[guards] @{text"b"}, where @{text b} is a boolean expression, or
+\item[local bindings] @{text"let x = e"}.
+\end{description}
 
 To avoid misunderstandings, the translation is not reversed upon
 output. You can add the inverse translations in your own theory if you
 desire.
 
-Hint: formulae containing complex list comprehensions may become quite
-unreadable after the simplifier has finished with them. It can be
-helpful to introduce definitions for such list comprehensions and
-treat them separately in suitable lemmas.
-*}
+It is easy to write short list comprehensions which stand for complex
+expressions. During proofs, they may become unreadable (and
+mangled). In such cases it can be advisable to introduce separate
+definitions for the list comprehensions in question.  *}
+
 (*
 Proper theorem proving support would be nice. For example, if
 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
@@ -249,28 +257,56 @@
 
 syntax
 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
-"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
+"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
+"_lc_let" :: "letbinds => lc_qual"  ("let _")
 "_lc_end" :: "lc_quals" ("]")
 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
+"_lc_abs" :: "'a => 'b list => 'b list"
 
 translations
-"[e. p<-xs]" => "map (%p. e) xs"
+"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
- => "concat (map (%p. _listcompr e Q Qs) xs)"
+ => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
 "[e. P]" => "if P then [e] else []"
 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
  => "if P then (_listcompr e Q Qs) else []"
+"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
+ => "_Let b (_listcompr e Q Qs)"
 
 syntax (xsymbols)
-"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
 syntax (HTML output)
-"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
-
+"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+
+parse_translation (advanced) {*
+let
+
+   fun abs_tr0 ctxt p es =
+    let
+      val x = Free (Name.variant (add_term_free_names (p$es, [])) "x", dummyT);
+      val case1 = Syntax.const "_case1" $ p $ es;
+      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
+                                        $ Syntax.const @{const_name Nil};
+      val cs = Syntax.const "_case2" $ case1 $ case2
+      val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
+                 ctxt [x, cs]
+    in lambda x ft end;
+
+  fun abs_tr ctxt [x as Free (s, T), r] =
+        let val thy = ProofContext.theory_of ctxt;
+            val s' = Sign.intern_const thy s
+        in if Sign.declared_const thy s' then abs_tr0 ctxt x r else lambda x r
+        end
+   | abs_tr ctxt [p,es] = abs_tr0 ctxt p es
+
+in [("_lc_abs", abs_tr)] end
+*}
 
 (*
 term "[(x,y,z). b]"
-term "[(x,y,z). x \<leftarrow> xs]"
+term "[(x,y). Cons True x \<leftarrow> xs]"
+term "[(x,y,z). Cons x [] \<leftarrow> xs]"
 term "[(x,y,z). x<a, x>b]"
 term "[(x,y,z). x<a, x\<leftarrow>xs]"
 term "[(x,y,z). x\<leftarrow>xs, x>b]"
@@ -283,9 +319,9 @@
 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
+term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
 *)
 
-
 subsubsection {* @{const Nil} and @{const Cons} *}
 
 lemma not_Cons_self [simp]:
@@ -367,7 +403,7 @@
 by (induct xs arbitrary: ys) (case_tac x, auto)+
 
 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
-  by (rule Eq_FalseI) auto
+by (rule Eq_FalseI) auto
 
 simproc_setup list_neq ("(xs::'a list) = ys") = {*
 (*
@@ -835,7 +871,7 @@
 by (induct xs) auto
 
 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
-  by (induct xs) simp_all
+by (induct xs) simp_all
 
 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
 apply (induct xs)
@@ -963,6 +999,9 @@
 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
 by (induct xs) auto
 
+lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs"
+by (induct xs) auto
+
 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
 by (induct xs) auto
 
@@ -1432,12 +1471,12 @@
 lemma takeWhile_cong [fundef_cong, recdef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> takeWhile P l = takeWhile Q k"
-  by (induct k arbitrary: l) (simp_all)
+by (induct k arbitrary: l) (simp_all)
 
 lemma dropWhile_cong [fundef_cong, recdef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> dropWhile P l = dropWhile Q k"
-  by (induct k arbitrary: l, simp_all)
+by (induct k arbitrary: l, simp_all)
 
 
 subsubsection {* @{text zip} *}
@@ -1544,17 +1583,17 @@
 
 lemma list_all2_lengthD [intro?]: 
   "list_all2 P xs ys ==> length xs = length ys"
-  by (simp add: list_all2_def)
+by (simp add: list_all2_def)
 
 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
-  by (simp add: list_all2_def)
+by (simp add: list_all2_def)
 
 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
-  by (simp add: list_all2_def)
+by (simp add: list_all2_def)
 
 lemma list_all2_Cons [iff, code]:
   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
-  by (auto simp add: list_all2_def)
+by (auto simp add: list_all2_def)
 
 lemma list_all2_Cons1:
 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
@@ -1603,7 +1642,7 @@
 
 lemma list_all2_appendI [intro?, trans]:
   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
-  by (simp add: list_all2_append list_all2_lengthD)
+by (simp add: list_all2_append list_all2_lengthD)
 
 lemma list_all2_conv_all_nth:
 "list_all2 P xs ys =
@@ -1626,39 +1665,39 @@
 
 lemma list_all2_all_nthI [intro?]:
   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
-  by (simp add: list_all2_conv_all_nth)
+by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2I:
   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
-  by (simp add: list_all2_def)
+by (simp add: list_all2_def)
 
 lemma list_all2_nthD:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-  by (simp add: list_all2_conv_all_nth)
+by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_nthD2:
   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
+by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
 
 lemma list_all2_map1: 
   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
-  by (simp add: list_all2_conv_all_nth)
+by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_map2: 
   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
-  by (auto simp add: list_all2_conv_all_nth)
+by (auto simp add: list_all2_conv_all_nth)
 
 lemma list_all2_refl [intro?]:
   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
-  by (simp add: list_all2_conv_all_nth)
+by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_update_cong:
   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-  by (simp add: list_all2_conv_all_nth nth_list_update)
+by (simp add: list_all2_conv_all_nth nth_list_update)
 
 lemma list_all2_update_cong2:
   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-  by (simp add: list_all2_lengthD list_all2_update_cong)
+by (simp add: list_all2_lengthD list_all2_update_cong)
 
 lemma list_all2_takeI [simp,intro?]:
   "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
@@ -1684,7 +1723,7 @@
 
 lemma list_all2_eq:
   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
-  by (induct xs ys rule: list_induct2') auto
+by (induct xs ys rule: list_induct2') auto
 
 
 subsubsection {* @{text foldl} and @{text foldr} *}
@@ -1705,12 +1744,12 @@
 lemma foldl_cong [fundef_cong, recdef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   ==> foldl f a l = foldl g b k"
-  by (induct k arbitrary: a b l) simp_all
+by (induct k arbitrary: a b l) simp_all
 
 lemma foldr_cong [fundef_cong, recdef_cong]:
   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   ==> foldr f l a = foldr g k b"
-  by (induct k arbitrary: a b l) simp_all
+by (induct k arbitrary: a b l) simp_all
 
 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
 
@@ -1923,10 +1962,10 @@
 by (induct xs) auto
 
 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
-  by (induct x, auto) 
+by (induct x, auto) 
 
 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
-  by (induct x, auto)
+by (induct x, auto)
 
 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
 by (induct xs) auto
@@ -2008,7 +2047,7 @@
 by(auto simp: distinct_conv_nth)
 
 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
 proof (induct xs)
@@ -2371,13 +2410,13 @@
 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
 
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
-  by (clarify, erule listsp.induct, blast+)
+by (clarify, erule listsp.induct, blast+)
 
 lemmas lists_mono = listsp_mono [to_set]
 
 lemma listsp_infI:
   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
-  by induct blast+
+by induct blast+
 
 lemmas lists_IntI = listsp_infI [to_set]
 
@@ -2556,10 +2595,10 @@
             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
-  by (unfold lexord_def, induct_tac y, auto) 
+by (unfold lexord_def, induct_tac y, auto) 
 
 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
-  by (unfold lexord_def, induct_tac x, auto)
+by (unfold lexord_def, induct_tac x, auto)
 
 lemma lexord_cons_cons[simp]:
      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
@@ -2572,18 +2611,18 @@
 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
 
 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
-  by (induct_tac x, auto)  
+by (induct_tac x, auto)  
 
 lemma lexord_append_left_rightI:
      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
-  by (induct_tac u, auto)
+by (induct_tac u, auto)
 
 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
-  by (induct x, auto)
+by (induct x, auto)
 
 lemma lexord_append_leftD:
      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
-  by (erule rev_mp, induct_tac x, auto)
+by (erule rev_mp, induct_tac x, auto)
 
 lemma lexord_take_index_conv: 
    "((x,y) : lexord r) = 
@@ -2629,7 +2668,7 @@
   by blast
 
 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
-  by (rule transI, drule lexord_trans, blast) 
+by (rule transI, drule lexord_trans, blast) 
 
 lemma lexord_linear: "(! a b. (a,b)\<in> r | a = b | (b,a) \<in> r) \<Longrightarrow> (x,y) : lexord r | x = y | (y,x) : lexord r"
   apply (rule_tac x = y in spec) 
@@ -2647,21 +2686,21 @@
   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
 
 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
-  unfolding measures_def
-  by blast
+unfolding measures_def
+by blast
 
 lemma in_measures[simp]: 
   "(x, y) \<in> measures [] = False"
   "(x, y) \<in> measures (f # fs)
          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
-  unfolding measures_def
-  by auto
+unfolding measures_def
+by auto
 
 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
-  by simp
+by simp
 
 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
-  by auto
+by auto
 
 (* install the lexicographic_order method and the "fun" command *)
 use "Tools/function_package/lexicographic_order.ML"
@@ -2899,34 +2938,34 @@
 
 lemma mem_iff [code post]:
   "x mem xs \<longleftrightarrow> x \<in> set xs"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemmas in_set_code [code unfold] = mem_iff [symmetric]
 
 lemma empty_null [code inline]:
   "xs = [] \<longleftrightarrow> null xs"
-  by (cases xs) simp_all
+by (cases xs) simp_all
 
 lemmas null_empty [code post] =
   empty_null [symmetric]
 
 lemma list_inter_conv:
   "set (list_inter xs ys) = set xs \<inter> set ys"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemma list_all_iff [code post]:
   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
 
 lemma list_all_append [simp]:
   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemma list_all_rev [simp]:
   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
-  by (simp add: list_all_iff)
+by (simp add: list_all_iff)
 
 lemma list_all_length:
   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
@@ -2934,7 +2973,7 @@
 
 lemma list_ex_iff [code post]:
   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
-  by (induct xs) simp_all
+by (induct xs) simp_all
 
 lemmas list_bex_code [code unfold] =
   list_ex_iff [symmetric]
@@ -2945,57 +2984,57 @@
 
 lemma filtermap_conv:
    "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
-  by (induct xs) (simp_all split: option.split) 
+by (induct xs) (simp_all split: option.split) 
 
 lemma map_filter_conv [simp]:
   "map_filter f P xs = map f (filter P xs)"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
-  by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
+by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
 
 
 text {* Code for bounded quantification over nats. *}
 
 lemma atMost_upto [code unfold]:
   "{..n} = set [0..n]"
-  by auto
+by auto
 
 lemma atLeast_upt [code unfold]:
   "{..<n} = set [0..<n]"
-  by auto
+by auto
 
 lemma greaterThanLessThan_upd [code unfold]:
   "{n<..<m} = set [Suc n..<m]"
-  by auto
+by auto
 
 lemma atLeastLessThan_upd [code unfold]:
   "{n..<m} = set [n..<m]"
-  by auto
+by auto
 
 lemma greaterThanAtMost_upto [code unfold]:
   "{n<..m} = set [Suc n..m]"
-  by auto
+by auto
 
 lemma atLeastAtMost_upto [code unfold]:
   "{n..m} = set [n..m]"
-  by auto
+by auto
 
 lemma all_nat_less_eq [code unfold]:
   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
-  by auto
+by auto
 
 lemma ex_nat_less_eq [code unfold]:
   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
-  by auto
+by auto
 
 lemma all_nat_less [code unfold]:
   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
-  by auto
+by auto
 
 lemma ex_nat_less [code unfold]:
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
-  by auto
+by auto
 
 lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
 by (induct xs, simp_all)
@@ -3006,7 +3045,8 @@
 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@ 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)
@@ -3057,11 +3097,11 @@
 
 lemma partition_filter1:
     "fst (partition P xs) = filter P xs"
-  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
+by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
 
 lemma partition_filter2:
     "snd (partition P xs) = filter (Not o P) xs"
-  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
+by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
 
 lemma partition_set:
   assumes "partition P xs = (yes, no)"
diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Mon Aug 20 18:07:49 2007 +0200
+++ b/src/HOL/Tools/datatype_case.ML	Mon Aug 20 18:10:13 2007 +0200
@@ -15,8 +15,8 @@
     string list -> term -> (term * (term * term) list) option
   val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
     term -> (term * (term * term) list) option
-  val case_tr: (theory -> string -> DatatypeAux.datatype_info option) ->
-    Proof.context -> term list -> term
+  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
+    -> Proof.context -> term list -> term
   val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
     string -> Proof.context -> term list -> term
 end;
@@ -304,7 +304,7 @@
 
 (* parse translation *)
 
-fun case_tr tab_of ctxt [t, u] =
+fun case_tr err tab_of ctxt [t, u] =
     let
       val thy = ProofContext.theory_of ctxt;
       (* replace occurrences of dummy_pattern by distinct variables *)
@@ -343,11 +343,11 @@
       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
         | dest_case2 t = [t];
       val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
-      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt true []
+      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
         (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
            (flat cnstrts) t) cases;
     in case_tm end
-  | case_tr _ _ ts = case_error "case_tr";
+  | case_tr _ _ _ ts = case_error "case_tr";
 
 
 (*---------------------------------------------------------------------------
diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Aug 20 18:07:49 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 20 18:10:13 2007 +0200
@@ -433,7 +433,7 @@
 
 val trfun_setup =
   Theory.add_advanced_trfuns ([],
-    [("_case_syntax", DatatypeCase.case_tr datatype_of_constr)],
+    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
     [], []);
 
 
diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:07:49 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:10:13 2007 +0200
@@ -1770,8 +1770,8 @@
     using mirror[OF lp, where x="- x", symmetric] by auto
   thus "\<exists> x. ?I x ?mp" by blast
 qed
-  
-  
+
+
 lemma cp_thm': 
   assumes lp: "iszlfm p"
   and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
@@ -1856,7 +1856,6 @@
   shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
   (is "(?lhs = ?rhs) \<and> _")
 proof-
-
   let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
   let ?q = "fst (unit p)"
   let ?B = "fst (snd(unit p))"
@@ -1903,7 +1902,7 @@
   also have "\<dots> = (?I i (evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))" 
    by (simp only: evaldjf_ex subst0_I[OF qfq])
  also have "\<dots>= (?I i ?md \<or> (\<exists> (b,j) \<in> set ?Bjs. (\<lambda> (b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
-   by (simp only: simpfm set_concat set_map UN_simps) blast
+   by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
    by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) (auto simp add: split_def)
  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp