--- a/src/HOL/Finite_Set.ML Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/Finite_Set.ML Thu Jan 10 01:10:58 2002 +0100
@@ -97,18 +97,18 @@
val finite_subset = thm "finite_subset";
val finite_subset_induct = thm "finite_subset_induct";
val finite_trancl = thm "finite_trancl";
-val foldSet_determ = thm "foldSet_determ";
+val foldSet_determ = thm "LC.foldSet_determ";
val foldSet_imp_finite = thm "foldSet_imp_finite";
-val fold_Un_Int = thm "fold_Un_Int";
-val fold_Un_disjoint = thm "fold_Un_disjoint";
-val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
-val fold_commute = thm "fold_commute";
+val fold_Un_Int = thm "ACe.fold_Un_Int";
+val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
+val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
+val fold_commute = thm "LC.fold_commute";
val fold_def = thm "fold_def";
val fold_empty = thm "fold_empty";
-val fold_equality = thm "fold_equality";
-val fold_insert = thm "fold_insert";
-val fold_nest_Un_Int = thm "fold_nest_Un_Int";
-val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
+val fold_equality = thm "LC.fold_equality";
+val fold_insert = thm "LC.fold_insert";
+val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
+val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
val n_sub_lemma = thm "n_sub_lemma";
val n_subsets = thm "n_subsets";
val psubset_card_mono = thm "psubset_card_mono";
--- 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")
--- a/src/HOL/NumberTheory/IntFact.thy Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy Thu Jan 10 01:10:58 2002 +0100
@@ -40,7 +40,7 @@
lemma setprod_insert [simp]:
"finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
apply (unfold setprod_def)
- apply (simp add: zmult_left_commute fold_insert [standard])
+ apply (simp add: zmult_left_commute LC.fold_insert)
done