src/HOL/Algebra/abstract/Factor.ML
author paulson
Fri Nov 05 11:14:26 1999 +0100 (1999-11-05)
changeset 7998 3d0c34795831
child 10448 da7d0e28f746
permissions -rw-r--r--
Algebra and Polynomial theories, by Clemens Ballarin
paulson@7998
     1
(*
paulson@7998
     2
    Factorisation within a factorial domain
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 25 November 1997
paulson@7998
     5
*)
paulson@7998
     6
paulson@7998
     7
open Factor;
paulson@7998
     8
paulson@7998
     9
goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
paulson@7998
    10
\  [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
paulson@7998
    11
by (ftac factorial_prime 1);
paulson@7998
    12
by (rewrite_goals_tac [irred_def, prime_def]);
paulson@7998
    13
by (Blast_tac 1);
paulson@7998
    14
qed "irred_dvd_lemma";
paulson@7998
    15
paulson@7998
    16
goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
paulson@7998
    17
\  [| irred c; a dvd <1> |] ==> \
paulson@7998
    18
\  (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
paulson@7998
    19
\  (EX d. c assoc d & d : set factors)";
paulson@7998
    20
by (induct_tac "factors" 1);
paulson@7998
    21
(* Base case: c dvd a contradicts irred c *)
paulson@7998
    22
by (full_simp_tac (simpset() addsimps [irred_def]) 1);
paulson@7998
    23
by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
paulson@7998
    24
(* Induction step *)
paulson@7998
    25
by (ftac factorial_prime 1);
paulson@7998
    26
by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
paulson@7998
    27
by (Blast_tac 1);
paulson@7998
    28
qed "irred_dvd_list_lemma";
paulson@7998
    29
paulson@7998
    30
goal Ring.thy "!! c::'a::factorial. \
paulson@7998
    31
\  [| irred c; ALL b : set factors. irred b; a dvd <1>; \
paulson@7998
    32
\    c dvd foldr op* factors a |] ==> \
paulson@7998
    33
\  EX d. c assoc d & d : set factors";
paulson@7998
    34
by (rtac (irred_dvd_list_lemma RS mp) 1);
paulson@7998
    35
by (Auto_tac);
paulson@7998
    36
qed "irred_dvd_list";
paulson@7998
    37
paulson@7998
    38
Goalw [Factorisation_def] "!! c::'a::factorial. \
paulson@7998
    39
\  [| irred c; Factorisation x factors u; c dvd x |] ==> \
paulson@7998
    40
\  EX d. c assoc d & d : set factors";
paulson@7998
    41
by (rtac (irred_dvd_list_lemma RS mp) 1);
paulson@7998
    42
by (Auto_tac);
paulson@7998
    43
qed "Factorisation_dvd";
paulson@7998
    44
paulson@7998
    45
Goalw [Factorisation_def] "!! c::'a::factorial. \
paulson@7998
    46
\  [| Factorisation x factors u; a : set factors |] ==> irred a";
paulson@7998
    47
by (Blast_tac 1);
paulson@7998
    48
qed "Factorisation_irred";
paulson@7998
    49