Theory Factor

Up to index of Isabelle/HOL/HOL-Algebra

theory Factor
imports Ring2
`(*  Author: Clemens Ballarin, started 25 November 1997Factorisation within a factorial domain.*)theory Factorimports Ring2begindefinition  Factorisation :: "['a::ring, 'a list, 'a] => bool" where  (* 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"lemma irred_dvd_lemma: "!! c::'a::factorial.   [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"  apply (unfold assoc_def)  apply (frule factorial_prime)  apply (unfold irred_def prime_def)  apply blast  donelemma irred_dvd_list_lemma: "!! c::'a::factorial.   [| irred c; a dvd 1 |] ==>     (ALL b : set factors. irred b) & c dvd foldr op* factors a -->     (EX d. c assoc d & d : set factors)"  apply (unfold assoc_def)  apply (induct_tac factors)  (* Base case: c dvd a contradicts irred c *)   apply (simp add: irred_def)   apply (blast intro: dvd_trans_ring)  (* Induction step *)  apply (frule factorial_prime)  apply (simp add: irred_def prime_def)  apply blast  donelemma irred_dvd_list: "!! c::'a::factorial.     [| irred c; ALL b : set factors. irred b; a dvd 1;       c dvd foldr op* factors a |] ==>     EX d. c assoc d & d : set factors"  apply (rule irred_dvd_list_lemma [THEN mp])    apply auto  donelemma Factorisation_dvd: "!! c::'a::factorial.     [| irred c; Factorisation x factors u; c dvd x |] ==>     EX d. c assoc d & d : set factors"  apply (unfold Factorisation_def)  apply (rule irred_dvd_list_lemma [THEN mp])    apply auto  donelemma Factorisation_irred: "!! c::'a::factorial.    [| Factorisation x factors u; a : set factors |] ==> irred a"  unfolding Factorisation_def by blastend`