--- a/Nominal/FSet.thy	Fri Oct 15 13:28:39 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 14:11:23 2010 +0100
@@ -2,14 +2,14 @@
     Author:     Cezary Kaliszyk, TU Munich
     Author:     Christian Urban, TU Munich
 
-A reasoning infrastructure for the type of finite sets.
+    Type of finite sets.
 *)
 
 theory FSet
 imports Quotient_List
 begin
 
-text {* Definiton of List relation and the quotient type *}
+text {* Definiton of the list equivalence relation *}
 
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
@@ -22,12 +22,15 @@
   unfolding reflp_def symp_def transp_def
   by auto
 
+text {* Fset type *}
+
 quotient_type
   'a fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-text {* Raw definitions of membership, sublist, cardinality,
-  intersection
+text {* 
+  Definitions of membership, sublist, cardinality,
+  intersection etc over lists
 *}
 
 definition
@@ -45,6 +48,13 @@
 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
@@ -73,7 +83,19 @@
        else f a (ffold_raw f z xs)
      else z)"
 
-text {* Composition Quotient *}
+
+
+lemma set_finter_raw[simp]:
+  shows "set (finter_raw xs ys) = set xs \<inter> set ys"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma set_fminus_raw[simp]: 
+  shows "set (fminus_raw xs ys) = (set xs - set ys)"
+  by (induct ys arbitrary: xs) (auto)
+
+
+
+section {* Quotient composition lemmas *}
 
 lemma list_all2_refl1:
   shows "(list_all2 op \<approx>) r r"
@@ -151,20 +173,11 @@
 qed
 
 
-lemma set_finter_raw[simp]:
-  "set (finter_raw xs ys) = set xs \<inter> set ys"
-  by (induct xs) (auto simp add: memb_def)
-
-lemma set_fminus_raw[simp]: 
-  "set (fminus_raw xs ys) = (set xs - set ys)"
-  by (induct ys arbitrary: xs) (auto)
-
-
 text {* Respectfulness *}
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
-  by (simp)
+  by simp
 
 lemma sub_list_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
@@ -212,23 +225,6 @@
 
 
 
-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_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 memb_commute_ffold_raw:
   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
   apply (induct b)
@@ -302,13 +298,6 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   by auto
 
-text {* Distributive lattice with bot *}
-
-lemma append_inter_distrib:
-  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
-  apply (induct x)
-  apply (auto)
-  done
 
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
@@ -366,6 +355,12 @@
 is
   "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
+lemma append_finter_raw_distrib:
+  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+  apply (induct x)
+  apply (auto)
+  done
+
 instance
 proof
   fix x y z :: "'a fset"
@@ -381,7 +376,7 @@
   show "x |\<inter>| y |\<subseteq>| y" 
     by (descending) (simp add: sub_list_def memb_def[symmetric])
   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
-    by (descending) (rule append_inter_distrib)
+    by (descending) (rule append_finter_raw_distrib)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
@@ -595,23 +590,14 @@
   shows "\<not>(fcard_raw A = 0)"
 proof -
   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
-  then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
+  then have "\<not>A \<approx> []" by (simp add: memb_def)
   then show ?thesis using fcard_raw_0[of A] by simp
 qed
 
 
 
-section {* fmap *}
-
-(* there is another fmap section below *)
+section {* ? *}
 
-lemma map_append:
-  "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
-  by simp
-
-lemma memb_append:
-  "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
-  by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
 lemma fset_raw_strong_cases:
   obtains "xs = []"
@@ -687,7 +673,7 @@
   apply (induct A)
   apply (simp add: memb_def list_eq2_refl)
   apply (case_tac "memb a (aa # A)")
-  apply (simp_all only: memb_cons_iff)
+  apply (simp_all only: memb_def)
   apply (case_tac [!] "a = aa")
   apply (simp_all)
   apply (case_tac "memb a A")
@@ -785,16 +771,16 @@
 
 lemma fset_simps[simp]:
   "fset {||} = ({} :: 'a set)"
-  "fset (finsert (h :: 'a) t) = insert h (fset t)"
+  "fset (finsert (x :: 'a) S) = insert x (fset S)"
   by (lifting set.simps)
 
-lemma in_fset:
-  "x \<in> fset S \<equiv> x |\<in>| S"
+lemma fin_fset:
+  "x \<in> fset S \<longleftrightarrow> x |\<in>| S"
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
   "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
-  by (lifting none_memb_nil)
+  by (descending) (simp add: memb_def)
 
 lemma fset_cong:
   "S = T \<longleftrightarrow> fset S = fset T"
@@ -949,12 +935,11 @@
 
 lemma fmap_funion: 
   shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
-  by (lifting map_append)
+  by (descending) (simp)
 
 lemma fin_funion:
   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
-  by (lifting memb_append)
-
+  by (descending) (simp add: memb_def)
 
 section {* fset *}