--- a/Nominal/FSet.thy	Tue Apr 13 07:40:54 2010 +0200
+++ b/Nominal/FSet.thy	Tue Apr 13 15:00:49 2010 +0200
@@ -70,6 +70,10 @@
   "\<not>x # xs \<approx> []"
   by auto
 
+lemma not_memb_nil:
+  "\<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)
@@ -139,12 +143,56 @@
   fixes xs :: "'a list"
   fixes n :: "nat"
   assumes c: "fcard_raw xs = Suc n"
-  shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys)"
+  shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys) \<and> fcard_raw ys = n"
+  unfolding memb_def
   using c
-  apply(induct xs)
+  proof (induct xs)
+    case Nil
+    then show ?case by simp
+  next
+    case (Cons a xs)
+    have f1: "fcard_raw xs = Suc n \<Longrightarrow> \<exists>a ys. a \<notin> set ys \<and> xs \<approx> a # ys \<and> fcard_raw ys = n" by fact
+    have f2: "fcard_raw (a # xs) = Suc n" by fact
+    then show ?case proof (cases "a \<in> set xs")
+      case True
+      then show ?thesis using f1 f2 apply -
+        apply (simp add: memb_def)
+        apply clarify
+        by metis
+      case False
+        then have ?thesis using f1 f2 apply -
+        apply (rule_tac x="a" in exI)
+        apply (rule_tac x="xs" in exI)
+        apply (simp add: memb_def)
+        done
+    qed
+  qed
+qed
+
+lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"
+  apply (induct a)
+  apply simp_all
+  apply auto
+  apply (subgoal_tac "set a2 = {b}")
   apply simp
-  apply (auto)
-  apply (metis memb_def)
+  apply (simp add: memb_def)
+  apply auto
+  apply (subgoal_tac "set a2 = {}")
+  apply simp
+  by (metis memb_def subset_empty subset_insert)
+
+lemma fcard_raw_1:
+  fixes a :: "'a list"
+  shows "(fcard_raw a = 1) = (\<exists>b. a \<approx> [b])"
+  apply auto
+  apply (drule fcard_raw_suc)
+  apply clarify
+  apply (simp add: fcard_raw_0)
+  apply (rule_tac x="aa" in exI)
+  apply simp
+  apply (subgoal_tac "set a = {b}")
+  apply (erule singleton_fcard_1)
+  apply auto
   done
 
 lemma fcard_raw_delete_one:
@@ -179,6 +227,10 @@
   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
   by simp
 
+lemma memb_append:
+  "memb e (append l r) = (memb e l \<or> memb e r)"
+  by (induct l) (simp_all add: not_memb_nil memb_cons_iff)
+
 text {* raw section *}
 
 lemma map_rsp_aux:
@@ -206,7 +258,7 @@
   "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
   by simp
 
-lemma finite_set_raw_strong_cases:
+lemma fset_raw_strong_cases:
   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
   apply (simp)
@@ -231,28 +283,35 @@
   "delete_raw [] x = []"
 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
-lemma mem_delete_raw:
-  "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
-  by (induct A arbitrary: x a) (auto)
+lemma memb_delete_raw:
+  "memb x (delete_raw A a) = (memb x A \<and> x \<noteq> a)"
+  by (induct A arbitrary: x a) (auto simp add: memb_def)
 
-lemma mem_delete_raw_ident:
-  "\<not>(a \<in> set (delete_raw A a))"
-  by (induct A) (auto)
+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:
+  "\<not> memb a (delete_raw A a)"
+  by (induct A) (auto simp add: memb_def)
 
-lemma not_mem_delete_raw_ident:
-  "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
-  by (induct A) (auto)
+lemma not_memb_delete_raw_ident:
+  "\<not> memb b A \<Longrightarrow> delete_raw A b = A"
+  by (induct A) (auto simp add: memb_def)
+
+lemma fset_raw_delete_raw_cases:
+  "X = [] \<or> (\<exists>a. memb a X \<and> X \<approx> a # delete_raw X a)"
+  by (induct X) (auto simp add: memb_def)
 
-lemma finite_set_raw_delete_raw_cases:
-  "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
-  by (induct X) (auto)
+lemma fdelete_raw_filter:
+  "delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
+  by (induct xs) simp_all
 
-lemma list2set_thm:
-  shows "set [] = {}"
-  and "set (h # t) = insert h (set t)"
-  by (auto)
+lemma fcard_raw_delete:
+  "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 list2set_rsp[quot_respect]:
+lemma set_rsp[quot_respect]:
   "(op \<approx> ===> op =) set set"
   by auto
 
@@ -262,15 +321,54 @@
   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
 primrec
-  fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 where
-  "fold_raw f z [] = z"
-| "fold_raw f z (a # A) =
+  "ffold_raw f z [] = z"
+| "ffold_raw f z (a # A) =
      (if (rsp_fold f) then
-       if a mem A then fold_raw f z A
-       else f a (fold_raw f z A)
+       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
+
+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 e (finter_raw l r) = (memb e l \<and> memb e r)"
+  apply (induct l)
+  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
@@ -281,6 +379,16 @@
   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
   is "set"
 
+quotient_definition
+  "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:
   "a @ b \<approx> b @ a"
   by auto
@@ -312,6 +420,8 @@
 
 section {* lifted part *}
 
+lemma not_fin_fnil: "x |\<notin>| {||}"
+  by (lifting not_memb_nil)
 
 lemma fin_finsert_iff[simp]:
   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
@@ -346,15 +456,15 @@
 text {* fset_to_set *}
 
 lemma fset_to_set_simps[simp]:
-  "fset_to_set {||} = {}"
-  "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"
-  by (lifting list2set_thm)
+  "fset_to_set {||} = ({} :: 'a set)"
+  "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
+  by (lifting set.simps)
 
 lemma in_fset_to_set:
   "x \<in> fset_to_set xs \<equiv> x |\<in>| xs"
   by (lifting memb_def[symmetric])
 
-lemma none_in_fempty:
+lemma none_fin_fempty:
   "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
   by (lifting none_mem_nil)
 
@@ -375,15 +485,22 @@
 lemma fcard_0: "(fcard a = 0) = (a = {||})"
   by (lifting fcard_raw_0)
 
+lemma fcard_1: "(fcard a = 1) = (\<exists>b. a = {|b|})"
+  by (lifting fcard_raw_1)
+
 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"
   by (lifting fcard_raw_gt_0)
 
-lemma fcard_not_memb: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
+lemma fcard_not_fin: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
   by (lifting fcard_raw_not_memb)
 
-lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys"
+lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys \<and> fcard ys = n"
   by (lifting fcard_raw_suc)
 
+lemma fcard_delete:
+  "fcard (fdelete xs y) = (if y |\<in>| xs then fcard xs - 1 else fcard xs)"
+  by (lifting fcard_raw_delete)
+
 text {* funion *}
 
 lemma funion_simps[simp]:
@@ -403,7 +520,7 @@
 
 lemma fset_strong_cases:
   "X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"
-  by (lifting finite_set_raw_strong_cases)
+  by (lifting fset_raw_strong_cases)
 
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
@@ -448,7 +565,8 @@
   apply simp_all
   done
 
-(* fmap *)
+text {* fmap *}
+
 lemma fmap_simps[simp]:
   "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
   "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
@@ -467,6 +585,54 @@
 lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"
   by (lifting map_append)
 
+lemma fin_funion:
+  "(e |\<in>| l |\<union>| r) = (e |\<in>| l \<or> e |\<in>| r)"
+  by (lifting memb_append)
+
+text {* ffold *}
+
+lemma ffold_nil: "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 (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])
+
+lemma fin_commute_ffold:
+  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
+  by (lifting memb_commute_ffold_raw)
+
+text {* fdelete *}
+
+lemma fin_fdelete: "(x |\<in>| fdelete A a) = (x |\<in>| A \<and> x \<noteq> a)"
+  by (lifting memb_delete_raw)
+
+lemma fin_fdelete_ident: "a |\<notin>| fdelete A a"
+  by (lifting memb_delete_raw_ident)
+
+lemma not_memb_fdelete_ident: "b |\<notin>| A \<Longrightarrow> fdelete A b = A"
+  by (lifting not_memb_delete_raw_ident)
+
+lemma fset_fdelete_cases:
+  "X = {||} \<or> (\<exists>a. a |\<in>| X \<and> X = finsert a (fdelete X a))"
+  by (lifting fset_raw_delete_raw_cases)
+
+text {* inter *}
+
+lemma finter_empty_l: "({||} |\<inter>| r) = {||}"
+  by (lifting finter_raw.simps(1))
+
+lemma finter_empty_r: "(l |\<inter>| {||}) = {||}"
+  by (lifting finter_raw_empty)
+
+lemma finter_finsert:
+  "(finsert h t |\<inter>| l) = (if h |\<in>| l then finsert h (t |\<inter>| l) else t |\<inter>| l)"
+  by (lifting finter_raw.simps(2))
+
+lemma fin_finter:
+  "(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"
+  by (lifting memb_finter_raw)
+
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);