# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287154040 -3600
# Node ID f99578469d08a995f06d55ef0cd9750a23df9245
# Parent  767161329839840db5b3991f873cc3f8fca49c6f
Further reorganisation and cleaning

diff -r 767161329839 -r f99578469d08 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 14:11:23 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 15:47:20 2010 +0100
@@ -48,13 +48,6 @@
 where
   "fcard_raw xs = card (set xs)"
 
-(*
-definition
-  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "finter_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
-*)
-
 primrec
   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -62,11 +55,12 @@
 | "finter_raw (x # xs) ys =
     (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
 
-primrec
+
+definition
   fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
-  "fminus_raw ys [] = ys"
-| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
+  "fminus_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
+
 
 definition
   rsp_fold
@@ -91,8 +85,7 @@
 
 lemma set_fminus_raw[simp]: 
   shows "set (fminus_raw xs ys) = (set xs - set ys)"
-  by (induct ys arbitrary: xs) (auto)
-
+  by (auto simp add: fminus_raw_def)
 
 
 section {* Quotient composition lemmas *}
@@ -405,11 +398,13 @@
 
 end
 
-section {* Finsert and Membership *}
+
+section {* Definitions for fsets *}
+
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is "Cons"
+  is "Cons"
 
 syntax
   "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
@@ -432,13 +427,11 @@
 
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat"
-is
-  fcard_raw
+  is fcard_raw
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-is
-  map
+  is map
 
 quotient_definition
   "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -450,19 +443,18 @@
 
 quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
-  is "ffold_raw"
+  is ffold_raw
 
 quotient_definition
   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-is
-  "concat"
+  is concat
 
 quotient_definition
   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "filter"
+  is filter
 
-text {* Compositional Respectfullness and Preservation *}
+
+subsection {* Compositional Respectfulness and Preservation *}
 
 lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
   by (fact compose_list_refl)
@@ -545,58 +537,9 @@
     by (rule pred_compI) (rule a', rule d')
 qed
 
-text {* Raw theorems. Finsert, memb, singleron, sub_list *}
-
-lemma nil_not_cons:
-  shows "\<not> ([] \<approx> x # xs)"
-  and   "\<not> (x # xs \<approx> [])"
-  by auto
-
-lemma no_memb_nil:
-  "(\<forall>x. \<not> memb x xs) = (xs = [])"
-  by (simp add: memb_def)
-
-lemma memb_consI1:
-  shows "memb x (x # xs)"
-  by (simp add: memb_def)
-
-lemma memb_consI2:
-  shows "memb x xs \<Longrightarrow> memb x (y # xs)"
-  by (simp add: memb_def)
-
-lemma singleton_list_eq:
-  shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
-  by (simp)
-
-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 fminus_raw_red: 
-  "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
-  by (induct ys arbitrary: xs x) (simp_all)
-
-text {* Cardinality of finite sets *}
-
-(* used in memb_card_not_0 *)
-lemma fcard_raw_0:
-  shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
-  unfolding fcard_raw_def
-  by (induct xs) (auto)
-
-(* used in list_eq2_equiv *)
-lemma memb_card_not_0:
-  assumes a: "memb a A"
-  shows "\<not>(fcard_raw A = 0)"
-proof -
-  have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
-  then have "\<not>A \<approx> []" by (simp add: memb_def)
-  then show ?thesis using fcard_raw_0[of A] by simp
-qed
 
 
-
-section {* ? *}
+section {* Cases *}
 
 
 lemma fset_raw_strong_cases:
@@ -609,7 +552,8 @@
   case (Cons a xs)
   have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
   have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
-  have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+  have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
+    by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
   have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
   proof -
     fix x :: 'a
@@ -632,24 +576,6 @@
   then show thesis using a c by blast
 qed
 
-section {* deletion *}
-
-
-lemma fset_raw_removeAll_cases:
-  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
-  by (induct xs) (auto simp add: memb_def)
-
-lemma fremoveAll_filter:
-  "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
-  by (induct xs) simp_all
-
-lemma fcard_raw_delete:
-  "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
-  by (auto simp add: fcard_raw_def memb_def)
-
-lemma inj_map_eq_iff:
-  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
-  by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
 
 text {* alternate formulation with a different decomposition principle
   and a proof of equivalence *}
@@ -702,8 +628,8 @@
     proof (induct n arbitrary: l r)
       case 0
       have "fcard_raw l = 0" by fact
-      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 "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto
+      then have z: "l = []" unfolding memb_def by auto
       then have "r = []" using `l \<approx> r` by simp
       then show ?case using z list_eq2_refl by simp
     next
@@ -718,7 +644,7 @@
       then obtain a where e: "memb a l" by auto
       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
 	unfolding memb_def by auto
-      have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
+      have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def)
       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
@@ -731,35 +657,59 @@
   then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
-text {* Lifted theorems *}
+
+section {* Lifted theorems *}
+
+
+subsection {* fin *}
 
-lemma not_fin_fnil: "x |\<notin>| {||}"
+lemma not_fin_fnil: 
+  shows "x |\<notin>| {||}"
+  by (descending) (simp add: memb_def)
+
+lemma fin_set: 
+  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
   by (descending) (simp add: memb_def)
 
+lemma fnotin_set: 
+  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
+  by (descending) (simp add: memb_def)
+
+lemma fset_eq_iff:
+  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+  by (descending) (auto simp add: memb_def)
+
+lemma none_fin_fempty:
+  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
+  by (descending) (simp add: memb_def)
+
+
+subsection {* finsert *}
+
 lemma fin_finsert_iff[simp]:
-  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+  shows "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
   by (descending) (simp add: memb_def)
 
 lemma
   shows finsertI1: "x |\<in>| finsert x S"
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
-  by (lifting memb_consI1 memb_consI2)
+  by (descending, simp add: memb_def)+
 
 lemma finsert_absorb[simp]:
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
   by (descending) (auto simp add: memb_def)
 
 lemma fempty_not_finsert[simp]:
-  "{||} \<noteq> finsert x S"
-  "finsert x S \<noteq> {||}"
-  by (lifting nil_not_cons)
+  shows "{||} \<noteq> finsert x S"
+  and   "finsert x S \<noteq> {||}"
+  by (descending, simp)+
 
 lemma finsert_left_comm:
-  "finsert x (finsert y S) = finsert y (finsert x S)"
+  shows "finsert x (finsert y S) = finsert y (finsert x S)"
   by (descending) (auto)
 
 lemma finsert_left_idem:
-  "finsert x (finsert x S) = finsert x S"
+  shows "finsert x (finsert x S) = finsert x S"
   by (descending) (auto)
 
 lemma fsingleton_eq[simp]:
@@ -767,27 +717,199 @@
   by (descending) (auto)
 
 
-text {* fset *}
+(* FIXME: is this in any case a useful lemma *)
+lemma fin_mdef:
+  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
+  by (descending) (auto simp add: memb_def fminus_raw_def)
+
+
+subsection {* fset *}
 
 lemma fset_simps[simp]:
   "fset {||} = ({} :: 'a set)"
   "fset (finsert (x :: 'a) S) = insert x (fset S)"
   by (lifting set.simps)
 
-lemma fin_fset:
-  "x \<in> fset S \<longleftrightarrow> x |\<in>| S"
-  by (lifting memb_def[symmetric])
+lemma finite_fset [simp]: 
+  shows "finite (fset S)"
+  by (descending) (simp)
+
+lemma fset_cong:
+  shows "fset S = fset T \<longleftrightarrow> S = T"
+  by (descending) (simp)
+
+lemma ffilter_set [simp]: 
+  shows "fset (ffilter P xs) = P \<inter> fset xs"
+  by (descending) (auto simp add: mem_def)
+
+lemma fdelete_set [simp]: 
+  shows "fset (fdelete x xs) = fset xs - {x}"
+  by (descending) (simp)
+
+lemma finter_set [simp]: 
+  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
+  by (lifting set_finter_raw)
+
+lemma funion_set [simp]: 
+  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
+  by (lifting set_append)
+
+lemma fminus_set [simp]: 
+  shows "fset (xs - ys) = fset xs - fset ys"
+  by (lifting set_fminus_raw)
+
+
+subsection {* funion *}
+
+lemmas [simp] =
+  sup_bot_left[where 'a="'a fset", standard]
+  sup_bot_right[where 'a="'a fset", standard]
+
+lemma funion_finsert[simp]:
+  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+  by (lifting append.simps(2))
+
+lemma singleton_funion_left:
+  shows "{|a|} |\<union>| S = finsert a S"
+  by simp
 
-lemma none_fin_fempty:
-  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
+lemma singleton_funion_right:
+  shows "S |\<union>| {|a|} = finsert a S"
+  by (subst sup.commute) simp
+
+lemma fin_funion:
+  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
+  by (descending) (simp add: memb_def)
+
+
+subsection {* fminus *}
+
+lemma fminus_fin: 
+  shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
+  by (descending) (simp add: memb_def)
+
+lemma fminus_red: 
+  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+  by (descending) (auto simp add: memb_def)
+
+lemma fminus_red_fin[simp]: 
+  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+  by (simp add: fminus_red)
+
+lemma fminus_red_fnotin[simp]: 
+  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+  by (simp add: fminus_red)
+
+lemma fin_fminus_fnotin: 
+  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+  unfolding fin_set fminus_set
+  by blast
+
+lemma fin_fnotin_fminus: 
+  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+  unfolding fin_set fminus_set
+  by blast
+
+
+section {* fdelete *}
+
+lemma fin_fdelete:
+  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
   by (descending) (simp add: memb_def)
 
-lemma fset_cong:
-  "S = T \<longleftrightarrow> fset S = fset T"
-  by (lifting list_eq.simps)
+lemma fnotin_fdelete:
+  shows "x |\<notin>| fdelete x S"
+  by (descending) (simp add: memb_def)
+
+lemma fnotin_fdelete_ident:
+  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
+  by (descending) (simp add: memb_def)
+
+lemma fset_fdelete_cases:
+  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
+  by (descending) (auto simp add: memb_def insert_absorb)
+  
+
+section {* finter *}
+
+lemma finter_empty_l:
+  shows "{||} |\<inter>| S = {||}"
+  by simp
+
+lemma finter_empty_r:
+  shows "S |\<inter>| {||} = {||}"
+  by simp
+
+lemma finter_finsert:
+  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
+  by (descending) (simp add: memb_def)
+
+lemma fin_finter:
+  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
+  by (descending) (simp add: memb_def)
 
 
-section {* fcard *}
+subsection {* fsubset *}
+
+lemma fsubseteq_set: 
+  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
+  by (descending) (simp add: sub_list_def)
+
+lemma fsubset_set: 
+  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
+  unfolding less_fset_def 
+  by (descending) (auto simp add: sub_list_def)
+
+lemma fsubseteq_finsert:
+  shows "(finsert x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
+  by (descending) (simp add: sub_list_def memb_def)
+
+lemma fsubset_fin: 
+  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+  by (descending) (auto simp add: sub_list_def memb_def)
+
+(* FIXME: no type ord *)
+(*
+lemma fsubset_finsert:
+  shows "(finsert x xs) |\<subset>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subset>| ys"
+  by (descending) (simp add: sub_list_def memb_def)
+*)
+
+lemma fsubseteq_fempty:
+  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
+  by (descending) (simp add: sub_list_def)
+
+(* also problem with ord *)
+lemma not_fsubset_fnil: 
+  shows "\<not> xs |\<subset>| {||}"
+  by (metis fset_simps(1) fsubset_set not_psubset_empty)
+
+
+section {* fmap *}
+
+lemma fmap_simps [simp]:
+   shows "fmap f {||} = {||}"
+  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
+  by (descending, simp)+
+
+lemma fmap_set_image [simp]:
+  shows "fset (fmap f S) = f ` (fset S)"
+  by (descending) (simp)
+
+lemma inj_fmap_eq_iff:
+  shows "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
+  by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
+
+lemma fmap_funion: 
+  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
+  by (descending) (simp)
+
+
+subsection {* fcard *}
+
+lemma fcard_set: 
+  shows "fcard xs = card (fset xs)"
+  by (lifting fcard_raw_def)
 
 lemma fcard_finsert_if [simp]:
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
@@ -816,7 +938,7 @@
 lemma fcard_suc: 
   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
   apply(descending)
-  apply(simp add: fcard_raw_def memb_def)
+  apply(auto simp add: fcard_raw_def memb_def)
   apply(drule card_eq_SucD)
   apply(auto)
   apply(rule_tac x="b" in exI)
@@ -825,8 +947,8 @@
   done
 
 lemma fcard_delete:
-  "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
-  by (lifting fcard_raw_delete)
+  shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
+  by (descending) (simp add: fcard_raw_def memb_def)
 
 lemma fcard_suc_memb: 
   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
@@ -840,24 +962,135 @@
   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
   by (descending) (auto simp add: fcard_raw_def memb_def)
 
+lemma fcard_mono: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+  unfolding fcard_set fsubseteq_set
+  by (simp add: card_mono[OF finite_fset])
 
-section {* funion *}
+lemma fcard_fsubset_eq: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+  unfolding fcard_set fsubseteq_set
+  by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
+
+lemma psubset_fcard_mono: 
+  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+  unfolding fcard_set fsubset_set
+  by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter: 
+  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+  unfolding fcard_set funion_set finter_set
+  by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint: 
+  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+  unfolding fcard_set funion_set 
+  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
+  by (metis finter_set fset_simps(1))
+
+lemma fcard_delete1_less: 
+  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
+  unfolding fcard_set fin_set fdelete_set 
+  by (rule card_Diff1_less[OF finite_fset])
 
-lemmas [simp] =
-  sup_bot_left[where 'a="'a fset", standard]
-  sup_bot_right[where 'a="'a fset", standard]
+lemma fcard_delete2_less: 
+  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
+  unfolding fcard_set fdelete_set fin_set
+  by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le: 
+  shows "fcard (fdelete x xs) \<le> fcard xs"
+  unfolding fdelete_set fcard_set
+  by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset: 
+  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+  unfolding fcard_set fsubseteq_set fsubset_set
+  by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le: 
+  shows "fcard (fmap f xs) \<le> fcard xs"
+  unfolding fcard_set fmap_set_image
+  by (rule card_image_le[OF finite_fset])
+
+lemma fcard_fminus_finsert[simp]:
+  assumes "a |\<in>| A" and "a |\<notin>| B"
+  shows "fcard (A - finsert a B) = fcard (A - B) - 1"
+  using assms 
+  unfolding fin_set fcard_set fminus_set
+  by (simp add: card_Diff_insert[OF finite_fset])
+
+lemma fcard_fminus_fsubset:
+  assumes "B |\<subseteq>| A"
+  shows "fcard (A - B) = fcard A - fcard B"
+  using assms 
+  unfolding fsubseteq_set fcard_set fminus_set
+  by (rule card_Diff_subset[OF finite_fset])
 
-lemma funion_finsert[simp]:
-  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
-  by (lifting append.simps(2))
+lemma fcard_fminus_subset_finter:
+  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+  unfolding finter_set fcard_set fminus_set
+  by (rule card_Diff_subset_Int) (simp)
+
+
+section {* fconcat *}
+
+lemma fconcat_fempty:
+  shows "fconcat {||} = {||}"
+  by (lifting concat.simps(1))
+
+lemma fconcat_finsert:
+  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+  by (lifting concat.simps(2))
+
+lemma fconcat_finter:
+  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+  by (lifting concat_append)
+
+
+section {* ffilter *}
+
+lemma subseteq_filter: 
+  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+  by  (descending) (auto simp add: memb_def sub_list_def)
+
+lemma eq_ffilter: 
+  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+  by (descending) (auto simp add: memb_def)
 
-lemma singleton_union_left:
-  shows "{|a|} |\<union>| S = finsert a S"
-  by simp
+lemma subset_ffilter:
+  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
+
+
+subsection {* ffold *}
+
+lemma ffold_nil: 
+  shows "ffold f z {||} = z"
+  by (descending) (simp)
+
+lemma ffold_finsert: "ffold f z (finsert a A) =
+  (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
+  by (descending) (simp add: memb_def)
 
-lemma singleton_union_right:
-  shows "S |\<union>| {|a|} = finsert a S"
-  by (subst sup.commute) simp
+lemma fin_commute_ffold:
+  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
+  by (descending) (simp add: memb_def memb_commute_ffold_raw)
+
+
+subsection {* Choice in fsets *}
+
+lemma fset_choice: 
+  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
+  shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+  using a
+  apply(descending)
+  using finite_set_choice
+  by (auto simp add: memb_def Ball_def)
+
+
+(* FIXME: is that in any way useful *)  
+
 
 
 section {* Induction and Cases rules for fsets *}
@@ -917,160 +1150,6 @@
 qed
 
 
-section {* fmap *}
-
-lemma fmap_simps[simp]:
-  fixes f::"'a \<Rightarrow> 'b"
-  shows "fmap f {||} = {||}"
-  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
-  by (lifting map.simps)
-
-lemma fmap_set_image:
-  "fset (fmap f S) = f ` (fset S)"
-  by (induct S) simp_all
-
-lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
-  by (lifting inj_map_eq_iff)
-
-lemma fmap_funion: 
-  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
-  by (descending) (simp)
-
-lemma fin_funion:
-  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
-  by (descending) (simp add: memb_def)
-
-section {* fset *}
-
-lemma fin_set: 
-  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
-  by (lifting memb_def)
-
-lemma fnotin_set: 
-  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
-  by (simp add: fin_set)
-
-lemma fcard_set: 
-  shows "fcard xs = card (fset xs)"
-  by (lifting fcard_raw_def)
-
-lemma fsubseteq_set: 
-  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
-  by (lifting sub_list_def)
-
-lemma fsubset_set: 
-  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
-  unfolding less_fset_def 
-  by (descending) (auto simp add: sub_list_def)
-
-lemma ffilter_set [simp]: 
-  shows "fset (ffilter P xs) = P \<inter> fset xs"
-  by (descending) (auto simp add: mem_def)
-
-lemma fdelete_set [simp]: 
-  shows "fset (fdelete x xs) = fset xs - {x}"
-  by (lifting set_removeAll)
-
-lemma finter_set [simp]: 
-  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
-  by (lifting set_finter_raw)
-
-lemma funion_set [simp]: 
-  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
-  by (lifting set_append)
-
-lemma fminus_set [simp]: 
-  shows "fset (xs - ys) = fset xs - fset ys"
-  by (lifting set_fminus_raw)
-
-
-
-section {* ffold *}
-
-lemma ffold_nil: 
-  shows "ffold f z {||} = z"
-  by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
-
-lemma ffold_finsert: "ffold f z (finsert a A) =
-  (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
-  by (descending) (simp add: memb_def)
-
-lemma fin_commute_ffold:
-  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
-  by (descending) (simp add: memb_def memb_commute_ffold_raw)
-
-
-
-section {* fdelete *}
-
-lemma fin_fdelete:
-  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
-  by (descending) (simp add: memb_def)
-
-lemma fnotin_fdelete:
-  shows "x |\<notin>| fdelete x S"
-  by (descending) (simp add: memb_def)
-
-lemma fnotin_fdelete_ident:
-  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
-  by (descending) (simp add: memb_def)
-
-lemma fset_fdelete_cases:
-  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
-  by (lifting fset_raw_removeAll_cases)
-
-
-section {* finter *}
-
-lemma finter_empty_l:
-  shows "{||} |\<inter>| S = {||}"
-  by simp
-
-lemma finter_empty_r:
-  shows "S |\<inter>| {||} = {||}"
-  by simp
-
-lemma finter_finsert:
-  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
-  by (descending) (simp add: memb_def)
-
-lemma fin_finter:
-  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
-  by (descending) (simp add: memb_def)
-
-lemma fsubset_finsert:
-  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
-  by (lifting sub_list_cons)
-
-lemma 
-  shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
-  by (descending) (auto simp add: sub_list_def memb_def)
-
-lemma fsubset_fin: 
-  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
-  by (descending) (auto simp add: sub_list_def memb_def)
-
-lemma fminus_fin: 
-  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
-  by (descending) (simp add: memb_def)
-
-lemma fminus_red: 
-  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
-  by (descending) (auto simp add: memb_def)
-
-lemma fminus_red_fin[simp]: 
-  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
-  by (simp add: fminus_red)
-
-lemma fminus_red_fnotin[simp]: 
-  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
-  by (simp add: fminus_red)
-
-lemma fset_eq_iff:
-  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
-  by (descending) (auto simp add: memb_def)
-
 (* We cannot write it as "assumes .. shows" since Isabelle changes
    the quantifiers to schematic variables and reintroduces them in
    a different order *)
@@ -1097,143 +1176,12 @@
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
 
-section {* fconcat *}
-
-lemma fconcat_empty:
-  shows "fconcat {||} = {||}"
-  by (lifting concat.simps(1))
-
-lemma fconcat_insert:
-  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-  by (lifting concat.simps(2))
-
-lemma 
-  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
-  by (lifting concat_append)
-
-
-section {* ffilter *}
-
-lemma subseteq_filter: 
-  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-  by  (descending) (auto simp add: memb_def sub_list_def)
-
-lemma eq_ffilter: 
-  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-  by (descending) (auto simp add: memb_def)
-
-lemma subset_ffilter:
-  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
-  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
-
 
 section {* lemmas transferred from Finite_Set theory *}
 
 text {* finiteness for finite sets holds *}
-lemma finite_fset [simp]: 
-  shows "finite (fset S)"
-  by (induct S) auto
-
-lemma fset_choice: 
-  shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
-  apply(descending)
-  apply(simp add: memb_def)
-  apply(rule finite_set_choice[simplified Ball_def])
-  apply(simp_all)
-  done
-
-lemma fsubseteq_fempty:
-  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
-  by (metis finter_empty_r le_iff_inf)
-
-lemma not_fsubset_fnil: 
-  shows "\<not> xs |\<subset>| {||}"
-  by (metis fset_simps(1) fsubset_set not_psubset_empty)
-  
-lemma fcard_mono: 
-  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
-  unfolding fcard_set fsubseteq_set
-  by (rule card_mono[OF finite_fset])
-
-lemma fcard_fseteq: 
-  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
-  unfolding fcard_set fsubseteq_set
-  by (simp add: card_seteq[OF finite_fset] fset_cong)
-
-lemma psubset_fcard_mono: 
-  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
-  unfolding fcard_set fsubset_set
-  by (rule psubset_card_mono[OF finite_fset])
-
-lemma fcard_funion_finter: 
-  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
-  unfolding fcard_set funion_set finter_set
-  by (rule card_Un_Int[OF finite_fset finite_fset])
-
-lemma fcard_funion_disjoint: 
-  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
-  unfolding fcard_set funion_set 
-  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
-  by (metis finter_set fset_simps(1))
-
-lemma fcard_delete1_less: 
-  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
-  unfolding fcard_set fin_set fdelete_set 
-  by (rule card_Diff1_less[OF finite_fset])
 
-lemma fcard_delete2_less: 
-  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
-  unfolding fcard_set fdelete_set fin_set
-  by (rule card_Diff2_less[OF finite_fset])
 
-lemma fcard_delete1_le: 
-  shows "fcard (fdelete x xs) \<le> fcard xs"
-  unfolding fdelete_set fcard_set
-  by (rule card_Diff1_le[OF finite_fset])
-
-lemma fcard_psubset: 
-  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
-  unfolding fcard_set fsubseteq_set fsubset_set
-  by (rule card_psubset[OF finite_fset])
-
-lemma fcard_fmap_le: 
-  shows "fcard (fmap f xs) \<le> fcard xs"
-  unfolding fcard_set  fmap_set_image
-  by (rule card_image_le[OF finite_fset])
-
-lemma fin_fminus_fnotin: 
-  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
-  unfolding fin_set fminus_set
-  by blast
-
-lemma fin_fnotin_fminus: 
-  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
-  unfolding fin_set fminus_set
-  by blast
-
-lemma fin_mdef:
-  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
-  unfolding fin_set fset_simps fset_cong fminus_set
-  by blast
-
-lemma fcard_fminus_finsert[simp]:
-  assumes "a |\<in>| A" and "a |\<notin>| B"
-  shows "fcard (A - finsert a B) = fcard (A - B) - 1"
-  using assms 
-  unfolding fin_set fcard_set fminus_set
-  by (simp add: card_Diff_insert[OF finite_fset])
-
-lemma fcard_fminus_fsubset:
-  assumes "B |\<subseteq>| A"
-  shows "fcard (A - B) = fcard A - fcard B"
-  using assms 
-  unfolding fsubseteq_set fcard_set fminus_set
-  by (rule card_Diff_subset[OF finite_fset])
-
-lemma fcard_fminus_subset_finter:
-  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
-  unfolding finter_set fcard_set fminus_set
-  by (rule card_Diff_subset_Int) (simp)
 
 
 lemma list_all2_refl: