# HG changeset patch
# User huffman
# Date 1228342983 28800
# Node ID 74c60b78969c7e6f518626a2e161e470332c1cce
# Parent  48cd567f6940f10c5d9323ce611a19c91dc72cb8
cleaned up subsection headings;
added simp rules for comparisons on binary numbers

diff -r 48cd567f6940 -r 74c60b78969c src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Dec 03 15:59:56 2008 +0100
+++ b/src/HOL/Int.thy	Wed Dec 03 14:23:03 2008 -0800
@@ -581,6 +581,8 @@
   Springer LNCS 488 (240-251), 1991.
 *}
 
+subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
+
 definition
   Pls :: int where
   [code del]: "Pls = 0"
@@ -651,127 +653,308 @@
   Bit0_Pls Bit1_Min
 
 
-subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
-
-lemma succ_Pls [simp]:
+subsubsection {* Successor and predecessor functions *}
+
+text {* Successor *}
+
+lemma succ_Pls:
   "succ Pls = Bit1 Pls"
   unfolding numeral_simps by simp
 
-lemma succ_Min [simp]:
+lemma succ_Min:
   "succ Min = Pls"
   unfolding numeral_simps by simp
 
-lemma succ_Bit0 [simp]:
+lemma succ_Bit0:
   "succ (Bit0 k) = Bit1 k"
   unfolding numeral_simps by simp
 
-lemma succ_Bit1 [simp]:
+lemma succ_Bit1:
   "succ (Bit1 k) = Bit0 (succ k)"
   unfolding numeral_simps by simp
 
-lemmas succ_bin_simps =
+lemmas succ_bin_simps [simp] =
   succ_Pls succ_Min succ_Bit0 succ_Bit1
 
-lemma pred_Pls [simp]:
+text {* Predecessor *}
+
+lemma pred_Pls:
   "pred Pls = Min"
   unfolding numeral_simps by simp
 
-lemma pred_Min [simp]:
+lemma pred_Min:
   "pred Min = Bit0 Min"
   unfolding numeral_simps by simp
 
-lemma pred_Bit0 [simp]:
+lemma pred_Bit0:
   "pred (Bit0 k) = Bit1 (pred k)"
   unfolding numeral_simps by simp 
 
-lemma pred_Bit1 [simp]:
+lemma pred_Bit1:
   "pred (Bit1 k) = Bit0 k"
   unfolding numeral_simps by simp
 
-lemmas pred_bin_simps =
+lemmas pred_bin_simps [simp] =
   pred_Pls pred_Min pred_Bit0 pred_Bit1
 
-lemma minus_Pls [simp]:
+
+subsubsection {* Binary arithmetic *}
+
+text {* Addition *}
+
+lemma add_Pls:
+  "Pls + k = k"
+  unfolding numeral_simps by simp
+
+lemma add_Min:
+  "Min + k = pred k"
+  unfolding numeral_simps by simp
+
+lemma add_Bit0_Bit0:
+  "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
+  unfolding numeral_simps by simp
+
+lemma add_Bit0_Bit1:
+  "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
+  unfolding numeral_simps by simp
+
+lemma add_Bit1_Bit0:
+  "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
+  unfolding numeral_simps by simp
+
+lemma add_Bit1_Bit1:
+  "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
+  unfolding numeral_simps by simp
+
+lemma add_Pls_right:
+  "k + Pls = k"
+  unfolding numeral_simps by simp
+
+lemma add_Min_right:
+  "k + Min = pred k"
+  unfolding numeral_simps by simp
+
+lemmas add_bin_simps [simp] =
+  add_Pls add_Min add_Pls_right add_Min_right
+  add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
+
+text {* Negation *}
+
+lemma minus_Pls:
   "- Pls = Pls"
-  unfolding numeral_simps by simp 
-
-lemma minus_Min [simp]:
+  unfolding numeral_simps by simp
+
+lemma minus_Min:
   "- Min = Bit1 Pls"
-  unfolding numeral_simps by simp 
-
-lemma minus_Bit0 [simp]:
+  unfolding numeral_simps by simp
+
+lemma minus_Bit0:
   "- (Bit0 k) = Bit0 (- k)"
-  unfolding numeral_simps by simp 
-
-lemma minus_Bit1 [simp]:
+  unfolding numeral_simps by simp
+
+lemma minus_Bit1:
   "- (Bit1 k) = Bit1 (pred (- k))"
   unfolding numeral_simps by simp
 
-lemmas minus_bin_simps =
+lemmas minus_bin_simps [simp] =
   minus_Pls minus_Min minus_Bit0 minus_Bit1
 
-
-subsection {*
-  Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
-    and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
-*}
-
-lemma add_Pls [simp]:
-  "Pls + k = k"
-  unfolding numeral_simps by simp 
-
-lemma add_Min [simp]:
-  "Min + k = pred k"
+text {* Subtraction *}
+
+lemma diff_Pls:
+  "Pls - k = - k"
+  unfolding numeral_simps by simp
+
+lemma diff_Min:
+  "Min - k = pred (- k)"
+  unfolding numeral_simps by simp
+
+lemma diff_Bit0_Bit0:
+  "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
+  unfolding numeral_simps by simp
+
+lemma diff_Bit0_Bit1:
+  "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
+  unfolding numeral_simps by simp
+
+lemma diff_Bit1_Bit0:
+  "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
   unfolding numeral_simps by simp
 
-lemma add_Bit0_Bit0 [simp]:
-  "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
-  unfolding numeral_simps by simp_all 
-
-lemma add_Bit0_Bit1 [simp]:
-  "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
-  unfolding numeral_simps by simp_all 
-
-lemma add_Bit1_Bit0 [simp]:
-  "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
+lemma diff_Bit1_Bit1:
+  "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
   unfolding numeral_simps by simp
 
-lemma add_Bit1_Bit1 [simp]:
-  "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
+lemma diff_Pls_right:
+  "k - Pls = k"
+  unfolding numeral_simps by simp
+
+lemma diff_Min_right:
+  "k - Min = succ k"
   unfolding numeral_simps by simp
 
-lemma add_Pls_right [simp]:
-  "k + Pls = k"
-  unfolding numeral_simps by simp 
-
-lemma add_Min_right [simp]:
-  "k + Min = pred k"
+lemmas diff_bin_simps [simp] =
+  diff_Pls diff_Min diff_Pls_right diff_Min_right
+  diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
+
+text {* Multiplication *}
+
+lemma mult_Pls:
+  "Pls * w = Pls"
   unfolding numeral_simps by simp
 
-lemmas add_bin_simps =
-  add_Pls add_Min add_Pls_right add_Min_right
-  add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
-
-lemma mult_Pls [simp]:
-  "Pls * w = Pls"
-  unfolding numeral_simps by simp 
-
-lemma mult_Min [simp]:
+lemma mult_Min:
   "Min * k = - k"
   unfolding numeral_simps by simp
 
-lemma mult_Bit0 [simp]:
+lemma mult_Bit0:
   "(Bit0 k) * l = Bit0 (k * l)"
   unfolding numeral_simps int_distrib by simp
 
-lemma mult_Bit1 [simp]:
+lemma mult_Bit1:
   "(Bit1 k) * l = (Bit0 (k * l)) + l"
-  unfolding numeral_simps int_distrib by simp 
-
-lemmas mult_bin_simps =
+  unfolding numeral_simps int_distrib by simp
+
+lemmas mult_bin_simps [simp] =
   mult_Pls mult_Min mult_Bit0 mult_Bit1
 
 
+subsubsection {* Binary comparisons *}
+
+text {* Preliminaries *}
+
+lemma even_less_0_iff:
+  "a + a < 0 \<longleftrightarrow> a < (0::'a::ordered_idom)"
+proof -
+  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
+  also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
+    by (simp add: mult_less_0_iff zero_less_two 
+                  order_less_not_sym [OF zero_less_two])
+  finally show ?thesis .
+qed
+
+lemma le_imp_0_less: 
+  assumes le: "0 \<le> z"
+  shows "(0::int) < 1 + z"
+proof -
+  have "0 \<le> z" by fact
+  also have "... < z + 1" by (rule less_add_one) 
+  also have "... = 1 + z" by (simp add: add_ac)
+  finally show "0 < 1 + z" .
+qed
+
+lemma odd_less_0_iff:
+  "(1 + z + z < 0) = (z < (0::int))"
+proof (cases z rule: int_cases)
+  case (nonneg n)
+  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
+                             le_imp_0_less [THEN order_less_imp_le])  
+next
+  case (neg n)
+  thus ?thesis by (simp del: of_nat_Suc of_nat_add
+    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
+qed
+
+lemma neg_simps:
+  "Pls < 0 \<longleftrightarrow> False"
+  "Min < 0 \<longleftrightarrow> True"
+  "Bit0 w < 0 \<longleftrightarrow> w < 0"
+  "Bit1 w < 0 \<longleftrightarrow> w < 0"
+  unfolding numeral_simps
+  by (simp_all add: even_less_0_iff odd_less_0_iff)
+
+lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
+  by simp
+
+lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
+  unfolding numeral_simps
+  proof
+    have "k - 1 < k" by simp
+    also assume "k \<le> l"
+    finally show "k - 1 < l" .
+  next
+    assume "k - 1 < l"
+    hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
+    thus "k \<le> l" by simp
+  qed
+
+lemma succ_pred: "succ (pred x) = x"
+  unfolding numeral_simps by simp
+
+text {* Less-than *}
+
+lemma less_bin_simps [simp]:
+  "Pls < Pls \<longleftrightarrow> False"
+  "Pls < Min \<longleftrightarrow> False"
+  "Pls < Bit0 k \<longleftrightarrow> Pls < k"
+  "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
+  "Min < Pls \<longleftrightarrow> True"
+  "Min < Min \<longleftrightarrow> False"
+  "Min < Bit0 k \<longleftrightarrow> Min < k"
+  "Min < Bit1 k \<longleftrightarrow> Min < k"
+  "Bit0 k < Pls \<longleftrightarrow> k < Pls"
+  "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
+  "Bit1 k < Pls \<longleftrightarrow> k < Pls"
+  "Bit1 k < Min \<longleftrightarrow> k < Min"
+  "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
+  "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
+  "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
+  "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
+  unfolding le_iff_pred_less
+    less_bin_lemma [of Pls]
+    less_bin_lemma [of Min]
+    less_bin_lemma [of "k"]
+    less_bin_lemma [of "Bit0 k"]
+    less_bin_lemma [of "Bit1 k"]
+    less_bin_lemma [of "pred Pls"]
+    less_bin_lemma [of "pred k"]
+  by (simp_all add: neg_simps succ_pred)
+
+text {* Less-than-or-equal *}
+
+lemma le_bin_simps [simp]:
+  "Pls \<le> Pls \<longleftrightarrow> True"
+  "Pls \<le> Min \<longleftrightarrow> False"
+  "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
+  "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
+  "Min \<le> Pls \<longleftrightarrow> True"
+  "Min \<le> Min \<longleftrightarrow> True"
+  "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
+  "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
+  "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
+  "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
+  "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
+  "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
+  "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
+  "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
+  "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
+  "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
+  unfolding not_less [symmetric]
+  by (simp_all add: not_le)
+
+text {* Equality *}
+
+lemma eq_bin_simps [simp]:
+  "Pls = Pls \<longleftrightarrow> True"
+  "Pls = Min \<longleftrightarrow> False"
+  "Pls = Bit0 l \<longleftrightarrow> Pls = l"
+  "Pls = Bit1 l \<longleftrightarrow> False"
+  "Min = Pls \<longleftrightarrow> False"
+  "Min = Min \<longleftrightarrow> True"
+  "Min = Bit0 l \<longleftrightarrow> False"
+  "Min = Bit1 l \<longleftrightarrow> Min = l"
+  "Bit0 k = Pls \<longleftrightarrow> k = Pls"
+  "Bit0 k = Min \<longleftrightarrow> False"
+  "Bit1 k = Pls \<longleftrightarrow> False"
+  "Bit1 k = Min \<longleftrightarrow> k = Min"
+  "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
+  "Bit0 k = Bit1 l \<longleftrightarrow> False"
+  "Bit1 k = Bit0 l \<longleftrightarrow> False"
+  "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
+  unfolding order_eq_iff [where 'a=int]
+  by (simp_all add: not_less)
+
+
 subsection {* Converting Numerals to Rings: @{term number_of} *}
 
 class number_ring = number + comm_ring_1 +
@@ -804,15 +987,19 @@
 
 lemma number_of_minus:
   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  unfolding number_of_eq by (rule of_int_minus)
 
 lemma number_of_add:
   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  unfolding number_of_eq by (rule of_int_add)
+
+lemma number_of_diff:
+  "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
+  unfolding number_of_eq by (rule of_int_diff)
 
 lemma number_of_mult:
   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  unfolding number_of_eq by (rule of_int_mult)
 
 text {*
   The correctness of shifting.
@@ -885,7 +1072,7 @@
   unfolding number_of_eq numeral_simps by simp
 
 
-subsection {* Equality of Binary Numbers *}
+subsubsection {* Equality of Binary Numbers *}
 
 text {* First version by Norbert Voelker *}
 
@@ -945,20 +1132,10 @@
   unfolding iszero_def numeral_m1_eq_minus_1 by simp
 
 
-subsection {* Comparisons, for Ordered Rings *}
+subsubsection {* Comparisons, for Ordered Rings *}
 
 lemmas double_eq_0_iff = double_zero
 
-lemma le_imp_0_less: 
-  assumes le: "0 \<le> z"
-  shows "(0::int) < 1 + z"
-proof -
-  have "0 \<le> z" by fact
-  also have "... < z + 1" by (rule less_add_one) 
-  also have "... = 1 + z" by (simp add: add_ac)
-  finally show "0 < 1 + z" .
-qed
-
 lemma odd_nonzero:
   "1 + z + z \<noteq> (0::int)";
 proof (cases z rule: int_cases)
@@ -1011,7 +1188,7 @@
 qed
 
 
-subsection {* The Less-Than Relation *}
+subsubsection {* The Less-Than Relation *}
 
 lemma less_number_of_eq_neg:
   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
@@ -1101,11 +1278,12 @@
   by auto
 
 
-subsection {* Simplification of arithmetic operations on integer constants. *}
+subsubsection {* Simplification of arithmetic operations on integer constants. *}
 
 lemmas arith_extra_simps [standard, simp] =
   number_of_add [symmetric]
-  number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
+  number_of_minus [symmetric]
+  numeral_m1_eq_minus_1 [symmetric]
   number_of_mult [symmetric]
   diff_number_of_eq abs_number_of 
 
@@ -1132,7 +1310,7 @@
    because its lhs simplifies to "iszero 0" *)
 
 
-subsection {* Simplification of arithmetic when nested to the right. *}
+subsubsection {* Simplification of arithmetic when nested to the right. *}
 
 lemma add_number_of_left [simp]:
   "number_of v + (number_of w + z) =
@@ -1482,7 +1660,7 @@
 by arith
 
 
-subsection{*The Functions @{term nat} and @{term int}*}
+subsection{*The functions @{term nat} and @{term int}*}
 
 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
   @{term "w + - z"}*}
@@ -1835,23 +2013,15 @@
   "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
   "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
   "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
-  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq Int.Pls k1"
+  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
   "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
   "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
-  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq Int.Min k1"
+  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
   "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
   "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
   "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
   "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
-  unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
-    eq_number_of_int_code [symmetric, of Int.Min]
-    eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
-    eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
-    eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
-    eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
-  by (simp_all add: eq Pls_def,
-    simp_all only: Min_def succ_def pred_def number_of_is_id)
-    (auto simp add: iszero_def)
+  unfolding eq_equals by simp_all
 
 lemma eq_int_refl [code nbe]:
   "eq_class.eq (k::int) k \<longleftrightarrow> True"
@@ -1878,15 +2048,7 @@
   "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
-  unfolding less_eq_number_of_int_code [symmetric, of Int.Pls] 
-    less_eq_number_of_int_code [symmetric, of Int.Min]
-    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
-    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
-    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
-    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
-  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
-    (auto simp add: neg_def linorder_not_less group_simps
-      zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
+  by simp_all
 
 lemma less_number_of_int_code [code]:
   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
@@ -1909,15 +2071,7 @@
   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
-  unfolding less_number_of_int_code [symmetric, of Int.Pls] 
-    less_number_of_int_code [symmetric, of Int.Min]
-    less_number_of_int_code [symmetric, of "Int.Bit0 k1"]
-    less_number_of_int_code [symmetric, of "Int.Bit1 k1"]
-    less_number_of_int_code [symmetric, of "Int.Bit0 k2"]
-    less_number_of_int_code [symmetric, of "Int.Bit1 k2"]
-  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
-    (auto simp add: neg_def group_simps zle_add1_eq_le [symmetric] del: iffI,
-      auto simp only: Bit0_def Bit1_def)
+  by simp_all
 
 definition
   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where