neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
authorchaieb
Sat Oct 20 12:09:30 2007 +0200 (2007-10-20)
changeset 25111d52a58b51f1f
parent 25110 7253d331e9fc
child 25112 98824cc791c0
neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Fri Oct 19 23:21:15 2007 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Oct 20 12:09:30 2007 +0200
     1.3 @@ -497,7 +497,7 @@
     1.4  lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
     1.5    by (cases n) simp_all
     1.6  
     1.7 -lemma neq0_conv [iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
     1.8 +lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
     1.9    by (cases n) simp_all
    1.10  
    1.11  text {* This theorem is useful with @{text blast} *}
    1.12 @@ -510,7 +510,7 @@
    1.13  lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
    1.14    apply (rule iffI)
    1.15    apply (rule ccontr)
    1.16 -  apply simp_all
    1.17 +  apply (simp_all add: neq0_conv)
    1.18    done
    1.19  
    1.20  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
    1.21 @@ -604,7 +604,7 @@
    1.22    and I dread to think what happens if I put them in
    1.23  *}
    1.24  lemma Suc_pred [simp]: "0 < n ==> Suc (n - Suc 0) = n"
    1.25 -  by (simp split add: nat.split)
    1.26 +  by (simp add: neq0_conv split add: nat.split)
    1.27  
    1.28  declare diff_Suc [simp del, code del]
    1.29  
    1.30 @@ -1084,7 +1084,7 @@
    1.31  by (simp add: linorder_not_less [symmetric], auto)
    1.32  
    1.33  lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
    1.34 -  apply (cut_tac less_linear, safe, auto)
    1.35 +  apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
    1.36    apply (drule mult_less_mono1, assumption, simp)+
    1.37    done
    1.38  
    1.39 @@ -1105,8 +1105,8 @@
    1.40    apply (drule sym)
    1.41    apply (rule disjCI)
    1.42    apply (rule nat_less_cases, erule_tac [2] _)
    1.43 -  apply (fastsimp elim!: less_SucE)
    1.44 -  apply (fastsimp dest: mult_less_mono2)
    1.45 +  apply (fastsimp simp add: neq0_conv elim!: less_SucE)
    1.46 +  apply (fastsimp simp add: neq0_conv dest: mult_less_mono2)
    1.47    done
    1.48  
    1.49