isabelle: src/HOL/Algebra/abstract/Factor.ML@38e58ed53e7b (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	open Factor;
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10	\ [\| irred c; irred a; irred b; c dvd (a*b) \|] ==> c assoc a \| c assoc b";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	by (ftac factorial_prime 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	by (rewrite_goals_tac [irred_def, prime_def]);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	qed "irred_dvd_lemma";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17	\ [\| irred c; a dvd <1> \|] ==> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	\ (EX d. c assoc d & d : set factors)";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20	by (induct_tac "factors" 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21	(* Base case: c dvd a contradicts irred c *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22	by (full_simp_tac (simpset() addsimps [irred_def]) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	23	by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	24	(* Induction step *)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	25	by (ftac factorial_prime 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	26	by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	27	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	28	qed "irred_dvd_list_lemma";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	29
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	30	goal Ring.thy "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	31	\ [\| irred c; ALL b : set factors. irred b; a dvd <1>; \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	32	\ c dvd foldr op* factors a \|] ==> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	33	\ EX d. c assoc d & d : set factors";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	34	by (rtac (irred_dvd_list_lemma RS mp) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	35	by (Auto_tac);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	36	qed "irred_dvd_list";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	37
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	38	Goalw [Factorisation_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	39	\ [\| irred c; Factorisation x factors u; c dvd x \|] ==> \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	40	\ EX d. c assoc d & d : set factors";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	41	by (rtac (irred_dvd_list_lemma RS mp) 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	42	by (Auto_tac);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	43	qed "Factorisation_dvd";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	44
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	45	Goalw [Factorisation_def] "!! c::'a::factorial. \
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	46	\ [\| Factorisation x factors u; a : set factors \|] ==> irred a";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	47	by (Blast_tac 1);
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	48	qed "Factorisation_irred";
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	49

author	paulson
	Sat, 12 Aug 2000 21:41:42 +0200
changeset 9582	38e58ed53e7b
parent 7998	3d0c34795831
child 10448	da7d0e28f746
permissions	-rw-r--r--