--- a/src/HOL/Algebra/Coset.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Jun 19 22:49:38 2009 +0200
@@ -934,8 +934,8 @@
lemma (in group_hom) FactGroup_hom:
"(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
-apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
-proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
+apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
+proof (intro ballI)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
and X': "X' \<in> carrier (G Mod kernel G H h)"
@@ -952,7 +952,7 @@
simp add: set_mult_def image_eq_UN
subsetD [OF Xsub] subsetD [OF X'sub])
thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
- by (simp add: all image_eq_UN FactGroup_nonempty X X')
+ by (simp add: all image_eq_UN FactGroup_nonempty X X')
qed
--- a/src/HOL/Algebra/FiniteProduct.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Jun 19 22:49:38 2009 +0200
@@ -508,7 +508,6 @@
apply force
apply (subst finprod_insert)
apply auto
- apply (force simp add: Pi_def)
apply (subst m_comm)
apply auto
done
--- a/src/HOL/Algebra/Group.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/Algebra/Group.thy Fri Jun 19 22:49:38 2009 +0200
@@ -544,7 +544,7 @@
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
apply (auto simp add: hom_def funcset_compose)
-apply (simp add: compose_def funcset_mem)
+apply (simp add: compose_def Pi_def)
done
constdefs
@@ -552,14 +552,14 @@
"G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
lemma iso_refl: "(%x. x) \<in> G \<cong> G"
-by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
lemma (in group) iso_sym:
"h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
apply (simp add: iso_def bij_betw_Inv)
apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
-apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
+apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
done
lemma (in group) iso_trans:
@@ -568,11 +568,11 @@
lemma DirProd_commute_iso:
shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
-by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
lemma DirProd_assoc_iso:
shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
-by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
text{*Basis for homomorphism proofs: we assume two groups @{term G} and
@@ -592,7 +592,7 @@
"x \<in> carrier G ==> h x \<in> carrier H"
proof -
assume "x \<in> carrier G"
- with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
+ with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
qed
lemma (in group_hom) one_closed [simp]:
--- a/src/HOL/Library/FuncSet.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Jun 19 22:49:38 2009 +0200
@@ -51,7 +51,7 @@
subsection{*Basic Properties of @{term Pi}*}
-lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
+lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
by (simp add: Pi_def)
lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
@@ -79,7 +79,10 @@
lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
by (simp add: Pi_def)
-
+(*
+lemma funcset_id [simp]: "(%x. x): A -> A"
+ by (simp add: Pi_def)
+*)
text{*Covariance of Pi-sets in their second argument*}
lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
by (simp add: Pi_def, blast)
--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy Fri Jun 19 22:49:38 2009 +0200
@@ -289,8 +289,6 @@
apply blast
apply (fastsimp)
apply (auto intro!: funcsetI finprod_closed)
- apply (subst finprod_insert)
- apply (auto intro!: funcsetI finprod_closed)
done
lemma (in comm_monoid) finprod_Union_disjoint:
@@ -304,11 +302,7 @@
lemma (in comm_monoid) finprod_one [rule_format]:
"finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
finprod G f A = \<one>"
- apply (induct set: finite)
- apply auto
- apply (subst finprod_insert)
- apply (auto intro!: funcsetI)
-done
+by (induct set: finite) auto
(* need better simplification rules for rings *)
--- a/src/HOL/NewNumberTheory/Residues.thy Fri Jun 19 21:08:07 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy Fri Jun 19 22:49:38 2009 +0200
@@ -186,17 +186,13 @@
lemma (in residues) prod_cong:
"finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
apply (induct set: finite)
- apply (auto simp add: one_cong)
- apply (subst finprod_insert)
- apply (auto intro!: funcsetI mult_cong)
+ apply (auto simp: one_cong mult_cong)
done
lemma (in residues) sum_cong:
"finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
apply (induct set: finite)
- apply (auto simp add: zero_cong)
- apply (subst finsum_insert)
- apply (auto intro!: funcsetI add_cong)
+ apply (auto simp: zero_cong add_cong)
done
lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>