10 "Ord(a) ==> {P(b). b:a} lepoll a"; |
10 "Ord(a) ==> {P(b). b:a} lepoll a"; |
11 by (res_inst_tac [("x","lam z:RepFun(a,P). LEAST i. z=P(i)")] exI 1); |
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); |
12 by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1); |
13 by (fast_tac (!claset addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1); |
13 by (fast_tac (!claset addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1); |
14 by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1)); |
14 by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1)); |
15 val RepFun_lepoll = result(); |
15 qed "RepFun_lepoll"; |
16 |
16 |
17 goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat"; |
17 goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat"; |
18 by (rtac conjI 1); |
18 by (rtac conjI 1); |
19 by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1); |
19 by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1); |
20 by (rtac notI 1); |
20 by (rtac notI 1); |
21 by (etac eqpollE 1); |
21 by (etac eqpollE 1); |
22 by (rtac succ_lepoll_natE 1 THEN (assume_tac 2)); |
22 by (rtac succ_lepoll_natE 1 THEN (assume_tac 2)); |
23 by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS |
23 by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS |
24 subset_imp_lepoll) RS lepoll_trans] 1 |
24 subset_imp_lepoll) RS lepoll_trans] 1 |
25 THEN (assume_tac 1)); |
25 THEN (assume_tac 1)); |
26 val n_lesspoll_nat = result(); |
26 qed "n_lesspoll_nat"; |
27 |
27 |
28 goalw thy [lepoll_def] |
28 goalw thy [lepoll_def] |
29 "!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X"; |
29 "!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X"; |
30 by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1); |
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); |
31 by (res_inst_tac [("d","%z. f`z")] lam_injective 1); |
32 by (fast_tac (!claset addSIs [Least_in_Ord, apply_equality]) 1); |
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); |
33 by (fast_tac (!claset addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1); |
34 val image_Ord_lepoll = result(); |
34 qed "image_Ord_lepoll"; |
35 |
35 |
36 val [major, minor] = goal thy |
36 val [major, minor] = goal thy |
37 "[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \ |
37 "[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \ |
38 \ |] ==> range(R) <= domain(R)"; |
38 \ |] ==> range(R) <= domain(R)"; |
39 by (rtac subsetI 1); |
39 by (rtac subsetI 1); |
40 by (etac rangeE 1); |
40 by (etac rangeE 1); |
41 by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1); |
41 by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1); |
42 by (Fast_tac 1); |
42 by (Fast_tac 1); |
43 val range_subset_domain = result(); |
43 qed "range_subset_domain"; |
44 |
44 |
45 val prems = goal thy "!!k. k:n ==> k~=n"; |
45 val prems = goal thy "!!k. k:n ==> k~=n"; |
46 by (fast_tac (!claset addSEs [mem_irrefl]) 1); |
46 by (fast_tac (!claset addSEs [mem_irrefl]) 1); |
47 val mem_not_eq = result(); |
47 qed "mem_not_eq"; |
48 |
48 |
49 goalw thy [succ_def] "!!g. g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)"; |
49 goalw thy [succ_def] "!!g. g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)"; |
50 by (fast_tac (!claset addSIs [fun_extend] addSEs [mem_irrefl]) 1); |
50 by (fast_tac (!claset addSIs [fun_extend] addSEs [mem_irrefl]) 1); |
51 val cons_fun_type = result(); |
51 qed "cons_fun_type"; |
52 |
52 |
53 goal thy "!!g. [| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X"; |
53 goal thy "!!g. [| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X"; |
54 by (etac (cons_absorb RS subst) 1 THEN etac cons_fun_type 1); |
54 by (etac (cons_absorb RS subst) 1 THEN etac cons_fun_type 1); |
55 val cons_fun_type2 = result(); |
55 qed "cons_fun_type2"; |
56 |
56 |
57 goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n"; |
57 goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n"; |
58 by (fast_tac (!claset addSEs [mem_irrefl]) 1); |
58 by (fast_tac (!claset addSEs [mem_irrefl]) 1); |
59 val cons_image_n = result(); |
59 qed "cons_image_n"; |
60 |
60 |
61 goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x"; |
61 goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x"; |
62 by (fast_tac (!claset addSIs [apply_equality] addSEs [cons_fun_type]) 1); |
62 by (fast_tac (!claset addSIs [apply_equality] addSEs [cons_fun_type]) 1); |
63 val cons_val_n = result(); |
63 qed "cons_val_n"; |
64 |
64 |
65 goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k"; |
65 goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k"; |
66 by (fast_tac (!claset addEs [mem_asym]) 1); |
66 by (fast_tac (!claset addEs [mem_asym]) 1); |
67 val cons_image_k = result(); |
67 qed "cons_image_k"; |
68 |
68 |
69 goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k"; |
69 goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k"; |
70 by (fast_tac (!claset addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1); |
70 by (fast_tac (!claset addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1); |
71 val cons_val_k = result(); |
71 qed "cons_val_k"; |
72 |
72 |
73 goal thy "!!f. domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)"; |
73 goal thy "!!f. domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)"; |
74 by (asm_full_simp_tac (!simpset addsimps [domain_cons, succ_def]) 1); |
74 by (asm_full_simp_tac (!simpset addsimps [domain_cons, succ_def]) 1); |
75 val domain_cons_eq_succ = result(); |
75 qed "domain_cons_eq_succ"; |
76 |
76 |
77 goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(<n,x>, g), n)=g"; |
77 goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(<n,x>, g), n)=g"; |
78 by (rtac fun_extension 1); |
78 by (rtac fun_extension 1); |
79 by (rtac lam_type 1); |
79 by (rtac lam_type 1); |
80 by (eresolve_tac [cons_fun_type RS apply_type] 1); |
80 by (eresolve_tac [cons_fun_type RS apply_type] 1); |
81 by (etac succI2 1); |
81 by (etac succI2 1); |
82 by (assume_tac 1); |
82 by (assume_tac 1); |
83 by (asm_full_simp_tac (!simpset addsimps [cons_val_k]) 1); |
83 by (asm_full_simp_tac (!simpset addsimps [cons_val_k]) 1); |
84 val restrict_cons_eq = result(); |
84 qed "restrict_cons_eq"; |
85 |
85 |
86 goal thy "!!k. [| Ord(k); i:k |] ==> succ(i) : succ(k)"; |
86 goal thy "!!k. [| Ord(k); i:k |] ==> succ(i) : succ(k)"; |
87 by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); |
87 by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); |
88 by (REPEAT (fast_tac (!claset addSIs [Ord_succ] |
88 by (REPEAT (fast_tac (!claset addSIs [Ord_succ] |
89 addEs [Ord_in_Ord, mem_irrefl, mem_asym] |
89 addEs [Ord_in_Ord, mem_irrefl, mem_asym] |
90 addSDs [succ_inject]) 1)); |
90 addSDs [succ_inject]) 1)); |
91 val succ_in_succ = result(); |
91 qed "succ_in_succ"; |
92 |
92 |
93 goalw thy [restrict_def] |
93 goalw thy [restrict_def] |
94 "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; |
94 "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; |
95 by (etac subst 1); |
95 by (etac subst 1); |
96 by (Asm_full_simp_tac 1); |
96 by (Asm_full_simp_tac 1); |
97 val restrict_eq_imp_val_eq = result(); |
97 qed "restrict_eq_imp_val_eq"; |
98 |
98 |
99 goal thy "!!f. [| domain(f)=A; f:B->C |] ==> f:A->C"; |
99 goal thy "!!f. [| domain(f)=A; f:B->C |] ==> f:A->C"; |
100 by (forward_tac [domain_of_fun] 1); |
100 by (forward_tac [domain_of_fun] 1); |
101 by (Fast_tac 1); |
101 by (Fast_tac 1); |
102 val domain_eq_imp_fun_type = result(); |
102 qed "domain_eq_imp_fun_type"; |
103 |
103 |
104 goal thy "!!R. [| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)"; |
104 goal thy "!!R. [| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)"; |
105 by (fast_tac (!claset addSEs [not_emptyE]) 1); |
105 by (fast_tac (!claset addSEs [not_emptyE]) 1); |
106 val ex_in_domain = result(); |
106 qed "ex_in_domain"; |
107 |
107 |