From c9e5e40477c974f3920bd6bc1bc8d263b1017a77 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Oct 2014 13:47:51 -0700
Subject: [PATCH] refactor(library/data/num): cleanup

---
 library/data/num.lean | 40 ++++++++++++++++++++++------------------
 1 file changed, 22 insertions(+), 18 deletions(-)

diff --git a/library/data/num.lean b/library/data/num.lean
index 8b7f47f3c..014b28c3b 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -38,15 +38,15 @@ namespace pos_num
   definition size (a : pos_num) : pos_num :=
   rec_on a one (λn r, succ r) (λn r, succ r)
 
-  theorem succ_not_is_one {a : pos_num} : is_one (succ a) = ff :=
+  theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=
   induction_on a rfl (take n iH, rfl) (take n iH, rfl)
 
-  theorem pred_succ {a : pos_num} : pred (succ a) = a :=
+  theorem pred.succ (a : pos_num) : pred (succ a) = a :=
   rec_on a
     rfl
     (take (n : pos_num) (iH : pred (succ n) = n),
       calc
-        pred (succ (bit1 n)) = cond ff one (bit1 (pred (succ n))) : {succ_not_is_one}
+        pred (succ (bit1 n)) = cond ff one (bit1 (pred (succ n))) : {!succ_not_is_one}
                        ...   = bit1 (pred (succ n))               : rfl
                        ...   = bit1 n                             : {iH})
     (take (n : pos_num) (iH : pred (succ n) = n), rfl)
@@ -66,32 +66,36 @@ namespace pos_num
 
   infixl `+` := add
 
-  theorem add_one_one : one + one = bit0 one :=
+  section
+  variables (a b : pos_num)
+
+  theorem add.one_one : one + one = bit0 one :=
   rfl
 
-  theorem add_one_bit0 {a : pos_num} : one + (bit0 a) = bit1 a :=
+  theorem add.one_bit0 : one + (bit0 a) = bit1 a :=
   rfl
 
-  theorem add_one_bit1 {a : pos_num} : one + (bit1 a) = succ (bit1 a) :=
+  theorem add.one_bit1 : one + (bit1 a) = succ (bit1 a) :=
   rfl
 
-  theorem add_bit0_one {a : pos_num} : (bit0 a) + one = bit1 a :=
+  theorem add.bit0_one : (bit0 a) + one = bit1 a :=
   rfl
 
-  theorem add_bit1_one {a : pos_num} : (bit1 a) + one = succ (bit1 a) :=
+  theorem add.bit1_one : (bit1 a) + one = succ (bit1 a) :=
   rfl
 
-  theorem add_bit0_bit0 {a b : pos_num} : (bit0 a) + (bit0 b) = bit0 (a + b) :=
+  theorem add.bit0_bit0 : (bit0 a) + (bit0 b) = bit0 (a + b) :=
   rfl
 
-  theorem add_bit0_bit1 {a b : pos_num} : (bit0 a) + (bit1 b) = bit1 (a + b) :=
+  theorem add.bit0_bit1 : (bit0 a) + (bit1 b) = bit1 (a + b) :=
   rfl
 
-  theorem add_bit1_bit0 {a b : pos_num} : (bit1 a) + (bit0 b) = bit1 (a + b) :=
+  theorem add.bit1_bit0 : (bit1 a) + (bit0 b) = bit1 (a + b) :=
   rfl
 
-  theorem add_bit1_bit1 {a b : pos_num} : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) :=
+  theorem add.bit1_bit1 : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) :=
   rfl
+  end
 
   definition mul (a b : pos_num) : pos_num :=
   rec_on a
@@ -101,16 +105,16 @@ namespace pos_num
 
   infixl `*` := mul
 
-  theorem mul_one_left (a : pos_num) : one * a = a :=
+  theorem mul.one_left (a : pos_num) : one * a = a :=
   rfl
 
-  theorem mul_one_right (a : pos_num) : a * one = a :=
+  theorem mul.one_right (a : pos_num) : a * one = a :=
   induction_on a
     rfl
     (take (n : pos_num) (iH : n * one = n),
       calc bit1 n * one = bit0 (n * one) + one : rfl
                    ...  = bit0 n + one : {iH}
-                   ...  = bit1 n       : add_bit0_one)
+                   ...  = bit1 n       : !add.bit0_one)
     (take (n : pos_num) (iH : n * one = n),
       calc bit0 n * one = bit0 (n * one) : rfl
                     ... = bit0 n         : {iH})
@@ -142,14 +146,14 @@ namespace num
   definition size (a : num) : num :=
   rec_on a (pos one) (λp, pos (size p))
 
-  theorem pred_succ (a : num) : pred (succ a) = a :=
+  theorem pred.succ (a : num) : pred (succ a) = a :=
   rec_on a
     rfl
     (λp, calc
       pred (succ (pos p)) = pred (pos (pos_num.succ p)) : rfl
-                   ...    = cond ff zero (pos (pos_num.pred (pos_num.succ p))) : {succ_not_is_one}
+                   ...    = cond ff zero (pos (pos_num.pred (pos_num.succ p))) : {!succ_not_is_one}
                    ...    = pos (pos_num.pred (pos_num.succ p)) : !cond.ff
-                   ...    = pos p : {pos_num.pred_succ})
+                   ...    = pos p : {!pos_num.pred.succ})
 
   definition add (a b : num) : num :=
   rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b)))