equal
deleted
inserted
replaced
31 by (rtac (major RS finite_induct) 1); |
31 by (rtac (major RS finite_induct) 1); |
32 by (ALLGOALS (blast_tac (claset() addIs prems))); |
32 by (ALLGOALS (blast_tac (claset() addIs prems))); |
33 val lemma_induct = result(); |
33 val lemma_induct = result(); |
34 |
34 |
35 Goalw [inj_on_def] |
35 Goalw [inj_on_def] |
36 "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f``A"; |
36 "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f`A"; |
37 by Auto_tac; |
37 by Auto_tac; |
38 val lemma = result(); |
38 val lemma = result(); |
39 |
39 |
40 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \ |
40 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \ |
41 \ ==> (F,f``F) : bijR P"; |
41 \ ==> (F,f`F) : bijR P"; |
42 by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1); |
42 by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1); |
43 by (rtac finite_subset 1); |
43 by (rtac finite_subset 1); |
44 by Auto_tac; |
44 by Auto_tac; |
45 by (rtac bijR.insert 1); |
45 by (rtac bijR.insert 1); |
46 by (rtac lemma 3); |
46 by (rtac lemma 3); |
47 by Auto_tac; |
47 by Auto_tac; |
48 val lemma = result(); |
48 val lemma = result(); |
49 |
49 |
50 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \ |
50 Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \ |
51 \ ==> (A,f``A) : bijR P"; |
51 \ ==> (A,f`A) : bijR P"; |
52 by (rtac lemma 1); |
52 by (rtac lemma 1); |
53 by Auto_tac; |
53 by Auto_tac; |
54 qed "inj_func_bijR"; |
54 qed "inj_func_bijR"; |
55 |
55 |
56 |
56 |