1.1 --- a/NEWS	Sat May 14 00:32:16 2011 +0200
     1.2 +++ b/NEWS	Sat May 14 18:26:25 2011 +0200
     1.3 @@ -58,6 +58,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
     1.8 +interpretation proofs may need adjustment.  INCOMPATIBILITY.
     1.9 +
    1.10  * Nitpick:
    1.11    - Added "need" and "total_consts" options.
    1.12    - Reintroduced "show_skolems" option by popular demand.

     2.1 --- a/src/HOL/Finite_Set.thy	Sat May 14 00:32:16 2011 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sat May 14 18:26:25 2011 +0200
     2.3 @@ -534,13 +534,11 @@
     2.4  
     2.5  locale fun_left_comm =
     2.6    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
     2.7 -  assumes fun_left_comm: "f x (f y z) = f y (f x z)"
     2.8 +  assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
     2.9  begin
    2.10  
    2.11 -text{* On a functional level it looks much nicer: *}
    2.12 -
    2.13 -lemma commute_comp: "f y \<circ> f x = f x \<circ> f y"
    2.14 -by (simp add: fun_left_comm fun_eq_iff)
    2.15 +lemma fun_left_comm: "f x (f y z) = f y (f x z)"
    2.16 +  using commute_comp by (simp add: fun_eq_iff)
    2.17  
    2.18  end
    2.19  
    2.20 @@ -706,7 +704,7 @@
    2.21  lemma (in fun_left_comm) fun_left_comm_apply:
    2.22    "fun_left_comm (\<lambda>x. f (g x))"
    2.23  proof
    2.24 -qed (simp_all add: fun_left_comm)
    2.25 +qed (simp_all add: commute_comp)
    2.26  
    2.27  lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
    2.28    "fun_left_comm_idem (\<lambda>x. f (g x))"
    2.29 @@ -830,9 +828,9 @@
    2.30  assumes "finite A" and "a \<notin> A"
    2.31  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
    2.32  proof -
    2.33 -  interpret I: fun_left_comm "%x y. (g x) * y"
    2.34 -    by unfold_locales (simp add: mult_ac)
    2.35 -  show ?thesis using assms by(simp add:fold_image_def)
    2.36 +  interpret I: fun_left_comm "%x y. (g x) * y" proof
    2.37 +  qed (simp add: fun_eq_iff mult_ac)
    2.38 +  show ?thesis using assms by (simp add: fold_image_def)
    2.39  qed
    2.40  
    2.41  (*
    2.42 @@ -1053,8 +1051,8 @@
    2.43  context ab_semigroup_mult
    2.44  begin
    2.45  
    2.46 -lemma fun_left_comm: "fun_left_comm(op *)"
    2.47 -by unfold_locales (simp add: mult_ac)
    2.48 +lemma fun_left_comm: "fun_left_comm (op *)" proof
    2.49 +qed (simp add: fun_eq_iff mult_ac)
    2.50  
    2.51  lemma fold_graph_insert_swap:
    2.52  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
    2.53 @@ -1139,11 +1137,8 @@
    2.54  context ab_semigroup_idem_mult
    2.55  begin
    2.56  
    2.57 -lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
    2.58 -apply unfold_locales
    2.59 - apply (rule mult_left_commute)
    2.60 -apply (rule mult_left_idem)
    2.61 -done
    2.62 +lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
    2.63 +qed (simp add: fun_eq_iff mult_left_commute, rule mult_left_idem)
    2.64  
    2.65  lemma fold1_insert_idem [simp]:
    2.66    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
    2.67 @@ -1465,7 +1460,7 @@
    2.68    shows "F (insert x A) = g x * F A"
    2.69  proof -
    2.70    interpret fun_left_comm "%x y. (g x) * y" proof
    2.71 -  qed (simp add: ac_simps)
    2.72 +  qed (simp add: ac_simps fun_eq_iff)
    2.73    with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
    2.74      by (simp add: fold_image_def)
    2.75    with `finite A` show ?thesis by (simp add: eq_fold_g)

     3.1 --- a/src/HOL/Library/Multiset.thy	Sat May 14 00:32:16 2011 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Sat May 14 18:26:25 2011 +0200
     3.3 @@ -1599,7 +1599,7 @@
     3.4    "image_mset f = fold_mset (op + o single o f) {#}"
     3.5  
     3.6  interpretation image_left_comm: fun_left_comm "op + o single o f"
     3.7 -proof qed (simp add: add_ac)
     3.8 +proof qed (simp add: add_ac fun_eq_iff)
     3.9  
    3.10  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
    3.11  by (simp add: image_mset_def)

     4.1 --- a/src/HOL/List.thy	Sat May 14 00:32:16 2011 +0200
     4.2 +++ b/src/HOL/List.thy	Sat May 14 18:26:25 2011 +0200
     4.3 @@ -3765,7 +3765,7 @@
     4.4  lemma fun_left_comm_insort:
     4.5    "fun_left_comm insort"
     4.6  proof
     4.7 -qed (fact insort_left_comm)
     4.8 +qed (simp add: insort_left_comm fun_eq_iff)
     4.9  
    4.10  lemma sort_key_simps [simp]:
    4.11    "sort_key f [] = []"