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.14      by (simp add: prod_mset_prime_factorization)
    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.43        by (simp add: primefact_def)
    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"