# HG changeset patch
# User nipkow
# Date 1181149979 -7200
# Node ID e26ec695c9b3375dc4357d1ff489afc2f8f172f9
# Parent  4e61c67a87e38270ae89128d98b4787f51653841
changed filter syntax from : to <-

diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/Induct/SList.thy
--- 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 **)
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/Library/AssocList.thy
--- 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)"
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/Library/Multiset.thy
--- 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
 
 
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/MicroJava/BV/Kildall.thy
--- 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
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/MicroJava/BV/LBVComplete.thy
--- 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
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/MicroJava/BV/LBVCorrect.thy
--- 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 
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/MicroJava/BV/LBVSpec.thy
--- 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
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/MicroJava/BV/SemilatAlg.thy
--- 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
diff -r 4e61c67a87e3 -r e26ec695c9b3 src/HOL/ex/Qsort.thy
--- 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]: