equal
deleted
inserted
replaced
31 \ EX d. c assoc d & d : set factors"; |
31 \ EX d. c assoc d & d : set factors"; |
32 by (rtac (irred_dvd_list_lemma RS mp) 1); |
32 by (rtac (irred_dvd_list_lemma RS mp) 1); |
33 by (Auto_tac); |
33 by (Auto_tac); |
34 qed "irred_dvd_list"; |
34 qed "irred_dvd_list"; |
35 |
35 |
36 Goalw [Factorisation_def] "!! c::'a::factorial. \ |
36 Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \ |
37 \ [| irred c; Factorisation x factors u; c dvd x |] ==> \ |
37 \ [| irred c; Factorisation x factors u; c dvd x |] ==> \ |
38 \ EX d. c assoc d & d : set factors"; |
38 \ EX d. c assoc d & d : set factors"; |
39 by (rtac (irred_dvd_list_lemma RS mp) 1); |
39 by (rtac (irred_dvd_list_lemma RS mp) 1); |
40 by (Auto_tac); |
40 by (Auto_tac); |
41 qed "Factorisation_dvd"; |
41 qed "Factorisation_dvd"; |
42 |
42 |
43 Goalw [Factorisation_def] "!! c::'a::factorial. \ |
43 Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \ |
44 \ [| Factorisation x factors u; a : set factors |] ==> irred a"; |
44 \ [| Factorisation x factors u; a : set factors |] ==> irred a"; |
45 by (Blast_tac 1); |
45 by (Blast_tac 1); |
46 qed "Factorisation_irred"; |
46 qed "Factorisation_irred"; |
47 |
47 |