885 text {* @{term "op dvd"} is a partial order *} |
885 text {* @{term "op dvd"} is a partial order *} |
886 |
886 |
887 interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n" |
887 interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n" |
888 proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) |
888 proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) |
889 |
889 |
890 lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" |
890 lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" |
891 unfolding dvd_def |
891 unfolding dvd_def |
892 by (blast intro: diff_mult_distrib2 [symmetric]) |
892 by (blast intro: diff_mult_distrib2 [symmetric]) |
893 |
893 |
894 lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)" |
894 lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)" |
895 apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) |
895 apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) |
896 apply (blast intro: dvd_add) |
896 apply (blast intro: dvd_add) |
897 done |
897 done |
898 |
898 |
899 lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)" |
899 lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)" |
900 by (drule_tac m = m in nat_dvd_diff, auto) |
900 by (drule_tac m = m in dvd_diff_nat, auto) |
901 |
901 |
902 lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" |
902 lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" |
903 apply (rule iffI) |
903 apply (rule iffI) |
904 apply (erule_tac [2] dvd_add) |
904 apply (erule_tac [2] dvd_add) |
905 apply (rule_tac [2] dvd_refl) |
905 apply (rule_tac [2] dvd_refl) |
906 apply (subgoal_tac "n = (n+k) -k") |
906 apply (subgoal_tac "n = (n+k) -k") |
907 prefer 2 apply simp |
907 prefer 2 apply simp |
908 apply (erule ssubst) |
908 apply (erule ssubst) |
909 apply (erule nat_dvd_diff) |
909 apply (erule dvd_diff_nat) |
910 apply (rule dvd_refl) |
910 apply (rule dvd_refl) |
911 done |
911 done |
912 |
912 |
913 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n" |
913 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n" |
914 unfolding dvd_def |
914 unfolding dvd_def |