--- a/src/HOL/Finite_Set.thy Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/Finite_Set.thy Thu Jan 10 01:10:58 2002 +0100
@@ -711,7 +711,7 @@
AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" "x \<cdot> y = y \<cdot> x" "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
by (rule assoc, rule commute, rule left_commute) (* FIXME localize "lemmas" (!??) *)
-lemma (in ACe [simp]) left_ident: "e \<cdot> x = x"
+lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
proof -
have "x \<cdot> e = x" by (rule ident)
thus ?thesis by (subst commute)
@@ -722,7 +722,7 @@
fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
apply (induct set: Finites)
apply simp
- apply (simp add: AC fold_insert insert_absorb Int_insert_left)
+ apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left)
done
lemma (in ACe) fold_Un_disjoint:
@@ -746,13 +746,13 @@
have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
by simp
also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
- by (rule fold_insert) (insert b insert, auto simp add: left_commute) (* FIXME import of fold_insert (!?) *)
+ by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute) (* FIXME import of fold_insert (!?) *)
also from insert have "fold (f \<circ> g) e (F \<union> B) =
fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
by (simp add: AC)
also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
- by (rule fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
+ by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
finally show ?case .
qed
qed
@@ -777,7 +777,7 @@
lemma setsum_insert [simp]:
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
- by (simp add: setsum_def fold_insert plus_ac0_left_commute)
+ by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute)
lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
apply (case_tac "finite A")