1.1 --- a/NEWS	Thu May 20 07:36:50 2010 +0200
     1.2 +++ b/NEWS	Thu May 20 16:35:52 2010 +0200
     1.3 @@ -143,6 +143,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* List membership infix mem operation is only an input abbreviation.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Theory Library/Word.thy has been removed.  Use library Word/Word.thy for
    1.11  future developements;  former Library/Word.thy is still present in the AFP
    1.12  entry RSAPPS.

     2.1 --- a/src/HOL/List.thy	Thu May 20 07:36:50 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Thu May 20 16:35:52 2010 +0200
     2.3 @@ -4491,11 +4491,8 @@
     2.4  
     2.5  subsubsection {* Generation of efficient code *}
     2.6  
     2.7 -primrec
     2.8 -  member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
     2.9 -where 
    2.10 -  "x mem [] \<longleftrightarrow> False"
    2.11 -  | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
    2.12 +definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    2.13 +  mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
    2.14  
    2.15  primrec
    2.16    null:: "'a list \<Rightarrow> bool"
    2.17 @@ -4551,7 +4548,7 @@
    2.18    | "concat_map f (x#xs) = f x @ concat_map f xs"
    2.19  
    2.20  text {*
    2.21 -  Only use @{text mem} for generating executable code.  Otherwise use
    2.22 +  Only use @{text member} for generating executable code.  Otherwise use
    2.23    @{prop "x : set xs"} instead --- it is much easier to reason about.
    2.24    The same is true for @{const list_all} and @{const list_ex}: write
    2.25    @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
    2.26 @@ -4583,12 +4580,20 @@
    2.27    show ?case by (induct xs) (auto simp add: Cons aux)
    2.28  qed
    2.29  
    2.30 -lemma mem_iff [code_post]:
    2.31 -  "x mem xs \<longleftrightarrow> x \<in> set xs"
    2.32 -by (induct xs) auto
    2.33 -
    2.34  lemmas in_set_code [code_unfold] = mem_iff [symmetric]
    2.35  
    2.36 +lemma member_simps [simp, code]:
    2.37 +  "member [] y \<longleftrightarrow> False"
    2.38 +  "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
    2.39 +  by (auto simp add: mem_iff)
    2.40 +
    2.41 +lemma member_set:
    2.42 +  "member = set"
    2.43 +  by (simp add: expand_fun_eq mem_iff mem_def)
    2.44 +
    2.45 +abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
    2.46 +  "x mem xs \<equiv> member xs x" -- "for backward compatibility"
    2.47 +
    2.48  lemma empty_null:
    2.49    "xs = [] \<longleftrightarrow> null xs"
    2.50  by (cases xs) simp_all