--- a/src/HOL/Induct/SList.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/Induct/SList.thy Wed Jun 06 19:12:59 2007 +0200
@@ -231,14 +231,14 @@
no_translations
- "[x:xs . P]" == "filter (%x. P) xs"
+ "[x\<leftarrow>xs . P]" == "filter (%x. P) xs"
syntax
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
translations
- "[x:xs. P]" == "CONST filter(%x. P) xs"
+ "[x\<leftarrow>xs. P]" == "CONST filter(%x. P) xs"
"Alls x:xs. P" == "CONST list_all(%x. P)xs"
@@ -540,7 +540,7 @@
lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
by (induct_tac "xs" rule: list_induct, simp_all)
-lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
+lemma mem_filter [simp]: "x mem [x\<leftarrow>xs. P x ] = (x mem xs & P(x))"
by (induct_tac "xs" rule: list_induct, simp_all)
(** list_all **)
--- a/src/HOL/Library/AssocList.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/Library/AssocList.thy Wed Jun 06 19:12:59 2007 +0200
@@ -52,7 +52,7 @@
note length_filter_le [of "\<lambda>p. fst p \<noteq> fst a" al]
also have "\<And>n. n \<le> Suc n"
by simp
- finally have "length [p\<in>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
+ finally have "length [p\<leftarrow>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
with Cons show ?case
by auto
qed
@@ -189,7 +189,7 @@
by (induct al rule: clearjunk.induct)
(simp_all add: dom_clearjunk notin_filter_fst delete_def)
-lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<in>ps . fst q \<noteq> a] k = map_of ps k"
+lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<leftarrow>ps . fst q \<noteq> a] k = map_of ps k"
by (induct ps) auto
lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
@@ -204,7 +204,7 @@
case Nil thus ?case by simp
next
case (Cons p ps)
- from Cons have "length (clearjunk [q\<in>ps . fst q \<noteq> fst p]) \<le> length [q\<in>ps . fst q \<noteq> fst p]"
+ from Cons have "length (clearjunk [q\<leftarrow>ps . fst q \<noteq> fst p]) \<le> length [q\<leftarrow>ps . fst q \<noteq> fst p]"
by (simp add: delete_def)
also have "\<dots> \<le> length ps"
by simp
@@ -212,7 +212,7 @@
by (simp add: delete_def)
qed
-lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<in>ps . fst q \<noteq> a] = ps"
+lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<leftarrow>ps . fst q \<noteq> a] = ps"
by (induct ps) auto
lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
@@ -334,7 +334,7 @@
qed
lemma update_filter:
- "a\<noteq>k \<Longrightarrow> update k v [q\<in>ps . fst q \<noteq> a] = [q\<in>update k v ps . fst q \<noteq> a]"
+ "a\<noteq>k \<Longrightarrow> update k v [q\<leftarrow>ps . fst q \<noteq> a] = [q\<leftarrow>update k v ps . fst q \<noteq> a]"
by (induct ps) auto
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
@@ -460,7 +460,7 @@
lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
by (induct al) (auto simp add: dom_map_ran)
-lemma map_ran_filter: "map_ran f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_ran f ps. fst p \<noteq> a]"
+lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
by (induct ps) auto
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
--- a/src/HOL/Library/Multiset.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 06 19:12:59 2007 +0200
@@ -786,11 +786,11 @@
done
lemma multiset_of_compl_union [simp]:
- "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
+ "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
by (induct xs) (auto simp: union_ac)
lemma count_filter:
- "count (multiset_of xs) x = length [y \<in> xs. y = x]"
+ "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
by (induct xs) auto
--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Jun 06 19:12:59 2007 +0200
@@ -48,7 +48,7 @@
lemma (in semilat) nth_merges:
"\<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>
- (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
+ (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Jun 06 19:12:59 2007 +0200
@@ -82,13 +82,13 @@
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 [(p', t')\<in>ss1 . p'=pc+1]) ++_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 [(p',t')\<in>ss1 . p' = pc+1] ++_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: split_if_asm)
from app less
@@ -117,7 +117,7 @@
from x ss2 have
"?s2 =
(if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
- then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++_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
@@ -196,7 +196,7 @@
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 [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc
+ then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
else \<top>)" by (rule merge_def)
moreover {
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
@@ -209,7 +209,7 @@
} 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 [(p',t')\<in>?step.p'=pc+1] ++_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>"
@@ -217,7 +217,7 @@
moreover
from pc' bounded pc
have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
- hence "[(p',t')\<in>?step.p'=pc+1] = []" 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
@@ -264,7 +264,7 @@
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 [(p',t')\<in>?step.p'=pc+1] ++_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
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Jun 06 19:12:59 2007 +0200
@@ -88,7 +88,7 @@
also
from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
with cert_in_A step_in_A
- have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"
+ have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
by (rule merge_not_top_s)
finally
have "s' <=_r ?s2" using step_in_A cert_in_A True step
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Jun 06 19:12:59 2007 +0200
@@ -121,7 +121,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')\<in>S . p' = a] ++_f y"
+ shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_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')
@@ -180,7 +180,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') \<in> ss. p'=pc+1] ++_f x
+ map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_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)
@@ -210,15 +210,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')\<in>ls . p'=pc+1] ++_f ?if' =
- (map snd [(p',t')\<in>l#ls . p'=pc+1] ++_f x)"
+ "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' =
+ (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
by simp
ultimately
show ?thesis using True by simp
next
case False
moreover
- from ls have "set (map snd [(p', t')\<in>ls . p' = Suc pc]) \<subseteq> A" by auto
+ from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
ultimately show ?thesis by auto
qed
finally show "?P (l#ls) x" .
@@ -227,7 +227,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') \<in> ss. p'=pc+1] ++_f x)"
+ shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_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)
@@ -315,8 +315,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')\<in>ss . p'=pc+1]) \<subseteq> A" by auto
- with x have "(map snd [(p', t')\<in>ss . p'=pc+1] ++_f x) \<in> A"
+ 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"
by (auto intro!: plusplus_closed)
with s0 x show ?thesis by (simp add: merge_def T_A)
qed
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Wed Jun 06 19:12:59 2007 +0200
@@ -156,7 +156,7 @@
lemma ub1': includes semilat
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
- \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
+ \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
proof -
let "b <=_r ?map ++_f y" = ?thesis
@@ -175,7 +175,7 @@
lemma plusplus_empty:
"\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
- (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
+ (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
apply (induct S)
apply auto
done
--- a/src/HOL/ex/Qsort.thy Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/ex/Qsort.thy Wed Jun 06 19:12:59 2007 +0200
@@ -16,8 +16,8 @@
recdef qsort "measure (size o snd)"
"qsort(le, []) = []"
- "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
- qsort(le, [y:xs . le x y])"
+ "qsort(le, x#xs) = qsort(le, [y\<leftarrow>xs . ~ le x y]) @ [x] @
+ qsort(le, [y\<leftarrow>xs . le x y])"
(hints recdef_simp: length_filter_le[THEN le_less_trans])
lemma qsort_permutes [simp]:
@@ -43,7 +43,7 @@
recdef quickSort "measure size"
"quickSort [] = []"
- "quickSort (x#l) = quickSort [y:l. ~ x\<le>y] @ [x] @ quickSort [y:l. x\<le>y]"
+ "quickSort (x#l) = quickSort [y\<leftarrow>l. ~ x\<le>y] @ [x] @ quickSort [y\<leftarrow>l. x\<le>y]"
(hints recdef_simp: length_filter_le[THEN le_less_trans])
lemma quickSort_permutes[simp]: