35849
|
1 |
(* Author: Clemens Ballarin, started 25 November 1997
|
|
2 |
|
|
3 |
Factorisation within a factorial domain.
|
7998
|
4 |
*)
|
|
5 |
|
35849
|
6 |
theory Factor
|
|
7 |
imports Ring2
|
|
8 |
begin
|
7998
|
9 |
|
21423
|
10 |
definition
|
|
11 |
Factorisation :: "['a::ring, 'a list, 'a] => bool" where
|
7998
|
12 |
(* factorisation of x into a list of irred factors and a unit u *)
|
21423
|
13 |
"Factorisation x factors u \<longleftrightarrow>
|
17479
|
14 |
x = foldr op* factors u &
|
|
15 |
(ALL a : set factors. irred a) & u dvd 1"
|
7998
|
16 |
|
21423
|
17 |
lemma irred_dvd_lemma: "!! c::'a::factorial.
|
|
18 |
[| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"
|
|
19 |
apply (unfold assoc_def)
|
|
20 |
apply (frule factorial_prime)
|
|
21 |
apply (unfold irred_def prime_def)
|
|
22 |
apply blast
|
|
23 |
done
|
|
24 |
|
|
25 |
lemma irred_dvd_list_lemma: "!! c::'a::factorial.
|
|
26 |
[| irred c; a dvd 1 |] ==>
|
|
27 |
(ALL b : set factors. irred b) & c dvd foldr op* factors a -->
|
|
28 |
(EX d. c assoc d & d : set factors)"
|
|
29 |
apply (unfold assoc_def)
|
|
30 |
apply (induct_tac factors)
|
|
31 |
(* Base case: c dvd a contradicts irred c *)
|
|
32 |
apply (simp add: irred_def)
|
|
33 |
apply (blast intro: dvd_trans_ring)
|
|
34 |
(* Induction step *)
|
|
35 |
apply (frule factorial_prime)
|
|
36 |
apply (simp add: irred_def prime_def)
|
|
37 |
apply blast
|
|
38 |
done
|
|
39 |
|
|
40 |
lemma irred_dvd_list: "!! c::'a::factorial.
|
|
41 |
[| irred c; ALL b : set factors. irred b; a dvd 1;
|
|
42 |
c dvd foldr op* factors a |] ==>
|
|
43 |
EX d. c assoc d & d : set factors"
|
|
44 |
apply (rule irred_dvd_list_lemma [THEN mp])
|
|
45 |
apply auto
|
|
46 |
done
|
|
47 |
|
|
48 |
lemma Factorisation_dvd: "!! c::'a::factorial.
|
|
49 |
[| irred c; Factorisation x factors u; c dvd x |] ==>
|
|
50 |
EX d. c assoc d & d : set factors"
|
|
51 |
apply (unfold Factorisation_def)
|
|
52 |
apply (rule irred_dvd_list_lemma [THEN mp])
|
|
53 |
apply auto
|
|
54 |
done
|
|
55 |
|
|
56 |
lemma Factorisation_irred: "!! c::'a::factorial.
|
|
57 |
[| Factorisation x factors u; a : set factors |] ==> irred a"
|
|
58 |
unfolding Factorisation_def by blast
|
|
59 |
|
7998
|
60 |
end
|