From 372d17ab96a35b0256f0b355cabd6f90f84f245e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jul 2015 23:21:10 -0700
Subject: [PATCH] refactor(library/data/nat/primes): rename is_prime to prime

---
 library/data/nat/primes.lean | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/library/data/nat/primes.lean b/library/data/nat/primes.lean
index 570b0c1955..23f4f954f7 100644
--- a/library/data/nat/primes.lean
+++ b/library/data/nat/primes.lean
@@ -11,12 +11,12 @@ open bool
 namespace nat
 open decidable
 
-definition is_prime [reducible] (p : nat) := p ≥ 2 ∧ ∀ m, m ∣ p → m = 1 ∨ m = p
+definition prime [reducible] (p : nat) := p ≥ 2 ∧ ∀ m, m ∣ p → m = 1 ∨ m = p
 
-definition is_prime_ext (p : nat) := p ≥ 2 ∧ ∀ m, m ≤ p → m ∣ p → m = 1 ∨ m = p
-local attribute is_prime_ext [reducible]
+definition prime_ext (p : nat) := p ≥ 2 ∧ ∀ m, m ≤ p → m ∣ p → m = 1 ∨ m = p
+local attribute prime_ext [reducible]
 
-lemma is_prime_ext_iff_is_prime (p : nat) : is_prime_ext p ↔ is_prime p :=
+lemma prime_ext_iff_prime (p : nat) : prime_ext p ↔ prime p :=
 iff.intro
   begin
     intro h, cases h with h₁ h₂, constructor, assumption,
@@ -27,27 +27,27 @@ iff.intro
     intro m l d, exact h₂ m d
   end
 
-definition decidable_is_prime [instance] (p : nat) : decidable (is_prime p) :=
-decidable_of_decidable_of_iff _ (is_prime_ext_iff_is_prime p)
+definition decidable_prime [instance] (p : nat) : decidable (prime p) :=
+decidable_of_decidable_of_iff _ (prime_ext_iff_prime p)
 
-lemma ge_two_of_is_prime {p : nat} : is_prime p → p ≥ 2 :=
+lemma ge_two_of_prime {p : nat} : prime p → p ≥ 2 :=
 assume h, obtain h₁ h₂, from h, h₁
 
-lemma pred_prime_pos {p : nat} : is_prime p → pred p > 0 :=
+lemma pred_prime_pos {p : nat} : prime p → pred p > 0 :=
 assume h,
-have h₁ : p ≥ 2, from ge_two_of_is_prime h,
+have h₁ : p ≥ 2, from ge_two_of_prime h,
 lt_of_succ_le (pred_le_pred h₁)
 
-lemma succ_pred_prime {p : nat} : is_prime p → succ (pred p) = p :=
-assume h, succ_pred_of_pos (lt_of_succ_le (le_of_succ_le (ge_two_of_is_prime h)))
+lemma succ_pred_prime {p : nat} : prime p → succ (pred p) = p :=
+assume h, succ_pred_of_pos (lt_of_succ_le (le_of_succ_le (ge_two_of_prime h)))
 
-lemma divisor_of_prime {p m : nat} : is_prime p → m ∣ p → m = 1 ∨ m = p :=
+lemma divisor_of_prime {p m : nat} : prime p → m ∣ p → m = 1 ∨ m = p :=
 assume h d, obtain h₁ h₂, from h, h₂ m d
 
-lemma gt_one_of_pos_of_prime_dvd {i p : nat} : is_prime p → 0 < i → i mod p = 0 → 1 < i :=
+lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i :=
 assume ipp pos h,
 have h₁ : p ∣ i, from dvd_of_mod_eq_zero h,
-have h₂ : p ≥ 2, from ge_two_of_is_prime ipp,
+have h₂ : p ≥ 2, from ge_two_of_prime ipp,
 have h₃ : p ≤ i, from le_of_dvd pos h₁,
 lt_of_succ_le (le.trans h₂ h₃)