# HG changeset patch
# User nipkow
# Date 1192998815 -7200
# Node ID 273772abbea274fbfb00165e92323b95893df985
# Parent  ffc5054a72740b2ca4df393d45698c510a4c1b90
More changes from >0 to ~=0::nat

diff -r ffc5054a7274 -r 273772abbea2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Oct 21 19:32:19 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Oct 21 22:33:35 2007 +0200
@@ -759,7 +759,7 @@
   apply (rule_tac x = "x # xa" in exI, auto)
   done
 
-lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
+lemma set_count_greater_0: "set x = {a. count (multiset_of x) a \<noteq> 0}"
   by (induct x) auto
 
 lemma distinct_count_atmost_1:
diff -r ffc5054a7274 -r 273772abbea2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 21 19:32:19 2007 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 21 22:33:35 2007 +0200
@@ -500,6 +500,8 @@
 lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   by (cases n) simp_all
 
+lemmas gr0_conv = neq0_conv[symmetric]
+
 text {* This theorem is useful with @{text blast} *}
 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   by (rule iffD1, rule neq0_conv, iprover)
@@ -655,8 +657,8 @@
 lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   by (rule trans, rule eq_commute, rule add_is_1)
 
-lemma add_gr_0 [iff]: "!!m::nat. (m + n \<noteq> 0) = (m\<noteq>0 | n\<noteq>0)"
-by simp
+lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m\<noteq>0 | n\<noteq>0)"
+by (simp add:gr0_conv)
 
 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   apply (drule add_0_right [THEN ssubst])
diff -r ffc5054a7274 -r 273772abbea2 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Sun Oct 21 19:32:19 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Sun Oct 21 22:33:35 2007 +0200
@@ -1208,10 +1208,10 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
+lemma natfloor_div_nat: "1 <= x ==> y \<noteq> 0 ==>
   natfloor (x / real y) = natfloor x div y"
 proof -
-  assume "1 <= (x::real)" and "0 < (y::nat)"
+  assume "1 <= (x::real)" and "(y::nat) \<noteq> 0"
   have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
     by simp
   then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
@@ -1269,14 +1269,12 @@
     apply (subgoal_tac "natfloor x mod y < y")
     apply arith
     apply (rule mod_less_divisor)
-    apply assumption
     apply auto
     apply (simp add: compare_rls)
     apply (subst add_commute)
     apply (rule real_natfloor_add_one_gt)
     done
-  finally show ?thesis
-    by simp
+  finally show ?thesis by simp
 qed
 
 end
diff -r ffc5054a7274 -r 273772abbea2 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sun Oct 21 19:32:19 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Sun Oct 21 22:33:35 2007 +0200
@@ -746,8 +746,8 @@
 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
 by (simp add: add: real_of_nat_def of_nat_diff)
 
-lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
-by (simp add: add: real_of_nat_def) 
+lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
+by (auto simp: real_of_nat_def)
 
 lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
 by (simp add: add: real_of_nat_def)
@@ -755,7 +755,7 @@
 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
 by (simp add: add: real_of_nat_def)
 
-lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
+lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat))"
 by (simp add: add: real_of_nat_def)
 
 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"