diff --git a/src/HOL/Library/Library.thy b/src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy +++ b/src/HOL/Library/Library.thy @@ -1,102 +1,103 @@ (*<*) theory Library imports AList Adhoc_Overloading BNF_Axiomatization BNF_Corec Bourbaki_Witt_Fixpoint Centered_Division Char_ord Code_Cardinality Code_Lazy Code_Test Combine_PER Complete_Partial_Order2 Conditional_Parametricity Confluence Confluent_Quotient Countable Countable_Complete_Lattices Countable_Set_Type Debug Diagonal_Subsequence Discrete Disjoint_Sets Disjoint_FSets Dlist Dual_Ordered_Lattice Equipollence Extended Extended_Nat Extended_Nonnegative_Real Extended_Real Finite_Map Float FSet FuncSet Function_Division Fun_Lexorder Going_To_Filter Groups_Big_Fun Indicator_Function Infinite_Set Infinite_Typeclass Interval Interval_Float IArray Landau_Symbols Lattice_Algebras Lattice_Constructions Linear_Temporal_Logic_on_Streams ListVector Lub_Glb Mapping Monad_Syntax More_List Multiset_Order NList Nonpos_Ints Numeral_Type Omega_Words_Fun Open_State_Syntax Option_ord Order_Continuity Parallel Pattern_Aliases Periodic_Fun Poly_Mapping Power_By_Squaring Preorder Product_Plus Quadratic_Discriminant Quotient_List Quotient_Option Quotient_Product Quotient_Set Quotient_Sum Quotient_Syntax Quotient_Type Ramsey + Real_Mod Reflection Rewrite Saturated Set_Algebras Set_Idioms Signed_Division State_Monad Stream Sorting_Algorithms Sublist Sum_of_Squares Transitive_Closure_Table Tree_Multiset Tree_Real Type_Length Uprod While_Combinator Word Z2 begin end (*>*) diff --git a/src/HOL/Library/Real_Mod.thy b/src/HOL/Library/Real_Mod.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Library/Real_Mod.thy @@ -0,0 +1,238 @@ +(* + File: HOL/Library/Real_Mod.thy + Authors: Manuel Eberl, University of Innsbruck +*) +section \Modulo and congruence on the reals\ +theory Real_Mod + imports Complex_Main +begin + +definition rmod :: "real \ real \ real" (infixl "rmod" 70) where + "x rmod y = x - \y\ * of_int \x / \y\\" + +lemma rmod_conv_frac: "y \ 0 \ x rmod y = frac (x / \y\) * \y\" + by (simp add: rmod_def frac_def algebra_simps) + +lemma rmod_conv_frac': "x rmod y = (if y = 0 then x else frac (x / \y\) * \y\)" + by (simp add: rmod_def frac_def algebra_simps) + +lemma rmod_rmod [simp]: "(x rmod y) rmod y = x rmod y" + by (simp add: rmod_conv_frac') + +lemma rmod_0_right [simp]: "x rmod 0 = x" + by (simp add: rmod_def) + +lemma rmod_less: "m > 0 \ x rmod m < m" + by (simp add: rmod_conv_frac' frac_lt_1) + +lemma rmod_less_abs: "m \ 0 \ x rmod m < \m\" + by (simp add: rmod_conv_frac' frac_lt_1) + +lemma rmod_le: "m > 0 \ x rmod m \ m" + by (intro less_imp_le rmod_less) + +lemma rmod_nonneg: "m \ 0 \ x rmod m \ 0" + unfolding rmod_def + by (metis abs_le_zero_iff diff_ge_0_iff_ge floor_divide_lower linorder_not_le mult.commute) + +lemma rmod_unique: + assumes "z \ {0..<\y\}" "x = z + of_int n * y" + shows "x rmod y = z" +proof - + have "(x - z) / y = of_int n" + using assms by auto + hence "(x - z) / \y\ = of_int ((if y > 0 then 1 else -1) * n)" + using assms(1) by (cases y "0 :: real" rule: linorder_cases) (auto split: if_splits) + also have "\ \ \" + by auto + finally have "frac (x / \y\) = z / \y\" + using assms(1) by (subst frac_unique_iff) (auto simp: field_simps) + thus ?thesis + using assms(1) by (auto simp: rmod_conv_frac') +qed + +lemma rmod_0 [simp]: "0 rmod z = 0" + by (simp add: rmod_def) + +lemma rmod_add: "(x rmod z + y rmod z) rmod z = (x + y) rmod z" +proof (cases "z = 0") + case [simp]: False + show ?thesis + proof (rule sym, rule rmod_unique) + define n where "n = (if z > 0 then 1 else -1) * (\x / \z\\ + \y / \z\\ + + \(x + y - (\z\ * real_of_int \x / \z\\ + \z\ * real_of_int \y / \z\\)) / \z\\)" + show "x + y = (x rmod z + y rmod z) rmod z + real_of_int n * z" + by (simp add: rmod_def algebra_simps n_def) + qed (auto simp: rmod_less_abs rmod_nonneg) +qed auto + +lemma rmod_diff: "(x rmod z - y rmod z) rmod z = (x - y) rmod z" +proof (cases "z = 0") + case [simp]: False + show ?thesis + proof (rule sym, rule rmod_unique) + define n where "n = (if z > 0 then 1 else -1) * (\x / \z\\ + + \(x + \z\ * real_of_int \y / \z\\ - (y + \z\ * real_of_int \x / \z\\)) / \z\\ - \y / \z\\)" + show "x - y = (x rmod z - y rmod z) rmod z + real_of_int n * z" + by (simp add: rmod_def algebra_simps n_def) + qed (auto simp: rmod_less_abs rmod_nonneg) +qed auto + +lemma rmod_self [simp]: "x rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_int [simp]: "(of_int n * x) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_nat [simp]: "(of_nat n * x) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_numeral [simp]: "(numeral n * x) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_int' [simp]: "(x * of_int n) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_nat' [simp]: "(x * of_nat n) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_self_multiple_numeral' [simp]: "(x * numeral n) rmod x = 0" + by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac) + +lemma rmod_idem [simp]: "x \ {0..<\y\} \ x rmod y = x" + by (rule rmod_unique[of _ _ _ 0]) auto + + + +definition rcong :: "real \ real \ real \ bool" (\(1[_ = _] '(' rmod _'))\) where + "[x = y] (rmod m) \ x rmod m = y rmod m" + +named_theorems rcong_intros + +lemma rcong_0_right [simp]: "[x = y] (rmod 0) \ x = y" + by (simp add: rcong_def) + +lemma rcong_0_iff: "[x = 0] (rmod m) \ x rmod m = 0" + and rcong_0_iff': "[0 = x] (rmod m) \ x rmod m = 0" + by (simp_all add: rcong_def) + +lemma rcong_refl [simp, intro!, rcong_intros]: "[x = x] (rmod m)" + by (simp add: rcong_def) + +lemma rcong_sym: "[y = x] (rmod m) \ [x = y] (rmod m)" + by (simp add: rcong_def) + +lemma rcong_sym_iff: "[y = x] (rmod m) \ [x = y] (rmod m)" + unfolding rcong_def by (simp add: eq_commute del: rmod_idem) + +lemma rcong_trans [trans]: "[x = y] (rmod m) \ [y = z] (rmod m) \ [x = z] (rmod m)" + by (simp add: rcong_def) + +lemma rcong_add [rcong_intros]: + "[a = b] (rmod m) \ [c = d] (rmod m) \ [a + c = b + d] (rmod m)" + unfolding rcong_def using rmod_add by metis + +lemma rcong_diff [rcong_intros]: + "[a = b] (rmod m) \ [c = d] (rmod m) \ [a - c = b - d] (rmod m)" + unfolding rcong_def using rmod_diff by metis + +lemma rcong_uminus [rcong_intros]: + "[a = b] (rmod m) \ [-a = -b] (rmod m)" + using rcong_diff[of 0 0 m a b] by simp + +lemma rcong_uminus_uminus_iff [simp]: "[-x = -y] (rmod m) \ [x = y] (rmod m)" + using rcong_uminus minus_minus by metis + +lemma rcong_uminus_left_iff: "[-x = y] (rmod m) \ [x = -y] (rmod m)" + using rcong_uminus minus_minus by metis + +lemma rcong_add_right_cancel [simp]: "[a + c = b + c] (rmod m) \ [a = b] (rmod m)" + using rcong_add[of a b m c c] rcong_add[of "a + c" "b + c" m "-c" "-c"] by auto + +lemma rcong_add_left_cancel [simp]: "[c + a = c + b] (rmod m) \ [a = b] (rmod m)" + by (subst (1 2) add.commute) simp + +lemma rcong_diff_right_cancel [simp]: "[a - c = b - c] (rmod m) \ [a = b] (rmod m)" + by (metis rcong_add_left_cancel uminus_add_conv_diff) + +lemma rcong_diff_left_cancel [simp]: "[c - a = c - b] (rmod m) \ [a = b] (rmod m)" + by (metis minus_diff_eq rcong_diff_right_cancel rcong_uminus_uminus_iff) + +lemma rcong_rmod_right_iff [simp]: "[a = (b rmod m)] (rmod m) \ [a = b] (rmod m)" + and rcong_rmod_left_iff [simp]: "[(a rmod m) = b] (rmod m) \ [a = b] (rmod m)" + by (simp_all add: rcong_def) + +lemma rcong_rmod_left [rcong_intros]: "[a = b] (rmod m) \ [(a rmod m) = b] (rmod m)" + and rcong_rmod_right [rcong_intros]: "[a = b] (rmod m) \ [a = (b rmod m)] (rmod m)" + by simp_all + +lemma rcong_mult_of_int_0_left_left [rcong_intros]: "[0 = of_int n * m] (rmod m)" + and rcong_mult_of_int_0_right_left [rcong_intros]: "[0 = m * of_int n] (rmod m)" + and rcong_mult_of_int_0_left_right [rcong_intros]: "[of_int n * m = 0] (rmod m)" + and rcong_mult_of_int_0_right_right [rcong_intros]: "[m * of_int n = 0] (rmod m)" + by (simp_all add: rcong_def) + +lemma rcong_altdef: "[a = b] (rmod m) \ (\n. b = a + of_int n * m)" +proof (cases "m = 0") + case False + show ?thesis + proof + assume "[a = b] (rmod m)" + hence "[a - b = b - b] (rmod m)" + by (intro rcong_intros) + hence "(a - b) rmod m = 0" + by (simp add: rcong_def) + then obtain n where "of_int n = (a - b) / \m\" + using False by (auto simp: rmod_conv_frac elim!: Ints_cases) + thus "\n. b = a + of_int n * m" using False + by (intro exI[of _ "if m > 0 then -n else n"]) (auto simp: field_simps) + next + assume "\n. b = a + of_int n * m" + then obtain n where n: "b = a + of_int n * m" + by auto + have "[a + 0 = a + of_int n * m] (rmod m)" + by (intro rcong_intros) + with n show "[a = b] (rmod m)" + by simp + qed +qed auto + +lemma rcong_conv_diff_rmod_eq_0: "[x = y] (rmod m) \ (x - y) rmod m = 0" + by (metis cancel_comm_monoid_add_class.diff_cancel rcong_0_iff rcong_diff_right_cancel) + +lemma rcong_imp_eq: + assumes "[x = y] (rmod m)" "\x - y\ < \m\" + shows "x = y" +proof - + from assms obtain n where n: "y = x + of_int n * m" + unfolding rcong_altdef by blast + have "of_int \n\ * \m\ = \x - y\" + by (simp add: n abs_mult) + also have "\ < 1 * \m\" + using assms(2) by simp + finally have "n = 0" + by (subst (asm) mult_less_cancel_right) auto + with n show ?thesis + by simp +qed + +lemma rcong_mult_modulus: + assumes "[a = b] (rmod (m / c))" "c \ 0" + shows "[a * c = b * c] (rmod m)" +proof - + from assms obtain k where k: "b = a + of_int k * (m / c)" + by (auto simp: rcong_altdef) + have "b * c = (a + of_int k * (m / c)) * c" + by (simp only: k) + also have "\ = a * c + of_int k * m" + using assms(2) by (auto simp: divide_simps) + finally show ?thesis + unfolding rcong_altdef by blast +qed + +lemma rcong_divide_modulus: + assumes "[a = b] (rmod (m * c))" "c \ 0" + shows "[a / c = b / c] (rmod m)" + using rcong_mult_modulus[of a b m "1 / c"] assms by (auto simp: field_simps) + +end \ No newline at end of file