header{*Arithmetic on Binary Integers*}

 header{*Arithmetic on Binary Integers*}

 theory Bin = IntDef + Numeral:

 theory Bin = IntDef + Numeral:

   number_of_Pls: "number_of bin.Pls = 0"

   number_of_Pls: "number_of bin.Pls = 0"

   number_of_Min: "number_of bin.Min = - 1"

   number_of_Min: "number_of bin.Min = - 1"

   number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +

   number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +

 	                               (number_of w) + (number_of w)"

 	                               (number_of w) + (number_of w)"

 subsection{*Converting Numerals to Rings: @{term number_of}*}

 subsection{*Converting Numerals to Rings: @{term number_of}*}

 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)

 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)

 subsection{*Comparisons, for Ordered Rings*}

 subsection{*Comparisons, for Ordered Rings*}

 proof -

 proof -

   have "a + a = (1+1)*a" by (simp add: left_distrib)

   have "a + a = (1+1)*a" by (simp add: left_distrib)

   with zero_less_two [where 'a = 'a]

   with zero_less_two [where 'a = 'a]

   show ?thesis by force

   show ?thesis by force

 qed

 qed

   qed

   qed

 qed

 qed

 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}

 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}

 proof (unfold Ints_def) 

 proof (unfold Ints_def) 

   assume "a \<in> range of_int"

   assume "a \<in> range of_int"

   then obtain z where a: "a = of_int z" ..

   then obtain z where a: "a = of_int z" ..

   show ?thesis

   show ?thesis

   proof

   proof

 lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"

 lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"

 by (induct_tac "w", simp_all add: number_of)

 by (induct_tac "w", simp_all add: number_of)

 lemma iszero_number_of_BIT:

 lemma iszero_number_of_BIT:

      "iszero (number_of (w BIT x)::'a) = 

      "iszero (number_of (w BIT x)::'a) = 

 by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff 

 by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff 

               number_of Ints_odd_nonzero [OF Ints_number_of])

               number_of Ints_odd_nonzero [OF Ints_number_of])

 lemma iszero_number_of_0:

 lemma iszero_number_of_0:

       iszero (number_of w :: 'a)"

       iszero (number_of w :: 'a)"

 by (simp only: iszero_number_of_BIT simp_thms)

 by (simp only: iszero_number_of_BIT simp_thms)

 lemma iszero_number_of_1:

 lemma iszero_number_of_1:

 by (simp only: iszero_number_of_BIT simp_thms)

 by (simp only: iszero_number_of_BIT simp_thms)

 subsection{*The Less-Than Relation*}

 subsection{*The Less-Than Relation*}

 lemma less_number_of_eq_neg:

 lemma less_number_of_eq_neg:

      = neg (number_of (bin_add x (bin_minus y)) :: 'a)"

      = neg (number_of (bin_add x (bin_minus y)) :: 'a)"

 apply (subst less_iff_diff_less_0) 

 apply (subst less_iff_diff_less_0) 

 apply (simp add: neg_def diff_minus number_of_add number_of_minus)

 apply (simp add: neg_def diff_minus number_of_add number_of_minus)

 done

 done

 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:

 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:

   @{term Numeral0} IS @{term "number_of Pls"} *}

   @{term Numeral0} IS @{term "number_of Pls"} *}

 lemma not_neg_number_of_Pls:

 lemma not_neg_number_of_Pls:

 by (simp add: neg_def numeral_0_eq_0)

 by (simp add: neg_def numeral_0_eq_0)

 lemma neg_number_of_Min:

 lemma neg_number_of_Min:

 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)

 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)

 proof -

 proof -

   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)

   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)

   also have "... = (a < 0)"

   also have "... = (a < 0)"

     by (simp add: mult_less_0_iff zero_less_two 

     by (simp add: mult_less_0_iff zero_less_two 

                   order_less_not_sym [OF zero_less_two]) 

                   order_less_not_sym [OF zero_less_two]) 

 			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)

 			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)

 qed

 qed

 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}

 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}

 lemma Ints_odd_less_0: 

 lemma Ints_odd_less_0: 

 proof (unfold Ints_def) 

 proof (unfold Ints_def) 

   assume "a \<in> range of_int"

   assume "a \<in> range of_int"

   then obtain z where a: "a = of_int z" ..

   then obtain z where a: "a = of_int z" ..

   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"

   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"

     by (simp add: a)

     by (simp add: a)

   finally show ?thesis .

   finally show ?thesis .

 qed

 qed

 lemma neg_number_of_BIT:

 lemma neg_number_of_BIT:

      "neg (number_of (w BIT x)::'a) = 

      "neg (number_of (w BIT x)::'a) = 

 by (simp add: number_of neg_def double_less_0_iff

 by (simp add: number_of neg_def double_less_0_iff

               Ints_odd_less_0 [OF Ints_number_of])

               Ints_odd_less_0 [OF Ints_number_of])

 text{*Less-Than or Equals*}

 text{*Less-Than or Equals*}

 lemmas le_number_of_eq_not_less =

 lemmas le_number_of_eq_not_less =

        linorder_not_less [of "number_of w" "number_of v", symmetric, 

        linorder_not_less [of "number_of w" "number_of v", symmetric, 

                           standard]

                           standard]

 lemma le_number_of_eq:

 lemma le_number_of_eq:

      = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"

      = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"

 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)

 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)

 text{*Absolute value (@{term abs})*}

 text{*Absolute value (@{term abs})*}

 lemma abs_number_of:

 lemma abs_number_of:

       (if number_of x < (0::'a) then -number_of x else number_of x)"

       (if number_of x < (0::'a) then -number_of x else number_of x)"

 by (simp add: abs_if)

 by (simp add: abs_if)

 text{*Re-orientation of the equation nnn=x*}

 text{*Re-orientation of the equation nnn=x*}