src/HOL/Algebra/abstract/Factor.ML
author ballarin
Thu Nov 28 10:50:42 2002 +0100 (2002-11-28)
changeset 13735 7de9342aca7a
parent 10789 260fa2c67e3e
child 17479 68a7acb5f22e
permissions -rw-r--r--
HOL-Algebra partially ported to Isar.
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
ballarin@13735
     7
Goalw [thm "assoc_def"] "!! c::'a::factorial. \
nipkow@10789
     8
\  [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
ballarin@13735
     9
by (ftac (thm "factorial_prime") 1);
ballarin@13735
    10
by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
paulson@7998
    11
by (Blast_tac 1);
paulson@7998
    12
qed "irred_dvd_lemma";
paulson@7998
    13
ballarin@13735
    14
Goalw [thm "assoc_def"] "!! c::'a::factorial. \
ballarin@13735
    15
\  [| irred c; a dvd 1 |] ==> \
paulson@7998
    16
\  (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
paulson@7998
    17
\  (EX d. c assoc d & d : set factors)";
paulson@7998
    18
by (induct_tac "factors" 1);
paulson@7998
    19
(* Base case: c dvd a contradicts irred c *)
ballarin@13735
    20
by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
paulson@7998
    21
by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
paulson@7998
    22
(* Induction step *)
ballarin@13735
    23
by (ftac (thm "factorial_prime") 1);
ballarin@13735
    24
by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
paulson@7998
    25
by (Blast_tac 1);
paulson@7998
    26
qed "irred_dvd_list_lemma";
paulson@7998
    27
ballarin@13735
    28
Goal "!! c::'a::factorial. \
ballarin@13735
    29
\  [| irred c; ALL b : set factors. irred b; a dvd 1; \
paulson@7998
    30
\    c dvd foldr op* factors a |] ==> \
paulson@7998
    31
\  EX d. c assoc d & d : set factors";
paulson@7998
    32
by (rtac (irred_dvd_list_lemma RS mp) 1);
paulson@7998
    33
by (Auto_tac);
paulson@7998
    34
qed "irred_dvd_list";
paulson@7998
    35
paulson@7998
    36
Goalw [Factorisation_def] "!! c::'a::factorial. \
paulson@7998
    37
\  [| irred c; Factorisation x factors u; c dvd x |] ==> \
paulson@7998
    38
\  EX d. c assoc d & d : set factors";
paulson@7998
    39
by (rtac (irred_dvd_list_lemma RS mp) 1);
paulson@7998
    40
by (Auto_tac);
paulson@7998
    41
qed "Factorisation_dvd";
paulson@7998
    42
paulson@7998
    43
Goalw [Factorisation_def] "!! c::'a::factorial. \
paulson@7998
    44
\  [| Factorisation x factors u; a : set factors |] ==> irred a";
paulson@7998
    45
by (Blast_tac 1);
paulson@7998
    46
qed "Factorisation_irred";
paulson@7998
    47