equal
deleted
inserted
replaced
48 \ cmod (xa - x) < s & r <= cmod (f xa - L)) \ |
48 \ cmod (xa - x) < s & r <= cmod (f xa - L)) \ |
49 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
49 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
50 \ cmod(xa - x) < inverse(real(Suc n)) & r <= cmod(f xa - L)"; |
50 \ cmod(xa - x) < inverse(real(Suc n)) & r <= cmod(f xa - L)"; |
51 by (Clarify_tac 1); |
51 by (Clarify_tac 1); |
52 by (cut_inst_tac [("n1","n")] |
52 by (cut_inst_tac [("n1","n")] |
53 (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); |
53 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
54 by Auto_tac; |
54 by Auto_tac; |
55 val lemma_CLIM = result(); |
55 val lemma_CLIM = result(); |
56 |
56 |
57 (* not needed? *) |
57 (* not needed? *) |
58 Goal "ALL x z. EX y. Q x z y ==> EX f. ALL x z. Q x z (f x z)"; |
58 Goal "ALL x z. EX y. Q x z y ==> EX f. ALL x z. Q x z (f x z)"; |
130 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |
130 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |
131 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
131 \ ==> ALL (n::nat). EX xa. xa ~= x & \ |
132 \ cmod(xa - x) < inverse(real(Suc n)) & r <= abs (f xa - L)"; |
132 \ cmod(xa - x) < inverse(real(Suc n)) & r <= abs (f xa - L)"; |
133 by (Clarify_tac 1); |
133 by (Clarify_tac 1); |
134 by (cut_inst_tac [("n1","n")] |
134 by (cut_inst_tac [("n1","n")] |
135 (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); |
135 (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); |
136 by Auto_tac; |
136 by Auto_tac; |
137 val lemma_CRLIM = result(); |
137 val lemma_CRLIM = result(); |
138 |
138 |
139 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
139 Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ |
140 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |
140 \ cmod (xa - x) < s & r <= abs (f xa - L)) \ |