Adjusting Number_Theory for new Algebra
authorpaulson <lp15@cam.ac.uk>
Thu Jun 14 15:20:10 2018 +0100 (5 months ago)
changeset 684470beb927eed89
parent 68446 92ddca1edc43
child 68448 3d1517f3ba49
Adjusting Number_Theory for new Algebra
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:48 2018 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 15:20:10 2018 +0100
     1.3 @@ -332,15 +332,18 @@
     1.4    apply (auto simp add: finprod_def)
     1.5    done
     1.6  
     1.7 -lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
     1.8 +lemma finprod_one_eqI: "(\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
     1.9  proof (induct A rule: infinite_finite_induct)
    1.10    case empty show ?case by simp
    1.11  next
    1.12    case (insert a A)
    1.13 -  have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
    1.14 +  have "(\<lambda>i. \<one>) \<in> A \<rightarrow> carrier G" by auto
    1.15    with insert show ?case by simp
    1.16  qed simp
    1.17  
    1.18 +lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
    1.19 +  by (simp add: finprod_one_eqI)
    1.20 +
    1.21  lemma finprod_closed [simp]:
    1.22    fixes A
    1.23    assumes f: "f \<in> A \<rightarrow> carrier G" 
     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 14:23:48 2018 +0100
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 15:20:10 2018 +0100
     2.3 @@ -10,9 +10,6 @@
     2.4  theory Residues
     2.5  imports
     2.6    Cong
     2.7 -  "HOL-Algebra.More_Group"
     2.8 -  "HOL-Algebra.More_Ring"
     2.9 -  "HOL-Algebra.More_Finite_Product"
    2.10    "HOL-Algebra.Multiplicative_Group"
    2.11    Totient
    2.12  begin
    2.13 @@ -355,7 +352,7 @@
    2.14       apply (metis Units_inv_inv)+
    2.15      done
    2.16    also have "\<dots> = \<one>"
    2.17 -    apply (rule finprod_one)
    2.18 +    apply (rule finprod_one_eqI)
    2.19       apply auto
    2.20      apply (subst finprod_insert)
    2.21          apply auto