src/HOL/Algebra/abstract/Factor.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 13735 7de9342aca7a
child 17479 68a7acb5f22e
permissions -rw-r--r--
Constant "If" is now local
     1 (*
     2     Factorisation within a factorial domain
     3     $Id$
     4     Author: Clemens Ballarin, started 25 November 1997
     5 *)
     6 
     7 Goalw [thm "assoc_def"] "!! c::'a::factorial. \
     8 \  [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
     9 by (ftac (thm "factorial_prime") 1);
    10 by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
    11 by (Blast_tac 1);
    12 qed "irred_dvd_lemma";
    13 
    14 Goalw [thm "assoc_def"] "!! c::'a::factorial. \
    15 \  [| irred c; a dvd 1 |] ==> \
    16 \  (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
    17 \  (EX d. c assoc d & d : set factors)";
    18 by (induct_tac "factors" 1);
    19 (* Base case: c dvd a contradicts irred c *)
    20 by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
    21 by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
    22 (* Induction step *)
    23 by (ftac (thm "factorial_prime") 1);
    24 by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
    25 by (Blast_tac 1);
    26 qed "irred_dvd_list_lemma";
    27 
    28 Goal "!! c::'a::factorial. \
    29 \  [| irred c; ALL b : set factors. irred b; a dvd 1; \
    30 \    c dvd foldr op* factors a |] ==> \
    31 \  EX d. c assoc d & d : set factors";
    32 by (rtac (irred_dvd_list_lemma RS mp) 1);
    33 by (Auto_tac);
    34 qed "irred_dvd_list";
    35 
    36 Goalw [Factorisation_def] "!! c::'a::factorial. \
    37 \  [| irred c; Factorisation x factors u; c dvd x |] ==> \
    38 \  EX d. c assoc d & d : set factors";
    39 by (rtac (irred_dvd_list_lemma RS mp) 1);
    40 by (Auto_tac);
    41 qed "Factorisation_dvd";
    42 
    43 Goalw [Factorisation_def] "!! c::'a::factorial. \
    44 \  [| Factorisation x factors u; a : set factors |] ==> irred a";
    45 by (Blast_tac 1);
    46 qed "Factorisation_irred";
    47