# HG changeset patch
# User haftmann
# Date 1305872216 -7200
# Node ID 43b0f61f56d020a8e4115962deeb0b93602326a5
# Parent  1608daf27c1f189f532f7f95f698a170b3e2b63d
use point-free characterization for locale fun_left_comm_idem

diff -r 1608daf27c1f -r 43b0f61f56d0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri May 20 08:16:13 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Fri May 20 08:16:56 2011 +0200
@@ -672,12 +672,11 @@
 text{* A simplified version for idempotent functions: *}
 
 locale fun_left_comm_idem = fun_left_comm +
-  assumes fun_left_idem: "f x (f x z) = f x z"
+  assumes fun_comp_idem: "f x o f x = f x"
 begin
 
-text{* The nice version: *}
-lemma fun_comp_idem : "f x o f x = f x"
-by (simp add: fun_left_idem fun_eq_iff)
+lemma fun_left_idem: "f x (f x z) = f x z"
+  using fun_comp_idem by (simp add: fun_eq_iff)
 
 lemma fold_insert_idem:
   assumes fin: "finite A"
@@ -701,15 +700,15 @@
 
 subsubsection {* Expressing set operations via @{const fold} *}
 
-lemma (in fun_left_comm) fun_left_comm_apply:
-  "fun_left_comm (\<lambda>x. f (g x))"
+lemma (in fun_left_comm) comp_comp_fun_commute:
+  "fun_left_comm (f \<circ> g)"
 proof
 qed (simp_all add: commute_comp)
 
-lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
-  "fun_left_comm_idem (\<lambda>x. f (g x))"
-  by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
-    (simp_all add: fun_left_idem)
+lemma (in fun_left_comm_idem) comp_comp_fun_idem:
+  "fun_left_comm_idem (f \<circ> g)"
+  by (rule fun_left_comm_idem.intro, rule comp_comp_fun_commute, unfold_locales)
+    (simp_all add: fun_comp_idem)
 
 lemma fun_left_comm_idem_insert:
   "fun_left_comm_idem insert"
@@ -783,10 +782,11 @@
   shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
 proof (rule sym)
   interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
-  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?inf"
-  by (induct A arbitrary: B)
-    (simp_all add: INFI_def Inf_insert inf_left_commute)
+  interpret fun_left_comm_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
+  from `finite A` have "fold (inf \<circ> f) B A = ?inf"
+    by (induct A arbitrary: B)
+      (simp_all add: INFI_def Inf_insert inf_left_commute)
+  then show "?fold = ?inf" by (simp add: comp_def)
 qed
 
 lemma sup_SUPR_fold_sup:
@@ -794,10 +794,11 @@
   shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
 proof (rule sym)
   interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
-  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?sup"
-  by (induct A arbitrary: B)
-    (simp_all add: SUPR_def Sup_insert sup_left_commute)
+  interpret fun_left_comm_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
+  from `finite A` have "fold (sup \<circ> f) B A = ?sup"
+    by (induct A arbitrary: B)
+      (simp_all add: SUPR_def Sup_insert sup_left_commute)
+  then show "?fold = ?sup" by (simp add: comp_def)
 qed
 
 lemma INFI_fold_inf:
@@ -1138,7 +1139,7 @@
 begin
 
 lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
-qed (simp add: fun_eq_iff mult_left_commute, rule mult_left_idem)
+qed (simp_all add: fun_eq_iff mult_left_commute)
 
 lemma fold1_insert_idem [simp]:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
diff -r 1608daf27c1f -r 43b0f61f56d0 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:56 2011 +0200
@@ -1850,12 +1850,12 @@
 proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
   show ?thesis unfolding iterate_def if_P[OF True] * by auto
 next case False note x=this
-  note * = fun_left_comm.fun_left_comm_apply[OF fun_left_comm_monoidal[OF assms(1)]]
+  note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
   show ?thesis proof(cases "f x = neutral opp")
     case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
       unfolding True monoidal_simps[OF assms(1)] by auto
   next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
-      apply(subst fun_left_comm.fold_insert[OF * finite_support])
+      apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
       using `finite s` unfolding support_def using False x by auto qed qed 
 
 lemma iterate_some: