# Theory Factor

Up to index of Isabelle/HOL/HOL-Algebra

theory Factor
imports Ring
uses [Factor.ML]
begin

    (*
        Factorisation within a factorial domain
        $Id: Factor.thy,v 1.3 2005/09/17 18:49:14 wenzelm Exp $
        Author: Clemens Ballarin, started 25 November 1997
    *)

    theory Factor imports Ring begin

    constdefs
      Factorisation :: "['a::ring, 'a list, 'a] => bool"
      (* factorisation of x into a list of irred factors and a unit u *)
      "Factorisation x factors u ==
         x = foldr op* factors u &
         (ALL a : set factors. irred a) & u dvd 1"

    end

theorem irred_dvd_lemma:

      [| irred c; irred a; irred b; c dvd a * b |] ==> c assoc a ∨ c assoc b

theorem irred_dvd_list_lemma:

      [| irred c; a dvd (1::'a) |]
      ==> (∀b∈set factors. irred b) ∧ c dvd foldr op * factors a -->
          (∃d. c assoc d ∧ d ∈ set factors)

theorem irred_dvd_list:

      [| irred c; ∀b∈set factors. irred b; a dvd (1::'a);
         c dvd foldr op * factors a |]
      ==> ∃d. c assoc d ∧ d ∈ set factors

theorem Factorisation_dvd:

      [| irred c; Factorisation x factors u; c dvd x |]
      ==> ∃d. c assoc d ∧ d ∈ set factors

theorem Factorisation_irred:

      [| Factorisation x factors u; a ∈ set factors |] ==> irred a  [.]