357 apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ") |
357 apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ") |
358 prefer 2 |
358 prefer 2 |
359 apply (erule zle_zless_trans) |
359 apply (erule zle_zless_trans) |
360 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) |
360 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) |
361 apply (erule zle_zless_trans) |
361 apply (erule zle_zless_trans) |
362 apply (simp add: ); |
362 apply simp |
363 apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)") |
363 apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)") |
364 prefer 2 |
364 prefer 2 |
365 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) |
365 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) |
366 apply (auto elim: zless_asym |
366 apply (auto elim: zless_asym |
367 simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls) |
367 simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls) |
428 |
428 |
429 lemma posDivAlg_induct_lemma [rule_format]: |
429 lemma posDivAlg_induct_lemma [rule_format]: |
430 assumes prem: |
430 assumes prem: |
431 "!!a b. [| a \<in> int; b \<in> int; |
431 "!!a b. [| a \<in> int; b \<in> int; |
432 ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)" |
432 ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)" |
433 shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)" |
433 shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)" |
434 apply (rule_tac a = "<u,v>" in wf_induct) |
434 using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"] |
435 apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)" |
435 proof (induct "<u,v>" arbitrary: u v rule: wf_induct) |
436 in wf_measure) |
436 case (step x) |
437 apply clarify |
437 hence uv: "u \<in> int" "v \<in> int" by auto |
438 apply (rule prem) |
438 thus ?case |
439 apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec) |
439 apply (rule prem) |
440 apply auto |
440 apply (rule impI) |
441 apply (simp add: not_zle_iff_zless posDivAlg_termination) |
441 apply (rule step) |
442 done |
442 apply (auto simp add: step uv not_zle_iff_zless posDivAlg_termination) |
|
443 done |
|
444 qed |
443 |
445 |
444 |
446 |
445 lemma posDivAlg_induct [consumes 2]: |
447 lemma posDivAlg_induct [consumes 2]: |
446 assumes u_int: "u \<in> int" |
448 assumes u_int: "u \<in> int" |
447 and v_int: "v \<in> int" |
449 and v_int: "v \<in> int" |
457 done |
459 done |
458 |
460 |
459 (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}. |
461 (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}. |
460 then this rewrite can work for all constants!!*) |
462 then this rewrite can work for all constants!!*) |
461 lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)" |
463 lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)" |
462 apply (simp (no_asm) add: int_eq_iff_zle) |
464 by (simp add: int_eq_iff_zle) |
463 done |
|
464 |
465 |
465 |
466 |
466 subsection{* Some convenient biconditionals for products of signs *} |
467 subsection{* Some convenient biconditionals for products of signs *} |
467 |
468 |
468 lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j" |
469 lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j" |
469 apply (drule zmult_zless_mono1) |
470 by (drule zmult_zless_mono1, auto) |
470 apply auto |
|
471 done |
|
472 |
471 |
473 lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j" |
472 lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j" |
474 apply (drule zmult_zless_mono1_neg) |
473 by (drule zmult_zless_mono1_neg, auto) |
475 apply auto |
|
476 done |
|
477 |
474 |
478 lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0" |
475 lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0" |
479 apply (drule zmult_zless_mono1_neg) |
476 by (drule zmult_zless_mono1_neg, auto) |
480 apply auto |
477 |
481 done |
|
482 |
478 |
483 (** Inequality reasoning **) |
479 (** Inequality reasoning **) |
484 |
480 |
485 lemma int_0_less_lemma: |
481 lemma int_0_less_lemma: |
486 "[| x \<in> int; y \<in> int |] |
482 "[| x \<in> int; y \<in> int |] |
589 lemma negDivAlg_induct_lemma [rule_format]: |
585 lemma negDivAlg_induct_lemma [rule_format]: |
590 assumes prem: |
586 assumes prem: |
591 "!!a b. [| a \<in> int; b \<in> int; |
587 "!!a b. [| a \<in> int; b \<in> int; |
592 ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] |
588 ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] |
593 ==> P(<a,b>)" |
589 ==> P(<a,b>)" |
594 shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)" |
590 shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)" |
595 apply (rule_tac a = "<u,v>" in wf_induct) |
591 using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"] |
596 apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)" |
592 proof (induct "<u,v>" arbitrary: u v rule: wf_induct) |
597 in wf_measure) |
593 case (step x) |
598 apply clarify |
594 hence uv: "u \<in> int" "v \<in> int" by auto |
599 apply (rule prem) |
595 thus ?case |
600 apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec) |
596 apply (rule prem) |
601 apply auto |
597 apply (rule impI) |
602 apply (simp add: not_zle_iff_zless negDivAlg_termination) |
598 apply (rule step) |
603 done |
599 apply (auto simp add: step uv not_zle_iff_zless negDivAlg_termination) |
|
600 done |
|
601 qed |
604 |
602 |
605 lemma negDivAlg_induct [consumes 2]: |
603 lemma negDivAlg_induct [consumes 2]: |
606 assumes u_int: "u \<in> int" |
604 assumes u_int: "u \<in> int" |
607 and v_int: "v \<in> int" |
605 and v_int: "v \<in> int" |
608 and ih: "!!a b. [| a \<in> int; b \<in> int; |
606 and ih: "!!a b. [| a \<in> int; b \<in> int; |
727 |
725 |
728 |
726 |
729 (** intify cancellation **) |
727 (** intify cancellation **) |
730 |
728 |
731 lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y" |
729 lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y" |
732 apply (simp (no_asm) add: zdiv_def) |
730 by (simp add: zdiv_def) |
733 done |
|
734 |
731 |
735 lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y" |
732 lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y" |
736 apply (simp (no_asm) add: zdiv_def) |
733 by (simp add: zdiv_def) |
737 done |
|
738 |
734 |
739 lemma zdiv_type [iff,TC]: "z zdiv w \<in> int" |
735 lemma zdiv_type [iff,TC]: "z zdiv w \<in> int" |
740 apply (unfold zdiv_def) |
736 apply (unfold zdiv_def) |
741 apply (blast intro: fst_type divAlg_type) |
737 apply (blast intro: fst_type divAlg_type) |
742 done |
738 done |
743 |
739 |
744 lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y" |
740 lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y" |
745 apply (simp (no_asm) add: zmod_def) |
741 by (simp add: zmod_def) |
746 done |
|
747 |
742 |
748 lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y" |
743 lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y" |
749 apply (simp (no_asm) add: zmod_def) |
744 by (simp add: zmod_def) |
750 done |
|
751 |
745 |
752 lemma zmod_type [iff,TC]: "z zmod w \<in> int" |
746 lemma zmod_type [iff,TC]: "z zmod w \<in> int" |
753 apply (unfold zmod_def) |
747 apply (unfold zmod_def) |
754 apply (rule snd_type) |
748 apply (rule snd_type) |
755 apply (blast intro: divAlg_type) |
749 apply (blast intro: divAlg_type) |
758 |
752 |
759 (** Arbitrary definitions for division by zero. Useful to simplify |
753 (** Arbitrary definitions for division by zero. Useful to simplify |
760 certain equations **) |
754 certain equations **) |
761 |
755 |
762 lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0" |
756 lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0" |
763 apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor) |
757 by (simp add: zdiv_def divAlg_def posDivAlg_zero_divisor) |
764 done (*NOT for adding to default simpset*) |
|
765 |
758 |
766 lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)" |
759 lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)" |
767 apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor) |
760 by (simp add: zmod_def divAlg_def posDivAlg_zero_divisor) |
768 done (*NOT for adding to default simpset*) |
|
769 |
|
770 |
761 |
771 |
762 |
772 (** Basic laws about division and remainder **) |
763 (** Basic laws about division and remainder **) |
773 |
764 |
774 lemma raw_zmod_zdiv_equality: |
765 lemma raw_zmod_zdiv_equality: |
1019 |
1010 |
1020 |
1011 |
1021 subsection{* Computation of division and remainder *} |
1012 subsection{* Computation of division and remainder *} |
1022 |
1013 |
1023 lemma zdiv_zero [simp]: "#0 zdiv b = #0" |
1014 lemma zdiv_zero [simp]: "#0 zdiv b = #0" |
1024 apply (simp (no_asm) add: zdiv_def divAlg_def) |
1015 by (simp add: zdiv_def divAlg_def) |
1025 done |
|
1026 |
1016 |
1027 lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1" |
1017 lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1" |
1028 apply (simp (no_asm_simp) add: zdiv_def divAlg_def) |
1018 by (simp (no_asm_simp) add: zdiv_def divAlg_def) |
1029 done |
|
1030 |
1019 |
1031 lemma zmod_zero [simp]: "#0 zmod b = #0" |
1020 lemma zmod_zero [simp]: "#0 zmod b = #0" |
1032 apply (simp (no_asm) add: zmod_def divAlg_def) |
1021 by (simp add: zmod_def divAlg_def) |
1033 done |
|
1034 |
1022 |
1035 lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1" |
1023 lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1" |
1036 apply (simp (no_asm_simp) add: zdiv_def divAlg_def) |
1024 by (simp add: zdiv_def divAlg_def) |
1037 done |
|
1038 |
1025 |
1039 lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1" |
1026 lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1" |
1040 apply (simp (no_asm_simp) add: zmod_def divAlg_def) |
1027 by (simp add: zmod_def divAlg_def) |
1041 done |
|
1042 |
1028 |
1043 (** a positive, b positive **) |
1029 (** a positive, b positive **) |
1044 |
1030 |
1045 lemma zdiv_pos_pos: "[| #0 $< a; #0 $<= b |] |
1031 lemma zdiv_pos_pos: "[| #0 $< a; #0 $<= b |] |
1046 ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))" |
1032 ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))" |
1348 apply (rule zmod_zmult1_eq' [THEN trans]) |
1334 apply (rule zmod_zmult1_eq' [THEN trans]) |
1349 apply (rule zmod_zmult1_eq) |
1335 apply (rule zmod_zmult1_eq) |
1350 done |
1336 done |
1351 |
1337 |
1352 lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)" |
1338 lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)" |
1353 apply (simp (no_asm_simp) add: zdiv_zmult1_eq) |
1339 by (simp add: zdiv_zmult1_eq) |
1354 done |
|
1355 |
1340 |
1356 lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)" |
1341 lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)" |
1357 apply (subst zmult_commute , erule zdiv_zmult_self1) |
1342 by (simp add: zmult_commute) |
1358 done |
|
1359 |
1343 |
1360 lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0" |
1344 lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0" |
1361 apply (simp (no_asm) add: zmod_zmult1_eq) |
1345 by (simp add: zmod_zmult1_eq) |
1362 done |
|
1363 |
1346 |
1364 lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0" |
1347 lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0" |
1365 apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq) |
1348 by (simp add: zmult_commute zmod_zmult1_eq) |
1366 done |
|
1367 |
1349 |
1368 |
1350 |
1369 (** proving (a$+b) zdiv c = |
1351 (** proving (a$+b) zdiv c = |
1370 a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **) |
1352 a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **) |
1371 |
1353 |