# HG changeset patch
# User kuncar
# Date 1363181595 -3600
# Node ID deb59caefdb3c244823e66439ae53dbe86806e88
# Parent  f0865a641e762998593761e5749842c7d3d6db2a
rename fset_member to fmember and prove parametricity

diff -r f0865a641e76 -r deb59caefdb3 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 13:23:16 2013 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Mar 13 14:33:15 2013 +0100
@@ -93,18 +93,23 @@
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
 
-lift_definition fset_member :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
-   by simp
+lemma member_transfer:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
+by transfer_prover
+
+lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
+   parametric member_transfer by simp
 
 abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
-lemma fset_member_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
+lemma fmember_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
   by transfer auto
 
 text {* We can export code: *}
 
-export_code fnil fcons fappend fmap ffilter fset in SML
+export_code fnil fcons fappend fmap ffilter fset fmember in SML
 
 subsection {* Using transfer with type @{text "fset"} *}