isabelle: src/HOL/Algebra/abstract/Factor.ML@b8bb6a6a2c46 (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Factorisation within a factorial domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 25 November 1997
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	7	Goalw [thm "assoc_def"] "!! c::'a::factorial. \
10789 260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation. nipkow parents: 10448 diff changeset	8	\ [\| irred c; irred a; irred b; c dvd a*b \|] ==> c assoc a \| c assoc b";
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	9	by (ftac (thm "factorial_prime") 1);
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	10	by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	qed "irred_dvd_lemma";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	14	Goalw [thm "assoc_def"] "!! c::'a::factorial. \
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	15	\ [\| irred c; a dvd 1 \|] ==> \
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17	\ (EX d. c assoc d & d : set factors)";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	by (induct_tac "factors" 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	(* Base case: c dvd a contradicts irred c *)
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	20	by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21	by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22	(* Induction step *)
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	23	by (ftac (thm "factorial_prime") 1);
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	24	by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	25	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	26	qed "irred_dvd_list_lemma";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	27
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	28	Goal "!! c::'a::factorial. \
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 10789 diff changeset	29	\ [\| irred c; ALL b : set factors. irred b; a dvd 1; \
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	30	\ c dvd foldr op* factors a \|] ==> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	31	\ EX d. c assoc d & d : set factors";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	32	by (rtac (irred_dvd_list_lemma RS mp) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	33	by (Auto_tac);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	34	qed "irred_dvd_list";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	35
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	36	Goalw [Factorisation_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	37	\ [\| irred c; Factorisation x factors u; c dvd x \|] ==> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	38	\ EX d. c assoc d & d : set factors";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	39	by (rtac (irred_dvd_list_lemma RS mp) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	40	by (Auto_tac);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	41	qed "Factorisation_dvd";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	42
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	43	Goalw [Factorisation_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	44	\ [\| Factorisation x factors u; a : set factors \|] ==> irred a";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	45	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	46	qed "Factorisation_irred";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	47

author	paulson
	Fri, 15 Aug 2003 13:45:39 +0200
changeset 14151	b8bb6a6a2c46
parent 13735	7de9342aca7a
child 17479	68a7acb5f22e
permissions	-rw-r--r--