diff --git a/thys/Lucas_Theorem/Lucas_Theorem.thy b/thys/Lucas_Theorem/Lucas_Theorem.thy new file mode 100644 --- /dev/null +++ b/thys/Lucas_Theorem/Lucas_Theorem.thy @@ -0,0 +1,373 @@ +(* + Title: Lucas_Theorem.thy + Author: Chelsea Edmonds, University of Cambridge +*) + +theory Lucas_Theorem + imports Main "HOL-Computational_Algebra.Computational_Algebra" +begin + +notation fps_nth (infixl "$" 75) + +section \Extensions on Formal Power Series (FPS) Library\ + +text \This section presents a few extensions on the Formal Power Series (FPS) library, described in \cite{Chaieb2011} \ + +subsection \FPS Equivalence Relation \ + +text \ This proof requires reasoning around the equivalence of coefficients mod some prime number. +This section defines an equivalence relation on FPS using the pattern described by Paulson +in \cite{paulsonDefiningFunctionsEquivalence2006}, as well as some basic lemmas for reasoning around +how the equivalence holds after common operations are applied \ + +definition "fpsmodrel p \ { (f, g). \ n. (f $ n) mod p = (g $ n) mod p }" + +lemma fpsrel_iff [simp]: "(f, g) \ fpsmodrel p \ (\n. (f $ n) mod p = (g $ n) mod p)" + by (simp add: fpsmodrel_def) + +lemma fps_equiv: "equiv UNIV (fpsmodrel p)" +proof (rule equivI) + show "refl (fpsmodrel p)" by (simp add: refl_on_def fpsmodrel_def) + show "sym (fpsmodrel p)" by (simp add: sym_def fpsmodrel_def) + show "trans (fpsmodrel p)" by (intro transI) (simp add: fpsmodrel_def) +qed + +text \ Equivalence relation over multiplication \ + +lemma fps_mult_equiv_coeff: + fixes f g :: "('a :: {euclidean_ring_cancel}) fps" + assumes "(f, g) \ fpsmodrel p" + shows "(f*h)$n mod p = (g*h)$n mod p" +proof - + have "((f*h) $ n) mod p =(\i=0..n. (f$i mod p * h$(n - i) mod p) mod p) mod p" + using mod_sum_eq mod_mult_left_eq + by (simp add: fps_mult_nth mod_sum_eq mod_mult_left_eq) + also have "... = (\i=0..n. (g$i mod p * h$(n - i) mod p) mod p) mod p" + using assms by auto + also have "... = ((g*h) $ n) mod p" + by (simp add: mod_mult_left_eq mod_sum_eq fps_mult_nth) + thus ?thesis by (simp add: calculation) +qed + +lemma fps_mult_equiv: + fixes f g :: "('a :: {euclidean_ring_cancel}) fps" + assumes "(f, g) \ fpsmodrel p" + shows "(f*h, g*h) \ fpsmodrel p" + using fpsmodrel_def fps_mult_equiv_coeff assms by blast + + +text \ Equivalence relation over power operator \ +lemma fps_power_equiv: + fixes f g :: "('a :: {euclidean_ring_cancel}) fps" + fixes x :: nat + assumes "(f, g) \ fpsmodrel p" + shows "(f^x, g^x) \ fpsmodrel p" + using assms +proof (induct x) + case 0 + thus ?case by (simp add: fpsmodrel_def) +next + case (Suc x) + then have hyp: " \n. f^x $ n mod p = g ^x $ n mod p" + using fpsrel_iff by blast + thus ?case + proof - + have fact: "\n h. (g * h) $ n mod p = (f * h) $ n mod p" + by (metis assms fps_mult_equiv_coeff) + have "\n h. (g ^ x * h) $ n mod p = (f ^ x * h) $ n mod p" + by (simp add: fps_mult_equiv_coeff hyp) + then have "\n h. (h * g ^ x) $ n mod p = (h * f ^ x) $ n mod p" + by (simp add: mult.commute) + thus ?thesis + using fact by force + qed +qed + +subsection \Binomial Coefficients \ + +text \The @{term "fps_binomial"} definition in the formal power series uses the @{term "n gchoose k"} operator. It's +defined as being of type @{typ "'a :: field_char_0 fps"}, however the equivalence relation requires a type @{typ 'a} +that supports the modulo operator. +The proof of the binomial theorem based on FPS coefficients below uses the choose operator and does +not put bounds on the type of @{term "fps_X"}.\ + +lemma binomial_coeffs_induct: + fixes n k :: nat + shows "(1 + fps_X)^n $ k = of_nat(n choose k)" +proof (induct n arbitrary: k) + case 0 + thus ?case + by (metis binomial_eq_0_iff binomial_n_0 fps_nth_of_nat not_gr_zero of_nat_0 of_nat_1 power_0) +next + case h: (Suc n) + fix k + have start: "(1 + fps_X)^(n + 1) = (1 + fps_X) * (1 + fps_X)^n" by auto + show ?case + using One_nat_def Suc_eq_plus1 Suc_pred add.commute binomial_Suc_Suc binomial_n_0 + fps_mult_fps_X_plus_1_nth h.hyps neq0_conv start by (smt of_nat_add) +qed + +subsection \Freshman's Dream Lemma on FPS \ +text \ The Freshman's dream lemma modulo a prime number $p$ is a well known proof that $(1 + x^p) \equiv (1 + x)^p \mod p$\ + +text \ First prove that $\binom{p^n}{k} \equiv 0 \mod p$ for $k \ge 1$ and $k < p^n$. The eventual +proof only ended up requiring this with $n = 1$\ + +lemma pn_choose_k_modp_0: + fixes n k::nat + assumes "prime p" + "k \ 1 \ k \ p^n - 1" + "n > 0" + shows "(p^n choose k) mod p = 0" +proof - + have inequality: "k \ p^n" using assms (2) by arith + have choose_take_1: "((p^n - 1) choose ( k - 1))= fact (p^n - 1) div (fact (k - 1) * fact (p^n - k))" + using binomial_altdef_nat diff_le_mono inequality assms(2) by auto + have "k * (p^n choose k) = k * ((fact (p^n)) div (fact k * fact((p^n) - k)))" + using assms binomial_fact'[OF inequality] by auto + also have "... = k * fact (p^n) div (fact k * fact((p^n) - k))" + using binomial_fact_lemma div_mult_self_is_m fact_gt_zero inequality mult.assoc mult.commute + nat_0_less_mult_iff by smt + also have "... = k * fact (p^n) div (k * fact (k - 1) * fact((p^n) - k))" + by (metis assms(2) fact_nonzero fact_num_eq_if le0 le_antisym of_nat_id) + also have "... = fact (p^n) div (fact (k - 1) * fact((p^n) - k))" + using assms by auto + also have "... = ((p^n) * fact (p^n - 1)) div (fact (k - 1) * fact((p^n) - k))" + by (metis assms(2) fact_nonzero fact_num_eq_if inequality le0 le_antisym of_nat_id) + also have "... = (p^n) * (fact (p^n - 1) div (fact (k - 1) * fact((p^n) - k)))" + by (metis assms(2) calculation choose_take_1 neq0_conv not_one_le_zero times_binomial_minus1_eq) + finally have equality: "k * (p^n choose k) = p^n * ((p^n - 1) choose (k - 1))" + using assms(2) times_binomial_minus1_eq by auto + then have dvd_result: "p^n dvd (k * (p^n choose k))" by simp + have "\ (p^n dvd k)" + using assms (2) binomial_n_0 diff_diff_cancel nat_dvd_not_less neq0_conv by auto + then have "p dvd (p^n choose k)" + using mult.commute prime_imp_prime_elem prime_power_dvd_multD assms dvd_result by metis + thus "?thesis" by simp +qed + +text \ Applying the above lemma to the coefficients of $(1 + X)^p$, it is easy to show that all +coefficients other than the $0$th and $p$th will be $0$ \ + +lemma fps_middle_coeffs: + assumes "prime p" + "n \ 0 \ n \ p" + shows "((1 + fps_X :: int fps) ^p) $ n mod p = 0 mod p" +proof - + let ?f = "(1 + fps_X :: int fps)^p" + have "\ n. n > 0 \ n < p \ (p choose n) mod p = 0" using pn_choose_k_modp_0 + by (metis (no_types, lifting) add_le_imp_le_diff assms(1) diff_diff_cancel diff_is_0_eq' + discrete le_add_diff_inverse le_numeral_extra(4) power_one_right zero_le_one zero_less_one) + then have middle_0: "\ n. n > 0 \ n < p \ (?f $ n) mod p = 0" + using binomial_coeffs_induct by (metis of_nat_0 zmod_int) + have "\ n. n > p \ ?f $ n mod p = 0" + using binomial_eq_0_iff binomial_coeffs_induct mod_0 by (metis of_nat_eq_0_iff) + thus ?thesis using middle_0 assms(2) nat_neq_iff by auto +qed + +text \It follows that $(1+ X)^p$ is equivalent to $(1 + X^p)$ under our equivalence relation, +as required to prove the freshmans dream lemma. \ + +lemma fps_freshmans_dream: + assumes "prime p" + shows "(((1 + fps_X :: int fps ) ^p), (1 + (fps_X)^(p))) \ fpsmodrel p" +proof - + let ?f = "(1 + fps_X :: int fps)^p" + let ?g = "(1 + (fps_X :: int fps)^p)" + have all_f_coeffs: "\ n. n \ 0 \ n \ p \ ?f $ n mod p = 0 mod p" + using fps_middle_coeffs assms by blast + have "?g $ 0 = 1" using assms by auto + then have "?g $ 0 mod p = 1 mod p" + using int_ops(2) zmod_int assms by presburger + then have "?g $ p mod p = 1 mod p" using assms by auto + then have "\ n . ?f $ n mod p = ?g $ n mod p" + using all_f_coeffs by (simp add: binomial_coeffs_induct) + thus ?thesis using fpsrel_iff by blast +qed + +section \Lucas's Theorem Proof\ + +text \A formalisation of Lucas's theorem based on a generating function proof using the existing formal power series (FPS) Isabelle library\ + +subsection \Reasoning about Coefficients Helpers\ + +text \A generating function proof of Lucas's theorem relies on direct comparison between coefficients of FPS which requires a number +of helper lemmas to prove formally. In particular it compares the coefficients of +$(1 + X)^n \mod p$ to $(1 + X^p)^N * (1 + X) ^rn \mod p$, where $N = n / p$, and $rn = n \mod p$. +This section proves that the $k$th coefficient of $(1 + X^p)^N * (1 + X) ^rn = (N choose K) * (rn choose rk)$\ + +text \Applying the @{term "fps_compose"} operator enables reasoning about the coefficients of $(1 + X^p)^n$ +using the existing binomial theorem proof with $X^p$ instead of $X$.\ + +lemma fps_binomial_p_compose: + assumes "p \ 0" + shows "(1 + (fps_X:: ('a :: {idom} fps))^p)^n = ((1 + fps_X)^n) oo (fps_X^p)" +proof - + have "(1::'a fps) + fps_X ^ p = 1 + fps_X oo fps_X ^ p" + by (simp add: assms fps_compose_add_distrib) + then show ?thesis + by (simp add: assms fps_compose_power) +qed + +text \ Next the proof determines the value of the $k$th coefficient of $(1 + X^p)^N$. \ + +lemma fps_X_pow_binomial_coeffs: + assumes "prime p" + shows "(1 + (fps_X ::int fps)^p)^N $k = (if p dvd k then (N choose (k div p)) else 0)" +proof - + let ?fx = "(fps_X :: int fps)" + have "(1 + ?fx^p)^N $ k = (((1 + ?fx)^N) oo (?fx^p)) $k" + by (metis assms fps_binomial_p_compose not_prime_0) + also have "... = (\i=0..k.((1 + ?fx)^N)$i * ((?fx^p)^i$k))" + by (simp add: fps_compose_nth) + finally have coeffs: "(1 + ?fx^p)^N $ k = (\i=0..k. (N choose i) * ((?fx^(p*i))$k))" + using binomial_coeffs_induct sum.cong by (metis (no_types, lifting) power_mult) + thus ?thesis + proof (cases "p dvd k") + case False \ \$p$ does not divide $k$ implies the $k$th term has a coefficient of 0\ + have "\ i. \(p dvd k) \ (?fx^(p*i)) $ k = 0" + by auto + thus ?thesis using coeffs by (simp add: False) + next + case True \ \$p$ divides $k$ implies the $k$th term has a non-zero coefficient\ + have contained: "k div p \ {0.. k}" by simp + have "\ i. i \ k div p \ (?fx^(p*i)) $ k = 0" using assms by auto + then have notdivpis0: "\ i \ ({0 .. k} - {k div p}). (?fx^(p*i)) $ k = 0" by simp + have "(1 + ?fx^p)^N $ k = (N choose (k div p)) * (?fx^(p * (k div p))) $ k + (\i\({0..k} -{k div p}). (N choose i) * ((?fx^(p*i))$k))" + using contained coeffs sum.remove by (metis (no_types, lifting) finite_atLeastAtMost) + thus ?thesis using notdivpis0 True by simp + qed +qed + +text \ The final helper lemma proves the $k$th coefficient is equivalent to $\binom{?N}{?K}*\binom{?rn}{?rk}$ as required.\ +lemma fps_div_rep_coeffs: + assumes "prime p" + shows "((1 + (fps_X::int fps)^p)^(n div p) * (1 + fps_X)^(n mod p)) $ k = + ((n div p) choose (k div p)) * ((n mod p) choose (k mod p))" + (is "((1 + (fps_X::int fps)^p)^?N * (1 + fps_X)^?rn) $ k = (?N choose ?K) * (?rn choose ?rk)") +proof - + \ \Initial facts with results around representation and 0 valued terms\ + let ?fx = "fps_X :: int fps" + have krep: "k - ?rk = ?K*p" + by (simp add: minus_mod_eq_mult_div) + have rk_in_range: "?rk \ {0..k}" by simp + have "\ i \ p. (?rn choose i) = 0" + using binomial_eq_0_iff + by (metis assms(1) leD le_less_trans linorder_cases mod_le_divisor mod_less_divisor prime_gt_0_nat) + then have ptok0: "\ i \ {p..k}. ((?rn choose i) * (1 + ?fx^p)^?N $ (k - i)) = 0" + by simp + then have notrkis0: "\i \ {0.. k}. i \ ?rk \ (?rn choose i) * (1 + ?fx^p)^?N $ (k - i) = 0" + proof (cases "k < p") + case True \ \When $k < p$, it presents a side case with regards to range of reasoning\ + then have k_value: "k = ?rk" by simp + then have "\ i < k. \ (p dvd (k - i))" + using True by (metis diff_diff_cancel diff_is_0_eq dvd_imp_mod_0 less_imp_diff_less less_irrefl_nat mod_less) + then show ?thesis using fps_X_pow_binomial_coeffs assms(1) k_value by simp + next + case False + then have "\ i < p. i \ ?rk \ \(p dvd (k - i))" + using mod_nat_eqI by auto + then have "\ i \ {0.. ?rk \ (1 + ?fx^p)^?N $ (k - i) = 0" + using assms fps_X_pow_binomial_coeffs by simp + then show ?thesis using ptok0 by auto + qed + \ \Main body of the proof, using helper facts above\ + have "((1 + fps_X^p)^?N * (1 + fps_X)^?rn) $ k = (((1 + fps_X)^?rn) * (1 + fps_X^p)^?N) $ k" + by (metis (no_types, hide_lams) distrib_left distrib_right fps_mult_fps_X_commute fps_one_mult(1) + fps_one_mult(2) power_commuting_commutes) + also have "... = (\i=0..k.(of_nat(?rn choose i)) * ((1 + (fps_X)^p)^?N $ (k - i)))" + by (simp add: fps_mult_nth binomial_coeffs_induct) + also have "... = ((?rn choose ?rk) * (1 + ?fx^p)^?N $ (k - ?rk)) + (\i\({0..k} - {?rk}). (?rn choose i) * (1 + ?fx^p)^?N $ (k - i))" + using rk_in_range sum.remove by (metis (no_types, lifting) finite_atLeastAtMost) + finally have "((1 + ?fx^p)^?N * (1 + ?fx)^?rn) $ k = ((?rn choose ?rk) * (1 + ?fx^p)^?N $ (k - ?rk))" + using notrkis0 by simp + thus ?thesis using fps_X_pow_binomial_coeffs assms krep by auto +qed + +(* Lucas theorem proof *) +subsection \Lucas Theorem Proof\ + +text \ The proof of Lucas's theorem combines a generating function approach, based off \cite{Fine} with induction. +For formalisation purposes, it was easier to first prove a well known corollary of the main theorem (also +often presented as an alternative statement for Lucas's theorem), which can itself be used to backwards +prove the the original statement by induction. +This approach was adapted from P. Cameron's lecture notes on combinatorics \cite{petercameronNotesCombinatorics2007} \ + +subsubsection \ Proof of the Corollary \ +text \ This step makes use of the coefficient equivalence arguments proved in the previous sections \ +corollary lucas_corollary: + fixes n k :: nat + assumes "prime p" + shows "(n choose k) mod p = (((n div p) choose (k div p)) * ((n mod p) choose (k mod p))) mod p" + (is "(n choose k) mod p = ((?N choose ?K) * (?rn choose ?rk)) mod p") +proof - + let ?fx = "fps_X :: int fps" + have n_rep: "n = ?N * p + ?rn" + by simp + have k_rep: "k =?K * p + ?rk" by simp + have rhs_coeffs: "((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn)) $ k = (?N choose ?K) * (?rn choose ?rk)" + using assms fps_div_rep_coeffs k_rep n_rep by blast \ \Application of coefficient reasoning\ + have "((((1 + ?fx)^p)^(?N) * (1 + ?fx)^(?rn)), + ((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn))) \ fpsmodrel p" + using fps_freshmans_dream assms fps_mult_equiv fps_power_equiv by blast \ \Application of equivalence facts and freshmans dream lemma\ + then have modrel2: "((1 + ?fx)^n, ((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn))) + \ fpsmodrel p" + by (metis (mono_tags, hide_lams) mult_div_mod_eq power_add power_mult) + thus ?thesis + using fpsrel_iff binomial_coeffs_induct rhs_coeffs by (metis of_nat_eq_iff zmod_int) +qed + +subsubsection \ Proof of the Theorem \ + +text \The theorem statement requires a formalised way of referring to the base $p$ representation of a number. +We use a definition that specifies the $i$th digit of the base $p$ representation. This definition is originally +from the Hilbert's 10th Problem Formalisation project \cite{bayerDPRMTheoremIsabelle2019} which this work contributes to.\ +definition nth_digit_general :: "nat \ nat \ nat \ nat" where + "nth_digit_general num i base = (num div (base ^ i)) mod base" + +text \Applying induction on $d$, where $d$ is the highest power required in either $n$ or $k$'s base $p$ +representation, @{thm lucas_corollary} can be used to prove the original theorem.\ + +theorem lucas_theorem: + fixes n k d::nat +assumes "n < p ^ (Suc d)" +assumes "k < p ^ (Suc d)" +assumes "prime p" +shows "(n choose k) mod p = (\i\d. ((nth_digit_general n i p) choose (nth_digit_general k i p))) mod p" + using assms +proof (induct d arbitrary: n k) + case 0 + thus ?case using nth_digit_general_def assms by simp +next + case (Suc d) + \ \Representation Variables\ + let ?N = "n div p" + let ?K = "k div p" + let ?nr = "n mod p" + let ?kr = "k mod p" + \ \Required assumption facts\ + have Mlessthan: "?N < p ^ (Suc d)" + using less_mult_imp_div_less power_Suc2 assms(3) prime_ge_2_nat Suc.prems(1) by metis + have Nlessthan: "?K < p ^ (Suc d)" + using less_mult_imp_div_less power_Suc2 prime_ge_2_nat Suc.prems(2) assms(3) by metis + have shift_bounds_fact: "(\i=(Suc 0)..(Suc (d )). ((nth_digit_general n i p) choose (nth_digit_general k i p))) = + (\i=0..(d). (nth_digit_general n (Suc i) p) choose (nth_digit_general k (Suc i) p))" + using prod.shift_bounds_cl_Suc_ivl by blast \ \Product manipulation helper fact\ + have "(n choose k ) mod p = ((?N choose ?K) * (?nr choose ?kr)) mod p" + using lucas_corollary assms(3) by blast \ \Application of corollary\ + also have "...= ((\i\d. ((nth_digit_general ?N i p) choose (nth_digit_general ?K i p))) * (?nr choose ?kr)) mod p" + using Mlessthan Nlessthan Suc.hyps mod_mult_cong assms(3) by blast \ \Using Inductive Hypothesis\ + \ \Product manipulation steps\ + also have "... = ((\i=0..(d). (nth_digit_general n (Suc i) p) choose (nth_digit_general k (Suc i) p)) * (?nr choose ?kr)) mod p" + using atMost_atLeast0 nth_digit_general_def div_mult2_eq by auto + also have "... = ((\i=1..(d+1). (nth_digit_general n i p) choose (nth_digit_general k i p)) * + ((nth_digit_general n 0 p) choose (nth_digit_general k 0 p))) mod p" + using nth_digit_general_def shift_bounds_fact by simp + finally have "(n choose k ) mod p = ((\i=0..(d+1). (nth_digit_general n i p) choose (nth_digit_general k i p))) mod p" + using One_nat_def atMost_atLeast0 mult.commute prod.atLeast1_atMost_eq prod.atMost_shift + by (smt Suc_eq_plus1 shift_bounds_fact) + thus ?case + using Suc_eq_plus1 atMost_atLeast0 by presburger +qed + +end \ No newline at end of file diff --git a/thys/Lucas_Theorem/ROOT b/thys/Lucas_Theorem/ROOT new file mode 100644 --- /dev/null +++ b/thys/Lucas_Theorem/ROOT @@ -0,0 +1,10 @@ +chapter AFP + +session Lucas_Theorem (AFP) = "HOL-Computational_Algebra" + + options [timeout = 600] + theories + Lucas_Theorem + document_files + "root.bib" + "root.tex" + diff --git a/thys/Lucas_Theorem/document/root.bib b/thys/Lucas_Theorem/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Lucas_Theorem/document/root.bib @@ -0,0 +1,71 @@ + +@article{Chaieb2011, + title = {Formal Power Series}, + author = {Chaieb, Amine}, + year = {2011}, + month = oct, + volume = {47}, + pages = {291--318}, + issn = {1573-0670}, + doi = {10.1007/s10817-010-9195-9}, + journal = {Journal of Automated Reasoning}, + number = {3} +} + +@article{Fine, + title = {Binomial Coefficients modulo a Prime}, + author = {Fine, N. J.}, + year = {1947}, + volume = {54}, + pages = {589--592}, + publisher = {{Mathematical Association of America}}, + issn = {00029890, 19300972}, + journal = {The American Mathematical Monthly}, + number = {10} +} + +@article{paulsonDefiningFunctionsEquivalence2006, + title = {Defining {{Functions}} on {{Equivalence Classes}}}, + author = {Paulson, Lawrence C.}, + year = {2006}, + month = oct, + volume = {7}, + pages = {658--675}, + issn = {1529-3785, 1557-945X}, + doi = {10.1145/1183278.1183280}, + abstract = {A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are \textbackslash{}emph\{equivalence classes\}: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.}, + archivePrefix = {arXiv}, + eprint = {1907.07591}, + eprinttype = {arxiv}, + journal = {ACM Transactions on Computational Logic (TOCL)}, + keywords = {Computer Science - Logic in Computer Science,F.4.1,G.2.0}, + number = {4} +} + +@misc{petercameronNotesCombinatorics2007, + title = {Notes on {{Combinatorics}}}, + author = {{Peter Cameron}}, + year = {2007}, + publisher = {{Queen Mary University of London}}, + url = {http://www.maths.qmul.ac.uk/~pjc/notes/comb.pdf}, + howpublished = {\url{http://www.maths.qmul.ac.uk/~pjc/notes/comb.pdf}} +} + +@InProceedings{bayerDPRMTheoremIsabelle2019, + author = {Jonas Bayer and Marco David and Abhik Pal and Benedikt Stock and Dierk Schleicher}, + title = {{The DPRM Theorem in Isabelle (Short Paper)}}, + booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, + pages = {33:1--33:7}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-122-1}, + ISSN = {1868-8969}, + year = {2019}, + volume = {141}, + editor = {John Harrison and John O'Leary and Andrew Tolmach}, + publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, + address = {Dagstuhl, Germany}, + URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11088}, + URN = {urn:nbn:de:0030-drops-110883}, + doi = {10.4230/LIPIcs.ITP.2019.33}, + annote = {Keywords: DPRM theorem, Hilbert's tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification} +} diff --git a/thys/Lucas_Theorem/document/root.tex b/thys/Lucas_Theorem/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Lucas_Theorem/document/root.tex @@ -0,0 +1,66 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{amsmath} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Lucas's Theorem} +\author{Chelsea Edmonds} +\maketitle + +\begin{abstract} + This work presents a formalisation of a generating function proof for Lucas's theorem. We first outline extensions to the existing Formal Power Series (FPS) library, including an equivalence relation for coefficients modulo $n$, an alternate binomial theorem statement, and a formalised proof of the Freshman's dream (mod $p$) lemma. + + The second part of the work presents the formal proof of Lucas's Theorem. Working backwards, the formalisation first proves a well known corollary of the theorem which is easier to formalise and then applies induction to prove the original theorem statement. The proof of the corollary aims to provide a good example of a formalised generating function equivalence proof using the FPS library. The final theorem statement is intended to be integrated into the formalised proof of Hilbert's 10th Problem \cite{bayerDPRMTheoremIsabelle2019}. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,528 +1,529 @@ AODV Auto2_HOL Auto2_Imperative_HOL AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS AutoFocus-Stream Automatic_Refinement AxiomaticCategoryTheory BDD BNF_Operations Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BNF_CC Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Completeness Complete_Non_Orders Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series Discrete_Summation DiscretePricing DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Factored_Transition_System_Bounding Farkas FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Falling_Factorial_Sum FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrationality_J_Hancl Isabelle_C Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_to_DRA LTL_to_GBA LTL_Master_Theorem Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_KBOs Lambda_Free_RPOs Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Lambda_Free_EPO Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp +Lucas_Theorem MFMC_Countable MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MFODL_Monitor_Optimized MFOTL_Monitor MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multirelations Multi_Party_Computation Myhill-Nerode Name_Carrying_Type_Inference Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions Open_Induction OpSets Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinals_and_Cardinals Ordinary_Differential_Equations PCF PLM Pell POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Polynomial_Factorization Polynomial_Interpolation Polynomials Poincare_Bendixson Poincare_Disc Pop_Refinement Posix-Lexing Possibilistic_Noninterference Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Projective_Geometry Program-Conflict-Analysis Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Randomised_BSTs Random_Graph_Subgraph_Threshold Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_OCL Saturation_Framework Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Universal_Turing_Machine UPF UPF_Firewall UpDown_Scheme UTP Valuation VectorSpace VeriComp Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval WOOT_Strong_Eventual_Consistency Word_Lib WorkerWrapper XML Zeta_Function Zeta_3_Irrational ZFC_in_HOL pGCL