--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Tue May 22 11:08:37 2018 +0200
@@ -113,7 +113,7 @@
lemma (in Semilat) pp_ub1':
assumes S: "snd`set S \<subseteq> A"
assumes y: "y \<in> A" and ab: "(a, b) \<in> set S"
- shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
+ shows "b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
proof -
from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
with semilat y ab show ?thesis by - (rule ub1')
@@ -172,7 +172,7 @@
"\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
merge c pc ss x =
(if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
- map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
+ map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x
else \<top>)"
(is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
proof (induct ss)
@@ -202,15 +202,15 @@
hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
moreover
from True have
- "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' =
- (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
+ "map snd (filter (\<lambda>(p',t'). p'=pc+1) ls) ++_f ?if' =
+ (map snd (filter (\<lambda>(p',t'). p'=pc+1) (l#ls)) ++_f x)"
by simp
ultimately
show ?thesis using True by simp
next
case False
moreover
- from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
+ from ls have "set (map snd (filter (\<lambda>(p', t'). p' = Suc pc) ls)) \<subseteq> A" by auto
ultimately show ?thesis by auto
qed
finally show "?P (l#ls) x" .
@@ -219,7 +219,7 @@
lemma (in lbv) merge_not_top_s:
assumes x: "x \<in> A" and ss: "snd`set ss \<subseteq> A"
assumes m: "merge c pc ss x \<noteq> \<top>"
- shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
+ shows "merge c pc ss x = (map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x)"
proof -
from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')"
by (rule merge_not_top)
@@ -307,8 +307,8 @@
assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
shows "merge c pc ss x \<in> A"
proof -
- from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
- with x have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
+ from s0 have "set (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss)) \<subseteq> A" by auto
+ with x have "(map snd (filter (\<lambda>(p', t'). p'=pc+1) ss) ++_f x) \<in> A"
by (auto intro!: plusplus_closed semilat)
with s0 x show ?thesis by (simp add: merge_def T_A)
qed