# Theory IntArith

Up to index of Isabelle/ZF

theory IntArith
imports Bin
`theory IntArith imports Binbegin(** To simplify inequalities involving integer negation and literals,    such as -x = #3**)lemmas [simp] =  zminus_equation [where y = "integ_of(w)"]  equation_zminus [where x = "integ_of(w)"]  for wlemmas [iff] =  zminus_zless [where y = "integ_of(w)"]  zless_zminus [where x = "integ_of(w)"]  for wlemmas [iff] =  zminus_zle [where y = "integ_of(w)"]  zle_zminus [where x = "integ_of(w)"]  for wlemmas [simp] =  Let_def [where s = "integ_of(w)"] for w(*** Simprocs for numeric literals ***)(** Combining of literal coefficients in sums of products **)lemma zless_iff_zdiff_zless_0: "(x \$< y) <-> (x\$-y \$< #0)"  by (simp add: zcompare_rls)lemma eq_iff_zdiff_eq_0: "[| x ∈ int; y ∈ int |] ==> (x = y) <-> (x\$-y = #0)"  by (simp add: zcompare_rls)lemma zle_iff_zdiff_zle_0: "(x \$<= y) <-> (x\$-y \$<= #0)"  by (simp add: zcompare_rls)(** For combine_numerals **)lemma left_zadd_zmult_distrib: "i\$*u \$+ (j\$*u \$+ k) = (i\$+j)\$*u \$+ k"  by (simp add: zadd_zmult_distrib zadd_ac)(** For cancel_numerals **)lemmas rel_iff_rel_0_rls =  zless_iff_zdiff_zless_0 [where y = "u \$+ v"]  eq_iff_zdiff_eq_0 [where y = "u \$+ v"]  zle_iff_zdiff_zle_0 [where y = "u \$+ v"]  zless_iff_zdiff_zless_0 [where y = n]  eq_iff_zdiff_eq_0 [where y = n]  zle_iff_zdiff_zle_0 [where y = n]  for u v (* FIXME n (!?) *)lemma eq_add_iff1: "(i\$*u \$+ m = j\$*u \$+ n) <-> ((i\$-j)\$*u \$+ m = intify(n))"  apply (simp add: zdiff_def zadd_zmult_distrib)  apply (simp add: zcompare_rls)  apply (simp add: zadd_ac)  donelemma eq_add_iff2: "(i\$*u \$+ m = j\$*u \$+ n) <-> (intify(m) = (j\$-i)\$*u \$+ n)"  apply (simp add: zdiff_def zadd_zmult_distrib)  apply (simp add: zcompare_rls)  apply (simp add: zadd_ac)  donelemma less_add_iff1: "(i\$*u \$+ m \$< j\$*u \$+ n) <-> ((i\$-j)\$*u \$+ m \$< n)"  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)  donelemma less_add_iff2: "(i\$*u \$+ m \$< j\$*u \$+ n) <-> (m \$< (j\$-i)\$*u \$+ n)"  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)  donelemma le_add_iff1: "(i\$*u \$+ m \$<= j\$*u \$+ n) <-> ((i\$-j)\$*u \$+ m \$<= n)"  apply (simp add: zdiff_def zadd_zmult_distrib)  apply (simp add: zcompare_rls)  apply (simp add: zadd_ac)  donelemma le_add_iff2: "(i\$*u \$+ m \$<= j\$*u \$+ n) <-> (m \$<= (j\$-i)\$*u \$+ n)"  apply (simp add: zdiff_def zadd_zmult_distrib)  apply (simp add: zcompare_rls)  apply (simp add: zadd_ac)  doneML_file "int_arith.ML"end`