1166 --------------------------------------------*) |
1166 --------------------------------------------*) |
1167 Goal "(%n. r + inverse(real(Suc n))) ----> r"; |
1167 Goal "(%n. r + inverse(real(Suc n))) ----> r"; |
1168 by (cut_facts_tac |
1168 by (cut_facts_tac |
1169 [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1); |
1169 [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1); |
1170 by Auto_tac; |
1170 by Auto_tac; |
1171 qed "LIMSEQ_inverse_real_of_posnat_add"; |
1171 qed "LIMSEQ_inverse_real_of_nat_add"; |
1172 |
1172 |
1173 Goal "(%n. r + inverse(real(Suc n))) ----NS> r"; |
1173 Goal "(%n. r + inverse(real(Suc n))) ----NS> r"; |
1174 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1174 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1175 LIMSEQ_inverse_real_of_posnat_add]) 1); |
1175 LIMSEQ_inverse_real_of_nat_add]) 1); |
1176 qed "NSLIMSEQ_inverse_real_of_posnat_add"; |
1176 qed "NSLIMSEQ_inverse_real_of_nat_add"; |
1177 |
1177 |
1178 (*-------------- |
1178 (*-------------- |
1179 Also... |
1179 Also... |
1180 --------------*) |
1180 --------------*) |
1181 |
1181 |
1182 Goal "(%n. r + -inverse(real(Suc n))) ----> r"; |
1182 Goal "(%n. r + -inverse(real(Suc n))) ----> r"; |
1183 by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat] |
1183 by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat] |
1184 MRS LIMSEQ_add_minus] 1); |
1184 MRS LIMSEQ_add_minus] 1); |
1185 by (Auto_tac); |
1185 by (Auto_tac); |
1186 qed "LIMSEQ_inverse_real_of_posnat_add_minus"; |
1186 qed "LIMSEQ_inverse_real_of_nat_add_minus"; |
1187 |
1187 |
1188 Goal "(%n. r + -inverse(real(Suc n))) ----NS> r"; |
1188 Goal "(%n. r + -inverse(real(Suc n))) ----NS> r"; |
1189 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1189 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1190 LIMSEQ_inverse_real_of_posnat_add_minus]) 1); |
1190 LIMSEQ_inverse_real_of_nat_add_minus]) 1); |
1191 qed "NSLIMSEQ_inverse_real_of_posnat_add_minus"; |
1191 qed "NSLIMSEQ_inverse_real_of_nat_add_minus"; |
1192 |
1192 |
1193 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"; |
1193 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"; |
1194 by (cut_inst_tac [("b","1")] ([LIMSEQ_const, |
1194 by (cut_inst_tac [("b","1")] ([LIMSEQ_const, |
1195 LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1); |
1195 LIMSEQ_inverse_real_of_nat_add_minus] MRS LIMSEQ_mult) 1); |
1196 by (Auto_tac); |
1196 by (Auto_tac); |
1197 qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult"; |
1197 qed "LIMSEQ_inverse_real_of_nat_add_minus_mult"; |
1198 |
1198 |
1199 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"; |
1199 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"; |
1200 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1200 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, |
1201 LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1); |
1201 LIMSEQ_inverse_real_of_nat_add_minus_mult]) 1); |
1202 qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult"; |
1202 qed "NSLIMSEQ_inverse_real_of_nat_add_minus_mult"; |
1203 |
1203 |
1204 (*--------------------------------------------------------------- |
1204 (*--------------------------------------------------------------- |
1205 Real Powers |
1205 Real Powers |
1206 --------------------------------------------------------------*) |
1206 --------------------------------------------------------------*) |
1207 Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"; |
1207 Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"; |