diff -r 9568f9f31822 -r 72b777cc5479 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun May 09 12:38:59 2010 +0100
+++ b/Nominal/FSet.thy	Mon May 10 10:22:57 2010 +0200
@@ -1,11 +1,12 @@
-(*  Title:      Quotient.thy
-    Author:     Cezary Kaliszyk 
-    Author:     Christian Urban
+(*  Title:      HOL/Quotient_Examples/FSet.thy
+    Author:     Cezary Kaliszyk, TU Munich
+    Author:     Christian Urban, TU Munich
 
-    provides a reasoning infrastructure for the type of finite sets
+A reasoning infrastructure for the type of finite sets.
 *)
+
 theory FSet
-imports Quotient Quotient_List List
+imports Quotient_List
 begin
 
 text {* Definiton of List relation and the quotient type *}
@@ -50,11 +51,17 @@
 | "finter_raw (h # t) l =
      (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
-fun
+primrec
   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))"
+| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
+
+primrec
+  fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "fminus_raw l [] = l"
+| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t"
 
 definition
   rsp_fold
@@ -65,10 +72,10 @@
   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) =
+| "ffold_raw f z (a # xs) =
      (if (rsp_fold f) then
-       if memb a A then ffold_raw f z A
-       else f a (ffold_raw f z A)
+       if memb a xs then ffold_raw f z xs
+       else f a (ffold_raw f z xs)
      else z)"
 
 text {* Composition Quotient *}
@@ -80,16 +87,16 @@
 lemma compose_list_refl:
   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 proof
-  show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
-  have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
-  show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+  show "list_rel op \<approx> r r" by (rule list_rel_refl)
+  with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
 qed
 
 lemma Quotient_fset_list:
   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
   by (fact list_quotient[OF Quotient_fset])
 
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
   by (rule eq_reflection) auto
 
 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
@@ -117,7 +124,8 @@
     show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
   next
     assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
-    then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+    then have b: "map abs_fset r \<approx> map abs_fset s"
+    proof (elim pred_compE)
       fix b ba
       assume c: "list_rel op \<approx> r b"
       assume d: "b \<approx> ba"
@@ -208,6 +216,14 @@
   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
   by (simp add: memb_def[symmetric] memb_delete_raw)
 
+lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
+  by (induct ys arbitrary: xs)
+     (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+  by (simp add: memb_def[symmetric] fminus_raw_memb)
+
 lemma fcard_raw_gt_0:
   assumes a: "x \<in> set xs"
   shows "0 < fcard_raw xs"
@@ -221,20 +237,43 @@
   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
+  proof (induct xs arbitrary: ys)
+    case Nil
+    show ?case using Nil.prems by simp
+  next
+    case (Cons a xs)
+    have a: "a # xs \<approx> ys" by fact
+    have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
+    show ?case proof (cases "a \<in> set xs")
+      assume c: "a \<in> set xs"
+      have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
+      proof (intro allI iffI)
+        fix x
+        assume "x \<in> set xs"
+        then show "x \<in> set ys" using a by auto
+      next
+        fix x
+        assume d: "x \<in> set ys"
+        have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+        show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+      qed
+      then show ?thesis using b c by (simp add: memb_def)
+    next
+      assume c: "a \<notin> set xs"
+      have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
+      have "Suc (fcard_raw xs) = fcard_raw ys"
+      proof (cases "a \<in> set ys")
+        assume e: "a \<in> set ys"
+        have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+          by (auto simp add: fcard_raw_delete_one)
+        have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+        then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+      next
+        case False then show ?thesis using a c d by auto
+      qed
+      then show ?thesis using a c d by (simp add: memb_def)
+  qed
+qed
 
 lemma fcard_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
@@ -306,8 +345,8 @@
   obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
   have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
   then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
-  have j: "ya \<in> set y'" using b h by simp
-  have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+  have "ya \<in> set y'" using b h by simp
+  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
   then show ?thesis using f i by auto
 qed
 
@@ -334,6 +373,10 @@
   then show "concat a \<approx> concat b" by simp
 qed
 
+lemma [quot_respect]:
+  "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+  by auto
+
 text {* Distributive lattice with bot *}
 
 lemma sub_list_not_eq:
@@ -385,9 +428,10 @@
   apply (induct x)
   apply (simp_all add: memb_def)
   apply (simp add: memb_def[symmetric] memb_finter_raw)
-  by (auto simp add: memb_def)
+  apply (auto simp add: memb_def)
+  done
 
-instantiation fset :: (type) "{bot,distrib_lattice}"
+instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
 begin
 
 quotient_definition
@@ -423,12 +467,12 @@
   "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 abbreviation
-  funion  (infixl "|\<union>|" 65)
+  funion (infixl "|\<union>|" 65)
 where
   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 
 quotient_definition
-  "inf  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+  "inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 is
   "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
@@ -437,6 +481,11 @@
 where
   "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
 
+quotient_definition
+  "minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+  "fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
 instance
 proof
   fix x y z :: "'a fset"
@@ -496,10 +545,10 @@
 where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
-section {* Other constants on the Quotient Type *} 
+section {* Other constants on the Quotient Type *}
 
 quotient_definition
-  "fcard :: 'a fset \<Rightarrow> nat" 
+  "fcard :: 'a fset \<Rightarrow> nat"
 is
   "fcard_raw"
 
@@ -509,11 +558,11 @@
  "map"
 
 quotient_definition
-  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
+  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
   is "delete_raw"
 
 quotient_definition
-  "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
+  "fset_to_set :: 'a fset \<Rightarrow> 'a set"
   is "set"
 
 quotient_definition
@@ -525,6 +574,11 @@
 is
   "concat"
 
+quotient_definition
+  "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "filter"
+
 text {* Compositional Respectfullness and Preservation *}
 
 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
@@ -636,6 +690,10 @@
   "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 memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
+  by (induct ys arbitrary: xs x)
+     (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+
 text {* Cardinality of finite sets *}
 
 lemma fcard_raw_0:
@@ -701,23 +759,37 @@
   by auto
 
 lemma fset_raw_strong_cases:
-  "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
-  apply (induct xs)
-  apply (simp)
-  apply (rule disjI2)
-  apply (erule disjE)
-  apply (rule_tac x="a" in exI)
-  apply (rule_tac x="[]" in exI)
-  apply (simp add: memb_def)
-  apply (erule exE)+
-  apply (case_tac "x = a")
-  apply (rule_tac x="a" in exI)
-  apply (rule_tac x="ys" in exI)
-  apply (simp)
-  apply (rule_tac x="x" in exI)
-  apply (rule_tac x="a # ys" in exI)
-  apply (auto simp add: memb_def)
-  done
+  obtains "xs = []"
+    | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+proof (induct xs arbitrary: x ys)
+  case Nil
+  then show thesis by simp
+next
+  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 "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+  proof -
+    fix x :: 'a
+    fix ys :: "'a list"
+    assume d:"\<not> memb x ys"
+    assume e:"xs \<approx> x # ys"
+    show thesis
+    proof (cases "x = a")
+      assume h: "x = a"
+      then have f: "\<not> memb a ys" using d by simp
+      have g: "a # xs \<approx> a # ys" using e h by auto
+      show thesis using b f g by simp
+    next
+      assume h: "x \<noteq> a"
+      then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+      show thesis using b f g by simp
+    qed
+  qed
+  then show thesis using a c by blast
+qed
 
 section {* deletion *}
 
@@ -741,8 +813,8 @@
   "finter_raw l [] = []"
   by (induct l) (simp_all add: not_memb_nil)
 
-lemma set_cong: 
-  shows "(set x = set y) = (x \<approx> y)"
+lemma set_cong:
+  shows "(x \<approx> y) = (set x = set y)"
   by auto
 
 lemma inj_map_eq_iff:
@@ -812,13 +884,13 @@
       case (Suc m)
       have b: "l \<approx> r" by fact
       have d: "fcard_raw l = Suc m" by fact
-      have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+      then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
       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 by auto
       have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
       have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
-      have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
-      have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+      have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+      then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
       have i: "list_eq2 l (a # delete_raw l a)"
         by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
       have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
@@ -828,6 +900,42 @@
   then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
+text {* Set *}
+
+lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+  by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+
+lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+  by (auto simp add: sub_list_set)
+
+lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+
+lemma memb_set: "memb x xs = (x \<in> set xs)"
+  by (simp only: memb_def)
+
+lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+  by (induct xs, simp)
+     (metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+
+lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+  by (induct xs) auto
+
+lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+  by (induct xs) (simp_all add: memb_def)
+
+lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
+  by (induct ys arbitrary: xs)
+     (simp_all add: fminus_raw.simps delete_raw_set, blast)
+
+text {* Raw theorems of ffilter *}
+
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
+
 text {* Lifted theorems *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -879,7 +987,7 @@
   by (lifting none_memb_nil)
 
 lemma fset_cong:
-  "(fset_to_set S = fset_to_set T) = (S = T)"
+  "(S = T) = (fset_to_set S = fset_to_set T)"
   by (lifting set_cong)
 
 text {* fcard *}
@@ -899,11 +1007,11 @@
   shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
   by (lifting fcard_raw_1)
 
-lemma fcard_gt_0: 
+lemma fcard_gt_0:
   shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
   by (lifting fcard_raw_gt_0)
 
-lemma fcard_not_fin: 
+lemma fcard_not_fin:
   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
   by (lifting fcard_raw_not_memb)
 
@@ -922,14 +1030,13 @@
 
 text {* funion *}
 
-lemma funion_simps[simp]:
-  shows "{||} |\<union>| S = S"
-  and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
-  by (lifting append.simps)
+lemmas [simp] =
+  sup_bot_left[where 'a="'a fset", standard]
+  sup_bot_right[where 'a="'a fset", standard]
 
-lemma funion_empty[simp]:
-  shows "S |\<union>| {||} = S"
-  by (lifting append_Nil2)
+lemma funion_finsert[simp]:
+  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+  by (lifting append.simps(2))
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
@@ -942,7 +1049,8 @@
 section {* Induction and Cases rules for finite sets *}
 
 lemma fset_strong_cases:
-  "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
+  obtains "xs = {||}"
+    | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
   by (lifting fset_raw_strong_cases)
 
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
@@ -954,7 +1062,7 @@
   by (lifting list.induct)
 
 lemma fset_induct[case_names fempty finsert, induct type: fset]:
-  assumes prem1: "P {||}" 
+  assumes prem1: "P {||}"
   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
   shows "P S"
 proof(induct S rule: fset_induct_weak)
@@ -980,6 +1088,20 @@
   apply simp_all
   done
 
+lemma fset_fcard_induct:
+  assumes a: "P {||}"
+  and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
+  shows "P zs"
+proof (induct zs)
+  show "P {||}" by (rule a)
+next
+  fix x :: 'a and zs :: "'a fset"
+  assume h: "P zs"
+  assume "x |\<notin>| zs"
+  then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
+  then show "P (finsert x zs)" using b h by simp
+qed
+
 text {* fmap *}
 
 lemma fmap_simps[simp]:
@@ -989,7 +1111,7 @@
 
 lemma fmap_set_image:
   "fset_to_set (fmap f S) = f ` (fset_to_set S)"
-  by (induct S) (simp_all)
+  by (induct S) simp_all
 
 lemma inj_fmap_eq_iff:
   "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
@@ -1002,6 +1124,44 @@
   "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
 
+text {* to_set *}
+
+lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+  by (lifting memb_set)
+
+lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+  by (simp add: fin_set)
+
+lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+  by (lifting fcard_raw_set)
+
+lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+  by (lifting sub_list_set)
+
+lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+  unfolding less_fset by (lifting sub_list_neq_set)
+
+lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+  by (lifting filter_set)
+
+lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+  by (lifting delete_raw_set)
+
+lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+  by (lifting inter_raw_set)
+
+lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+  by (lifting set_append)
+
+lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+  by (lifting fminus_raw_set)
+
+lemmas fset_to_set_trans =
+  fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+  inter_set union_set ffilter_set fset_to_set_simps
+  fset_cong fdelete_set fmap_set_image fminus_set
+
+
 text {* ffold *}
 
 lemma ffold_nil: "ffold f z {||} = z"
@@ -1017,15 +1177,15 @@
 
 text {* fdelete *}
 
-lemma fin_fdelete: 
+lemma fin_fdelete:
   shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
   by (lifting memb_delete_raw)
 
-lemma fin_fdelete_ident: 
+lemma fin_fdelete_ident:
   shows "x |\<notin>| fdelete S x"
   by (lifting memb_delete_raw_ident)
 
-lemma not_memb_fdelete_ident: 
+lemma not_memb_fdelete_ident:
   shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
   by (lifting not_memb_delete_raw_ident)
 
@@ -1060,6 +1220,18 @@
 by (rule meta_eq_to_obj_eq)
    (lifting sub_list_def[simplified memb_def[symmetric]])
 
+lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+  by (lifting fminus_raw_memb)
+
+lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+  by (lifting fminus_raw_red)
+
+lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+  by (simp add: fminus_red)
+
+lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+  by (simp add: fminus_red)
+
 lemma expand_fset_eq:
   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])
@@ -1102,8 +1274,107 @@
 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
   by (lifting concat_append)
 
+text {* ffilter *}
+
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+
+lemma subset_ffilter: "(\<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 by (auto simp add: subseteq_filter eq_ffilter)
+
+section {* lemmas transferred from Finite_Set theory *}
+
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+  by (induct S) auto
+
+lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+  unfolding fset_to_set_trans
+  by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+  unfolding fset_to_set_trans
+  by (rule subset_empty)
+
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+  unfolding fset_to_set_trans
+  by (rule not_psubset_empty)
+
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+  unfolding fset_to_set_trans
+  by (rule card_mono[OF finite_fset])
+
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+  unfolding fset_to_set_trans
+  by (rule card_seteq[OF finite_fset])
+
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+  unfolding fset_to_set_trans
+  by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+  unfolding fset_to_set_trans
+  by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+  unfolding fset_to_set_trans
+  by (rule card_Un_disjoint[OF finite_fset finite_fset])
+
+lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff1_less[OF finite_fset])
+
+lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+  unfolding fset_to_set_trans
+  by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+  unfolding fset_to_set_trans
+  by (rule card_image_le[OF finite_fset])
+
+lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+  unfolding fset_to_set_trans
+  by blast
+
+lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+  unfolding fset_to_set_trans
+  by blast
+
+lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+  unfolding fset_to_set_trans
+  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 fset_to_set_trans
+  by (rule 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 fset_to_set_trans
+  by (rule card_Diff_subset[OF finite_fset])
+
+lemma fcard_fminus_subset_finter:
+  "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+  unfolding fset_to_set_trans
+  by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+
+
 ML {*
-fun dest_fsetT (Type ("FSet.fset", [T])) = T
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}