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
```