equal
deleted
inserted
replaced
959 proof (intro exI conjI strip) |
959 proof (intro exI conjI strip) |
960 show "0<s" using s . |
960 show "0<s" using s . |
961 fix h::real |
961 fix h::real |
962 assume "0 < h" "h < s" |
962 assume "0 < h" "h < s" |
963 with all [of h] show "f x < f (x+h)" |
963 with all [of h] show "f x < f (x+h)" |
964 proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm) |
964 proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm) |
965 assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" |
965 assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" |
966 with l |
966 with l |
967 have "0 < (f (x+h) - f x) / h" by arith |
967 have "0 < (f (x+h) - f x) / h" by arith |
968 thus "f x < f (x+h)" |
968 thus "f x < f (x+h)" |
969 by (simp add: pos_less_divide_eq h) |
969 by (simp add: pos_less_divide_eq h) |
988 proof (intro exI conjI strip) |
988 proof (intro exI conjI strip) |
989 show "0<s" using s . |
989 show "0<s" using s . |
990 fix h::real |
990 fix h::real |
991 assume "0 < h" "h < s" |
991 assume "0 < h" "h < s" |
992 with all [of "-h"] show "f x < f (x-h)" |
992 with all [of "-h"] show "f x < f (x-h)" |
993 proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm) |
993 proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm) |
994 assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" |
994 assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" |
995 with l |
995 with l |
996 have "0 < (f (x-h) - f x) / h" by arith |
996 have "0 < (f (x-h) - f x) / h" by arith |
997 thus "f x < f (x-h)" |
997 thus "f x < f (x-h)" |
998 by (simp add: pos_less_divide_eq h) |
998 by (simp add: pos_less_divide_eq h) |