# HG changeset patch # User paulson # Date 1640516487 0 # Node ID 9469d922368930243378b4337a59138110def174 # Parent 77a96ed74340d5685ecab27ead848b4e959b5398 Tiny additions inspired by Roth development diff -r 77a96ed74340 -r 9469d9223689 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Tue Dec 21 22:11:10 2021 +0100 +++ b/src/HOL/GCD.thy Sun Dec 26 11:01:27 2021 +0000 @@ -1637,6 +1637,26 @@ end +text \And some consequences: cancellation modulo @{term m}\ +lemma mult_mod_cancel_right: + fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}" + assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n" + shows "a mod m = b mod m" +proof - + have "m dvd (a*n - b*n)" + using eq mod_eq_dvd_iff by blast + then have "m dvd a-b" + by (metis \coprime m n\ coprime_dvd_mult_left_iff left_diff_distrib') + then show ?thesis + using mod_eq_dvd_iff by blast +qed + +lemma mult_mod_cancel_left: + fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}" + assumes "(n * a) mod m = (n * b) mod m" and "coprime m n" + shows "a mod m = b mod m" + by (metis assms mult.commute mult_mod_cancel_right) + subsection \GCD and LCM for multiplicative normalisation functions\ diff -r 77a96ed74340 -r 9469d9223689 src/HOL/Library/Nat_Bijection.thy --- a/src/HOL/Library/Nat_Bijection.thy Tue Dec 21 22:11:10 2021 +0100 +++ b/src/HOL/Library/Nat_Bijection.thy Sun Dec 26 11:01:27 2021 +0000 @@ -87,10 +87,10 @@ lemma bij_prod_decode: "bij prod_decode" by (rule bijI [OF inj_prod_decode surj_prod_decode]) -lemma prod_encode_eq: "prod_encode x = prod_encode y \ x = y" +lemma prod_encode_eq [simp]: "prod_encode x = prod_encode y \ x = y" by (rule inj_prod_encode [THEN inj_eq]) -lemma prod_decode_eq: "prod_decode x = prod_decode y \ x = y" +lemma prod_decode_eq [simp]: "prod_decode x = prod_decode y \ x = y" by (rule inj_prod_decode [THEN inj_eq]) diff -r 77a96ed74340 -r 9469d9223689 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Tue Dec 21 22:11:10 2021 +0100 +++ b/src/HOL/Set_Interval.thy Sun Dec 26 11:01:27 2021 +0000 @@ -22,6 +22,9 @@ lemma card_2_iff': "card S = 2 \ (\x\S. \y\S. x \ y \ (\z\S. z = x \ z = y))" by (auto simp: card_Suc_eq numeral_eq_Suc) +lemma card_3_iff: "card S = 3 \ (\x y z. S = {x,y,z} \ x \ y \ y \ z \ x \ z)" + by (fastforce simp: card_Suc_eq numeral_eq_Suc) + context ord begin