--- a/NEWS Sat May 14 00:32:16 2011 +0200
+++ b/NEWS Sat May 14 18:26:25 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.
--- a/src/HOL/Finite_Set.thy Sat May 14 00:32:16 2011 +0200
+++ b/src/HOL/Finite_Set.thy Sat May 14 18:26:25 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)
--- a/src/HOL/Library/Multiset.thy Sat May 14 00:32:16 2011 +0200
+++ b/src/HOL/Library/Multiset.thy Sat May 14 18:26:25 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)
--- a/src/HOL/List.thy Sat May 14 00:32:16 2011 +0200
+++ b/src/HOL/List.thy Sat May 14 18:26:25 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 [] = []"