author nipkow Wed Jun 06 13:04:52 2018 +0200 (11 months ago) changeset 68387 691c02d1699b parent 68385 54f07e7f68f9 parent 68386 98cf1c823c48 child 68398 194fa3d2d6a4 child 68403 223172b97d0b
merged
     1.1 --- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Jun 05 23:26:15 2018 +0200
1.2 +++ b/src/Doc/Tutorial/Inductive/AB.thy	Wed Jun 06 13:04:52 2018 +0200
1.3 @@ -64,13 +64,15 @@
1.4  \<close>
1.5
1.6  lemma correctness:
1.7 -  "(w \<in> S \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w))     \<and>
1.8 -   (w \<in> A \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1) \<and>
1.9 -   (w \<in> B \<longrightarrow> size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1)"
1.10 +  "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b])     \<and>
1.11 +   (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
1.12 +   (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
1.13
1.14  txt\<open>\noindent
1.15  These propositions are expressed with the help of the predefined @{term
1.16 -filter} function on lists. Remember that on lists @{text size} and @{text length} are synonymous.
1.17 +filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
1.18 +x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
1.19 +holds. Remember that on lists @{text size} and @{text length} are synonymous.
1.20
1.21  The proof itself is by rule induction and afterwards automatic:
1.22  \<close>
1.23 @@ -110,8 +112,8 @@
1.24  \<close>
1.25
1.26  lemma step1: "\<forall>i < size w.
1.27 -  \<bar>(int(size(filter P (take (i+1) w)))-int(size(filter (\<lambda>x. \<not>P x) (take (i+1) w))))
1.28 -   - (int(size(filter P (take i w)))-int(size(filter (\<lambda>x. \<not>P x) (take i w))))\<bar> \<le> 1"
1.29 +  \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
1.30 +   - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
1.31
1.32  txt\<open>\noindent
1.33  The lemma is a bit hard to read because of the coercion function
1.34 @@ -135,8 +137,8 @@
1.35  \<close>
1.36
1.37  lemma part1:
1.38 - "size(filter P w) = size(filter (\<lambda>x. \<not>P x) w)+2 \<Longrightarrow>
1.39 -  \<exists>i\<le>size w. size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1"
1.40 + "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
1.41 +  \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
1.42
1.43  txt\<open>\noindent
1.44  This is proved by @{text force} with the help of the intermediate value theorem,
1.45 @@ -155,10 +157,10 @@
1.46
1.47
1.48  lemma part2:
1.49 -  "\<lbrakk>size(filter P (take i w @ drop i w)) =
1.50 -    size(filter (\<lambda>x. \<not>P x) (take i w @ drop i w))+2;
1.51 -    size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1\<rbrakk>
1.52 -   \<Longrightarrow> size(filter P (drop i w)) = size(filter (\<lambda>x. \<not>P x) (drop i w))+1"
1.53 +  "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
1.54 +    size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
1.55 +    size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
1.56 +   \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
1.57  by(simp del: append_take_drop_id)
1.58
1.59  text\<open>\noindent
1.60 @@ -185,9 +187,9 @@
1.61  \<close>
1.62
1.63  theorem completeness:
1.64 -  "(size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w)     \<longrightarrow> w \<in> S) \<and>
1.65 -   (size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1 \<longrightarrow> w \<in> A) \<and>
1.66 -   (size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1 \<longrightarrow> w \<in> B)"
1.67 +  "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]     \<longrightarrow> w \<in> S) \<and>
1.68 +   (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
1.69 +   (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
1.70
1.71  txt\<open>\noindent
1.72  The proof is by induction on @{term w}. Structural induction would fail here
1.73 @@ -232,9 +234,9 @@
1.74   apply(clarify)
1.75  txt\<open>\noindent
1.76  This yields an index @{prop"i \<le> length v"} such that
1.77 -@{prop[display]"length (filter (\<lambda>x. x=a) (take i v)) = length (filter (\<lambda>x. x=b) (take i v)) + 1"}
1.78 +@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
1.79  With the help of @{thm[source]part2} it follows that
1.80 -@{prop[display]"length (filter (\<lambda>x. x=a) (drop i v)) = length (filter (\<lambda>x. x=b) (drop i v)) + 1"}
1.81 +@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
1.82  \<close>
1.83
1.84   apply(drule part2[of "\<lambda>x. x=a", simplified])

     2.1 --- a/src/HOL/Library/AList.thy	Tue Jun 05 23:26:15 2018 +0200
2.2 +++ b/src/HOL/Library/AList.thy	Wed Jun 06 13:04:52 2018 +0200
2.3 @@ -45,7 +45,7 @@
2.4    using assms by (simp add: update_keys)
2.5
2.6  lemma update_filter:
2.7 -  "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)"
2.8 +  "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
2.9    by (induct ps) auto
2.10
2.11  lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
2.12 @@ -361,12 +361,12 @@
2.13  proof -
2.14    have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
2.15      by auto
2.16 -  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"
2.17 +  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]"
2.18      by simp
2.19    assume "x \<notin> D"
2.20    then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
2.21      by auto
2.22 -  then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D) al"
2.23 +  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
2.24      by simp
2.25  qed
2.26
2.27 @@ -492,7 +492,7 @@
2.28  lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
2.29    by (simp add: map_ran_def split_def comp_def)
2.30
2.31 -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)"
2.32 +lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
2.33    by (simp add: map_ran_def filter_map split_def comp_def)
2.34
2.35  lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"

     3.1 --- a/src/HOL/Library/Finite_Map.thy	Tue Jun 05 23:26:15 2018 +0200
3.2 +++ b/src/HOL/Library/Finite_Map.thy	Wed Jun 06 13:04:52 2018 +0200
3.3 @@ -84,10 +84,10 @@
3.4  definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
3.5  "map_filter P m = (\<lambda>x. if P x then m x else None)"
3.6
3.7 -lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\<lambda>(k, _). P k) m)"
3.8 +lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
3.9  proof
3.10    fix x
3.11 -  show "map_filter P (map_of m) x = map_of (filter (\<lambda>(k, _). P k) m) x"
3.12 +  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
3.13      by (induct m) (auto simp: map_filter_def)
3.14  qed
3.15

     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Jun 05 23:26:15 2018 +0200
4.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 06 13:04:52 2018 +0200
4.3 @@ -1888,7 +1888,7 @@
4.4  apply simp
4.5  done
4.6
4.7 -lemma mset_compl_union [simp]: "mset (filter P xs) + mset (filter (\<lambda>x. \<not>P x) xs) = mset xs"
4.8 +lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
4.9    by (induct xs) auto
4.10
4.11  lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
4.12 @@ -2582,14 +2582,14 @@
4.13    show "mset ys = mset xs" by simp
4.14    from \<open>sorted (map f ys)\<close>
4.15    show "sorted (map f ys)" .
4.16 -  show "filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" if "k \<in> set ys" for k
4.17 +  show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
4.18    proof -
4.19      from mset_equal
4.20      have set_equal: "set xs = set ys" by (rule mset_eq_setD)
4.21      with that have "insert k (set ys) = set ys" by auto
4.22      with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))"
4.24 -    from inj have "filter (\<lambda>x. f k = f x) ys = filter (HOL.eq k) ys"
4.25 +    from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
4.26        by (auto intro!: inj_on_filter_key_eq)
4.27      also have "\<dots> = replicate (count (mset ys) k) k"
4.29 @@ -2597,7 +2597,7 @@
4.30        using mset_equal by simp
4.31      also have "\<dots> = filter (HOL.eq k) xs"
4.33 -    also have "\<dots> = filter (\<lambda>x. f k = f x) xs"
4.34 +    also have "\<dots> = [x\<leftarrow>xs . f k = f x]"
4.35        using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal)
4.36      finally show ?thesis .
4.37    qed
4.38 @@ -2610,9 +2610,9 @@
4.39    by (rule sort_key_inj_key_eq) (simp_all add: assms)
4.40
4.41  lemma sort_key_by_quicksort:
4.42 -  "sort_key f xs = sort_key f (filter (\<lambda>x. f x < f (xs ! (length xs div 2))) xs)
4.43 -    @ filter (\<lambda>x. f x = f (xs ! (length xs div 2))) xs
4.44 -    @ sort_key f (filter (\<lambda>x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs")
4.45 +  "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
4.46 +    @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
4.47 +    @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
4.48  proof (rule properties_for_sort_key)
4.49    show "mset ?rhs = mset ?lhs"
4.50      by (rule multiset_eqI) (auto simp add: mset_filter)
4.51 @@ -2623,14 +2623,14 @@
4.52    assume "l \<in> set ?rhs"
4.53    let ?pivot = "f (xs ! (length xs div 2))"
4.54    have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
4.55 -  have "filter (\<lambda>x. f x = f l) (sort_key f xs) = filter (\<lambda>x. f x = f l) xs"
4.56 +  have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
4.57      unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
4.58 -  with * have **: "filter (\<lambda>x. f l = f x) (sort_key f xs) = filter (\<lambda>x. f l = f x) xs" by simp
4.59 +  with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
4.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
4.61 -  then have "\<And>P. filter (\<lambda>x. P (f x) ?pivot \<and> f l = f x) (sort_key f xs) =
4.62 -    filter (\<lambda>x. P (f l) ?pivot \<and> f l = f x) (sort_key f xs)" by simp
4.63 +  then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
4.64 +    [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
4.65    note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
4.66 -  show "filter (\<lambda>x. f l = f x) ?rhs = filter (\<lambda>x. f l = f x) ?lhs"
4.67 +  show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
4.68    proof (cases "f l" ?pivot rule: linorder_cases)
4.69      case less
4.70      then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
4.71 @@ -2648,15 +2648,15 @@
4.72  qed
4.73
4.74  lemma sort_by_quicksort:
4.75 -  "sort xs = sort (filter (\<lambda>x. x < xs ! (length xs div 2)) xs)
4.76 -    @ filter (\<lambda>x. x = xs ! (length xs div 2)) xs
4.77 -    @ sort (filter (\<lambda>x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs")
4.78 +  "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
4.79 +    @ [x\<leftarrow>xs. x = xs ! (length xs div 2)]
4.80 +    @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
4.81    using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
4.82
4.83  text \<open>A stable parametrized quicksort\<close>
4.84
4.85  definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
4.86 -  "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)"
4.87 +  "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
4.88
4.89  lemma part_code [code]:
4.90    "part f pivot [] = ([], [], [])"

     5.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Tue Jun 05 23:26:15 2018 +0200
5.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Wed Jun 06 13:04:52 2018 +0200
5.3 @@ -38,7 +38,7 @@
5.4
5.5  lemma (in Semilat) nth_merges:
5.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>
5.7 -  (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p"
5.8 +  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
5.9    (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
5.10  proof (induct ps)
5.11    show "\<And>ss. ?P ss []" by simp

     6.1 --- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Tue Jun 05 23:26:15 2018 +0200
6.2 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Jun 06 13:04:52 2018 +0200
6.3 @@ -80,13 +80,13 @@
6.4      assume merge: "?s1 \<noteq> T"
6.5      from x ss1 have "?s1 =
6.6        (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
6.7 -      then (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss1)) ++_f x
6.8 +      then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
6.9        else \<top>)"
6.10        by (rule merge_def)
6.11      with merge obtain
6.12        app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'"
6.13             (is "?app ss1") and
6.14 -      sum: "(map snd (filter (\<lambda>(p',t'). p' = pc+1) ss1) ++_f x) = ?s1"
6.15 +      sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1"
6.16             (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
6.17        by (simp split: if_split_asm)
6.18      from app less
6.19 @@ -115,7 +115,7 @@
6.20      from x ss2 have
6.21        "?s2 =
6.22        (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
6.23 -      then map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss2) ++_f x
6.24 +      then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
6.25        else \<top>)"
6.26        by (rule merge_def)
6.27      ultimately have ?thesis by simp
6.28 @@ -194,7 +194,7 @@
6.29    ultimately
6.30    have "merge c pc ?step (c!Suc pc) =
6.31      (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
6.32 -    then map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc
6.33 +    then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
6.34      else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
6.35    moreover {
6.36      fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
6.37 @@ -207,7 +207,7 @@
6.38    } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
6.39    moreover
6.40    from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
6.41 -  hence "map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc \<noteq> \<top>"
6.42 +  hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>"
6.43           (is "?map ++_f _ \<noteq> _")
6.44    proof (rule disjE)
6.45      assume pc': "Suc pc = length \<phi>"
6.46 @@ -215,7 +215,7 @@
6.47      moreover
6.48      from pc' bounded pc
6.49      have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
6.50 -    hence "filter (\<lambda>(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False)
6.51 +    hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False)
6.52      hence "?map = []" by simp
6.53      ultimately show ?thesis by (simp add: B_neq_T)
6.54    next
6.55 @@ -262,7 +262,7 @@
6.56    hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
6.57    ultimately
6.58    have "merge c pc ?step (c!Suc pc) =
6.59 -    map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s)
6.60 +    map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s)
6.61    hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
6.62    also {
6.63      from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp

     7.1 --- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Tue Jun 05 23:26:15 2018 +0200
7.2 +++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Wed Jun 06 13:04:52 2018 +0200
7.3 @@ -88,7 +88,7 @@
7.4      also
7.5      from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
7.6      with cert_in_A step_in_A
7.7 -    have "?merge = (map snd (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
7.8 +    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
7.9        by (rule merge_not_top_s)
7.10      finally
7.11      have "s' <=_r ?s2" using step_in_A cert_in_A True step

     8.1 --- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Tue Jun 05 23:26:15 2018 +0200
8.2 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Jun 06 13:04:52 2018 +0200
8.3 @@ -113,7 +113,7 @@
8.4  lemma (in Semilat) pp_ub1':
8.5    assumes S: "sndset S \<subseteq> A"
8.6    assumes y: "y \<in> A" and ab: "(a, b) \<in> set S"
8.7 -  shows "b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
8.8 +  shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
8.9  proof -
8.10    from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
8.11    with semilat y ab show ?thesis by - (rule ub1')
8.12 @@ -172,7 +172,7 @@
8.13    "\<And>x. x \<in> A \<Longrightarrow> sndset ss \<subseteq> A \<Longrightarrow>
8.14    merge c pc ss x =
8.15    (if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
8.16 -    map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x
8.17 +    map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
8.18    else \<top>)"
8.19    (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
8.20  proof (induct ss)
8.21 @@ -202,15 +202,15 @@
8.22        hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
8.23        moreover
8.24        from True have
8.25 -        "map snd (filter (\<lambda>(p',t'). p'=pc+1) ls) ++_f ?if' =
8.26 -        (map snd (filter (\<lambda>(p',t'). p'=pc+1) (l#ls)) ++_f x)"
8.27 +        "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' =
8.28 +        (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
8.29          by simp
8.30        ultimately
8.31        show ?thesis using True by simp
8.32      next
8.33        case False
8.34        moreover
8.35 -      from ls have "set (map snd (filter (\<lambda>(p', t'). p' = Suc pc) ls)) \<subseteq> A" by auto
8.36 +      from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
8.37        ultimately show ?thesis by auto
8.38      qed
8.39    finally show "?P (l#ls) x" .
8.40 @@ -219,7 +219,7 @@
8.41  lemma (in lbv) merge_not_top_s:
8.42    assumes x:  "x \<in> A" and ss: "sndset ss \<subseteq> A"
8.43    assumes m:  "merge c pc ss x \<noteq> \<top>"
8.44 -  shows "merge c pc ss x = (map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x)"
8.45 +  shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
8.46  proof -
8.47    from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')"
8.48      by (rule merge_not_top)
8.49 @@ -307,8 +307,8 @@
8.50    assumes s0: "sndset ss \<subseteq> A" and x: "x \<in> A"
8.51    shows "merge c pc ss x \<in> A"
8.52  proof -
8.53 -  from s0 have "set (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss)) \<subseteq> A" by auto
8.54 -  with x  have "(map snd (filter (\<lambda>(p', t'). p'=pc+1) ss) ++_f x) \<in> A"
8.55 +  from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
8.56 +  with x  have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
8.57      by (auto intro!: plusplus_closed semilat)
8.58    with s0 x show ?thesis by (simp add: merge_def T_A)
8.59  qed

     9.1 --- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Tue Jun 05 23:26:15 2018 +0200
9.2 +++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Wed Jun 06 13:04:52 2018 +0200
9.3 @@ -155,7 +155,7 @@
9.4  lemma ub1':
9.5    assumes "semilat (A, r, f)"
9.6    shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
9.7 -  \<Longrightarrow> b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
9.8 +  \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
9.9  proof -
9.10    interpret Semilat A r f using assms by (rule Semilat.intro)
9.11
9.12 @@ -175,7 +175,7 @@
9.13
9.14  lemma plusplus_empty:
9.15    "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
9.16 -   (map snd (filter (\<lambda>(p', t'). p' = q) S) ++_f ss ! q) = ss ! q"
9.17 +   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
9.18    by (induct S) auto
9.19
9.20  end

    10.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Jun 05 23:26:15 2018 +0200
10.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Jun 06 13:04:52 2018 +0200
10.3 @@ -317,7 +317,7 @@
10.4  | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
10.5
10.6  theorem S\<^sub>1_sound:
10.7 -"w \<in> S\<^sub>1 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
10.8 +"w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
10.9  nitpick [expect = genuine]
10.10  oops
10.11
10.12 @@ -330,7 +330,7 @@
10.13  | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
10.14
10.15  theorem S\<^sub>2_sound:
10.16 -"w \<in> S\<^sub>2 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
10.17 +"w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
10.18  nitpick [expect = genuine]
10.19  oops
10.20
10.21 @@ -343,12 +343,12 @@
10.22  | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
10.23
10.24  theorem S\<^sub>3_sound:
10.25 -"w \<in> S\<^sub>3 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
10.26 +"w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
10.27  nitpick [card = 1-5, expect = none]
10.28  sorry
10.29
10.30  theorem S\<^sub>3_complete:
10.31 -"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>3"
10.32 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
10.33  nitpick [expect = genuine]
10.34  oops
10.35
10.36 @@ -362,19 +362,19 @@
10.37  | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
10.38
10.39  theorem S\<^sub>4_sound:
10.40 -"w \<in> S\<^sub>4 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
10.41 +"w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
10.42  nitpick [card = 1-5, expect = none]
10.43  sorry
10.44
10.45  theorem S\<^sub>4_complete:
10.46 -"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>4"
10.47 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
10.48  nitpick [card = 1-5, expect = none]
10.49  sorry
10.50
10.51  theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
10.52 -"w \<in> S\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
10.53 -"w \<in> A\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) + 1"
10.54 -"w \<in> B\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = b) w) = length (filter (\<lambda>x. x = a) w) + 1"
10.55 +"w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
10.56 +"w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
10.57 +"w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
10.58  nitpick [card = 1-5, expect = none]
10.59  sorry
10.60

    11.1 --- a/src/HOL/Nominal/Examples/W.thy	Tue Jun 05 23:26:15 2018 +0200
11.2 +++ b/src/HOL/Nominal/Examples/W.thy	Wed Jun 06 13:04:52 2018 +0200
11.3 @@ -9,7 +9,7 @@
11.4  abbreviation
11.5    "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60)
11.6  where
11.7 -  "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
11.8 +  "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
11.9
11.10  lemma difference_eqvt_tvar[eqvt]:
11.11    fixes pi::"tvar prm"

    12.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Jun 05 23:26:15 2018 +0200
12.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Jun 06 13:04:52 2018 +0200
12.3 @@ -71,7 +71,7 @@
12.4  oops
12.5
12.6  theorem S\<^sub>1_sound:
12.7 -"S\<^sub>1p w \<Longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
12.8 +"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
12.9  quickcheck[tester=smart_exhaustive, size=15]
12.10  oops
12.11
12.12 @@ -113,7 +113,7 @@
12.13  oops
12.14  *)
12.15  theorem S\<^sub>2_sound:
12.16 -"S\<^sub>2p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
12.17 +"S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
12.18  quickcheck[tester=smart_exhaustive, size=5, iterations=10]
12.19  oops
12.20
12.21 @@ -133,16 +133,16 @@
12.22
12.23
12.24  lemma S\<^sub>3_sound:
12.25 -"S\<^sub>3p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
12.26 +"S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
12.27  quickcheck[tester=smart_exhaustive, size=10, iterations=10]
12.28  oops
12.29
12.30 -lemma "\<not> (length w > 2) \<or> \<not> (length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w))"
12.31 +lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
12.32  quickcheck[size=10, tester = smart_exhaustive]
12.33  oops
12.34
12.35  theorem S\<^sub>3_complete:
12.36 -"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>3p w"
12.37 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> S\<^sub>3p w"
12.38  (*quickcheck[generator=SML]*)
12.39  quickcheck[tester=smart_exhaustive, size=10, iterations=100]
12.40  oops
12.41 @@ -158,12 +158,12 @@
12.42  | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
12.43
12.44  theorem S\<^sub>4_sound:
12.45 -"S\<^sub>4p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
12.46 +"S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
12.47  quickcheck[tester = smart_exhaustive, size=5, iterations=1]
12.48  oops
12.49
12.50  theorem S\<^sub>4_complete:
12.51 -"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>4p w"
12.52 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
12.53  quickcheck[tester = smart_exhaustive, size=5, iterations=1]
12.54  oops
12.55
12.56 @@ -301,7 +301,7 @@
12.57
12.58  subsection "Compressed matrix"
12.59
12.60 -definition "sparsify xs = filter (\<lambda>i. snd i \<noteq> 0) (zip [0..<length xs] xs)"
12.61 +definition "sparsify xs = [i \<leftarrow> zip [0..<length xs] xs. snd i \<noteq> 0]"
12.62  (*
12.63  lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
12.64    by (auto simp: sparsify_def set_zip)

    13.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jun 05 23:26:15 2018 +0200
13.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 06 13:04:52 2018 +0200
13.3 @@ -2028,7 +2028,7 @@
13.4  private lemma pmf_of_list_aux:
13.5    assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
13.6    assumes "sum_list (map snd xs) = 1"
13.7 -  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) = 1"
13.8 +  shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
13.9  proof -
13.10    have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
13.11              (\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
13.12 @@ -2083,7 +2083,7 @@
13.13    show "x \<in> set (map fst xs)"
13.14    proof (rule ccontr)
13.15      assume "x \<notin> set (map fst xs)"
13.16 -    hence "filter (\<lambda>z. fst z = x) xs = []" by (auto simp: filter_empty_conv)
13.17 +    hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
13.18      with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
13.19    qed
13.20  qed
13.21 @@ -2122,10 +2122,10 @@
13.22    have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
13.23      by simp
13.24    also from assms
13.25 -    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))))"
13.26 +    have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
13.27      by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
13.28    also from assms
13.29 -    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)))"
13.30 +    have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
13.31      by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
13.32    also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
13.33        indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
13.34 @@ -2184,7 +2184,7 @@
13.35    {
13.36      fix x assume A: "x \<in> fst  set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
13.37      then obtain y where y: "(x, y) \<in> set xs" by auto
13.38 -    from B have "sum_list (map snd (filter (\<lambda>z. fst z = x) xs)) = 0"
13.39 +    from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
13.40        by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
13.41      moreover from y have "y \<in> snd  {xa \<in> set xs. fst xa = x}" by force
13.42      ultimately have "y = 0" using assms(1)
13.43 @@ -2199,11 +2199,11 @@
13.44    defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
13.45    shows   "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs"
13.46  proof -
13.47 -  have "map snd (filter (\<lambda>z. snd z \<noteq> 0) xs) = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
13.48 +  have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
13.49      by (induction xs) simp_all
13.50    with assms(1) show wf: "pmf_of_list_wf xs'"
13.51      by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
13.52 -  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
13.53 +  have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
13.54      unfolding xs'_def by (induction xs) simp_all
13.55    with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
13.56      by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)

    14.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue Jun 05 23:26:15 2018 +0200
14.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Jun 06 13:04:52 2018 +0200
14.3 @@ -186,7 +186,7 @@
14.4  oops
14.5
14.6  lemma
14.7 -  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
14.8 +  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
14.9  quickcheck[random, iterations = 10000]
14.10  quickcheck[exhaustive, expect = counterexample]
14.11  oops
14.12 @@ -228,13 +228,13 @@
14.13  oops
14.14
14.15  lemma
14.16 -  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
14.17 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
14.18  quickcheck[random]
14.19  quickcheck[exhaustive, expect = counterexample]
14.20  oops
14.21
14.22  lemma
14.23 -  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
14.24 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
14.25  quickcheck[random]
14.26  quickcheck[exhaustive, expect = counterexample]
14.27  oops

    15.1 --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Tue Jun 05 23:26:15 2018 +0200
15.2 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Wed Jun 06 13:04:52 2018 +0200
15.3 @@ -69,12 +69,12 @@
15.4  definition
15.5    inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
15.6  where
15.7 -  [simp]: "inter_list xs ys = filter (\<lambda>x. x \<in> set xs \<and> x \<in> set ys) xs"
15.8 +  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
15.9
15.10  definition
15.11    diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
15.12  where
15.13 -  [simp]: "diff_list xs ys = filter (\<lambda>x. x \<notin> set ys) xs"
15.14 +  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
15.15
15.16  definition
15.17    rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"

    16.1 --- a/src/HOL/Random.thy	Tue Jun 05 23:26:15 2018 +0200
16.2 +++ b/src/HOL/Random.thy	Wed Jun 06 13:04:52 2018 +0200
16.3 @@ -116,7 +116,7 @@
16.4  lemma select_weight_drop_zero:
16.5    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
16.6  proof -
16.7 -  have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = sum_list (map fst xs)"
16.8 +  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
16.9      by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
16.10    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
16.11  qed

    17.1 --- a/src/HOL/ex/Quicksort.thy	Tue Jun 05 23:26:15 2018 +0200
17.2 +++ b/src/HOL/ex/Quicksort.thy	Wed Jun 06 13:04:52 2018 +0200
17.3 @@ -13,11 +13,11 @@
17.4
17.5  fun quicksort :: "'a list \<Rightarrow> 'a list" where
17.6    "quicksort []     = []"
17.7 -| "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
17.8 +| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
17.9
17.10  lemma [code]:
17.11    "quicksort []     = []"
17.12 -  "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
17.13 +  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
17.15
17.16  lemma quicksort_permutes [simp]:

    18.1 --- a/src/HOL/ex/Radix_Sort.thy	Tue Jun 05 23:26:15 2018 +0200
18.2 +++ b/src/HOL/ex/Radix_Sort.thy	Wed Jun 06 13:04:52 2018 +0200
18.3 @@ -44,7 +44,7 @@
18.4  lemma sorted_from_Suc2:
18.5    "\<lbrakk> cols xss n; i < n;
18.6      sorted_col i xss;
18.7 -    \<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk>
18.8 +    \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
18.9    \<Longrightarrow> sorted_from i xss"
18.10  proof(induction xss rule: induct_list012)
18.11    case 1 show ?case by simp
18.12 @@ -68,7 +68,7 @@
18.13    proof(rule "3.IH"[OF _ "3.prems"(2)])
18.14      show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
18.15      show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
18.16 -    show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))"
18.17 +    show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
18.18        using "3.prems"(4)
18.19          sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
18.20        by fastforce
18.21 @@ -81,7 +81,7 @@
18.22  shows "sorted_from i (sort_col i xss)"
18.23  proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
18.24    show "sorted_col i (sort_col i xss)" by(simp add: sorted)
18.25 -  fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))"
18.26 +  fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
18.27    proof -
18.28      from assms(3)
18.29      have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"