# HG changeset patch
# User haftmann
# Date 1274366152 -7200
# Node ID 6c699a8e692722a5bd6ad6f929460817b9019a57
# Parent  8096a4c755ebed71a58debb1237a952361e961be
turned old-style mem into an input abbreviation

diff -r 8096a4c755eb -r 6c699a8e6927 NEWS
--- a/NEWS	Thu May 20 07:36:50 2010 +0200
+++ b/NEWS	Thu May 20 16:35:52 2010 +0200
@@ -143,6 +143,9 @@
 
 *** HOL ***
 
+* List membership infix mem operation is only an input abbreviation.
+INCOMPATIBILITY.
+
 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy for
 future developements;  former Library/Word.thy is still present in the AFP
 entry RSAPPS.
diff -r 8096a4c755eb -r 6c699a8e6927 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 20 07:36:50 2010 +0200
+++ b/src/HOL/List.thy	Thu May 20 16:35:52 2010 +0200
@@ -4491,11 +4491,8 @@
 
 subsubsection {* Generation of efficient code *}
 
-primrec
-  member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
-where 
-  "x mem [] \<longleftrightarrow> False"
-  | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
+definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
 
 primrec
   null:: "'a list \<Rightarrow> bool"
@@ -4551,7 +4548,7 @@
   | "concat_map f (x#xs) = f x @ concat_map f xs"
 
 text {*
-  Only use @{text mem} for generating executable code.  Otherwise use
+  Only use @{text member} for generating executable code.  Otherwise use
   @{prop "x : set xs"} instead --- it is much easier to reason about.
   The same is true for @{const list_all} and @{const list_ex}: write
   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
@@ -4583,12 +4580,20 @@
   show ?case by (induct xs) (auto simp add: Cons aux)
 qed
 
-lemma mem_iff [code_post]:
-  "x mem xs \<longleftrightarrow> x \<in> set xs"
-by (induct xs) auto
-
 lemmas in_set_code [code_unfold] = mem_iff [symmetric]
 
+lemma member_simps [simp, code]:
+  "member [] y \<longleftrightarrow> False"
+  "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
+  by (auto simp add: mem_iff)
+
+lemma member_set:
+  "member = set"
+  by (simp add: expand_fun_eq mem_iff mem_def)
+
+abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
+  "x mem xs \<equiv> member xs x" -- "for backward compatibility"
+
 lemma empty_null:
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all