# HG changeset patch
# User nipkow
# Date 1245444552 -7200
# Node ID 2621a957d417c92da387e6f98caae1a16bfa6cf4
# Parent  caa89b41dcf267da5827495116c185e5d6222094
Made Pi_I [simp]

diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/Algebra/Coset.thy	Fri Jun 19 22:49:12 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
 
 
diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jun 19 22:49:12 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
diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri Jun 19 22:49:12 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]:
diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Jun 19 22:49:12 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)
diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/NewNumberTheory/MiscAlgebra.thy
--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 22:49:12 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 *)
diff -r caa89b41dcf2 -r 2621a957d417 src/HOL/NewNumberTheory/Residues.thy
--- a/src/HOL/NewNumberTheory/Residues.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy	Fri Jun 19 22:49:12 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>