src/HOL/Number_Theory/Pocklington.thy
 changeset 69064 5840724b1d71 parent 68707 5b269897df9d child 69785 9e326f6f8a24
```     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sun Sep 23 21:49:31 2018 +0200
1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Sep 24 14:30:09 2018 +0200
1.3 @@ -731,7 +731,7 @@
1.4
1.5  (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
1.6
1.7 -definition "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
1.8 +definition "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
1.9
1.10  lemma primefact:
1.11    fixes n :: nat
1.12 @@ -743,8 +743,8 @@
1.13    from assms have "n = prod_mset (prime_factorization n)"
1.15    also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
1.16 -  also have "\<dots> = foldr ( * ) xs 1" by (induct xs) simp_all
1.17 -  finally have "foldr ( * ) xs 1 = n" ..
1.18 +  also have "\<dots> = foldr (*) xs 1" by (induct xs) simp_all
1.19 +  finally have "foldr (*) xs 1 = n" ..
1.20    moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
1.21    ultimately have "primefact xs n" by (auto simp: primefact_def)
1.22    then show ?thesis ..
1.23 @@ -763,10 +763,10 @@
1.24  next
1.25    case (Cons q qs)
1.26    from Cons.prems[unfolded primefact_def]
1.27 -  have q: "prime q" "q * foldr ( * ) qs 1 = n" "\<forall>p \<in>set qs. prime p"
1.28 -    and p: "prime p" "p dvd q * foldr ( * ) qs 1"
1.29 +  have q: "prime q" "q * foldr (*) qs 1 = n" "\<forall>p \<in>set qs. prime p"
1.30 +    and p: "prime p" "p dvd q * foldr (*) qs 1"
1.31      by simp_all
1.32 -  consider "p dvd q" | "p dvd foldr ( * ) qs 1"
1.33 +  consider "p dvd q" | "p dvd foldr (*) qs 1"
1.34      by (metis p prime_dvd_mult_eq_nat)
1.35    then show ?case
1.36    proof cases
1.37 @@ -776,19 +776,19 @@
1.38      then show ?thesis by simp
1.39    next
1.40      case prem: 2
1.41 -    from q(3) have pqs: "primefact qs (foldr ( * ) qs 1)"
1.42 +    from q(3) have pqs: "primefact qs (foldr (*) qs 1)"
1.44      from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
1.45    qed
1.46  qed
1.47
1.48 -lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> list_all prime ps"
1.49 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> list_all prime ps"
1.50    by (auto simp add: primefact_def list_all_iff)
1.51
1.52  text \<open>Variant of Lucas theorem.\<close>
1.53  lemma lucas_primefact:
1.54    assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
1.55 -    and psn: "foldr ( * ) ps 1 = n - 1"
1.56 +    and psn: "foldr (*) ps 1 = n - 1"
1.57      and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
1.58    shows "prime n"
1.59  proof -
1.60 @@ -806,7 +806,7 @@
1.61  text \<open>Variant of Pocklington theorem.\<close>
1.62  lemma pocklington_primefact:
1.63    assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
1.64 -    and arnb: "(a^r) mod n = b" and psq: "foldr ( * ) ps 1 = q"
1.65 +    and arnb: "(a^r) mod n = b" and psq: "foldr (*) ps 1 = q"
1.66      and bqn: "(b^q) mod n = 1"
1.67      and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
1.68    shows "prime n"
```