Up to index of Isabelle/HOL/HOL-Algebra
theory Factor(* 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 [.]