First step to remove nonstandard "[x <- xs. P]" syntax: only input
authornipkow
Tue May 22 11:08:37 2018 +0200 (20 months ago ago)
changeset 68250949d93804740
parent 68249 ef1e0cb80fde
child 68251 c45067867860
First step to remove nonstandard "[x <- xs. P]" syntax: only input
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Main/Main_Doc.thy
src/Doc/Tutorial/Inductive/AB.thy
src/HOL/Library/AList.thy
src/HOL/Library/Finite_Map.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/MicroJava/DFA/Kildall.thy
src/HOL/MicroJava/DFA/LBVComplete.thy
src/HOL/MicroJava/DFA/LBVCorrect.thy
src/HOL/MicroJava/DFA/LBVSpec.thy
src/HOL/MicroJava/DFA/SemilatAlg.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nominal/Examples/W.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Quotient_Examples/Quotient_FSet.thy
src/HOL/Random.thy
src/HOL/ex/Quicksort.thy
src/HOL/ex/Radix_Sort.thy
     1.1 --- a/NEWS	Tue May 22 14:12:15 2018 +0200
     1.2 +++ b/NEWS	Tue May 22 11:08:37 2018 +0200
     1.3 @@ -315,6 +315,9 @@
     1.4  * Theory List: functions "sorted_wrt" and "sorted" now compare every
     1.5    element in a list to all following elements, not just the next one.
     1.6  
     1.7 +* Theory List: the non-standard filter-syntax "[x <- xs. P]" is
     1.8 +  deprecated and is currently only available as input syntax anymore.
     1.9 +
    1.10  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
    1.11  
    1.12  * Predicate coprime is now a real definition, not a mere
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue May 22 14:12:15 2018 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue May 22 11:08:37 2018 +0200
     2.3 @@ -1217,8 +1217,8 @@
     2.4  
     2.5    \<^item> Change of binding status of variables: anything beyond the built-in
     2.6    @{keyword "binder"} mixfix annotation requires explicit syntax translations.
     2.7 -  For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
     2.8 -  defined in theory @{theory List} in Isabelle/HOL.
     2.9 +  For example, consider the set comprehension syntax @{term "{x. P}"} as
    2.10 +  defined in theory @{theory Set} in Isabelle/HOL.
    2.11  \<close>
    2.12  
    2.13  
     3.1 --- a/src/Doc/Main/Main_Doc.thy	Tue May 22 14:12:15 2018 +0200
     3.2 +++ b/src/Doc/Main/Main_Doc.thy	Tue May 22 11:08:37 2018 +0200
     3.3 @@ -572,7 +572,6 @@
     3.4  @{term"[m..<n]"} & @{term[source]"upt m n"}\\
     3.5  @{term"[i..j]"} & @{term[source]"upto i j"}\\
     3.6  \<open>[e. x \<leftarrow> xs]\<close> & @{term"map (%x. e) xs"}\\
     3.7 -@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
     3.8  @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
     3.9  @{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
    3.10  \end{supertabular}
     4.1 --- a/src/Doc/Tutorial/Inductive/AB.thy	Tue May 22 14:12:15 2018 +0200
     4.2 +++ b/src/Doc/Tutorial/Inductive/AB.thy	Tue May 22 11:08:37 2018 +0200
     4.3 @@ -64,15 +64,13 @@
     4.4  \<close>
     4.5  
     4.6  lemma correctness:
     4.7 -  "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b])     \<and>
     4.8 -   (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
     4.9 -   (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
    4.10 +  "(w \<in> S \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w))     \<and>
    4.11 +   (w \<in> A \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1) \<and>
    4.12 +   (w \<in> B \<longrightarrow> size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1)"
    4.13  
    4.14  txt\<open>\noindent
    4.15  These propositions are expressed with the help of the predefined @{term
    4.16 -filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
    4.17 -x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
    4.18 -holds. Remember that on lists @{text size} and @{text length} are synonymous.
    4.19 +filter} function on lists. Remember that on lists @{text size} and @{text length} are synonymous.
    4.20  
    4.21  The proof itself is by rule induction and afterwards automatic:
    4.22  \<close>
    4.23 @@ -112,8 +110,8 @@
    4.24  \<close>
    4.25  
    4.26  lemma step1: "\<forall>i < size w.
    4.27 -  \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
    4.28 -   - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
    4.29 +  \<bar>(int(size(filter P (take (i+1) w)))-int(size(filter (\<lambda>x. \<not>P x) (take (i+1) w))))
    4.30 +   - (int(size(filter P (take i w)))-int(size(filter (\<lambda>x. \<not>P x) (take i w))))\<bar> \<le> 1"
    4.31  
    4.32  txt\<open>\noindent
    4.33  The lemma is a bit hard to read because of the coercion function
    4.34 @@ -137,8 +135,8 @@
    4.35  \<close>
    4.36  
    4.37  lemma part1:
    4.38 - "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
    4.39 -  \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
    4.40 + "size(filter P w) = size(filter (\<lambda>x. \<not>P x) w)+2 \<Longrightarrow>
    4.41 +  \<exists>i\<le>size w. size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1"
    4.42  
    4.43  txt\<open>\noindent
    4.44  This is proved by @{text force} with the help of the intermediate value theorem,
    4.45 @@ -157,10 +155,10 @@
    4.46  
    4.47  
    4.48  lemma part2:
    4.49 -  "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
    4.50 -    size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
    4.51 -    size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
    4.52 -   \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
    4.53 +  "\<lbrakk>size(filter P (take i w @ drop i w)) =
    4.54 +    size(filter (\<lambda>x. \<not>P x) (take i w @ drop i w))+2;
    4.55 +    size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1\<rbrakk>
    4.56 +   \<Longrightarrow> size(filter P (drop i w)) = size(filter (\<lambda>x. \<not>P x) (drop i w))+1"
    4.57  by(simp del: append_take_drop_id)
    4.58  
    4.59  text\<open>\noindent
    4.60 @@ -187,9 +185,9 @@
    4.61  \<close>
    4.62  
    4.63  theorem completeness:
    4.64 -  "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]     \<longrightarrow> w \<in> S) \<and>
    4.65 -   (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
    4.66 -   (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
    4.67 +  "(size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w)     \<longrightarrow> w \<in> S) \<and>
    4.68 +   (size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1 \<longrightarrow> w \<in> A) \<and>
    4.69 +   (size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1 \<longrightarrow> w \<in> B)"
    4.70  
    4.71  txt\<open>\noindent
    4.72  The proof is by induction on @{term w}. Structural induction would fail here
    4.73 @@ -234,9 +232,9 @@
    4.74   apply(clarify)
    4.75  txt\<open>\noindent
    4.76  This yields an index @{prop"i \<le> length v"} such that
    4.77 -@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
    4.78 +@{prop[display]"length (filter (\<lambda>x. x=a) (take i v)) = length (filter (\<lambda>x. x=b) (take i v)) + 1"}
    4.79  With the help of @{thm[source]part2} it follows that
    4.80 -@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
    4.81 +@{prop[display]"length (filter (\<lambda>x. x=a) (drop i v)) = length (filter (\<lambda>x. x=b) (drop i v)) + 1"}
    4.82  \<close>
    4.83  
    4.84   apply(drule part2[of "\<lambda>x. x=a", simplified])
     5.1 --- a/src/HOL/Library/AList.thy	Tue May 22 14:12:15 2018 +0200
     5.2 +++ b/src/HOL/Library/AList.thy	Tue May 22 11:08:37 2018 +0200
     5.3 @@ -45,7 +45,7 @@
     5.4    using assms by (simp add: update_keys)
     5.5  
     5.6  lemma update_filter:
     5.7 -  "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
     5.8 +  "a \<noteq> k \<Longrightarrow> update k v (filter (\<lambda>q. fst q \<noteq> a) ps) = filter (\<lambda>q. fst q \<noteq> a) (update k v ps)"
     5.9    by (induct ps) auto
    5.10  
    5.11  lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    5.12 @@ -361,12 +361,12 @@
    5.13  proof -
    5.14    have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
    5.15      by auto
    5.16 -  then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
    5.17 +  then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D \<and> fst p \<noteq> x) al"
    5.18      by simp
    5.19    assume "x \<notin> D"
    5.20    then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
    5.21      by auto
    5.22 -  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
    5.23 +  then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D) al"
    5.24      by simp
    5.25  qed
    5.26  
    5.27 @@ -492,7 +492,7 @@
    5.28  lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
    5.29    by (simp add: map_ran_def split_def comp_def)
    5.30  
    5.31 -lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
    5.32 +lemma map_ran_filter: "map_ran f (filter (\<lambda>p. fst p \<noteq> a) ps) = filter (\<lambda>p. fst p \<noteq> a) (map_ran f ps)"
    5.33    by (simp add: map_ran_def filter_map split_def comp_def)
    5.34  
    5.35  lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
     6.1 --- a/src/HOL/Library/Finite_Map.thy	Tue May 22 14:12:15 2018 +0200
     6.2 +++ b/src/HOL/Library/Finite_Map.thy	Tue May 22 11:08:37 2018 +0200
     6.3 @@ -84,10 +84,10 @@
     6.4  definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
     6.5  "map_filter P m = (\<lambda>x. if P x then m x else None)"
     6.6  
     6.7 -lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
     6.8 +lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\<lambda>(k, _). P k) m)"
     6.9  proof
    6.10    fix x
    6.11 -  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
    6.12 +  show "map_filter P (map_of m) x = map_of (filter (\<lambda>(k, _). P k) m) x"
    6.13      by (induct m) (auto simp: map_filter_def)
    6.14  qed
    6.15  
     7.1 --- a/src/HOL/Library/Multiset.thy	Tue May 22 14:12:15 2018 +0200
     7.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 22 11:08:37 2018 +0200
     7.3 @@ -1888,7 +1888,7 @@
     7.4  apply simp
     7.5  done
     7.6  
     7.7 -lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
     7.8 +lemma mset_compl_union [simp]: "mset (filter P xs) + mset (filter (\<lambda>x. \<not>P x) xs) = mset xs"
     7.9    by (induct xs) auto
    7.10  
    7.11  lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
    7.12 @@ -2582,14 +2582,14 @@
    7.13    show "mset ys = mset xs" by simp
    7.14    from \<open>sorted (map f ys)\<close>
    7.15    show "sorted (map f ys)" .
    7.16 -  show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
    7.17 +  show "filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" if "k \<in> set ys" for k
    7.18    proof -
    7.19      from mset_equal
    7.20      have set_equal: "set xs = set ys" by (rule mset_eq_setD)
    7.21      with that have "insert k (set ys) = set ys" by auto
    7.22      with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))"
    7.23        by (simp add: set_equal)
    7.24 -    from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
    7.25 +    from inj have "filter (\<lambda>x. f k = f x) ys = filter (HOL.eq k) ys"
    7.26        by (auto intro!: inj_on_filter_key_eq)
    7.27      also have "\<dots> = replicate (count (mset ys) k) k"
    7.28        by (simp add: replicate_count_mset_eq_filter_eq)
    7.29 @@ -2597,7 +2597,7 @@
    7.30        using mset_equal by simp
    7.31      also have "\<dots> = filter (HOL.eq k) xs"
    7.32        by (simp add: replicate_count_mset_eq_filter_eq)
    7.33 -    also have "\<dots> = [x\<leftarrow>xs . f k = f x]"
    7.34 +    also have "\<dots> = filter (\<lambda>x. f k = f x) xs"
    7.35        using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal)
    7.36      finally show ?thesis .
    7.37    qed
    7.38 @@ -2610,9 +2610,9 @@
    7.39    by (rule sort_key_inj_key_eq) (simp_all add: assms)
    7.40  
    7.41  lemma sort_key_by_quicksort:
    7.42 -  "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
    7.43 -    @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
    7.44 -    @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
    7.45 +  "sort_key f xs = sort_key f (filter (\<lambda>x. f x < f (xs ! (length xs div 2))) xs)
    7.46 +    @ filter (\<lambda>x. f x = f (xs ! (length xs div 2))) xs
    7.47 +    @ sort_key f (filter (\<lambda>x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs")
    7.48  proof (rule properties_for_sort_key)
    7.49    show "mset ?rhs = mset ?lhs"
    7.50      by (rule multiset_eqI) (auto simp add: mset_filter)
    7.51 @@ -2623,14 +2623,14 @@
    7.52    assume "l \<in> set ?rhs"
    7.53    let ?pivot = "f (xs ! (length xs div 2))"
    7.54    have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
    7.55 -  have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
    7.56 +  have "filter (\<lambda>x. f x = f l) (sort_key f xs) = filter (\<lambda>x. f x = f l) xs"
    7.57      unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
    7.58 -  with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
    7.59 +  with * have **: "filter (\<lambda>x. f l = f x) (sort_key f xs) = filter (\<lambda>x. f l = f x) xs" by simp
    7.60    have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
    7.61 -  then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
    7.62 -    [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
    7.63 +  then have "\<And>P. filter (\<lambda>x. P (f x) ?pivot \<and> f l = f x) (sort_key f xs) =
    7.64 +    filter (\<lambda>x. P (f l) ?pivot \<and> f l = f x) (sort_key f xs)" by simp
    7.65    note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
    7.66 -  show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
    7.67 +  show "filter (\<lambda>x. f l = f x) ?rhs = filter (\<lambda>x. f l = f x) ?lhs"
    7.68    proof (cases "f l" ?pivot rule: linorder_cases)
    7.69      case less
    7.70      then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
    7.71 @@ -2648,15 +2648,15 @@
    7.72  qed
    7.73  
    7.74  lemma sort_by_quicksort:
    7.75 -  "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
    7.76 -    @ [x\<leftarrow>xs. x = xs ! (length xs div 2)]
    7.77 -    @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
    7.78 +  "sort xs = sort (filter (\<lambda>x. x < xs ! (length xs div 2)) xs)
    7.79 +    @ filter (\<lambda>x. x = xs ! (length xs div 2)) xs
    7.80 +    @ sort (filter (\<lambda>x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs")
    7.81    using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
    7.82  
    7.83  text \<open>A stable parametrized quicksort\<close>
    7.84  
    7.85  definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
    7.86 -  "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
    7.87 +  "part f pivot xs = (filter (\<lambda>x. f x < pivot) xs, filter (\<lambda>x. f x = pivot) xs, filter (\<lambda>x. f x > pivot) xs)"
    7.88  
    7.89  lemma part_code [code]:
    7.90    "part f pivot [] = ([], [], [])"
     8.1 --- a/src/HOL/List.thy	Tue May 22 14:12:15 2018 +0200
     8.2 +++ b/src/HOL/List.thy	Tue May 22 11:08:37 2018 +0200
     8.3 @@ -78,13 +78,13 @@
     8.4  "filter P [] = []" |
     8.5  "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
     8.6  
     8.7 -text \<open>Special syntax for filter:\<close>
     8.8 +text \<open>Special input syntax for filter:\<close>
     8.9  syntax (ASCII)
    8.10    "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_<-_./ _])")
    8.11  syntax
    8.12    "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_\<leftarrow>_ ./ _])")
    8.13  translations
    8.14 -  "[x<-xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs"
    8.15 +  "[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
    8.16  
    8.17  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    8.18  fold_Nil:  "fold f [] = id" |
    8.19 @@ -1598,7 +1598,7 @@
    8.20  
    8.21  lemma inj_on_filter_key_eq:
    8.22    assumes "inj_on f (insert y (set xs))"
    8.23 -  shows "[x\<leftarrow>xs . f y = f x] = filter (HOL.eq y) xs"
    8.24 +  shows "filter (\<lambda>x. f y = f x) xs = filter (HOL.eq y) xs"
    8.25    using assms by (induct xs) auto
    8.26  
    8.27  lemma filter_cong[fundef_cong]:
    8.28 @@ -4430,8 +4430,8 @@
    8.29  done
    8.30  
    8.31  lemma nths_shift_lemma:
    8.32 -  "map fst [p<-zip xs [i..<i + length xs] . snd p \<in> A] =
    8.33 -   map fst [p<-zip xs [0..<length xs] . snd p + i \<in> A]"
    8.34 +  "map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [i..<i + length xs])) =
    8.35 +   map fst (filter (\<lambda>p. snd p + i \<in> A) (zip xs [0..<length xs]))"
    8.36  by (induct xs rule: rev_induct) (simp_all add: add.commute)
    8.37  
    8.38  lemma nths_append:
    8.39 @@ -4720,19 +4720,19 @@
    8.40  
    8.41  lemma transpose_aux_filter_head:
    8.42    "concat (map (case_list [] (\<lambda>h t. [h])) xss) =
    8.43 -  map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
    8.44 +  map (\<lambda>xs. hd xs) (filter (\<lambda>ys. ys \<noteq> []) xss)"
    8.45    by (induct xss) (auto split: list.split)
    8.46  
    8.47  lemma transpose_aux_filter_tail:
    8.48    "concat (map (case_list [] (\<lambda>h t. [t])) xss) =
    8.49 -  map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
    8.50 +  map (\<lambda>xs. tl xs) (filter (\<lambda>ys. ys \<noteq> []) xss)"
    8.51    by (induct xss) (auto split: list.split)
    8.52  
    8.53  lemma transpose_aux_max:
    8.54    "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
    8.55 -  Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
    8.56 +  Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0))"
    8.57    (is "max _ ?foldB = Suc (max _ ?foldA)")
    8.58 -proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
    8.59 +proof (cases "(filter (\<lambda>ys. ys \<noteq> []) xss) = []")
    8.60    case True
    8.61    hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
    8.62    proof (induct xss)
    8.63 @@ -4744,16 +4744,16 @@
    8.64  next
    8.65    case False
    8.66  
    8.67 -  have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
    8.68 +  have foldA: "?foldA = foldr (\<lambda>x. max (length x)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0 - 1"
    8.69      by (induct xss) auto
    8.70 -  have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
    8.71 +  have foldB: "?foldB = foldr (\<lambda>x. max (length x)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0"
    8.72      by (induct xss) auto
    8.73  
    8.74    have "0 < ?foldB"
    8.75    proof -
    8.76      from False
    8.77 -    obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
    8.78 -    hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
    8.79 +    obtain z zs where zs: "(filter (\<lambda>ys. ys \<noteq> []) xss) = z#zs" by (auto simp: neq_Nil_conv)
    8.80 +    hence "z \<in> set (filter (\<lambda>ys. ys \<noteq> []) xss)" by auto
    8.81      hence "z \<noteq> []" by auto
    8.82      thus ?thesis
    8.83        unfolding foldB zs
    8.84 @@ -4781,7 +4781,7 @@
    8.85  lemma nth_transpose:
    8.86    fixes xs :: "'a list list"
    8.87    assumes "i < length (transpose xs)"
    8.88 -  shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
    8.89 +  shows "transpose xs ! i = map (\<lambda>xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
    8.90  using assms proof (induct arbitrary: i rule: transpose.induct)
    8.91    case (3 x xs xss)
    8.92    define XS where "XS = (x # xs) # xss"
    8.93 @@ -5154,7 +5154,7 @@
    8.94  
    8.95  lemma filter_equals_takeWhile_sorted_rev:
    8.96    assumes sorted: "sorted (rev (map f xs))"
    8.97 -  shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
    8.98 +  shows "filter (\<lambda>x. t < f x) xs = takeWhile (\<lambda> x. t < f x) xs"
    8.99      (is "filter ?P xs = ?tW")
   8.100  proof (rule takeWhile_eq_filter[symmetric])
   8.101    let "?dW" = "dropWhile ?P xs"
   8.102 @@ -5178,18 +5178,18 @@
   8.103  qed
   8.104  
   8.105  lemma sorted_map_same:
   8.106 -  "sorted (map f [x\<leftarrow>xs. f x = g xs])"
   8.107 +  "sorted (map f (filter (\<lambda>x. f x = g xs) xs))"
   8.108  proof (induct xs arbitrary: g)
   8.109    case Nil then show ?case by simp
   8.110  next
   8.111    case (Cons x xs)
   8.112 -  then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
   8.113 -  moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
   8.114 +  then have "sorted (map f (filter (\<lambda>y. f y = (\<lambda>xs. f x) xs) xs))" .
   8.115 +  moreover from Cons have "sorted (map f (filter (\<lambda>y. f y = (g \<circ> Cons x) xs) xs))" .
   8.116    ultimately show ?case by simp_all
   8.117  qed
   8.118  
   8.119  lemma sorted_same:
   8.120 -  "sorted [x\<leftarrow>xs. x = g xs]"
   8.121 +  "sorted (filter (\<lambda>x. x = g xs) xs)"
   8.122  using sorted_map_same [of "\<lambda>x. x"] by simp
   8.123  
   8.124  end
   8.125 @@ -5411,7 +5411,7 @@
   8.126  
   8.127  text \<open>Stability of @{const sort_key}:\<close>
   8.128  
   8.129 -lemma sort_key_stable: "[y <- sort_key f xs. f y = k] = [y <- xs. f y = k]"
   8.130 +lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
   8.131  proof (induction xs)
   8.132    case Nil thus ?case by simp
   8.133  next
   8.134 @@ -5422,12 +5422,12 @@
   8.135        using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
   8.136    next
   8.137      case True
   8.138 -    hence ler: "[y <- (a # xs). f y = k] = a # [y <- xs. f y = f a]" by simp
   8.139 -    have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
   8.140 -    hence "insort_key f a (sort_key f [y <- xs. f y = f a])
   8.141 -            = a # (sort_key f [y <- xs. f y = f a])"
   8.142 +    hence ler: "filter (\<lambda>y. f y = k) (a # xs) = a # filter (\<lambda>y. f y = f a) xs" by simp
   8.143 +    have "\<forall>y \<in> set (sort_key f (filter (\<lambda>y. f y = f a) xs)). f y = f a" by simp
   8.144 +    hence "insort_key f a (sort_key f (filter (\<lambda>y. f y = f a) xs))
   8.145 +            = a # (sort_key f (filter (\<lambda>y. f y = f a) xs))"
   8.146        by (simp add: insort_is_Cons)
   8.147 -    hence lel: "[y <- sort_key f (a # xs). f y = k] = a # [y <- sort_key f xs. f y = f a]"
   8.148 +    hence lel: "filter (\<lambda>y. f y = k) (sort_key f (a # xs)) = a # filter (\<lambda>y. f y = f a) (sort_key f xs)"
   8.149        by (metis True filter_sort ler sort_key_simps(2))
   8.150      from lel ler show ?thesis using Cons.IH True by (auto)
   8.151    qed
   8.152 @@ -5447,7 +5447,7 @@
   8.153      length_filter_conv_card intro: card_mono)
   8.154  
   8.155  lemma transpose_max_length:
   8.156 -  "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
   8.157 +  "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length (filter (\<lambda>x. x \<noteq> []) xs)"
   8.158    (is "?L = ?R")
   8.159  proof (cases "transpose xs = []")
   8.160    case False
   8.161 @@ -5459,7 +5459,7 @@
   8.162      using False by (simp add: nth_transpose)
   8.163  next
   8.164    case True
   8.165 -  hence "[x \<leftarrow> xs. x \<noteq> []] = []"
   8.166 +  hence "filter (\<lambda>x. x \<noteq> []) xs = []"
   8.167      by (auto intro!: filter_False simp: transpose_empty)
   8.168    thus ?thesis by (simp add: transpose_empty True)
   8.169  qed
   8.170 @@ -5480,7 +5480,7 @@
   8.171    fixes xs :: "'a list list"
   8.172    assumes sorted: "sorted (rev (map length xs))"
   8.173    and i: "i < length (transpose xs)"
   8.174 -  and j: "j < length [ys \<leftarrow> xs. i < length ys]"
   8.175 +  and j: "j < length (filter (\<lambda>ys. i < length ys) xs)"
   8.176    shows "transpose xs ! i ! j = xs ! j  ! i"
   8.177  using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
   8.178      nth_transpose[OF i] nth_map[OF j]
   8.179 @@ -5542,7 +5542,7 @@
   8.180      have "length (xs ! i) \<le> length (xs ! k)" by simp
   8.181      thus "Suc j \<le> length (xs ! k)" using j_less by simp
   8.182    qed
   8.183 -  have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
   8.184 +  have i_less_filter: "i < length (filter (\<lambda>ys. j < length ys) xs) "
   8.185      unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
   8.186      using i_less_tW by (simp_all add: Suc_le_eq)
   8.187    from j show "?R ! j = xs ! i ! j"
   8.188 @@ -5581,7 +5581,7 @@
   8.189    show len: "length ?trans = length ?map"
   8.190      by (simp_all add: length_transpose foldr_map comp_def)
   8.191    moreover
   8.192 -  { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
   8.193 +  { fix i assume "i < n" hence "filter (\<lambda>ys. i < length ys) xs = xs"
   8.194        using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
   8.195    ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
   8.196      by (auto simp: nth_transpose intro: nth_equalityI)
     9.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Tue May 22 14:12:15 2018 +0200
     9.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Tue May 22 11:08:37 2018 +0200
     9.3 @@ -38,7 +38,7 @@
     9.4  
     9.5  lemma (in Semilat) nth_merges:
     9.6   "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
     9.7 -  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
     9.8 +  (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p"
     9.9    (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
    9.10  proof (induct ps)
    9.11    show "\<And>ss. ?P ss []" by simp
    10.1 --- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Tue May 22 14:12:15 2018 +0200
    10.2 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Tue May 22 11:08:37 2018 +0200
    10.3 @@ -80,13 +80,13 @@
    10.4      assume merge: "?s1 \<noteq> T" 
    10.5      from x ss1 have "?s1 =
    10.6        (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
    10.7 -      then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
    10.8 +      then (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss1)) ++_f x
    10.9        else \<top>)" 
   10.10        by (rule merge_def)  
   10.11      with merge obtain
   10.12        app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
   10.13             (is "?app ss1") and
   10.14 -      sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" 
   10.15 +      sum: "(map snd (filter (\<lambda>(p',t'). p' = pc+1) ss1) ++_f x) = ?s1" 
   10.16             (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
   10.17        by (simp split: if_split_asm)
   10.18      from app less 
   10.19 @@ -115,7 +115,7 @@
   10.20      from x ss2 have 
   10.21        "?s2 =
   10.22        (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
   10.23 -      then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
   10.24 +      then map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss2) ++_f x
   10.25        else \<top>)" 
   10.26        by (rule merge_def)
   10.27      ultimately have ?thesis by simp
   10.28 @@ -194,7 +194,7 @@
   10.29    ultimately
   10.30    have "merge c pc ?step (c!Suc pc) =
   10.31      (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
   10.32 -    then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
   10.33 +    then map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc
   10.34      else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
   10.35    moreover {
   10.36      fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
   10.37 @@ -207,7 +207,7 @@
   10.38    } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
   10.39    moreover
   10.40    from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
   10.41 -  hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
   10.42 +  hence "map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc \<noteq> \<top>" 
   10.43           (is "?map ++_f _ \<noteq> _")
   10.44    proof (rule disjE)
   10.45      assume pc': "Suc pc = length \<phi>"
   10.46 @@ -215,7 +215,7 @@
   10.47      moreover 
   10.48      from pc' bounded pc 
   10.49      have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
   10.50 -    hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False) 
   10.51 +    hence "filter (\<lambda>(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False) 
   10.52      hence "?map = []" by simp
   10.53      ultimately show ?thesis by (simp add: B_neq_T)  
   10.54    next
   10.55 @@ -262,7 +262,7 @@
   10.56    hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
   10.57    ultimately
   10.58    have "merge c pc ?step (c!Suc pc) =
   10.59 -    map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
   10.60 +    map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s) 
   10.61    hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
   10.62    also {
   10.63      from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
    11.1 --- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Tue May 22 14:12:15 2018 +0200
    11.2 +++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Tue May 22 11:08:37 2018 +0200
    11.3 @@ -88,7 +88,7 @@
    11.4      also    
    11.5      from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
    11.6      with cert_in_A step_in_A
    11.7 -    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
    11.8 +    have "?merge = (map snd (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
    11.9        by (rule merge_not_top_s) 
   11.10      finally
   11.11      have "s' <=_r ?s2" using step_in_A cert_in_A True step 
    12.1 --- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Tue May 22 14:12:15 2018 +0200
    12.2 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Tue May 22 11:08:37 2018 +0200
    12.3 @@ -113,7 +113,7 @@
    12.4  lemma (in Semilat) pp_ub1':
    12.5    assumes S: "snd`set S \<subseteq> A" 
    12.6    assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" 
    12.7 -  shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
    12.8 +  shows "b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
    12.9  proof -
   12.10    from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
   12.11    with semilat y ab show ?thesis by - (rule ub1')
   12.12 @@ -172,7 +172,7 @@
   12.13    "\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
   12.14    merge c pc ss x = 
   12.15    (if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
   12.16 -    map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
   12.17 +    map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x
   12.18    else \<top>)" 
   12.19    (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
   12.20  proof (induct ss)
   12.21 @@ -202,15 +202,15 @@
   12.22        hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
   12.23        moreover
   12.24        from True have 
   12.25 -        "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' = 
   12.26 -        (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
   12.27 +        "map snd (filter (\<lambda>(p',t'). p'=pc+1) ls) ++_f ?if' = 
   12.28 +        (map snd (filter (\<lambda>(p',t'). p'=pc+1) (l#ls)) ++_f x)"
   12.29          by simp
   12.30        ultimately
   12.31        show ?thesis using True by simp
   12.32      next
   12.33        case False 
   12.34        moreover
   12.35 -      from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
   12.36 +      from ls have "set (map snd (filter (\<lambda>(p', t'). p' = Suc pc) ls)) \<subseteq> A" by auto
   12.37        ultimately show ?thesis by auto
   12.38      qed
   12.39    finally show "?P (l#ls) x" .
   12.40 @@ -219,7 +219,7 @@
   12.41  lemma (in lbv) merge_not_top_s:
   12.42    assumes x:  "x \<in> A" and ss: "snd`set ss \<subseteq> A"
   12.43    assumes m:  "merge c pc ss x \<noteq> \<top>"
   12.44 -  shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
   12.45 +  shows "merge c pc ss x = (map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x)"
   12.46  proof -
   12.47    from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')" 
   12.48      by (rule merge_not_top)
   12.49 @@ -307,8 +307,8 @@
   12.50    assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
   12.51    shows "merge c pc ss x \<in> A"
   12.52  proof -
   12.53 -  from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
   12.54 -  with x  have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
   12.55 +  from s0 have "set (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss)) \<subseteq> A" by auto
   12.56 +  with x  have "(map snd (filter (\<lambda>(p', t'). p'=pc+1) ss) ++_f x) \<in> A"
   12.57      by (auto intro!: plusplus_closed semilat)
   12.58    with s0 x show ?thesis by (simp add: merge_def T_A)
   12.59  qed
    13.1 --- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Tue May 22 14:12:15 2018 +0200
    13.2 +++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Tue May 22 11:08:37 2018 +0200
    13.3 @@ -155,7 +155,7 @@
    13.4  lemma ub1':
    13.5    assumes "semilat (A, r, f)"
    13.6    shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
    13.7 -  \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
    13.8 +  \<Longrightarrow> b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y" 
    13.9  proof -
   13.10    interpret Semilat A r f using assms by (rule Semilat.intro)
   13.11  
   13.12 @@ -175,7 +175,7 @@
   13.13  
   13.14  lemma plusplus_empty:  
   13.15    "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
   13.16 -   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
   13.17 +   (map snd (filter (\<lambda>(p', t'). p' = q) S) ++_f ss ! q) = ss ! q"
   13.18    by (induct S) auto 
   13.19  
   13.20  end
    14.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 22 14:12:15 2018 +0200
    14.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue May 22 11:08:37 2018 +0200
    14.3 @@ -317,7 +317,7 @@
    14.4  | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
    14.5  
    14.6  theorem S\<^sub>1_sound:
    14.7 -"w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    14.8 +"w \<in> S\<^sub>1 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
    14.9  nitpick [expect = genuine]
   14.10  oops
   14.11  
   14.12 @@ -330,7 +330,7 @@
   14.13  | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
   14.14  
   14.15  theorem S\<^sub>2_sound:
   14.16 -"w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   14.17 +"w \<in> S\<^sub>2 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
   14.18  nitpick [expect = genuine]
   14.19  oops
   14.20  
   14.21 @@ -343,12 +343,12 @@
   14.22  | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
   14.23  
   14.24  theorem S\<^sub>3_sound:
   14.25 -"w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   14.26 +"w \<in> S\<^sub>3 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
   14.27  nitpick [card = 1-5, expect = none]
   14.28  sorry
   14.29  
   14.30  theorem S\<^sub>3_complete:
   14.31 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
   14.32 +"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>3"
   14.33  nitpick [expect = genuine]
   14.34  oops
   14.35  
   14.36 @@ -362,19 +362,19 @@
   14.37  | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   14.38  
   14.39  theorem S\<^sub>4_sound:
   14.40 -"w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   14.41 +"w \<in> S\<^sub>4 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
   14.42  nitpick [card = 1-5, expect = none]
   14.43  sorry
   14.44  
   14.45  theorem S\<^sub>4_complete:
   14.46 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
   14.47 +"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>4"
   14.48  nitpick [card = 1-5, expect = none]
   14.49  sorry
   14.50  
   14.51  theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
   14.52 -"w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   14.53 -"w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   14.54 -"w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   14.55 +"w \<in> S\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
   14.56 +"w \<in> A\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) + 1"
   14.57 +"w \<in> B\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = b) w) = length (filter (\<lambda>x. x = a) w) + 1"
   14.58  nitpick [card = 1-5, expect = none]
   14.59  sorry
   14.60  
    15.1 --- a/src/HOL/Nominal/Examples/W.thy	Tue May 22 14:12:15 2018 +0200
    15.2 +++ b/src/HOL/Nominal/Examples/W.thy	Tue May 22 11:08:37 2018 +0200
    15.3 @@ -9,7 +9,7 @@
    15.4  abbreviation
    15.5    "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) 
    15.6  where
    15.7 -  "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
    15.8 +  "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
    15.9  
   15.10  lemma difference_eqvt_tvar[eqvt]:
   15.11    fixes pi::"tvar prm"
    16.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue May 22 14:12:15 2018 +0200
    16.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue May 22 11:08:37 2018 +0200
    16.3 @@ -71,7 +71,7 @@
    16.4  oops
    16.5  
    16.6  theorem S\<^sub>1_sound:
    16.7 -"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    16.8 +"S\<^sub>1p w \<Longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
    16.9  quickcheck[tester=smart_exhaustive, size=15]
   16.10  oops
   16.11  
   16.12 @@ -113,7 +113,7 @@
   16.13  oops
   16.14  *)
   16.15  theorem S\<^sub>2_sound:
   16.16 -"S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   16.17 +"S\<^sub>2p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
   16.18  quickcheck[tester=smart_exhaustive, size=5, iterations=10]
   16.19  oops
   16.20  
   16.21 @@ -133,16 +133,16 @@
   16.22  
   16.23  
   16.24  lemma S\<^sub>3_sound:
   16.25 -"S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   16.26 +"S\<^sub>3p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
   16.27  quickcheck[tester=smart_exhaustive, size=10, iterations=10]
   16.28  oops
   16.29  
   16.30 -lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
   16.31 +lemma "\<not> (length w > 2) \<or> \<not> (length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w))"
   16.32  quickcheck[size=10, tester = smart_exhaustive]
   16.33  oops
   16.34  
   16.35  theorem S\<^sub>3_complete:
   16.36 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> S\<^sub>3p w"
   16.37 +"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>3p w"
   16.38  (*quickcheck[generator=SML]*)
   16.39  quickcheck[tester=smart_exhaustive, size=10, iterations=100]
   16.40  oops
   16.41 @@ -158,12 +158,12 @@
   16.42  | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   16.43  
   16.44  theorem S\<^sub>4_sound:
   16.45 -"S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   16.46 +"S\<^sub>4p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
   16.47  quickcheck[tester = smart_exhaustive, size=5, iterations=1]
   16.48  oops
   16.49  
   16.50  theorem S\<^sub>4_complete:
   16.51 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
   16.52 +"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>4p w"
   16.53  quickcheck[tester = smart_exhaustive, size=5, iterations=1]
   16.54  oops
   16.55  
   16.56 @@ -301,7 +301,7 @@
   16.57  
   16.58  subsection "Compressed matrix"
   16.59  
   16.60 -definition "sparsify xs = [i \<leftarrow> zip [0..<length xs] xs. snd i \<noteq> 0]"
   16.61 +definition "sparsify xs = filter (\<lambda>i. snd i \<noteq> 0) (zip [0..<length xs] xs)"
   16.62  (*
   16.63  lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
   16.64    by (auto simp: sparsify_def set_zip)
    17.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 22 14:12:15 2018 +0200
    17.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 22 11:08:37 2018 +0200
    17.3 @@ -2028,7 +2028,7 @@
    17.4  private lemma pmf_of_list_aux:
    17.5    assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
    17.6    assumes "sum_list (map snd xs) = 1"
    17.7 -  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
    17.8 +  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) = 1"
    17.9  proof -
   17.10    have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
   17.11              (\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
   17.12 @@ -2083,7 +2083,7 @@
   17.13    show "x \<in> set (map fst xs)"
   17.14    proof (rule ccontr)
   17.15      assume "x \<notin> set (map fst xs)"
   17.16 -    hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
   17.17 +    hence "filter (\<lambda>z. fst z = x) xs = []" by (auto simp: filter_empty_conv)
   17.18      with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
   17.19    qed
   17.20  qed
   17.21 @@ -2122,10 +2122,10 @@
   17.22    have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
   17.23      by simp
   17.24    also from assms
   17.25 -    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
   17.26 +    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))))"
   17.27      by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
   17.28    also from assms
   17.29 -    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
   17.30 +    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
   17.31      by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
   17.32    also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
   17.33        indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
   17.34 @@ -2184,7 +2184,7 @@
   17.35    {
   17.36      fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
   17.37      then obtain y where y: "(x, y) \<in> set xs" by auto
   17.38 -    from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
   17.39 +    from B have "sum_list (map snd (filter (\<lambda>z. fst z = x) xs)) = 0"
   17.40        by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
   17.41      moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
   17.42      ultimately have "y = 0" using assms(1)
   17.43 @@ -2199,11 +2199,11 @@
   17.44    defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
   17.45    shows   "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs"
   17.46  proof -
   17.47 -  have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
   17.48 +  have "map snd (filter (\<lambda>z. snd z \<noteq> 0) xs) = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
   17.49      by (induction xs) simp_all
   17.50    with assms(1) show wf: "pmf_of_list_wf xs'"
   17.51      by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
   17.52 -  have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
   17.53 +  have "sum_list (map snd (filter (\<lambda>z. fst z = i) xs')) = sum_list (map snd (filter (\<lambda>z. fst z = i) xs))" for i
   17.54      unfolding xs'_def by (induction xs) simp_all
   17.55    with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
   17.56      by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
    18.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 22 14:12:15 2018 +0200
    18.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 22 11:08:37 2018 +0200
    18.3 @@ -186,7 +186,7 @@
    18.4  oops
    18.5  
    18.6  lemma
    18.7 -  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
    18.8 +  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
    18.9  quickcheck[random, iterations = 10000]
   18.10  quickcheck[exhaustive, expect = counterexample]
   18.11  oops
   18.12 @@ -228,13 +228,13 @@
   18.13  oops
   18.14  
   18.15  lemma
   18.16 -  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
   18.17 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
   18.18  quickcheck[random]
   18.19  quickcheck[exhaustive, expect = counterexample]
   18.20  oops
   18.21  
   18.22  lemma
   18.23 -  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
   18.24 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
   18.25  quickcheck[random]
   18.26  quickcheck[exhaustive, expect = counterexample]
   18.27  oops
    19.1 --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Tue May 22 14:12:15 2018 +0200
    19.2 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Tue May 22 11:08:37 2018 +0200
    19.3 @@ -69,12 +69,12 @@
    19.4  definition
    19.5    inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    19.6  where
    19.7 -  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
    19.8 +  [simp]: "inter_list xs ys = filter (\<lambda>x. x \<in> set xs \<and> x \<in> set ys) xs"
    19.9  
   19.10  definition
   19.11    diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   19.12  where
   19.13 -  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
   19.14 +  [simp]: "diff_list xs ys = filter (\<lambda>x. x \<notin> set ys) xs"
   19.15  
   19.16  definition
   19.17    rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
    20.1 --- a/src/HOL/Random.thy	Tue May 22 14:12:15 2018 +0200
    20.2 +++ b/src/HOL/Random.thy	Tue May 22 11:08:37 2018 +0200
    20.3 @@ -116,7 +116,7 @@
    20.4  lemma select_weight_drop_zero:
    20.5    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
    20.6  proof -
    20.7 -  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
    20.8 +  have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = sum_list (map fst xs)"
    20.9      by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
   20.10    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
   20.11  qed
    21.1 --- a/src/HOL/ex/Quicksort.thy	Tue May 22 14:12:15 2018 +0200
    21.2 +++ b/src/HOL/ex/Quicksort.thy	Tue May 22 11:08:37 2018 +0200
    21.3 @@ -13,11 +13,11 @@
    21.4  
    21.5  fun quicksort :: "'a list \<Rightarrow> 'a list" where
    21.6    "quicksort []     = []"
    21.7 -| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
    21.8 +| "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
    21.9  
   21.10  lemma [code]:
   21.11    "quicksort []     = []"
   21.12 -  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
   21.13 +  "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
   21.14    by (simp_all add: not_le)
   21.15  
   21.16  lemma quicksort_permutes [simp]:
    22.1 --- a/src/HOL/ex/Radix_Sort.thy	Tue May 22 14:12:15 2018 +0200
    22.2 +++ b/src/HOL/ex/Radix_Sort.thy	Tue May 22 11:08:37 2018 +0200
    22.3 @@ -44,7 +44,7 @@
    22.4  lemma sorted_from_Suc2:
    22.5    "\<lbrakk> cols xss n; i < n;
    22.6      sorted_col i xss;
    22.7 -    \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
    22.8 +    \<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk>
    22.9    \<Longrightarrow> sorted_from i xss"
   22.10  proof(induction xss rule: induct_list012)
   22.11    case 1 show ?case by simp
   22.12 @@ -68,7 +68,7 @@
   22.13    proof(rule "3.IH"[OF _ "3.prems"(2)])
   22.14      show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
   22.15      show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
   22.16 -    show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
   22.17 +    show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))"
   22.18        using "3.prems"(4)
   22.19          sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
   22.20        by fastforce
   22.21 @@ -81,7 +81,7 @@
   22.22  shows "sorted_from i (sort_col i xss)"
   22.23  proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
   22.24    show "sorted_col i (sort_col i xss)" by(simp add: sorted)
   22.25 -  fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
   22.26 +  fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))"
   22.27    proof -
   22.28      from assms(3)
   22.29      have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"