(*  Title:      Int.thy

    ID:         $Id$

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

                Tobias Nipkow, Florian Haftmann, TU Muenchen

    Copyright   1994  University of Cambridge

*)

header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 

theory Int

imports Equiv_Relations Wellfounded_Relations Datatype Nat

uses

  ("Tools/numeral.ML")

  ("Tools/numeral_syntax.ML")

  ("~~/src/Provers/Arith/assoc_fold.ML")

  "~~/src/Provers/Arith/cancel_numerals.ML"

  "~~/src/Provers/Arith/combine_numerals.ML"

  ("int_arith1.ML")

begin

subsection {* The equivalence relation underlying the integers *}

definition

  intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"

where

  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"

typedef (Integ)

  int = "UNIV//intrel"

  by (auto simp add: quotient_def)

instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"

begin

definition

  Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"

definition

  One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"

definition

  add_int_def [code func del]: "z + w = Abs_Integ

    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.

      intrel `` {(x + u, y + v)})"

definition

  minus_int_def [code func del]:

    "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"

definition

  diff_int_def [code func del]:  "z - w = z + (-w \<Colon> int)"

definition

  mult_int_def [code func del]: "z * w = Abs_Integ

    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.

      intrel `` {(x*u + y*v, x*v + y*u)})"

definition

  le_int_def [code func del]:

   "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"

definition

  less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"

definition

  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"

definition

  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"

instance ..

end

subsection{*Construction of the Integers*}

lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"

by (simp add: intrel_def)

lemma equiv_intrel: "equiv UNIV intrel"

by (simp add: intrel_def equiv_def refl_def sym_def trans_def)

text{*Reduces equality of equivalence classes to the @{term intrel} relation:

  @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}

lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]

text{*All equivalence classes belong to set of representatives*}

lemma [simp]: "intrel``{(x,y)} \<in> Integ"

by (auto simp add: Integ_def intrel_def quotient_def)

text{*Reduces equality on abstractions to equality on representatives:

  @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}

declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]

text{*Case analysis on the representation of an integer as an equivalence

      class of pairs of naturals.*}

lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:

     "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"

apply (rule Abs_Integ_cases [of z]) 

apply (auto simp add: Integ_def quotient_def) 

done

subsection {* Arithmetic Operations *}

lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"

proof -

  have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"

    by (simp add: congruent_def) 

  thus ?thesis

    by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])

qed

lemma add:

     "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =

      Abs_Integ (intrel``{(x+u, y+v)})"

proof -

  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 

        respects2 intrel"

    by (simp add: congruent2_def)

  thus ?thesis

    by (simp add: add_int_def UN_UN_split_split_eq

                  UN_equiv_class2 [OF equiv_intrel equiv_intrel])

qed

text{*Congruence property for multiplication*}

lemma mult_congruent2:

     "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)

      respects2 intrel"

apply (rule equiv_intrel [THEN congruent2_commuteI])

 apply (force simp add: mult_ac, clarify) 

apply (simp add: congruent_def mult_ac)  

apply (rename_tac u v w x y z)

apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")

apply (simp add: mult_ac)

apply (simp add: add_mult_distrib [symmetric])

done

lemma mult:

     "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =

      Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"

by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2

              UN_equiv_class2 [OF equiv_intrel equiv_intrel])

text{*The integers form a @{text comm_ring_1}*}

instance int :: comm_ring_1

proof

  fix i j k :: int

  show "(i + j) + k = i + (j + k)"

    by (cases i, cases j, cases k) (simp add: add add_assoc)

  show "i + j = j + i" 

    by (cases i, cases j) (simp add: add_ac add)

  show "0 + i = i"

    by (cases i) (simp add: Zero_int_def add)

  show "- i + i = 0"

    by (cases i) (simp add: Zero_int_def minus add)

  show "i - j = i + - j"

    by (simp add: diff_int_def)

  show "(i * j) * k = i * (j * k)"

    by (cases i, cases j, cases k) (simp add: mult ring_simps)

  show "i * j = j * i"

    by (cases i, cases j) (simp add: mult ring_simps)

  show "1 * i = i"

    by (cases i) (simp add: One_int_def mult)

  show "(i + j) * k = i * k + j * k"

    by (cases i, cases j, cases k) (simp add: add mult ring_simps)

  show "0 \<noteq> (1::int)"

    by (simp add: Zero_int_def One_int_def)

qed

lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"

by (induct m, simp_all add: Zero_int_def One_int_def add)

subsection {* The @{text "\<le>"} Ordering *}

lemma le:

  "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"

by (force simp add: le_int_def)

lemma less:

  "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"

by (simp add: less_int_def le order_less_le)

instance int :: linorder

proof

  fix i j k :: int

  show "(i < j) = (i \<le> j \<and> i \<noteq> j)"

    by (simp add: less_int_def)

  show "i \<le> i"

    by (cases i) (simp add: le)

  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"

    by (cases i, cases j, cases k) (simp add: le)

  show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"

    by (cases i, cases j) (simp add: le)

  show "i \<le> j \<or> j \<le> i"

    by (cases i, cases j) (simp add: le linorder_linear)

qed

instantiation int :: distrib_lattice

begin

definition

  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"

definition

  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"

instance

  by intro_classes

    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)

end

instance int :: pordered_cancel_ab_semigroup_add

proof

  fix i j k :: int

  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"

    by (cases i, cases j, cases k) (simp add: le add)

qed

text{*Strict Monotonicity of Multiplication*}

text{*strict, in 1st argument; proof is by induction on k>0*}

lemma zmult_zless_mono2_lemma:

     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"

apply (induct "k", simp)

apply (simp add: left_distrib)

apply (case_tac "k=0")

apply (simp_all add: add_strict_mono)

done

lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"

apply (cases k)

apply (auto simp add: le add int_def Zero_int_def)

apply (rule_tac x="x-y" in exI, simp)

done

lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"

apply (cases k)

apply (simp add: less int_def Zero_int_def)

apply (rule_tac x="x-y" in exI, simp)

done

lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"

apply (drule zero_less_imp_eq_int)

apply (auto simp add: zmult_zless_mono2_lemma)

done

text{*The integers form an ordered integral domain*}

instance int :: ordered_idom

proof

  fix i j k :: int

  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"

    by (rule zmult_zless_mono2)

  show "\<bar>i\<bar> = (if i < 0 then -i else i)"

    by (simp only: zabs_def)

  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"

    by (simp only: zsgn_def)

qed

lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"

apply (cases w, cases z) 

apply (simp add: less le add One_int_def)

done

lemma zless_iff_Suc_zadd:

  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"

apply (cases z, cases w)

apply (auto simp add: less add int_def)

apply (rename_tac a b c d) 

apply (rule_tac x="a+d - Suc(c+b)" in exI) 

apply arith

done

lemmas int_distrib =

  left_distrib [of "z1::int" "z2" "w", standard]

  right_distrib [of "w::int" "z1" "z2", standard]

  left_diff_distrib [of "z1::int" "z2" "w", standard]

  right_diff_distrib [of "w::int" "z1" "z2", standard]

subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}

context ring_1

begin

definition

  of_int :: "int \<Rightarrow> 'a"

where

  [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"

lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"

proof -

  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"

    by (simp add: congruent_def compare_rls of_nat_add [symmetric]

            del: of_nat_add) 

  thus ?thesis

    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])

qed

lemma of_int_0 [simp]: "of_int 0 = 0"

  by (simp add: of_int Zero_int_def)

lemma of_int_1 [simp]: "of_int 1 = 1"

  by (simp add: of_int One_int_def)

lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"

  by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add)

lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"

  by (cases z, simp add: compare_rls of_int minus)

lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"

  by (simp add: OrderedGroup.diff_minus diff_minus)

lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"

apply (cases w, cases z)

apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib

                 mult add_ac of_nat_mult)

done

text{*Collapse nested embeddings*}

lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"

  by (induct n) auto

end

context ordered_idom

begin

lemma of_int_le_iff [simp]:

  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"

  by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add)

text{*Special cases where either operand is zero*}

lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]

lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]

lemma of_int_less_iff [simp]:

  "of_int w < of_int z \<longleftrightarrow> w < z"

  by (simp add: not_le [symmetric] linorder_not_le [symmetric])

text{*Special cases where either operand is zero*}

lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]

lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]

end

text{*Class for unital rings with characteristic zero.

 Includes non-ordered rings like the complex numbers.*}

class ring_char_0 = ring_1 + semiring_char_0

begin

lemma of_int_eq_iff [simp]:

   "of_int w = of_int z \<longleftrightarrow> w = z"

apply (cases w, cases z, simp add: of_int)

apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)

apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)

done

text{*Special cases where either operand is zero*}

lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]

lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]

end

text{*Every @{text ordered_idom} has characteristic zero.*}

subclass (in ordered_idom) ring_char_0 by intro_locales

lemma of_int_eq_id [simp]: "of_int = id"

proof

  fix z show "of_int z = id z"

    by (cases z) (simp add: of_int add minus int_def diff_minus)

qed

subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}

definition

  nat :: "int \<Rightarrow> nat"

where

  [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"

lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"

proof -

  have "(\<lambda>(x,y). {x-y}) respects intrel"

    by (simp add: congruent_def) arith

  thus ?thesis

    by (simp add: nat_def UN_equiv_class [OF equiv_intrel])

qed

lemma nat_int [simp]: "nat (of_nat n) = n"

by (simp add: nat int_def)

lemma nat_zero [simp]: "nat 0 = 0"

by (simp add: Zero_int_def nat)

lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"

by (cases z, simp add: nat le int_def Zero_int_def)

corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"

by simp

lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"

by (cases z, simp add: nat le Zero_int_def)

lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"

apply (cases w, cases z) 

apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)

done

text{*An alternative condition is @{term "0 \<le> w"} *}

corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"

by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 

corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"

by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 

lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"

apply (cases w, cases z) 

apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)

done

lemma nonneg_eq_int:

  fixes z :: int

  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"

  shows P

  using assms by (blast dest: nat_0_le sym)

lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"

by (cases w, simp add: nat le int_def Zero_int_def, arith)

corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"

by (simp only: eq_commute [of m] nat_eq_iff)

lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"

apply (cases w)

apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)

done

lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"

by (auto simp add: nat_eq_iff2)

lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"

by (insert zless_nat_conj [of 0], auto)

lemma nat_add_distrib:

     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"

by (cases z, cases z', simp add: nat add le Zero_int_def)

lemma nat_diff_distrib:

     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"

by (cases z, cases z', 

    simp add: nat add minus diff_minus le Zero_int_def)

lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"

by (simp add: int_def minus nat Zero_int_def) 

lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"

by (cases z, simp add: nat less int_def, arith)

context ring_1

begin

lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"

  by (cases z rule: eq_Abs_Integ)

   (simp add: nat le of_int Zero_int_def of_nat_diff)

end

subsection{*Lemmas about the Function @{term of_nat} and Orderings*}

lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"

by (simp add: order_less_le del: of_nat_Suc)

lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"

by (rule negative_zless_0 [THEN order_less_le_trans], simp)

lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"

by (simp add: minus_le_iff)

lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"

by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])

lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"

by (subst le_minus_iff, simp del: of_nat_Suc)

lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"

by (simp add: int_def le minus Zero_int_def)

lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"

by (simp add: linorder_not_less)

lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"

by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)

lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"

proof -

  have "(w \<le> z) = (0 \<le> z - w)"

    by (simp only: le_diff_eq add_0_left)

  also have "\<dots> = (\<exists>n. z - w = of_nat n)"

    by (auto elim: zero_le_imp_eq_int)

  also have "\<dots> = (\<exists>n. z = w + of_nat n)"

    by (simp only: group_simps)

  finally show ?thesis .

qed

lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"

by simp

lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"

by simp

text{*This version is proved for all ordered rings, not just integers!

      It is proved here because attribute @{text arith_split} is not available

      in theory @{text Ring_and_Field}.

      But is it really better than just rewriting with @{text abs_if}?*}

lemma abs_split [arith_split,noatp]:

     "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"

by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)

lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"

apply (cases x)

apply (auto simp add: le minus Zero_int_def int_def order_less_le)

apply (rule_tac x="y - Suc x" in exI, arith)

done

subsection {* Cases and induction *}

text{*Now we replace the case analysis rule by a more conventional one:

whether an integer is negative or not.*}

theorem int_cases [cases type: int, case_names nonneg neg]:

  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"

apply (cases "z < 0", blast dest!: negD)

apply (simp add: linorder_not_less del: of_nat_Suc)

apply auto

apply (blast dest: nat_0_le [THEN sym])

done

theorem int_induct [induct type: int, case_names nonneg neg]:

     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"

  by (cases z rule: int_cases) auto

text{*Contributed by Brian Huffman*}

theorem int_diff_cases:

  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"

apply (cases z rule: eq_Abs_Integ)

apply (rule_tac m=x and n=y in diff)

apply (simp add: int_def diff_def minus add)

done

subsection {* Binary representation *}

text {*

  This formalization defines binary arithmetic in terms of the integers

  rather than using a datatype. This avoids multiple representations (leading

  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text

  int_of_binary}, for the numerical interpretation.

  The representation expects that @{text "(m mod 2)"} is 0 or 1,

  even if m is negative;

  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus

  @{text "-5 = (-3)*2 + 1"}.

  This two's complement binary representation derives from the paper 

  "An Efficient Representation of Arithmetic for Term Rewriting" by

  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,

  Springer LNCS 488 (240-251), 1991.

*}

datatype bit = B0 | B1

text{*

  Type @{typ bit} avoids the use of type @{typ bool}, which would make

  all of the rewrite rules higher-order.

*}

definition

  Pls :: int where

  [code func del]: "Pls = 0"

definition

  Min :: int where

  [code func del]: "Min = - 1"

definition

  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where

  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"

class number = type + -- {* for numeric types: nat, int, real, \dots *}

  fixes number_of :: "int \<Rightarrow> 'a"

use "Tools/numeral.ML"

syntax

  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

use "Tools/numeral_syntax.ML"

setup NumeralSyntax.setup

abbreviation

  "Numeral0 \<equiv> number_of Pls"

abbreviation

  "Numeral1 \<equiv> number_of (Pls BIT B1)"

lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"

  -- {* Unfold all @{text let}s involving constants *}

  unfolding Let_def ..

definition

  succ :: "int \<Rightarrow> int" where

  [code func del]: "succ k = k + 1"

definition

  pred :: "int \<Rightarrow> int" where

  [code func del]: "pred k = k - 1"

lemmas

  max_number_of [simp] = max_def

    [of "number_of u" "number_of v", standard, simp]

and

  min_number_of [simp] = min_def 

    [of "number_of u" "number_of v", standard, simp]

  -- {* unfolding @{text minx} and @{text max} on numerals *}

lemmas numeral_simps = 

  succ_def pred_def Pls_def Min_def Bit_def

text {* Removal of leading zeroes *}

lemma Pls_0_eq [simp, code post]:

  "Pls BIT B0 = Pls"

  unfolding numeral_simps by simp

lemma Min_1_eq [simp, code post]:

  "Min BIT B1 = Min"

  unfolding numeral_simps by simp

subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}

lemma succ_Pls [simp]:

  "succ Pls = Pls BIT B1"

  unfolding numeral_simps by simp

lemma succ_Min [simp]:

  "succ Min = Pls"

  unfolding numeral_simps by simp

lemma succ_1 [simp]:

  "succ (k BIT B1) = succ k BIT B0"

  unfolding numeral_simps by simp

lemma succ_0 [simp]:

  "succ (k BIT B0) = k BIT B1"

  unfolding numeral_simps by simp

lemma pred_Pls [simp]:

  "pred Pls = Min"

  unfolding numeral_simps by simp

lemma pred_Min [simp]:

  "pred Min = Min BIT B0"

  unfolding numeral_simps by simp

lemma pred_1 [simp]:

  "pred (k BIT B1) = k BIT B0"

  unfolding numeral_simps by simp

lemma pred_0 [simp]:

  "pred (k BIT B0) = pred k BIT B1"

  unfolding numeral_simps by simp 

lemma minus_Pls [simp]:

  "- Pls = Pls"

  unfolding numeral_simps by simp 

lemma minus_Min [simp]:

  "- Min = Pls BIT B1"

  unfolding numeral_simps by simp 

lemma minus_1 [simp]:

  "- (k BIT B1) = pred (- k) BIT B1"

  unfolding numeral_simps by simp 

lemma minus_0 [simp]:

  "- (k BIT B0) = (- k) BIT B0"

  unfolding numeral_simps by simp 

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"

  unfolding numeral_simps by simp

lemma add_BIT_11 [simp]:

  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"

  unfolding numeral_simps by simp

lemma add_BIT_10 [simp]:

  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"

  unfolding numeral_simps by simp

lemma add_BIT_0 [simp]:

  "(k BIT B0) + (l BIT b) = (k + l) BIT b"

  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"

  unfolding numeral_simps by simp 

lemma mult_Pls [simp]:

  "Pls * w = Pls"

  unfolding numeral_simps by simp 

lemma mult_Min [simp]:

  "Min * k = - k"

  unfolding numeral_simps by simp

lemma mult_num1 [simp]:

  "(k BIT B1) * l = ((k * l) BIT B0) + l"

  unfolding numeral_simps int_distrib by simp 

lemma mult_num0 [simp]:

  "(k BIT B0) * l = (k * l) BIT B0"

  unfolding numeral_simps int_distrib by simp 

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

class number_ring = number + comm_ring_1 +

  assumes number_of_eq: "number_of k = of_int k"

text {* self-embedding of the integers *}

instantiation int :: number_ring

begin

definition

  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"

instance

  by intro_classes (simp only: int_number_of_def)

end

lemma number_of_is_id:

  "number_of (k::int) = k"

  unfolding int_number_of_def by simp

lemma number_of_succ:

  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma number_of_pred:

  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma number_of_minus:

  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

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

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

text {*

  The correctness of shifting.

  But it doesn't seem to give a measurable speed-up.

*}

lemma double_number_of_BIT:

  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"

  unfolding number_of_eq numeral_simps left_distrib by simp

text {*

  Converting numerals 0 and 1 to their abstract versions.

*}

lemma numeral_0_eq_0 [simp]:

  "Numeral0 = (0::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma numeral_1_eq_1 [simp]:

  "Numeral1 = (1::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

text {*

  Special-case simplification for small constants.

*}

text{*

  Unary minus for the abstract constant 1. Cannot be inserted

  as a simprule until later: it is @{text number_of_Min} re-oriented!

*}

lemma numeral_m1_eq_minus_1:

  "(-1::'a::number_ring) = - 1"

  unfolding number_of_eq numeral_simps by simp

lemma mult_minus1 [simp]:

  "-1 * z = -(z::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma mult_minus1_right [simp]:

  "z * -1 = -(z::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

(*Negation of a coefficient*)

lemma minus_number_of_mult [simp]:

   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"

   unfolding number_of_eq by simp

text {* Subtraction *}

lemma diff_number_of_eq:

  "number_of v - number_of w =

    (number_of (v + uminus w)::'a::number_ring)"

  unfolding number_of_eq by simp

lemma number_of_Pls:

  "number_of Pls = (0::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma number_of_Min:

  "number_of Min = (- 1::'a::number_ring)"

  unfolding number_of_eq numeral_simps by simp

lemma number_of_BIT:

  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))

    + (number_of w) + (number_of w)"

  unfolding number_of_eq numeral_simps by (simp split: bit.split)

subsection {* Equality of Binary Numbers *}

text {* First version by Norbert Voelker *}

definition

  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"

where

  "neg Z \<longleftrightarrow> Z < 0"

definition (*for simplifying equalities*)

  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"

where

  "iszero z \<longleftrightarrow> z = 0"

lemma not_neg_int [simp]: "~ neg (of_nat n)"

by (simp add: neg_def)

lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"

by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)

lemmas neg_eq_less_0 = neg_def

lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"

by (simp add: neg_def linorder_not_less)

text{*To simplify inequalities when Numeral1 can get simplified to 1*}

lemma not_neg_0: "~ neg 0"

by (simp add: One_int_def neg_def)

lemma not_neg_1: "~ neg 1"

by (simp add: neg_def linorder_not_less zero_le_one)

lemma iszero_0: "iszero 0"

by (simp add: iszero_def)

lemma not_iszero_1: "~ iszero 1"

by (simp add: iszero_def eq_commute)

lemma neg_nat: "neg z ==> nat z = 0"

by (simp add: neg_def order_less_imp_le) 

lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"

by (simp add: linorder_not_less neg_def)

lemma eq_number_of_eq:

  "((number_of x::'a::number_ring) = number_of y) =

   iszero (number_of (x + uminus y) :: 'a)"

  unfolding iszero_def number_of_add number_of_minus

  by (simp add: compare_rls)

lemma iszero_number_of_Pls:

  "iszero ((number_of Pls)::'a::number_ring)"

  unfolding iszero_def numeral_0_eq_0 ..

lemma nonzero_number_of_Min:

  "~ iszero ((number_of Min)::'a::number_ring)"

  unfolding iszero_def numeral_m1_eq_minus_1 by simp

subsection {* 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)

  case (nonneg n)

  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 

  thus ?thesis using  le_imp_0_less [OF le]

    by (auto simp add: add_assoc) 

next

  case (neg n)

  show ?thesis

  proof

    assume eq: "1 + z + z = 0"

    have "(0::int) < 1 + (of_nat n + of_nat n)"

      by (simp add: le_imp_0_less add_increasing) 

    also have "... = - (1 + z + z)" 

      by (simp add: neg add_assoc [symmetric]) 

    also have "... = 0" by (simp add: eq) 

    finally have "0<0" ..

    thus False by blast

  qed

qed

lemma iszero_number_of_BIT:

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

   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"

proof -

  have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"

  proof -

    assume eq: "of_int w + of_int w = (0::'a)"

    then have "of_int (w + w) = (of_int 0 :: 'a)" by simp

    then have "w + w = 0" by (simp only: of_int_eq_iff)

    then show "w = 0" by (simp only: double_eq_0_iff)

  qed

  moreover have "1 + of_int w + of_int w \<noteq> (0::'a)"

  proof

    assume eq: "1 + of_int w + of_int w = (0::'a)"

    hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 

    hence "1 + w + w = 0" by (simp only: of_int_eq_iff)

    with odd_nonzero show False by blast

  qed

  ultimately show ?thesis

    by (auto simp add: iszero_def number_of_eq numeral_simps 

     split: bit.split)

qed

lemma iszero_number_of_0:

  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 

  iszero (number_of w :: 'a)"

  by (simp only: iszero_number_of_BIT simp_thms)

lemma iszero_number_of_1:

  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"

  by (simp add: iszero_number_of_BIT) 

subsection {* The Less-Than Relation *}

lemma less_number_of_eq_neg:

  "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)

  = neg (number_of (x + uminus y) :: 'a)"

apply (subst less_iff_diff_less_0)