# HG changeset patch
# User huffman
# Date 1235059672 28800
# Node ID c60ace776315c6245bc9fc12912c7de05ffedc3f
# Parent  b11793ea15a3caef8565e645d07226bc8279c5a5
add more ordering lemmas

diff -r b11793ea15a3 -r c60ace776315 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Feb 19 06:47:06 2009 -0800
+++ b/src/HOL/ex/Numeral.thy	Thu Feb 19 08:07:52 2009 -0800
@@ -157,6 +157,18 @@
   by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
                     left_distrib right_distrib)
 
+lemma Dig_eq:
+  "One = One \<longleftrightarrow> True"
+  "One = Dig0 n \<longleftrightarrow> False"
+  "One = Dig1 n \<longleftrightarrow> False"
+  "Dig0 m = One \<longleftrightarrow> False"
+  "Dig1 m = One \<longleftrightarrow> False"
+  "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
+  "Dig0 m = Dig1 n \<longleftrightarrow> False"
+  "Dig1 m = Dig0 n \<longleftrightarrow> False"
+  "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
+  by simp_all
+
 lemma less_eq_num_code [numeral, simp, code]:
   "One \<le> n \<longleftrightarrow> True"
   "Dig0 m \<le> One \<longleftrightarrow> False"
@@ -433,21 +445,12 @@
 
 text {*  Could be perhaps more general than here. *}
 
-lemma (in ordered_semidom) of_num_pos: "0 < of_num n"
-proof -
-  have "(0::nat) < of_num n"
-    by (induct n) (simp_all add: semiring_numeral_class.of_num.simps)
-  then have "of_nat 0 \<noteq> of_nat (of_num n)" 
-    by (cases n) (simp_all only: semiring_numeral_class.of_num.simps of_nat_eq_iff)
-  then have "0 \<noteq> of_num n"
-    by (simp add: of_nat_of_num)
-  moreover have "0 \<le> of_nat (of_num n)" by simp
-  ultimately show ?thesis by (simp add: of_nat_of_num)
-qed
-
 context ordered_semidom
 begin
 
+lemma of_num_pos [numeral]: "0 < of_num n"
+  by (induct n) (simp_all add: of_num.simps add_pos_pos)
+
 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
 proof -
   have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"
@@ -490,6 +493,68 @@
   then show ?thesis by (simp add: of_num_one)
 qed
 
+lemma of_num_nonneg [numeral]: "0 \<le> of_num n"
+  by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg)
+
+lemma of_num_less_zero_iff [numeral]: "\<not> of_num n < 0"
+  by (simp add: not_less of_num_nonneg)
+
+lemma of_num_le_zero_iff [numeral]: "\<not> of_num n \<le> 0"
+  by (simp add: not_le of_num_pos)
+
+end
+
+context ordered_idom
+begin
+
+lemma minus_of_num_less_of_num_iff [numeral]: "- of_num m < of_num n"
+proof -
+  have "- of_num m < 0" by (simp add: of_num_pos)
+  also have "0 < of_num n" by (simp add: of_num_pos)
+  finally show ?thesis .
+qed
+
+lemma minus_of_num_less_one_iff [numeral]: "- of_num n < 1"
+proof -
+  have "- of_num n < 0" by (simp add: of_num_pos)
+  also have "0 < 1" by simp
+  finally show ?thesis .
+qed
+
+lemma minus_one_less_of_num_iff [numeral]: "- 1 < of_num n"
+proof -
+  have "- 1 < 0" by simp
+  also have "0 < of_num n" by (simp add: of_num_pos)
+  finally show ?thesis .
+qed
+
+lemma minus_of_num_le_of_num_iff [numeral]: "- of_num m \<le> of_num n"
+  by (simp add: less_imp_le minus_of_num_less_of_num_iff)
+
+lemma minus_of_num_le_one_iff [numeral]: "- of_num n \<le> 1"
+  by (simp add: less_imp_le minus_of_num_less_one_iff)
+
+lemma minus_one_le_of_num_iff [numeral]: "- 1 \<le> of_num n"
+  by (simp add: less_imp_le minus_one_less_of_num_iff)
+
+lemma of_num_le_minus_of_num_iff [numeral]: "\<not> of_num m \<le> - of_num n"
+  by (simp add: not_le minus_of_num_less_of_num_iff)
+
+lemma one_le_minus_of_num_iff [numeral]: "\<not> 1 \<le> - of_num n"
+  by (simp add: not_le minus_of_num_less_one_iff)
+
+lemma of_num_le_minus_one_iff [numeral]: "\<not> of_num n \<le> - 1"
+  by (simp add: not_le minus_one_less_of_num_iff)
+
+lemma of_num_less_minus_of_num_iff [numeral]: "\<not> of_num m < - of_num n"
+  by (simp add: not_less minus_of_num_le_of_num_iff)
+
+lemma one_less_minus_of_num_iff [numeral]: "\<not> 1 < - of_num n"
+  by (simp add: not_less minus_of_num_le_one_iff)
+
+lemma of_num_less_minus_one_iff [numeral]: "\<not> of_num n < - 1"
+  by (simp add: not_less minus_one_le_of_num_iff)
+
 end
 
 subsubsection {*