author wenzelm Fri Jun 19 23:40:46 2015 +0200 (2015-06-19) changeset 60527 eb431a5651fe parent 60526 fad653acf58f child 60528 190b4a7d8b87
tuned proofs;
     1.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 21:41:33 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 23:40:46 2015 +0200
1.3 @@ -20,6 +20,7 @@
1.4
1.5  end
1.6
1.7 +
1.8  subsection \<open>Main corpus\<close>
1.9
1.10  text \<open>The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}.\<close>
1.11 @@ -59,21 +60,19 @@
1.12
1.13
1.14  text \<open>Marking out multiples in a sieve\<close>
1.15 -
1.16 +
1.17  definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks"
1.18  where
1.19    "mark_out n bs = map (\<lambda>(q, b). b \<and> \<not> Suc n dvd Suc (Suc q)) (enumerate n bs)"
1.20
1.21 -lemma mark_out_Nil [simp]:
1.22 -  "mark_out n [] = []"
1.23 +lemma mark_out_Nil [simp]: "mark_out n [] = []"
1.25 -
1.26 -lemma length_mark_out [simp]:
1.27 -  "length (mark_out n bs) = length bs"
1.28 +
1.29 +lemma length_mark_out [simp]: "length (mark_out n bs) = length bs"
1.31
1.32  lemma numbers_of_marks_mark_out:
1.33 -  "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
1.34 +    "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
1.35    by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
1.36      nth_enumerate_eq less_eq_dvd_minus)
1.37
1.38 @@ -85,36 +84,36 @@
1.39    "mark_out_aux n m bs =
1.40      map (\<lambda>(q, b). b \<and> (q < m + n \<or> \<not> Suc n dvd Suc (Suc q) + (n - m mod Suc n))) (enumerate n bs)"
1.41
1.42 -lemma mark_out_code [code]:
1.43 -  "mark_out n bs = mark_out_aux n n bs"
1.44 +lemma mark_out_code [code]: "mark_out n bs = mark_out_aux n n bs"
1.45  proof -
1.46 -  { fix a
1.47 -    assume A: "Suc n dvd Suc (Suc a)"
1.48 -      and B: "a < n + n"
1.49 -      and C: "n \<le> a"
1.50 -    have False
1.51 -    proof (cases "n = 0")
1.52 -      case True with A B C show False by simp
1.53 -    next
1.54 -      def m \<equiv> "Suc n" then have "m > 0" by simp
1.55 -      case False then have "n > 0" by simp
1.56 -      from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
1.57 -      have "q > 0"
1.58 -      proof (rule ccontr)
1.59 -        assume "\<not> q > 0"
1.60 -        with q show False by simp
1.61 -      qed
1.62 -      with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
1.63 -      with q have a: "a = Suc n * q - 2" by simp
1.64 -      with B have "q + n * q < n + n + 2"
1.65 -        by auto
1.66 -      then have "m * q < m * 2" by (simp add: m_def)
1.67 -      with \<open>m > 0\<close> have "q < 2" by simp
1.68 -      with \<open>q > 0\<close> have "q = 1" by simp
1.69 -      with a have "a = n - 1" by simp
1.70 -      with \<open>n > 0\<close> C show False by simp
1.71 +  have aux: False
1.72 +    if A: "Suc n dvd Suc (Suc a)"
1.73 +    and B: "a < n + n"
1.74 +    and C: "n \<le> a"
1.75 +    for a
1.76 +  proof (cases "n = 0")
1.77 +    case True
1.78 +    with A B C show ?thesis by simp
1.79 +  next
1.80 +    case False
1.81 +    def m \<equiv> "Suc n"
1.82 +    then have "m > 0" by simp
1.83 +    from False have "n > 0" by simp
1.84 +    from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
1.85 +    have "q > 0"
1.86 +    proof (rule ccontr)
1.87 +      assume "\<not> q > 0"
1.88 +      with q show False by simp
1.89      qed
1.90 -  } note aux = this
1.91 +    with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
1.92 +    with q have a: "a = Suc n * q - 2" by simp
1.93 +    with B have "q + n * q < n + n + 2" by auto
1.94 +    then have "m * q < m * 2" by (simp add: m_def)
1.95 +    with \<open>m > 0\<close> have "q < 2" by simp
1.96 +    with \<open>q > 0\<close> have "q = 1" by simp
1.97 +    with a have "a = n - 1" by simp
1.98 +    with \<open>n > 0\<close> C show False by simp
1.99 +  qed
1.100    show ?thesis
1.101      by (auto simp add: mark_out_def mark_out_aux_def in_set_enumerate_eq intro: aux)
1.102  qed
1.103 @@ -185,51 +184,55 @@
1.104    "numbers_of_marks (Suc n) (sieve n bs) =
1.105      {q \<in> numbers_of_marks (Suc n) bs. \<forall>m \<in> numbers_of_marks (Suc n) bs. \<not> m dvd_strict q}"
1.106  proof (induct n bs rule: sieve.induct)
1.107 -  case 1 show ?case by simp
1.108 +  case 1
1.109 +  show ?case by simp
1.110  next
1.111 -  case 2 then show ?case by simp
1.112 +  case 2
1.113 +  then show ?case by simp
1.114  next
1.115    case (3 n bs)
1.116 -  have aux: "\<And>M n. n \<in> Suc  M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M"
1.117 +  have aux: "n \<in> Suc  M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M" (is "?lhs \<longleftrightarrow> ?rhs") for M n
1.118    proof
1.119 -    fix M and n
1.120 -    assume "n \<in> Suc  M" then show "n > 0 \<and> n - 1 \<in> M" by auto
1.121 -  next
1.122 -    fix M and n :: nat
1.123 -    assume "n > 0 \<and> n - 1 \<in> M"
1.124 -    then have "n > 0" and "n - 1 \<in> M" by auto
1.125 -    then have "Suc (n - 1) \<in> Suc  M" by blast
1.126 -    with \<open>n > 0\<close> show "n \<in> Suc  M" by simp
1.127 +    show ?rhs if ?lhs using that by auto
1.128 +    show ?lhs if ?rhs
1.129 +    proof -
1.130 +      from that have "n > 0" and "n - 1 \<in> M" by auto
1.131 +      then have "Suc (n - 1) \<in> Suc  M" by blast
1.132 +      with \<open>n > 0\<close> show "n \<in> Suc  M" by simp
1.133 +    qed
1.134    qed
1.135 -  { fix m :: nat
1.136 -    assume "Suc (Suc n) \<le> m" and "m dvd Suc n"
1.137 +  have aux1: False if "Suc (Suc n) \<le> m" and "m dvd Suc n" for m :: nat
1.138 +  proof -
1.139      from \<open>m dvd Suc n\<close> obtain q where "Suc n = m * q" ..
1.140      with \<open>Suc (Suc n) \<le> m\<close> have "Suc (m * q) \<le> m" by simp
1.141      then have "m * q < m" by arith
1.142      then have "q = 0" by simp
1.143 -    with \<open>Suc n = m * q\<close> have False by simp
1.144 -  } note aux1 = this
1.145 -  { fix m q :: nat
1.146 -    assume "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs)
1.147 -      \<longrightarrow> bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q"
1.148 -    then have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs)
1.149 -      \<Longrightarrow> bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
1.150 +    with \<open>Suc n = m * q\<close> show ?thesis by simp
1.151 +  qed
1.152 +  have aux2: "m dvd q"
1.153 +    if 1: "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs) \<longrightarrow>
1.154 +      bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q"
1.155 +    and 2: "\<not> Suc n dvd m" "q dvd m"
1.156 +    and 3: "Suc n < q" "q \<le> Suc (n + length bs)" "bs ! (q - Suc (Suc n))"
1.157 +    for m q :: nat
1.158 +  proof -
1.159 +    from 1 have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs) \<Longrightarrow>
1.160 +      bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
1.161        by auto
1.162 -    assume "\<not> Suc n dvd m" and "q dvd m"
1.163 -    then have "\<not> Suc n dvd q" by (auto elim: dvdE)
1.164 -    moreover assume "Suc n < q" and "q \<le> Suc (n + length bs)"
1.165 -      and "bs ! (q - Suc (Suc n))"
1.166 +    from 2 have "\<not> Suc n dvd q" by (auto elim: dvdE)
1.167 +    moreover note 3
1.168      moreover note \<open>q dvd m\<close>
1.169 -    ultimately have "m dvd q" by (auto intro: *)
1.170 -  } note aux2 = this
1.171 +    ultimately show ?thesis by (auto intro: *)
1.172 +  qed
1.173    from 3 show ?case
1.174 -    apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq inj_image_eq_iff
1.175 -      in_numbers_of_marks_eq Ball_def imp_conjL aux)
1.176 +    apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq
1.177 +      inj_image_eq_iff in_numbers_of_marks_eq Ball_def imp_conjL aux)
1.178      apply safe
1.179      apply (simp_all add: less_diff_conv2 le_diff_conv2 dvd_minus_self not_less)
1.180      apply (clarsimp dest!: aux1)
1.181      apply (simp add: Suc_le_eq less_Suc_eq_le)
1.182 -    apply (rule aux2) apply (clarsimp dest!: aux1)+
1.183 +    apply (rule aux2)
1.184 +    apply (clarsimp dest!: aux1)+
1.185      done
1.186  qed
1.187
1.188 @@ -240,51 +243,56 @@
1.189  where
1.190    "primes_upto n = sorted_list_of_set {m. m \<le> n \<and> prime m}"
1.191
1.192 -lemma set_primes_upto:
1.193 -  "set (primes_upto n) = {m. m \<le> n \<and> prime m}"
1.194 +lemma set_primes_upto: "set (primes_upto n) = {m. m \<le> n \<and> prime m}"
1.196
1.197 -lemma sorted_primes_upto [iff]:
1.198 -  "sorted (primes_upto n)"
1.199 +lemma sorted_primes_upto [iff]: "sorted (primes_upto n)"
1.201
1.202 -lemma distinct_primes_upto [iff]:
1.203 -  "distinct (primes_upto n)"
1.204 +lemma distinct_primes_upto [iff]: "distinct (primes_upto n)"
1.206
1.207  lemma set_primes_upto_sieve:
1.208    "set (primes_upto n) = numbers_of_marks 2 (sieve 1 (replicate (n - 1) True))"
1.209 -proof (cases "n > 1")
1.210 -  case False then have "n = 0 \<or> n = 1" by arith
1.211 +proof -
1.212 +  consider "n = 0 \<or> n = 1" | "n > 1" by arith
1.213    then show ?thesis
1.214 -    by (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
1.215 -next
1.216 -  { fix m q
1.217 -    assume "Suc (Suc 0) \<le> q"
1.218 -      and "q < Suc n"
1.219 -      and "m dvd q"
1.220 -    then have "m < Suc n" by (auto dest: dvd_imp_le)
1.221 -    assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
1.222 -      and "m dvd q" and "m \<noteq> 1"
1.223 -    have "m = q" proof (cases "m = 0")
1.224 -      case True with \<open>m dvd q\<close> show ?thesis by simp
1.225 -    next
1.226 -      case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
1.227 -      with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
1.228 -      with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
1.229 -    qed
1.230 -  }
1.231 -  then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
1.232 -    q < Suc n \<Longrightarrow>
1.233 -    m dvd q \<Longrightarrow>
1.234 -    \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
1.235 -    m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
1.236 -  case True then show ?thesis
1.237 -    apply (auto simp add: One_nat_def numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
1.238 +  proof cases
1.239 +    case 1
1.240 +    then show ?thesis
1.241 +      by (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
1.242          dest: prime_gt_Suc_0_nat)
1.243 -    apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
1.244 -    apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
1.245 -    done
1.246 +  next
1.247 +    case 2
1.248 +    {
1.249 +      fix m q
1.250 +      assume "Suc (Suc 0) \<le> q"
1.251 +        and "q < Suc n"
1.252 +        and "m dvd q"
1.253 +      then have "m < Suc n" by (auto dest: dvd_imp_le)
1.254 +      assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
1.255 +        and "m dvd q" and "m \<noteq> 1"
1.256 +      have "m = q"
1.257 +      proof (cases "m = 0")
1.258 +        case True with \<open>m dvd q\<close> show ?thesis by simp
1.259 +      next
1.260 +        case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
1.261 +        with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
1.262 +        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
1.263 +      qed
1.264 +    }
1.265 +    then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
1.266 +      q < Suc n \<Longrightarrow>
1.267 +      m dvd q \<Longrightarrow>
1.268 +      \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
1.269 +      m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
1.270 +    from 2 show ?thesis
1.271 +      apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
1.272 +        dest: prime_gt_Suc_0_nat)
1.273 +      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
1.274 +      apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
1.275 +      done
1.276 +  qed
1.277  qed
1.278
1.279  lemma primes_upto_sieve [code]:
1.280 @@ -295,11 +303,11 @@
1.281      apply (simp_all only: set_primes_upto_sieve numbers_of_marks_def)
1.282      apply auto
1.283      done
1.284 -  then show ?thesis by (simp add: sorted_list_of_set_numbers_of_marks)
1.285 +  then show ?thesis
1.286 +    by (simp add: sorted_list_of_set_numbers_of_marks)
1.287  qed
1.288
1.289 -lemma prime_in_primes_upto:
1.290 -  "prime n \<longleftrightarrow> n \<in> set (primes_upto n)"
1.291 +lemma prime_in_primes_upto: "prime n \<longleftrightarrow> n \<in> set (primes_upto n)"
1.293
1.294
1.295 @@ -309,19 +317,19 @@
1.296  where
1.297    "smallest_prime_beyond n = (LEAST p. prime p \<and> p \<ge> n)"
1.298
1.299 -lemma
1.300 -  prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P)
1.301 +lemma prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P)
1.302    and smallest_prime_beyond_le [iff]: "smallest_prime_beyond n \<ge> n" (is ?Q)
1.303  proof -
1.304    let ?least = "LEAST p. prime p \<and> p \<ge> n"
1.305    from primes_infinite obtain q where "prime q \<and> q \<ge> n"
1.306      by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear)
1.307 -  then have "prime ?least \<and> ?least \<ge> n" by (rule LeastI)
1.308 -  then show ?P and ?Q by (simp_all add: smallest_prime_beyond_def)
1.309 +  then have "prime ?least \<and> ?least \<ge> n"
1.310 +    by (rule LeastI)
1.311 +  then show ?P and ?Q
1.312 +    by (simp_all add: smallest_prime_beyond_def)
1.313  qed
1.314
1.315 -lemma smallest_prime_beyond_smallest:
1.316 -  "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p"
1.317 +lemma smallest_prime_beyond_smallest: "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p"
1.318    by (simp only: smallest_prime_beyond_def) (auto intro: Least_le)
1.319
1.320  lemma smallest_prime_beyond_eq:
1.321 @@ -341,22 +349,28 @@
1.322    "smallest_prime_between m n = Some p \<longleftrightarrow> smallest_prime_beyond m = p \<and> p \<le> n"
1.323    by (auto simp add: smallest_prime_between_def dest: smallest_prime_beyond_smallest [of _ m])
1.324
1.325 -lemma [code]:
1.326 -  "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)"
1.327 +lemma [code]: "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)"
1.328  proof -
1.329 -  { fix p
1.330 +  have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
1.331 +    if assms: "m \<le> p" "prime p" "p \<le> n" for p
1.332 +  proof -
1.333      def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
1.334 -    assume assms: "m \<le> p" "prime p" "p \<le> n"
1.335 -    then have "smallest_prime_beyond m \<le> p" by (auto intro: smallest_prime_beyond_smallest)
1.336 -    from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
1.337 -    from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" by auto
1.338 -    then have "finite A" by (auto simp add: A_def)
1.339 +    from assms have "smallest_prime_beyond m \<le> p"
1.340 +      by (auto intro: smallest_prime_beyond_smallest)
1.341 +    from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n"
1.342 +      by (rule order_trans)
1.343 +    from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p"
1.344 +      by auto
1.345 +    then have "finite A"
1.346 +      by (auto simp add: A_def)
1.347      with * have "Min A = smallest_prime_beyond m"
1.348        by (auto simp add: A_def intro: Min_eqI smallest_prime_beyond_smallest)
1.349 -    with ex sorted_primes_upto have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
1.350 +    with ex sorted_primes_upto show ?thesis
1.351        by (auto simp add: set_primes_upto sorted_find_Min A_def)
1.352 -  } then show ?thesis
1.353 -  by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto intro!: sym [of _ None])
1.354 +  qed
1.355 +  then show ?thesis
1.356 +    by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto
1.357 +      intro!: sym [of _ None])
1.358  qed
1.359
1.360  definition smallest_prime_beyond_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.361 @@ -365,14 +379,12 @@
1.362
1.363  lemma [code]:
1.364    "smallest_prime_beyond_aux k n =
1.365 -    (case smallest_prime_between n (k * n)
1.366 -     of Some p \<Rightarrow> p
1.367 -      | None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)"
1.368 +    (case smallest_prime_between n (k * n) of
1.369 +      Some p \<Rightarrow> p
1.370 +    | None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)"
1.371    by (simp add: smallest_prime_beyond_aux_def smallest_prime_betwen_Some split: option.split)
1.372
1.373 -lemma [code]:
1.374 -  "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n"
1.375 +lemma [code]: "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n"
1.377
1.378  end
1.379 -

     2.1 --- a/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:41:33 2015 +0200
2.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 23:40:46 2015 +0200
2.3 @@ -1,17 +1,12 @@
2.4  (*  Title:      HOL/Number_Theory/Fib.thy
2.5      Author:     Lawrence C. Paulson
2.7 -
2.8 -Defines the fibonacci function.
2.9 -
2.10 -The original "Fib" is due to Lawrence C. Paulson, and was adapted by
2.12  *)
2.13
2.14 -section \<open>Fib\<close>
2.15 +section \<open>The fibonacci function\<close>
2.16
2.17  theory Fib
2.18 -imports Main "../GCD" "../Binomial"
2.19 +imports Main GCD Binomial
2.20  begin
2.21
2.22
2.23 @@ -19,9 +14,10 @@
2.24
2.25  fun fib :: "nat \<Rightarrow> nat"
2.26  where
2.27 -    fib0: "fib 0 = 0"
2.28 -  | fib1: "fib (Suc 0) = 1"
2.29 -  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
2.30 +  fib0: "fib 0 = 0"
2.31 +| fib1: "fib (Suc 0) = 1"
2.32 +| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
2.33 +
2.34
2.35  subsection \<open>Basic Properties\<close>
2.36
2.37 @@ -41,6 +37,7 @@
2.38  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
2.39    by (induct n rule: fib.induct) (auto simp add: )
2.40
2.41 +
2.42  subsection \<open>A Few Elementary Results\<close>
2.43
2.44  text \<open>
2.45 @@ -49,12 +46,12 @@
2.46  \<close>
2.47
2.48  lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
2.49 -  by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
2.50 +  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
2.51
2.52  lemma fib_Cassini_nat:
2.53 -    "fib (Suc (Suc n)) * fib n =
2.54 -       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
2.55 -using fib_Cassini_int [of n] by auto
2.56 +  "fib (Suc (Suc n)) * fib n =
2.57 +     (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
2.58 +  using fib_Cassini_int [of n] by auto
2.59
2.60
2.61  subsection \<open>Law 6.111 of Concrete Mathematics\<close>
2.62 @@ -69,28 +66,26 @@
2.63    apply (simp add: gcd_commute_nat [of "fib m"])
2.64    apply (cases m)
2.66 -  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
2.67 +  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
2.69    done
2.70
2.71 -lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
2.72 -    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
2.73 +lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
2.75
2.76 -lemma gcd_fib_mod: "0 < m \<Longrightarrow>
2.77 -    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
2.78 +lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
2.79  proof (induct n rule: less_induct)
2.80    case (less n)
2.81 -  from less.prems have pos_m: "0 < m" .
2.82    show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
2.83    proof (cases "m < n")
2.84      case True
2.85      then have "m \<le> n" by auto
2.86 -    with pos_m have pos_n: "0 < n" by auto
2.87 -    with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
2.88 +    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
2.89 +    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
2.90      have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
2.91        by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
2.92      also have "\<dots> = gcd (fib m)  (fib (n - m))"
2.93 -      by (simp add: less.hyps diff pos_m)
2.94 +      by (simp add: less.hyps diff \<open>0 < m\<close>)
2.95      also have "\<dots> = gcd (fib m) (fib n)"
2.96        by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
2.97      finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
2.98 @@ -105,10 +100,10 @@
2.99      -- \<open>Law 6.111\<close>
2.100    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
2.101
2.102 -theorem fib_mult_eq_setsum_nat:
2.103 -    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
2.104 +theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
2.105    by (induct n rule: nat.induct) (auto simp add:  field_simps)
2.106
2.107 +
2.108  subsection \<open>Fibonacci and Binomial Coefficients\<close>
2.109
2.110  lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
2.111 @@ -118,21 +113,22 @@
2.112      "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
2.113    by (rule trans [OF setsum.cong setsum_drop_zero]) auto
2.114
2.115 -lemma ne_diagonal_fib:
2.116 -   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
2.117 +lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
2.118  proof (induct n rule: fib.induct)
2.119 -  case 1 show ?case by simp
2.120 +  case 1
2.121 +  show ?case by simp
2.122  next
2.123 -  case 2 show ?case by simp
2.124 +  case 2
2.125 +  show ?case by simp
2.126  next
2.127    case (3 n)
2.128    have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
2.129          (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
2.130      by (rule setsum.cong) (simp_all add: choose_reduce_nat)
2.131 -  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
2.132 +  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
2.133                     (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
2.135 -  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
2.136 +  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
2.137                     (\<Sum>j = 0..n. n - j choose j)"
2.138      by (metis setsum_choose_drop_zero)
2.139    finally show ?case using 3

     3.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:41:33 2015 +0200
3.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 23:40:46 2015 +0200
3.3 @@ -1,8 +1,8 @@
3.4  (*  Title:      HOL/Number_Theory/MiscAlgebra.thy
3.6 +*)
3.7
3.8 -These are things that can be added to the Algebra library.
3.9 -*)
3.10 +section \<open>Things that can be added to the Algebra library\<close>
3.11
3.12  theory MiscAlgebra
3.13  imports
3.14 @@ -10,26 +10,25 @@
3.15    "~~/src/HOL/Algebra/FiniteProduct"
3.16  begin
3.17
3.18 -(* finiteness stuff *)
3.19 +subsection \<open>Finiteness stuff\<close>
3.20
3.21  lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
3.22    apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
3.23    apply (erule finite_subset)
3.24    apply auto
3.25 -done
3.26 +  done
3.27
3.28
3.29 -(* The rest is for the algebra libraries *)
3.30 +subsection \<open>The rest is for the algebra libraries\<close>
3.31
3.32 -(* These go in Group.thy. *)
3.33 +subsubsection \<open>These go in Group.thy\<close>
3.34
3.35 -(*
3.36 +text \<open>
3.37    Show that the units in any monoid give rise to a group.
3.38
3.39    The file Residues.thy provides some infrastructure to use
3.40    facts about the unit group within the ring locale.
3.41 -*)
3.42 -
3.43 +\<close>
3.44
3.45  definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
3.46    "units_of G == (| carrier = Units G,
3.47 @@ -83,8 +82,7 @@
3.48  lemma units_of_one: "one(units_of G) = one G"
3.49    unfolding units_of_def by auto
3.50
3.51 -lemma (in monoid) units_of_inv: "x : Units G ==>
3.52 -    m_inv (units_of G) x = m_inv G x"
3.53 +lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
3.54    apply (rule sym)
3.55    apply (subst m_inv_def)
3.56    apply (rule the1_equality)
3.57 @@ -103,14 +101,12 @@
3.58    apply (subst units_of_mult [symmetric])
3.59    apply (subst units_of_one [symmetric])
3.60    apply (erule group.l_inv, assumption)
3.61 -done
3.62 +  done
3.63
3.64 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
3.65 -    inj_on (%x. a \<otimes> x) (carrier G)"
3.66 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
3.67    unfolding inj_on_def by auto
3.68
3.69 -lemma (in group) surj_const_mult: "a : (carrier G) ==>
3.70 -    (%x. a \<otimes> x)  (carrier G) = (carrier G)"
3.71 +lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x)  (carrier G) = (carrier G)"
3.72    apply (auto simp add: image_def)
3.73    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
3.74    apply auto
3.75 @@ -120,8 +116,8 @@
3.76    apply auto
3.77    done
3.78
3.79 -lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
3.80 -    (x \<otimes> a = x) = (a = one G)"
3.81 +lemma (in group) l_cancel_one [simp]:
3.82 +    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
3.83    apply auto
3.84    apply (subst l_cancel [symmetric])
3.85    prefer 4
3.86 @@ -139,7 +135,6 @@
3.87    done
3.88
3.89  (* Is there a better way to do this? *)
3.90 -
3.91  lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
3.92      (x = x \<otimes> a) = (a = one G)"
3.93    apply (subst eq_commute)
3.94 @@ -173,10 +168,9 @@
3.95  qed
3.96
3.97
3.98 -(* Miscellaneous *)
3.99 +subsubsection \<open>Miscellaneous\<close>
3.100
3.101 -lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
3.102 -    x : Units R \<Longrightarrow> field R"
3.103 +lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
3.104    apply (unfold_locales)
3.105    apply (insert cring_axioms, auto)
3.106    apply (rule trans)
3.107 @@ -239,10 +233,10 @@
3.108    done
3.109
3.110  lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
3.111 -by (metis Units_inv_inv inv_one)
3.112 +  by (metis Units_inv_inv inv_one)
3.113
3.114
3.115 -(* This goes in FiniteProduct *)
3.116 +subsubsection \<open>This goes in FiniteProduct\<close>
3.117
3.118  lemma (in comm_monoid) finprod_UN_disjoint:
3.119    "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
3.120 @@ -276,17 +270,13 @@
3.121  (* need better simplification rules for rings *)
3.122  (* the next one holds more generally for abelian groups *)
3.123
3.124 -lemma (in cring) sum_zero_eq_neg:
3.125 -    "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
3.126 -by (metis minus_equality)
3.127 +lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
3.128 +  by (metis minus_equality)
3.129
3.130 -(* there's a name conflict -- maybe "domain" should be
3.131 -   "integral_domain" *)
3.132 -
3.133 -lemma (in Ring.domain) square_eq_one:
3.134 +lemma (in domain) square_eq_one:
3.135    fixes x
3.136 -  assumes [simp]: "x : carrier R" and
3.137 -    "x \<otimes> x = \<one>"
3.138 +  assumes [simp]: "x : carrier R"
3.139 +    and "x \<otimes> x = \<one>"
3.140    shows "x = \<one> | x = \<ominus>\<one>"
3.141  proof -
3.142    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
3.143 @@ -308,23 +298,22 @@
3.144      done
3.145  qed
3.146
3.147 -lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
3.148 -    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
3.149 -by (metis Units_closed Units_l_inv square_eq_one)
3.150 +lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
3.151 +  by (metis Units_closed Units_l_inv square_eq_one)
3.152
3.153
3.154 -(*
3.155 +text \<open>
3.157    the units of a ring. (The list should be expanded as more things are
3.158    needed.)
3.159 -*)
3.160 +\<close>
3.161
3.162 -lemma (in ring) finite_ring_finite_units [intro]:
3.163 -    "finite (carrier R) \<Longrightarrow> finite (Units R)"
3.164 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
3.165    by (rule finite_subset) auto
3.166
3.167  lemma (in monoid) units_of_pow:
3.168 -    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
3.169 +  fixes n :: nat
3.170 +  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
3.171    apply (induct n)
3.172    apply (auto simp add: units_group group.is_monoid
3.173      monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)

     4.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:41:33 2015 +0200
4.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:40:46 2015 +0200
4.3 @@ -11,26 +11,21 @@
4.4  imports UniqueFactorization MiscAlgebra
4.5  begin
4.6
4.7 -(*
4.8 -
4.9 -  A locale for residue rings
4.10 -
4.11 -*)
4.12 +subsection \<open>A locale for residue rings\<close>
4.13
4.14 -definition residue_ring :: "int => int ring" where
4.15 -  "residue_ring m == (|
4.16 -    carrier =       {0..m - 1},
4.17 -    mult =          (%x y. (x * y) mod m),
4.18 -    one =           1,
4.19 -    zero =          0,
4.20 -    add =           (%x y. (x + y) mod m) |)"
4.21 +definition residue_ring :: "int \<Rightarrow> int ring"
4.22 +  where
4.23 +  "residue_ring m =
4.24 +    \<lparr>carrier = {0..m - 1},
4.25 +     mult = \<lambda>x y. (x * y) mod m,
4.26 +     one = 1,
4.27 +     zero = 0,
4.28 +     add = \<lambda>x y. (x + y) mod m\<rparr>"
4.29
4.30  locale residues =
4.31    fixes m :: int and R (structure)
4.32    assumes m_gt_one: "m > 1"
4.33 -  defines "R == residue_ring m"
4.34 -
4.35 -context residues
4.36 +  defines "R \<equiv> residue_ring m"
4.37  begin
4.38
4.39  lemma abelian_group: "abelian_group R"
4.40 @@ -76,8 +71,10 @@
4.41  context residues
4.42  begin
4.43
4.44 -(* These lemmas translate back and forth between internal and
4.45 -   external concepts *)
4.46 +text \<open>
4.47 +  These lemmas translate back and forth between internal and
4.48 +  external concepts.
4.49 +\<close>
4.50
4.51  lemma res_carrier_eq: "carrier R = {0..m - 1}"
4.52    unfolding R_def residue_ring_def by auto
4.53 @@ -94,11 +91,11 @@
4.54  lemma res_one_eq: "\<one> = 1"
4.55    unfolding R_def residue_ring_def units_of_def by auto
4.56
4.57 -lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
4.58 +lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
4.59    apply (insert m_gt_one)
4.60    apply (unfold Units_def R_def residue_ring_def)
4.61    apply auto
4.62 -  apply (subgoal_tac "x ~= 0")
4.63 +  apply (subgoal_tac "x \<noteq> 0")
4.64    apply auto
4.65    apply (metis invertible_coprime_int)
4.66    apply (subst (asm) coprime_iff_invertible'_int)
4.67 @@ -121,19 +118,20 @@
4.68    done
4.69
4.70  lemma finite [iff]: "finite (carrier R)"
4.71 -  by (subst res_carrier_eq, auto)
4.72 +  by (subst res_carrier_eq) auto
4.73
4.74  lemma finite_Units [iff]: "finite (Units R)"
4.75    by (subst res_units_eq) auto
4.76
4.77 -(* The function a -> a mod m maps the integers to the
4.78 -   residue classes. The following lemmas show that this mapping
4.79 -   respects addition and multiplication on the integers. *)
4.80 +text \<open>
4.81 +  The function @{text "a \<mapsto> a mod m"} maps the integers to the
4.82 +  residue classes. The following lemmas show that this mapping
4.83 +  respects addition and multiplication on the integers.
4.84 +\<close>
4.85
4.86 -lemma mod_in_carrier [iff]: "a mod m : carrier R"
4.87 -  apply (unfold res_carrier_eq)
4.88 -  apply (insert m_gt_one, auto)
4.89 -  done
4.90 +lemma mod_in_carrier [iff]: "a mod m \<in> carrier R"
4.91 +  unfolding res_carrier_eq
4.92 +  using insert m_gt_one by auto
4.93
4.94  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
4.95    unfolding R_def residue_ring_def
4.96 @@ -151,7 +149,7 @@
4.97  lemma one_cong: "\<one> = 1 mod m"
4.98    using m_gt_one unfolding R_def residue_ring_def by auto
4.99
4.100 -(* revise algebra library to use 1? *)
4.101 +(* FIXME revise algebra library to use 1? *)
4.102  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
4.103    apply (insert m_gt_one)
4.104    apply (induct n)
4.105 @@ -162,19 +160,17 @@
4.106  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
4.107    by (metis mod_minus_eq res_neg_eq)
4.108
4.109 -lemma (in residues) prod_cong:
4.110 -    "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
4.111 +lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
4.112    by (induct set: finite) (auto simp: one_cong mult_cong)
4.113
4.114 -lemma (in residues) sum_cong:
4.115 -    "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
4.116 +lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
4.117    by (induct set: finite) (auto simp: zero_cong add_cong)
4.118
4.119 -lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
4.120 -    a mod m : Units R"
4.121 -  apply (subst res_units_eq, auto)
4.122 +lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
4.123 +  apply (subst res_units_eq)
4.124 +  apply auto
4.125    apply (insert pos_mod_sign [of m a])
4.126 -  apply (subgoal_tac "a mod m ~= 0")
4.127 +  apply (subgoal_tac "a mod m \<noteq> 0")
4.128    apply arith
4.129    apply auto
4.130    apply (metis gcd_int.commute gcd_red_int)
4.131 @@ -183,13 +179,13 @@
4.132  lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
4.133    unfolding cong_int_def by auto
4.134
4.135 -(* Simplifying with these will translate a ring equation in R to a
4.136 -   congruence. *)
4.137
4.138 +text \<open>Simplifying with these will translate a ring equation in R to a
4.139 +   congruence.\<close>
4.140  lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
4.141      prod_cong sum_cong neg_cong res_eq_to_cong
4.142
4.143 -(* Other useful facts about the residue ring *)
4.144 +text \<open>Other useful facts about the residue ring.\<close>
4.145
4.146  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
4.147    apply (simp add: res_one_eq res_neg_eq)
4.148 @@ -200,12 +196,12 @@
4.149  end
4.150
4.151
4.152 -(* prime residues *)
4.153 +subsection \<open>Prime residues\<close>
4.154
4.155  locale residues_prime =
4.156    fixes p and R (structure)
4.157    assumes p_prime [intro]: "prime p"
4.158 -  defines "R == residue_ring p"
4.159 +  defines "R \<equiv> residue_ring p"
4.160
4.161  sublocale residues_prime < residues p
4.162    apply (unfold R_def residues_def)
4.163 @@ -243,40 +239,42 @@
4.164    by (rule is_field)
4.165
4.166
4.167 -(*
4.168 -  Test cases: Euler's theorem and Wilson's theorem.
4.169 -*)
4.170 +section \<open>Test cases: Euler's theorem and Wilson's theorem\<close>
4.171
4.172 -
4.173 -subsection\<open>Euler's theorem\<close>
4.174 +subsection \<open>Euler's theorem\<close>
4.175
4.176 -(* the definition of the phi function *)
4.177 +text \<open>The definition of the phi function.\<close>
4.178
4.179 -definition phi :: "int => nat"
4.180 -  where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
4.181 +definition phi :: "int \<Rightarrow> nat"
4.182 +  where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}"
4.183
4.184 -lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})"
4.185 +lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}"
4.187    apply (rule bij_betw_same_card [of nat])
4.188    apply (auto simp add: inj_on_def bij_betw_def image_def)
4.189    apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
4.190 -  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int transfer_int_nat_gcd(1) zless_int)
4.191 +  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int
4.192 +    transfer_int_nat_gcd(1) zless_int)
4.193    done
4.194
4.195  lemma prime_phi:
4.196 -  assumes  "2 \<le> p" "phi p = p - 1" shows "prime p"
4.197 +  assumes "2 \<le> p" "phi p = p - 1"
4.198 +  shows "prime p"
4.199  proof -
4.200    have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
4.201      using assms unfolding phi_def_nat
4.202      by (intro card_seteq) fastforce+
4.203 -  then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
4.204 +  then have cop: "\<And>x::nat. x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
4.205      by blast
4.206 -  { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
4.207 +  have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat
4.208 +  proof -
4.209      have "coprime x p"
4.210        apply (rule cop)
4.211        using * apply auto
4.212        done
4.213 -    with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
4.214 +    with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
4.215 +      by auto
4.216 +  qed
4.217    then show ?thesis
4.218      using \<open>2 \<le> p\<close>
4.220 @@ -285,9 +283,9 @@
4.221  qed
4.222
4.223  lemma phi_zero [simp]: "phi 0 = 0"
4.224 -  apply (subst phi_def)
4.225 +  unfolding phi_def
4.226  (* Auto hangs here. Once again, where is the simplification rule
4.227 -   1 == Suc 0 coming from? *)
4.228 +   1 \<equiv> Suc 0 coming from? *)
4.229    apply (auto simp add: card_eq_0_iff)
4.230  (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
4.231    done
4.232 @@ -295,19 +293,19 @@
4.233  lemma phi_one [simp]: "phi 1 = 0"
4.234    by (auto simp add: phi_def card_eq_0_iff)
4.235
4.236 -lemma (in residues) phi_eq: "phi m = card(Units R)"
4.237 +lemma (in residues) phi_eq: "phi m = card (Units R)"
4.238    by (simp add: phi_def res_units_eq)
4.239
4.240  lemma (in residues) euler_theorem1:
4.241    assumes a: "gcd a m = 1"
4.242    shows "[a^phi m = 1] (mod m)"
4.243  proof -
4.244 -  from a m_gt_one have [simp]: "a mod m : Units R"
4.245 +  from a m_gt_one have [simp]: "a mod m \<in> Units R"
4.246      by (intro mod_in_res_units)
4.247    from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
4.248      by simp
4.249    also have "\<dots> = \<one>"
4.250 -    by (intro units_power_order_eq_one, auto)
4.251 +    by (intro units_power_order_eq_one) auto
4.252    finally show ?thesis
4.254  qed
4.255 @@ -329,55 +327,57 @@
4.256  (* outside the locale, we can relax the restriction m > 1 *)
4.257
4.258  lemma euler_theorem:
4.259 -  assumes "m >= 0" and "gcd a m = 1"
4.260 +  assumes "m \<ge> 0"
4.261 +    and "gcd a m = 1"
4.262    shows "[a^phi m = 1] (mod m)"
4.263 -proof (cases)
4.264 -  assume "m = 0 | m = 1"
4.265 +proof (cases "m = 0 | m = 1")
4.266 +  case True
4.267    then show ?thesis by auto
4.268  next
4.269 -  assume "~(m = 0 | m = 1)"
4.270 +  case False
4.271    with assms show ?thesis
4.272      by (intro residues.euler_theorem1, unfold residues_def, auto)
4.273  qed
4.274
4.275 -lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"
4.276 +lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
4.277    apply (subst phi_eq)
4.278    apply (subst res_prime_units_eq)
4.279    apply auto
4.280    done
4.281
4.282 -lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
4.283 +lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
4.284    apply (rule residues_prime.phi_prime)
4.285    apply (erule residues_prime.intro)
4.286    done
4.287
4.288  lemma fermat_theorem:
4.289 -  fixes a::int
4.290 -  assumes "prime p" and "~ (p dvd a)"
4.291 +  fixes a :: int
4.292 +  assumes "prime p"
4.293 +    and "\<not> p dvd a"
4.294    shows "[a^(p - 1) = 1] (mod p)"
4.295  proof -
4.296 -  from assms have "[a^phi p = 1] (mod p)"
4.297 +  from assms have "[a ^ phi p = 1] (mod p)"
4.298      apply (intro euler_theorem)
4.299      apply (metis of_nat_0_le_iff)
4.300      apply (metis gcd_int.commute prime_imp_coprime_int)
4.301      done
4.302    also have "phi p = nat p - 1"
4.303 -    by (rule phi_prime, rule assms)
4.304 +    by (rule phi_prime) (rule assms)
4.305    finally show ?thesis
4.306      by (metis nat_int)
4.307  qed
4.308
4.309  lemma fermat_theorem_nat:
4.310 -  assumes "prime p" and "~ (p dvd a)"
4.311 -  shows "[a^(p - 1) = 1] (mod p)"
4.312 -using fermat_theorem [of p a] assms
4.313 -by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
4.314 +  assumes "prime p" and "\<not> p dvd a"
4.315 +  shows "[a ^ (p - 1) = 1] (mod p)"
4.316 +  using fermat_theorem [of p a] assms
4.317 +  by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
4.318
4.319
4.320  subsection \<open>Wilson's theorem\<close>
4.321
4.322 -lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
4.323 -    {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
4.324 +lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow>
4.325 +    {x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}"
4.326    apply auto
4.327    apply (metis Units_inv_inv)+
4.328    done
4.329 @@ -386,41 +386,43 @@
4.330    assumes a: "p > 2"
4.331    shows "[fact (p - 1) = (-1::int)] (mod p)"
4.332  proof -
4.333 -  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
4.334 -  have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
4.335 +  let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}"
4.336 +  have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs"
4.337      by auto
4.338 -  have "(\<Otimes>i: Units R. i) =
4.339 -    (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
4.340 +  have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
4.341      apply (subst UR)
4.342      apply (subst finprod_Un_disjoint)
4.343      apply (auto intro: funcsetI)
4.344 -    apply (metis Units_inv_inv inv_one inv_neg_one)+
4.345 +    using inv_one apply auto
4.346 +    using inv_eq_neg_one_eq apply auto
4.347      done
4.348 -  also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
4.349 +  also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
4.350      apply (subst finprod_insert)
4.351      apply auto
4.352      apply (frule one_eq_neg_one)
4.353 -    apply (insert a, force)
4.354 +    using a apply force
4.355      done
4.356 -  also have "(\<Otimes>i:(Union ?InversePairs). i) =
4.357 -      (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
4.358 -    apply (subst finprod_Union_disjoint, auto)
4.359 +  also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
4.360 +    apply (subst finprod_Union_disjoint)
4.361 +    apply auto
4.362      apply (metis Units_inv_inv)+
4.363      done
4.364    also have "\<dots> = \<one>"
4.365 -    apply (rule finprod_one, auto)
4.366 -    apply (subst finprod_insert, auto)
4.367 +    apply (rule finprod_one)
4.368 +    apply auto
4.369 +    apply (subst finprod_insert)
4.370 +    apply auto
4.371      apply (metis inv_eq_self)
4.372      done
4.373 -  finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
4.374 +  finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
4.375      by simp
4.376 -  also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
4.377 +  also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
4.378      apply (rule finprod_cong')
4.379 -    apply (auto)
4.380 +    apply auto
4.381      apply (subst (asm) res_prime_units_eq)
4.382      apply auto
4.383      done
4.384 -  also have "\<dots> = (PROD i: Units R. i) mod p"
4.385 +  also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
4.386      apply (rule prod_cong)
4.387      apply auto
4.388      done
4.389 @@ -430,13 +432,14 @@
4.390      apply (subst res_prime_units_eq)
4.391      apply (simp add: int_setprod zmod_int setprod_int_eq)
4.392      done
4.393 -  finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
4.394 -  then show ?thesis
4.395 +  finally have "fact (p - 1) mod p = \<ominus> \<one>" .
4.396 +  then show ?thesis
4.397      by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
4.398  qed
4.399
4.400  lemma wilson_theorem:
4.401 -  assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
4.402 +  assumes "prime p"
4.403 +  shows "[fact (p - 1) = - 1] (mod p)"
4.404  proof (cases "p = 2")
4.405    case True
4.406    then show ?thesis

     5.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 21:41:33 2015 +0200
5.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 23:40:46 2015 +0200
5.3 @@ -1,14 +1,12 @@
5.4  (*  Title:      HOL/Number_Theory/UniqueFactorization.thy
5.6
5.7 -Unique factorization for the natural numbers and the integers.
5.8 -
5.9  Note: there were previous Isabelle formalizations of unique
5.10  factorization due to Thomas Marthedal Rasmussen, and, building on
5.11 -that, by Jeremy Avigad and David Gray.
5.12 +that, by Jeremy Avigad and David Gray.
5.13  *)
5.14
5.15 -section \<open>UniqueFactorization\<close>
5.16 +section \<open>Unique factorization for the natural numbers and the integers\<close>
5.17
5.18  theory UniqueFactorization
5.19  imports Cong "~~/src/HOL/Library/Multiset"
5.20 @@ -18,132 +16,135 @@
5.21
5.22       prime p \<Longrightarrow> p > 0
5.23
5.24 -   wreaks havoc here. When the premise includes ALL x :# M. prime x, it
5.25 +   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
5.27
5.28 -     x > 0
5.29 -     prime x
5.30 -     x :# M   which is, unfortunately,
5.31 +     x > 0
5.32 +     prime x
5.33 +     x \<in># M   which is, unfortunately,
5.34       count M x > 0
5.35  *)
5.36
5.37  (* Here is a version of set product for multisets. Is it worth moving
5.38 -   to multiset.thy? If so, one should similarly define msetsum for abelian
5.39 -   semirings, using of_nat. Also, is it worth developing bounded quantifiers
5.40 -   "ALL i :# M. P i"?
5.41 +   to multiset.thy? If so, one should similarly define msetsum for abelian
5.42 +   semirings, using of_nat. Also, is it worth developing bounded quantifiers
5.43 +   "\<forall>i \<in># M. P i"?
5.44  *)
5.45
5.46
5.47 -subsection \<open>unique factorization: multiset version\<close>
5.48 +subsection \<open>Unique factorization: multiset version\<close>
5.49
5.50 -lemma multiset_prime_factorization_exists [rule_format]: "n > 0 -->
5.51 -    (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
5.52 -proof (rule nat_less_induct, clarify)
5.53 +lemma multiset_prime_factorization_exists:
5.54 +  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
5.55 +proof (induct n rule: nat_less_induct)
5.56    fix n :: nat
5.57 -  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_mset M. prime p) & m =
5.58 -      (PROD i :# M. i))"
5.59 -  assume "(n::nat) > 0"
5.60 -  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
5.61 +  assume ih: "\<forall>m < n. 0 < m \<longrightarrow> (\<exists>M. (\<forall>p\<in>set_mset M. prime p) \<and> m = (\<Prod>i \<in># M. i))"
5.62 +  assume "n > 0"
5.63 +  then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
5.64      by arith
5.65 -  moreover {
5.66 -    assume "n = 1"
5.67 -    then have "(ALL p : set_mset {#}. prime p) & n = (PROD i :# {#}. i)" by auto
5.68 -  } moreover {
5.69 -    assume "n > 1" and "prime n"
5.70 -    then have "(ALL p : set_mset {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
5.71 +  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i::nat\<in>#M. i)"
5.72 +  proof cases
5.73 +    case 1
5.74 +    then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"
5.75        by auto
5.76 -  } moreover {
5.77 -    assume "n > 1" and "~ prime n"
5.78 +    then show ?thesis ..
5.79 +  next
5.80 +    case 2
5.81 +    then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)"
5.82 +      by auto
5.83 +    then show ?thesis ..
5.84 +  next
5.85 +    case 3
5.86      with not_prime_eq_prod_nat
5.87 -    obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
5.88 +    obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
5.89        by blast
5.90 -    with ih obtain Q R where "(ALL p : set_mset Q. prime p) & m = (PROD i:#Q. i)"
5.91 -        and "(ALL p: set_mset R. prime p) & k = (PROD i:#R. i)"
5.92 +    with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)"
5.93 +        and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)"
5.94        by blast
5.95 -    then have "(ALL p: set_mset (Q + R). prime p) & n = (PROD i :# Q + R. i)"
5.96 +    then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)"
5.97        by (auto simp add: n msetprod_Un)
5.98 -    then have "EX M. (ALL p : set_mset M. prime p) & n = (PROD i :# M. i)"..
5.99 -  }
5.100 -  ultimately show "EX M. (ALL p : set_mset M. prime p) & n = (PROD i::nat:#M. i)"
5.101 -    by blast
5.102 +    then show ?thesis ..
5.103 +  qed
5.104  qed
5.105
5.106  lemma multiset_prime_factorization_unique_aux:
5.107    fixes a :: nat
5.108 -  assumes "(ALL p : set_mset M. prime p)" and
5.109 -    "(ALL p : set_mset N. prime p)" and
5.110 -    "(PROD i :# M. i) dvd (PROD i:# N. i)"
5.111 -  shows
5.112 -    "count M a <= count N a"
5.113 -proof cases
5.114 -  assume M: "a : set_mset M"
5.115 -  with assms have a: "prime a" by auto
5.116 -  with M have "a ^ count M a dvd (PROD i :# M. i)"
5.117 +  assumes "\<forall>p\<in>set_mset M. prime p"
5.118 +    and "\<forall>p\<in>set_mset N. prime p"
5.119 +    and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)"
5.120 +  shows "count M a \<le> count N a"
5.121 +proof (cases "a \<in> set_mset M")
5.122 +  case True
5.123 +  with assms have a: "prime a"
5.124 +    by auto
5.125 +  with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)"
5.126      by (auto simp add: msetprod_multiplicity)
5.127 -  also have "... dvd (PROD i :# N. i)" by (rule assms)
5.128 -  also have "... = (PROD i : (set_mset N). i ^ (count N i))"
5.129 +  also have "\<dots> dvd (\<Prod>i \<in># N. i)"
5.130 +    by (rule assms)
5.131 +  also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)"
5.133 -  also have "... = a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))"
5.134 -  proof (cases)
5.135 -    assume "a : set_mset N"
5.136 -    then have b: "set_mset N = {a} Un (set_mset N - {a})"
5.137 +  also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
5.138 +  proof (cases "a \<in> set_mset N")
5.139 +    case True
5.140 +    then have b: "set_mset N = {a} \<union> (set_mset N - {a})"
5.141        by auto
5.142      then show ?thesis
5.143        by (subst (1) b, subst setprod.union_disjoint, auto)
5.144    next
5.145 -    assume "a ~: set_mset N"
5.146 -    then show ?thesis by auto
5.147 +    case False
5.148 +    then show ?thesis
5.149 +      by auto
5.150    qed
5.151 -  finally have "a ^ count M a dvd
5.152 -      a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))".
5.153 +  finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
5.154    moreover
5.155 -  have "coprime (a ^ count M a) (PROD i : (set_mset N - {a}). i ^ (count N i))"
5.156 +  have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
5.157      apply (subst gcd_commute_nat)
5.158      apply (rule setprod_coprime_nat)
5.159      apply (rule primes_imp_powers_coprime_nat)
5.160 -    using assms M
5.161 +    using assms True
5.162      apply auto
5.163      done
5.164 -  ultimately have "a ^ count M a dvd a^(count N a)"
5.165 +  ultimately have "a ^ count M a dvd a ^ count N a"
5.166      by (elim coprime_dvd_mult_nat)
5.167 -  with a show ?thesis
5.168 +  with a show ?thesis
5.169      apply (intro power_dvd_imp_le)
5.170      apply auto
5.171      done
5.172  next
5.173 -  assume "a ~: set_mset M"
5.174 -  then show ?thesis by auto
5.175 +  case False
5.176 +  then show ?thesis
5.177 +    by auto
5.178  qed
5.179
5.180  lemma multiset_prime_factorization_unique:
5.181 -  assumes "(ALL (p::nat) : set_mset M. prime p)" and
5.182 -    "(ALL p : set_mset N. prime p)" and
5.183 -    "(PROD i :# M. i) = (PROD i:# N. i)"
5.184 -  shows
5.185 -    "M = N"
5.186 +  assumes "\<forall>p::nat \<in> set_mset M. prime p"
5.187 +    and "\<forall>p \<in> set_mset N. prime p"
5.188 +    and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
5.189 +  shows "M = N"
5.190  proof -
5.191 -  {
5.192 -    fix a
5.193 -    from assms have "count M a <= count N a"
5.194 -      by (intro multiset_prime_factorization_unique_aux, auto)
5.195 -    moreover from assms have "count N a <= count M a"
5.196 -      by (intro multiset_prime_factorization_unique_aux, auto)
5.197 -    ultimately have "count M a = count N a"
5.198 +  have "count M a = count N a" for a
5.199 +  proof -
5.200 +    from assms have "count M a \<le> count N a"
5.201 +      by (intro multiset_prime_factorization_unique_aux, auto)
5.202 +    moreover from assms have "count N a \<le> count M a"
5.203 +      by (intro multiset_prime_factorization_unique_aux, auto)
5.204 +    ultimately show ?thesis
5.205        by auto
5.206 -  }
5.207 -  then show ?thesis by (simp add:multiset_eq_iff)
5.208 +  qed
5.209 +  then show ?thesis
5.210 +    by (simp add: multiset_eq_iff)
5.211  qed
5.212
5.213 -definition multiset_prime_factorization :: "nat => nat multiset"
5.214 +definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset"
5.215  where
5.216 -  "multiset_prime_factorization n ==
5.217 -     if n > 0 then (THE M. ((ALL p : set_mset M. prime p) &
5.218 -       n = (PROD i :# M. i)))
5.219 -     else {#}"
5.220 +  "multiset_prime_factorization n =
5.221 +    (if n > 0
5.222 +     then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i)
5.223 +     else {#})"
5.224
5.225 -lemma multiset_prime_factorization: "n > 0 ==>
5.226 -    (ALL p : set_mset (multiset_prime_factorization n). prime p) &
5.227 -       n = (PROD i :# (multiset_prime_factorization n). i)"
5.228 +lemma multiset_prime_factorization: "n > 0 \<Longrightarrow>
5.229 +    (\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and>
5.230 +       n = (\<Prod>i \<in># (multiset_prime_factorization n). i)"
5.231    apply (unfold multiset_prime_factorization_def)
5.232    apply clarsimp
5.233    apply (frule multiset_prime_factorization_exists)
5.234 @@ -151,17 +152,16 @@
5.235    apply (rule theI)
5.236    apply (insert multiset_prime_factorization_unique)
5.237    apply auto
5.238 -done
5.239 +  done
5.240
5.241
5.242 -subsection \<open>Prime factors and multiplicity for nats and ints\<close>
5.243 +subsection \<open>Prime factors and multiplicity for nat and int\<close>
5.244
5.245  class unique_factorization =
5.246    fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
5.247      and prime_factors :: "'a \<Rightarrow> 'a set"
5.248
5.249 -(* definitions for the natural numbers *)
5.250 -
5.251 +text \<open>Definitions for the natural numbers.\<close>
5.252  instantiation nat :: unique_factorization
5.253  begin
5.254
5.255 @@ -175,8 +175,7 @@
5.256
5.257  end
5.258
5.259 -(* definitions for the integers *)
5.260 -
5.261 +text \<open>Definitions for the integers.\<close>
5.262  instantiation int :: unique_factorization
5.263  begin
5.264
5.265 @@ -200,96 +199,107 @@
5.266    apply assumption
5.267    done
5.268
5.269 -lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
5.270 +lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)"
5.271    by (auto simp add: nat_set_def prime_factors_int_def)
5.272
5.273 -lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
5.274 -    multiplicity (nat p) (nat n) = multiplicity p n"
5.275 +lemma transfer_nat_int_multiplicity:
5.276 +  "p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n"
5.277    by (auto simp add: multiplicity_int_def)
5.278
5.281    transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
5.282    transfer_nat_int_multiplicity]
5.283
5.284 -
5.285  lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int  prime_factors n"
5.286    unfolding prime_factors_int_def by auto
5.287
5.288 -lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow>
5.289 -    nat_set (prime_factors n)"
5.290 +lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)"
5.291    by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
5.292
5.293 -lemma transfer_int_nat_multiplicity:
5.294 -    "multiplicity (int p) (int n) = multiplicity p n"
5.295 +lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n"
5.296    by (auto simp add: multiplicity_int_def)
5.297
5.300    transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
5.301    transfer_int_nat_multiplicity]
5.302
5.303
5.304 -subsection \<open>Properties of prime factors and multiplicity for nats and ints\<close>
5.305 +subsection \<open>Properties of prime factors and multiplicity for nat and int\<close>
5.306
5.307 -lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
5.308 +lemma prime_factors_ge_0_int [elim]:
5.309 +  fixes n :: int
5.310 +  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
5.311    unfolding prime_factors_int_def by auto
5.312
5.313 -lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
5.314 +lemma prime_factors_prime_nat [intro]:
5.315 +  fixes n :: nat
5.316 +  shows "p \<in> prime_factors n \<Longrightarrow> prime p"
5.317    apply (cases "n = 0")
5.318    apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
5.319    apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
5.320    done
5.321
5.322  lemma prime_factors_prime_int [intro]:
5.323 -  assumes "n >= 0" and "p : prime_factors (n::int)"
5.324 +  fixes n :: int
5.325 +  assumes "n \<ge> 0" and "p \<in> prime_factors n"
5.326    shows "prime p"
5.327    apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
5.328    using assms apply auto
5.329    done
5.330
5.331 -lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
5.332 -  apply (frule prime_factors_prime_nat)
5.333 -  apply auto
5.334 -  done
5.335 +lemma prime_factors_gt_0_nat [elim]:
5.336 +  fixes p :: nat
5.337 +  shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
5.338 +  by (auto dest!: prime_factors_prime_nat)
5.339
5.340 -lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
5.341 -    int p > (0::int)"
5.342 -  apply auto
5.343 -  done
5.344 +lemma prime_factors_gt_0_int [elim]:
5.345 +  shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
5.346 +  by auto
5.347
5.348 -lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
5.349 +lemma prime_factors_finite_nat [iff]:
5.350 +  fixes n :: nat
5.351 +  shows "finite (prime_factors n)"
5.352    unfolding prime_factors_nat_def by auto
5.353
5.354 -lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
5.355 +lemma prime_factors_finite_int [iff]:
5.356 +  fixes n :: int
5.357 +  shows "finite (prime_factors n)"
5.358    unfolding prime_factors_int_def by auto
5.359
5.360 -lemma prime_factors_altdef_nat: "prime_factors (n::nat) =
5.361 -    {p. multiplicity p n > 0}"
5.362 +lemma prime_factors_altdef_nat:
5.363 +  fixes n :: nat
5.364 +  shows "prime_factors n = {p. multiplicity p n > 0}"
5.365    by (force simp add: prime_factors_nat_def multiplicity_nat_def)
5.366
5.367 -lemma prime_factors_altdef_int: "prime_factors (n::int) =
5.368 -    {p. p >= 0 & multiplicity p n > 0}"
5.369 +lemma prime_factors_altdef_int:
5.370 +  fixes n :: int
5.371 +  shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}"
5.372    apply (unfold prime_factors_int_def multiplicity_int_def)
5.373    apply (subst prime_factors_altdef_nat)
5.374    apply (auto simp add: image_def)
5.375    done
5.376
5.377 -lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
5.378 -    n = (PROD p : prime_factors n. p^(multiplicity p n))"
5.379 +lemma prime_factorization_nat:
5.380 +  fixes n :: nat
5.381 +  shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
5.382    apply (frule multiset_prime_factorization)
5.383    apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
5.384    done
5.385
5.386 -lemma prime_factorization_int:
5.387 -  assumes "(n::int) > 0"
5.388 -  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
5.389 +lemma prime_factorization_int:
5.390 +  fixes n :: int
5.391 +  assumes "n > 0"
5.392 +  shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
5.393    apply (rule prime_factorization_nat [transferred, of n])
5.394    using assms apply auto
5.395    done
5.396
5.397 -lemma prime_factorization_unique_nat:
5.398 +lemma prime_factorization_unique_nat:
5.399    fixes f :: "nat \<Rightarrow> _"
5.400 -  assumes S_eq: "S = {p. 0 < f p}" and "finite S"
5.401 -    and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
5.402 +  assumes S_eq: "S = {p. 0 < f p}"
5.403 +    and "finite S"
5.404 +    and "\<forall>p\<in>S. prime p"
5.405 +    and "n = (\<Prod>p\<in>S. p ^ f p)"
5.406    shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
5.407  proof -
5.408    from assms have "f \<in> multiset"
5.409 @@ -305,8 +315,7 @@
5.410      apply force
5.411      apply force
5.412      apply force
5.413 -    using assms
5.414 -    apply (simp add: set_mset_def msetprod_multiplicity)
5.415 +    using assms apply (simp add: set_mset_def msetprod_multiplicity)
5.416      done
5.417    with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
5.418      by simp
5.419 @@ -314,49 +323,40 @@
5.420      by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
5.421  qed
5.422
5.423 -lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
5.424 -    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
5.425 -      prime_factors n = S"
5.426 -  apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
5.427 -  apply assumption+
5.428 -  done
5.429 +lemma prime_factors_characterization_nat:
5.430 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
5.431 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
5.432 +  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
5.433
5.434 -lemma prime_factors_characterization'_nat:
5.435 +lemma prime_factors_characterization'_nat:
5.436    "finite {p. 0 < f (p::nat)} \<Longrightarrow>
5.437 -    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
5.438 -      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
5.439 -  apply (rule prime_factors_characterization_nat)
5.440 -  apply auto
5.441 -  done
5.442 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
5.443 +      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
5.444 +  by (rule prime_factors_characterization_nat) auto
5.445
5.446  (* A minor glitch:*)
5.447 -
5.448 -thm prime_factors_characterization'_nat
5.449 -    [where f = "%x. f (int (x::nat))",
5.450 -      transferred direction: nat "op <= (0::int)", rule_format]
5.451 +thm prime_factors_characterization'_nat
5.452 +    [where f = "\<lambda>x. f (int (x::nat))",
5.453 +      transferred direction: nat "op \<le> (0::int)", rule_format]
5.454
5.455  (*
5.456 -  Transfer isn't smart enough to know that the "0 < f p" should
5.457 -  remain a comparison between nats. But the transfer still works.
5.458 +  Transfer isn't smart enough to know that the "0 < f p" should
5.459 +  remain a comparison between nats. But the transfer still works.
5.460  *)
5.461
5.462 -lemma primes_characterization'_int [rule_format]:
5.463 -    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
5.464 -      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
5.465 -        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) =
5.466 -          {p. p >= 0 & 0 < f p}"
5.467 +lemma primes_characterization'_int [rule_format]:
5.468 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
5.469 +      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
5.470 +  using prime_factors_characterization'_nat
5.471 +    [where f = "\<lambda>x. f (int (x::nat))",
5.472 +    transferred direction: nat "op \<le> (0::int)"]
5.473 +  by auto
5.474
5.475 -  apply (insert prime_factors_characterization'_nat
5.476 -    [where f = "%x. f (int (x::nat))",
5.477 -    transferred direction: nat "op <= (0::int)"])
5.478 -  apply auto
5.479 -  done
5.480 -
5.481 -lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
5.482 -    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
5.483 -      prime_factors n = S"
5.484 +lemma prime_factors_characterization_int:
5.485 +  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
5.486 +    \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
5.487    apply simp
5.488 -  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
5.489 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
5.490    apply (simp only:)
5.491    apply (subst primes_characterization'_int)
5.492    apply auto
5.493 @@ -364,36 +364,36 @@
5.494    apply (metis le_cases nat_le_0 zero_not_prime_nat)
5.495    done
5.496
5.497 -lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
5.498 -    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
5.499 -      multiplicity p n = f p"
5.500 +lemma multiplicity_characterization_nat:
5.501 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow>
5.502 +    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
5.503    apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
5.504    apply auto
5.505    done
5.506
5.507  lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
5.508 -    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
5.509 -      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
5.510 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
5.511 +      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
5.512    apply (intro impI)
5.513    apply (rule multiplicity_characterization_nat)
5.514    apply auto
5.515    done
5.516
5.517 -lemma multiplicity_characterization'_int [rule_format]:
5.518 -  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
5.519 -    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
5.520 -      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
5.521 -  apply (insert multiplicity_characterization'_nat
5.522 -    [where f = "%x. f (int (x::nat))",
5.523 -      transferred direction: nat "op <= (0::int)", rule_format])
5.524 +lemma multiplicity_characterization'_int [rule_format]:
5.525 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
5.526 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
5.527 +      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
5.528 +  apply (insert multiplicity_characterization'_nat
5.529 +    [where f = "\<lambda>x. f (int (x::nat))",
5.530 +      transferred direction: nat "op \<le> (0::int)", rule_format])
5.531    apply auto
5.532    done
5.533
5.534 -lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
5.535 -    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
5.536 -      p >= 0 \<Longrightarrow> multiplicity p n = f p"
5.537 +lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
5.538 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow>
5.539 +      p \<ge> 0 \<Longrightarrow> multiplicity p n = f p"
5.540    apply simp
5.541 -  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
5.542 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
5.543    apply (simp only:)
5.544    apply (subst multiplicity_characterization'_int)
5.545    apply auto
5.546 @@ -405,10 +405,10 @@
5.547    by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
5.548
5.549  lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
5.550 -  by (simp add: multiplicity_int_def)
5.551 +  by (simp add: multiplicity_int_def)
5.552
5.553  lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0"
5.554 -  by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
5.555 +  by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto)
5.556
5.557  lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
5.558    by (metis One_nat_def multiplicity_one_nat')
5.559 @@ -417,99 +417,101 @@
5.560    by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
5.561
5.562  lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
5.563 -  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
5.564 +  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"])
5.565    apply auto
5.566 -  by (metis (full_types) less_not_refl)
5.567 +  apply (metis (full_types) less_not_refl)
5.568 +  done
5.569
5.570 -lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p^n) = n"
5.571 +lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n"
5.572    apply (cases "n = 0")
5.573    apply auto
5.574 -  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
5.575 +  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"])
5.576    apply auto
5.577 -  by (metis (full_types) less_not_refl)
5.578 +  apply (metis (full_types) less_not_refl)
5.579 +  done
5.580
5.581 -lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p ( (int p)^n) = n"
5.582 +lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = n"
5.583    by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
5.584
5.585 -lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
5.586 +lemma multiplicity_nonprime_nat [simp]:
5.587 +  fixes p n :: nat
5.588 +  shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
5.589    apply (cases "n = 0")
5.590    apply auto
5.591    apply (frule multiset_prime_factorization)
5.592    apply (auto simp add: set_mset_def multiplicity_nat_def)
5.593    done
5.594
5.595 -lemma multiplicity_not_factor_nat [simp]:
5.596 -    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
5.597 +lemma multiplicity_not_factor_nat [simp]:
5.598 +  fixes p n :: nat
5.599 +  shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
5.600    apply (subst (asm) prime_factors_altdef_nat)
5.601    apply auto
5.602    done
5.603
5.604 -lemma multiplicity_not_factor_int [simp]:
5.605 -    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
5.606 +lemma multiplicity_not_factor_int [simp]:
5.607 +  fixes n :: int
5.608 +  shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
5.609    apply (subst (asm) prime_factors_altdef_int)
5.610    apply auto
5.611    done
5.612
5.613  (*FIXME: messy*)
5.614  lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
5.615 -    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
5.616 -    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
5.617 +    (prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and>
5.618 +    (\<forall>p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
5.619    apply (rule prime_factorization_unique_nat)
5.620    apply (simp only: prime_factors_altdef_nat)
5.621    apply auto
5.623    apply (subst setprod.distrib)
5.624    apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"])
5.625 -  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un
5.626 +  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union>
5.627        (prime_factors l - prime_factors k)")
5.628    apply (erule ssubst)
5.629    apply (subst setprod.union_disjoint)
5.630    apply auto
5.631    apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
5.632 -  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un
5.633 +  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union>
5.634        (prime_factors k - prime_factors l)")
5.635    apply (erule ssubst)
5.636    apply (subst setprod.union_disjoint)
5.637    apply auto
5.638 -  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
5.639 +  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
5.640        (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
5.641    apply auto
5.642    apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
5.643    done
5.644
5.645 -(* transfer doesn't have the same problem here with the right
5.646 +(* transfer doesn't have the same problem here with the right
5.647     choice of rules. *)
5.648
5.649 -lemma multiplicity_product_aux_int:
5.650 +lemma multiplicity_product_aux_int:
5.651    assumes "(k::int) > 0" and "l > 0"
5.652 -  shows
5.653 -    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
5.654 -    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
5.655 +  shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and>
5.656 +    (\<forall>p \<ge> 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
5.657    apply (rule multiplicity_product_aux_nat [transferred, of l k])
5.658    using assms apply auto
5.659    done
5.660
5.661 -lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
5.662 -    prime_factors k Un prime_factors l"
5.663 +lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
5.664 +    prime_factors k \<union> prime_factors l"
5.665    by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
5.666
5.667 -lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
5.668 -    prime_factors k Un prime_factors l"
5.669 +lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
5.670 +    prime_factors k \<union> prime_factors l"
5.671    by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
5.672
5.673 -lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
5.674 +lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
5.675      multiplicity p k + multiplicity p l"
5.676 -  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format,
5.677 -      symmetric])
5.678 +  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric])
5.679
5.680 -lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow>
5.681 +lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
5.682      multiplicity p (k * l) = multiplicity p k + multiplicity p l"
5.683 -  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format,
5.684 -      symmetric])
5.685 +  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric])
5.686
5.687 -lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow>
5.688 -    multiplicity (p::nat) (PROD x : S. f x) =
5.689 -      (SUM x : S. multiplicity p (f x))"
5.690 +lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
5.691 +    multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
5.692    apply (induct set: finite)
5.693    apply auto
5.694    apply (subst multiplicity_product_nat)
5.695 @@ -517,33 +519,28 @@
5.696    done
5.697
5.698  (* Transfer is delicate here for two reasons: first, because there is
5.699 -   an implicit quantifier over functions (f), and, second, because the
5.700 -   product over the multiplicity should not be translated to an integer
5.701 +   an implicit quantifier over functions (f), and, second, because the
5.702 +   product over the multiplicity should not be translated to an integer
5.703     product.
5.704
5.705     The way to handle the first is to use quantifier rules for functions.
5.706     The way to handle the second is to turn off the offending rule.
5.707  *)
5.708
5.709 -lemma transfer_nat_int_sum_prod_closure3:
5.710 -  "(SUM x : A. int (f x)) >= 0"
5.711 -  "(PROD x : A. int (f x)) >= 0"
5.712 -  apply (rule setsum_nonneg, auto)
5.713 -  apply (rule setprod_nonneg, auto)
5.714 +lemma transfer_nat_int_sum_prod_closure3: "(\<Sum>x \<in> A. int (f x)) \<ge> 0" "(\<Prod>x \<in> A. int (f x)) \<ge> 0"
5.715 +  apply (rule setsum_nonneg; auto)
5.716 +  apply (rule setprod_nonneg; auto)
5.717    done
5.718
5.719 -declare transfer_morphism_nat_int[transfer
5.720 +declare transfer_morphism_nat_int[transfer
5.722    del: transfer_nat_int_sum_prod2 (1)]
5.723
5.724 -lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow>
5.725 -  (ALL x : S. f x > 0) \<Longrightarrow>
5.726 -    multiplicity (p::int) (PROD x : S. f x) =
5.727 -      (SUM x : S. multiplicity p (f x))"
5.728 -
5.729 +lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
5.730 +    multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
5.731    apply (frule multiplicity_setprod_nat
5.732 -    [where f = "%x. nat(int(nat(f x)))",
5.733 -      transferred direction: nat "op <= (0::int)"])
5.734 +    [where f = "\<lambda>x. nat(int(nat(f x)))",
5.735 +      transferred direction: nat "op \<le> (0::int)"])
5.736    apply auto
5.737    apply (subst (asm) setprod.cong)
5.738    apply (rule refl)
5.739 @@ -553,14 +550,13 @@
5.740    apply auto
5.741    done
5.742
5.743 -declare transfer_morphism_nat_int[transfer
5.744 +declare transfer_morphism_nat_int[transfer
5.746
5.747  lemma multiplicity_prod_prime_powers_nat:
5.748 -    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
5.749 -       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
5.750 -  apply (subgoal_tac "(PROD p : S. p ^ f p) =
5.751 -      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
5.752 +    "finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow>
5.753 +       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
5.754 +  apply (subgoal_tac "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ (\<lambda>x. if x \<in> S then f x else 0) p)")
5.755    apply (erule ssubst)
5.756    apply (subst multiplicity_characterization_nat)
5.757    prefer 5 apply (rule refl)
5.758 @@ -572,43 +568,43 @@
5.759    apply (rule setprod.cong)
5.760    apply (rule refl)
5.761    apply auto
5.762 -done
5.763 +  done
5.764
5.765  (* Here the issue with transfer is the implicit quantifier over S *)
5.766
5.767  lemma multiplicity_prod_prime_powers_int:
5.768 -    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow>
5.769 -       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
5.770 +    "(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow>
5.771 +       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
5.772    apply (subgoal_tac "int  nat  S = S")
5.773 -  apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
5.774 -    and S = "nat  S", transferred])
5.775 +  apply (frule multiplicity_prod_prime_powers_nat
5.776 +    [where f = "\<lambda>x. f(int x)" and S = "nat  S", transferred])
5.777    apply auto
5.778    apply (metis linear nat_0_iff zero_not_prime_nat)
5.779    apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
5.780    done
5.781
5.782 -lemma multiplicity_distinct_prime_power_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow>
5.783 -    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
5.784 -  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
5.785 +lemma multiplicity_distinct_prime_power_nat:
5.786 +    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
5.787 +  apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}")
5.788    apply (erule ssubst)
5.789    apply (subst multiplicity_prod_prime_powers_nat)
5.790    apply auto
5.791    done
5.792
5.793 -lemma multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow>
5.794 -    p ~= q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
5.795 +lemma multiplicity_distinct_prime_power_int:
5.796 +    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
5.797    by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
5.798
5.799 -
5.800  lemma dvd_multiplicity_nat:
5.801 -    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
5.802 +  fixes x y :: nat
5.803 +  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
5.804    apply (cases "x = 0")
5.805    apply (auto simp add: dvd_def multiplicity_product_nat)
5.806    done
5.807
5.808 -lemma dvd_multiplicity_int:
5.809 -    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow>
5.810 -      multiplicity p x <= multiplicity p y"
5.811 +lemma dvd_multiplicity_int:
5.812 +  fixes p x y :: int
5.813 +  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
5.814    apply (cases "x = 0")
5.815    apply (auto simp add: dvd_def)
5.816    apply (subgoal_tac "0 < k")
5.817 @@ -618,20 +614,23 @@
5.818    done
5.819
5.820  lemma dvd_prime_factors_nat [intro]:
5.821 -    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
5.822 +  fixes x y :: nat
5.823 +  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
5.824    apply (simp only: prime_factors_altdef_nat)
5.825    apply auto
5.826    apply (metis dvd_multiplicity_nat le_0_eq neq0_conv)
5.827    done
5.828
5.829  lemma dvd_prime_factors_int [intro]:
5.830 -    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
5.831 +  fixes x y :: int
5.832 +  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
5.833    apply (auto simp add: prime_factors_altdef_int)
5.834    apply (metis dvd_multiplicity_int le_0_eq neq0_conv)
5.835    done
5.836
5.837 -lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
5.838 -    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
5.839 +lemma multiplicity_dvd_nat:
5.840 +  fixes x y :: nat
5.841 +  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
5.842    apply (subst prime_factorization_nat [of x], assumption)
5.843    apply (subst prime_factorization_nat [of y], assumption)
5.844    apply (rule setprod_dvd_setprod_subset2)
5.845 @@ -642,8 +641,9 @@
5.846    apply (metis le_imp_power_dvd)
5.847    done
5.848
5.849 -lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
5.850 -    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
5.851 +lemma multiplicity_dvd_int:
5.852 +  fixes x y :: int
5.853 +  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
5.854    apply (subst prime_factorization_int [of x], assumption)
5.855    apply (subst prime_factorization_int [of y], assumption)
5.856    apply (rule setprod_dvd_setprod_subset2)
5.857 @@ -653,155 +653,171 @@
5.858    apply (metis le_imp_power_dvd prime_factors_ge_0_int)
5.859    done
5.860
5.861 -lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
5.862 -    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
5.863 +lemma multiplicity_dvd'_nat:
5.864 +  fixes x y :: nat
5.865 +  shows "0 < x \<Longrightarrow> \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
5.866    by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
5.867        multiplicity_nonprime_nat neq0_conv)
5.868
5.869 -lemma multiplicity_dvd'_int:
5.870 -  fixes x::int and y::int
5.871 -  shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow>
5.872 +lemma multiplicity_dvd'_int:
5.873 +  fixes x y :: int
5.874 +  shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
5.875      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
5.876 -by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
5.877 -          zero_le_imp_eq_int zero_less_imp_eq_int)
5.878 +  by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
5.879 +    zero_le_imp_eq_int zero_less_imp_eq_int)
5.880
5.881 -lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
5.882 -    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
5.883 +lemma dvd_multiplicity_eq_nat:
5.884 +  fixes x y :: nat
5.885 +  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
5.886    by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
5.887
5.888  lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
5.889 -    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
5.890 +    (x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)"
5.891    by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
5.892
5.893 -lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow>
5.894 -    (p : prime_factors n) = (prime p & p dvd n)"
5.895 +lemma prime_factors_altdef2_nat:
5.896 +  fixes n :: nat
5.897 +  shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
5.898    apply (cases "prime p")
5.899    apply auto
5.900    apply (subst prime_factorization_nat [where n = n], assumption)
5.901 -  apply (rule dvd_trans)
5.902 +  apply (rule dvd_trans)
5.903    apply (rule dvd_power [where x = p and n = "multiplicity p n"])
5.904    apply (subst (asm) prime_factors_altdef_nat, force)
5.905    apply rule
5.906    apply auto
5.907 -  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
5.908 +  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0
5.909 +    le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
5.910    done
5.911
5.912 -lemma prime_factors_altdef2_int:
5.913 -  assumes "(n::int) > 0"
5.914 -  shows "(p : prime_factors n) = (prime p & p dvd n)"
5.915 -using assms by (simp add:  prime_factors_altdef2_nat [transferred])
5.916 +lemma prime_factors_altdef2_int:
5.917 +  fixes n :: int
5.918 +  assumes "n > 0"
5.919 +  shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
5.920 +  using assms by (simp add:  prime_factors_altdef2_nat [transferred])
5.921
5.922  lemma multiplicity_eq_nat:
5.923 -  fixes x and y::nat
5.924 -  assumes [arith]: "x > 0" "y > 0" and
5.925 -    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
5.926 +  fixes x and y::nat
5.927 +  assumes [arith]: "x > 0" "y > 0"
5.928 +    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
5.929    shows "x = y"
5.930    apply (rule dvd_antisym)
5.931 -  apply (auto intro: multiplicity_dvd'_nat)
5.932 +  apply (auto intro: multiplicity_dvd'_nat)
5.933    done
5.934
5.935  lemma multiplicity_eq_int:
5.936 -  fixes x and y::int
5.937 -  assumes [arith]: "x > 0" "y > 0" and
5.938 -    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
5.939 +  fixes x y :: int
5.940 +  assumes [arith]: "x > 0" "y > 0"
5.941 +    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
5.942    shows "x = y"
5.943    apply (rule dvd_antisym [transferred])
5.944 -  apply (auto intro: multiplicity_dvd'_int)
5.945 +  apply (auto intro: multiplicity_dvd'_int)
5.946    done
5.947
5.948
5.949  subsection \<open>An application\<close>
5.950
5.951 -lemma gcd_eq_nat:
5.952 +lemma gcd_eq_nat:
5.953 +  fixes x y :: nat
5.954    assumes pos [arith]: "x > 0" "y > 0"
5.955 -  shows "gcd (x::nat) y =
5.956 -    (PROD p: prime_factors x Un prime_factors y.
5.957 -      p ^ (min (multiplicity p x) (multiplicity p y)))"
5.958 +  shows "gcd x y =
5.959 +    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
5.960 +  (is "_ = ?z")
5.961  proof -
5.962 -  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
5.963 -      p ^ (min (multiplicity p x) (multiplicity p y)))"
5.964 -  have [arith]: "z > 0"
5.965 -    unfolding z_def by (rule setprod_pos_nat, auto)
5.966 -  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
5.967 -      min (multiplicity p x) (multiplicity p y)"
5.968 -    unfolding z_def
5.969 +  have [arith]: "?z > 0"
5.970 +    by (rule setprod_pos_nat) auto
5.971 +  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
5.972      apply (subst multiplicity_prod_prime_powers_nat)
5.973      apply auto
5.974      done
5.975 -  have "z dvd x"
5.976 -    by (intro multiplicity_dvd'_nat, auto simp add: aux)
5.977 -  moreover have "z dvd y"
5.978 -    by (intro multiplicity_dvd'_nat, auto simp add: aux)
5.979 -  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
5.980 -    apply auto
5.981 -    apply (case_tac "w = 0", auto)
5.982 -    apply (erule multiplicity_dvd'_nat)
5.983 -    apply (auto intro: dvd_multiplicity_nat simp add: aux)
5.984 -    done
5.985 -  ultimately have "z = gcd x y"
5.986 +  have "?z dvd x"
5.987 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
5.988 +  moreover have "?z dvd y"
5.989 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
5.990 +  moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
5.991 +  proof (cases "w = 0")
5.992 +    case True
5.993 +    then show ?thesis by simp
5.994 +  next
5.995 +    case False
5.996 +    then show ?thesis
5.997 +      apply auto
5.998 +      apply (erule multiplicity_dvd'_nat)
5.999 +      apply (auto intro: dvd_multiplicity_nat simp add: aux)
5.1000 +      done
5.1001 +  qed
5.1002 +  ultimately have "?z = gcd x y"
5.1003      by (subst gcd_unique_nat [symmetric], blast)
5.1004    then show ?thesis
5.1005 -    unfolding z_def by auto
5.1006 +    by auto
5.1007  qed
5.1008
5.1009 -lemma lcm_eq_nat:
5.1010 +lemma lcm_eq_nat:
5.1011    assumes pos [arith]: "x > 0" "y > 0"
5.1012 -  shows "lcm (x::nat) y =
5.1013 -    (PROD p: prime_factors x Un prime_factors y.
5.1014 -      p ^ (max (multiplicity p x) (multiplicity p y)))"
5.1015 +  shows "lcm (x::nat) y =
5.1016 +    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
5.1017 +  (is "_ = ?z")
5.1018  proof -
5.1019 -  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
5.1020 -      p ^ (max (multiplicity p x) (multiplicity p y)))"
5.1021 -  have [arith]: "z > 0"
5.1022 -    unfolding z_def by (rule setprod_pos_nat, auto)
5.1023 -  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
5.1024 -      max (multiplicity p x) (multiplicity p y)"
5.1025 -    unfolding z_def
5.1026 +  have [arith]: "?z > 0"
5.1027 +    by (rule setprod_pos_nat, auto)
5.1028 +  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
5.1029      apply (subst multiplicity_prod_prime_powers_nat)
5.1030      apply auto
5.1031      done
5.1032 -  have "x dvd z"
5.1033 -    by (intro multiplicity_dvd'_nat, auto simp add: aux)
5.1034 -  moreover have "y dvd z"
5.1035 -    by (intro multiplicity_dvd'_nat, auto simp add: aux)
5.1036 -  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
5.1037 -    apply auto
5.1038 -    apply (case_tac "w = 0", auto)
5.1039 -    apply (rule multiplicity_dvd'_nat)
5.1040 -    apply (auto intro: dvd_multiplicity_nat simp add: aux)
5.1041 -    done
5.1042 -  ultimately have "z = lcm x y"
5.1043 +  have "x dvd ?z"
5.1044 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
5.1045 +  moreover have "y dvd ?z"
5.1046 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
5.1047 +  moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w
5.1048 +  proof (cases "w = 0")
5.1049 +    case True
5.1050 +    then show ?thesis by auto
5.1051 +  next
5.1052 +    case False
5.1053 +    then show ?thesis
5.1054 +      apply auto
5.1055 +      apply (rule multiplicity_dvd'_nat)
5.1056 +      apply (auto intro: dvd_multiplicity_nat simp add: aux)
5.1057 +      done
5.1058 +  qed
5.1059 +  ultimately have "?z = lcm x y"
5.1060      by (subst lcm_unique_nat [symmetric], blast)
5.1061    then show ?thesis
5.1062 -    unfolding z_def by auto
5.1063 +    by auto
5.1064  qed
5.1065
5.1066 -lemma multiplicity_gcd_nat:
5.1067 +lemma multiplicity_gcd_nat:
5.1068 +  fixes p x y :: nat
5.1069    assumes [arith]: "x > 0" "y > 0"
5.1070 -  shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
5.1071 +  shows "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
5.1072    apply (subst gcd_eq_nat)
5.1073    apply auto
5.1074    apply (subst multiplicity_prod_prime_powers_nat)
5.1075    apply auto
5.1076    done
5.1077
5.1078 -lemma multiplicity_lcm_nat:
5.1079 +lemma multiplicity_lcm_nat:
5.1080 +  fixes p x y :: nat
5.1081    assumes [arith]: "x > 0" "y > 0"
5.1082 -  shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
5.1083 +  shows "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
5.1084    apply (subst lcm_eq_nat)
5.1085    apply auto
5.1086    apply (subst multiplicity_prod_prime_powers_nat)
5.1087    apply auto
5.1088    done
5.1089
5.1090 -lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
5.1091 -  apply (cases "x = 0 | y = 0 | z = 0")
5.1092 +lemma gcd_lcm_distrib_nat:
5.1093 +  fixes x y z :: nat
5.1094 +  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
5.1095 +  apply (cases "x = 0 | y = 0 | z = 0")
5.1096    apply auto
5.1097    apply (rule multiplicity_eq_nat)
5.1098    apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
5.1099    done
5.1100
5.1101 -lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
5.1102 +lemma gcd_lcm_distrib_int:
5.1103 +  fixes x y z :: int
5.1104 +  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
5.1105    apply (subst (1 2 3) gcd_abs_int)
5.1106    apply (subst lcm_abs_int)
5.1107    apply (subst (2) abs_of_nonneg)
5.1108 @@ -811,4 +827,3 @@
5.1109    done
5.1110
5.1111  end
5.1112 -