1 (* Title: ZF/AC/first.ML |
1 (* Title: ZF/AC/first.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Lemmas involving the first element of a well ordered set |
5 Lemmas involving the first element of a well ordered set |
6 *) |
6 *) |
7 |
7 |
8 open first; |
8 open first; |
9 |
9 |
10 goalw thy [first_def] "!!b. first(b,B,r) ==> b:B"; |
10 goalw thy [first_def] "!!b. first(b,B,r) ==> b:B"; |
11 by (fast_tac AC_cs 1); |
11 by (fast_tac AC_cs 1); |
12 val first_is_elem = result(); |
12 val first_is_elem = result(); |
13 |
13 |
14 goalw thy [well_ord_def, wf_on_def, wf_def, first_def] |
14 goalw thy [well_ord_def, wf_on_def, wf_def, first_def] |
15 "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; |
15 "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; |
16 by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); |
16 by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); |
17 by (contr_tac 1); |
17 by (contr_tac 1); |
18 by (etac bexE 1); |
18 by (etac bexE 1); |
19 by (res_inst_tac [("a","x")] ex1I 1); |
19 by (res_inst_tac [("a","x")] ex1I 1); |
20 by (fast_tac ZF_cs 2); |
20 by (fast_tac ZF_cs 2); |