src/HOL/List.thy
changeset 24349 0dd8782fb02d
parent 24335 21b4350cf5ec
child 24449 2f05cb7fed85
     1.1 --- a/src/HOL/List.thy	Mon Aug 20 18:07:49 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Aug 20 18:10:13 2007 +0200
     1.3 @@ -222,22 +222,30 @@
     1.4  
     1.5  subsubsection {* List comprehension *}
     1.6  
     1.7 -text{* Input syntax for Haskell-like list comprehension
     1.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}.
     1.9 -
    1.10 -There are two differences to Haskell.  The general synatx is
    1.11 -@{text"[e. p \<leftarrow> xs, \<dots>]"} rather than \verb![x| x <- xs, ...]!. Patterns in
    1.12 -generators can only be tuples (at the moment).
    1.13 +text{* Input syntax for Haskell-like list comprehension notation.
    1.14 +Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
    1.15 +the list of all pairs of distinct elements from @{text xs} and @{text ys}.
    1.16 +The syntax is as in Haskell, except that @{text"|"} becomes a dot
    1.17 +(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
    1.18 +\verb![e| x <- xs, ...]!.
    1.19 +
    1.20 +The qualifiers after the dot are
    1.21 +\begin{description}
    1.22 +\item[generators] @{text"p \<leftarrow> xs"},
    1.23 + where @{text p} is a pattern and @{text xs} an expression of list type,
    1.24 +\item[guards] @{text"b"}, where @{text b} is a boolean expression, or
    1.25 +\item[local bindings] @{text"let x = e"}.
    1.26 +\end{description}
    1.27  
    1.28  To avoid misunderstandings, the translation is not reversed upon
    1.29  output. You can add the inverse translations in your own theory if you
    1.30  desire.
    1.31  
    1.32 -Hint: formulae containing complex list comprehensions may become quite
    1.33 -unreadable after the simplifier has finished with them. It can be
    1.34 -helpful to introduce definitions for such list comprehensions and
    1.35 -treat them separately in suitable lemmas.
    1.36 -*}
    1.37 +It is easy to write short list comprehensions which stand for complex
    1.38 +expressions. During proofs, they may become unreadable (and
    1.39 +mangled). In such cases it can be advisable to introduce separate
    1.40 +definitions for the list comprehensions in question.  *}
    1.41 +
    1.42  (*
    1.43  Proper theorem proving support would be nice. For example, if
    1.44  @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
    1.45 @@ -249,28 +257,56 @@
    1.46  
    1.47  syntax
    1.48  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    1.49 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
    1.50 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
    1.51  "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
    1.52 +"_lc_let" :: "letbinds => lc_qual"  ("let _")
    1.53  "_lc_end" :: "lc_quals" ("]")
    1.54  "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
    1.55 +"_lc_abs" :: "'a => 'b list => 'b list"
    1.56  
    1.57  translations
    1.58 -"[e. p<-xs]" => "map (%p. e) xs"
    1.59 +"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
    1.60  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
    1.61 - => "concat (map (%p. _listcompr e Q Qs) xs)"
    1.62 + => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
    1.63  "[e. P]" => "if P then [e] else []"
    1.64  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
    1.65   => "if P then (_listcompr e Q Qs) else []"
    1.66 +"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
    1.67 + => "_Let b (_listcompr e Q Qs)"
    1.68  
    1.69  syntax (xsymbols)
    1.70 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.71 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.72  syntax (HTML output)
    1.73 -"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.74 -
    1.75 +"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.76 +
    1.77 +parse_translation (advanced) {*
    1.78 +let
    1.79 +
    1.80 +   fun abs_tr0 ctxt p es =
    1.81 +    let
    1.82 +      val x = Free (Name.variant (add_term_free_names (p$es, [])) "x", dummyT);
    1.83 +      val case1 = Syntax.const "_case1" $ p $ es;
    1.84 +      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
    1.85 +                                        $ Syntax.const @{const_name Nil};
    1.86 +      val cs = Syntax.const "_case2" $ case1 $ case2
    1.87 +      val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
    1.88 +                 ctxt [x, cs]
    1.89 +    in lambda x ft end;
    1.90 +
    1.91 +  fun abs_tr ctxt [x as Free (s, T), r] =
    1.92 +        let val thy = ProofContext.theory_of ctxt;
    1.93 +            val s' = Sign.intern_const thy s
    1.94 +        in if Sign.declared_const thy s' then abs_tr0 ctxt x r else lambda x r
    1.95 +        end
    1.96 +   | abs_tr ctxt [p,es] = abs_tr0 ctxt p es
    1.97 +
    1.98 +in [("_lc_abs", abs_tr)] end
    1.99 +*}
   1.100  
   1.101  (*
   1.102  term "[(x,y,z). b]"
   1.103 -term "[(x,y,z). x \<leftarrow> xs]"
   1.104 +term "[(x,y). Cons True x \<leftarrow> xs]"
   1.105 +term "[(x,y,z). Cons x [] \<leftarrow> xs]"
   1.106  term "[(x,y,z). x<a, x>b]"
   1.107  term "[(x,y,z). x<a, x\<leftarrow>xs]"
   1.108  term "[(x,y,z). x\<leftarrow>xs, x>b]"
   1.109 @@ -283,9 +319,9 @@
   1.110  term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
   1.111  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
   1.112  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
   1.113 +term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
   1.114  *)
   1.115  
   1.116 -
   1.117  subsubsection {* @{const Nil} and @{const Cons} *}
   1.118  
   1.119  lemma not_Cons_self [simp]:
   1.120 @@ -367,7 +403,7 @@
   1.121  by (induct xs arbitrary: ys) (case_tac x, auto)+
   1.122  
   1.123  lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
   1.124 -  by (rule Eq_FalseI) auto
   1.125 +by (rule Eq_FalseI) auto
   1.126  
   1.127  simproc_setup list_neq ("(xs::'a list) = ys") = {*
   1.128  (*
   1.129 @@ -835,7 +871,7 @@
   1.130  by (induct xs) auto
   1.131  
   1.132  lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
   1.133 -  by (induct xs) simp_all
   1.134 +by (induct xs) simp_all
   1.135  
   1.136  lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
   1.137  apply (induct xs)
   1.138 @@ -963,6 +999,9 @@
   1.139  lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
   1.140  by (induct xs) auto
   1.141  
   1.142 +lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs"
   1.143 +by (induct xs) auto
   1.144 +
   1.145  lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
   1.146  by (induct xs) auto
   1.147  
   1.148 @@ -1432,12 +1471,12 @@
   1.149  lemma takeWhile_cong [fundef_cong, recdef_cong]:
   1.150    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   1.151    ==> takeWhile P l = takeWhile Q k"
   1.152 -  by (induct k arbitrary: l) (simp_all)
   1.153 +by (induct k arbitrary: l) (simp_all)
   1.154  
   1.155  lemma dropWhile_cong [fundef_cong, recdef_cong]:
   1.156    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   1.157    ==> dropWhile P l = dropWhile Q k"
   1.158 -  by (induct k arbitrary: l, simp_all)
   1.159 +by (induct k arbitrary: l, simp_all)
   1.160  
   1.161  
   1.162  subsubsection {* @{text zip} *}
   1.163 @@ -1544,17 +1583,17 @@
   1.164  
   1.165  lemma list_all2_lengthD [intro?]: 
   1.166    "list_all2 P xs ys ==> length xs = length ys"
   1.167 -  by (simp add: list_all2_def)
   1.168 +by (simp add: list_all2_def)
   1.169  
   1.170  lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
   1.171 -  by (simp add: list_all2_def)
   1.172 +by (simp add: list_all2_def)
   1.173  
   1.174  lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
   1.175 -  by (simp add: list_all2_def)
   1.176 +by (simp add: list_all2_def)
   1.177  
   1.178  lemma list_all2_Cons [iff, code]:
   1.179    "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
   1.180 -  by (auto simp add: list_all2_def)
   1.181 +by (auto simp add: list_all2_def)
   1.182  
   1.183  lemma list_all2_Cons1:
   1.184  "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
   1.185 @@ -1603,7 +1642,7 @@
   1.186  
   1.187  lemma list_all2_appendI [intro?, trans]:
   1.188    "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
   1.189 -  by (simp add: list_all2_append list_all2_lengthD)
   1.190 +by (simp add: list_all2_append list_all2_lengthD)
   1.191  
   1.192  lemma list_all2_conv_all_nth:
   1.193  "list_all2 P xs ys =
   1.194 @@ -1626,39 +1665,39 @@
   1.195  
   1.196  lemma list_all2_all_nthI [intro?]:
   1.197    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   1.198 -  by (simp add: list_all2_conv_all_nth)
   1.199 +by (simp add: list_all2_conv_all_nth)
   1.200  
   1.201  lemma list_all2I:
   1.202    "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
   1.203 -  by (simp add: list_all2_def)
   1.204 +by (simp add: list_all2_def)
   1.205  
   1.206  lemma list_all2_nthD:
   1.207    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   1.208 -  by (simp add: list_all2_conv_all_nth)
   1.209 +by (simp add: list_all2_conv_all_nth)
   1.210  
   1.211  lemma list_all2_nthD2:
   1.212    "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   1.213 -  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   1.214 +by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
   1.215  
   1.216  lemma list_all2_map1: 
   1.217    "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
   1.218 -  by (simp add: list_all2_conv_all_nth)
   1.219 +by (simp add: list_all2_conv_all_nth)
   1.220  
   1.221  lemma list_all2_map2: 
   1.222    "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
   1.223 -  by (auto simp add: list_all2_conv_all_nth)
   1.224 +by (auto simp add: list_all2_conv_all_nth)
   1.225  
   1.226  lemma list_all2_refl [intro?]:
   1.227    "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
   1.228 -  by (simp add: list_all2_conv_all_nth)
   1.229 +by (simp add: list_all2_conv_all_nth)
   1.230  
   1.231  lemma list_all2_update_cong:
   1.232    "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
   1.233 -  by (simp add: list_all2_conv_all_nth nth_list_update)
   1.234 +by (simp add: list_all2_conv_all_nth nth_list_update)
   1.235  
   1.236  lemma list_all2_update_cong2:
   1.237    "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
   1.238 -  by (simp add: list_all2_lengthD list_all2_update_cong)
   1.239 +by (simp add: list_all2_lengthD list_all2_update_cong)
   1.240  
   1.241  lemma list_all2_takeI [simp,intro?]:
   1.242    "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
   1.243 @@ -1684,7 +1723,7 @@
   1.244  
   1.245  lemma list_all2_eq:
   1.246    "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
   1.247 -  by (induct xs ys rule: list_induct2') auto
   1.248 +by (induct xs ys rule: list_induct2') auto
   1.249  
   1.250  
   1.251  subsubsection {* @{text foldl} and @{text foldr} *}
   1.252 @@ -1705,12 +1744,12 @@
   1.253  lemma foldl_cong [fundef_cong, recdef_cong]:
   1.254    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   1.255    ==> foldl f a l = foldl g b k"
   1.256 -  by (induct k arbitrary: a b l) simp_all
   1.257 +by (induct k arbitrary: a b l) simp_all
   1.258  
   1.259  lemma foldr_cong [fundef_cong, recdef_cong]:
   1.260    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   1.261    ==> foldr f l a = foldr g k b"
   1.262 -  by (induct k arbitrary: a b l) simp_all
   1.263 +by (induct k arbitrary: a b l) simp_all
   1.264  
   1.265  text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
   1.266  
   1.267 @@ -1923,10 +1962,10 @@
   1.268  by (induct xs) auto
   1.269  
   1.270  lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
   1.271 -  by (induct x, auto) 
   1.272 +by (induct x, auto) 
   1.273  
   1.274  lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
   1.275 -  by (induct x, auto)
   1.276 +by (induct x, auto)
   1.277  
   1.278  lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
   1.279  by (induct xs) auto
   1.280 @@ -2008,7 +2047,7 @@
   1.281  by(auto simp: distinct_conv_nth)
   1.282  
   1.283  lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
   1.284 -  by (induct xs) auto
   1.285 +by (induct xs) auto
   1.286  
   1.287  lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
   1.288  proof (induct xs)
   1.289 @@ -2371,13 +2410,13 @@
   1.290  inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
   1.291  
   1.292  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
   1.293 -  by (clarify, erule listsp.induct, blast+)
   1.294 +by (clarify, erule listsp.induct, blast+)
   1.295  
   1.296  lemmas lists_mono = listsp_mono [to_set]
   1.297  
   1.298  lemma listsp_infI:
   1.299    assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
   1.300 -  by induct blast+
   1.301 +by induct blast+
   1.302  
   1.303  lemmas lists_IntI = listsp_infI [to_set]
   1.304  
   1.305 @@ -2556,10 +2595,10 @@
   1.306              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   1.307  
   1.308  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
   1.309 -  by (unfold lexord_def, induct_tac y, auto) 
   1.310 +by (unfold lexord_def, induct_tac y, auto) 
   1.311  
   1.312  lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
   1.313 -  by (unfold lexord_def, induct_tac x, auto)
   1.314 +by (unfold lexord_def, induct_tac x, auto)
   1.315  
   1.316  lemma lexord_cons_cons[simp]:
   1.317       "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
   1.318 @@ -2572,18 +2611,18 @@
   1.319  lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
   1.320  
   1.321  lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
   1.322 -  by (induct_tac x, auto)  
   1.323 +by (induct_tac x, auto)  
   1.324  
   1.325  lemma lexord_append_left_rightI:
   1.326       "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
   1.327 -  by (induct_tac u, auto)
   1.328 +by (induct_tac u, auto)
   1.329  
   1.330  lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
   1.331 -  by (induct x, auto)
   1.332 +by (induct x, auto)
   1.333  
   1.334  lemma lexord_append_leftD:
   1.335       "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
   1.336 -  by (erule rev_mp, induct_tac x, auto)
   1.337 +by (erule rev_mp, induct_tac x, auto)
   1.338  
   1.339  lemma lexord_take_index_conv: 
   1.340     "((x,y) : lexord r) = 
   1.341 @@ -2629,7 +2668,7 @@
   1.342    by blast
   1.343  
   1.344  lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
   1.345 -  by (rule transI, drule lexord_trans, blast) 
   1.346 +by (rule transI, drule lexord_trans, blast) 
   1.347  
   1.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"
   1.349    apply (rule_tac x = y in spec) 
   1.350 @@ -2647,21 +2686,21 @@
   1.351    "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
   1.352  
   1.353  lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
   1.354 -  unfolding measures_def
   1.355 -  by blast
   1.356 +unfolding measures_def
   1.357 +by blast
   1.358  
   1.359  lemma in_measures[simp]: 
   1.360    "(x, y) \<in> measures [] = False"
   1.361    "(x, y) \<in> measures (f # fs)
   1.362           = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
   1.363 -  unfolding measures_def
   1.364 -  by auto
   1.365 +unfolding measures_def
   1.366 +by auto
   1.367  
   1.368  lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
   1.369 -  by simp
   1.370 +by simp
   1.371  
   1.372  lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
   1.373 -  by auto
   1.374 +by auto
   1.375  
   1.376  (* install the lexicographic_order method and the "fun" command *)
   1.377  use "Tools/function_package/lexicographic_order.ML"
   1.378 @@ -2899,34 +2938,34 @@
   1.379  
   1.380  lemma mem_iff [code post]:
   1.381    "x mem xs \<longleftrightarrow> x \<in> set xs"
   1.382 -  by (induct xs) auto
   1.383 +by (induct xs) auto
   1.384  
   1.385  lemmas in_set_code [code unfold] = mem_iff [symmetric]
   1.386  
   1.387  lemma empty_null [code inline]:
   1.388    "xs = [] \<longleftrightarrow> null xs"
   1.389 -  by (cases xs) simp_all
   1.390 +by (cases xs) simp_all
   1.391  
   1.392  lemmas null_empty [code post] =
   1.393    empty_null [symmetric]
   1.394  
   1.395  lemma list_inter_conv:
   1.396    "set (list_inter xs ys) = set xs \<inter> set ys"
   1.397 -  by (induct xs) auto
   1.398 +by (induct xs) auto
   1.399  
   1.400  lemma list_all_iff [code post]:
   1.401    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   1.402 -  by (induct xs) auto
   1.403 +by (induct xs) auto
   1.404  
   1.405  lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
   1.406  
   1.407  lemma list_all_append [simp]:
   1.408    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   1.409 -  by (induct xs) auto
   1.410 +by (induct xs) auto
   1.411  
   1.412  lemma list_all_rev [simp]:
   1.413    "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
   1.414 -  by (simp add: list_all_iff)
   1.415 +by (simp add: list_all_iff)
   1.416  
   1.417  lemma list_all_length:
   1.418    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   1.419 @@ -2934,7 +2973,7 @@
   1.420  
   1.421  lemma list_ex_iff [code post]:
   1.422    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   1.423 -  by (induct xs) simp_all
   1.424 +by (induct xs) simp_all
   1.425  
   1.426  lemmas list_bex_code [code unfold] =
   1.427    list_ex_iff [symmetric]
   1.428 @@ -2945,57 +2984,57 @@
   1.429  
   1.430  lemma filtermap_conv:
   1.431     "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
   1.432 -  by (induct xs) (simp_all split: option.split) 
   1.433 +by (induct xs) (simp_all split: option.split) 
   1.434  
   1.435  lemma map_filter_conv [simp]:
   1.436    "map_filter f P xs = map f (filter P xs)"
   1.437 -  by (induct xs) auto
   1.438 +by (induct xs) auto
   1.439  
   1.440  lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
   1.441 -  by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
   1.442 +by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
   1.443  
   1.444  
   1.445  text {* Code for bounded quantification over nats. *}
   1.446  
   1.447  lemma atMost_upto [code unfold]:
   1.448    "{..n} = set [0..n]"
   1.449 -  by auto
   1.450 +by auto
   1.451  
   1.452  lemma atLeast_upt [code unfold]:
   1.453    "{..<n} = set [0..<n]"
   1.454 -  by auto
   1.455 +by auto
   1.456  
   1.457  lemma greaterThanLessThan_upd [code unfold]:
   1.458    "{n<..<m} = set [Suc n..<m]"
   1.459 -  by auto
   1.460 +by auto
   1.461  
   1.462  lemma atLeastLessThan_upd [code unfold]:
   1.463    "{n..<m} = set [n..<m]"
   1.464 -  by auto
   1.465 +by auto
   1.466  
   1.467  lemma greaterThanAtMost_upto [code unfold]:
   1.468    "{n<..m} = set [Suc n..m]"
   1.469 -  by auto
   1.470 +by auto
   1.471  
   1.472  lemma atLeastAtMost_upto [code unfold]:
   1.473    "{n..m} = set [n..m]"
   1.474 -  by auto
   1.475 +by auto
   1.476  
   1.477  lemma all_nat_less_eq [code unfold]:
   1.478    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
   1.479 -  by auto
   1.480 +by auto
   1.481  
   1.482  lemma ex_nat_less_eq [code unfold]:
   1.483    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
   1.484 -  by auto
   1.485 +by auto
   1.486  
   1.487  lemma all_nat_less [code unfold]:
   1.488    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
   1.489 -  by auto
   1.490 +by auto
   1.491  
   1.492  lemma ex_nat_less [code unfold]:
   1.493    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   1.494 -  by auto
   1.495 +by auto
   1.496  
   1.497  lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)"
   1.498  by (induct xs, simp_all)
   1.499 @@ -3006,7 +3045,8 @@
   1.500  next
   1.501    case (Cons x xs ss)
   1.502    have "set (foldl op @ ss (map f (x # xs))) = set (foldl op @ (ss @ f x) (map f xs))" by simp
   1.503 -  also have "\<dots> = set (ss@ f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" using prems  by simp
   1.504 +  also have "\<dots> = set (ss@ f x) \<union> UNION (set xs) (\<lambda>x. set (f x))"
   1.505 +    using prems by simp
   1.506    also have "\<dots>= set ss \<union> set (f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" by simp
   1.507    also have "\<dots> = set ss \<union> UNION (set (x#xs)) (\<lambda>x. set (f x))"
   1.508      by (simp add: Un_assoc)
   1.509 @@ -3057,11 +3097,11 @@
   1.510  
   1.511  lemma partition_filter1:
   1.512      "fst (partition P xs) = filter P xs"
   1.513 -  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   1.514 +by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   1.515  
   1.516  lemma partition_filter2:
   1.517      "snd (partition P xs) = filter (Not o P) xs"
   1.518 -  by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   1.519 +by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
   1.520  
   1.521  lemma partition_set:
   1.522    assumes "partition P xs = (yes, no)"