src/HOL/NumberTheory/Factorization.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9944 2a705d1af4dc
child 10700 b18f417d0b62
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Factorization.thy
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     2
    ID:         $Id$
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     3
    Author:     Thomas Marthedal Rasmussen
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     5
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     6
Fundamental Theorem of Arithmetic (unique factorization into primes)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     7
*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     8
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     9
val prime_def = thm "prime_def";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    10
val prime_dvd_mult = thm "prime_dvd_mult";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    11
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    12
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    13
(* --- Arithmetic --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    14
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    15
Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1<m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    16
by (case_tac "m" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    17
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    18
qed "one_less_m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    19
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    20
Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    21
by (case_tac "k" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    22
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    23
qed "one_less_k";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    24
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    25
Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    26
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    27
qed "mult_left_cancel";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    28
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    29
Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    30
by (case_tac "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    31
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    32
qed "mn_eq_m_one";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    33
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    34
Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    35
by (induct_tac "m" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    36
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    37
qed_spec_mp "prod_mn_less_k";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    38
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    39
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    40
(* --- Prime List & Product --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    41
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    42
Goal "prod (xs @ ys) = prod xs * prod ys"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    43
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    44
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    45
qed "prod_append";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    46
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    47
Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    48
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    49
qed "prod_xy_prod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    50
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    51
Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    52
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    53
qed "primel_append";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    54
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    55
Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    56
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    57
qed "prime_primel";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    58
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    59
Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    60
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    61
by (case_tac "k" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    62
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    63
qed "prime_nd_one";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    64
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    65
Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    66
by (rtac exI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    67
by (rtac sym 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    68
by (Asm_full_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    69
qed "hd_dvd_prod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    70
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    71
Goalw [primel_def] "primel (x#xs) ==> primel xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    72
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    73
qed "primel_tl";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    74
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    75
Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    76
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    77
qed "primel_hd_tl";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    78
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    79
Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    80
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    81
qed "primes_eq";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    82
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    83
Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    84
by (case_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    85
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    86
qed "primel_one_empty";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    87
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    88
Goalw [prime_def] "p:prime ==> 1<p";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    89
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    90
qed "prime_g_one";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    91
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    92
Goalw [prime_def] "p:prime ==> 0<p";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    93
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    94
qed "prime_g_zero";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    95
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    96
Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    97
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    98
by (auto_tac (claset() addEs [one_less_mult], simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    99
qed_spec_mp "primel_nempty_g_one";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   100
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   101
Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   102
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   103
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   104
qed_spec_mp "primel_prod_gz";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   105
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   106
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   107
(* --- Sorting --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   108
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   109
Goal "nondec xs --> nondec (oinsert x xs)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   110
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   111
by (case_tac "list" 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   112
by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   113
qed_spec_mp "nondec_oinsert";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   114
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   115
Goal "nondec (sort xs)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   116
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   117
by (ALLGOALS (Asm_full_simp_tac));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   118
by (etac nondec_oinsert 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   119
qed "nondec_sort";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   120
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   121
Goal "[| x<=y; l=y#ys |]  ==> x#l = oinsert x l";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   122
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   123
qed "x_less_y_oinsert";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   124
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   125
Goal "nondec xs --> xs = sort xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   126
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   127
by Safe_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   128
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   129
by (case_tac "list" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   130
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   131
by (case_tac "list" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   132
by (Asm_full_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   133
by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   134
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   135
qed_spec_mp "nondec_sort_eq";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   136
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   137
Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   138
by (induct_tac "l" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   139
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   140
qed "oinsert_x_y";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   141
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   142
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   143
(* --- Permutation --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   144
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   145
Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   146
by (etac perm.induct 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   147
by (ALLGOALS Asm_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   148
qed_spec_mp "perm_primel";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   149
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   150
Goal "xs <~~> ys ==> prod xs = prod ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   151
by (etac perm.induct 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   152
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   153
qed_spec_mp "perm_prod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   154
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   155
Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   156
by (etac perm.induct 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   157
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   158
qed "perm_subst_oinsert";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   159
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   160
Goal "x#xs <~~> oinsert x xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   161
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   162
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   163
qed "perm_oinsert";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   164
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   165
Goal "xs <~~> sort xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   166
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   167
by (auto_tac (claset() addIs [perm_oinsert] 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   168
	               addEs [perm_subst_oinsert],
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   169
              simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   170
qed "perm_sort";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   171
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   172
Goal "xs <~~> ys ==> sort xs = sort ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   173
by (etac perm.induct 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   174
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   175
qed "perm_sort_eq";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   176
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   177
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   178
(* --- Existence --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   179
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   180
Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   181
by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   182
			       perm_sym]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   183
qed "ex_nondec_lemma";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   184
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   185
Goalw [prime_def,dvd_def]
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   186
     "1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   187
by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   188
			      one_less_m, one_less_k], 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   189
	      simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   190
qed_spec_mp "not_prime_ex_mk";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   191
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   192
Goal "[| primel xs; primel ys |] \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   193
\     ==> EX l. primel l & prod l = prod xs * prod ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   194
by (rtac exI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   195
by Safe_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   196
by (rtac prod_append 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   197
by (asm_simp_tac (simpset() addsimps [primel_append]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   198
qed "split_primel";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   199
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   200
Goal "1<n --> (EX l. primel l & prod l = n)"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   201
by (induct_thm_tac nat_less_induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   202
by (rtac impI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   203
by (case_tac "n:prime" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   204
by (rtac exI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   205
by (etac prime_primel 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   206
by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   207
by (auto_tac (claset() addSIs [split_primel], simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   208
qed_spec_mp "factor_exists";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   209
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   210
Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   211
by (etac (factor_exists RS exE) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   212
by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   213
qed "nondec_factor_exists";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   214
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   215
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   216
(* --- Uniqueness --- *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   217
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   218
Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   219
by (induct_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   220
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   221
by (etac prime_nd_one 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   222
by (rtac impI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   223
by (dtac prime_dvd_mult 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   224
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   225
qed_spec_mp "prime_dvd_mult_list";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   226
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   227
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   228
\     ==> EX m. m :set ys & x dvd m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   229
by (rtac prime_dvd_mult_list 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   230
by (etac hd_dvd_prod 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   231
by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   232
qed "hd_xs_dvd_prod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   233
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   234
Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   235
by (rtac primes_eq 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   236
by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   237
qed "prime_dvd_eq";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   238
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   239
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   240
by (ftac hd_xs_dvd_prod 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   241
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   242
by (dtac prime_dvd_eq 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   243
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   244
qed "hd_xs_eq_prod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   245
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   246
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   247
\     ==> EX l. ys <~~> (x#l)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   248
by (rtac exI 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   249
by (rtac perm_remove 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   250
by (etac hd_xs_eq_prod 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   251
by (ALLGOALS assume_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   252
qed "perm_primel_ex";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   253
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   254
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   255
\     ==> prod xs < prod ys";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   256
by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   257
              simpset() addsimps [primel_hd_tl]));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   258
qed "primel_prod_less";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   259
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   260
Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   261
by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero], 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   262
	      simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   263
qed "prod_one_empty";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   264
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   265
Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   266
\        prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   267
\        primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   268
by (Asm_full_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   269
qed "uniq_ex_lemma";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   270
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   271
Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   272
\     --> xs <~~> ys)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   273
by (induct_thm_tac nat_less_induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   274
by Safe_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   275
by (case_tac "xs" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   276
by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   277
by (rtac (perm_primel_ex RS exE) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   278
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   279
by (rtac (perm.trans RS perm_sym) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   280
by (assume_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   281
by (rtac perm.Cons 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   282
by (case_tac "x=[]" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   283
by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   284
by (res_inst_tac [("p","a")] prod_one_empty 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   285
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   286
by (etac uniq_ex_lemma 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   287
by (auto_tac (claset() addIs [primel_tl,perm_primel],
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   288
	      simpset() addsimps [primel_hd_tl]));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   289
by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   290
by (res_inst_tac [("x","a")] primel_prod_less 3);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   291
by (rtac prod_xy_prod 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   292
by (res_inst_tac [("s","prod ys")] trans 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   293
by (etac perm_prod 3);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   294
by (etac (perm_prod RS sym) 5); 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   295
by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   296
qed_spec_mp "factor_unique";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   297
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   298
Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   299
by (rtac trans 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   300
by (rtac trans 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   301
by (etac nondec_sort_eq 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   302
by (etac perm_sort_eq 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   303
by (etac (nondec_sort_eq RS sym) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   304
qed "perm_nondec_unique";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   305
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   306
Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   307
by Safe_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   308
by (etac nondec_factor_exists 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   309
by (rtac perm_nondec_unique 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   310
by (rtac factor_unique 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   311
by (ALLGOALS Asm_full_simp_tac);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   312
qed_spec_mp "unique_prime_factorization";