feat(library/standard/bool_decidable): cleanup bool_decidable, and remove the artificial dependency to bit

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/bool_decidable.lean

@@ -1,26 +1,18 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import classical hilbert bit decidable
-using bit decidable
+import classical hilbert decidable
+using decidable
 
 -- Excluded middle + Hilbert implies every proposition is decidable
-definition to_bit (a : Bool) : bit
-:= epsilon (λ b : bit, (b = '1) ↔ a)
 
-theorem to_bit_def (a : Bool) : (to_bit a) = '1 ↔ a
+-- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle
+theorem inhabited_decidable [instance] (a : Bool) : inhabited (decidable a)
 := or_elim (em a)
-    (assume Hp, epsilon_ax (exists_intro '1 (iff_intro (assume H, Hp) (assume H, refl b1))))
-    (assume Hn, epsilon_ax (exists_intro '0 (iff_intro (assume H, absurd_elim a H b0_ne_b1) (assume H, absurd_elim ('0 = '1) H Hn))))
+    (assume Ha,  inhabited_intro (inl Ha))
+    (assume Hna, inhabited_intro (inr Hna))
 
+-- Note that inhabited_decidable is marked as an instance, and it is silently used
+-- for synthesizing the implicit argument in the following 'epsilon'
 theorem bool_decidable [instance] (a : Bool) : decidable a
-:= bit_rec
-    (assume H0 : to_bit a = '0,
-     have e1 : ¬ to_bit a = '1, from subst (symm H0) b0_ne_b1,
-     have Hna : ¬a, from iff_mp_left (iff_flip_sign (to_bit_def a)) e1,
-     inr Hna)
-    (assume H1 : to_bit a = '1,
-     have Ha : a, from iff_mp_left (to_bit_def a) H1,
-     inl Ha)
-    (to_bit a)
-    (refl (to_bit a))
+:= epsilon (λ d, true)