# HG changeset patch
# User haftmann
# Date 1291384018 -3600
# Node ID ecca598474ddced47b92174e18bfc8f434d12558
# Parent  d13bcb42e4795c865c520e238457ac0d2769f652
conventional point-free characterization of rsp_fold

diff -r d13bcb42e479 -r ecca598474dd src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Dec 03 14:39:15 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Dec 03 14:46:58 2010 +0100
@@ -70,9 +70,9 @@
   [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
 
 definition
-  rsp_fold
+  rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
 where
-  "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))"
+  "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"
@@ -227,7 +227,7 @@
   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)
+  using a b by (induct xs) (auto simp add: rsp_fold_def fun_eq_iff)
 
 lemma fold_list_rsp_pre:
   assumes a: "set xs = set ys"