# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1512057619 -3600
# Node ID 6b350c594ae3973a56efc773cf68f8b0d95079ed
# Parent  cef76a19125ef194bd184854e78e1637f796351d
bij_betw lemma for prime powers

diff -r cef76a19125e -r 6b350c594ae3 src/HOL/Number_Theory/Prime_Powers.thy
--- 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)"