src/HOL/Number_Theory/Factorial_Ring.thy
author haftmann
Mon Jul 27 22:44:02 2015 +0200 (2015-07-27)
changeset 60804 080a979a985b
child 62348 9a5f43dac883
permissions -rw-r--r--
formal class for factorial (semi)rings
     1 (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Factorial (semi)rings\<close>
     6 
     7 theory Factorial_Ring
     8 imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
     9 begin
    10 
    11 context algebraic_semidom
    12 begin
    13 
    14 lemma is_unit_mult_iff:
    15   "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
    16   by (auto dest: dvd_mult_left dvd_mult_right)
    17 
    18 lemma is_unit_power_iff:
    19   "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
    20   by (induct n) (auto simp add: is_unit_mult_iff)
    21   
    22 lemma subset_divisors_dvd:
    23   "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
    24   by (auto simp add: subset_iff intro: dvd_trans)
    25 
    26 lemma strict_subset_divisors_dvd:
    27   "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
    28   by (auto simp add: subset_iff intro: dvd_trans)
    29 
    30 end
    31 
    32 class factorial_semiring = normalization_semidom +
    33   assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
    34   fixes is_prime :: "'a \<Rightarrow> bool"
    35   assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
    36     and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
    37     and no_prime_divisorsI: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
    38   assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
    39     and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    40 begin
    41 
    42 lemma not_is_prime_one [simp]:
    43   "\<not> is_prime 1"
    44   by (auto dest: is_prime_not_unit)
    45 
    46 lemma is_prime_not_zeroI:
    47   assumes "is_prime p"
    48   shows "p \<noteq> 0"
    49   using assms by (auto intro: ccontr)
    50 
    51 lemma is_prime_multD:
    52   assumes "is_prime (a * b)"
    53   shows "is_unit a \<or> is_unit b"
    54 proof -
    55   from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
    56   moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
    57     by auto
    58   ultimately show ?thesis
    59     using dvd_times_left_cancel_iff [of a b 1]
    60       dvd_times_right_cancel_iff [of b a 1]
    61     by auto
    62 qed
    63 
    64 lemma is_primeD2:
    65   assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
    66   shows "p dvd a"
    67 proof -
    68   from \<open>a dvd p\<close> obtain b where "p = a * b" ..
    69   with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
    70   with \<open>p = a * b\<close> show ?thesis
    71     by (auto simp add: mult_unit_dvd_iff)
    72 qed
    73 
    74 lemma is_prime_mult_unit_left:
    75   assumes "is_prime p"
    76     and "is_unit a"
    77   shows "is_prime (a * p)"
    78 proof (rule is_primeI)
    79   from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
    80     by (auto simp add: is_unit_mult_iff is_prime_not_unit)
    81   show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
    82   proof -
    83     from that \<open>is_unit a\<close> have "b dvd p"
    84       using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
    85     with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
    86       using is_primeD2 [of p b] by auto
    87     with \<open>is_unit a\<close> show ?thesis
    88       using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
    89   qed
    90 qed
    91 
    92 lemma is_primeI2:
    93   assumes "p \<noteq> 0"
    94   assumes "\<not> is_unit p"
    95   assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    96   shows "is_prime p"
    97 using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
    98   fix a
    99   assume "a dvd p"
   100   then obtain b where "p = a * b" ..
   101   with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
   102   moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
   103   moreover assume "\<not> is_unit a"
   104   ultimately show "p dvd a"
   105     using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
   106 qed    
   107 
   108 lemma not_is_prime_divisorE:
   109   assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
   110   obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
   111 proof -
   112   from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
   113     by (auto intro: is_primeI)
   114   with that show thesis by blast
   115 qed
   116 
   117 lemma prime_divisorE:
   118   assumes "a \<noteq> 0" and "\<not> is_unit a" 
   119   obtains p where "is_prime p" and "p dvd a"
   120   using assms no_prime_divisorsI [of a] by blast
   121 
   122 lemma prime_dvd_mult_iff:  
   123   assumes "is_prime p"
   124   shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   125   using assms by (auto dest: is_primeD)
   126 
   127 lemma prime_dvd_power_iff:
   128   assumes "is_prime p"
   129   shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   130   using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
   131 
   132 lemma is_prime_normalize_iff [simp]:
   133   "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
   134 proof
   135   assume ?Q show ?P
   136     by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
   137 next
   138   assume ?P show ?Q
   139     by (rule is_primeI)
   140       (insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \<open>?P\<close>, simp_all)
   141 qed  
   142 
   143 lemma is_prime_inj_power:
   144   assumes "is_prime p"
   145   shows "inj (op ^ p)"
   146 proof (rule injI, rule ccontr)
   147   fix m n :: nat
   148   have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
   149   proof
   150     assume ?Q then show ?P by simp
   151   next
   152     assume ?P then have "is_unit (p ^ q)" by simp
   153     with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
   154   qed
   155   have *: False if "p ^ m = p ^ n" and "m > n" for m n
   156   proof -
   157     from assms have "p \<noteq> 0"
   158       by (rule is_prime_not_zeroI)
   159     then have "p ^ n \<noteq> 0"
   160       by (induct n) simp_all
   161     from that have "m = n + (m - n)" and "m - n > 0" by arith+
   162     then obtain q where "m = n + q" and "q > 0" ..
   163     with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
   164     with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
   165       using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
   166     with \<open>q > 0\<close> show ?thesis by simp
   167   qed 
   168   assume "m \<noteq> n"
   169   then have "m > n \<or> m < n" by arith
   170   moreover assume "p ^ m = p ^ n"
   171   ultimately show False using * [of m n] * [of n m] by auto
   172 qed
   173 
   174 lemma prime_unique:
   175   assumes "is_prime q" and "is_prime p" and "q dvd p"
   176   shows "normalize q = normalize p"
   177 proof -
   178   from assms have "p dvd q"
   179     by (auto dest: is_primeD2 [of p] is_prime_not_unit [of q])
   180   with assms show ?thesis
   181     by (auto intro: associatedI)
   182 qed  
   183 
   184 lemma exists_factorization:
   185   assumes "a \<noteq> 0"
   186   obtains P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize a"
   187 proof -
   188   let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
   189   have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}" by auto
   190   moreover from assms have "finite {b. b dvd a \<and> normalize b = b}"
   191     by (rule finite_divisors)
   192   ultimately have "finite (?prime_factors a)" by (rule finite_subset)
   193   then show thesis using \<open>a \<noteq> 0\<close> that proof (induct "?prime_factors a" arbitrary: thesis a)
   194     case empty then have
   195       P: "\<And>b. is_prime b \<Longrightarrow> b dvd a \<Longrightarrow> normalize b \<noteq> b" and "a \<noteq> 0"
   196       by auto
   197     have "is_unit a"
   198     proof (rule no_prime_divisorsI)
   199       fix b
   200       assume "b dvd a"
   201       then show "\<not> is_prime b"
   202         using P [of "normalize b"] by auto
   203     qed
   204     then have "\<And>p. p \<in># {#} \<Longrightarrow> is_prime p" and "msetprod {#} = normalize a"
   205       by (simp_all add: is_unit_normalize)
   206     with empty show thesis by blast
   207   next
   208     case (insert p P)
   209     from \<open>insert p P = ?prime_factors a\<close>
   210     have "p dvd a" and "is_prime p" and "normalize p = p"
   211       by auto
   212     obtain n where "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
   213     proof (rule that)
   214       def N \<equiv> "{n. p ^ n dvd a}"
   215       from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
   216       then have "inj_on (op ^ p) U" for U
   217         by (rule subset_inj_on) simp
   218       moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
   219         by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
   220       ultimately have "finite N"
   221         by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
   222       from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
   223       then have "N \<noteq> {}" by blast
   224       note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
   225       from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
   226       with * show "Max N > 0"
   227         by (auto simp add: Max_gr_iff)
   228       from * have "Max N \<in> N" by (rule Max_in)
   229       then show "p ^ Max N dvd a" by (simp add: N_def)
   230       from * have "\<forall>n\<in>N. n \<le> Max N"
   231         by (simp add: Max_le_iff [symmetric])
   232       then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
   233         by (rule bspec) (simp add: N_def)
   234       then show "\<not> p ^ Suc (Max N) dvd a"
   235         by auto
   236     qed
   237     from \<open>p ^ n dvd a\<close> obtain c where "a = p ^ n * c" ..
   238     with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd c"
   239       by (auto elim: dvdE simp add: ac_simps)
   240     have "?prime_factors a - {p} = ?prime_factors c" (is "?A = ?B")
   241     proof (rule set_eqI)
   242       fix q
   243       show "q \<in> ?A \<longleftrightarrow> q \<in> ?B"
   244       using \<open>normalize p = p\<close> \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>\<not> p dvd c\<close>
   245         prime_unique [of q p]
   246         by (auto simp add: prime_dvd_power_iff prime_dvd_mult_iff)
   247     qed
   248     moreover from insert have "P = ?prime_factors a - {p}"
   249       by auto
   250     ultimately have "P = ?prime_factors c"
   251       by simp
   252     moreover from \<open>a \<noteq> 0\<close> \<open>a = p ^ n * c\<close> have "c \<noteq> 0"
   253       by auto
   254     ultimately obtain P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize c"
   255       using insert(3) by blast 
   256     with \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>normalize p = p\<close>
   257     have "\<And>q. q \<in># P + (replicate_mset n p) \<longrightarrow> is_prime q" "msetprod (P + replicate_mset n p) = normalize a"
   258       by (auto simp add: ac_simps normalize_mult normalize_power)
   259     with insert(6) show thesis by blast
   260   qed
   261 qed
   262   
   263 end
   264 
   265 instantiation nat :: factorial_semiring
   266 begin
   267 
   268 definition is_prime_nat :: "nat \<Rightarrow> bool"
   269 where
   270   "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
   271 
   272 lemma is_prime_eq_prime:
   273   "is_prime = prime"
   274   by (simp add: fun_eq_iff prime_def is_prime_nat_def)
   275 
   276 instance proof
   277   show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
   278   show "\<not> is_unit p" if "is_prime p" for p :: nat
   279     using that by (simp add: is_prime_nat_def)
   280 next
   281   fix p :: nat
   282   assume "p \<noteq> 0" and "\<not> is_unit p"
   283   then have "p > 1" by simp
   284   assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
   285   have "n = 1" if "n dvd p" "n \<noteq> p" for n
   286   proof (rule ccontr)
   287     assume "n \<noteq> 1"
   288     with that P have "p dvd n" by auto
   289     with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
   290     with that show False by simp
   291   qed
   292   with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
   293 next
   294   fix p m n :: nat
   295   assume "is_prime p"
   296   then have "prime p" by (simp add: is_prime_eq_prime)
   297   moreover assume "p dvd m * n"
   298   ultimately show "p dvd m \<or> p dvd n"
   299     by (rule prime_dvd_mult_nat)
   300 next
   301   fix n :: nat
   302   show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
   303     using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
   304 qed simp
   305 
   306 end
   307 
   308 instantiation int :: factorial_semiring
   309 begin
   310 
   311 definition is_prime_int :: "int \<Rightarrow> bool"
   312 where
   313   "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
   314 
   315 lemma is_prime_int_iff [simp]:
   316   "is_prime (int n) \<longleftrightarrow> is_prime n"
   317   by (simp add: is_prime_int_def)
   318 
   319 lemma is_prime_nat_abs_iff [simp]:
   320   "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
   321   by (simp add: is_prime_int_def)
   322 
   323 instance proof
   324   show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
   325   show "\<not> is_unit p" if "is_prime p" for p :: int
   326     using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
   327 next
   328   fix p :: int
   329   assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
   330   have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
   331   proof -
   332     from that have "int n dvd p" by (simp add: int_dvd_iff)
   333     moreover from that have "\<not> is_unit (int n)" by simp
   334     ultimately have "p dvd int n" by (rule P)
   335     with that have "p dvd int n" by auto
   336     then show ?thesis by (simp add: dvd_int_iff)
   337   qed
   338   moreover assume "p \<noteq> 0" and "\<not> is_unit p"
   339   ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
   340   then show "is_prime p" by simp
   341 next
   342   fix p k l :: int
   343   assume "is_prime p"
   344   then have *: "is_prime (nat \<bar>p\<bar>)" by simp
   345   assume "p dvd k * l"
   346   then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
   347     by (simp add: dvd_int_iff)
   348   then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
   349     by (simp add: abs_mult nat_mult_distrib)
   350   with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
   351     using is_primeD [of "nat \<bar>p\<bar>"] by auto
   352   then show "p dvd k \<or> p dvd l"
   353     by (simp add: dvd_int_iff)
   354 next
   355   fix k :: int
   356   assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
   357   have "is_unit (nat \<bar>k\<bar>)"
   358   proof (rule no_prime_divisorsI)
   359     fix m
   360     assume "m dvd nat \<bar>k\<bar>"
   361     then have "int m dvd k" by (simp add: int_dvd_iff)
   362     then have "\<not> is_prime (int m)" by (rule P)
   363     then show "\<not> is_prime m" by simp
   364   qed
   365   then show "is_unit k" by simp
   366 qed simp
   367 
   368 end
   369 
   370 end