refactor(library): make sure "choose" compute inside the kernel

library/data/encodable.lean

@@ -273,7 +273,7 @@ exists.intro (encode w)
     unfold pn, rewrite [encodek], esimp, exact pw
   end
 
-private lemma decode_ne_none_of_pn {n : nat} : pn n → decode A n ≠ none :=
+private definition decode_ne_none_of_pn {n : nat} : pn n → decode A n ≠ none :=
 assume pnn e,
 begin
   rewrite [▸ (match decode A n with | some a := p a | none   := false end) at pnn],
@@ -283,7 +283,7 @@ end
 
 open subtype
 
-private lemma of_nat (n : nat) : pn n → { a : A | p a } :=
+private definition of_nat (n : nat) : pn n → { a : A | p a } :=
 match decode A n with
 | some a := λ (e : decode A n = some a),
   begin

library/data/fintype.lean

@@ -91,13 +91,13 @@ definition check_pred (p : A → Prop) [h : decidable_pred p] : list A → bool
 | []     := tt
 | (a::l) := if p a then check_pred l else ff
 
-theorem check_pred_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : p a → check_pred p (a::l) = check_pred p l :=
+definition check_pred_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : p a → check_pred p (a::l) = check_pred p l :=
 assume pa, if_pos pa
 
-theorem check_pred_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : ¬ p a → check_pred p (a::l) = ff :=
+definition check_pred_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : ¬ p a → check_pred p (a::l) = ff :=
 assume npa, if_neg npa
 
-theorem all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = tt → ∀ {a}, a ∈ l → p a
+definition all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = tt → ∀ {a}, a ∈ l → p a
 | []     eqtt a ainl := absurd ainl !not_mem_nil
 | (b::l) eqtt a ainbl := by_cases
   (λ pb  : p b, or.elim (eq_or_mem_of_mem_cons ainbl)
@@ -108,7 +108,7 @@ theorem all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l
   (λ npb : ¬ p b,
     by rewrite [check_pred_cons_of_neg _ npb at eqtt]; exact (bool.no_confusion eqtt))
 
-theorem ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = ff → ∃ w, ¬ p w
+definition ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = ff → ∃ w, ¬ p w
 | []     eqtt := bool.no_confusion eqtt
 | (a::l) eqtt := by_cases
   (λ pa  : p a,

library/data/nat/choose.lean

@@ -21,10 +21,10 @@ parameter {p : nat → Prop}
 
 private definition lbp (x : nat) : Prop := ∀ y, y < x → ¬ p y
 
-private lemma lbp_zero : lbp 0 :=
+private definition lbp_zero : lbp 0 :=
 λ y h, absurd h (not_lt_zero y)
 
-private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
+private definition lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
 λ lx npx y yltsx,
   or.elim (eq_or_lt_of_le yltsx)
     (λ yeqx, by rewrite [yeqx]; exact npx)

library/data/nat/order.lean

@@ -14,16 +14,16 @@ namespace nat
 
 /- lt and le -/
 
-theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
+definition le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
 or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
 
-theorem lt.by_cases {a b : ℕ} {P : Prop}
+definition lt.by_cases {a b : ℕ} {P : Prop}
   (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
 or.elim !lt.trichotomy
   (assume H, H1 H)
   (assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
 
-theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
+definition lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
 lt.by_cases
   (assume H1 : m < n, or.inl H1)
   (assume H1 : m = n, or.inr H1)
@@ -32,7 +32,7 @@ lt.by_cases
 theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n :=
 iff.intro lt_or_eq_of_le le_of_lt_or_eq
 
-theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
+definition lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
 or.elim (lt_or_eq_of_le H1)
   (take H3 : m < n, H3)
   (take H3 : m = n, absurd H3 H2)

library/init/logic.lean

@@ -20,7 +20,7 @@ false.rec b (H2 H1)
 
 /- not -/
 
-theorem not_false : ¬false :=
+definition not_false : ¬false :=
 assume H : false, H
 
 definition non_contradictory (a : Prop) : Prop := ¬¬a
@@ -172,7 +172,7 @@ notation a `\/` b := or a b
 notation a ∨ b := or a b
 
 namespace or
-  theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
+  definition elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
   or.rec H₂ H₃ H₁
 end or
 
@@ -266,7 +266,7 @@ definition exists.intro := @Exists.intro
 notation `exists` binders `,` r:(scoped P, Exists P) := r
 notation `∃` binders `,` r:(scoped P, Exists P) := r
 
-theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
+definition exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
 Exists.rec H2 H1
 
 /- decidable -/