src/HOL/MicroJava/DFA/LBVComplete.thy

   have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp
   moreover {
     assume merge: "?s1 \<noteq> T" 
     from x ss1 have "?s1 =
       (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
-      then (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss1)) ++_f x
+      then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
       else \<top>)" 
       by (rule merge_def)  
     with merge obtain
       app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
            (is "?app ss1") and
-      sum: "(map snd (filter (\<lambda>(p',t'). p' = pc+1) ss1) ++_f x) = ?s1" 
+      sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" 
            (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
       by (simp split: if_split_asm)
     from app less 
     have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
     moreover {

     }
     moreover
     from x ss2 have 
       "?s2 =
       (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
-      then map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss2) ++_f x
+      then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
       else \<top>)" 
       by (rule merge_def)
     ultimately have ?thesis by simp
   }
   ultimately show ?thesis by (cases "?s1 = \<top>") auto

   from pres this pc 
   have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2) 
   ultimately
   have "merge c pc ?step (c!Suc pc) =
     (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
-    then map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc
+    then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
     else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
   moreover {
     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
     with less have "s' <=_r \<phi>!pc'" by auto
     also 

     hence "\<phi>!pc' = c!pc'" ..
     finally have "s' <=_r c!pc'" .
   } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
   moreover
   from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
-  hence "map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc \<noteq> \<top>" 
+  hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
          (is "?map ++_f _ \<noteq> _")
   proof (rule disjE)
     assume pc': "Suc pc = length \<phi>"
     with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2)
     moreover 
     from pc' bounded pc 
     have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
-    hence "filter (\<lambda>(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False) 
+    hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False) 
     hence "?map = []" by simp
     ultimately show ?thesis by (simp add: B_neq_T)  
   next
     assume pc': "Suc pc < length \<phi>"
     from pc' phi have "\<phi>!Suc pc \<in> A" by simp

   moreover
   from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti)
   hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
   ultimately
   have "merge c pc ?step (c!Suc pc) =
-    map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s) 
+    map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
   hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
   also {
     from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
     moreover note cert_suc
     moreover from stepA have "set ?map \<subseteq> A" by auto