src/HOL/Nat.thy

   by (cases n) simp_all
 
 lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
   by (cases n) simp_all
 
-lemma neq0_conv [iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
+lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   by (cases n) simp_all
 
 text {* This theorem is useful with @{text blast} *}
 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   by (rule iffD1, rule neq0_conv, iprover)

   by (fast intro: not0_implies_Suc)
 
 lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   apply (rule iffI)
   apply (rule ccontr)
-  apply simp_all
+  apply (simp_all add: neq0_conv)
   done
 
 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   by (induct m') simp_all
 

   Could be (and is, below) generalized in various ways
   However, none of the generalizations are currently in the simpset,
   and I dread to think what happens if I put them in
 *}
 lemma Suc_pred [simp]: "0 < n ==> Suc (n - Suc 0) = n"
-  by (simp split add: nat.split)
+  by (simp add: neq0_conv split add: nat.split)
 
 declare diff_Suc [simp del, code del]
 
 
 subsection {* Addition *}

 
 lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
 by (simp add: linorder_not_less [symmetric], auto)
 
 lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
-  apply (cut_tac less_linear, safe, auto)
+  apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
   apply (drule mult_less_mono1, assumption, simp)+
   done
 
 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
 by (simp add: mult_commute [of k])

 text {* Lemma for @{text gcd} *}
 lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
-  apply (fastsimp elim!: less_SucE)
-  apply (fastsimp dest: mult_less_mono2)
+  apply (fastsimp simp add: neq0_conv elim!: less_SucE)
+  apply (fastsimp simp add: neq0_conv dest: mult_less_mono2)
   done
 
 
 subsection {* size of a datatype value *}