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);
|
4091
|
13 |
by (fast_tac (claset() addSEs [RepFunE] 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 |
|
5068
|
17 |
Goalw [lesspoll_def] "!!n. 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]
|
1461
|
29 |
"!!f. [| 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 |
|
5068
|
49 |
Goalw [succ_def] "!!g. 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 |
|
5068
|
53 |
Goal "!!g. [| 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 |
|
5068
|
57 |
Goal "!!n. 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 |
|
5068
|
61 |
Goal "!!n. 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 |
|
5068
|
65 |
Goal "!!k. 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 |
|
5068
|
69 |
Goal "!!k. [| 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 |
|
5068
|
73 |
Goal "!!f. 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 |
|
5068
|
77 |
Goalw [restrict_def] "!!g. 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 |
|
5068
|
86 |
Goal "!!k. [| 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]
|
1461
|
94 |
"!!f. [| 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 |
|
5068
|
99 |
Goal "!!f. [| 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 |
|
5068
|
104 |
Goal "!!R. [| 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 |
|