# HG changeset patch
# User wenzelm
# Date 1305403224 -7200
# Node ID c5146d5fc54c15df4cc4a256024b9d82edc5e3bc
# Parent  5b45125b15bad5edaf02d456cf19e60d8613606d# Parent  2425068fe13ac9808ad2f1211b757c36b1e5ca55
merged

diff -r 2425068fe13a -r c5146d5fc54c NEWS
--- a/NEWS	Sat May 14 21:42:17 2011 +0200
+++ b/NEWS	Sat May 14 22:00:24 2011 +0200
@@ -58,6 +58,9 @@
 
 *** HOL ***
 
+* Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
+interpretation proofs may need adjustment.  INCOMPATIBILITY.
+
 * Nitpick:
   - Added "need" and "total_consts" options.
   - Reintroduced "show_skolems" option by popular demand.
diff -r 2425068fe13a -r c5146d5fc54c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat May 14 21:42:17 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Sat May 14 22:00:24 2011 +0200
@@ -534,13 +534,11 @@
 
 locale fun_left_comm =
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
-  assumes fun_left_comm: "f x (f y z) = f y (f x z)"
+  assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
 begin
 
-text{* On a functional level it looks much nicer: *}
-
-lemma commute_comp: "f y \<circ> f x = f x \<circ> f y"
-by (simp add: fun_left_comm fun_eq_iff)
+lemma fun_left_comm: "f x (f y z) = f y (f x z)"
+  using commute_comp by (simp add: fun_eq_iff)
 
 end
 
@@ -706,7 +704,7 @@
 lemma (in fun_left_comm) fun_left_comm_apply:
   "fun_left_comm (\<lambda>x. f (g x))"
 proof
-qed (simp_all add: fun_left_comm)
+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))"
@@ -830,9 +828,9 @@
 assumes "finite A" and "a \<notin> A"
 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
 proof -
-  interpret I: fun_left_comm "%x y. (g x) * y"
-    by unfold_locales (simp add: mult_ac)
-  show ?thesis using assms by(simp add:fold_image_def)
+  interpret I: fun_left_comm "%x y. (g x) * y" proof
+  qed (simp add: fun_eq_iff mult_ac)
+  show ?thesis using assms by (simp add: fold_image_def)
 qed
 
 (*
@@ -1053,8 +1051,8 @@
 context ab_semigroup_mult
 begin
 
-lemma fun_left_comm: "fun_left_comm(op *)"
-by unfold_locales (simp add: mult_ac)
+lemma fun_left_comm: "fun_left_comm (op *)" proof
+qed (simp add: fun_eq_iff mult_ac)
 
 lemma fold_graph_insert_swap:
 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
@@ -1139,11 +1137,8 @@
 context ab_semigroup_idem_mult
 begin
 
-lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
-apply unfold_locales
- apply (rule mult_left_commute)
-apply (rule mult_left_idem)
-done
+lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
+qed (simp add: fun_eq_iff mult_left_commute, rule mult_left_idem)
 
 lemma fold1_insert_idem [simp]:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
@@ -1465,7 +1460,7 @@
   shows "F (insert x A) = g x * F A"
 proof -
   interpret fun_left_comm "%x y. (g x) * y" proof
-  qed (simp add: ac_simps)
+  qed (simp add: ac_simps fun_eq_iff)
   with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
     by (simp add: fold_image_def)
   with `finite A` show ?thesis by (simp add: eq_fold_g)
diff -r 2425068fe13a -r c5146d5fc54c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat May 14 21:42:17 2011 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat May 14 22:00:24 2011 +0200
@@ -1599,7 +1599,7 @@
   "image_mset f = fold_mset (op + o single o f) {#}"
 
 interpretation image_left_comm: fun_left_comm "op + o single o f"
-proof qed (simp add: add_ac)
+proof qed (simp add: add_ac fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)
diff -r 2425068fe13a -r c5146d5fc54c src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 14 21:42:17 2011 +0200
+++ b/src/HOL/List.thy	Sat May 14 22:00:24 2011 +0200
@@ -3765,7 +3765,7 @@
 lemma fun_left_comm_insort:
   "fun_left_comm insort"
 proof
-qed (fact insort_left_comm)
+qed (simp add: insort_left_comm fun_eq_iff)
 
 lemma sort_key_simps [simp]:
   "sort_key f [] = []"