changed filter syntax from : to <-
authornipkow
Wed Jun 06 19:12:59 2007 +0200 (2007-06-06)
changeset 23281e26ec695c9b3
parent 23280 4e61c67a87e3
child 23282 dfc459989d24
changed filter syntax from : to <-
src/HOL/Induct/SList.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/Multiset.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/BV/SemilatAlg.thy
src/HOL/ex/Qsort.thy
     1.1 --- a/src/HOL/Induct/SList.thy	Wed Jun 06 19:12:40 2007 +0200
     1.2 +++ b/src/HOL/Induct/SList.thy	Wed Jun 06 19:12:59 2007 +0200
     1.3 @@ -231,14 +231,14 @@
     1.4  
     1.5  
     1.6  no_translations
     1.7 -  "[x:xs . P]" == "filter (%x. P) xs"
     1.8 +  "[x\<leftarrow>xs . P]" == "filter (%x. P) xs"
     1.9  
    1.10  syntax
    1.11    (* Special syntax for list_all and filter *)
    1.12    "@Alls"       :: "[idt, 'a list, bool] => bool"        ("(2Alls _:_./ _)" 10)
    1.13  
    1.14  translations
    1.15 -  "[x:xs. P]" == "CONST filter(%x. P) xs"
    1.16 +  "[x\<leftarrow>xs. P]" == "CONST filter(%x. P) xs"
    1.17    "Alls x:xs. P" == "CONST list_all(%x. P)xs"
    1.18  
    1.19  
    1.20 @@ -540,7 +540,7 @@
    1.21  lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
    1.22  by (induct_tac "xs" rule: list_induct, simp_all)
    1.23  
    1.24 -lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
    1.25 +lemma mem_filter [simp]: "x mem [x\<leftarrow>xs. P x ] = (x mem xs & P(x))"
    1.26  by (induct_tac "xs" rule: list_induct, simp_all)
    1.27  
    1.28  (** list_all **)
     2.1 --- a/src/HOL/Library/AssocList.thy	Wed Jun 06 19:12:40 2007 +0200
     2.2 +++ b/src/HOL/Library/AssocList.thy	Wed Jun 06 19:12:59 2007 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4    note length_filter_le [of "\<lambda>p. fst p \<noteq> fst a" al] 
     2.5    also have "\<And>n. n \<le> Suc n"
     2.6      by simp
     2.7 -  finally have "length [p\<in>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
     2.8 +  finally have "length [p\<leftarrow>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
     2.9    with Cons show ?case
    2.10      by auto
    2.11  qed
    2.12 @@ -189,7 +189,7 @@
    2.13    by (induct al rule: clearjunk.induct) 
    2.14       (simp_all add: dom_clearjunk notin_filter_fst delete_def)
    2.15  
    2.16 -lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<in>ps . fst q \<noteq> a] k = map_of ps k"
    2.17 +lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<leftarrow>ps . fst q \<noteq> a] k = map_of ps k"
    2.18    by (induct ps) auto
    2.19  
    2.20  lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
    2.21 @@ -204,7 +204,7 @@
    2.22    case Nil thus ?case by simp
    2.23  next
    2.24    case (Cons p ps)
    2.25 -  from Cons have "length (clearjunk [q\<in>ps . fst q \<noteq> fst p]) \<le> length [q\<in>ps . fst q \<noteq> fst p]" 
    2.26 +  from Cons have "length (clearjunk [q\<leftarrow>ps . fst q \<noteq> fst p]) \<le> length [q\<leftarrow>ps . fst q \<noteq> fst p]" 
    2.27      by (simp add: delete_def)
    2.28    also have "\<dots> \<le> length ps"
    2.29      by simp
    2.30 @@ -212,7 +212,7 @@
    2.31      by (simp add: delete_def)
    2.32  qed
    2.33  
    2.34 -lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<in>ps . fst q \<noteq> a] = ps"
    2.35 +lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<leftarrow>ps . fst q \<noteq> a] = ps"
    2.36    by (induct ps) auto
    2.37              
    2.38  lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
    2.39 @@ -334,7 +334,7 @@
    2.40  qed
    2.41  
    2.42  lemma update_filter: 
    2.43 -  "a\<noteq>k \<Longrightarrow> update k v [q\<in>ps . fst q \<noteq> a] = [q\<in>update k v ps . fst q \<noteq> a]"
    2.44 +  "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.45    by (induct ps) auto
    2.46  
    2.47  lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
    2.48 @@ -460,7 +460,7 @@
    2.49  lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
    2.50    by (induct al) (auto simp add: dom_map_ran)
    2.51  
    2.52 -lemma map_ran_filter: "map_ran f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_ran f ps. fst p \<noteq> a]"
    2.53 +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.54    by (induct ps) auto
    2.55  
    2.56  lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
     3.1 --- a/src/HOL/Library/Multiset.thy	Wed Jun 06 19:12:40 2007 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 06 19:12:59 2007 +0200
     3.3 @@ -786,11 +786,11 @@
     3.4    done
     3.5  
     3.6  lemma multiset_of_compl_union [simp]:
     3.7 -    "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
     3.8 +    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
     3.9    by (induct xs) (auto simp: union_ac)
    3.10  
    3.11  lemma count_filter:
    3.12 -    "count (multiset_of xs) x = length [y \<in> xs. y = x]"
    3.13 +    "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
    3.14    by (induct xs) auto
    3.15  
    3.16  
     4.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Jun 06 19:12:40 2007 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Jun 06 19:12:59 2007 +0200
     4.3 @@ -48,7 +48,7 @@
     4.4  
     4.5  lemma (in semilat) nth_merges:
     4.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>
     4.7 -  (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
     4.8 +  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
     4.9    (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
    4.10  proof (induct ps)
    4.11    show "\<And>ss. ?P ss []" by simp
     5.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 06 19:12:40 2007 +0200
     5.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 06 19:12:59 2007 +0200
     5.3 @@ -82,13 +82,13 @@
     5.4      assume merge: "?s1 \<noteq> T" 
     5.5      from x ss1 have "?s1 =
     5.6        (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
     5.7 -      then (map snd [(p', t')\<in>ss1 . p'=pc+1]) ++_f x
     5.8 +      then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
     5.9        else \<top>)" 
    5.10        by (rule merge_def)  
    5.11      with merge obtain
    5.12        app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
    5.13             (is "?app ss1") and
    5.14 -      sum: "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++_f x) = ?s1" 
    5.15 +      sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" 
    5.16             (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
    5.17        by (simp split: split_if_asm)
    5.18      from app less 
    5.19 @@ -117,7 +117,7 @@
    5.20      from x ss2 have 
    5.21        "?s2 =
    5.22        (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
    5.23 -      then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++_f x
    5.24 +      then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
    5.25        else \<top>)" 
    5.26        by (rule merge_def)
    5.27      ultimately have ?thesis by simp
    5.28 @@ -196,7 +196,7 @@
    5.29    ultimately
    5.30    have "merge c pc ?step (c!Suc pc) =
    5.31      (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
    5.32 -    then map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc
    5.33 +    then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
    5.34      else \<top>)" by (rule merge_def)
    5.35    moreover {
    5.36      fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
    5.37 @@ -209,7 +209,7 @@
    5.38    } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
    5.39    moreover
    5.40    from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
    5.41 -  hence "map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
    5.42 +  hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
    5.43           (is "?map ++_f _ \<noteq> _")
    5.44    proof (rule disjE)
    5.45      assume pc': "Suc pc = length \<phi>"
    5.46 @@ -217,7 +217,7 @@
    5.47      moreover 
    5.48      from pc' bounded pc 
    5.49      have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
    5.50 -    hence "[(p',t')\<in>?step.p'=pc+1] = []" by (blast intro: filter_False) 
    5.51 +    hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False) 
    5.52      hence "?map = []" by simp
    5.53      ultimately show ?thesis by (simp add: B_neq_T)  
    5.54    next
    5.55 @@ -264,7 +264,7 @@
    5.56    hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
    5.57    ultimately
    5.58    have "merge c pc ?step (c!Suc pc) =
    5.59 -    map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
    5.60 +    map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
    5.61    hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
    5.62    also {
    5.63      from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
     6.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Jun 06 19:12:40 2007 +0200
     6.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Jun 06 19:12:59 2007 +0200
     6.3 @@ -88,7 +88,7 @@
     6.4      also    
     6.5      from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
     6.6      with cert_in_A step_in_A
     6.7 -    have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"
     6.8 +    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
     6.9        by (rule merge_not_top_s) 
    6.10      finally
    6.11      have "s' <=_r ?s2" using step_in_A cert_in_A True step 
     7.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Jun 06 19:12:40 2007 +0200
     7.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Jun 06 19:12:59 2007 +0200
     7.3 @@ -121,7 +121,7 @@
     7.4  lemma (in semilat) pp_ub1':
     7.5    assumes S: "snd`set S \<subseteq> A" 
     7.6    assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" 
     7.7 -  shows "b <=_r map snd [(p', t')\<in>S . p' = a] ++_f y"
     7.8 +  shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
     7.9  proof -
    7.10    from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
    7.11    with semilat y ab show ?thesis by - (rule ub1')
    7.12 @@ -180,7 +180,7 @@
    7.13    "\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
    7.14    merge c pc ss x = 
    7.15    (if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
    7.16 -    map snd [(p',t') \<in> ss. p'=pc+1] ++_f x
    7.17 +    map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
    7.18    else \<top>)" 
    7.19    (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
    7.20  proof (induct ss)
    7.21 @@ -210,15 +210,15 @@
    7.22        hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
    7.23        moreover
    7.24        from True have 
    7.25 -        "map snd [(p',t')\<in>ls . p'=pc+1] ++_f ?if' = 
    7.26 -        (map snd [(p',t')\<in>l#ls . p'=pc+1] ++_f x)"
    7.27 +        "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' = 
    7.28 +        (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
    7.29          by simp
    7.30        ultimately
    7.31        show ?thesis using True by simp
    7.32      next
    7.33        case False 
    7.34        moreover
    7.35 -      from ls have "set (map snd [(p', t')\<in>ls . p' = Suc pc]) \<subseteq> A" by auto
    7.36 +      from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
    7.37        ultimately show ?thesis by auto
    7.38      qed
    7.39    finally show "?P (l#ls) x" .
    7.40 @@ -227,7 +227,7 @@
    7.41  lemma (in lbv) merge_not_top_s:
    7.42    assumes x:  "x \<in> A" and ss: "snd`set ss \<subseteq> A"
    7.43    assumes m:  "merge c pc ss x \<noteq> \<top>"
    7.44 -  shows "merge c pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++_f x)"
    7.45 +  shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
    7.46  proof -
    7.47    from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')" 
    7.48      by (rule merge_not_top)
    7.49 @@ -315,8 +315,8 @@
    7.50    assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
    7.51    shows "merge c pc ss x \<in> A"
    7.52  proof -
    7.53 -  from s0 have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> A" by auto
    7.54 -  with x  have "(map snd [(p', t')\<in>ss . p'=pc+1] ++_f x) \<in> A"
    7.55 +  from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
    7.56 +  with x  have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
    7.57      by (auto intro!: plusplus_closed)
    7.58    with s0 x show ?thesis by (simp add: merge_def T_A)
    7.59  qed
     8.1 --- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Wed Jun 06 19:12:40 2007 +0200
     8.2 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Wed Jun 06 19:12:59 2007 +0200
     8.3 @@ -156,7 +156,7 @@
     8.4  
     8.5  lemma ub1': includes semilat
     8.6  shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
     8.7 -  \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y" 
     8.8 +  \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
     8.9  proof -
    8.10    let "b <=_r ?map ++_f y" = ?thesis
    8.11  
    8.12 @@ -175,7 +175,7 @@
    8.13  
    8.14  lemma plusplus_empty:  
    8.15    "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
    8.16 -   (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
    8.17 +   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
    8.18  apply (induct S)
    8.19  apply auto 
    8.20  done
     9.1 --- a/src/HOL/ex/Qsort.thy	Wed Jun 06 19:12:40 2007 +0200
     9.2 +++ b/src/HOL/ex/Qsort.thy	Wed Jun 06 19:12:59 2007 +0200
     9.3 @@ -16,8 +16,8 @@
     9.4  
     9.5  recdef qsort "measure (size o snd)"
     9.6      "qsort(le, [])   = []"
     9.7 -    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
     9.8 -		       qsort(le, [y:xs . le x y])"
     9.9 +    "qsort(le, x#xs) = qsort(le, [y\<leftarrow>xs . ~ le x y]) @ [x] @
    9.10 +		       qsort(le, [y\<leftarrow>xs . le x y])"
    9.11  (hints recdef_simp: length_filter_le[THEN le_less_trans])
    9.12  
    9.13  lemma qsort_permutes [simp]:
    9.14 @@ -43,7 +43,7 @@
    9.15  
    9.16  recdef quickSort "measure size"
    9.17      "quickSort []   = []"
    9.18 -    "quickSort (x#l) = quickSort [y:l. ~ x\<le>y] @ [x] @ quickSort [y:l. x\<le>y]"
    9.19 +    "quickSort (x#l) = quickSort [y\<leftarrow>l. ~ x\<le>y] @ [x] @ quickSort [y\<leftarrow>l. x\<le>y]"
    9.20  (hints recdef_simp: length_filter_le[THEN le_less_trans])
    9.21  
    9.22  lemma quickSort_permutes[simp]: