
diff -r 0a857f662e4c -r 39951d71bfce Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:09:07 2010 +0200
@@ -8,6 +8,8 @@
 imports Quotient Quotient_List List
 begin
 
+text {* Definiton of List relation and the quotient type *}
+
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
@@ -15,10 +17,16 @@
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-  unfolding equivp_reflp_symp_transp 
+  unfolding equivp_reflp_symp_transp
   unfolding reflp_def symp_def transp_def
   by auto
 
+quotient_type
+  'a fset = "'a list" / "list_eq"
+  by (rule list_eq_equivp)
+
+text {* Raw definitions *}
+
 definition
   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 where
@@ -29,24 +37,188 @@
 where
   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
-quotient_type
-  'a fset = "'a list" / "list_eq"
-by (rule list_eq_equivp)
+fun
+  fcard_raw :: "'a list \<Rightarrow> nat"
+where
+  fcard_raw_nil:  "fcard_raw [] = 0"
+| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
-lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
-  by (simp add: sub_list_def)
+primrec
+  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "finter_raw [] l = []"
+| "finter_raw (h # t) l =
+     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
-lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
-  by (simp add: sub_list_def)
+fun
+  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
+where
+  "delete_raw [] x = []"
+| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+
+definition
+  rsp_fold
+where
+  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
-lemma [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
+primrec
+  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+where
+  "ffold_raw f z [] = z"
+| "ffold_raw f z (a # A) =
+     (if (rsp_fold f) then
+       if memb a A then ffold_raw f z A
+       else f a (ffold_raw f z A)
+     else z)"
+
+text {* Respectfullness *}
 
 lemma [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  by (auto simp add: sub_list_def)
+
+lemma memb_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op =) memb memb"
+  by (auto simp add: memb_def)
+
+lemma nil_rsp[quot_respect]:
+  shows "[] \<approx> []"
+  by simp
+
+lemma cons_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+  by simp
+
+lemma map_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+  by auto
+
+lemma set_rsp[quot_respect]:
+  "(op \<approx> ===> op =) set set"
+  by auto
+
+lemma list_equiv_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+  by auto
+
+lemma not_memb_nil:
+  shows "\<not> memb x []"
+  by (simp add: memb_def)
+
+lemma memb_cons_iff:
+  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma memb_finter_raw:
+  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
+  by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+  by (simp add: memb_def[symmetric] memb_finter_raw)
+
+lemma memb_delete_raw:
+  "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
+  by (induct xs arbitrary: x y) (auto simp add: memb_def)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
+lemma fcard_raw_gt_0:
+  assumes a: "x \<in> set xs"
+  shows "0 < fcard_raw xs"
+  using a by (induct xs) (auto simp add: memb_def)
+
+lemma fcard_raw_delete_one:
+  shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
+
+lemma fcard_raw_rsp_aux:
+  assumes a: "xs \<approx> ys"
+  shows "fcard_raw xs = fcard_raw ys"
+  using a
+  apply (induct xs arbitrary: ys)
+  apply (auto simp add: memb_def)
+  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
+  apply (auto)
+  apply (drule_tac x="x" in spec)
+  apply (blast)
+  apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
+  apply (simp add: fcard_raw_delete_one memb_def)
+  apply (case_tac "a \<in> set ys")
+  apply (simp only: if_True)
+  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
+  apply (drule Suc_pred'[OF fcard_raw_gt_0])
+  apply (auto)
+  done
+
+lemma fcard_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+  by (simp add: fcard_raw_rsp_aux)
+
+lemma memb_absorb:
+  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
+
+lemma not_memb_delete_raw_ident:
+  shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma memb_commute_ffold_raw:
+  "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+  apply (induct b)
+  apply (simp_all add: not_memb_nil)
+  apply (auto)
+  apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident  rsp_fold_def  memb_cons_iff)
+  done
+
+lemma ffold_raw_rsp_pre:
+  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+  apply (induct a arbitrary: b)
+  apply (simp add: memb_absorb memb_def none_memb_nil)
+  apply (simp)
+  apply (rule conjI)
+  apply (rule_tac [!] impI)
+  apply (rule_tac [!] conjI)
+  apply (rule_tac [!] impI)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+  apply (simp)
+  apply (simp add: memb_cons_iff memb_def)
+  apply (auto)[1]
+  apply (drule_tac x="e" in spec)
+  apply (blast)
+  apply (case_tac b)
+  apply (simp_all)
+  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+  apply (simp only:)
+  apply (rule_tac f="f a1" in arg_cong)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+  apply (simp)
+  apply (simp add: memb_delete_raw)
+  apply (auto simp add: memb_cons_iff)[1]
+  apply (erule memb_commute_ffold_raw)
+  apply (drule_tac x="a1" in spec)
+  apply (simp add: memb_cons_iff)
+  apply (simp add: memb_cons_iff)
+  apply (case_tac b)
+  apply (simp_all)
+  done
+
+lemma [quot_respect]:
+  "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+  by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+
+text {* Distributive lattice with bot *}
+
 lemma sub_list_not_eq:
   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
   by (auto simp add: sub_list_def)
@@ -63,7 +235,42 @@
   "sub_list [] x"
   by (simp add: sub_list_def)
 
-instantiation fset :: (type) bot
+lemma sub_list_append_left:
+  "sub_list x (x @ y)"
+  by (simp add: sub_list_def)
+
+lemma sub_list_append_right:
+  "sub_list y (x @ y)"
+  by (simp add: sub_list_def)
+
+lemma sub_list_inter_left:
+  shows "sub_list (finter_raw x y) x"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma sub_list_inter_right:
+  shows "sub_list (finter_raw x y) y"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma sub_list_list_eq:
+  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
+  unfolding sub_list_def list_eq.simps by blast
+
+lemma sub_list_append:
+  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
+  unfolding sub_list_def by auto
+
+lemma sub_list_inter:
+  "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma append_inter_distrib:
+  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+  apply (induct x)
+  apply (simp_all add: memb_def)
+  apply (simp add: memb_def[symmetric] memb_finter_raw)
+  by (auto simp add: memb_def)
+
+instantiation fset :: (type) "{bot,distrib_lattice}"
 begin
 
 quotient_definition
@@ -93,40 +300,6 @@
 where
   "xs |\<subset>| ys \<equiv> xs < ys"
 
-instance
-proof
-  fix x y z :: "'a fset"
-  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
-    unfolding less_fset by (lifting sub_list_not_eq)
-  show "x |\<subseteq>| x" by (lifting sub_list_refl)
-  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
-next
-  fix x y z :: "'a fset"
-  assume a: "x |\<subseteq>| y"
-  assume b: "y |\<subseteq>| z"
-  show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
-qed
-end
-
-lemma sub_list_append_left:
-  "sub_list x (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_right:
-  "sub_list y (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_list_eq:
-  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
-  unfolding sub_list_def list_eq.simps by blast
-
-lemma sub_list_append:
-  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
-  unfolding sub_list_def by auto
-
-instantiation fset :: (type) "semilattice_sup"
-begin
-
 quotient_definition
   "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 is
@@ -137,11 +310,33 @@
 where
   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 
+quotient_definition
+  "inf  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+  "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
+abbreviation
+  finter (infixl "|\<inter>|" 65)
+where
+  "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+
 instance
 proof
-  fix x y :: "'a fset"
+  fix x y z :: "'a fset"
+  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+    unfolding less_fset by (lifting sub_list_not_eq)
+  show "x |\<subseteq>| x" by (lifting sub_list_refl)
+  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
   show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
   show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
+  show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
+  show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
+  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+next
+  fix x y z :: "'a fset"
+  assume a: "x |\<subseteq>| y"
+  assume b: "y |\<subseteq>| z"
+  show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 next
   fix x y :: "'a fset"
   assume a: "x |\<subseteq>| y"
@@ -152,10 +347,16 @@
   assume a: "y |\<subseteq>| x"
   assume b: "z |\<subseteq>| x"
   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+next
+  fix x y z :: "'a fset"
+  assume a: "x |\<subseteq>| y"
+  assume b: "x |\<subseteq>| z"
+  show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 qed
+
 end
 
-section {* Empty fset, Finsert and Membership *}
+section {* Finsert and Membership *}
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -178,18 +379,6 @@
 where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
-lemma memb_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op =) memb memb"
-by (auto simp add: memb_def)
-
-lemma nil_rsp[quot_respect]:
-  shows "[] \<approx> []"
-by simp
-
-lemma cons_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
-
 section {* Augmenting an fset -- @{const finsert} *}
 
 lemma nil_not_cons:
@@ -197,22 +386,10 @@
   and   "\<not> (x # xs \<approx> [])"
   by auto
 
-lemma not_memb_nil:
-  shows "\<not> memb x []"
-  by (simp add: memb_def)
-
 lemma no_memb_nil:
   "(\<forall>x. \<not> memb x xs) = (xs = [])"
   by (simp add: memb_def)
 
-lemma none_memb_nil:
-  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
-  by (simp add: memb_def)
-
-lemma memb_cons_iff:
-  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
-  by (induct xs) (auto simp add: memb_def)
-
 lemma memb_consI1:
   shows "memb x (x # xs)"
   by (simp add: memb_def)
@@ -221,10 +398,6 @@
   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
   by (simp add: memb_def)
 
-lemma memb_absorb:
-  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
-  by (induct xs) (auto simp add: memb_def id_simps)
-
 section {* Singletons *}
 
 lemma singleton_list_eq:
@@ -239,12 +412,6 @@
 
 section {* Cardinality of finite sets *}
 
-fun
-  fcard_raw :: "'a list \<Rightarrow> nat"
-where
-  fcard_raw_nil:  "fcard_raw [] = 0"
-| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
-
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
 is
@@ -254,10 +421,6 @@
   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
   by (induct xs) (auto simp add: memb_def)
 
-lemma fcard_raw_gt_0:
-  assumes a: "x \<in> set xs"
-  shows "0 < fcard_raw xs"
-  using a by (induct xs) (auto simp add: memb_def)
 
 lemma fcard_raw_not_memb:
   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
@@ -284,10 +447,6 @@
   apply auto
   done
 
-lemma fcard_raw_delete_one:
-  shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
-  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
-
 lemma fcard_raw_suc_memb:
   assumes a: "fcard_raw A = Suc n"
   shows "\<exists>a. memb a A"
@@ -307,32 +466,7 @@
   then show ?thesis using fcard_raw_0[of A] by simp
 qed
 
-lemma fcard_raw_rsp_aux:
-  assumes a: "xs \<approx> ys"
-  shows "fcard_raw xs = fcard_raw ys"
-  using a
-  apply(induct xs arbitrary: ys)
-  apply(auto simp add: memb_def)
-  apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
-  apply simp
-  apply auto
-  apply (drule_tac x="x" in spec)
-  apply blast
-  apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
-  apply(simp add: fcard_raw_delete_one memb_def)
-  apply (case_tac "a \<in> set ys")
-  apply (simp only: if_True)
-  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
-  apply (drule Suc_pred'[OF fcard_raw_gt_0])
-  apply auto
-  done
-
-lemma fcard_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
-  by (simp add: fcard_raw_rsp_aux)
-
-
-section {* fmap and fset comprehension *}
+section {* fmap *}
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
@@ -347,12 +481,6 @@
   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
-text {* raw section *}
-
-lemma map_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by auto
-
 lemma cons_left_comm:
   "x # y # xs \<approx> y # x # xs"
   by auto
@@ -382,32 +510,10 @@
 
 section {* deletion *}
 
-fun
-  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
-where
-  "delete_raw [] x = []"
-| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
-
-lemma memb_delete_raw:
-  "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
-  by (induct xs arbitrary: x y) (auto simp add: memb_def)
-
-lemma delete_raw_rsp:
-  "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
-  by (simp add: memb_def[symmetric] memb_delete_raw)
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
-  by (simp add: memb_def[symmetric] memb_delete_raw)
-
 lemma memb_delete_raw_ident:
   shows "\<not> memb x (delete_raw xs x)"
   by (induct xs) (auto simp add: memb_def)
 
-lemma not_memb_delete_raw_ident:
-  shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
-  by (induct xs) (auto simp add: memb_def)
-
 lemma fset_raw_delete_raw_cases:
   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
   by (induct xs) (auto simp add: memb_def)
@@ -420,100 +526,14 @@
   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
-lemma set_rsp[quot_respect]:
-  "(op \<approx> ===> op =) set set"
-  by auto
 
-definition
-  rsp_fold
-where
-  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
-
-primrec
-  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
-where
-  "ffold_raw f z [] = z"
-| "ffold_raw f z (a # A) =
-     (if (rsp_fold f) then
-       if memb a A then ffold_raw f z A
-       else f a (ffold_raw f z A)
-     else z)"
-
-lemma memb_commute_ffold_raw:
-  "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
-  apply (induct b)
-  apply (simp add: not_memb_nil)
-  apply (simp add: ffold_raw.simps)
-  apply (rule conjI)
-  apply (rule_tac [!] impI)
-  apply (rule_tac [!] conjI)
-  apply (rule_tac [!] impI)
-  apply (simp_all add: memb_delete_raw)
-  apply (simp add: memb_cons_iff)
-  apply (simp add: not_memb_delete_raw_ident)
-  apply (simp add: memb_cons_iff rsp_fold_def)
-  done
 
-lemma ffold_raw_rsp_pre:
-  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
-  apply (induct a arbitrary: b)
-  apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
-  apply (simp add: ffold_raw.simps)
-  apply (rule conjI)
-  apply (rule_tac [!] impI)
-  apply (rule_tac [!] conjI)
-  apply (rule_tac [!] impI)
-  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
-  apply (simp)
-  apply (simp add: memb_cons_iff memb_def)
-  apply auto
-  apply (drule_tac x="e" in spec)
-  apply blast
-  apply (case_tac b)
-  apply simp_all
-  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
-  apply (simp only:)
-  apply (rule_tac f="f a1" in arg_cong)
-  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
-  apply simp
-  apply (simp add: memb_delete_raw)
-  apply (auto simp add: memb_cons_iff)[1]
-  apply (erule memb_commute_ffold_raw)
-  apply (drule_tac x="a1" in spec)
-  apply (simp add: memb_cons_iff)
-  apply (simp add: memb_cons_iff)
-  apply (case_tac b)
-  apply simp_all
-  done
 
-lemma [quot_respect]:
-  "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
-  by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
-
-primrec
-  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "finter_raw [] l = []"
-| "finter_raw (h # t) l =
-     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
 lemma finter_raw_empty:
   "finter_raw l [] = []"
   by (induct l) (simp_all add: not_memb_nil)
 
-lemma memb_finter_raw:
-  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
-  apply (induct xs)
-  apply (simp add: not_memb_nil)
-  apply (simp add: finter_raw.simps)
-  apply (simp add: memb_cons_iff)
-  apply auto
-  done
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-  by (simp add: memb_def[symmetric] memb_finter_raw)
-
 section {* Constants on the Quotient Type *} 
 
 quotient_definition
@@ -528,16 +548,6 @@
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   is "ffold_raw"
 
-quotient_definition
-  finter (infix "|\<inter>|" 50)
-where
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is "finter_raw"
-
-lemma funion_sym_pre:
-  "xs @ ys \<approx> ys @ xs"
-  by auto
-
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
   by auto
@@ -551,9 +561,6 @@
 is
   "concat"
 
-lemma list_equiv_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-  by auto
 
 text {* alternate formulation with a different decomposition principle
   and a proof of equivalence *}
@@ -579,7 +586,7 @@
   apply (case_tac "memb a (aa # A)")
   apply (simp_all only: memb_cons_iff)
   apply (case_tac [!] "a = aa")
-  apply (simp_all add: delete_raw.simps)
+  apply (simp_all)
   apply (case_tac "memb a A")
   apply (auto simp add: memb_def)[2]
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
@@ -593,6 +600,10 @@
   using a cons_delete_list_eq2[of e r]
   by simp
 
+lemma delete_raw_rsp:
+  "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
 lemma list_eq2_equiv_aux:
   assumes a: "fcard_raw l = n"
   and b: "l \<approx> r"
@@ -731,13 +742,9 @@
   shows "S |\<union>| {||} = S"
   by (lifting append_Nil2)
 
-lemma funion_sym:
-  shows "S |\<union>| T = T |\<union>| S"
-  by (lifting funion_sym_pre)
+thm sup.commute[where 'a="'a fset"]
 
-lemma funion_assoc:
-  shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
-  by (lifting append_assoc)
+thm sup.assoc[where 'a="'a fset"]
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
@@ -745,7 +752,7 @@
 
 lemma singleton_union_right:
   "S |\<union>| {|a|} = finsert a S"
-  by (subst funion_sym) simp
+  by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}
 




