|
1 (* Title: ZF/AC/first.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 Lemmas involving the first element of a well ordered set |
|
6 *) |
|
7 |
|
8 open first; |
|
9 |
|
10 goalw thy [first_def] "!!b. first(b,B,r) ==> b:B"; |
|
11 by (fast_tac AC_cs 1); |
|
12 val first_is_elem = result(); |
|
13 |
|
14 goalw thy [well_ord_def, wf_on_def, wf_def, exists_first_def, first_def] |
|
15 "!!r. well_ord(A,r) ==> ALL B. (B<=A & B~=0) --> exists_first(B,r)"; |
|
16 by (resolve_tac [allI] 1); |
|
17 by (resolve_tac [impI] 1); |
|
18 by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); |
|
19 by (contr_tac 1); |
|
20 by (eresolve_tac [bexE] 1); |
|
21 by (resolve_tac [bexI] 1 THEN (atac 2)); |
|
22 by (rewrite_goals_tac [tot_ord_def, linear_def]); |
|
23 by (fast_tac ZF_cs 1); |
|
24 val well_ord_imp_ex_first = result(); |
|
25 |
|
26 goalw thy [well_ord_def, wf_on_def, wf_def, first_def] |
|
27 "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; |
|
28 by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); |
|
29 by (contr_tac 1); |
|
30 by (eresolve_tac [bexE] 1); |
|
31 by (res_inst_tac [("a","x")] ex1I 1); |
|
32 by (fast_tac ZF_cs 2); |
|
33 by (rewrite_goals_tac [tot_ord_def, linear_def]); |
|
34 by (fast_tac ZF_cs 1); |
|
35 val well_ord_imp_ex1_first = result(); |
|
36 |
|
37 goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"; |
|
38 by (dresolve_tac [well_ord_imp_ex1_first] 1 THEN REPEAT (atac 1)); |
|
39 by (resolve_tac [first_is_elem] 1); |
|
40 by (eresolve_tac [theI] 1); |
|
41 val the_first_in = result(); |