isabelle: src/HOL/Algebra/abstract/Factor.ML@8b2eafed6183 (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
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7	goalw Ring.thy [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";
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	by (ftac factorial_prime 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10	by (rewrite_goals_tac [irred_def, prime_def]);
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
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	\ [\| irred c; a dvd <1> \|] ==> \
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 *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20	by (full_simp_tac (simpset() addsimps [irred_def]) 1);
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 *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	23	by (ftac factorial_prime 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	24	by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
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
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	28	goal Ring.thy "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	29	\ [\| irred c; ALL b : set factors. irred b; a dvd <1>; \
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	wenzelm
	Sun, 07 Jan 2001 21:35:34 +0100
changeset 10816	8b2eafed6183
parent 10789	260fa2c67e3e
child 13735	7de9342aca7a
permissions	-rw-r--r--