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