src/HOL/Old_Number_Theory/Factorization.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 57983 6edc3529bb4e
child 58889 5b7a9633cfa8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
wenzelm@38159
     1
(*  Title:      HOL/Old_Number_Theory/Factorization.thy
wenzelm@38159
     2
    Author:     Thomas Marthedal Rasmussen
paulson@9944
     3
    Copyright   2000  University of Cambridge
wenzelm@11049
     4
*)
paulson@9944
     5
wenzelm@11049
     6
header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
wenzelm@11049
     7
haftmann@27368
     8
theory Factorization
wenzelm@41413
     9
imports Primes "~~/src/HOL/Library/Permutation"
haftmann@27368
    10
begin
paulson@9944
    11
paulson@9944
    12
wenzelm@11049
    13
subsection {* Definitions *}
paulson@9944
    14
wenzelm@38159
    15
definition primel :: "nat list => bool"
wenzelm@38159
    16
  where "primel xs = (\<forall>p \<in> set xs. prime p)"
wenzelm@19670
    17
wenzelm@38159
    18
primrec nondec :: "nat list => bool"
wenzelm@38159
    19
where
wenzelm@11049
    20
  "nondec [] = True"
wenzelm@38159
    21
| "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
paulson@9944
    22
wenzelm@38159
    23
primrec prod :: "nat list => nat"
wenzelm@38159
    24
where
wenzelm@11701
    25
  "prod [] = Suc 0"
wenzelm@38159
    26
| "prod (x # xs) = x * prod xs"
wenzelm@11049
    27
wenzelm@38159
    28
primrec oinsert :: "nat => nat list => nat list"
wenzelm@38159
    29
where
wenzelm@11049
    30
  "oinsert x [] = [x]"
wenzelm@38159
    31
| "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
paulson@9944
    32
wenzelm@38159
    33
primrec sort :: "nat list => nat list"
wenzelm@38159
    34
where
wenzelm@11049
    35
  "sort [] = []"
wenzelm@38159
    36
| "sort (x # xs) = oinsert x (sort xs)"
wenzelm@11049
    37
wenzelm@11049
    38
wenzelm@11049
    39
subsection {* Arithmetic *}
wenzelm@11049
    40
wenzelm@11701
    41
lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
wenzelm@19670
    42
  apply (cases m)
wenzelm@11049
    43
   apply auto
wenzelm@11049
    44
  done
wenzelm@11049
    45
wenzelm@11701
    46
lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
wenzelm@19670
    47
  apply (cases k)
wenzelm@11049
    48
   apply auto
wenzelm@11049
    49
  done
wenzelm@11049
    50
wenzelm@11049
    51
lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"
wenzelm@11049
    52
  apply auto
wenzelm@11049
    53
  done
wenzelm@11049
    54
wenzelm@11701
    55
lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
wenzelm@19670
    56
  apply (cases n)
wenzelm@11049
    57
   apply auto
wenzelm@11049
    58
  done
wenzelm@11049
    59
wenzelm@11049
    60
lemma prod_mn_less_k:
wenzelm@11701
    61
    "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
wenzelm@11049
    62
  apply (induct m)
wenzelm@11049
    63
   apply auto
wenzelm@11049
    64
  done
wenzelm@11049
    65
wenzelm@11049
    66
wenzelm@11049
    67
subsection {* Prime list and product *}
wenzelm@11049
    68
wenzelm@11049
    69
lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
wenzelm@11049
    70
  apply (induct xs)
haftmann@57512
    71
   apply (simp_all add: mult.assoc)
wenzelm@11049
    72
  done
wenzelm@11049
    73
wenzelm@11049
    74
lemma prod_xy_prod:
wenzelm@11049
    75
    "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"
wenzelm@11049
    76
  apply auto
wenzelm@11049
    77
  done
wenzelm@11049
    78
wenzelm@11049
    79
lemma primel_append: "primel (xs @ ys) = (primel xs \<and> primel ys)"
wenzelm@11049
    80
  apply (unfold primel_def)
wenzelm@11049
    81
  apply auto
wenzelm@11049
    82
  done
wenzelm@11049
    83
nipkow@16663
    84
lemma prime_primel: "prime n ==> primel [n] \<and> prod [n] = n"
wenzelm@11049
    85
  apply (unfold primel_def)
wenzelm@11049
    86
  apply auto
wenzelm@11049
    87
  done
wenzelm@11049
    88
nipkow@16663
    89
lemma prime_nd_one: "prime p ==> \<not> p dvd Suc 0"
wenzelm@11049
    90
  apply (unfold prime_def dvd_def)
wenzelm@11049
    91
  apply auto
wenzelm@11049
    92
  done
wenzelm@11049
    93
paulson@23814
    94
lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" 
paulson@23814
    95
  by (metis dvd_mult_left dvd_refl prod.simps(2))
wenzelm@11049
    96
wenzelm@11049
    97
lemma primel_tl: "primel (x # xs) ==> primel xs"
wenzelm@11049
    98
  apply (unfold primel_def)
wenzelm@11049
    99
  apply auto
wenzelm@11049
   100
  done
wenzelm@11049
   101
nipkow@16663
   102
lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)"
wenzelm@11049
   103
  apply (unfold primel_def)
wenzelm@11049
   104
  apply auto
wenzelm@11049
   105
  done
wenzelm@11049
   106
nipkow@16663
   107
lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
wenzelm@11049
   108
  apply (unfold prime_def)
wenzelm@11049
   109
  apply auto
wenzelm@11049
   110
  done
wenzelm@11049
   111
wenzelm@11701
   112
lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
wenzelm@19670
   113
  apply (cases xs)
wenzelm@19670
   114
   apply (simp_all add: primel_def prime_def)
wenzelm@11049
   115
  done
wenzelm@11049
   116
nipkow@16663
   117
lemma prime_g_one: "prime p ==> Suc 0 < p"
wenzelm@11049
   118
  apply (unfold prime_def)
wenzelm@11049
   119
  apply auto
wenzelm@11049
   120
  done
wenzelm@11049
   121
nipkow@16663
   122
lemma prime_g_zero: "prime p ==> 0 < p"
wenzelm@11049
   123
  apply (unfold prime_def)
wenzelm@11049
   124
  apply auto
wenzelm@11049
   125
  done
wenzelm@11049
   126
wenzelm@19670
   127
lemma primel_nempty_g_one:
wenzelm@19670
   128
    "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
wenzelm@11049
   129
  apply (induct xs)
wenzelm@19670
   130
   apply simp
nipkow@44890
   131
  apply (fastforce simp: primel_def prime_def elim: one_less_mult)
wenzelm@11049
   132
  done
wenzelm@11049
   133
wenzelm@11049
   134
lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
wenzelm@11049
   135
  apply (induct xs)
wenzelm@19670
   136
   apply (auto simp: primel_def prime_def)
wenzelm@11049
   137
  done
wenzelm@11049
   138
wenzelm@11049
   139
wenzelm@11049
   140
subsection {* Sorting *}
wenzelm@11049
   141
wenzelm@19670
   142
lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
wenzelm@11049
   143
  apply (induct xs)
wenzelm@19670
   144
   apply simp
wenzelm@19670
   145
   apply (case_tac xs)
blanchet@57983
   146
    apply (simp_all cong del: list.case_cong_weak)
wenzelm@11049
   147
  done
wenzelm@11049
   148
wenzelm@11049
   149
lemma nondec_sort: "nondec (sort xs)"
wenzelm@11049
   150
  apply (induct xs)
wenzelm@11049
   151
   apply simp_all
wenzelm@11049
   152
  apply (erule nondec_oinsert)
wenzelm@11049
   153
  done
wenzelm@11049
   154
wenzelm@11049
   155
lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l"
wenzelm@11049
   156
  apply simp_all
wenzelm@11049
   157
  done
wenzelm@11049
   158
wenzelm@19670
   159
lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
wenzelm@11049
   160
  apply (induct xs)
wenzelm@11049
   161
   apply safe
wenzelm@11049
   162
    apply simp_all
nipkow@15236
   163
   apply (case_tac xs)
wenzelm@11049
   164
    apply simp_all
nipkow@15236
   165
  apply (case_tac xs)
wenzelm@11049
   166
   apply simp
nipkow@15236
   167
  apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
wenzelm@11049
   168
   apply simp_all
wenzelm@11049
   169
  done
wenzelm@11049
   170
wenzelm@11049
   171
lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
wenzelm@11049
   172
  apply (induct l)
wenzelm@11049
   173
  apply auto
wenzelm@11049
   174
  done
wenzelm@11049
   175
wenzelm@11049
   176
wenzelm@11049
   177
subsection {* Permutation *}
wenzelm@11049
   178
wenzelm@11049
   179
lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
wenzelm@11049
   180
  apply (unfold primel_def)
wenzelm@19670
   181
  apply (induct set: perm)
nipkow@16663
   182
     apply simp
nipkow@16663
   183
    apply simp
nipkow@16663
   184
   apply (simp (no_asm))
nipkow@16663
   185
   apply blast
nipkow@16663
   186
  apply blast
wenzelm@11049
   187
  done
wenzelm@11049
   188
wenzelm@19670
   189
lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
wenzelm@19670
   190
  apply (induct set: perm)
haftmann@57514
   191
     apply (simp_all add: ac_simps)
wenzelm@11049
   192
  done
paulson@9944
   193
wenzelm@11049
   194
lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
wenzelm@19670
   195
  apply (induct set: perm)
wenzelm@11049
   196
     apply auto
wenzelm@11049
   197
  done
wenzelm@11049
   198
wenzelm@11049
   199
lemma perm_oinsert: "x # xs <~~> oinsert x xs"
wenzelm@11049
   200
  apply (induct xs)
wenzelm@11049
   201
   apply auto
wenzelm@11049
   202
  done
wenzelm@11049
   203
wenzelm@11049
   204
lemma perm_sort: "xs <~~> sort xs"
wenzelm@11049
   205
  apply (induct xs)
wenzelm@11049
   206
  apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
wenzelm@11049
   207
  done
wenzelm@11049
   208
wenzelm@11049
   209
lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
wenzelm@19670
   210
  apply (induct set: perm)
wenzelm@11049
   211
     apply (simp_all add: oinsert_x_y)
wenzelm@11049
   212
  done
wenzelm@11049
   213
wenzelm@11049
   214
wenzelm@11049
   215
subsection {* Existence *}
wenzelm@11049
   216
wenzelm@11049
   217
lemma ex_nondec_lemma:
wenzelm@11049
   218
    "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
wenzelm@11049
   219
  apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
wenzelm@11049
   220
  done
wenzelm@11049
   221
wenzelm@11049
   222
lemma not_prime_ex_mk:
nipkow@16663
   223
  "Suc 0 < n \<and> \<not> prime n ==>
wenzelm@11701
   224
    \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
wenzelm@11049
   225
  apply (unfold prime_def dvd_def)
wenzelm@11049
   226
  apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
wenzelm@11049
   227
  done
wenzelm@11049
   228
wenzelm@11049
   229
lemma split_primel:
wenzelm@25687
   230
  "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
wenzelm@25687
   231
  apply (rule exI)
wenzelm@25687
   232
  apply safe
wenzelm@25687
   233
   apply (rule_tac [2] prod_append)
wenzelm@25687
   234
  apply (simp add: primel_append)
wenzelm@25687
   235
  done
wenzelm@11049
   236
wenzelm@11701
   237
lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
wenzelm@11049
   238
  apply (induct n rule: nat_less_induct)
wenzelm@11049
   239
  apply (rule impI)
nipkow@16663
   240
  apply (case_tac "prime n")
wenzelm@11049
   241
   apply (rule exI)
wenzelm@11049
   242
   apply (erule prime_primel)
wenzelm@11049
   243
  apply (cut_tac n = n in not_prime_ex_mk)
wenzelm@11049
   244
   apply (auto intro!: split_primel)
wenzelm@11049
   245
  done
wenzelm@11049
   246
wenzelm@11701
   247
lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
wenzelm@11049
   248
  apply (erule factor_exists [THEN exE])
wenzelm@11049
   249
  apply (blast intro!: ex_nondec_lemma)
wenzelm@11049
   250
  done
wenzelm@11049
   251
wenzelm@11049
   252
wenzelm@11049
   253
subsection {* Uniqueness *}
wenzelm@11049
   254
wenzelm@11049
   255
lemma prime_dvd_mult_list [rule_format]:
nipkow@16663
   256
    "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
wenzelm@11049
   257
  apply (induct xs)
paulson@11364
   258
   apply (force simp add: prime_def)
paulson@11364
   259
   apply (force dest: prime_dvd_mult)
wenzelm@11049
   260
  done
wenzelm@11049
   261
wenzelm@11049
   262
lemma hd_xs_dvd_prod:
wenzelm@11049
   263
  "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys
wenzelm@11049
   264
    ==> \<exists>m. m \<in> set ys \<and> x dvd m"
wenzelm@11049
   265
  apply (rule prime_dvd_mult_list)
wenzelm@11049
   266
   apply (simp add: primel_hd_tl)
wenzelm@11049
   267
  apply (erule hd_dvd_prod)
wenzelm@11049
   268
  done
wenzelm@11049
   269
wenzelm@11049
   270
lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m"
wenzelm@11049
   271
  apply (rule primes_eq)
wenzelm@11049
   272
    apply (auto simp add: primel_def primel_hd_tl)
wenzelm@11049
   273
  done
paulson@9944
   274
wenzelm@11049
   275
lemma hd_xs_eq_prod:
wenzelm@11049
   276
  "primel (x # xs) ==>
wenzelm@11049
   277
    primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys"
wenzelm@11049
   278
  apply (frule hd_xs_dvd_prod)
wenzelm@11049
   279
    apply auto
wenzelm@11049
   280
  apply (drule prime_dvd_eq)
wenzelm@11049
   281
     apply auto
wenzelm@11049
   282
  done
wenzelm@11049
   283
wenzelm@11049
   284
lemma perm_primel_ex:
wenzelm@11049
   285
  "primel (x # xs) ==>
wenzelm@11049
   286
    primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)"
wenzelm@11049
   287
  apply (rule exI)
wenzelm@11049
   288
  apply (rule perm_remove)
wenzelm@11049
   289
  apply (erule hd_xs_eq_prod)
wenzelm@11049
   290
   apply simp_all
wenzelm@11049
   291
  done
wenzelm@11049
   292
wenzelm@11049
   293
lemma primel_prod_less:
wenzelm@11049
   294
  "primel (x # xs) ==>
wenzelm@11049
   295
    primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
wenzelm@26316
   296
  by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
wenzelm@25180
   297
    nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
wenzelm@11049
   298
wenzelm@11049
   299
lemma prod_one_empty:
nipkow@16663
   300
    "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
wenzelm@11049
   301
  apply (auto intro: primel_one_empty simp add: prime_def)
wenzelm@11049
   302
  done
wenzelm@11049
   303
wenzelm@11049
   304
lemma uniq_ex_aux:
wenzelm@11049
   305
  "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
wenzelm@11049
   306
      prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==>
wenzelm@11049
   307
    primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys
wenzelm@11049
   308
    ==> x <~~> list"
wenzelm@11049
   309
  apply simp
wenzelm@11049
   310
  done
paulson@9944
   311
wenzelm@11049
   312
lemma factor_unique [rule_format]:
wenzelm@11049
   313
  "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n
wenzelm@11049
   314
    --> xs <~~> ys"
wenzelm@11049
   315
  apply (induct n rule: nat_less_induct)
wenzelm@11049
   316
  apply safe
wenzelm@11049
   317
  apply (case_tac xs)
wenzelm@11049
   318
   apply (force intro: primel_one_empty)
wenzelm@11049
   319
  apply (rule perm_primel_ex [THEN exE])
wenzelm@11049
   320
     apply simp_all
wenzelm@11049
   321
  apply (rule perm.trans [THEN perm_sym])
wenzelm@11049
   322
  apply assumption
wenzelm@11049
   323
  apply (rule perm.Cons)
wenzelm@11049
   324
  apply (case_tac "x = []")
paulson@25493
   325
   apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty)
paulson@25493
   326
  apply (metis nat_0_less_mult_iff nat_mult_eq_cancel1 perm_primel perm_prod primel_prod_gz primel_prod_less primel_tl prod.simps(2))
wenzelm@11049
   327
  done
wenzelm@11049
   328
wenzelm@11049
   329
lemma perm_nondec_unique:
wenzelm@11049
   330
    "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"
paulson@23814
   331
  by (metis nondec_sort_eq perm_sort_eq)
paulson@23814
   332
paulson@25493
   333
theorem unique_prime_factorization [rule_format]:
wenzelm@11701
   334
    "\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
paulson@25493
   335
  by (metis factor_unique nondec_factor_exists perm_nondec_unique)
wenzelm@11049
   336
wenzelm@11049
   337
end