author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 1208 | bc3093616ba4 |
child 1461 | 6bcb44e4d6e5 |
permissions | -rw-r--r-- |
1123 | 1 |
(* Title: ZF/AC/first.ML |
2 |
ID: $Id$ |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
3 |
Author: Krzysztof Grabczewski |
1123 | 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, first_def] |
|
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)); |
|
17 |
by (contr_tac 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
18 |
by (etac bexE 1); |
1123 | 19 |
by (res_inst_tac [("a","x")] ex1I 1); |
20 |
by (fast_tac ZF_cs 2); |
|
21 |
by (rewrite_goals_tac [tot_ord_def, linear_def]); |
|
22 |
by (fast_tac ZF_cs 1); |
|
23 |
val well_ord_imp_ex1_first = result(); |
|
24 |
||
25 |
goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
26 |
by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1)); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
27 |
by (rtac first_is_elem 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
28 |
by (etac theI 1); |
1123 | 29 |
val the_first_in = result(); |