Final mods for list comprehension
authornipkow
Mon Aug 20 18:10:13 2007 +0200 (2007-08-20)
changeset 243490dd8782fb02d
parent 24348 c708ea5b109a
child 24350 4d74f37c6367
Final mods for list comprehension
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/datatype_package.ML
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Inductive.thy	Mon Aug 20 18:07:49 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Mon Aug 20 18:10:13 2007 +0200
     1.3 @@ -141,8 +141,8 @@
     1.4    fun fun_tr ctxt [cs] =
     1.5      let
     1.6        val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
     1.7 -      val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
     1.8 -                 [x, cs]
     1.9 +      val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
    1.10 +                 ctxt [x, cs]
    1.11      in lambda x ft end
    1.12  in [("_lam_pats_syntax", fun_tr)] end
    1.13  *}
     2.1 --- a/src/HOL/List.thy	Mon Aug 20 18:07:49 2007 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Aug 20 18:10:13 2007 +0200
     2.3 @@ -222,22 +222,30 @@
     2.4  
     2.5  subsubsection {* List comprehension *}
     2.6  
     2.7 -text{* Input syntax for Haskell-like list comprehension
     2.8 -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}.
     2.9 -
    2.10 -There are two differences to Haskell.  The general synatx is
    2.11 -@{text"[e. p \<leftarrow> xs, \<dots>]"} rather than \verb![x| x <- xs, ...]!. Patterns in
    2.12 -generators can only be tuples (at the moment).
    2.13 +text{* Input syntax for Haskell-like list comprehension notation.
    2.14 +Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
    2.15 +the list of all pairs of distinct elements from @{text xs} and @{text ys}.
    2.16 +The syntax is as in Haskell, except that @{text"|"} becomes a dot
    2.17 +(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
    2.18 +\verb![e| x <- xs, ...]!.
    2.19 +
    2.20 +The qualifiers after the dot are
    2.21 +\begin{description}
    2.22 +\item[generators] @{text"p \<leftarrow> xs"},
    2.23 + where @{text p} is a pattern and @{text xs} an expression of list type,
    2.24 +\item[guards] @{text"b"}, where @{text b} is a boolean expression, or
    2.25 +\item[local bindings] @{text"let x = e"}.
    2.26 +\end{description}
    2.27  
    2.28  To avoid misunderstandings, the translation is not reversed upon
    2.29  output. You can add the inverse translations in your own theory if you
    2.30  desire.
    2.31  
    2.32 -Hint: formulae containing complex list comprehensions may become quite
    2.33 -unreadable after the simplifier has finished with them. It can be
    2.34 -helpful to introduce definitions for such list comprehensions and
    2.35 -treat them separately in suitable lemmas.
    2.36 -*}
    2.37 +It is easy to write short list comprehensions which stand for complex
    2.38 +expressions. During proofs, they may become unreadable (and
    2.39 +mangled). In such cases it can be advisable to introduce separate
    2.40 +definitions for the list comprehensions in question.  *}
    2.41 +
    2.42  (*
    2.43  Proper theorem proving support would be nice. For example, if
    2.44  @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
    2.45 @@ -249,28 +257,56 @@
    2.46  
    2.47  syntax
    2.48  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    2.49 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
    2.50 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
    2.51  "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
    2.52 +"_lc_let" :: "letbinds => lc_qual"  ("let _")
    2.53  "_lc_end" :: "lc_quals" ("]")
    2.54  "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
    2.55 +"_lc_abs" :: "'a => 'b list => 'b list"
    2.56  
    2.57  translations
    2.58 -"[e. p<-xs]" => "map (%p. e) xs"
    2.59 +"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
    2.60  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
    2.61 - => "concat (map (%p. _listcompr e Q Qs) xs)"
    2.62 + => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
    2.63  "[e. P]" => "if P then [e] else []"
    2.64  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
    2.65   => "if P then (_listcompr e Q Qs) else []"
    2.66 +"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
    2.67 + => "_Let b (_listcompr e Q Qs)"
    2.68  
    2.69  syntax (xsymbols)
    2.70 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    2.71 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    2.72  syntax (HTML output)
    2.73 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    2.74 -
    2.75 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    2.76 +
    2.77 +parse_translation (advanced) {*
    2.78 +let
    2.79 +
    2.80 +   fun abs_tr0 ctxt p es =
    2.81 +    let
    2.82 +      val x = Free (Name.variant (add_term_free_names (p$es, [])) "x", dummyT);
    2.83 +      val case1 = Syntax.const "_case1" $ p $ es;
    2.84 +      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
    2.85 +                                        $ Syntax.const @{const_name Nil};
    2.86 +      val cs = Syntax.const "_case2" $ case1 $ case2
    2.87 +      val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
    2.88 +                 ctxt [x, cs]
    2.89 +    in lambda x ft end;
    2.90 +
    2.91 +  fun abs_tr ctxt [x as Free (s, T), r] =
    2.92 +        let val thy = ProofContext.theory_of ctxt;
    2.93 +            val s' = Sign.intern_const thy s
    2.94 +        in if Sign.declared_const thy s' then abs_tr0 ctxt x r else lambda x r
    2.95 +        end
    2.96 +   | abs_tr ctxt [p,es] = abs_tr0 ctxt p es
    2.97 +
    2.98 +in [("_lc_abs", abs_tr)] end
    2.99 +*}
   2.100  
   2.101  (*
   2.102  term "[(x,y,z). b]"
   2.103 -term "[(x,y,z). x \<leftarrow> xs]"
   2.104 +term "[(x,y). Cons True x \<leftarrow> xs]"
   2.105 +term "[(x,y,z). Cons x [] \<leftarrow> xs]"
   2.106  term "[(x,y,z). x<a, x>b]"
   2.107  term "[(x,y,z). x<a, x\<leftarrow>xs]"
   2.108  term "[(x,y,z). x\<leftarrow>xs, x>b]"
   2.109 @@ -283,9 +319,9 @@
   2.110  term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
   2.111  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
   2.112  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
   2.113 +term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
   2.114  *)
   2.115  
   2.116 -
   2.117  subsubsection {* @{const Nil} and @{const Cons} *}
   2.118  
   2.119  lemma not_Cons_self [simp]:
   2.120 @@ -367,7 +403,7 @@
   2.121  by (induct xs arbitrary: ys) (case_tac x, auto)+
   2.122  
   2.123  lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
   2.124 -  by (rule Eq_FalseI) auto
   2.125 +by (rule Eq_FalseI) auto
   2.126  
   2.127  simproc_setup list_neq ("(xs::'a list) = ys") = {*
   2.128  (*
   2.129 @@ -835,7 +871,7 @@
   2.130  by (induct xs) auto
   2.131  
   2.132  lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
   2.133 -  by (induct xs) simp_all
   2.134 +by (induct xs) simp_all
   2.135  
   2.136  lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
   2.137  apply (induct xs)
   2.138 @@ -963,6 +999,9 @@
   2.139  lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
   2.140  by (induct xs) auto
   2.141  
   2.142 +lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs"
   2.143 +by (induct xs) auto
   2.144 +
   2.145  lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
   2.146  by (induct xs) auto
   2.147  
   2.148 @@ -1432,12 +1471,12 @@
   2.149  lemma takeWhile_cong [fundef_cong, recdef_cong]:
   2.150    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   2.151    ==> takeWhile P l = takeWhile Q k"
   2.152 -  by (induct k arbitrary: l) (simp_all)
   2.153 +by (induct k arbitrary: l) (simp_all)
   2.154  
   2.155  lemma dropWhile_cong [fundef_cong, recdef_cong]:
   2.156    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   2.157    ==> dropWhile P l = dropWhile Q k"
   2.158 -  by (induct k arbitrary: l, simp_all)
   2.159 +by (induct k arbitrary: l, simp_all)
   2.160  
   2.161  
   2.162  subsubsection {* @{text zip} *}
   2.163 @@ -1544,17 +1583,17 @@
   2.164  
   2.165  lemma list_all2_lengthD [intro?]: 
   2.166    "list_all2 P xs ys ==> length xs = length ys"
   2.167 -  by (simp add: list_all2_def)
   2.168 +by (simp add: list_all2_def)
   2.169  
   2.170  lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
   2.171 -  by (simp add: list_all2_def)
   2.172 +by (simp add: list_all2_def)
   2.173  
   2.174  lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
   2.175 -  by (simp add: list_all2_def)
   2.176 +by (simp add: list_all2_def)
   2.177  
   2.178  lemma list_all2_Cons [iff, code]:
   2.179    "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
   2.180 -  by (auto simp add: list_all2_def)
   2.181 +by (auto simp add: list_all2_def)
   2.182  
   2.183  lemma list_all2_Cons1:
   2.184  "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
   2.185 @@ -1603,7 +1642,7 @@
   2.186  
   2.187  lemma list_all2_appendI [intro?, trans]:
   2.188    "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
   2.189 -  by (simp add: list_all2_append list_all2_lengthD)
   2.190 +by (simp add: list_all2_append list_all2_lengthD)
   2.191  
   2.192  lemma list_all2_conv_all_nth:
   2.193  "list_all2 P xs ys =
   2.194 @@ -1626,39 +1665,39 @@
   2.195  
   2.196  lemma list_all2_all_nthI [intro?]:
   2.197    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   2.198 -  by (simp add: list_all2_conv_all_nth)
   2.199 +by (simp add: list_all2_conv_all_nth)
   2.200  
   2.201  lemma list_all2I:
   2.202    "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
   2.203 -  by (simp add: list_all2_def)
   2.204 +by (simp add: list_all2_def)
   2.205  
   2.206  lemma list_all2_nthD:
   2.207    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   2.208 -  by (simp add: list_all2_conv_all_nth)
   2.209 +by (simp add: list_all2_conv_all_nth)
   2.210  
   2.211  lemma list_all2_nthD2:
   2.212    "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   2.213 -  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   2.214 +by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   2.215  
   2.216  lemma list_all2_map1: 
   2.217    "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
   2.218 -  by (simp add: list_all2_conv_all_nth)
   2.219 +by (simp add: list_all2_conv_all_nth)
   2.220  
   2.221  lemma list_all2_map2: 
   2.222    "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
   2.223 -  by (auto simp add: list_all2_conv_all_nth)
   2.224 +by (auto simp add: list_all2_conv_all_nth)
   2.225  
   2.226  lemma list_all2_refl [intro?]:
   2.227    "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
   2.228 -  by (simp add: list_all2_conv_all_nth)
   2.229 +by (simp add: list_all2_conv_all_nth)
   2.230  
   2.231  lemma list_all2_update_cong:
   2.232    "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
   2.233 -  by (simp add: list_all2_conv_all_nth nth_list_update)
   2.234 +by (simp add: list_all2_conv_all_nth nth_list_update)
   2.235  
   2.236  lemma list_all2_update_cong2:
   2.237    "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
   2.238 -  by (simp add: list_all2_lengthD list_all2_update_cong)
   2.239 +by (simp add: list_all2_lengthD list_all2_update_cong)
   2.240  
   2.241  lemma list_all2_takeI [simp,intro?]:
   2.242    "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
   2.243 @@ -1684,7 +1723,7 @@
   2.244  
   2.245  lemma list_all2_eq:
   2.246    "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
   2.247 -  by (induct xs ys rule: list_induct2') auto
   2.248 +by (induct xs ys rule: list_induct2') auto
   2.249  
   2.250  
   2.251  subsubsection {* @{text foldl} and @{text foldr} *}
   2.252 @@ -1705,12 +1744,12 @@
   2.253  lemma foldl_cong [fundef_cong, recdef_cong]:
   2.254    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   2.255    ==> foldl f a l = foldl g b k"
   2.256 -  by (induct k arbitrary: a b l) simp_all
   2.257 +by (induct k arbitrary: a b l) simp_all
   2.258  
   2.259  lemma foldr_cong [fundef_cong, recdef_cong]:
   2.260    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   2.261    ==> foldr f l a = foldr g k b"
   2.262 -  by (induct k arbitrary: a b l) simp_all
   2.263 +by (induct k arbitrary: a b l) simp_all
   2.264  
   2.265  text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
   2.266  
   2.267 @@ -1923,10 +1962,10 @@
   2.268  by (induct xs) auto
   2.269  
   2.270  lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
   2.271 -  by (induct x, auto) 
   2.272 +by (induct x, auto) 
   2.273  
   2.274  lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
   2.275 -  by (induct x, auto)
   2.276 +by (induct x, auto)
   2.277  
   2.278  lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
   2.279  by (induct xs) auto
   2.280 @@ -2008,7 +2047,7 @@
   2.281  by(auto simp: distinct_conv_nth)
   2.282  
   2.283  lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
   2.284 -  by (induct xs) auto
   2.285 +by (induct xs) auto
   2.286  
   2.287  lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
   2.288  proof (induct xs)
   2.289 @@ -2371,13 +2410,13 @@
   2.290  inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
   2.291  
   2.292  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
   2.293 -  by (clarify, erule listsp.induct, blast+)
   2.294 +by (clarify, erule listsp.induct, blast+)
   2.295  
   2.296  lemmas lists_mono = listsp_mono [to_set]
   2.297  
   2.298  lemma listsp_infI:
   2.299    assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
   2.300 -  by induct blast+
   2.301 +by induct blast+
   2.302  
   2.303  lemmas lists_IntI = listsp_infI [to_set]
   2.304  
   2.305 @@ -2556,10 +2595,10 @@
   2.306              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   2.307  
   2.308  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
   2.309 -  by (unfold lexord_def, induct_tac y, auto) 
   2.310 +by (unfold lexord_def, induct_tac y, auto) 
   2.311  
   2.312  lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
   2.313 -  by (unfold lexord_def, induct_tac x, auto)
   2.314 +by (unfold lexord_def, induct_tac x, auto)
   2.315  
   2.316  lemma lexord_cons_cons[simp]:
   2.317       "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
   2.318 @@ -2572,18 +2611,18 @@
   2.319  lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
   2.320  
   2.321  lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
   2.322 -  by (induct_tac x, auto)  
   2.323 +by (induct_tac x, auto)  
   2.324  
   2.325  lemma lexord_append_left_rightI:
   2.326       "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
   2.327 -  by (induct_tac u, auto)
   2.328 +by (induct_tac u, auto)
   2.329  
   2.330  lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
   2.331 -  by (induct x, auto)
   2.332 +by (induct x, auto)
   2.333  
   2.334  lemma lexord_append_leftD:
   2.335       "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
   2.336 -  by (erule rev_mp, induct_tac x, auto)
   2.337 +by (erule rev_mp, induct_tac x, auto)
   2.338  
   2.339  lemma lexord_take_index_conv: 
   2.340     "((x,y) : lexord r) = 
   2.341 @@ -2629,7 +2668,7 @@
   2.342    by blast
   2.343  
   2.344  lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
   2.345 -  by (rule transI, drule lexord_trans, blast) 
   2.346 +by (rule transI, drule lexord_trans, blast) 
   2.347  
   2.348  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"
   2.349    apply (rule_tac x = y in spec) 
   2.350 @@ -2647,21 +2686,21 @@
   2.351    "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
   2.352  
   2.353  lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
   2.354 -  unfolding measures_def
   2.355 -  by blast
   2.356 +unfolding measures_def
   2.357 +by blast
   2.358  
   2.359  lemma in_measures[simp]: 
   2.360    "(x, y) \<in> measures [] = False"
   2.361    "(x, y) \<in> measures (f # fs)
   2.362           = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
   2.363 -  unfolding measures_def
   2.364 -  by auto
   2.365 +unfolding measures_def
   2.366 +by auto
   2.367  
   2.368  lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
   2.369 -  by simp
   2.370 +by simp
   2.371  
   2.372  lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
   2.373 -  by auto
   2.374 +by auto
   2.375  
   2.376  (* install the lexicographic_order method and the "fun" command *)
   2.377  use "Tools/function_package/lexicographic_order.ML"
   2.378 @@ -2899,34 +2938,34 @@
   2.379  
   2.380  lemma mem_iff [code post]:
   2.381    "x mem xs \<longleftrightarrow> x \<in> set xs"
   2.382 -  by (induct xs) auto
   2.383 +by (induct xs) auto
   2.384  
   2.385  lemmas in_set_code [code unfold] = mem_iff [symmetric]
   2.386  
   2.387  lemma empty_null [code inline]:
   2.388    "xs = [] \<longleftrightarrow> null xs"
   2.389 -  by (cases xs) simp_all
   2.390 +by (cases xs) simp_all
   2.391  
   2.392  lemmas null_empty [code post] =
   2.393    empty_null [symmetric]
   2.394  
   2.395  lemma list_inter_conv:
   2.396    "set (list_inter xs ys) = set xs \<inter> set ys"
   2.397 -  by (induct xs) auto
   2.398 +by (induct xs) auto
   2.399  
   2.400  lemma list_all_iff [code post]:
   2.401    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   2.402 -  by (induct xs) auto
   2.403 +by (induct xs) auto
   2.404  
   2.405  lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
   2.406  
   2.407  lemma list_all_append [simp]:
   2.408    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   2.409 -  by (induct xs) auto
   2.410 +by (induct xs) auto
   2.411  
   2.412  lemma list_all_rev [simp]:
   2.413    "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
   2.414 -  by (simp add: list_all_iff)
   2.415 +by (simp add: list_all_iff)
   2.416  
   2.417  lemma list_all_length:
   2.418    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   2.419 @@ -2934,7 +2973,7 @@
   2.420  
   2.421  lemma list_ex_iff [code post]:
   2.422    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   2.423 -  by (induct xs) simp_all
   2.424 +by (induct xs) simp_all
   2.425  
   2.426  lemmas list_bex_code [code unfold] =
   2.427    list_ex_iff [symmetric]
   2.428 @@ -2945,57 +2984,57 @@
   2.429  
   2.430  lemma filtermap_conv:
   2.431     "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
   2.432 -  by (induct xs) (simp_all split: option.split) 
   2.433 +by (induct xs) (simp_all split: option.split) 
   2.434  
   2.435  lemma map_filter_conv [simp]:
   2.436    "map_filter f P xs = map f (filter P xs)"
   2.437 -  by (induct xs) auto
   2.438 +by (induct xs) auto
   2.439  
   2.440  lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
   2.441 -  by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
   2.442 +by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
   2.443  
   2.444  
   2.445  text {* Code for bounded quantification over nats. *}
   2.446  
   2.447  lemma atMost_upto [code unfold]:
   2.448    "{..n} = set [0..n]"
   2.449 -  by auto
   2.450 +by auto
   2.451  
   2.452  lemma atLeast_upt [code unfold]:
   2.453    "{..<n} = set [0..<n]"
   2.454 -  by auto
   2.455 +by auto
   2.456  
   2.457  lemma greaterThanLessThan_upd [code unfold]:
   2.458    "{n<..<m} = set [Suc n..<m]"
   2.459 -  by auto
   2.460 +by auto
   2.461  
   2.462  lemma atLeastLessThan_upd [code unfold]:
   2.463    "{n..<m} = set [n..<m]"
   2.464 -  by auto
   2.465 +by auto
   2.466  
   2.467  lemma greaterThanAtMost_upto [code unfold]:
   2.468    "{n<..m} = set [Suc n..m]"
   2.469 -  by auto
   2.470 +by auto
   2.471  
   2.472  lemma atLeastAtMost_upto [code unfold]:
   2.473    "{n..m} = set [n..m]"
   2.474 -  by auto
   2.475 +by auto
   2.476  
   2.477  lemma all_nat_less_eq [code unfold]:
   2.478    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
   2.479 -  by auto
   2.480 +by auto
   2.481  
   2.482  lemma ex_nat_less_eq [code unfold]:
   2.483    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
   2.484 -  by auto
   2.485 +by auto
   2.486  
   2.487  lemma all_nat_less [code unfold]:
   2.488    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
   2.489 -  by auto
   2.490 +by auto
   2.491  
   2.492  lemma ex_nat_less [code unfold]:
   2.493    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   2.494 -  by auto
   2.495 +by auto
   2.496  
   2.497  lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
   2.498  by (induct xs, simp_all)
   2.499 @@ -3006,7 +3045,8 @@
   2.500  next
   2.501    case (Cons x xs ss)
   2.502    have "set (foldl op @ ss (map f (x # xs))) = set (foldl op @ (ss @ f x) (map f xs))" by simp
   2.503 -  also have "\<dots> = set (ss@ f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" using prems  by simp
   2.504 +  also have "\<dots> = set (ss@ f x) \<union> UNION (set xs) (\<lambda>x. set (f x))"
   2.505 +    using prems by simp
   2.506    also have "\<dots>= set ss \<union> set (f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" by simp
   2.507    also have "\<dots> = set ss \<union> UNION (set (x#xs)) (\<lambda>x. set (f x))"
   2.508      by (simp add: Un_assoc)
   2.509 @@ -3057,11 +3097,11 @@
   2.510  
   2.511  lemma partition_filter1:
   2.512      "fst (partition P xs) = filter P xs"
   2.513 -  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   2.514 +by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   2.515  
   2.516  lemma partition_filter2:
   2.517      "snd (partition P xs) = filter (Not o P) xs"
   2.518 -  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   2.519 +by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   2.520  
   2.521  lemma partition_set:
   2.522    assumes "partition P xs = (yes, no)"
     3.1 --- a/src/HOL/Tools/datatype_case.ML	Mon Aug 20 18:07:49 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_case.ML	Mon Aug 20 18:10:13 2007 +0200
     3.3 @@ -15,8 +15,8 @@
     3.4      string list -> term -> (term * (term * term) list) option
     3.5    val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
     3.6      term -> (term * (term * term) list) option
     3.7 -  val case_tr: (theory -> string -> DatatypeAux.datatype_info option) ->
     3.8 -    Proof.context -> term list -> term
     3.9 +  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
    3.10 +    -> Proof.context -> term list -> term
    3.11    val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
    3.12      string -> Proof.context -> term list -> term
    3.13  end;
    3.14 @@ -304,7 +304,7 @@
    3.15  
    3.16  (* parse translation *)
    3.17  
    3.18 -fun case_tr tab_of ctxt [t, u] =
    3.19 +fun case_tr err tab_of ctxt [t, u] =
    3.20      let
    3.21        val thy = ProofContext.theory_of ctxt;
    3.22        (* replace occurrences of dummy_pattern by distinct variables *)
    3.23 @@ -343,11 +343,11 @@
    3.24        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
    3.25          | dest_case2 t = [t];
    3.26        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
    3.27 -      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt true []
    3.28 +      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
    3.29          (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
    3.30             (flat cnstrts) t) cases;
    3.31      in case_tm end
    3.32 -  | case_tr _ _ ts = case_error "case_tr";
    3.33 +  | case_tr _ _ _ ts = case_error "case_tr";
    3.34  
    3.35  
    3.36  (*---------------------------------------------------------------------------
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Aug 20 18:07:49 2007 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 20 18:10:13 2007 +0200
     4.3 @@ -433,7 +433,7 @@
     4.4  
     4.5  val trfun_setup =
     4.6    Theory.add_advanced_trfuns ([],
     4.7 -    [("_case_syntax", DatatypeCase.case_tr datatype_of_constr)],
     4.8 +    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
     4.9      [], []);
    4.10  
    4.11  
     5.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:07:49 2007 +0200
     5.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:10:13 2007 +0200
     5.3 @@ -1770,8 +1770,8 @@
     5.4      using mirror[OF lp, where x="- x", symmetric] by auto
     5.5    thus "\<exists> x. ?I x ?mp" by blast
     5.6  qed
     5.7 -  
     5.8 -  
     5.9 +
    5.10 +
    5.11  lemma cp_thm': 
    5.12    assumes lp: "iszlfm p"
    5.13    and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
    5.14 @@ -1856,7 +1856,6 @@
    5.15    shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
    5.16    (is "(?lhs = ?rhs) \<and> _")
    5.17  proof-
    5.18 -
    5.19    let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
    5.20    let ?q = "fst (unit p)"
    5.21    let ?B = "fst (snd(unit p))"
    5.22 @@ -1903,7 +1902,7 @@
    5.23    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)))" 
    5.24     by (simp only: evaldjf_ex subst0_I[OF qfq])
    5.25   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)))"
    5.26 -   by (simp only: simpfm set_concat set_map UN_simps) blast
    5.27 +   by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
    5.28   also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
    5.29     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)
    5.30   finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp