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