author | paulson |
Tue, 04 Aug 1998 16:05:19 +0200 | |
changeset 5241 | e5129172cb2b |
parent 5147 | 825877190618 |
child 7499 | 23e090051cb8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/DC_lemmas.ML |
1196 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1196 | 4 |
|
5 |
More general lemmas used in the proofs concerning DC |
|
6 |
||
7 |
*) |
|
8 |
||
9 |
val [prem] = goalw thy [lepoll_def] |
|
1461 | 10 |
"Ord(a) ==> {P(b). b:a} lepoll a"; |
1196 | 11 |
by (res_inst_tac [("x","lam z:RepFun(a,P). LEAST i. z=P(i)")] exI 1); |
12 |
by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1); |
|
5241 | 13 |
by (fast_tac (claset() addSIs [Least_in_Ord, prem]) 1); |
1196 | 14 |
by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1)); |
3731 | 15 |
qed "RepFun_lepoll"; |
1196 | 16 |
|
5137 | 17 |
Goalw [lesspoll_def] "n:nat ==> n lesspoll nat"; |
1207 | 18 |
by (rtac conjI 1); |
1196 | 19 |
by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1); |
1207 | 20 |
by (rtac notI 1); |
21 |
by (etac eqpollE 1); |
|
22 |
by (rtac succ_lepoll_natE 1 THEN (assume_tac 2)); |
|
1196 | 23 |
by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS |
1461 | 24 |
subset_imp_lepoll) RS lepoll_trans] 1 |
25 |
THEN (assume_tac 1)); |
|
3731 | 26 |
qed "n_lesspoll_nat"; |
1196 | 27 |
|
5068 | 28 |
Goalw [lepoll_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
29 |
"[| f:X->Y; Ord(X) |] ==> f``X lepoll X"; |
1196 | 30 |
by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1); |
31 |
by (res_inst_tac [("d","%z. f`z")] lam_injective 1); |
|
4091 | 32 |
by (fast_tac (claset() addSIs [Least_in_Ord, apply_equality]) 1); |
33 |
by (fast_tac (claset() addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1); |
|
3731 | 34 |
qed "image_Ord_lepoll"; |
1196 | 35 |
|
36 |
val [major, minor] = goal thy |
|
1461 | 37 |
"[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \ |
38 |
\ |] ==> range(R) <= domain(R)"; |
|
1207 | 39 |
by (rtac subsetI 1); |
40 |
by (etac rangeE 1); |
|
1196 | 41 |
by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1); |
2469 | 42 |
by (Fast_tac 1); |
3731 | 43 |
qed "range_subset_domain"; |
1196 | 44 |
|
45 |
val prems = goal thy "!!k. k:n ==> k~=n"; |
|
4091 | 46 |
by (fast_tac (claset() addSEs [mem_irrefl]) 1); |
3731 | 47 |
qed "mem_not_eq"; |
1196 | 48 |
|
5137 | 49 |
Goalw [succ_def] "g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)"; |
4091 | 50 |
by (fast_tac (claset() addSIs [fun_extend] addSEs [mem_irrefl]) 1); |
3731 | 51 |
qed "cons_fun_type"; |
1196 | 52 |
|
5137 | 53 |
Goal "[| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X"; |
2469 | 54 |
by (etac (cons_absorb RS subst) 1 THEN etac cons_fun_type 1); |
3731 | 55 |
qed "cons_fun_type2"; |
1196 | 56 |
|
5137 | 57 |
Goal "n: nat ==> cons(<n,x>, g)``n = g``n"; |
4091 | 58 |
by (fast_tac (claset() addSEs [mem_irrefl]) 1); |
3731 | 59 |
qed "cons_image_n"; |
1196 | 60 |
|
5137 | 61 |
Goal "g:n->X ==> cons(<n,x>, g)`n = x"; |
4091 | 62 |
by (fast_tac (claset() addSIs [apply_equality] addSEs [cons_fun_type]) 1); |
3731 | 63 |
qed "cons_val_n"; |
1196 | 64 |
|
5137 | 65 |
Goal "k : n ==> cons(<n,x>, g)``k = g``k"; |
4091 | 66 |
by (fast_tac (claset() addEs [mem_asym]) 1); |
3731 | 67 |
qed "cons_image_k"; |
1196 | 68 |
|
5137 | 69 |
Goal "[| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k"; |
4091 | 70 |
by (fast_tac (claset() addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1); |
3731 | 71 |
qed "cons_val_k"; |
1196 | 72 |
|
5137 | 73 |
Goal "domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)"; |
4091 | 74 |
by (asm_full_simp_tac (simpset() addsimps [domain_cons, succ_def]) 1); |
3731 | 75 |
qed "domain_cons_eq_succ"; |
1196 | 76 |
|
5137 | 77 |
Goalw [restrict_def] "g:n->X ==> restrict(cons(<n,x>, g), n)=g"; |
1207 | 78 |
by (rtac fun_extension 1); |
79 |
by (rtac lam_type 1); |
|
1196 | 80 |
by (eresolve_tac [cons_fun_type RS apply_type] 1); |
1207 | 81 |
by (etac succI2 1); |
1196 | 82 |
by (assume_tac 1); |
4091 | 83 |
by (asm_full_simp_tac (simpset() addsimps [cons_val_k]) 1); |
3731 | 84 |
qed "restrict_cons_eq"; |
1196 | 85 |
|
5137 | 86 |
Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)"; |
1196 | 87 |
by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); |
4091 | 88 |
by (REPEAT (fast_tac (claset() addSIs [Ord_succ] |
1461 | 89 |
addEs [Ord_in_Ord, mem_irrefl, mem_asym] |
90 |
addSDs [succ_inject]) 1)); |
|
3731 | 91 |
qed "succ_in_succ"; |
1196 | 92 |
|
5068 | 93 |
Goalw [restrict_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
94 |
"[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; |
1207 | 95 |
by (etac subst 1); |
2469 | 96 |
by (Asm_full_simp_tac 1); |
3731 | 97 |
qed "restrict_eq_imp_val_eq"; |
1196 | 98 |
|
5137 | 99 |
Goal "[| domain(f)=A; f:B->C |] ==> f:A->C"; |
1196 | 100 |
by (forward_tac [domain_of_fun] 1); |
2469 | 101 |
by (Fast_tac 1); |
3731 | 102 |
qed "domain_eq_imp_fun_type"; |
1196 | 103 |
|
5137 | 104 |
Goal "[| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)"; |
4091 | 105 |
by (fast_tac (claset() addSEs [not_emptyE]) 1); |
3731 | 106 |
qed "ex_in_domain"; |
1196 | 107 |