# HG changeset patch
# User haftmann
# Date 1291534442 -3600
# Node ID 08939f7b62622f4caf3415d6d01fc0b79ef957f6
# Parent  9e54eb514a4618b49f13114615a1f570b24e377f# Parent  069cd1c1f39b4dc474ba932ee4d4d679cc034b37
merged

diff -r 9e54eb514a46 -r 08939f7b6262 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Sat Dec 04 21:26:55 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sun Dec 05 08:34:02 2010 +0100
@@ -74,16 +74,27 @@
 where
   "rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)"
 
-primrec
-  fold_list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+lemma rsp_foldI:
+  "(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f"
+  by (simp add: rsp_fold_def)
+
+lemma rsp_foldE:
+  assumes "rsp_fold f"
+  obtains "f u \<circ> f v = f v \<circ> f u"
+  using assms by (simp add: rsp_fold_def)
+
+definition
+  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
 where
-  "fold_list f z [] = z"
-| "fold_list f z (a # xs) =
-     (if (rsp_fold f) then
-       if a \<in> set xs then fold_list f z xs
-       else f a (fold_list f z xs)
-     else z)"
+  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"
 
+lemma fold_once_default [simp]:
+  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
+  by (simp add: fold_once_def)
+
+lemma fold_once_fold_remdups:
+  "rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)"
+  by (simp add: fold_once_def)
 
 
 section {* Quotient composition lemmas *}
@@ -223,36 +234,39 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   by (auto intro!: fun_relI)
 
-lemma member_commute_fold_list:
-  assumes a: "rsp_fold f"
-  and     b: "x \<in> set xs"
-  shows "fold_list f y xs = f x (fold_list f y (removeAll x xs))"
-  using a b by (induct xs) (auto simp add: rsp_fold_def fun_eq_iff)
+lemma remdups_removeAll: (*FIXME move*)
+  "remdups (removeAll x xs) = remove1 x (remdups xs)"
+  by (induct xs) auto
+
+lemma member_commute_fold_once:
+  assumes "rsp_fold f"
+    and "x \<in> set xs"
+  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
+proof -
+  from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x"
+    by (auto intro!: fold_remove1_split elim: rsp_foldE)
+  then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
+qed
 
-lemma fold_list_rsp_pre:
-  assumes a: "set xs = set ys"
-  shows "fold_list f z xs = fold_list f z ys"
-  using a
-  apply (induct xs arbitrary: ys)
-  apply (simp)
-  apply (simp (no_asm_use))
-  apply (rule conjI)
-  apply (rule_tac [!] impI)
-  apply (rule_tac [!] conjI)
-  apply (rule_tac [!] impI)
-  apply (metis insert_absorb)
-  apply (metis List.insert_def List.set.simps(2) List.set_insert fold_list.simps(2))
-  apply (metis Diff_insert_absorb insertI1 member_commute_fold_list set_removeAll)
-  apply(drule_tac x="removeAll a ys" in meta_spec)
-  apply(auto)
-  apply(drule meta_mp)
-  apply(blast)
-  by (metis List.set.simps(2) emptyE fold_list.simps(2) in_listsp_conv_set listsp.simps mem_def)
+lemma fold_once_set_equiv:
+  assumes "xs \<approx> ys"
+  shows "fold_once f xs = fold_once f ys"
+proof (cases "rsp_fold f")
+  case False then show ?thesis by simp
+next
+  case True
+  then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+    by (rule rsp_foldE)
+  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
+    by (simp add: set_eq_iff_multiset_of_remdups_eq)
+  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
+    by (rule fold_multiset_equiv)
+  with True show ?thesis by (simp add: fold_once_fold_remdups)
+qed
 
-lemma fold_list_rsp [quot_respect]:
-  shows "(op = ===> op = ===> op \<approx> ===> op =) fold_list fold_list"
-  unfolding fun_rel_def
-  by(auto intro: fold_list_rsp_pre)
+lemma fold_once_rsp [quot_respect]:
+  shows "(op = ===> op \<approx> ===> op =) fold_once fold_once"
+  unfolding fun_rel_def by (auto intro: fold_once_set_equiv) 
 
 lemma concat_rsp_pre:
   assumes a: "list_all2 op \<approx> x x'"
@@ -439,8 +453,8 @@
   is "set"
 
 quotient_definition
-  "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
-  is fold_list
+  "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
+  is fold_once
 
 quotient_definition
   "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
@@ -903,15 +917,15 @@
 subsection {* filter_fset *}
 
 lemma subset_filter_fset: 
-  shows "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-  by  (descending) (auto)
+  "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+  by descending auto
 
 lemma eq_filter_fset: 
-  shows "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-  by (descending) (auto)
+  "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+  by descending auto
 
 lemma psubset_filter_fset:
-  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> 
+  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> 
     filter_fset P xs |\<subset>| filter_fset Q xs"
   unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset)
 
@@ -919,16 +933,16 @@
 subsection {* fold_fset *}
 
 lemma fold_empty_fset: 
-  shows "fold_fset f z {||} = z"
-  by (descending) (simp)
+  "fold_fset f {||} = id"
+  by descending (simp add: fold_once_def)
 
-lemma fold_insert_fset: "fold_fset f z (insert_fset a A) =
-  (if rsp_fold f then if a |\<in>| A then fold_fset f z A else f a (fold_fset f z A) else z)"
-  by (descending) (simp)
+lemma fold_insert_fset: "fold_fset f (insert_fset a A) =
+  (if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
+  by descending (simp add: fold_once_fold_remdups)
 
 lemma in_commute_fold_fset:
-  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> fold_fset f z b = f h (fold_fset f z (remove_fset h b))"
-  by (descending) (simp add: member_commute_fold_list)
+  "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
+  by descending (simp add: member_commute_fold_once)
 
 
 subsection {* Choice in fsets *}