(* Title: ZF/IntDiv.thy ID: $Id: IntDiv.thy,v 1.12 2005/06/17 14:15:11 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge Here is the division algorithm in ML: fun posDivAlg (a,b) = if a<b then (0,a) else let val (q,r) = posDivAlg(a, 2*b) in if 0<=r-b then (2*q+1, r-b) else (2*q, r) end fun negDivAlg (a,b) = if 0<=a+b then (~1,a+b) else let val (q,r) = negDivAlg(a, 2*b) in if 0<=r-b then (2*q+1, r-b) else (2*q, r) end; fun negateSnd (q,r:int) = (q,~r); fun divAlg (a,b) = if 0<=a then if b>0 then posDivAlg (a,b) else if a=0 then (0,0) else negateSnd (negDivAlg (~a,~b)) else if 0<b then negDivAlg (a,b) else negateSnd (posDivAlg (~a,~b)); *) header{*The Division Operators Div and Mod*} theory IntDiv imports IntArith OrderArith begin constdefs quorem :: "[i,i] => o" "quorem == %<a,b> <q,r>. a = b$*q $+ r & (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)" adjust :: "[i,i] => i" "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b> else <#2$*q,r>" (** the division algorithm **) constdefs posDivAlg :: "i => i" (*for the case a>=0, b>0*) (*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*) "posDivAlg(ab) == wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)), ab, %<a,b> f. if (a$<b | b$<=#0) then <#0,a> else adjust(b, f ` <a,#2$*b>))" (*for the case a<0, b>0*) constdefs negDivAlg :: "i => i" (*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*) "negDivAlg(ab) == wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)), ab, %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b> else adjust(b, f ` <a,#2$*b>))" (*for the general case b≠0*) constdefs negateSnd :: "i => i" "negateSnd == %<q,r>. <q, $-r>" (*The full division algorithm considers all possible signs for a, b including the special case a=0, b<0, because negDivAlg requires a<0*) divAlg :: "i => i" "divAlg == %<a,b>. if #0 $<= a then if #0 $<= b then posDivAlg (<a,b>) else if a=#0 then <#0,#0> else negateSnd (negDivAlg (<$-a,$-b>)) else if #0$<b then negDivAlg (<a,b>) else negateSnd (posDivAlg (<$-a,$-b>))" zdiv :: "[i,i]=>i" (infixl "zdiv" 70) "a zdiv b == fst (divAlg (<intify(a), intify(b)>))" zmod :: "[i,i]=>i" (infixl "zmod" 70) "a zmod b == snd (divAlg (<intify(a), intify(b)>))" (** Some basic laws by Sidi Ehmety (need linear arithmetic!) **) lemma zspos_add_zspos_imp_zspos: "[| #0 $< x; #0 $< y |] ==> #0 $< x $+ y" apply (rule_tac y = "y" in zless_trans) apply (rule_tac [2] zdiff_zless_iff [THEN iffD1]) apply auto done lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x; #0 $<= y |] ==> #0 $<= x $+ y" apply (rule_tac y = "y" in zle_trans) apply (rule_tac [2] zdiff_zle_iff [THEN iffD1]) apply auto done lemma zneg_add_zneg_imp_zneg: "[| x $< #0; y $< #0 |] ==> x $+ y $< #0" apply (rule_tac y = "y" in zless_trans) apply (rule zless_zdiff_iff [THEN iffD1]) apply auto done (* this theorem is used below *) lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0: "[| x $<= #0; y $<= #0 |] ==> x $+ y $<= #0" apply (rule_tac y = "y" in zle_trans) apply (rule zle_zdiff_iff [THEN iffD1]) apply auto done lemma zero_lt_zmagnitude: "[| #0 $< k; k ∈ int |] ==> 0 < zmagnitude(k)" apply (drule zero_zless_imp_znegative_zminus) apply (drule_tac [2] zneg_int_of) apply (auto simp add: zminus_equation [of k]) apply (subgoal_tac "0 < zmagnitude ($# succ (n))") apply simp apply (simp only: zmagnitude_int_of) apply simp done (*** Inequality lemmas involving $#succ(m) ***) lemma zless_add_succ_iff: "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)" apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric]) apply (rule_tac [3] x = "0" in bexI) apply (cut_tac m = "m" in int_succ_int_1) apply (cut_tac m = "n" in int_succ_int_1) apply simp apply (erule natE) apply auto apply (rule_tac x = "succ (n) " in bexI) apply auto done lemma zadd_succ_lemma: "z ∈ int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)" apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff) apply (auto intro: zle_anti_sym elim: zless_asym simp add: zless_imp_zle not_zless_iff_zle) done lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)" apply (cut_tac z = "intify (z)" in zadd_succ_lemma) apply auto done (** Inequality reasoning **) lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)" apply (subgoal_tac "#1 = $# 1") apply (simp only: zless_add_succ_iff zle_def) apply auto done lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)" apply (subgoal_tac "#1 = $# 1") apply (simp only: zadd_succ_zle_iff) apply auto done lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)" apply (subst zadd_commute) apply (rule add1_zle_iff) done (*** Monotonicity of Multiplication ***) lemma zmult_mono_lemma: "k ∈ nat ==> i $<= j ==> i $* $#k $<= j $* $#k" apply (induct_tac "k") prefer 2 apply (subst int_succ_int_1) apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono) done lemma zmult_zle_mono1: "[| i $<= j; #0 $<= k |] ==> i$*k $<= j$*k" apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ") apply (simp (no_asm_use)) apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst]) apply (rule_tac [3] zmult_mono_lemma) apply auto apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym]) done lemma zmult_zle_mono1_neg: "[| i $<= j; k $<= #0 |] ==> j$*k $<= i$*k" apply (rule zminus_zle_zminus [THEN iffD1]) apply (simp del: zmult_zminus_right add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus) done lemma zmult_zle_mono2: "[| i $<= j; #0 $<= k |] ==> k$*i $<= k$*j" apply (drule zmult_zle_mono1) apply (simp_all add: zmult_commute) done lemma zmult_zle_mono2_neg: "[| i $<= j; k $<= #0 |] ==> k$*j $<= k$*i" apply (drule zmult_zle_mono1_neg) apply (simp_all add: zmult_commute) done (* $<= monotonicity, BOTH arguments*) lemma zmult_zle_mono: "[| i $<= j; k $<= l; #0 $<= j; #0 $<= k |] ==> i$*k $<= j$*l" apply (erule zmult_zle_mono1 [THEN zle_trans]) apply assumption apply (erule zmult_zle_mono2) apply assumption done (** strict, in 1st argument; proof is by induction on k>0 **) lemma zmult_zless_mono2_lemma [rule_format]: "[| i$<j; k ∈ nat |] ==> 0<k --> $#k $* i $< $#k $* j" apply (induct_tac "k") prefer 2 apply (subst int_succ_int_1) apply (erule natE) apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def) apply (frule nat_0_le) apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ") apply (simp (no_asm_use)) apply (rule zadd_zless_mono) apply (simp_all (no_asm_simp) add: zle_def) done lemma zmult_zless_mono2: "[| i$<j; #0 $< k |] ==> k$*i $< k$*j" apply (subgoal_tac "intify (k) $* i $< intify (k) $* j") apply (simp (no_asm_use)) apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst]) apply (rule_tac [3] zmult_zless_mono2_lemma) apply auto apply (simp add: znegative_iff_zless_0) apply (drule zless_trans, assumption) apply (auto simp add: zero_lt_zmagnitude) done lemma zmult_zless_mono1: "[| i$<j; #0 $< k |] ==> i$*k $< j$*k" apply (drule zmult_zless_mono2) apply (simp_all add: zmult_commute) done (* < monotonicity, BOTH arguments*) lemma zmult_zless_mono: "[| i $< j; k $< l; #0 $< j; #0 $< k |] ==> i$*k $< j$*l" apply (erule zmult_zless_mono1 [THEN zless_trans]) apply assumption apply (erule zmult_zless_mono2) apply assumption done lemma zmult_zless_mono1_neg: "[| i $< j; k $< #0 |] ==> j$*k $< i$*k" apply (rule zminus_zless_zminus [THEN iffD1]) apply (simp del: zmult_zminus_right add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus) done lemma zmult_zless_mono2_neg: "[| i $< j; k $< #0 |] ==> k$*j $< k$*i" apply (rule zminus_zless_zminus [THEN iffD1]) apply (simp del: zmult_zminus add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus) done (** Products of zeroes **) lemma zmult_eq_lemma: "[| m ∈ int; n ∈ int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)" apply (case_tac "m $< #0") apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless) apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+ done lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)" apply (simp add: zmult_eq_lemma) done (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, but not (yet?) for k*m < n*k. **) lemma zmult_zless_lemma: "[| k ∈ int; m ∈ int; n ∈ int |] ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" apply (case_tac "k = #0") apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg) apply (auto simp add: not_zless_iff_zle not_zle_iff_zless [THEN iff_sym, of "m$*k"] not_zle_iff_zless [THEN iff_sym, of m]) apply (auto elim: notE simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg) done lemma zmult_zless_cancel2: "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)" in zmult_zless_lemma) apply auto done lemma zmult_zless_cancel1: "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" by (simp add: zmult_commute [of k] zmult_zless_cancel2) lemma zmult_zle_cancel2: "(m$*k $<= n$*k) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))" by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2) lemma zmult_zle_cancel1: "(k$*m $<= k$*n) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))" by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1) lemma int_eq_iff_zle: "[| m ∈ int; n ∈ int |] ==> m=n <-> (m $<= n & n $<= m)" apply (blast intro: zle_refl zle_anti_sym) done lemma zmult_cancel2_lemma: "[| k ∈ int; m ∈ int; n ∈ int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)" apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m]) apply (auto simp add: zmult_zle_cancel2 neq_iff_zless) done lemma zmult_cancel2 [simp]: "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))" apply (rule iff_trans) apply (rule_tac [2] zmult_cancel2_lemma) apply auto done lemma zmult_cancel1 [simp]: "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))" by (simp add: zmult_commute [of k] zmult_cancel2) subsection{* Uniqueness and monotonicity of quotients and remainders *} lemma unique_quotient_lemma: "[| b$*q' $+ r' $<= b$*q $+ r; #0 $<= r'; #0 $< b; r $< b |] ==> q' $<= q" apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r") prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls) apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ") prefer 2 apply (erule zle_zless_trans) apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) apply (erule zle_zless_trans) apply (simp add: ); apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)") prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) apply (auto elim: zless_asym simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls) done lemma unique_quotient_lemma_neg: "[| b$*q' $+ r' $<= b$*q $+ r; r $<= #0; b $< #0; b $< r' |] ==> q $<= q'" apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r" in unique_quotient_lemma) apply (auto simp del: zminus_zadd_distrib simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus) done lemma unique_quotient: "[| quorem (<a,b>, <q,r>); quorem (<a,b>, <q',r'>); b ∈ int; b ~= #0; q ∈ int; q' ∈ int |] ==> q = q'" apply (simp add: split_ifs quorem_def neq_iff_zless) apply safe apply simp_all apply (blast intro: zle_anti_sym dest: zle_eq_refl [THEN unique_quotient_lemma] zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+ done lemma unique_remainder: "[| quorem (<a,b>, <q,r>); quorem (<a,b>, <q',r'>); b ∈ int; b ~= #0; q ∈ int; q' ∈ int; r ∈ int; r' ∈ int |] ==> r = r'" apply (subgoal_tac "q = q'") prefer 2 apply (blast intro: unique_quotient) apply (simp add: quorem_def) done subsection{*Correctness of posDivAlg, the Division Algorithm for @{text "a≥0"} and @{text "b>0"} *} lemma adjust_eq [simp]: "adjust(b, <q,r>) = (let diff = r$-b in if #0 $<= diff then <#2$*q $+ #1,diff> else <#2$*q,r>)" by (simp add: Let_def adjust_def) lemma posDivAlg_termination: "[| #0 $< b; ~ a $< b |] ==> nat_of(a $- #2 $× b $+ #1) < nat_of(a $- b $+ #1)" apply (simp (no_asm) add: zless_nat_conj) apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls) done lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure] lemma posDivAlg_eqn: "[| #0 $< b; a ∈ int; b ∈ int |] ==> posDivAlg(<a,b>) = (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))" apply (rule posDivAlg_unfold [THEN trans]) apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym]) apply (blast intro: posDivAlg_termination) done lemma posDivAlg_induct_lemma [rule_format]: assumes prem: "!!a b. [| a ∈ int; b ∈ int; ~ (a $< b | b $<= #0) --> P(<a, #2 $* b>) |] ==> P(<a,b>)" shows "<u,v> ∈ int*int --> P(<u,v>)" apply (rule_tac a = "<u,v>" in wf_induct) apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)" in wf_measure) apply clarify apply (rule prem) apply (drule_tac [3] x = "<xa, #2 $× y>" in spec) apply auto apply (simp add: not_zle_iff_zless posDivAlg_termination) done lemma posDivAlg_induct: assumes u_int: "u ∈ int" and v_int: "v ∈ int" and ih: "!!a b. [| a ∈ int; b ∈ int; ~ (a $< b | b $<= #0) --> P(a, #2 $* b) |] ==> P(a,b)" shows "P(u,v)" apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)") apply simp apply (rule posDivAlg_induct_lemma) apply (simp (no_asm_use)) apply (rule ih) apply (auto simp add: u_int v_int) done (*FIXME: use intify in integ_of so that we always have integ_of w ∈ int. then this rewrite can work for ALL constants!!*) lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)" apply (simp (no_asm) add: int_eq_iff_zle) done subsection{* Some convenient biconditionals for products of signs *} lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j" apply (drule zmult_zless_mono1) apply auto done lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j" apply (drule zmult_zless_mono1_neg) apply auto done lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0" apply (drule zmult_zless_mono1_neg) apply auto done (** Inequality reasoning **) lemma int_0_less_lemma: "[| x ∈ int; y ∈ int |] ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)" apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg) apply (rule ccontr) apply (rule_tac [2] ccontr) apply (auto simp add: zle_def not_zless_iff_zle) apply (erule_tac P = "#0$< x$* y" in rev_mp) apply (erule_tac [2] P = "#0$< x$* y" in rev_mp) apply (drule zmult_pos_neg, assumption) prefer 2 apply (drule zmult_pos_neg, assumption) apply (auto dest: zless_not_sym simp add: zmult_commute) done lemma int_0_less_mult_iff: "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)" apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma) apply auto done lemma int_0_le_lemma: "[| x ∈ int; y ∈ int |] ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)" by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff) lemma int_0_le_mult_iff: "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))" apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma) apply auto done lemma zmult_less_0_iff: "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)" apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym]) apply (auto dest: zless_not_sym simp add: not_zle_iff_zless) done lemma zmult_le_0_iff: "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)" by (auto dest: zless_not_sym simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym]) (*Typechecking for posDivAlg*) lemma posDivAlg_type [rule_format]: "[| a ∈ int; b ∈ int |] ==> posDivAlg(<a,b>) ∈ int * int" apply (rule_tac u = "a" and v = "b" in posDivAlg_induct) apply assumption+ apply (case_tac "#0 $< ba") apply (simp add: posDivAlg_eqn adjust_def integ_of_type split add: split_if_asm) apply clarify apply (simp add: int_0_less_mult_iff not_zle_iff_zless) apply (simp add: not_zless_iff_zle) apply (subst posDivAlg_unfold) apply simp done (*Correctness of posDivAlg: it computes quotients correctly*) lemma posDivAlg_correct [rule_format]: "[| a ∈ int; b ∈ int |] ==> #0 $<= a --> #0 $< b --> quorem (<a,b>, posDivAlg(<a,b>))" apply (rule_tac u = "a" and v = "b" in posDivAlg_induct) apply auto apply (simp_all add: quorem_def) txt{*base case: a<b*} apply (simp add: posDivAlg_eqn) apply (simp add: not_zless_iff_zle [THEN iff_sym]) apply (simp add: int_0_less_mult_iff) txt{*main argument*} apply (subst posDivAlg_eqn) apply (simp_all (no_asm_simp)) apply (erule splitE) apply (rule posDivAlg_type) apply (simp_all add: int_0_less_mult_iff) apply (auto simp add: zadd_zmult_distrib2 Let_def) txt{*now just linear arithmetic*} apply (simp add: not_zle_iff_zless zdiff_zless_iff) done subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*} lemma negDivAlg_termination: "[| #0 $< b; a $+ b $< #0 |] ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)" apply (simp (no_asm) add: zless_nat_conj) apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym] zless_zminus) done lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure] lemma negDivAlg_eqn: "[| #0 $< b; a : int; b : int |] ==> negDivAlg(<a,b>) = (if #0 $<= a$+b then <#-1,a$+b> else adjust(b, negDivAlg (<a, #2$*b>)))" apply (rule negDivAlg_unfold [THEN trans]) apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym]) apply (blast intro: negDivAlg_termination) done lemma negDivAlg_induct_lemma [rule_format]: assumes prem: "!!a b. [| a ∈ int; b ∈ int; ~ (#0 $<= a $+ b | b $<= #0) --> P(<a, #2 $* b>) |] ==> P(<a,b>)" shows "<u,v> ∈ int*int --> P(<u,v>)" apply (rule_tac a = "<u,v>" in wf_induct) apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)" in wf_measure) apply clarify apply (rule prem) apply (drule_tac [3] x = "<xa, #2 $× y>" in spec) apply auto apply (simp add: not_zle_iff_zless negDivAlg_termination) done lemma negDivAlg_induct: assumes u_int: "u ∈ int" and v_int: "v ∈ int" and ih: "!!a b. [| a ∈ int; b ∈ int; ~ (#0 $<= a $+ b | b $<= #0) --> P(a, #2 $* b) |] ==> P(a,b)" shows "P(u,v)" apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)") apply simp apply (rule negDivAlg_induct_lemma) apply (simp (no_asm_use)) apply (rule ih) apply (auto simp add: u_int v_int) done (*Typechecking for negDivAlg*) lemma negDivAlg_type: "[| a ∈ int; b ∈ int |] ==> negDivAlg(<a,b>) ∈ int * int" apply (rule_tac u = "a" and v = "b" in negDivAlg_induct) apply assumption+ apply (case_tac "#0 $< ba") apply (simp add: negDivAlg_eqn adjust_def integ_of_type split add: split_if_asm) apply clarify apply (simp add: int_0_less_mult_iff not_zle_iff_zless) apply (simp add: not_zless_iff_zle) apply (subst negDivAlg_unfold) apply simp done (*Correctness of negDivAlg: it computes quotients correctly It doesn't work if a=0 because the 0/b=0 rather than -1*) lemma negDivAlg_correct [rule_format]: "[| a ∈ int; b ∈ int |] ==> a $< #0 --> #0 $< b --> quorem (<a,b>, negDivAlg(<a,b>))" apply (rule_tac u = "a" and v = "b" in negDivAlg_induct) apply auto apply (simp_all add: quorem_def) txt{*base case: @{term "0$<=a$+b"}*} apply (simp add: negDivAlg_eqn) apply (simp add: not_zless_iff_zle [THEN iff_sym]) apply (simp add: int_0_less_mult_iff) txt{*main argument*} apply (subst negDivAlg_eqn) apply (simp_all (no_asm_simp)) apply (erule splitE) apply (rule negDivAlg_type) apply (simp_all add: int_0_less_mult_iff) apply (auto simp add: zadd_zmult_distrib2 Let_def) txt{*now just linear arithmetic*} apply (simp add: not_zle_iff_zless zdiff_zless_iff) done subsection{* Existence shown by proving the division algorithm to be correct *} (*the case a=0*) lemma quorem_0: "[|b ≠ #0; b ∈ int|] ==> quorem (<#0,b>, <#0,#0>)" by (force simp add: quorem_def neq_iff_zless) lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>" apply (subst posDivAlg_unfold) apply simp done lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>" apply (subst posDivAlg_unfold) apply (simp add: not_zle_iff_zless) done (*Needed below. Actually it's an equivalence.*) lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)" apply (simp add: not_zle_iff_zless) apply (drule zminus_zless_zminus [THEN iffD2]) apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus) done lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b$-#1>" apply (subst negDivAlg_unfold) apply (simp add: linear_arith_lemma integ_of_type vimage_iff) done lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>" apply (unfold negateSnd_def) apply auto done lemma negateSnd_type: "qr ∈ int * int ==> negateSnd (qr) ∈ int * int" apply (unfold negateSnd_def) apply auto done lemma quorem_neg: "[|quorem (<$-a,$-b>, qr); a ∈ int; b ∈ int; qr ∈ int * int|] ==> quorem (<a,b>, negateSnd(qr))" apply clarify apply (auto elim: zless_asym simp add: quorem_def zless_zminus) txt{*linear arithmetic from here on*} apply (simp_all add: zminus_equation [of a] zminus_zless) apply (cut_tac [2] z = "b" and w = "#0" in zless_linear) apply (cut_tac [1] z = "b" and w = "#0" in zless_linear) apply auto apply (blast dest: zle_zless_trans)+ done lemma divAlg_correct: "[|b ≠ #0; a ∈ int; b ∈ int|] ==> quorem (<a,b>, divAlg(<a,b>))" apply (auto simp add: quorem_0 divAlg_def) apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct posDivAlg_type negDivAlg_type) apply (auto simp add: quorem_def neq_iff_zless) txt{*linear arithmetic from here on*} apply (auto simp add: zle_def) done lemma divAlg_type: "[|a ∈ int; b ∈ int|] ==> divAlg(<a,b>) ∈ int * int" apply (auto simp add: divAlg_def) apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type) done (** intify cancellation **) lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y" apply (simp (no_asm) add: zdiv_def) done lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y" apply (simp (no_asm) add: zdiv_def) done lemma zdiv_type [iff,TC]: "z zdiv w ∈ int" apply (unfold zdiv_def) apply (blast intro: fst_type divAlg_type) done lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y" apply (simp (no_asm) add: zmod_def) done lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y" apply (simp (no_asm) add: zmod_def) done lemma zmod_type [iff,TC]: "z zmod w ∈ int" apply (unfold zmod_def) apply (rule snd_type) apply (blast intro: divAlg_type) done (** Arbitrary definitions for division by zero. Useful to simplify certain equations **) lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0" apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor) done (*NOT for adding to default simpset*) lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)" apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor) done (*NOT for adding to default simpset*) (** Basic laws about division and remainder **) lemma raw_zmod_zdiv_equality: "[| a ∈ int; b ∈ int |] ==> a = b $* (a zdiv b) $+ (a zmod b)" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (cut_tac a = "a" and b = "b" in divAlg_correct) apply (auto simp add: quorem_def zdiv_def zmod_def split_def) done lemma zmod_zdiv_equality: "intify(a) = b $* (a zdiv b) $+ (a zmod b)" apply (rule trans) apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality) apply auto done lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct) apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def) apply (blast dest: zle_zless_trans)+ done lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard] and pos_mod_bound = pos_mod [THEN conjunct2, standard] lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct) apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def) apply (blast dest: zle_zless_trans) apply (blast dest: zless_trans)+ done lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard] and neg_mod_bound = neg_mod [THEN conjunct2, standard] (** proving general properties of zdiv and zmod **) lemma quorem_div_mod: "[|b ≠ #0; a ∈ int; b ∈ int |] ==> quorem (<a,b>, <a zdiv b, a zmod b>)" apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) done (*Surely quorem(<a,b>,<q,r>) implies a ∈ int, but it doesn't matter*) lemma quorem_div: "[| quorem(<a,b>,<q,r>); b ≠ #0; a ∈ int; b ∈ int; q ∈ int |] ==> a zdiv b = q" by (blast intro: quorem_div_mod [THEN unique_quotient]) lemma quorem_mod: "[| quorem(<a,b>,<q,r>); b ≠ #0; a ∈ int; b ∈ int; q ∈ int; r ∈ int |] ==> a zmod b = r" by (blast intro: quorem_div_mod [THEN unique_remainder]) lemma zdiv_pos_pos_trivial_raw: "[| a ∈ int; b ∈ int; #0 $<= a; a $< b |] ==> a zdiv b = #0" apply (rule quorem_div) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zle_zless_trans)+ done lemma zdiv_pos_pos_trivial: "[| #0 $<= a; a $< b |] ==> a zdiv b = #0" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_pos_pos_trivial_raw) apply auto done lemma zdiv_neg_neg_trivial_raw: "[| a ∈ int; b ∈ int; a $<= #0; b $< a |] ==> a zdiv b = #0" apply (rule_tac r = "a" in quorem_div) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zle_zless_trans zless_trans)+ done lemma zdiv_neg_neg_trivial: "[| a $<= #0; b $< a |] ==> a zdiv b = #0" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_neg_neg_trivial_raw) apply auto done lemma zadd_le_0_lemma: "[| a$+b $<= #0; #0 $< a; #0 $< b |] ==> False" apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono) apply (auto simp add: zle_def) apply (blast dest: zless_trans) done lemma zdiv_pos_neg_trivial_raw: "[| a ∈ int; b ∈ int; #0 $< a; a$+b $<= #0 |] ==> a zdiv b = #-1" apply (rule_tac r = "a $+ b" in quorem_div) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zadd_le_0_lemma zle_zless_trans)+ done lemma zdiv_pos_neg_trivial: "[| #0 $< a; a$+b $<= #0 |] ==> a zdiv b = #-1" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_pos_neg_trivial_raw) apply auto done (*There is no zdiv_neg_pos_trivial because #0 zdiv b = #0 would supersede it*) lemma zmod_pos_pos_trivial_raw: "[| a ∈ int; b ∈ int; #0 $<= a; a $< b |] ==> a zmod b = a" apply (rule_tac q = "#0" in quorem_mod) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zle_zless_trans)+ done lemma zmod_pos_pos_trivial: "[| #0 $<= a; a $< b |] ==> a zmod b = intify(a)" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_pos_pos_trivial_raw) apply auto done lemma zmod_neg_neg_trivial_raw: "[| a ∈ int; b ∈ int; a $<= #0; b $< a |] ==> a zmod b = a" apply (rule_tac q = "#0" in quorem_mod) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zle_zless_trans zless_trans)+ done lemma zmod_neg_neg_trivial: "[| a $<= #0; b $< a |] ==> a zmod b = intify(a)" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_neg_neg_trivial_raw) apply auto done lemma zmod_pos_neg_trivial_raw: "[| a ∈ int; b ∈ int; #0 $< a; a$+b $<= #0 |] ==> a zmod b = a$+b" apply (rule_tac q = "#-1" in quorem_mod) apply (auto simp add: quorem_def) (*linear arithmetic*) apply (blast dest: zadd_le_0_lemma zle_zless_trans)+ done lemma zmod_pos_neg_trivial: "[| #0 $< a; a$+b $<= #0 |] ==> a zmod b = a$+b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_pos_neg_trivial_raw) apply auto done (*There is no zmod_neg_pos_trivial...*) (*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*) lemma zdiv_zminus_zminus_raw: "[|a ∈ int; b ∈ int|] ==> ($-a) zdiv ($-b) = a zdiv b" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div]) apply auto done lemma zdiv_zminus_zminus [simp]: "($-a) zdiv ($-b) = a zdiv b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw) apply auto done (*Simpler laws such as -a zmod b = -(a zmod b) FAIL*) lemma zmod_zminus_zminus_raw: "[|a ∈ int; b ∈ int|] ==> ($-a) zmod ($-b) = $- (a zmod b)" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod]) apply auto done lemma zmod_zminus_zminus [simp]: "($-a) zmod ($-b) = $- (a zmod b)" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw) apply auto done subsection{* division of a number by itself *} lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q" apply (subgoal_tac "#0 $< a$*q") apply (cut_tac w = "#0" and z = "q" in add1_zle_iff) apply (simp add: int_0_less_mult_iff) apply (blast dest: zless_trans) (*linear arithmetic...*) apply (drule_tac t = "%x. x $- r" in subst_context) apply (drule sym) apply (simp add: zcompare_rls) done lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1" apply (subgoal_tac "#0 $<= a$* (#1$-q)") apply (simp add: int_0_le_mult_iff zcompare_rls) apply (blast dest: zle_zless_trans) apply (simp add: zdiff_zmult_distrib2) apply (drule_tac t = "%x. x $- a $* q" in subst_context) apply (simp add: zcompare_rls) done lemma self_quotient: "[| quorem(<a,a>,<q,r>); a ∈ int; q ∈ int; a ≠ #0|] ==> q = #1" apply (simp add: split_ifs quorem_def neq_iff_zless) apply (rule zle_anti_sym) apply safe apply auto prefer 4 apply (blast dest: zless_trans) apply (blast dest: zless_trans) apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1) apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2) apply (rule_tac [6] zminus_equation [THEN iffD1]) apply (rule_tac [2] zminus_equation [THEN iffD1]) apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+ done lemma self_remainder: "[|quorem(<a,a>,<q,r>); a ∈ int; q ∈ int; r ∈ int; a ≠ #0|] ==> r = #0" apply (frule self_quotient) apply (auto simp add: quorem_def) done lemma zdiv_self_raw: "[|a ≠ #0; a ∈ int|] ==> a zdiv a = #1" apply (blast intro: quorem_div_mod [THEN self_quotient]) done lemma zdiv_self [simp]: "intify(a) ≠ #0 ==> a zdiv a = #1" apply (drule zdiv_self_raw) apply auto done (*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *) lemma zmod_self_raw: "a ∈ int ==> a zmod a = #0" apply (case_tac "a = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (blast intro: quorem_div_mod [THEN self_remainder]) done lemma zmod_self [simp]: "a zmod a = #0" apply (cut_tac a = "intify (a)" in zmod_self_raw) apply auto done subsection{* Computation of division and remainder *} lemma zdiv_zero [simp]: "#0 zdiv b = #0" apply (simp (no_asm) add: zdiv_def divAlg_def) done lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1" apply (simp (no_asm_simp) add: zdiv_def divAlg_def) done lemma zmod_zero [simp]: "#0 zmod b = #0" apply (simp (no_asm) add: zmod_def divAlg_def) done lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1" apply (simp (no_asm_simp) add: zdiv_def divAlg_def) done lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1" apply (simp (no_asm_simp) add: zmod_def divAlg_def) done (** a positive, b positive **) lemma zdiv_pos_pos: "[| #0 $< a; #0 $<= b |] ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))" apply (simp (no_asm_simp) add: zdiv_def divAlg_def) apply (auto simp add: zle_def) done lemma zmod_pos_pos: "[| #0 $< a; #0 $<= b |] ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))" apply (simp (no_asm_simp) add: zmod_def divAlg_def) apply (auto simp add: zle_def) done (** a negative, b positive **) lemma zdiv_neg_pos: "[| a $< #0; #0 $< b |] ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))" apply (simp (no_asm_simp) add: zdiv_def divAlg_def) apply (blast dest: zle_zless_trans) done lemma zmod_neg_pos: "[| a $< #0; #0 $< b |] ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))" apply (simp (no_asm_simp) add: zmod_def divAlg_def) apply (blast dest: zle_zless_trans) done (** a positive, b negative **) lemma zdiv_pos_neg: "[| #0 $< a; b $< #0 |] ==> a zdiv b = fst (negateSnd(negDivAlg (<$-a, $-b>)))" apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle) apply auto apply (blast dest: zle_zless_trans)+ apply (blast dest: zless_trans) apply (blast intro: zless_imp_zle) done lemma zmod_pos_neg: "[| #0 $< a; b $< #0 |] ==> a zmod b = snd (negateSnd(negDivAlg (<$-a, $-b>)))" apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle) apply auto apply (blast dest: zle_zless_trans)+ apply (blast dest: zless_trans) apply (blast intro: zless_imp_zle) done (** a negative, b negative **) lemma zdiv_neg_neg: "[| a $< #0; b $<= #0 |] ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))" apply (simp (no_asm_simp) add: zdiv_def divAlg_def) apply auto apply (blast dest!: zle_zless_trans)+ done lemma zmod_neg_neg: "[| a $< #0; b $<= #0 |] ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))" apply (simp (no_asm_simp) add: zmod_def divAlg_def) apply auto apply (blast dest!: zle_zless_trans)+ done declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] (** Special-case simplification **) lemma zmod_1 [simp]: "a zmod #1 = #0" apply (cut_tac a = "a" and b = "#1" in pos_mod_sign) apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound) apply auto (*arithmetic*) apply (drule add1_zle_iff [THEN iffD2]) apply (rule zle_anti_sym) apply auto done lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)" apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality) apply auto done lemma zmod_minus1_right [simp]: "a zmod #-1 = #0" apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign) apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound) apply auto (*arithmetic*) apply (drule add1_zle_iff [THEN iffD2]) apply (rule zle_anti_sym) apply auto done lemma zdiv_minus1_right_raw: "a ∈ int ==> a zdiv #-1 = $-a" apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality) apply auto apply (rule equation_zminus [THEN iffD2]) apply auto done lemma zdiv_minus1_right: "a zdiv #-1 = $-a" apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw) apply auto done declare zdiv_minus1_right [simp] subsection{* Monotonicity in the first argument (divisor) *} lemma zdiv_mono1: "[| a $<= a'; #0 $< b |] ==> a zdiv b $<= a' zdiv b" apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality) apply (rule unique_quotient_lemma) apply (erule subst) apply (erule subst) apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound) done lemma zdiv_mono1_neg: "[| a $<= a'; b $< #0 |] ==> a' zdiv b $<= a zdiv b" apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality) apply (rule unique_quotient_lemma_neg) apply (erule subst) apply (erule subst) apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound) done subsection{* Monotonicity in the second argument (dividend) *} lemma q_pos_lemma: "[| #0 $<= b'$*q' $+ r'; r' $< b'; #0 $< b' |] ==> #0 $<= q'" apply (subgoal_tac "#0 $< b'$* (q' $+ #1)") apply (simp add: int_0_less_mult_iff) apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1]) apply (simp add: zadd_zmult_distrib2) apply (erule zle_zless_trans) apply (erule zadd_zless_mono2) done lemma zdiv_mono2_lemma: "[| b$*q $+ r = b'$*q' $+ r'; #0 $<= b'$*q' $+ r'; r' $< b'; #0 $<= r; #0 $< b'; b' $<= b |] ==> q $<= q'" apply (frule q_pos_lemma, assumption+) apply (subgoal_tac "b$*q $< b$* (q' $+ #1)") apply (simp add: zmult_zless_cancel1) apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans) apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'") prefer 2 apply (simp add: zcompare_rls) apply (simp (no_asm_simp) add: zadd_zmult_distrib2) apply (subst zadd_commute [of "b $× q'"], rule zadd_zless_mono) prefer 2 apply (blast intro: zmult_zle_mono1) apply (subgoal_tac "r' $+ #0 $< b $+ r") apply (simp add: zcompare_rls) apply (rule zadd_zless_mono) apply auto apply (blast dest: zless_zle_trans) done lemma zdiv_mono2_raw: "[| #0 $<= a; #0 $< b'; b' $<= b; a ∈ int |] ==> a zdiv b $<= a zdiv b'" apply (subgoal_tac "#0 $< b") prefer 2 apply (blast dest: zless_zle_trans) apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality) apply (rule zdiv_mono2_lemma) apply (erule subst) apply (erule subst) apply (simp_all add: pos_mod_sign pos_mod_bound) done lemma zdiv_mono2: "[| #0 $<= a; #0 $< b'; b' $<= b |] ==> a zdiv b $<= a zdiv b'" apply (cut_tac a = "intify (a)" in zdiv_mono2_raw) apply auto done lemma q_neg_lemma: "[| b'$*q' $+ r' $< #0; #0 $<= r'; #0 $< b' |] ==> q' $< #0" apply (subgoal_tac "b'$*q' $< #0") prefer 2 apply (force intro: zle_zless_trans) apply (simp add: zmult_less_0_iff) apply (blast dest: zless_trans) done lemma zdiv_mono2_neg_lemma: "[| b$*q $+ r = b'$*q' $+ r'; b'$*q' $+ r' $< #0; r $< b; #0 $<= r'; #0 $< b'; b' $<= b |] ==> q' $<= q" apply (subgoal_tac "#0 $< b") prefer 2 apply (blast dest: zless_zle_trans) apply (frule q_neg_lemma, assumption+) apply (subgoal_tac "b$*q' $< b$* (q $+ #1)") apply (simp add: zmult_zless_cancel1) apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1]) apply (simp (no_asm_simp) add: zadd_zmult_distrib2) apply (subgoal_tac "b$*q' $<= b'$*q'") prefer 2 apply (simp add: zmult_zle_cancel2) apply (blast dest: zless_trans) apply (subgoal_tac "b'$*q' $+ r $< b $+ (b$*q $+ r)") prefer 2 apply (erule ssubst) apply simp apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono) apply (assumption) apply simp apply (simp (no_asm_use) add: zadd_commute) apply (rule zle_zless_trans) prefer 2 apply (assumption) apply (simp (no_asm_simp) add: zmult_zle_cancel2) apply (blast dest: zless_trans) done lemma zdiv_mono2_neg_raw: "[| a $< #0; #0 $< b'; b' $<= b; a ∈ int |] ==> a zdiv b' $<= a zdiv b" apply (subgoal_tac "#0 $< b") prefer 2 apply (blast dest: zless_zle_trans) apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality) apply (rule zdiv_mono2_neg_lemma) apply (erule subst) apply (erule subst) apply (simp_all add: pos_mod_sign pos_mod_bound) done lemma zdiv_mono2_neg: "[| a $< #0; #0 $< b'; b' $<= b |] ==> a zdiv b' $<= a zdiv b" apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw) apply auto done subsection{* More algebraic laws for zdiv and zmod *} (** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **) lemma zmult1_lemma: "[| quorem(<b,c>, <q,r>); c ∈ int; c ≠ #0 |] ==> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)" apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2 pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) apply (auto intro: raw_zmod_zdiv_equality) done lemma zdiv_zmult1_eq_raw: "[|b ∈ int; c ∈ int|] ==> (a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c" apply (case_tac "c = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) apply auto done lemma zdiv_zmult1_eq: "(a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c" apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw) apply auto done lemma zmod_zmult1_eq_raw: "[|b ∈ int; c ∈ int|] ==> (a$*b) zmod c = a$*(b zmod c) zmod c" apply (case_tac "c = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) apply auto done lemma zmod_zmult1_eq: "(a$*b) zmod c = a$*(b zmod c) zmod c" apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw) apply auto done lemma zmod_zmult1_eq': "(a$*b) zmod c = ((a zmod c) $* b) zmod c" apply (rule trans) apply (rule_tac b = " (b $* a) zmod c" in trans) apply (rule_tac [2] zmod_zmult1_eq) apply (simp_all (no_asm) add: zmult_commute) done lemma zmod_zmult_distrib: "(a$*b) zmod c = ((a zmod c) $* (b zmod c)) zmod c" apply (rule zmod_zmult1_eq' [THEN trans]) apply (rule zmod_zmult1_eq) done lemma zdiv_zmult_self1 [simp]: "intify(b) ≠ #0 ==> (a$*b) zdiv b = intify(a)" apply (simp (no_asm_simp) add: zdiv_zmult1_eq) done lemma zdiv_zmult_self2 [simp]: "intify(b) ≠ #0 ==> (b$*a) zdiv b = intify(a)" apply (subst zmult_commute , erule zdiv_zmult_self1) done lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0" apply (simp (no_asm) add: zmod_zmult1_eq) done lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0" apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq) done (** proving (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **) lemma zadd1_lemma: "[| quorem(<a,c>, <aq,ar>); quorem(<b,c>, <bq,br>); c ∈ int; c ≠ #0 |] ==> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)" apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2 pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) apply (auto intro: raw_zmod_zdiv_equality) done (*NOT suitable for rewriting: the RHS has an instance of the LHS*) lemma zdiv_zadd1_eq_raw: "[|a ∈ int; b ∈ int; c ∈ int|] ==> (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)" apply (case_tac "c = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod, THEN quorem_div]) done lemma zdiv_zadd1_eq: "(a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)" apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" in zdiv_zadd1_eq_raw) apply auto done lemma zmod_zadd1_eq_raw: "[|a ∈ int; b ∈ int; c ∈ int|] ==> (a$+b) zmod c = (a zmod c $+ b zmod c) zmod c" apply (case_tac "c = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod, THEN quorem_mod]) done lemma zmod_zadd1_eq: "(a$+b) zmod c = (a zmod c $+ b zmod c) zmod c" apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" in zmod_zadd1_eq_raw) apply auto done lemma zmod_div_trivial_raw: "[|a ∈ int; b ∈ int|] ==> (a zmod b) zdiv b = #0" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial) done lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw) apply auto done lemma zmod_mod_trivial_raw: "[|a ∈ int; b ∈ int|] ==> (a zmod b) zmod b = a zmod b" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial) done lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw) apply auto done lemma zmod_zadd_left_eq: "(a$+b) zmod c = ((a zmod c) $+ b) zmod c" apply (rule trans [symmetric]) apply (rule zmod_zadd1_eq) apply (simp (no_asm)) apply (rule zmod_zadd1_eq [symmetric]) done lemma zmod_zadd_right_eq: "(a$+b) zmod c = (a $+ (b zmod c)) zmod c" apply (rule trans [symmetric]) apply (rule zmod_zadd1_eq) apply (simp (no_asm)) apply (rule zmod_zadd1_eq [symmetric]) done lemma zdiv_zadd_self1 [simp]: "intify(a) ≠ #0 ==> (a$+b) zdiv a = b zdiv a $+ #1" by (simp (no_asm_simp) add: zdiv_zadd1_eq) lemma zdiv_zadd_self2 [simp]: "intify(a) ≠ #0 ==> (b$+a) zdiv a = b zdiv a $+ #1" by (simp (no_asm_simp) add: zdiv_zadd1_eq) lemma zmod_zadd_self1 [simp]: "(a$+b) zmod a = b zmod a" apply (case_tac "a = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (simp (no_asm_simp) add: zmod_zadd1_eq) done lemma zmod_zadd_self2 [simp]: "(b$+a) zmod a = b zmod a" apply (case_tac "a = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (simp (no_asm_simp) add: zmod_zadd1_eq) done subsection{* proving a zdiv (b*c) = (a zdiv b) zdiv c *} (*The condition c>0 seems necessary. Consider that 7 zdiv ~6 = ~2 but 7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1. The subcase (a zdiv b) zmod c = 0 seems to cause particular problems.*) (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) lemma zdiv_zmult2_aux1: "[| #0 $< c; b $< r; r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r" apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1") apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls) apply (rule zle_zless_trans) apply (erule_tac [2] zmult_zless_mono1) apply (rule zmult_zle_mono2_neg) apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound) apply (blast intro: zless_imp_zle dest: zless_zle_trans) done lemma zdiv_zmult2_aux2: "[| #0 $< c; b $< r; r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0" apply (subgoal_tac "b $* (q zmod c) $<= #0") prefer 2 apply (simp add: zmult_le_0_iff pos_mod_sign) apply (blast intro: zless_imp_zle dest: zless_zle_trans) (*arithmetic*) apply (drule zadd_zle_mono) apply assumption apply (simp add: zadd_commute) done lemma zdiv_zmult2_aux3: "[| #0 $< c; #0 $<= r; r $< b |] ==> #0 $<= b $* (q zmod c) $+ r" apply (subgoal_tac "#0 $<= b $* (q zmod c)") prefer 2 apply (simp add: int_0_le_mult_iff pos_mod_sign) apply (blast intro: zless_imp_zle dest: zle_zless_trans) (*arithmetic*) apply (drule zadd_zle_mono) apply assumption apply (simp add: zadd_commute) done lemma zdiv_zmult2_aux4: "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c" apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)") apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls) apply (rule zless_zle_trans) apply (erule zmult_zless_mono1) apply (rule_tac [2] zmult_zle_mono2) apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound) apply (blast intro: zless_imp_zle dest: zle_zless_trans) done lemma zdiv_zmult2_lemma: "[| quorem (<a,b>, <q,r>); a ∈ int; b ∈ int; b ≠ #0; #0 $< c |] ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)" apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def neq_iff_zless int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2 zdiv_zmult2_aux3 zdiv_zmult2_aux4) apply (blast dest: zless_trans)+ done lemma zdiv_zmult2_eq_raw: "[|#0 $< c; a ∈ int; b ∈ int|] ==> a zdiv (b$*c) = (a zdiv b) zdiv c" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div]) apply (auto simp add: intify_eq_0_iff_zle) apply (blast dest: zle_zless_trans) done lemma zdiv_zmult2_eq: "#0 $< c ==> a zdiv (b$*c) = (a zdiv b) zdiv c" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw) apply auto done lemma zmod_zmult2_eq_raw: "[|#0 $< c; a ∈ int; b ∈ int|] ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod]) apply (auto simp add: intify_eq_0_iff_zle) apply (blast dest: zle_zless_trans) done lemma zmod_zmult2_eq: "#0 $< c ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw) apply auto done subsection{* Cancellation of common factors in "zdiv" *} lemma zdiv_zmult_zmult1_aux1: "[| #0 $< b; intify(c) ≠ #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b" apply (subst zdiv_zmult2_eq) apply auto done lemma zdiv_zmult_zmult1_aux2: "[| b $< #0; intify(c) ≠ #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b" apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)") apply (rule_tac [2] zdiv_zmult_zmult1_aux1) apply auto done lemma zdiv_zmult_zmult1_raw: "[|intify(c) ≠ #0; b ∈ int|] ==> (c$*a) zdiv (c$*b) = a zdiv b" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (auto simp add: neq_iff_zless [of b] zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) done lemma zdiv_zmult_zmult1: "intify(c) ≠ #0 ==> (c$*a) zdiv (c$*b) = a zdiv b" apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw) apply auto done lemma zdiv_zmult_zmult2: "intify(c) ≠ #0 ==> (a$*c) zdiv (b$*c) = a zdiv b" apply (drule zdiv_zmult_zmult1) apply (auto simp add: zmult_commute) done subsection{* Distribution of factors over "zmod" *} lemma zmod_zmult_zmult1_aux1: "[| #0 $< b; intify(c) ≠ #0 |] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)" apply (subst zmod_zmult2_eq) apply auto done lemma zmod_zmult_zmult1_aux2: "[| b $< #0; intify(c) ≠ #0 |] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)" apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))") apply (rule_tac [2] zmod_zmult_zmult1_aux1) apply auto done lemma zmod_zmult_zmult1_raw: "[|b ∈ int; c ∈ int|] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)" apply (case_tac "b = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (case_tac "c = #0") apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) apply (auto simp add: neq_iff_zless [of b] zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) done lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)" apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw) apply auto done lemma zmod_zmult_zmult2: "(a$*c) zmod (b$*c) = (a zmod b) $* c" apply (cut_tac c = "c" in zmod_zmult_zmult1) apply (auto simp add: zmult_commute) done (** Quotients of signs **) lemma zdiv_neg_pos_less0: "[| a $< #0; #0 $< b |] ==> a zdiv b $< #0" apply (subgoal_tac "a zdiv b $<= #-1") apply (erule zle_zless_trans) apply (simp (no_asm)) apply (rule zle_trans) apply (rule_tac a' = "#-1" in zdiv_mono1) apply (rule zless_add1_iff_zle [THEN iffD1]) apply (simp (no_asm)) apply (auto simp add: zdiv_minus1) done lemma zdiv_nonneg_neg_le0: "[| #0 $<= a; b $< #0 |] ==> a zdiv b $<= #0" apply (drule zdiv_mono1_neg) apply auto done lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)" apply auto apply (drule_tac [2] zdiv_mono1) apply (auto simp add: neq_iff_zless) apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym]) apply (blast intro: zdiv_neg_pos_less0) done lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)" apply (subst zdiv_zminus_zminus [symmetric]) apply (rule iff_trans) apply (rule pos_imp_zdiv_nonneg_iff) apply auto done (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*) lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)" apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) apply (erule pos_imp_zdiv_nonneg_iff) done (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*) lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)" apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) apply (erule neg_imp_zdiv_nonneg_iff) done (* THESE REMAIN TO BE CONVERTED -- but aren't that useful! subsection{* Speeding up the division algorithm with shifting *} (** computing "zdiv" by shifting **) lemma pos_zdiv_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a" apply (case_tac "a = #0") apply (subgoal_tac "#1 $<= a") apply (arith_tac 2) apply (subgoal_tac "#1 $< a $* #2") apply (arith_tac 2) apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a") apply (rule_tac [2] zmult_zle_mono2) apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound) apply (subst zdiv_zadd1_eq) apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial) apply (subst zdiv_pos_pos_trivial) apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ]) apply (auto simp add: zmod_pos_pos_trivial) apply (subgoal_tac "#0 $<= b zmod a") apply (asm_simp_tac (simpset () add: pos_mod_sign) 2) apply arith done lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a" apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)") apply (rule_tac [2] pos_zdiv_mult_2) apply (auto simp add: zmult_zminus_right) apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))") apply (Simp_tac 2) apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) done (*Not clear why this must be proved separately; probably integ_of causes simplification problems*) lemma lemma: "~ #0 $<= x ==> x $<= #0" apply auto done lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) = (if ~b | #0 $<= integ_of w then integ_of v zdiv (integ_of w) else (integ_of v $+ #1) zdiv (integ_of w))" apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT) apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2) done declare zdiv_integ_of_BIT [simp] (** computing "zmod" by shifting (proofs resemble those for "zdiv") **) lemma pos_zmod_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)" apply (case_tac "a = #0") apply (subgoal_tac "#1 $<= a") apply (arith_tac 2) apply (subgoal_tac "#1 $< a $* #2") apply (arith_tac 2) apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a") apply (rule_tac [2] zmult_zle_mono2) apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound) apply (subst zmod_zadd1_eq) apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial) apply (rule zmod_pos_pos_trivial) apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ]) apply (auto simp add: zmod_pos_pos_trivial) apply (subgoal_tac "#0 $<= b zmod a") apply (asm_simp_tac (simpset () add: pos_mod_sign) 2) apply arith done lemma neg_zmod_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1" apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zmod (#2$* ($-a)) = #1 $+ #2$* (($-b-#1) zmod ($-a))") apply (rule_tac [2] pos_zmod_mult_2) apply (auto simp add: zmult_zminus_right) apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))") apply (Simp_tac 2) apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) apply (dtac (zminus_equation [THEN iffD1, symmetric]) apply auto done lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) = (if b then if #0 $<= integ_of w then #2 $* (integ_of v zmod integ_of w) $+ #1 else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1 else #2 $* (integ_of v zmod integ_of w))" apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT) apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2) done declare zmod_integ_of_BIT [simp] *) ML{* val zspos_add_zspos_imp_zspos = thm "zspos_add_zspos_imp_zspos"; val zpos_add_zpos_imp_zpos = thm "zpos_add_zpos_imp_zpos"; val zneg_add_zneg_imp_zneg = thm "zneg_add_zneg_imp_zneg"; val zneg_or_0_add_zneg_or_0_imp_zneg_or_0 = thm "zneg_or_0_add_zneg_or_0_imp_zneg_or_0"; val zero_lt_zmagnitude = thm "zero_lt_zmagnitude"; val zless_add_succ_iff = thm "zless_add_succ_iff"; val zadd_succ_zle_iff = thm "zadd_succ_zle_iff"; val zless_add1_iff_zle = thm "zless_add1_iff_zle"; val add1_zle_iff = thm "add1_zle_iff"; val add1_left_zle_iff = thm "add1_left_zle_iff"; val zmult_zle_mono1 = thm "zmult_zle_mono1"; val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg"; val zmult_zle_mono2 = thm "zmult_zle_mono2"; val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg"; val zmult_zle_mono = thm "zmult_zle_mono"; val zmult_zless_mono2 = thm "zmult_zless_mono2"; val zmult_zless_mono1 = thm "zmult_zless_mono1"; val zmult_zless_mono = thm "zmult_zless_mono"; val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg"; val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg"; val zmult_eq_0_iff = thm "zmult_eq_0_iff"; val zmult_zless_cancel2 = thm "zmult_zless_cancel2"; val zmult_zless_cancel1 = thm "zmult_zless_cancel1"; val zmult_zle_cancel2 = thm "zmult_zle_cancel2"; val zmult_zle_cancel1 = thm "zmult_zle_cancel1"; val int_eq_iff_zle = thm "int_eq_iff_zle"; val zmult_cancel2 = thm "zmult_cancel2"; val zmult_cancel1 = thm "zmult_cancel1"; val unique_quotient = thm "unique_quotient"; val unique_remainder = thm "unique_remainder"; val adjust_eq = thm "adjust_eq"; val posDivAlg_termination = thm "posDivAlg_termination"; val posDivAlg_unfold = thm "posDivAlg_unfold"; val posDivAlg_eqn = thm "posDivAlg_eqn"; val posDivAlg_induct = thm "posDivAlg_induct"; val intify_eq_0_iff_zle = thm "intify_eq_0_iff_zle"; val zmult_pos = thm "zmult_pos"; val zmult_neg = thm "zmult_neg"; val zmult_pos_neg = thm "zmult_pos_neg"; val int_0_less_mult_iff = thm "int_0_less_mult_iff"; val int_0_le_mult_iff = thm "int_0_le_mult_iff"; val zmult_less_0_iff = thm "zmult_less_0_iff"; val zmult_le_0_iff = thm "zmult_le_0_iff"; val posDivAlg_type = thm "posDivAlg_type"; val posDivAlg_correct = thm "posDivAlg_correct"; val negDivAlg_termination = thm "negDivAlg_termination"; val negDivAlg_unfold = thm "negDivAlg_unfold"; val negDivAlg_eqn = thm "negDivAlg_eqn"; val negDivAlg_induct = thm "negDivAlg_induct"; val negDivAlg_type = thm "negDivAlg_type"; val negDivAlg_correct = thm "negDivAlg_correct"; val quorem_0 = thm "quorem_0"; val posDivAlg_zero_divisor = thm "posDivAlg_zero_divisor"; val posDivAlg_0 = thm "posDivAlg_0"; val negDivAlg_minus1 = thm "negDivAlg_minus1"; val negateSnd_eq = thm "negateSnd_eq"; val negateSnd_type = thm "negateSnd_type"; val quorem_neg = thm "quorem_neg"; val divAlg_correct = thm "divAlg_correct"; val divAlg_type = thm "divAlg_type"; val zdiv_intify1 = thm "zdiv_intify1"; val zdiv_intify2 = thm "zdiv_intify2"; val zdiv_type = thm "zdiv_type"; val zmod_intify1 = thm "zmod_intify1"; val zmod_intify2 = thm "zmod_intify2"; val zmod_type = thm "zmod_type"; val DIVISION_BY_ZERO_ZDIV = thm "DIVISION_BY_ZERO_ZDIV"; val DIVISION_BY_ZERO_ZMOD = thm "DIVISION_BY_ZERO_ZMOD"; val zmod_zdiv_equality = thm "zmod_zdiv_equality"; val pos_mod = thm "pos_mod"; val pos_mod_sign = thm "pos_mod_sign"; val neg_mod = thm "neg_mod"; val neg_mod_sign = thm "neg_mod_sign"; val quorem_div_mod = thm "quorem_div_mod"; val quorem_div = thm "quorem_div"; val quorem_mod = thm "quorem_mod"; val zdiv_pos_pos_trivial = thm "zdiv_pos_pos_trivial"; val zdiv_neg_neg_trivial = thm "zdiv_neg_neg_trivial"; val zdiv_pos_neg_trivial = thm "zdiv_pos_neg_trivial"; val zmod_pos_pos_trivial = thm "zmod_pos_pos_trivial"; val zmod_neg_neg_trivial = thm "zmod_neg_neg_trivial"; val zmod_pos_neg_trivial = thm "zmod_pos_neg_trivial"; val zdiv_zminus_zminus = thm "zdiv_zminus_zminus"; val zmod_zminus_zminus = thm "zmod_zminus_zminus"; val self_quotient = thm "self_quotient"; val self_remainder = thm "self_remainder"; val zdiv_self = thm "zdiv_self"; val zmod_self = thm "zmod_self"; val zdiv_zero = thm "zdiv_zero"; val zdiv_eq_minus1 = thm "zdiv_eq_minus1"; val zmod_zero = thm "zmod_zero"; val zdiv_minus1 = thm "zdiv_minus1"; val zmod_minus1 = thm "zmod_minus1"; val zdiv_pos_pos = thm "zdiv_pos_pos"; val zmod_pos_pos = thm "zmod_pos_pos"; val zdiv_neg_pos = thm "zdiv_neg_pos"; val zmod_neg_pos = thm "zmod_neg_pos"; val zdiv_pos_neg = thm "zdiv_pos_neg"; val zmod_pos_neg = thm "zmod_pos_neg"; val zdiv_neg_neg = thm "zdiv_neg_neg"; val zmod_neg_neg = thm "zmod_neg_neg"; val zmod_1 = thm "zmod_1"; val zdiv_1 = thm "zdiv_1"; val zmod_minus1_right = thm "zmod_minus1_right"; val zdiv_minus1_right = thm "zdiv_minus1_right"; val zdiv_mono1 = thm "zdiv_mono1"; val zdiv_mono1_neg = thm "zdiv_mono1_neg"; val zdiv_mono2 = thm "zdiv_mono2"; val zdiv_mono2_neg = thm "zdiv_mono2_neg"; val zdiv_zmult1_eq = thm "zdiv_zmult1_eq"; val zmod_zmult1_eq = thm "zmod_zmult1_eq"; val zmod_zmult1_eq' = thm "zmod_zmult1_eq'"; val zmod_zmult_distrib = thm "zmod_zmult_distrib"; val zdiv_zmult_self1 = thm "zdiv_zmult_self1"; val zdiv_zmult_self2 = thm "zdiv_zmult_self2"; val zmod_zmult_self1 = thm "zmod_zmult_self1"; val zmod_zmult_self2 = thm "zmod_zmult_self2"; val zdiv_zadd1_eq = thm "zdiv_zadd1_eq"; val zmod_zadd1_eq = thm "zmod_zadd1_eq"; val zmod_div_trivial = thm "zmod_div_trivial"; val zmod_mod_trivial = thm "zmod_mod_trivial"; val zmod_zadd_left_eq = thm "zmod_zadd_left_eq"; val zmod_zadd_right_eq = thm "zmod_zadd_right_eq"; val zdiv_zadd_self1 = thm "zdiv_zadd_self1"; val zdiv_zadd_self2 = thm "zdiv_zadd_self2"; val zmod_zadd_self1 = thm "zmod_zadd_self1"; val zmod_zadd_self2 = thm "zmod_zadd_self2"; val zdiv_zmult2_eq = thm "zdiv_zmult2_eq"; val zmod_zmult2_eq = thm "zmod_zmult2_eq"; val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1"; val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2"; val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1"; val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2"; val zdiv_neg_pos_less0 = thm "zdiv_neg_pos_less0"; val zdiv_nonneg_neg_le0 = thm "zdiv_nonneg_neg_le0"; val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff"; val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff"; val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff"; val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff"; *} end
lemma zspos_add_zspos_imp_zspos:
[| #0 $< x; #0 $< y |] ==> #0 $< x $+ y
lemma zpos_add_zpos_imp_zpos:
[| #0 $≤ x; #0 $≤ y |] ==> #0 $≤ x $+ y
lemma zneg_add_zneg_imp_zneg:
[| x $< #0; y $< #0 |] ==> x $+ y $< #0
lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
[| x $≤ #0; y $≤ #0 |] ==> x $+ y $≤ #0
lemma zero_lt_zmagnitude:
[| #0 $< k; k ∈ int |] ==> 0 < zmagnitude(k)
lemma zless_add_succ_iff:
w $< z $+ $# succ(m) <-> w $< z $+ $# m ∨ intify(w) = z $+ $# m
lemma zadd_succ_lemma:
z ∈ int ==> w $+ $# succ(m) $≤ z <-> w $+ $# m $< z
lemma zadd_succ_zle_iff:
w $+ $# succ(m) $≤ z <-> w $+ $# m $< z
lemma zless_add1_iff_zle:
w $< z $+ #1 <-> w $≤ z
lemma add1_zle_iff:
w $+ #1 $≤ z <-> w $< z
lemma add1_left_zle_iff:
#1 $+ w $≤ z <-> w $< z
lemma zmult_mono_lemma:
[| k ∈ nat; i $≤ j |] ==> i $× $# k $≤ j $× $# k
lemma zmult_zle_mono1:
[| i $≤ j; #0 $≤ k |] ==> i $× k $≤ j $× k
lemma zmult_zle_mono1_neg:
[| i $≤ j; k $≤ #0 |] ==> j $× k $≤ i $× k
lemma zmult_zle_mono2:
[| i $≤ j; #0 $≤ k |] ==> k $× i $≤ k $× j
lemma zmult_zle_mono2_neg:
[| i $≤ j; k $≤ #0 |] ==> k $× j $≤ k $× i
lemma zmult_zle_mono:
[| i $≤ j; k $≤ l; #0 $≤ j; #0 $≤ k |] ==> i $× k $≤ j $× l
lemma zmult_zless_mono2_lemma:
[| i $< j; k ∈ nat; 0 < k |] ==> $# k $× i $< $# k $× j
lemma zmult_zless_mono2:
[| i $< j; #0 $< k |] ==> k $× i $< k $× j
lemma zmult_zless_mono1:
[| i $< j; #0 $< k |] ==> i $× k $< j $× k
lemma zmult_zless_mono:
[| i $< j; k $< l; #0 $< j; #0 $< k |] ==> i $× k $< j $× l
lemma zmult_zless_mono1_neg:
[| i $< j; k $< #0 |] ==> j $× k $< i $× k
lemma zmult_zless_mono2_neg:
[| i $< j; k $< #0 |] ==> k $× j $< k $× i
lemma zmult_eq_lemma:
[| m ∈ int; n ∈ int |] ==> m = #0 ∨ n = #0 <-> m $× n = #0
lemma zmult_eq_0_iff:
m $× n = #0 <-> intify(m) = #0 ∨ intify(n) = #0
lemma zmult_zless_lemma:
[| k ∈ int; m ∈ int; n ∈ int |] ==> m $× k $< n $× k <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m
lemma zmult_zless_cancel2:
m $× k $< n $× k <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m
lemma zmult_zless_cancel1:
k $× m $< k $× n <-> #0 $< k ∧ m $< n ∨ k $< #0 ∧ n $< m
lemma zmult_zle_cancel2:
m $× k $≤ n $× k <-> (#0 $< k --> m $≤ n) ∧ (k $< #0 --> n $≤ m)
lemma zmult_zle_cancel1:
k $× m $≤ k $× n <-> (#0 $< k --> m $≤ n) ∧ (k $< #0 --> n $≤ m)
lemma int_eq_iff_zle:
[| m ∈ int; n ∈ int |] ==> m = n <-> m $≤ n ∧ n $≤ m
lemma zmult_cancel2_lemma:
[| k ∈ int; m ∈ int; n ∈ int |] ==> m $× k = n $× k <-> k = #0 ∨ m = n
lemma zmult_cancel2:
m $× k = n $× k <-> intify(k) = #0 ∨ intify(m) = intify(n)
lemma zmult_cancel1:
k $× m = k $× n <-> intify(k) = #0 ∨ intify(m) = intify(n)
lemma unique_quotient_lemma:
[| b $× q' $+ r' $≤ b $× q $+ r; #0 $≤ r'; #0 $< b; r $< b |] ==> q' $≤ q
lemma unique_quotient_lemma_neg:
[| b $× q' $+ r' $≤ b $× q $+ r; r $≤ #0; b $< #0; b $< r' |] ==> q $≤ q'
lemma unique_quotient:
[| quorem(〈a, b〉, 〈q, r〉); quorem(〈a, b〉, 〈q', r'〉); b ∈ int; b ≠ #0; q ∈ int; q' ∈ int |] ==> q = q'
lemma unique_remainder:
[| quorem(〈a, b〉, 〈q, r〉); quorem(〈a, b〉, 〈q', r'〉); b ∈ int; b ≠ #0; q ∈ int; q' ∈ int; r ∈ int; r' ∈ int |] ==> r = r'
lemma adjust_eq:
adjust(b, 〈q, r〉) = (let diff = r $- b in if #0 $≤ diff then 〈#2 $× q $+ #1, diff〉 else 〈#2 $× q, r〉)
lemma posDivAlg_termination:
[| #0 $< b; ¬ a $< b |] ==> nat_of(a $- #2 $× b $+ #1) < nat_of(a $- b $+ #1)
lemmas posDivAlg_unfold:
posDivAlg(a) = (%〈a,b〉 f. if a $< b ∨ b $≤ #0 then 〈#0, a〉 else adjust(b, f ` 〈a, #2 $× b〉)) (a, λx∈measure(int × int, %〈a,b〉. nat_of(a $- b $+ #1)) -`` {a}. posDivAlg(x))
lemmas posDivAlg_unfold:
posDivAlg(a) = (%〈a,b〉 f. if a $< b ∨ b $≤ #0 then 〈#0, a〉 else adjust(b, f ` 〈a, #2 $× b〉)) (a, λx∈measure(int × int, %〈a,b〉. nat_of(a $- b $+ #1)) -`` {a}. posDivAlg(x))
lemma posDivAlg_eqn:
[| #0 $< b; a ∈ int; b ∈ int |] ==> posDivAlg(〈a, b〉) = (if a $< b then 〈#0, a〉 else adjust(b, posDivAlg(〈a, #2 $× b〉)))
lemma posDivAlg_induct_lemma:
(!!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(〈a, #2 $× b〉) |] ==> P(〈a, b〉)) ==> 〈u, v〉 ∈ int × int --> P(〈u, v〉)
lemma posDivAlg_induct:
[| u ∈ int; v ∈ int; !!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(a, #2 $× b) |] ==> P(a, b) |] ==> P(u, v)
lemma intify_eq_0_iff_zle:
intify(m) = #0 <-> m $≤ #0 ∧ #0 $≤ m
lemma zmult_pos:
[| #0 $< i; #0 $< j |] ==> #0 $< i $× j
lemma zmult_neg:
[| i $< #0; j $< #0 |] ==> #0 $< i $× j
lemma zmult_pos_neg:
[| #0 $< i; j $< #0 |] ==> i $× j $< #0
lemma int_0_less_lemma:
[| x ∈ int; y ∈ int |] ==> #0 $< x $× y <-> #0 $< x ∧ #0 $< y ∨ x $< #0 ∧ y $< #0
lemma int_0_less_mult_iff:
#0 $< x $× y <-> #0 $< x ∧ #0 $< y ∨ x $< #0 ∧ y $< #0
lemma int_0_le_lemma:
[| x ∈ int; y ∈ int |] ==> #0 $≤ x $× y <-> #0 $≤ x ∧ #0 $≤ y ∨ x $≤ #0 ∧ y $≤ #0
lemma int_0_le_mult_iff:
#0 $≤ x $× y <-> #0 $≤ x ∧ #0 $≤ y ∨ x $≤ #0 ∧ y $≤ #0
lemma zmult_less_0_iff:
x $× y $< #0 <-> #0 $< x ∧ y $< #0 ∨ x $< #0 ∧ #0 $< y
lemma zmult_le_0_iff:
x $× y $≤ #0 <-> #0 $≤ x ∧ y $≤ #0 ∨ x $≤ #0 ∧ #0 $≤ y
lemma posDivAlg_type:
[| a ∈ int; b ∈ int |] ==> posDivAlg(〈a, b〉) ∈ int × int
lemma posDivAlg_correct:
[| a ∈ int; b ∈ int; #0 $≤ a; #0 $< b |] ==> quorem(〈a, b〉, posDivAlg(〈a, b〉))
lemma negDivAlg_termination:
[| #0 $< b; a $+ b $< #0 |] ==> nat_of($- a $- #2 $× b) < nat_of($- a $- b)
lemmas negDivAlg_unfold:
negDivAlg(a) = (%〈a,b〉 f. if #0 $≤ a $+ b ∨ b $≤ #0 then 〈#-1, a $+ b〉 else adjust(b, f ` 〈a, #2 $× b〉)) (a, λx∈measure(int × int, %〈a,b〉. nat_of($- a $- b)) -`` {a}. negDivAlg(x))
lemmas negDivAlg_unfold:
negDivAlg(a) = (%〈a,b〉 f. if #0 $≤ a $+ b ∨ b $≤ #0 then 〈#-1, a $+ b〉 else adjust(b, f ` 〈a, #2 $× b〉)) (a, λx∈measure(int × int, %〈a,b〉. nat_of($- a $- b)) -`` {a}. negDivAlg(x))
lemma negDivAlg_eqn:
[| #0 $< b; a ∈ int; b ∈ int |] ==> negDivAlg(〈a, b〉) = (if #0 $≤ a $+ b then 〈#-1, a $+ b〉 else adjust(b, negDivAlg(〈a, #2 $× b〉)))
lemma negDivAlg_induct_lemma:
(!!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(〈a, #2 $× b〉) |] ==> P(〈a, b〉)) ==> 〈u, v〉 ∈ int × int --> P(〈u, v〉)
lemma negDivAlg_induct:
[| u ∈ int; v ∈ int; !!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(a, #2 $× b) |] ==> P(a, b) |] ==> P(u, v)
lemma negDivAlg_type:
[| a ∈ int; b ∈ int |] ==> negDivAlg(〈a, b〉) ∈ int × int
lemma negDivAlg_correct:
[| a ∈ int; b ∈ int; a $< #0; #0 $< b |] ==> quorem(〈a, b〉, negDivAlg(〈a, b〉))
lemma quorem_0:
[| b ≠ #0; b ∈ int |] ==> quorem(〈#0, b〉, 〈#0, #0〉)
lemma posDivAlg_zero_divisor:
posDivAlg(〈a, #0〉) = 〈#0, a〉
lemma posDivAlg_0:
posDivAlg(〈#0, b〉) = 〈#0, #0〉
lemma linear_arith_lemma:
¬ #0 $≤ #-1 $+ b ==> b $≤ #0
lemma negDivAlg_minus1:
negDivAlg(〈#-1, b〉) = 〈#-1, b $- #1〉
lemma negateSnd_eq:
negateSnd(〈q, r〉) = 〈q, $- r〉
lemma negateSnd_type:
qr ∈ int × int ==> negateSnd(qr) ∈ int × int
lemma quorem_neg:
[| quorem(〈$- a, $- b〉, qr); a ∈ int; b ∈ int; qr ∈ int × int |] ==> quorem(〈a, b〉, negateSnd(qr))
lemma divAlg_correct:
[| b ≠ #0; a ∈ int; b ∈ int |] ==> quorem(〈a, b〉, divAlg(〈a, b〉))
lemma divAlg_type:
[| a ∈ int; b ∈ int |] ==> divAlg(〈a, b〉) ∈ int × int
lemma zdiv_intify1:
intify(x) zdiv y = x zdiv y
lemma zdiv_intify2:
x zdiv intify(y) = x zdiv y
lemma zdiv_type:
z zdiv w ∈ int
lemma zmod_intify1:
intify(x) zmod y = x zmod y
lemma zmod_intify2:
x zmod intify(y) = x zmod y
lemma zmod_type:
z zmod w ∈ int
lemma DIVISION_BY_ZERO_ZDIV:
a zdiv #0 = #0
lemma DIVISION_BY_ZERO_ZMOD:
a zmod #0 = intify(a)
lemma raw_zmod_zdiv_equality:
[| a ∈ int; b ∈ int |] ==> a = b $× (a zdiv b) $+ a zmod b
lemma zmod_zdiv_equality:
intify(a) = b $× (a zdiv b) $+ a zmod b
lemma pos_mod:
#0 $< b ==> #0 $≤ a zmod b ∧ a zmod b $< b
lemmas pos_mod_sign:
#0 $< b ==> #0 $≤ a zmod b
and pos_mod_bound:
#0 $< b ==> a zmod b $< b
lemmas pos_mod_sign:
#0 $< b ==> #0 $≤ a zmod b
and pos_mod_bound:
#0 $< b ==> a zmod b $< b
lemma neg_mod:
b $< #0 ==> a zmod b $≤ #0 ∧ b $< a zmod b
lemmas neg_mod_sign:
b $< #0 ==> a zmod b $≤ #0
and neg_mod_bound:
b $< #0 ==> b $< a zmod b
lemmas neg_mod_sign:
b $< #0 ==> a zmod b $≤ #0
and neg_mod_bound:
b $< #0 ==> b $< a zmod b
lemma quorem_div_mod:
[| b ≠ #0; a ∈ int; b ∈ int |] ==> quorem(〈a, b〉, 〈a zdiv b, a zmod b〉)
lemma quorem_div:
[| quorem(〈a, b〉, 〈q, r〉); b ≠ #0; a ∈ int; b ∈ int; q ∈ int |] ==> a zdiv b = q
lemma quorem_mod:
[| quorem(〈a, b〉, 〈q, r〉); b ≠ #0; a ∈ int; b ∈ int; q ∈ int; r ∈ int |] ==> a zmod b = r
lemma zdiv_pos_pos_trivial_raw:
[| a ∈ int; b ∈ int; #0 $≤ a; a $< b |] ==> a zdiv b = #0
lemma zdiv_pos_pos_trivial:
[| #0 $≤ a; a $< b |] ==> a zdiv b = #0
lemma zdiv_neg_neg_trivial_raw:
[| a ∈ int; b ∈ int; a $≤ #0; b $< a |] ==> a zdiv b = #0
lemma zdiv_neg_neg_trivial:
[| a $≤ #0; b $< a |] ==> a zdiv b = #0
lemma zadd_le_0_lemma:
[| a $+ b $≤ #0; #0 $< a; #0 $< b |] ==> False
lemma zdiv_pos_neg_trivial_raw:
[| a ∈ int; b ∈ int; #0 $< a; a $+ b $≤ #0 |] ==> a zdiv b = #-1
lemma zdiv_pos_neg_trivial:
[| #0 $< a; a $+ b $≤ #0 |] ==> a zdiv b = #-1
lemma zmod_pos_pos_trivial_raw:
[| a ∈ int; b ∈ int; #0 $≤ a; a $< b |] ==> a zmod b = a
lemma zmod_pos_pos_trivial:
[| #0 $≤ a; a $< b |] ==> a zmod b = intify(a)
lemma zmod_neg_neg_trivial_raw:
[| a ∈ int; b ∈ int; a $≤ #0; b $< a |] ==> a zmod b = a
lemma zmod_neg_neg_trivial:
[| a $≤ #0; b $< a |] ==> a zmod b = intify(a)
lemma zmod_pos_neg_trivial_raw:
[| a ∈ int; b ∈ int; #0 $< a; a $+ b $≤ #0 |] ==> a zmod b = a $+ b
lemma zmod_pos_neg_trivial:
[| #0 $< a; a $+ b $≤ #0 |] ==> a zmod b = a $+ b
lemma zdiv_zminus_zminus_raw:
[| a ∈ int; b ∈ int |] ==> $- a zdiv $- b = a zdiv b
lemma zdiv_zminus_zminus:
$- a zdiv $- b = a zdiv b
lemma zmod_zminus_zminus_raw:
[| a ∈ int; b ∈ int |] ==> $- a zmod $- b = $- (a zmod b)
lemma zmod_zminus_zminus:
$- a zmod $- b = $- (a zmod b)
lemma self_quotient_aux1:
[| #0 $< a; a = r $+ a $× q; r $< a |] ==> #1 $≤ q
lemma self_quotient_aux2:
[| #0 $< a; a = r $+ a $× q; #0 $≤ r |] ==> q $≤ #1
lemma self_quotient:
[| quorem(〈a, a〉, 〈q, r〉); a ∈ int; q ∈ int; a ≠ #0 |] ==> q = #1
lemma self_remainder:
[| quorem(〈a, a〉, 〈q, r〉); a ∈ int; q ∈ int; r ∈ int; a ≠ #0 |] ==> r = #0
lemma zdiv_self_raw:
[| a ≠ #0; a ∈ int |] ==> a zdiv a = #1
lemma zdiv_self:
intify(a) ≠ #0 ==> a zdiv a = #1
lemma zmod_self_raw:
a ∈ int ==> a zmod a = #0
lemma zmod_self:
a zmod a = #0
lemma zdiv_zero:
#0 zdiv b = #0
lemma zdiv_eq_minus1:
#0 $< b ==> #-1 zdiv b = #-1
lemma zmod_zero:
#0 zmod b = #0
lemma zdiv_minus1:
#0 $< b ==> #-1 zdiv b = #-1
lemma zmod_minus1:
#0 $< b ==> #-1 zmod b = b $- #1
lemma zdiv_pos_pos:
[| #0 $< a; #0 $≤ b |] ==> a zdiv b = fst(posDivAlg(〈intify(a), intify(b)〉))
lemma zmod_pos_pos:
[| #0 $< a; #0 $≤ b |] ==> a zmod b = snd(posDivAlg(〈intify(a), intify(b)〉))
lemma zdiv_neg_pos:
[| a $< #0; #0 $< b |] ==> a zdiv b = fst(negDivAlg(〈intify(a), intify(b)〉))
lemma zmod_neg_pos:
[| a $< #0; #0 $< b |] ==> a zmod b = snd(negDivAlg(〈intify(a), intify(b)〉))
lemma zdiv_pos_neg:
[| #0 $< a; b $< #0 |] ==> a zdiv b = fst(negateSnd(negDivAlg(〈$- a, $- b〉)))
lemma zmod_pos_neg:
[| #0 $< a; b $< #0 |] ==> a zmod b = snd(negateSnd(negDivAlg(〈$- a, $- b〉)))
lemma zdiv_neg_neg:
[| a $< #0; b $≤ #0 |] ==> a zdiv b = fst(negateSnd(posDivAlg(〈$- a, $- b〉)))
lemma zmod_neg_neg:
[| a $< #0; b $≤ #0 |] ==> a zmod b = snd(negateSnd(posDivAlg(〈$- a, $- b〉)))
lemma zmod_1:
a zmod #1 = #0
lemma zdiv_1:
a zdiv #1 = intify(a)
lemma zmod_minus1_right:
a zmod #-1 = #0
lemma zdiv_minus1_right_raw:
a ∈ int ==> a zdiv #-1 = $- a
lemma zdiv_minus1_right:
a zdiv #-1 = $- a
lemma zdiv_mono1:
[| a $≤ a'; #0 $< b |] ==> a zdiv b $≤ a' zdiv b
lemma zdiv_mono1_neg:
[| a $≤ a'; b $< #0 |] ==> a' zdiv b $≤ a zdiv b
lemma q_pos_lemma:
[| #0 $≤ b' $× q' $+ r'; r' $< b'; #0 $< b' |] ==> #0 $≤ q'
lemma zdiv_mono2_lemma:
[| b $× q $+ r = b' $× q' $+ r'; #0 $≤ b' $× q' $+ r'; r' $< b'; #0 $≤ r; #0 $< b'; b' $≤ b |] ==> q $≤ q'
lemma zdiv_mono2_raw:
[| #0 $≤ a; #0 $< b'; b' $≤ b; a ∈ int |] ==> a zdiv b $≤ a zdiv b'
lemma zdiv_mono2:
[| #0 $≤ a; #0 $< b'; b' $≤ b |] ==> a zdiv b $≤ a zdiv b'
lemma q_neg_lemma:
[| b' $× q' $+ r' $< #0; #0 $≤ r'; #0 $< b' |] ==> q' $< #0
lemma zdiv_mono2_neg_lemma:
[| b $× q $+ r = b' $× q' $+ r'; b' $× q' $+ r' $< #0; r $< b; #0 $≤ r'; #0 $< b'; b' $≤ b |] ==> q' $≤ q
lemma zdiv_mono2_neg_raw:
[| a $< #0; #0 $< b'; b' $≤ b; a ∈ int |] ==> a zdiv b' $≤ a zdiv b
lemma zdiv_mono2_neg:
[| a $< #0; #0 $< b'; b' $≤ b |] ==> a zdiv b' $≤ a zdiv b
lemma zmult1_lemma:
[| quorem(〈b, c〉, 〈q, r〉); c ∈ int; c ≠ #0 |] ==> quorem(〈a $× b, c〉, 〈a $× q $+ a $× r zdiv c, a $× r zmod c〉)
lemma zdiv_zmult1_eq_raw:
[| b ∈ int; c ∈ int |] ==> a $× b zdiv c = a $× (b zdiv c) $+ a $× (b zmod c) zdiv c
lemma zdiv_zmult1_eq:
a $× b zdiv c = a $× (b zdiv c) $+ a $× (b zmod c) zdiv c
lemma zmod_zmult1_eq_raw:
[| b ∈ int; c ∈ int |] ==> a $× b zmod c = a $× (b zmod c) zmod c
lemma zmod_zmult1_eq:
a $× b zmod c = a $× (b zmod c) zmod c
lemma zmod_zmult1_eq':
a $× b zmod c = a zmod c $× b zmod c
lemma zmod_zmult_distrib:
a $× b zmod c = a zmod c $× (b zmod c) zmod c
lemma zdiv_zmult_self1:
intify(b) ≠ #0 ==> a $× b zdiv b = intify(a)
lemma zdiv_zmult_self2:
intify(b) ≠ #0 ==> b $× a zdiv b = intify(a)
lemma zmod_zmult_self1:
a $× b zmod b = #0
lemma zmod_zmult_self2:
b $× a zmod b = #0
lemma zadd1_lemma:
[| quorem(〈a, c〉, 〈aq, ar〉); quorem(〈b, c〉, 〈bq, br〉); c ∈ int; c ≠ #0 |] ==> quorem(〈a $+ b, c〉, 〈aq $+ bq $+ (ar $+ br) zdiv c, (ar $+ br) zmod c〉)
lemma zdiv_zadd1_eq_raw:
[| a ∈ int; b ∈ int; c ∈ int |] ==> (a $+ b) zdiv c = a zdiv c $+ b zdiv c $+ (a zmod c $+ b zmod c) zdiv c
lemma zdiv_zadd1_eq:
(a $+ b) zdiv c = a zdiv c $+ b zdiv c $+ (a zmod c $+ b zmod c) zdiv c
lemma zmod_zadd1_eq_raw:
[| a ∈ int; b ∈ int; c ∈ int |] ==> (a $+ b) zmod c = (a zmod c $+ b zmod c) zmod c
lemma zmod_zadd1_eq:
(a $+ b) zmod c = (a zmod c $+ b zmod c) zmod c
lemma zmod_div_trivial_raw:
[| a ∈ int; b ∈ int |] ==> a zmod b zdiv b = #0
lemma zmod_div_trivial:
a zmod b zdiv b = #0
lemma zmod_mod_trivial_raw:
[| a ∈ int; b ∈ int |] ==> a zmod b zmod b = a zmod b
lemma zmod_mod_trivial:
a zmod b zmod b = a zmod b
lemma zmod_zadd_left_eq:
(a $+ b) zmod c = (a zmod c $+ b) zmod c
lemma zmod_zadd_right_eq:
(a $+ b) zmod c = (a $+ b zmod c) zmod c
lemma zdiv_zadd_self1:
intify(a) ≠ #0 ==> (a $+ b) zdiv a = b zdiv a $+ #1
lemma zdiv_zadd_self2:
intify(a) ≠ #0 ==> (b $+ a) zdiv a = b zdiv a $+ #1
lemma zmod_zadd_self1:
(a $+ b) zmod a = b zmod a
lemma zmod_zadd_self2:
(b $+ a) zmod a = b zmod a
lemma zdiv_zmult2_aux1:
[| #0 $< c; b $< r; r $≤ #0 |] ==> b $× c $< b $× (q zmod c) $+ r
lemma zdiv_zmult2_aux2:
[| #0 $< c; b $< r; r $≤ #0 |] ==> b $× (q zmod c) $+ r $≤ #0
lemma zdiv_zmult2_aux3:
[| #0 $< c; #0 $≤ r; r $< b |] ==> #0 $≤ b $× (q zmod c) $+ r
lemma zdiv_zmult2_aux4:
[| #0 $< c; #0 $≤ r; r $< b |] ==> b $× (q zmod c) $+ r $< b $× c
lemma zdiv_zmult2_lemma:
[| quorem(〈a, b〉, 〈q, r〉); a ∈ int; b ∈ int; b ≠ #0; #0 $< c |] ==> quorem(〈a, b $× c〉, 〈q zdiv c, b $× (q zmod c) $+ r〉)
lemma zdiv_zmult2_eq_raw:
[| #0 $< c; a ∈ int; b ∈ int |] ==> a zdiv (b $× c) = a zdiv b zdiv c
lemma zdiv_zmult2_eq:
#0 $< c ==> a zdiv (b $× c) = a zdiv b zdiv c
lemma zmod_zmult2_eq_raw:
[| #0 $< c; a ∈ int; b ∈ int |] ==> a zmod (b $× c) = b $× (a zdiv b zmod c) $+ a zmod b
lemma zmod_zmult2_eq:
#0 $< c ==> a zmod (b $× c) = b $× (a zdiv b zmod c) $+ a zmod b
lemma zdiv_zmult_zmult1_aux1:
[| #0 $< b; intify(c) ≠ #0 |] ==> c $× a zdiv (c $× b) = a zdiv b
lemma zdiv_zmult_zmult1_aux2:
[| b $< #0; intify(c) ≠ #0 |] ==> c $× a zdiv (c $× b) = a zdiv b
lemma zdiv_zmult_zmult1_raw:
[| intify(c) ≠ #0; b ∈ int |] ==> c $× a zdiv (c $× b) = a zdiv b
lemma zdiv_zmult_zmult1:
intify(c) ≠ #0 ==> c $× a zdiv (c $× b) = a zdiv b
lemma zdiv_zmult_zmult2:
intify(c) ≠ #0 ==> a $× c zdiv (b $× c) = a zdiv b
lemma zmod_zmult_zmult1_aux1:
[| #0 $< b; intify(c) ≠ #0 |] ==> c $× a zmod (c $× b) = c $× (a zmod b)
lemma zmod_zmult_zmult1_aux2:
[| b $< #0; intify(c) ≠ #0 |] ==> c $× a zmod (c $× b) = c $× (a zmod b)
lemma zmod_zmult_zmult1_raw:
[| b ∈ int; c ∈ int |] ==> c $× a zmod (c $× b) = c $× (a zmod b)
lemma zmod_zmult_zmult1:
c $× a zmod (c $× b) = c $× (a zmod b)
lemma zmod_zmult_zmult2:
a $× c zmod (b $× c) = a zmod b $× c
lemma zdiv_neg_pos_less0:
[| a $< #0; #0 $< b |] ==> a zdiv b $< #0
lemma zdiv_nonneg_neg_le0:
[| #0 $≤ a; b $< #0 |] ==> a zdiv b $≤ #0
lemma pos_imp_zdiv_nonneg_iff:
#0 $< b ==> #0 $≤ a zdiv b <-> #0 $≤ a
lemma neg_imp_zdiv_nonneg_iff:
b $< #0 ==> #0 $≤ a zdiv b <-> a $≤ #0
lemma pos_imp_zdiv_neg_iff:
#0 $< b ==> a zdiv b $< #0 <-> a $< #0
lemma neg_imp_zdiv_neg_iff:
b $< #0 ==> a zdiv b $< #0 <-> #0 $< a