# HG changeset patch # User paulson # Date 1030207521 -7200 # Node ID a3d5d8b03d638e128ca10808c34be047350d8127 # Parent 36ee816b5ee3568b2d09fd5eb41f2e31f7707d38 conversion of ZF/IntDiv to Isar script diff -r 36ee816b5ee3 -r a3d5d8b03d63 src/ZF/Integ/IntDiv.thy --- a/src/ZF/Integ/IntDiv.thy Fri Aug 23 17:10:47 2002 +0200 +++ b/src/ZF/Integ/IntDiv.thy Sat Aug 24 18:45:21 2002 +0200 @@ -3,10 +3,35 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge -The division operators div, mod +The division operators div and mod (borrowed from the HOL equivalent) + +Here is the division algorithm in ML: + + fun posDivAlg (a,b) = + if a0 then posDivAlg (a,b) + else if a=0 then (0,0) + else negateSnd (negDivAlg (~a,~b)) + else + if 0 o" @@ -40,7 +65,7 @@ % f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b> else adjust(b, f ` ))" -(*for the general case b\\0*) +(*for the general case b\0*) constdefs negateSnd :: "i => i" @@ -58,10 +83,1845 @@ if #0$) else negateSnd (posDivAlg (<$-a,$-b>))" - zdiv :: [i,i]=>i (infixl "zdiv" 70) + zdiv :: "[i,i]=>i" (infixl "zdiv" 70) "a zdiv b == fst (divAlg ())" - zmod :: [i,i]=>i (infixl "zmod" 70) + zmod :: "[i,i]=>i" (infixl "zmod" 70) "a zmod b == snd (divAlg ())" + +(** 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$ nat |] ==> 0 $#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 (erule (1) notE impE) +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$ 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$ 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$ ((#0 $< k & m$ ((#0 $< k & m$ ((#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 (, ); quorem (, ); 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 (, ); quorem (, ); 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) +apply auto +done + + +subsection{*Correctness of posDivAlg, + the Division Algorithm for @{text "a\0"} and @{text "b>0"} *} + +lemma adjust_eq [simp]: + "adjust(b, ) = (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() = + (if a$ else adjust(b, posDivAlg ()))" +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() |] ==> P()" + shows " \ int*int --> P()" +apply (rule_tac a = "" in wf_induct) +apply (rule_tac A = "int*int" and f = "%.nat_of (a $- b $+ #1)" + in wf_measure) +apply clarify +apply (rule prem) +apply (drule_tac [3] x = " 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 "(%. P (x,y)) ()") +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() \ 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 (, posDivAlg())" +apply (rule_tac u = "a" and v = "b" in posDivAlg_induct) +apply auto + apply (simp_all add: quorem_def) + txt{*base case: a0*} + +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() = + (if #0 $<= a$+b then <#-1,a$+b> + else adjust(b, negDivAlg ()))" +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() |] + ==> P()" + shows " \ int*int --> P()" +apply (rule_tac a = "" in wf_induct) +apply (rule_tac A = "int*int" and f = "%.nat_of ($- a $- b)" + in wf_measure) +apply clarify +apply (rule prem) +apply (drule_tac [3] x = " 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 " (%. P (x,y)) ()") +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() \ 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 (, negDivAlg())" +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>)" +apply (rotate_tac -1) +apply (auto simp add: quorem_def neq_iff_zless) +done + +lemma posDivAlg_zero_divisor: "posDivAlg() = <#0,a>" +apply (subst posDivAlg_unfold) +apply (simp (no_asm)) +done + +lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>" +apply (subst posDivAlg_unfold) +apply (simp (no_asm) 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 () = " +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 (, 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 (, divAlg())" +apply (rotate_tac 1) +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() \ 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 (, )" +apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) +apply (rotate_tac 1) +apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound + neg_mod_sign neg_mod_bound) +done + +(*Surely quorem(,) implies a \ int, but it doesn't matter*) +lemma quorem_div: + "[| quorem(,); 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(,); 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 lemma1: "[| #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 lemma2: "[| #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 \ 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 lemma1) +apply (rule_tac a = "$-a" and r = "$-r" in lemma2) +apply (rule_tac [6] zminus_equation [THEN iffD1]) +apply (rule_tac [2] zminus_equation [THEN iffD1]) +apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+ +done + +lemma self_remainder: + "[|quorem(,); 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())" +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())" +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())" +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())" +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, 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(, ); c \ int; c \ #0 |] + ==> quorem (, )" +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(, ); quorem(, ); + c \ int; c \ #0 |] + ==> quorem (, )" +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 lemma1: + "[| #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 lemma2: + "[| #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 lemma3: + "[| #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 lemma4: + "[| #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 \ int; b \ int; b \ #0; #0 $< c |] + ==> quorem (, )" +apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def + neq_iff_zless int_0_less_mult_iff + zadd_zmult_distrib2 [symmetric] lemma1 lemma2 lemma3 lemma4) +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 lemma1: + "[| #0 $< b; intify(c) \ #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b" +apply (subst zdiv_zmult2_eq) +apply auto +done + +lemma lemma2: + "[| 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] lemma1) +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] lemma1 lemma2) +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 lemma1: + "[| #0 $< b; intify(c) \ #0 |] + ==> (c$*a) zmod (c$*b) = c $* (a zmod b)" +apply (subst zmod_zmult2_eq) +apply auto +done + +lemma lemma2: + "[| 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] lemma1) +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] lemma1 lemma2) +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 + diff -r 36ee816b5ee3 -r a3d5d8b03d63 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Fri Aug 23 17:10:47 2002 +0200 +++ b/src/ZF/IsaMakefile Sat Aug 24 18:45:21 2002 +0200 @@ -35,7 +35,7 @@ Fixedpt.thy Inductive.ML Inductive.thy \ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ - Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \ + Integ/IntDiv.thy Integ/int_arith.ML \ Let.ML Let.thy List.thy Main.ML Main.thy \ Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \ OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \