# HG changeset patch
# User haftmann
# Date 1291495980 -3600
# Node ID 069cd1c1f39b4dc474ba932ee4d4d679cc034b37
# Parent  3afec5adee3500b1939b0c378e69e756d69d2165
more intimate definition of fold_list / fold_once in terms of fold

diff -r 3afec5adee35 -r 069cd1c1f39b src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Sat Dec 04 21:26:33 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sat Dec 04 21:53:00 2010 +0100
@@ -83,23 +83,18 @@
   obtains "f u \<circ> f v = f v \<circ> f u"
   using assms by (simp add: rsp_fold_def)
 
-primrec
-  fold_list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
+definition
+  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
 where
-  "fold_list f [] = id"
-| "fold_list f (a # xs) =
-     (if rsp_fold f then
-       if a \<in> set xs then fold_list f xs
-       else f a \<circ> fold_list f xs
-     else id)"
+  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"
 
-lemma fold_list_default [simp]:
-  "\<not> rsp_fold f \<Longrightarrow> fold_list f xs = id"
-  by (cases xs) simp_all
+lemma fold_once_default [simp]:
+  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
+  by (simp add: fold_once_def)
 
-lemma fold_list_fold_remdups:
-  "rsp_fold f \<Longrightarrow> fold_list f xs = fold f (remdups xs)"
-  by (induct xs) (auto elim: rsp_foldE intro: fold_commute)
+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 *}
@@ -239,15 +234,23 @@
   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 xs = f x \<circ> fold_list f (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 fold_list_set_equiv:
+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_once_set_equiv:
   assumes "xs \<approx> ys"
-  shows "fold_list f xs = fold_list f ys"
+  shows "fold_once f xs = fold_once f ys"
 proof (cases "rsp_fold f")
   case False then show ?thesis by simp
 next
@@ -258,12 +261,12 @@
     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_list_fold_remdups)
+  with True show ?thesis by (simp add: fold_once_fold_remdups)
 qed
 
-lemma fold_list_rsp [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op =) fold_list fold_list"
-  unfolding fun_rel_def by (auto intro: fold_list_set_equiv) 
+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'"
@@ -451,7 +454,7 @@
 
 quotient_definition
   "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
-  is fold_list
+  is fold_once
 
 quotient_definition
   "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
@@ -931,15 +934,15 @@
 
 lemma fold_empty_fset: 
   "fold_fset f {||} = id"
-  by descending simp
+  by descending (simp add: fold_once_def)
 
 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 f a \<circ> fold_fset f A else id)"
-  by descending simp
+  (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:
-  "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = f h \<circ> fold_fset f (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 *}