author eberlm Thu, 30 Nov 2017 17:00:19 +0100 changeset 67108 6b350c594ae3 parent 67107 cef76a19125e child 67109 5fce3a24e476
bij_betw lemma for prime powers
```--- a/src/HOL/Number_Theory/Prime_Powers.thy	Thu Nov 30 16:59:59 2017 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy	Thu Nov 30 17:00:19 2017 +0100
@@ -6,7 +6,7 @@
*)
section \<open>Prime powers\<close>
theory Prime_Powers
-  imports Complex_Main "HOL-Computational_Algebra.Primes"
+  imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet"
begin

definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
@@ -211,6 +211,37 @@
"prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
by (subst primepow_power_iff) auto

+lemma bij_betw_primepows:
+  "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring)
+     (Collect prime \<times> UNIV) (Collect primepow)"
+proof (rule bij_betwI [where ?g = "(\<lambda>n. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"],
+       goal_cases)
+  case 1
+  show "(\<lambda>(p, k). p ^ Suc k :: 'a) \<in> Collect prime \<times> UNIV \<rightarrow> Collect primepow"
+    by (auto intro!: primepow_prime_power simp del: power_Suc )
+next
+  case 2
+  show ?case
+    by (auto simp: primepow_def prime_aprimedivisor)
+next
+  case (3 n)
+  thus ?case
+    by (auto simp: aprimedivisor_prime_power simp del: power_Suc)
+next
+  case (4 n)
+  hence *: "0 < multiplicity (aprimedivisor n) n"
+    by (subst prime_multiplicity_gt_zero_iff)
+       (auto intro!: prime_imp_prime_elem aprimedivisor_dvd simp: primepow_def prime_aprimedivisor)
+  have "aprimedivisor n * aprimedivisor n ^ (multiplicity (aprimedivisor n) n - Suc 0) =
+          aprimedivisor n ^ Suc (multiplicity (aprimedivisor n) n - Suc 0)" by simp
+  also from * have "Suc (multiplicity (aprimedivisor n) n - Suc 0) =
+                      multiplicity (aprimedivisor n) n"
+    by (subst Suc_diff_Suc) (auto simp: prime_multiplicity_gt_zero_iff)
+  also have "aprimedivisor n ^ \<dots> = n"
+    using 4 by (subst primepow_decompose) auto
+  finally show ?case by auto
+qed
+
(* TODO Generalise *)
lemma primepow_multD:
assumes "primepow (a * b :: nat)"```