bij_betw lemma for prime powers
authoreberlm <eberlm@in.tum.de>
Thu Nov 30 17:00:19 2017 +0100 (7 months ago)
changeset 671086b350c594ae3
parent 67107 cef76a19125e
child 67109 5fce3a24e476
bij_betw lemma for prime powers
src/HOL/Number_Theory/Prime_Powers.thy
     1.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Thu Nov 30 16:59:59 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Thu Nov 30 17:00:19 2017 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  section \<open>Prime powers\<close>
     1.6  theory Prime_Powers
     1.7 -  imports Complex_Main "HOL-Computational_Algebra.Primes"
     1.8 +  imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet"
     1.9  begin
    1.10  
    1.11  definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
    1.12 @@ -211,6 +211,37 @@
    1.13      "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
    1.14    by (subst primepow_power_iff) auto
    1.15  
    1.16 +lemma bij_betw_primepows: 
    1.17 +  "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring) 
    1.18 +     (Collect prime \<times> UNIV) (Collect primepow)"
    1.19 +proof (rule bij_betwI [where ?g = "(\<lambda>n. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"], 
    1.20 +       goal_cases)
    1.21 +  case 1
    1.22 +  show "(\<lambda>(p, k). p ^ Suc k :: 'a) \<in> Collect prime \<times> UNIV \<rightarrow> Collect primepow"
    1.23 +    by (auto intro!: primepow_prime_power simp del: power_Suc )
    1.24 +next
    1.25 +  case 2
    1.26 +  show ?case
    1.27 +    by (auto simp: primepow_def prime_aprimedivisor)
    1.28 +next
    1.29 +  case (3 n)
    1.30 +  thus ?case
    1.31 +    by (auto simp: aprimedivisor_prime_power simp del: power_Suc)
    1.32 +next
    1.33 +  case (4 n)
    1.34 +  hence *: "0 < multiplicity (aprimedivisor n) n"
    1.35 +    by (subst prime_multiplicity_gt_zero_iff)
    1.36 +       (auto intro!: prime_imp_prime_elem aprimedivisor_dvd simp: primepow_def prime_aprimedivisor)
    1.37 +  have "aprimedivisor n * aprimedivisor n ^ (multiplicity (aprimedivisor n) n - Suc 0) =
    1.38 +          aprimedivisor n ^ Suc (multiplicity (aprimedivisor n) n - Suc 0)" by simp
    1.39 +  also from * have "Suc (multiplicity (aprimedivisor n) n - Suc 0) =
    1.40 +                      multiplicity (aprimedivisor n) n"
    1.41 +    by (subst Suc_diff_Suc) (auto simp: prime_multiplicity_gt_zero_iff)
    1.42 +  also have "aprimedivisor n ^ \<dots> = n"
    1.43 +    using 4 by (subst primepow_decompose) auto
    1.44 +  finally show ?case by auto
    1.45 +qed
    1.46 +
    1.47  (* TODO Generalise *)
    1.48  lemma primepow_multD:
    1.49    assumes "primepow (a * b :: nat)"