diff -r 59f41804b3f8 -r 6c5b5ec53a0b Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 15:08:29 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 15:28:57 2010 +0200
@@ -15,9 +15,38 @@
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-unfolding equivp_reflp_symp_transp 
-unfolding reflp_def symp_def transp_def
-by auto
+  unfolding equivp_reflp_symp_transp 
+  unfolding reflp_def symp_def transp_def
+  by auto
+
+definition
+  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "memb x xs \<equiv> x \<in> set xs"
+
+definition
+  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
+
+lemma sub_list_cons:
+  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+  by (auto simp add: memb_def sub_list_def)
+
+lemma nil_not_cons:
+  shows "\<not> ([] \<approx> x # xs)"
+  and   "\<not> (x # xs \<approx> [])"
+  by auto
+
+lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
+  by (simp add: sub_list_def)
+
+lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
+  by (simp add: sub_list_def)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
 
 quotient_type
   'a fset = "'a list" / "list_eq"
@@ -42,11 +71,6 @@
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
 
-definition
-  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "memb x xs \<equiv> x \<in> set xs"
-
 quotient_definition
   fin ("_ |\<in>| _" [50, 51] 50)
 where
@@ -71,11 +95,6 @@
 
 section {* Augmenting an fset -- @{const finsert} *}
 
-lemma nil_not_cons:
-  shows "\<not> ([] \<approx> x # xs)"
-  and   "\<not> (x # xs \<approx> [])"
-  by auto
-
 lemma not_memb_nil:
   shows "\<not> memb x []"
   by (simp add: memb_def)
@@ -487,7 +506,7 @@
 proof (induct n arbitrary: l r)
   case 0
   have "fcard_raw l = 0" by fact
-  then have "\<forall>x. \<not> memb x l" using mem_card_not_0[of _ l] by auto
+  then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
   then have z: "l = []" using no_memb_nil by auto
   then have "r = []" sorry
   then show ?case using z list_eq2_refl by simp