equal
deleted
inserted
replaced
512 assumes "bounded_by xs vs" |
512 assumes "bounded_by xs vs" |
513 and "vs ! i = Some ivl" |
513 and "vs ! i = Some ivl" |
514 and bnd: "x \<in>\<^sub>r ivl" |
514 and bnd: "x \<in>\<^sub>r ivl" |
515 shows "bounded_by (xs[i := x]) vs" |
515 shows "bounded_by (xs[i := x]) vs" |
516 using assms |
516 using assms |
517 using nth_list_update |
|
518 by (cases "i < length xs") |
517 by (cases "i < length xs") |
519 (force simp: bounded_by_def split: option.splits)+ |
518 (force simp: bounded_by_def nth_list_update list_update_beyond split: option.splits)+ |
520 |
519 |
521 lemma isDERIV_approx': |
520 lemma isDERIV_approx': |
522 assumes "bounded_by xs vs" |
521 assumes "bounded_by xs vs" |
523 and vs_x: "vs ! x = Some ivl" |
522 and vs_x: "vs ! x = Some ivl" |
524 and X_in: "X \<in>\<^sub>r ivl" |
523 and X_in: "X \<in>\<^sub>r ivl" |