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