Made Pi_I [simp]
authornipkow
Fri Jun 19 22:49:12 2009 +0200 (2009-06-19)
changeset 317272621a957d417
parent 31722 caa89b41dcf2
child 31728 60317e5211a2
Made Pi_I [simp]
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Library/FuncSet.thy
src/HOL/NewNumberTheory/MiscAlgebra.thy
src/HOL/NewNumberTheory/Residues.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Fri Jun 19 20:22:46 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Jun 19 22:49:12 2009 +0200
     1.3 @@ -934,8 +934,8 @@
     1.4  
     1.5  lemma (in group_hom) FactGroup_hom:
     1.6       "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
     1.7 -apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)  
     1.8 -proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
     1.9 +apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    1.10 +proof (intro ballI)
    1.11    fix X and X'
    1.12    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    1.13       and X': "X' \<in> carrier (G Mod kernel G H h)"
    1.14 @@ -952,7 +952,7 @@
    1.15               simp add: set_mult_def image_eq_UN 
    1.16                         subsetD [OF Xsub] subsetD [OF X'sub]) 
    1.17    thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
    1.18 -    by (simp add: all image_eq_UN FactGroup_nonempty X X')  
    1.19 +    by (simp add: all image_eq_UN FactGroup_nonempty X X')
    1.20  qed
    1.21  
    1.22  
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jun 19 20:22:46 2009 +0200
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jun 19 22:49:12 2009 +0200
     2.3 @@ -508,7 +508,6 @@
     2.4    apply force
     2.5    apply (subst finprod_insert)
     2.6    apply auto
     2.7 -  apply (force simp add: Pi_def)
     2.8    apply (subst m_comm)
     2.9    apply auto
    2.10  done
     3.1 --- a/src/HOL/Algebra/Group.thy	Fri Jun 19 20:22:46 2009 +0200
     3.2 +++ b/src/HOL/Algebra/Group.thy	Fri Jun 19 22:49:12 2009 +0200
     3.3 @@ -544,7 +544,7 @@
     3.4  lemma (in group) hom_compose:
     3.5       "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
     3.6  apply (auto simp add: hom_def funcset_compose) 
     3.7 -apply (simp add: compose_def funcset_mem)
     3.8 +apply (simp add: compose_def Pi_def)
     3.9  done
    3.10  
    3.11  constdefs
    3.12 @@ -552,14 +552,14 @@
    3.13    "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    3.14  
    3.15  lemma iso_refl: "(%x. x) \<in> G \<cong> G"
    3.16 -by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.17 +by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
    3.18  
    3.19  lemma (in group) iso_sym:
    3.20       "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
    3.21  apply (simp add: iso_def bij_betw_Inv) 
    3.22  apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    3.23   prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    3.24 -apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f) 
    3.25 +apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
    3.26  done
    3.27  
    3.28  lemma (in group) iso_trans: 
    3.29 @@ -568,11 +568,11 @@
    3.30  
    3.31  lemma DirProd_commute_iso:
    3.32    shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
    3.33 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.34 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
    3.35  
    3.36  lemma DirProd_assoc_iso:
    3.37    shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
    3.38 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    3.39 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
    3.40  
    3.41  
    3.42  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
    3.43 @@ -592,7 +592,7 @@
    3.44    "x \<in> carrier G ==> h x \<in> carrier H"
    3.45  proof -
    3.46    assume "x \<in> carrier G"
    3.47 -  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
    3.48 +  with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
    3.49  qed
    3.50  
    3.51  lemma (in group_hom) one_closed [simp]:
     4.1 --- a/src/HOL/Library/FuncSet.thy	Fri Jun 19 20:22:46 2009 +0200
     4.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Jun 19 22:49:12 2009 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4  
     4.5  subsection{*Basic Properties of @{term Pi}*}
     4.6  
     4.7 -lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
     4.8 +lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
     4.9    by (simp add: Pi_def)
    4.10  
    4.11  lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
    4.12 @@ -79,7 +79,10 @@
    4.13  
    4.14  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
    4.15    by (simp add: Pi_def)
    4.16 -
    4.17 +(*
    4.18 +lemma funcset_id [simp]: "(%x. x): A -> A"
    4.19 +  by (simp add: Pi_def)
    4.20 +*)
    4.21  text{*Covariance of Pi-sets in their second argument*}
    4.22  lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
    4.23    by (simp add: Pi_def, blast)
     5.1 --- a/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 20:22:46 2009 +0200
     5.2 +++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 22:49:12 2009 +0200
     5.3 @@ -289,8 +289,6 @@
     5.4    apply blast
     5.5    apply (fastsimp)
     5.6    apply (auto intro!: funcsetI finprod_closed) 
     5.7 -  apply (subst finprod_insert)
     5.8 -  apply (auto intro!: funcsetI finprod_closed)
     5.9  done
    5.10  
    5.11  lemma (in comm_monoid) finprod_Union_disjoint:
    5.12 @@ -304,11 +302,7 @@
    5.13  lemma (in comm_monoid) finprod_one [rule_format]: 
    5.14    "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
    5.15       finprod G f A = \<one>"
    5.16 -  apply (induct set: finite)
    5.17 -  apply auto
    5.18 -  apply (subst finprod_insert)
    5.19 -  apply (auto intro!: funcsetI)
    5.20 -done
    5.21 +by (induct set: finite) auto
    5.22  
    5.23  
    5.24  (* need better simplification rules for rings *)
     6.1 --- a/src/HOL/NewNumberTheory/Residues.thy	Fri Jun 19 20:22:46 2009 +0200
     6.2 +++ b/src/HOL/NewNumberTheory/Residues.thy	Fri Jun 19 22:49:12 2009 +0200
     6.3 @@ -186,17 +186,13 @@
     6.4  lemma (in residues) prod_cong: 
     6.5    "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
     6.6    apply (induct set: finite)
     6.7 -  apply (auto simp add: one_cong) 
     6.8 -  apply (subst finprod_insert)
     6.9 -  apply (auto intro!: funcsetI mult_cong)
    6.10 +  apply (auto simp: one_cong mult_cong)
    6.11  done
    6.12  
    6.13  lemma (in residues) sum_cong:
    6.14    "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
    6.15    apply (induct set: finite)
    6.16 -  apply (auto simp add: zero_cong) 
    6.17 -  apply (subst finsum_insert)
    6.18 -  apply (auto intro!: funcsetI add_cong)
    6.19 +  apply (auto simp: zero_cong add_cong)
    6.20  done
    6.21  
    6.22  lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>