--- a/Nominal/FSet.thy	Fri Oct 15 16:01:03 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 17:37:44 2010 +0100
@@ -29,43 +29,29 @@
   by (rule list_eq_equivp)
 
 text {* 
-  Definitions of membership, sublist, cardinality,
-  intersection etc over lists
+  Definitions of membership, sublist, cardinality, intersection, 
+  difference and respectful fold over lists
 *}
 
 definition
-  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
-where
   "memb x xs \<equiv> x \<in> set xs"
 
 definition
-  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-where
   "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
 
 definition
-  card_list :: "'a list \<Rightarrow> nat"
-where
   "card_list xs = card (set xs)"
 
-primrec
-  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "finter_raw [] ys = []"
-| "finter_raw (x # xs) ys =
-    (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
-
+definition
+  "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
 
 definition
-  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
   "diff_list xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
 
-
 definition
   rsp_fold
 where
-  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
+  "rsp_fold f \<equiv> \<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"
@@ -78,16 +64,6 @@
      else z)"
 
 
-
-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_diff_list[simp]: 
-  shows "set (diff_list xs ys) = (set xs - set ys)"
-  by (auto simp add: diff_list_def)
-
-
 section {* Quotient composition lemmas *}
 
 lemma list_all2_refl1:
@@ -166,57 +142,59 @@
 qed
 
 
-text {* Respectfulness *}
+subsection {* Respectfulness lemmas for list operations *}
 
-lemma append_rsp[quot_respect]:
+lemma list_equiv_rsp [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+  by auto
+
+lemma append_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   by simp
 
-lemma sub_list_rsp[quot_respect]:
+lemma sub_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp add: sub_list_def)
 
-lemma memb_rsp[quot_respect]:
+lemma memb_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op =) memb memb"
   by (auto simp add: memb_def)
 
-lemma nil_rsp[quot_respect]:
+lemma nil_rsp [quot_respect]:
   shows "(op \<approx>) Nil Nil"
   by simp
 
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
   by simp
 
-lemma map_rsp[quot_respect]:
+lemma map_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
   by auto
 
-lemma set_rsp[quot_respect]:
+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 inter_list_rsp [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
+  by (simp add: inter_list_def)
 
-lemma finter_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-  by simp
-
-lemma removeAll_rsp[quot_respect]:
+lemma removeAll_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
   by simp
 
-lemma diff_list_rsp[quot_respect]:
+lemma diff_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-  by simp
+  by (simp add: diff_list_def)
 
-lemma card_list_rsp[quot_respect]:
+lemma card_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op =) card_list card_list"
   by (simp add: card_list_def)
 
-
+lemma filter_rsp [quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
+  by simp
 
 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))"
@@ -242,7 +220,7 @@
   apply(blast)
   by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
 
-lemma ffold_raw_rsp[quot_respect]:
+lemma ffold_raw_rsp [quot_respect]:
   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
   unfolding fun_rel_def
   by(auto intro: ffold_raw_rsp_pre)
@@ -262,7 +240,7 @@
   then show ?thesis using f i by auto
 qed
 
-lemma concat_rsp[quot_respect]:
+lemma concat_rsp [quot_respect]:
   shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 proof (rule fun_relI, elim pred_compE)
   fix a b ba bb
@@ -287,16 +265,15 @@
   then show "concat a \<approx> concat b" by auto
 qed
 
-lemma [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
-  by auto
 
+subsection {* Finite sets are a bounded, distributive lattice with minus *}
 
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 
 quotient_definition
-  "bot :: 'a fset" is "[] :: 'a list"
+  "bot :: 'a fset" 
+  is "Nil :: 'a list"
 
 abbreviation
   fempty  ("{||}")
@@ -304,9 +281,8 @@
   "{||} \<equiv> bot :: 'a fset"
 
 quotient_definition
-  "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
-is
-  "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+  "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
+  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
 
 abbreviation
   f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
@@ -325,8 +301,7 @@
 
 quotient_definition
   "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 abbreviation
   funion (infixl "|\<union>|" 65)
@@ -335,8 +310,7 @@
 
 quotient_definition
   "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 abbreviation
   finter (infixl "|\<inter>|" 65)
@@ -345,14 +319,8 @@
 
 quotient_definition
   "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  is "diff_list :: '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
@@ -365,11 +333,11 @@
   show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
   show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
   show "x |\<inter>| y |\<subseteq>| x"
-    by (descending) (simp add: sub_list_def memb_def[symmetric])
+    by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
   show "x |\<inter>| y |\<subseteq>| y" 
-    by (descending) (simp add: sub_list_def memb_def[symmetric])
+    by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
-    by (descending) (rule append_finter_raw_distrib)
+    by (descending) (auto simp add: inter_list_def)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
@@ -393,13 +361,13 @@
   assume a: "x |\<subseteq>| y"
   assume b: "x |\<subseteq>| z"
   show "x |\<subseteq>| y |\<inter>| z" using a b 
-    by (descending) (simp add: sub_list_def memb_def[symmetric])
+    by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
 qed
 
 end
 
 
-section {* Definitions for fsets *}
+section {* Quotient definitions for fsets *}
 
 
 quotient_definition
@@ -459,7 +427,7 @@
 lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
   by (fact compose_list_refl)
 
-lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+lemma  [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
   by simp
 
 lemma [quot_respect]:
@@ -748,7 +716,7 @@
 
 lemma finter_set [simp]: 
   shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
-  by (lifting set_finter_raw)
+  by (descending) (auto simp add: inter_list_def)
 
 lemma funion_set [simp]: 
   shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
@@ -756,7 +724,7 @@
 
 lemma fminus_set [simp]: 
   shows "fset (xs - ys) = fset xs - fset ys"
-  by (lifting set_diff_list)
+  by (descending) (auto simp add: diff_list_def)
 
 
 subsection {* funion *}
@@ -786,11 +754,11 @@
 
 lemma fminus_fin: 
   shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp add: diff_list_def 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)
+  by (descending) (auto simp add: diff_list_def memb_def)
 
 lemma fminus_red_fin[simp]: 
   shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
@@ -842,11 +810,11 @@
 
 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)
+  by (descending) (auto simp add: inter_list_def 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)
+  by (descending) (simp add: inter_list_def memb_def)
 
 
 subsection {* fsubset *}